diff --git a/src/base/as_prover0.ml b/src/base/as_prover0.ml index 2c22b8334..033176d7d 100644 --- a/src/base/as_prover0.ml +++ b/src/base/as_prover0.ml @@ -82,9 +82,7 @@ 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 @@ -92,7 +90,7 @@ 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 diff --git a/src/base/as_prover_intf.ml b/src/base/as_prover_intf.ml index 2d56f7bae..6c6dc27e6 100644 --- a/src/base/as_prover_intf.ml +++ b/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 diff --git a/src/base/checked.ml b/src/base/checked.ml index 0e2fefdb1..ae8d7859e 100644 --- a/src/base/checked.ml +++ b/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 diff --git a/src/base/checked_intf.ml b/src/base/checked_intf.ml index 52a0a32a6..b430989d2 100644 --- a/src/base/checked_intf.ml +++ b/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 diff --git a/src/base/checked_runner.ml b/src/base/checked_runner.ml index 5906303ab..ba2c8d22a 100644 --- a/src/base/checked_runner.ml +++ b/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 diff --git a/src/base/snark0.ml b/src/base/snark0.ml index e14eb8085..6f46a25e2 100644 --- a/src/base/snark0.ml +++ b/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 diff --git a/src/base/typ.ml b/src/base/typ.ml index 90da372dc..e5140be12 100644 --- a/src/base/typ.ml +++ b/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