Skip to content

Commit

Permalink
refactor binding of bitstrings
Browse files Browse the repository at this point in the history
  • Loading branch information
@strub
strub committed Oct 8, 2024
1 parent 3153548 commit fc489e6
Show file tree
Hide file tree
Showing 12 changed files with 268 additions and 224 deletions.
26 changes: 13 additions & 13 deletions src/ecCommands.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -712,17 +712,17 @@ and process_bdep (scope : EcScope.scope) ((p, f, n, m, vs, pcond) : pgamepath *
assert false
(* EcPhlBDep.bdep_xpath (EcScope.env scope) p f n m vs pcond *)

and process_bind_bitstring (scope : EcScope.scope) (tb: pqsymbol) (fb: pqsymbol) (t: pty) (n: int) =
EcScope.Circ.add_bitstring scope tb fb t n
and process_bind_bitstring (scope : EcScope.scope) (bs : pbind_bitstring) =
EcScope.Circuit.add_bitstring scope bs

and process_bind_bsarray (scope : EcScope.scope) (get: pqsymbol) (set: pqsymbol) (to_list: pqsymbol) (t: pty) (n: int) =
EcScope.Circ.add_bsarray scope get set to_list t n
and process_bind_bsarray (scope : EcScope.scope) (ba : pbind_array) =
EcScope.Circuit.add_bsarray scope ba

and process_bind_circuit (scope : EcScope.scope) (o: pqsymbol) (c: string) =
EcScope.Circ.add_circuit scope o c
and process_bind_circuit (scope : EcScope.scope) ((o, c) : pqsymbol * string) =
EcScope.Circuit.add_circuit scope o c

and process_bind_qfabvop (scope : EcScope.scope) (o: pqsymbol) (c: string) =
EcScope.Circ.add_qfabvop scope o c
and process_bind_qfabvop (scope : EcScope.scope) ((o, c) : pqsymbol * string) =
EcScope.Circuit.add_qfabvop scope o c

and process_test (scope: EcScope.scope) (q: pqsymbol) (q2: pqsymbol) =
let env = EcScope.env scope in
Expand Down Expand Up @@ -772,11 +772,11 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
| Ghint hint -> `Fct (fun scope -> process_hint scope hint)
| GdumpWhy3 file -> `Fct (fun scope -> process_dump_why3 scope file)
| Gbdep (proc, f, n, m, vs, b) -> `State (fun scope -> process_bdep scope (proc, f, n, m, vs, b))
| Gbbitstring (tb, fb, t, n) -> `Fct (fun scope -> process_bind_bitstring scope tb fb t n )
| Gbbsarray (get, set, to_list, t, n) -> `Fct (fun scope -> process_bind_bsarray scope get set to_list t n )
| Gbcircuit (o, c) -> `Fct (fun scope -> process_bind_circuit scope o c)
| Gbqfabvop (o, c) -> `Fct (fun scope -> process_bind_qfabvop scope o c)
| Gtest (p1, p2) -> `State (fun scope -> process_test scope p1 p2)
| Gbbitstring bs -> `Fct (fun scope -> process_bind_bitstring scope bs)
| Gbbsarray ba -> `Fct (fun scope -> process_bind_bsarray scope ba)
| Gbcircuit oc -> `Fct (fun scope -> process_bind_circuit scope oc)
| Gbqfabvop oc -> `Fct (fun scope -> process_bind_qfabvop scope oc)
| Gtest (p1, p2) -> `State (fun scope -> process_test scope p1 p2)
with
| `Fct f -> Some (f scope)
| `State f -> f scope; None
Expand Down
17 changes: 4 additions & 13 deletions src/ecEnv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,12 +168,6 @@ end = struct
end

(* -------------------------------------------------------------------- *)
type bitstring = {
to_bits: path;
from_bits: path;
size: int;
}

type bsarray = {
get : path;
set : path;
Expand Down Expand Up @@ -3581,7 +3575,7 @@ let pp_debug_form = ref (fun _env _fmt _f -> assert false)
module Circ : sig
val bind_bitstring : env -> path -> path -> path -> int -> env
val bind_bitstring : env -> bitstring -> env
val bind_bsarray : env -> path -> path -> path -> path -> int -> env
val bind_circuit : env -> path -> string -> env
val bind_qfabvop : env -> path -> string -> env
Expand All @@ -3597,13 +3591,10 @@ module Circ : sig
val lookup_qfabvop_path : env -> path -> qfabvop option
val lookup_qfabvop : env -> qsymbol -> qfabvop option
val lookup_bsarrayop : env -> path -> bsarrayop option
end = struct
let bind_bitstring (env: env) (to_bits: path) (from_bits:path) (ty: path) (size: int) : env =
Format.eprintf "Binding bitstring for type %s@." (EcPath.tostring ty);
{env with env_circ =
{env.env_circ with bitstrings = Mp.add ty {to_bits;from_bits;size} env.env_circ.bitstrings}}
let bind_bitstring (env : env) (bs : bitstring) : env =
{ env with env_circ =
{ env.env_circ with bitstrings = Mp.add bs.type_ bs env.env_circ.bitstrings } }
let bind_bsarray (env: env) (get: path) (set: path) (to_list: path) (ty: path) (size: int) : env =
Format.eprintf "Binding bsarray for type %s@." (EcPath.tostring ty);
Expand Down
12 changes: 3 additions & 9 deletions src/ecEnv.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,6 @@ type 'a suspension = {
}

(* -------------------------------------------------------------------- *)
type bitstring = { (* FIXME: maybe move this later? *)
to_bits : path;
from_bits : path;
size : int;
}

type bsarray = {
get : path;
set : path;
Expand Down Expand Up @@ -528,9 +522,9 @@ val pp_debug_form : (env -> Format.formatter -> form -> unit) ref

module Circ : sig

val bind_bitstring : env -> path -> path -> path -> int -> env
val bind_circuit : env -> path -> string -> env
val bind_qfabvop : env -> path -> string -> env
val bind_bitstring : env -> bitstring -> env
val bind_circuit : env -> path -> string -> env
val bind_qfabvop : env -> path -> string -> env

val lookup_bitstring : env -> ty -> bitstring option
val lookup_bitstring_path : env -> path -> bitstring option
Expand Down
8 changes: 4 additions & 4 deletions src/ecParser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3930,11 +3930,11 @@ global_action:
| BDEP p=loc(fident) f=oident n=uint m=uint LBRACKET vl=plist0(STRING, SEMICOLON) RBRACKET pc=oident
{ Gbdep (p, f, (BI.to_int n), (BI.to_int m), vl, pc) }

| BIND BITSTRING tb=qoident fb=qoident t=loc(simpl_type_exp) n=uint
{ Gbbitstring (tb, fb, t, (BI.to_int n)) }
| BIND BITSTRING from_=qoident to_=qoident type_=loc(simpl_type_exp) size=uint
{ Gbbitstring { from_; to_; type_; size; } }

| BIND BITSTRING CIRCUIT get=qoident set=qoident tl=qoident t=loc(simpl_type_exp) n=uint
{ Gbbsarray (get, set, tl, t, (BI.to_int n)) }
| BIND BITSTRING CIRCUIT get=qoident set=qoident tolist=qoident type_=loc(simpl_type_exp) size=uint
{ Gbbsarray { get; set; tolist; type_; size; } }

| BIND CIRCUIT o=qoident c=STRING
{ Gbcircuit (o, c) }
Expand Down
31 changes: 27 additions & 4 deletions src/ecParsetree.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1268,6 +1268,29 @@ type puserred =
type threquire =
psymbol option * (psymbol * psymbol option) list * [`Import|`Export] option

(* -------------------------------------------------------------------- *)
type pbind_bitstring =
{ from_ : pqsymbol
; to_ : pqsymbol
; type_ : pty
; size : EcBigInt.zint }

(* -------------------------------------------------------------------- *)
type pbind_array =
{ get : pqsymbol
; set : pqsymbol
; tolist : pqsymbol
; type_ : pty
; size : EcBigInt.zint }

(* -------------------------------------------------------------------- *)
type pbind_circuit =
pqsymbol * string

(* -------------------------------------------------------------------- *)
type pbind_qfabvop =
pqsymbol * string

(* -------------------------------------------------------------------- *)
type global_action =
| Gmodule of pmodule_def_or_decl
Expand Down Expand Up @@ -1307,10 +1330,10 @@ type global_action =
| Goption of (psymbol * [`Bool of bool | `Int of int])
| GdumpWhy3 of string
| Gbdep of pgamepath * psymbol * int * int * (string list) * psymbol
| Gbbitstring of pqsymbol * pqsymbol * pty * int
| Gbbsarray of pqsymbol * pqsymbol * pqsymbol * pty * int
| Gbcircuit of pqsymbol * string
| Gbqfabvop of pqsymbol * string
| Gbbitstring of pbind_bitstring
| Gbbsarray of pbind_array
| Gbcircuit of pbind_circuit
| Gbqfabvop of pbind_qfabvop
| Gtest of pqsymbol * pqsymbol

type global = {
Expand Down
Loading

0 comments on commit fc489e6

Please sign in to comment.