Merge pull request #854 from o1-labs/feature/lift-typ

Remove polymorphism from `As_prover.t`, hoist `Typ.t`

src/base/as_prover0.ml

@@ -1,90 +1,82 @@
 open Core_kernel
 
-type ('a, 'f) t = ('a, 'f) Types.As_prover.t
+module Make (Backend : sig
+  module Field : sig
+    type t
+  end
+end)
+(Types : Types.Types
+           with type 'a As_prover.t =
+             (Backend.Field.t Cvar.t -> Backend.Field.t) -> 'a) =
+struct
+  type 'a t = 'a 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 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 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.Make (struct
+    type nonrec 'a t = 'a 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
-        witness over field ['f].
-
-        This is one of:
-        * a [Request], dispatching an ['a Request.t];
-        * [Compute], running a computation to generate the value;
-        * [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 Provider = struct
+    include Types.Provider
 
-module Handle = struct
-  let value (t : ('var, 'value) Handle.t) : ('value, 'field) t =
-   fun _ -> Option.value_exn t.value
-end
-
-module type Extended = sig
-  include As_prover_intf.Basic
+    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
 
-  type nonrec 'a t = ('a, field) t
+  module Handle = struct
+    let value (t : ('var, 'value) Handle.t) : 'value t =
+     fun _ -> Option.value_exn t.value
+  end
 end
 
 module Make_extended (Env : sig
@@ -94,6 +86,4 @@ end)
 struct
   include Env
   include As_prover
-
-  type nonrec 'a t = ('a, field) t
 end

src/base/as_prover_intf.ml

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

src/base/checked.ml

@@ -5,14 +5,16 @@ 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)
-      (r : ('value Request.t, field) As_prover.t) =
+      (r : 'value Request.t As_prover.t) =
     let%map h = exists typ (Request r) in
     Handle.var h