From fc489e6e45ba25b75a464e41602e185676cf80c2 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 8 Oct 2024 12:05:11 +0200 Subject: [PATCH] refactor binding of bitstrings --- src/ecCommands.ml | 26 +-- src/ecEnv.ml | 17 +- src/ecEnv.mli | 12 +- src/ecParser.mly | 8 +- src/ecParsetree.ml | 31 +++- src/ecScope.ml | 362 +++++++++++++++++++++++------------------- src/ecScope.mli | 16 +- src/ecSection.ml | 2 +- src/ecTheory.ml | 5 +- src/ecTheory.mli | 7 +- src/phl/ecPhlBDep.ml | 4 +- src/phl/ecPhlBDep.mli | 2 - 12 files changed, 268 insertions(+), 224 deletions(-) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 88af5e69a9..c8ceed0b74 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -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 @@ -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 diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 3813541845..ead16848d4 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -168,12 +168,6 @@ end = struct end (* -------------------------------------------------------------------- *) -type bitstring = { - to_bits: path; - from_bits: path; - size: int; -} - type bsarray = { get : path; set : path; @@ -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 @@ -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); diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 93a05c4457..87b8194a5d 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -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; @@ -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 diff --git a/src/ecParser.mly b/src/ecParser.mly index eb39847c45..ef5a5631cb 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -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) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 19924b26eb..f84c4459ee 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -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 @@ -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 = { diff --git a/src/ecScope.ml b/src/ecScope.ml index b8967d1cbc..1759d48ba0 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2233,7 +2233,31 @@ module Cloning = struct end (* ------------------------------------------------------------------ *) - let clone (scope : scope) mode (thcl : theory_cloning) = + let replay_proofs (scope : scope) (mode : Tactics.proofmode) (proofs : _) = + proofs |> List.pmap (fun axc -> + match axc.C.axc_tac with + | None -> + Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env) + + | Some pt -> + let t = { pt_core = pt; pt_intros = []; } in + let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in + let t = { pt_core = t; pt_intros = []; } in + let (x, ax) = axc.C.axc_axiom in + + let pucflags = { puc_visibility = `Visible; puc_local = false; } in + let pucflags = (([], None), pucflags) in + let check = Check_mode.check scope.sc_options in + + let escope = { scope with sc_env = axc.C.axc_env; } in + let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in + let escope = Tactics.proof escope in + let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in + ignore (Ax.save_r escope); None + ) + + (* ------------------------------------------------------------------ *) + let clone (scope : scope) (mode : Tactics.proofmode) (thcl : theory_cloning) = assert (scope.sc_pr_uc = None); let { cl_name = name; @@ -2262,28 +2286,7 @@ module Cloning = struct scope (name, oth.cth_items) in - let proofs = List.pmap (fun axc -> - match axc.C.axc_tac with - | None -> - Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env) - - | Some pt -> - let t = { pt_core = pt; pt_intros = []; } in - let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in - let t = { pt_core = t; pt_intros = []; } in - let (x, ax) = axc.C.axc_axiom in - - let pucflags = { puc_visibility = `Visible; puc_local = false; } in - let pucflags = (([], None), pucflags) in - let check = Check_mode.check scope.sc_options in - - let escope = { scope with sc_env = axc.C.axc_env; } in - let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in - let escope = Tactics.proof escope in - let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in - ignore (Ax.save_r escope); None) - proofs - in + let proofs = replay_proofs scope mode proofs in let scope = thcl.pthc_import |> ofold (fun flag scope -> @@ -2294,12 +2297,180 @@ module Cloning = struct let item = EcTheory.mkitem EcTheory.import0 (Th_export (npath, `Global)) in { scope with sc_env = EcSection.add_item item scope.sc_env; } | `Include -> scope) - scope - - in Ax.add_defer scope proofs + scope in + Ax.add_defer scope proofs end +(* -------------------------------------------------------------------- *) +module Circuit : sig + val add_bitstring : scope -> pbind_bitstring -> scope + val add_bsarray : scope -> pbind_array -> scope + val add_circuit : scope -> pqsymbol -> string -> scope + val add_qfabvop : scope -> pqsymbol -> string -> scope +end = struct + type preoperator = [`Path of path | `Int of BI.zint] + + type clone = { + path : EcPath.path; + name : symbol; + types_ : (symbol * path) list; + operators : (symbol * preoperator) list; + } + + let doclone (scope : scope) (clone : clone) = + let loced x = mk_loc _dummy x in + let env = env scope in + + let evclone = + let do_type ((x, type_) : symbol * path) : symbol * ty_override located = + (x, loced (`ByPath type_, `Inline `Keep)) in + + let do_operator ((x, operator) : symbol * preoperator) : symbol * op_override located = + let operator = + match operator with + | `Path name -> `ByPath name + | `Int i -> + `BySyntax + { opov_tyvars = None + ; opov_args = [] + ; opov_retty = loced PTunivar + ; opov_body = loced (PFint i) } + in (x, loced (operator, `Inline `Keep)) + in + + { EcThCloning.evc_empty with + evc_types = Msym.of_list (List.map do_type clone.types_); + evc_ops = Msym.of_list (List.map do_operator clone.operators); + evc_lemmas = { + ev_bynames = Msym.of_list [ + "ge0_size", (Some (loced (Pby None)), `Alias, false) + ]; + ev_global = [None, None]; } } in + + let npath = EcPath.pqname (EcEnv.root env) clone.name in + let theory = EcEnv.Theory.by_path clone.path env in + + let (proofs, scope) = + EcTheoryReplay.replay Cloning.hooks + ~abstract:false ~local:`Global ~incl:false + ~clears:Sp.empty ~renames:[] ~opath:clone.path ~npath + evclone scope (EcPath.basename clone.path, theory.cth_items) + in + + let proofs = Cloning.replay_proofs scope `Check proofs in + + (proofs, scope) + + let add_bitstring (scope : scope) (bs : pbind_bitstring) : scope = + let env = env scope in + + let type_ = + let ue = EcUnify.UniEnv.create None in + let ty = EcTyping.transty tp_tydecl env ue bs.type_ in + assert (EcUnify.UniEnv.closed ue); + ty_subst (Tuni.subst (EcUnify.UniEnv.close ue)) ty in + + let bspath = + match (EcEnv.ty_hnorm type_ env).ty_node with + | Tconstr (p, []) -> p + | _ -> + hierror ~loc:(bs.type_.pl_loc) + "bit-string type must be a monomorphic named type" in + + let from_, _ = EcEnv.Op.lookup bs.to_.pl_desc env in + let to_ , _ = EcEnv.Op.lookup bs.from_.pl_desc env in + + let preclone = + { path = EcPath.fromqsymbol (["Top"; "QFABV"], "BV") + ; name = "BVA" + ; types_ = ["bv", bspath] + ; operators = + [ ("size" , `Int bs.size) + ; ("tolist", `Path to_) + ; ("oflist", `Path from_) ] } in + + let proofs, scope = doclone scope preclone in + + let item = + EcTheory.mkitem EcTheory.import0 + (EcTheory.Th_bitstring + { from_; to_; type_ = bspath; size = BI.to_int bs.size }) in + + let scope = { scope with sc_env = EcSection.add_item item scope.sc_env } in + + Ax.add_defer scope proofs + + let add_bsarray (scope : scope) (ba : pbind_array) : scope = + let env = env scope in + + let getp, _geto = EcEnv.Op.lookup ba.get.pl_desc env in + let setp, _seto = EcEnv.Op.lookup ba.set.pl_desc env in + let to_listp, _to_listo = EcEnv.Op.lookup ba.tolist.pl_desc env in + + let ue = EcUnify.UniEnv.create None in + let t = EcTyping.transty tp_tydecl env ue ba.type_ in + match t.ty_node with + | Tconstr (p, [t]) -> + Format.eprintf "Registering array type %s over type %a@." + (EcPath.tostring p) (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) t; + let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_bsarray (getp, setp, to_listp, p, BI.to_int ba.size)) in + { scope with sc_env = EcSection.add_item item scope.sc_env } + | _ -> assert false + + + let add_circuit (scope : scope) (o : pqsymbol) (c : string) : scope = + let p, _o = EcEnv.Op.lookup o.pl_desc (env scope) in + let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_circuit (p, c)) in + { scope with sc_env = EcSection.add_item item scope.sc_env } + + let add_qfabvop (scope : scope) (o : pqsymbol) (c : string) : scope = + (* FIXME: rewrite this, this is horrible *) + let loced a = mk_loc o.pl_loc a in + let env = env scope in + let opth, oop = EcEnv.Op.lookup o.pl_desc env in + let t = match oop.op_ty.ty_node with + | Tfun (t, _) -> t + | _ -> assert false + in + let thry = match c with + | "bvadd" -> "BVAdd" + | "bvsub" -> "BVSub" + | _ -> assert false + in + let o_ovrd = { + opov_tyvars = None; + opov_args = []; + opov_retty = loced PTunivar; + opov_body = loced @@ PFident ((loced @@ EcPath.toqsymbol @@ opth), None) + } + in + let th_name = + (Format.asprintf "BV_%a" (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) t) + |> String.map (fun c -> if c = '.' then '_' else c) + in + let (tc: EcParsetree.theory_cloning) = { + pthc_base = loced ([th_name], thry); + pthc_name = Some (loced + (Format.asprintf "%s_%s" th_name thry)); + pthc_ext = [ + ((loced ([], c), PTHO_Op (`BySyntax o_ovrd, `Inline `Keep))) + ]; (* FIXME: add override for theory *) + pthc_prf = [{pthp_mode = `All (None, []); pthp_tactic = None}]; + pthc_rnm = []; + pthc_opts = []; + pthc_clears = []; + pthc_local = `Global; + pthc_import = None; + } + in + (* let sc = Cloning.clone sc `Check tc in *) + + let p, _o = EcEnv.Op.lookup o.pl_desc env in + let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_qfabvop (p, c)) in + Cloning.clone { scope with sc_env = EcSection.add_item item scope.sc_env } `Check tc + end + (* -------------------------------------------------------------------- *) module Search = struct let search (scope : scope) qs = @@ -2424,142 +2595,3 @@ module Search = struct notify scope `Info "%s" (Buffer.contents buffer) end - -module Circ : sig - val add_bitstring : scope -> pqsymbol -> pqsymbol -> pty -> int -> scope - val add_bsarray : scope -> pqsymbol -> pqsymbol -> pqsymbol -> pty -> int -> scope - val add_circuit : scope -> pqsymbol -> string -> scope - val add_qfabvop : scope -> pqsymbol -> string -> scope - -end = struct - let add_bitstring (sc: scope) (tb: pqsymbol) (fb: pqsymbol) (pt: pty) (n: int) : scope = - let env = (env sc) in - let loced a = mk_loc (tb.pl_loc) a in - - let tbp, _tbo = EcEnv.Op.lookup tb.pl_desc env in - let fbp, _fbo = EcEnv.Op.lookup fb.pl_desc env in - - let ue = EcTyping.transtyvars env (pt.pl_loc, None) in - let t = EcTyping.transty tp_tydecl env ue pt in - - let ov = { - opov_tyvars = None; - opov_args = []; - opov_retty = loced PTunivar; - opov_body = loced (PFint (BI.of_int n)); - } in - - let otb = { - opov_tyvars = None; - opov_args = []; - opov_retty = loced PTunivar; - opov_body = loced @@ PFident ((loced @@ EcPath.toqsymbol @@ tbp), None) - } in - - let ofb = { - opov_tyvars = None; - opov_args = []; - opov_retty = loced PTunivar; - opov_body = loced @@ PFident ((loced @@ EcPath.toqsymbol @@ fbp), None) - } in - - let (tc: EcParsetree.theory_cloning) = { - pthc_base = loced (["Top"; "QFABV"], "BV"); - pthc_name = Some (loced @@ (Format.asprintf "BV_%a" - (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) t - |> String.map (fun c -> if c = '.' then '_' else c))); - pthc_ext = [ - (loced ([], "bv"), PTHO_Type (`BySyntax ([], pt), `Inline `Clear)); - (loced ([], "size"), PTHO_Op (`BySyntax ov, `Inline `Keep)); - (loced ([], "tolist"), PTHO_Op (`BySyntax otb, `Inline `Keep)); - (loced ([], "oflist"), PTHO_Op (`BySyntax ofb, `Inline `Keep)); - ]; (* FIXME: add override for theory *) - pthc_prf = [{pthp_mode = `All (None, []); pthp_tactic = None}]; - pthc_rnm = []; - pthc_opts = []; - pthc_clears = []; - pthc_local = `Global; - pthc_import = None; - } - in - let () = Format.eprintf "Registering theory %s@." (tc.pthc_name |> Option.get).pl_desc in - (* let sc = Cloning.clone sc `Check tc in *) - match t.ty_node with - | Tconstr (p, []) -> - let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_bitstring (tbp, fbp, p, n)) in - Cloning.clone {sc with sc_env = EcSection.add_item item sc.sc_env } `Check tc - | _ -> assert false - - - let add_bsarray (sc: scope) (get: pqsymbol) (set: pqsymbol) (to_list: pqsymbol) (pt: pty) (n: int) : scope = - let env = (env sc) in - (* let loced a = mk_loc (get.pl_loc) a in *) - - let getp, _geto = EcEnv.Op.lookup get.pl_desc env in - let setp, _seto = EcEnv.Op.lookup set.pl_desc env in - let to_listp, _to_listo = EcEnv.Op.lookup to_list.pl_desc env in - - let ue = EcTyping.transtyvars env (pt.pl_loc, None) in - let t = EcTyping.transty tp_tydecl env ue pt in - match t.ty_node with - | Tconstr (p, [t]) -> - Format.eprintf "Registering array type %s over type %a@." - (EcPath.tostring p) (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) t; - let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_bsarray (getp, setp, to_listp, p, n)) in - {sc with sc_env = EcSection.add_item item sc.sc_env} - | _ -> assert false - - - let add_circuit (sc: scope) (o: pqsymbol) (c: string) : scope = - let p, _o = EcEnv.Op.lookup o.pl_desc (env sc) in - let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_circuit (p, c)) in - {sc with sc_env = EcSection.add_item item sc.sc_env } - - let add_qfabvop (sc: scope) (o: pqsymbol) (c: string) : scope = - (* FIXME: rewrite this, this is horrible *) - let loced a = mk_loc o.pl_loc a in - let env = env sc in - let opth, oop = EcEnv.Op.lookup o.pl_desc env in - let t = match oop.op_ty.ty_node with - | Tfun (t, _) -> t - | _ -> assert false - in - let thry = match c with - | "bvadd" -> "BVAdd" - | "bvsub" -> "BVSub" - | _ -> assert false - in - let o_ovrd = { - opov_tyvars = None; - opov_args = []; - opov_retty = loced PTunivar; - opov_body = loced @@ PFident ((loced @@ EcPath.toqsymbol @@ opth), None) - } - in - let th_name = - (Format.asprintf "BV_%a" (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) t) - |> String.map (fun c -> if c = '.' then '_' else c) - in - let (tc: EcParsetree.theory_cloning) = { - pthc_base = loced ([th_name], thry); - pthc_name = Some (loced - (Format.asprintf "%s_%s" th_name thry)); - pthc_ext = [ - ((loced ([], c), PTHO_Op (`BySyntax o_ovrd, `Inline `Keep))) - ]; (* FIXME: add override for theory *) - pthc_prf = [{pthp_mode = `All (None, []); pthp_tactic = None}]; - pthc_rnm = []; - pthc_opts = []; - pthc_clears = []; - pthc_local = `Global; - pthc_import = None; - } - in - (* let sc = Cloning.clone sc `Check tc in *) - - let p, _o = EcEnv.Op.lookup o.pl_desc env in - let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_qfabvop (p, c)) in - Cloning.clone {sc with sc_env = EcSection.add_item item sc.sc_env } `Check tc - - -end diff --git a/src/ecScope.mli b/src/ecScope.mli index b200cbf57a..6d3ef91e49 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -244,6 +244,14 @@ module Reduction : sig val add_reduction : scope -> puserred -> scope end +(* -------------------------------------------------------------------- *) +module Circuit : sig + val add_bitstring : scope -> pbind_bitstring -> scope + val add_bsarray : scope -> pbind_array -> scope + val add_circuit : scope -> pqsymbol -> string -> scope + val add_qfabvop : scope -> pqsymbol -> string -> scope +end + (* -------------------------------------------------------------------- *) module Cloning : sig val clone : scope -> Ax.proofmode -> theory_cloning -> scope @@ -254,11 +262,3 @@ module Search : sig val search : scope -> pformula list -> unit val locate : scope -> pqsymbol -> unit end - -module Circ : sig - val add_bitstring : scope -> pqsymbol -> pqsymbol -> pty -> int -> scope - val add_bsarray : scope -> pqsymbol -> pqsymbol -> pqsymbol -> pty -> int -> scope - val add_circuit : scope -> pqsymbol -> string -> scope - val add_qfabvop : scope -> pqsymbol -> string -> scope - -end diff --git a/src/ecSection.ml b/src/ecSection.ml index 043a5c9ac2..e3b2e5b0a8 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1351,7 +1351,7 @@ let add_item_ (item : theory_item) (scenv:scenv) = | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env | Th_auto (level, base, ps, lc) -> EcEnv.Auto.add ~level ?base ps lc env | Th_reduction r -> EcEnv.Reduction.add r env - | Th_bitstring (tb, fb, t, n) -> EcEnv.Circ.bind_bitstring env tb fb t n + | Th_bitstring bs -> EcEnv.Circ.bind_bitstring env bs | Th_bsarray (get, set, to_list, t, n) -> EcEnv.Circ.bind_bsarray env get set to_list t n | Th_circuit (o, c) -> EcEnv.Circ.bind_circuit env o c | Th_qfabvop (o, c) -> EcEnv.Circ.bind_qfabvop env o c diff --git a/src/ecTheory.ml b/src/ecTheory.ml index 8eede94816..f012dc0fcc 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -38,11 +38,14 @@ and theory_item_r = | Th_addrw of EcPath.path * EcPath.path list * is_local | Th_reduction of (EcPath.path * rule_option * rule option) list | Th_auto of (int * symbol option * path list * is_local) - | Th_bitstring of (path * path * path * int) + | Th_bitstring of bitstring | Th_bsarray of (path * path * path * path * int) | Th_circuit of (path * string) | Th_qfabvop of (path * string) +and bitstring = + { type_: path; from_: path; to_: path; size: int; } + and thsource = { ths_base : EcPath.path; } diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 583f8ea74a..b068aabd8d 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -36,11 +36,14 @@ and theory_item_r = | Th_reduction of (EcPath.path * rule_option * rule option) list | Th_auto of (int * symbol option * path list * is_local) (* check this V *) - | Th_bitstring of (path * path * path * int) - | Th_bsarray of (path * path * path * path * int) + | Th_bitstring of bitstring + | Th_bsarray of (path * path * path * path * int) | Th_circuit of (path * string) | Th_qfabvop of (path * string) +and bitstring = + { type_: path; from_: path; to_: path; size: int; } + and thsource = { ths_base : EcPath.path; } diff --git a/src/phl/ecPhlBDep.ml b/src/phl/ecPhlBDep.ml index de1660818c..e8f25341d1 100644 --- a/src/phl/ecPhlBDep.ml +++ b/src/phl/ecPhlBDep.ml @@ -241,7 +241,7 @@ let t_circ (tc: tcenv1) : tcenv = | _ -> failwith "Wrong type structure for array" in let ptb, otb = match EcEnv.Circ.lookup_bitstring env bty with - | Some {to_bits=tb; _} -> tb, EcEnv.Op.by_path tb env + | Some {to_=tb; _} -> tb, EcEnv.Op.by_path tb env | _ -> Format.eprintf "No w2bits for type %a@." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty; assert false in EcCoreLib.CI_List.p_flatten @@! [ EcCoreLib.CI_List.p_map @@! [f_op ptb [] otb.op_ty; @@ -249,7 +249,7 @@ let t_circ (tc: tcenv1) : tcenv = ] | None -> begin match EcEnv.Circ.lookup_bitstring env ty with - | Some {to_bits=tb; _} -> tb @@! [arg] + | Some {to_=tb; _} -> tb @@! [arg] | _ -> Format.eprintf "No w2bits for type %a@." (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty; assert false end diff --git a/src/phl/ecPhlBDep.mli b/src/phl/ecPhlBDep.mli index a07b68c839..a99cb0ebf9 100644 --- a/src/phl/ecPhlBDep.mli +++ b/src/phl/ecPhlBDep.mli @@ -1,8 +1,6 @@ (* -------------------------------------------------------------------- *) open EcParsetree -open EcEnv open EcCoreGoal -open EcPath open EcAst (* -------------------------------------------------------------------- *)