Merge pull request #853 from o1-labs/feature/remove-polymorphism

[trivial] Remove polymorphism from field in `Checked_intf`

src/base/as_prover0.ml

@@ -82,17 +82,15 @@ module Handle = struct
 end
 
 module type Extended = sig
-  type field
-
-  include As_prover_intf.Basic with type 'f field := field
+  include As_prover_intf.Basic
 
   type nonrec 'a t = ('a, field) t
 end
 
 module Make_extended (Env : sig
   type field
 end)
-(As_prover : As_prover_intf.Basic with type 'f field := Env.field) =
+(As_prover : As_prover_intf.Basic with type field := Env.field) =
 struct
   include Env
   include As_prover

src/base/as_prover_intf.ml

@@ -1,34 +1,27 @@
 module type Basic = sig
   type ('a, 'f) t = ('a, 'f) Types.As_prover.t
 
-  type 'f field
+  type field
 
-  include Monad_let.S2 with type ('a, 'f) t := ('a, 'f field) t
+  include Monad_let.S2 with type ('a, 'f) t := ('a, field) t
 
-  val run : ('a, 'f field) t -> ('f field Cvar.t -> 'f field) -> 'a
+  val run : ('a, field) t -> (field Cvar.t -> field) -> 'a
 
   val map2 :
-       ('a, 'f field) t
-    -> ('b, 'f field) t
-    -> f:('a -> 'b -> 'c)
-    -> ('c, 'f field) t
+    ('a, field) t -> ('b, field) t -> f:('a -> 'b -> 'c) -> ('c, field) t
 
-  val read_var : 'f field Cvar.t -> ('f field, 'f field) t
+  val read_var : field Cvar.t -> (field, field) t
 
-  val read :
-    ('var, 'value, 'f field, _) Types.Typ.t -> 'var -> ('value, 'f field) t
+  val read : ('var, 'value, field, _) Types.Typ.t -> 'var -> ('value, field) t
 
   module Provider : sig
     type ('a, 'f) t
 
     val run :
-         ('a, 'f field) t
-      -> ('f field Cvar.t -> 'f field)
-      -> Request.Handler.t
-      -> 'a option
+      ('a, field) t -> (field Cvar.t -> field) -> Request.Handler.t -> 'a option
   end
 
   module Handle : sig
-    val value : ('var, 'value) Handle.t -> ('value, 'f field) Types.As_prover.t
+    val value : ('var, 'value) Handle.t -> ('value, field) Types.As_prover.t
   end
 end

src/base/checked.ml

@@ -5,15 +5,14 @@ module Make (Field : sig
 
   val equal : t -> t -> bool
 end)
-(Basic : Checked_intf.Basic with type 'f field = Field.t)
-(As_prover : As_prover_intf.Basic with type 'f field := 'f Basic.field) :
-  Checked_intf.S
-    with module Types = Basic.Types
-    with type 'f field = 'f Basic.field = struct
+(Basic : Checked_intf.Basic with type field = Field.t)
+(As_prover : As_prover_intf.Basic with type field := Basic.field) :
+  Checked_intf.S with module Types = Basic.Types with type field = Basic.field =
+struct
   include Basic
 
-  let request_witness (typ : ('var, 'value, 'f field) Types.Typ.t)
-      (r : ('value Request.t, 'f field) As_prover.t) =
+  let request_witness (typ : ('var, 'value, field) Types.Typ.t)
+      (r : ('value Request.t, field) As_prover.t) =
     let%map h = exists typ (Request r) in
     Handle.var h
 

src/base/checked_intf.ml

@@ -3,36 +3,34 @@ module type Basic = sig
 
   type ('a, 'f) t = ('a, 'f) Types.Checked.t
 
-  type 'f field
+  type field
 
   include Monad_let.S2 with type ('a, 'f) t := ('a, 'f) t
 
-  val add_constraint :
-    ('f field Cvar.t, 'f field) Constraint.t -> (unit, 'f field) t
+  val add_constraint : (field Cvar.t, field) Constraint.t -> (unit, field) t
 
-  val as_prover : (unit, 'f field) As_prover0.t -> (unit, 'f field) t
+  val as_prover : (unit, field) As_prover0.t -> (unit, field) t
 
   val mk_lazy : (unit -> ('a, 'f) t) -> ('a Lazy.t, 'f) t
 
-  val with_label : string -> (unit -> ('a, 'f field) t) -> ('a, 'f field) t
+  val with_label : string -> (unit -> ('a, field) t) -> ('a, field) t
 
   val with_handler :
-    Request.Handler.single -> (unit -> ('a, 'f field) t) -> ('a, 'f field) t
+    Request.Handler.single -> (unit -> ('a, field) t) -> ('a, field) t
 
   val exists :
-       ('var, 'value, 'f field) Types.Typ.t
-    -> ('value, 'f field) Types.Provider.t
-    -> (('var, 'value) Handle.t, 'f field) t
+       ('var, 'value, field) Types.Typ.t
+    -> ('value, field) Types.Provider.t
+    -> (('var, 'value) Handle.t, field) t
 
-  val next_auxiliary : unit -> (int, 'f field) t
+  val next_auxiliary : unit -> (int, field) t
 
-  val direct :
-    ('f field Run_state.t -> 'f field Run_state.t * 'a) -> ('a, 'f field) t
+  val direct : (field Run_state.t -> field Run_state.t * 'a) -> ('a, field) t
 
   val constraint_count :
-       ?weight:(('f field Cvar.t, 'f field) Constraint.t -> int)
+       ?weight:((field Cvar.t, field) Constraint.t -> int)
     -> ?log:(?start:bool -> string -> int -> unit)
-    -> (unit -> ('a, 'f field) t)
+    -> (unit -> ('a, field) t)
     -> int
 end
 
@@ -41,36 +39,36 @@ module type S = sig
 
   type ('a, 'f) t = ('a, 'f) Types.Checked.t
 
-  type 'f field
+  type field
 
   include Monad_let.S2 with type ('a, 'f) t := ('a, 'f) t
 
-  val as_prover : (unit, 'f field) As_prover0.t -> (unit, 'f field) t
+  val as_prover : (unit, field) As_prover0.t -> (unit, field) t
 
   val mk_lazy : (unit -> ('a, 'f) t) -> ('a Lazy.t, 'f) t
 
   val request_witness :
-       ('var, 'value, 'f field) Types.Typ.t
-    -> ('value Request.t, 'f field) As_prover0.t
-    -> ('var, 'f field) t
+       ('var, 'value, field) Types.Typ.t
+    -> ('value Request.t, field) As_prover0.t
+    -> ('var, field) t
 
   val request :
-       ?such_that:('var -> (unit, 'f field) t)
-    -> ('var, 'value, 'f field) Types.Typ.t
+       ?such_that:('var -> (unit, field) t)
+    -> ('var, 'value, field) Types.Typ.t
     -> 'value Request.t
-    -> ('var, 'f field) t
+    -> ('var, field) t
 
   val exists_handle :
-       ?request:('value Request.t, 'f field) As_prover0.t
-    -> ?compute:('value, 'f field) As_prover0.t
-    -> ('var, 'value, 'f field) Types.Typ.t
-    -> (('var, 'value) Handle.t, 'f field) t
+       ?request:('value Request.t, field) As_prover0.t
+    -> ?compute:('value, field) As_prover0.t
+    -> ('var, 'value, field) Types.Typ.t
+    -> (('var, 'value) Handle.t, field) t
 
   val exists :
-       ?request:('value Request.t, 'f field) As_prover0.t
-    -> ?compute:('value, 'f field) As_prover0.t
-    -> ('var, 'value, 'f field) Types.Typ.t
-    -> ('var, 'f field) t
+       ?request:('value Request.t, field) As_prover0.t
+    -> ?compute:('value, field) As_prover0.t
+    -> ('var, 'value, field) Types.Typ.t
+    -> ('var, field) t
 
   type response = Request.response
 
@@ -81,54 +79,44 @@ module type S = sig
         { request : 'a Request.t; respond : 'a Request.Response.t -> response }
         -> request
 
-  val handle :
-    (unit -> ('a, 'f field) t) -> (request -> response) -> ('a, 'f field) t
+  val handle : (unit -> ('a, field) t) -> (request -> response) -> ('a, field) t
 
   val handle_as_prover :
-       (unit -> ('a, 'f field) t)
-    -> (request -> response, 'f field) As_prover0.t
-    -> ('a, 'f field) t
+       (unit -> ('a, field) t)
+    -> (request -> response, field) As_prover0.t
+    -> ('a, field) t
 
-  val next_auxiliary : unit -> (int, 'f field) t
+  val next_auxiliary : unit -> (int, field) t
 
-  val with_label : string -> (unit -> ('a, 'f field) t) -> ('a, 'f field) t
+  val with_label : string -> (unit -> ('a, field) t) -> ('a, field) t
 
   val assert_ :
-       ?label:Base.string
-    -> ('f field Cvar.t, 'f field) Constraint.t
-    -> (unit, 'f field) t
+    ?label:Base.string -> (field Cvar.t, field) Constraint.t -> (unit, field) t
 
   val assert_r1cs :
        ?label:Base.string
-    -> 'f field Cvar.t
-    -> 'f field Cvar.t
-    -> 'f field Cvar.t
-    -> (unit, 'f field) t
+    -> field Cvar.t
+    -> field Cvar.t
+    -> field Cvar.t
+    -> (unit, field) t
 
   val assert_square :
-       ?label:Base.string
-    -> 'f field Cvar.t
-    -> 'f field Cvar.t
-    -> (unit, 'f field) t
+    ?label:Base.string -> field Cvar.t -> field Cvar.t -> (unit, field) t
 
   val assert_all :
        ?label:Base.string
-    -> ('f field Cvar.t, 'f field) Constraint.t list
-    -> (unit, 'f field) t
+    -> (field Cvar.t, field) Constraint.t list
+    -> (unit, field) t
 
   val assert_equal :
-       ?label:Base.string
-    -> 'f field Cvar.t
-    -> 'f field Cvar.t
-    -> (unit, 'f field) t
+    ?label:Base.string -> field Cvar.t -> field Cvar.t -> (unit, field) t
 
-  val direct :
-    ('f field Run_state.t -> 'f field Run_state.t * 'a) -> ('a, 'f field) t
+  val direct : (field Run_state.t -> field Run_state.t * 'a) -> ('a, field) t
 
   val constraint_count :
-       ?weight:(('f field Cvar.t, 'f field) Constraint.t -> int)
+       ?weight:((field Cvar.t, field) Constraint.t -> int)
     -> ?log:(?start:bool -> string -> int -> unit)
-    -> (unit -> ('a, 'f field) t)
+    -> (unit -> ('a, field) t)
     -> int
 end
 
@@ -142,23 +130,22 @@ module type Extended = sig
   include
     S
       with module Types := Types
-      with type 'f field := field
+      with type field := field
        and type ('a, 'f) t := ('a, 'f) Types.Checked.t
 
   val run : 'a t -> field Run_state.t -> field Run_state.t * 'a
 end
 
 module Unextend (Checked : Extended) :
-  S with module Types = Checked.Types with type 'f field = Checked.field =
-struct
+  S with module Types = Checked.Types with type field = Checked.field = struct
   include (
     Checked :
       S
         with module Types = Checked.Types
-        with type 'f field := Checked.field
+        with type field := Checked.field
          and type ('a, 'f) t := ('a, 'f) Checked.Types.Checked.t )
 
-  type 'f field = Checked.field
+  type field = Checked.field
 
   type ('a, 'f) t = ('a, 'f) Types.Checked.t
 end

src/base/checked_runner.ml

@@ -68,7 +68,7 @@ end
 
 module Make_checked
     (Backend : Backend_extended.S)
-    (As_prover : As_prover_intf.Basic with type 'f field := Backend.Field.t) =
+    (As_prover : As_prover_intf.Basic with type field := Backend.Field.t) =
 struct
   type run_state = Backend.Field.t Run_state.t
 
@@ -91,7 +91,7 @@ struct
     end
   end
 
-  type 'f field = Backend.Field.t
+  type field = Backend.Field.t
 
   include Types.Checked
 
@@ -361,7 +361,7 @@ module Make (Backend : Backend_extended.S) = struct
         include
           Checked_intf.Basic
             with module Types := Checked_runner.Types
-            with type 'f field := 'f Checked_runner.field
+            with type field := Checked_runner.field
 
         include
           Run_extras

src/base/snark0.ml

@@ -661,7 +661,7 @@ module Make (Backend : Backend_intf.S) = struct
         Checked_intf.S
           with module Types = Checked1.Types
           with type ('a, 'f) t := ('a, 'f) Checked1.t
-           and type 'f field := Backend_extended.Field.t )
+           and type field := Backend_extended.Field.t )
 
     type field = Backend_extended.Field.t
 

src/base/typ.ml

@@ -77,7 +77,7 @@ end
 module type Checked_monad = sig
   type ('a, 'f) t
 
-  type 'f field
+  type field
 
   include Monad_let.S2 with type ('a, 'e) t := ('a, 'e) t