Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove polymorphism from As_prover.t, hoist Typ.t #854

Merged
merged 16 commits into from
Dec 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
130 changes: 60 additions & 70 deletions src/base/as_prover0.ml
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -94,6 +86,4 @@ end)
struct
include Env
include As_prover

type nonrec 'a t = ('a, field) t
end
22 changes: 11 additions & 11 deletions src/base/as_prover_intf.ml
Original file line number Diff line number Diff line change
@@ -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
12 changes: 7 additions & 5 deletions src/base/checked.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading
Loading