Remove polymorphism from As_prover.t, hoist Typ.t

src/base/as_prover0.ml

@@ -1,53 +1,56 @@
 open Core_kernel
 
-type ('a, 'f) t = ('a, 'f) Types.As_prover.t
+module Make
+    (Types : Types.Types
+               with type ('a, 'f) As_prover.t = ('f Cvar.t -> 'f) -> 'a) =
+struct
+  type ('a, 'f) t = ('a, 'f) Types.As_prover.t
 
-let map t ~f tbl =
-  let x = t tbl in
-  f x
+  let map t ~f tbl =
+    let x = t tbl in
+    f x
 
-let bind t ~f tbl =
-  let x = t tbl in
-  f x tbl
+  let bind t ~f tbl =
+    let x = t tbl in
+    f x tbl
 
-let return x _ = x
+  let return x _ = x
 
-let run t tbl = t tbl
+  let run t tbl = t tbl
 
-let get_state _tbl s = (s, s)
+  let get_state _tbl s = (s, s)
 
-let set_state s _tbl _ = (s, ())
+  let set_state s _tbl _ = (s, ())
 
-let modify_state f _tbl s = (f s, ())
+  let modify_state f _tbl s = (f s, ())
 
-let map2 x y ~f tbl =
-  let x = x tbl in
-  let y = y tbl in
-  f x y
+  let map2 x y ~f tbl =
+    let x = x tbl in
+    let y = y tbl in
+    f x y
 
-let read_var (v : 'var) : ('field, 'field) t = fun tbl -> tbl v
+  let read_var (v : 'var) : ('field, 'field) t = fun tbl -> tbl v
 
-let read
-    (Typ { var_to_fields; value_of_fields; _ } :
-      ('var, 'value, 'field, _) Types.Typ.t ) (var : 'var) : ('value, 'field) t
-    =
- fun tbl ->
-  let field_vars, aux = var_to_fields var in
-  let fields = Array.map ~f:tbl field_vars in
-  value_of_fields (fields, aux)
+  let read
+      (Typ { var_to_fields; value_of_fields; _ } :
+        ('var, 'value, 'field) Types.Typ.t ) (var : 'var) : ('value, 'field) t =
+   fun tbl ->
+    let field_vars, aux = var_to_fields var in
+    let fields = Array.map ~f:tbl field_vars in
+    value_of_fields (fields, aux)
 
-include Monad_let.Make2 (struct
-  type nonrec ('a, 'e) t = ('a, 'e) t
+  include Monad_let.Make2 (struct
+    type nonrec ('a, 'e) t = ('a, 'e) t
 
-  let map = `Custom map
+    let map = `Custom map
 
-  let bind = bind
+    let bind = bind
 
-  let return = return
-end)
+    let return = return
+  end)
 
-module Provider = struct
-  (** The different ways to generate a value of type ['a] for a circuit
+  module Provider = struct
+    (** The different ways to generate a value of type ['a] for a circuit
         witness over field ['f].
 
         This is one of:
@@ -56,29 +59,30 @@ module Provider = struct
         * [Both], attempting to dispatch an ['a Request.t], and falling back to
           the computation if the request is unhandled or raises an exception.
     *)
-  type nonrec ('a, 'f) t = (('a Request.t, 'f) t, ('a, 'f) t) Types.Provider.t
-
-  open Types.Provider
-
-  let run t tbl (handler : Request.Handler.t) =
-    match t with
-    | Request rc ->
-        let r = run rc tbl in
-        Request.Handler.run handler r
-    | Compute c ->
-        Some (run c tbl)
-    | Both (rc, c) -> (
-        let r = run rc tbl in
-        match Request.Handler.run handler r with
-        | None | (exception _) ->
-            Some (run c tbl)
-        | x ->
-            x )
-end
-
-module Handle = struct
-  let value (t : ('var, 'value) Handle.t) : ('value, 'field) t =
-   fun _ -> Option.value_exn t.value
+    type nonrec ('a, 'f) t = ('a, 'f) Types.Provider.t
+
+    open Types.Provider
+
+    let run t tbl (handler : Request.Handler.t) =
+      match t with
+      | Request rc ->
+          let r = run rc tbl in
+          Request.Handler.run handler r
+      | Compute c ->
+          Some (run c tbl)
+      | Both (rc, c) -> (
+          let r = run rc tbl in
+          match Request.Handler.run handler r with
+          | None | (exception _) ->
+              Some (run c tbl)
+          | x ->
+              x )
+  end
+
+  module Handle = struct
+    let value (t : ('var, 'value) Handle.t) : ('value, 'field) t =
+     fun _ -> Option.value_exn t.value
+  end
 end
 
 module type Extended = sig

src/base/as_prover_intf.ml

@@ -1,4 +1,6 @@
 module type Basic = sig
+  module Types : Types.Types
+
   type ('a, 'f) t = ('a, 'f) Types.As_prover.t
 
   type field
@@ -12,7 +14,7 @@ module type Basic = sig
 
   val read_var : field Cvar.t -> (field, field) t
 
-  val read : ('var, 'value, field, _) Types.Typ.t -> 'var -> ('value, field) t
+  val read : ('var, 'value, field) Types.Typ.t -> 'var -> ('value, field) t
 
   module Provider : sig
     type ('a, 'f) t

src/base/checked.ml

@@ -5,10 +5,12 @@ module Make (Field : sig
 
   val equal : t -> t -> bool
 end)
-(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
+(Types : Types.Types)
+(Basic : Checked_intf.Basic with type field = Field.t with module Types := Types)
+(As_prover : As_prover_intf.Basic
+               with type field := Basic.field
+               with module Types := Types) :
+  Checked_intf.S with module Types := Types with type field = Field.t = struct
   include Basic
 
   let request_witness (typ : ('var, 'value, field) Types.Typ.t)

src/base/checked_intf.ml

@@ -9,7 +9,7 @@ module type Basic = sig
 
   val add_constraint : (field Cvar.t, field) Constraint.t -> (unit, field) t
 
-  val as_prover : (unit, field) As_prover0.t -> (unit, field) t
+  val as_prover : (unit, field) Types.As_prover.t -> (unit, field) t
 
   val mk_lazy : (unit -> ('a, 'f) t) -> ('a Lazy.t, 'f) t
 
@@ -43,13 +43,13 @@ module type S = sig
 
   include Monad_let.S2 with type ('a, 'f) t := ('a, 'f) t
 
-  val as_prover : (unit, field) As_prover0.t -> (unit, field) t
+  val as_prover : (unit, field) Types.As_prover.t -> (unit, field) t
 
   val mk_lazy : (unit -> ('a, 'f) t) -> ('a Lazy.t, 'f) t
 
   val request_witness :
        ('var, 'value, field) Types.Typ.t
-    -> ('value Request.t, field) As_prover0.t
+    -> ('value Request.t, field) Types.As_prover.t
     -> ('var, field) t
 
   val request :
@@ -59,14 +59,14 @@ module type S = sig
     -> ('var, field) t
 
   val exists_handle :
-       ?request:('value Request.t, field) As_prover0.t
-    -> ?compute:('value, field) As_prover0.t
+       ?request:('value Request.t, field) Types.As_prover.t
+    -> ?compute:('value, field) Types.As_prover.t
     -> ('var, 'value, field) Types.Typ.t
     -> (('var, 'value) Handle.t, field) t
 
   val exists :
-       ?request:('value Request.t, field) As_prover0.t
-    -> ?compute:('value, field) As_prover0.t
+       ?request:('value Request.t, field) Types.As_prover.t
+    -> ?compute:('value, field) Types.As_prover.t
     -> ('var, 'value, field) Types.Typ.t
     -> ('var, field) t
 
@@ -83,7 +83,7 @@ module type S = sig
 
   val handle_as_prover :
        (unit -> ('a, field) t)
-    -> (request -> response, field) As_prover0.t
+    -> (request -> response, field) Types.As_prover.t
     -> ('a, field) t
 
   val next_auxiliary : unit -> (int, field) t
@@ -136,14 +136,16 @@ module type Extended = sig
   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 field = Checked.field = struct
+module Unextend
+    (Types : Types.Types)
+    (Checked : Extended with module Types := Types) :
+  S with module Types := Types with type field = Checked.field = struct
   include (
     Checked :
       S
-        with module Types = Checked.Types
+        with module Types := Types
         with type field := Checked.field
-         and type ('a, 'f) t := ('a, 'f) Checked.Types.Checked.t )
+         and type ('a, 'f) t := ('a, 'f) Types.Checked.t )
 
   type field = Checked.field