From 34cff983df41e75b542bb0b975e8753a487d8faa Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 10 Oct 2024 10:53:06 +0200 Subject: [PATCH] refactoring --- src/ecCircuits.ml | 7 +- src/ecCircuits.mli | 2 +- src/ecCommands.ml | 22 ++---- src/ecDecl.ml | 45 +++++++++++ src/ecDecl.mli | 45 +++++++++++ src/ecEnv.ml | 169 ++++++++++++++++++++++-------------------- src/ecEnv.mli | 27 +++---- src/ecParser.mly | 32 +++++--- src/ecParsetree.ml | 29 ++++---- src/ecPrinting.ml | 13 ++-- src/ecScope.ml | 39 +++++----- src/ecScope.mli | 8 +- src/ecSection.ml | 107 ++++++++++++-------------- src/ecSubst.ml | 86 ++++++++++----------- src/ecThCloning.ml | 5 +- src/ecTheory.ml | 37 +-------- src/ecTheory.mli | 38 +--------- src/ecTheoryReplay.ml | 52 +++++++------ 18 files changed, 395 insertions(+), 368 deletions(-) diff --git a/src/ecCircuits.ml b/src/ecCircuits.ml index 993b4c59ba..81c804f4cd 100644 --- a/src/ecCircuits.ml +++ b/src/ecCircuits.ml @@ -33,6 +33,7 @@ let rec blocks (xs: 'a list) (w: int) : 'a list list = | _ -> let h, t = List.takedrop w xs in h::(blocks t w) + (* -------------------------------------------------------------------- *) type width = int type deps = ((int * int) * int C.VarRange.t) list @@ -637,7 +638,7 @@ module BaseOps = struct | _, "zeroextu64" -> true - | _ -> begin match EcEnv.Circuit.lookup_qfabvop_path env p with + | _ -> begin match EcEnv.Circuit.lookup_bvoperator_path env p with | Some _ -> Format.eprintf "Found qfabv binding for %s@." (EcPath.tostring p); true | None -> Format.eprintf "Did not find qfabv binding for %s@." (EcPath.tostring p); false end @@ -820,7 +821,7 @@ module BaseOps = struct (* let dc = C.or_ dp_modqt dm_modqt in *) {circ = BWCirc([dc]); inps = [BWInput(id1, 16); BWInput(id2, 16)]} - | _ -> begin match EcEnv.Circuit.lookup_qfabvop_path env p with + | _ -> begin match EcEnv.Circuit.lookup_bvoperator_path env p with | Some { kind = `Add size } -> let id1 = EcIdent.create (temp_symbol) in let id2 = EcIdent.create (temp_symbol) in @@ -901,7 +902,7 @@ module ArrayOps = struct | None -> false - let destr_getset_opt (env: env) (pth: path) : bsarrayop option = + let destr_getset_opt (env: env) (pth: path) : crb_array_op option = match EcEnv.Circuit.lookup_bsarrayop env pth with | Some (GET _) as g -> g | Some (SET _) as g -> g diff --git a/src/ecCircuits.mli b/src/ecCircuits.mli index bb943f8079..3208908ac1 100644 --- a/src/ecCircuits.mli +++ b/src/ecCircuits.mli @@ -6,7 +6,7 @@ open EcEnv (* -------------------------------------------------------------------- *) module Map = Batteries.Map - + (* -------------------------------------------------------------------- *) val blocks : 'a list -> int -> 'a list list diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 6e655ce934..7ad8548ca1 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -706,17 +706,12 @@ and process_dump scope (source, tc) = scope (* -------------------------------------------------------------------- *) -and process_bind_bitstring (scope : EcScope.scope) (bs : pbind_bitstring) = - EcScope.Circuit.add_bitstring scope bs - -and process_bind_bsarray (scope : EcScope.scope) (ba : pbind_array) = - EcScope.Circuit.add_bsarray scope ba - -and process_bind_qfabvop (scope : EcScope.scope) (bop : pbind_qfabvop) = - EcScope.Circuit.add_qfabvop scope bop - -and process_bind_circuit (scope : EcScope.scope) (pc : pbind_circuit) = - EcScope.Circuit.add_circuit scope pc +and process_crbind (scope : EcScope.scope) (binding : pcrbinding) = + match binding.binding with + | CRB_Bitstring bs -> EcScope.Circuit.add_bitstring scope binding.locality bs + | CRB_Array ba -> EcScope.Circuit.add_bsarray scope binding.locality ba + | CRB_BvOperator op -> EcScope.Circuit.add_qfabvop scope binding.locality op + | CRB_Circuit cr -> EcScope.Circuit.add_circuit scope binding.locality cr (* -------------------------------------------------------------------- *) and process (ld : Loader.loader) (scope : EcScope.scope) g = @@ -761,10 +756,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g = | Greduction red -> `Fct (fun scope -> process_reduction scope red) | Ghint hint -> `Fct (fun scope -> process_hint scope hint) | GdumpWhy3 file -> `Fct (fun scope -> process_dump_why3 scope file) - | 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) + | Gcrbinding bind -> `Fct (fun scope -> process_crbind scope bind) with | `Fct f -> Some (f scope) | `State f -> f scope; None diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 5806407fa3..2166b321ff 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -344,3 +344,48 @@ let field_equal f1 f2 = ring_equal f1.f_ring f2.f_ring && EcPath.p_equal f1.f_inv f2.f_inv && EcUtils.oall2 EcPath.p_equal f1.f_div f2.f_div + +(* -------------------------------------------------------------------- *) +type crb_bitstring = + { type_ : EcPath.path + ; from_ : EcPath.path + ; to_ : EcPath.path + ; size : int + ; theory : EcPath.path } + +type crb_array = + { type_ : EcPath.path + ; get : EcPath.path + ; set : EcPath.path + ; tolist : EcPath.path + ; size : int } + +type bv_opkind = [ + | `Add of int + | `Sub of int + | `Mul of int + | `UDiv of int + | `URem of int + | `Shl of int + | `Shr of int + | `And of int + | `Or of int + | `Not of int +] + +type crb_bvoperator = + { kind : bv_opkind + ; type_ : EcPath.path + ; operator : EcPath.path + ; theory : EcPath.path } + +type crb_circuit = +{ name : string +; circuit : Lospecs.Ast.adef +; operator : EcPath.path } + +type crbinding = +| CRB_Bitstring of crb_bitstring +| CRB_Array of crb_array +| CRB_BvOperator of crb_bvoperator +| CRB_Circuit of crb_circuit diff --git a/src/ecDecl.mli b/src/ecDecl.mli index 65e2dea27c..1b7cfb835e 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -194,3 +194,48 @@ type field = { f_div : EcPath.path option; } val field_equal : field -> field -> bool + +(* -------------------------------------------------------------------- *) +type crb_bitstring = + { type_ : EcPath.path + ; from_ : EcPath.path + ; to_ : EcPath.path + ; size : int + ; theory : EcPath.path } + +type crb_array = + { type_ : EcPath.path + ; get : EcPath.path + ; set : EcPath.path + ; tolist : EcPath.path + ; size : int } + +type bv_opkind = [ + | `Add of int + | `Sub of int + | `Mul of int + | `UDiv of int + | `URem of int + | `Shl of int + | `Shr of int + | `And of int + | `Or of int + | `Not of int +] + +type crb_bvoperator = + { kind : bv_opkind + ; type_ : EcPath.path + ; operator : EcPath.path + ; theory : EcPath.path } + +type crb_circuit = +{ name : string +; circuit : Lospecs.Ast.adef +; operator : EcPath.path } + +type crbinding = +| CRB_Bitstring of crb_bitstring +| CRB_Array of crb_array +| CRB_BvOperator of crb_bvoperator +| CRB_Circuit of crb_circuit diff --git a/src/ecEnv.ml b/src/ecEnv.ml index fb5963d7f9..5cccfe4439 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -167,16 +167,16 @@ end = struct end (* -------------------------------------------------------------------- *) -type bsarrayop = +type crb_array_op = | GET of int | SET of int -type circuits = { - bitstrings : bitstring Mp.t; - circuits : circuit Mp.t; - qfabvops : qfabvop Mp.t; - bsarrays : bsarray Mp.t; - bsarrayops : bsarrayop Mp.t; +type crbindings = { + bitstrings : crb_bitstring Mp.t; + arrays : crb_array Mp.t; + bvoperators : crb_bvoperator Mp.t; + circuits : crb_circuit Mp.t; + arrayops : crb_array_op Mp.t; } (* -------------------------------------------------------------------- *) @@ -199,7 +199,7 @@ type preenv = { env_modlcs : Sid.t; (* declared modules *) env_item : theory_item list; (* in reverse order *) env_norm : env_norm ref; - env_circ : circuits; + env_crbds : crbindings; (* Map theory paths to their env before just before theory was closed. *) (* The environment should be incuded for all theories, including *) (* abstract ones. The purpose of this map is to simplify the code *) @@ -306,6 +306,13 @@ let empty gstate = let icomps = MMsym.add name (IPPath path) MMsym.empty in { (empty_mc None) with mc_components = icomps } in + let empty_crbindings : crbindings = + { bitstrings = Mp.empty + ; arrays = Mp.empty + ; bvoperators = Mp.empty + ; arrayops = Mp.empty + ; circuits = Mp.empty } in + { env_top = None; env_gstate = gstate; env_scope = { ec_path = path; ec_scope = `Theory; }; @@ -324,9 +331,7 @@ let empty gstate = env_modlcs = Sid.empty; env_item = []; env_norm = ref empty_norm_cache; - env_circ = {circuits = Mp.empty; bitstrings = Mp.empty; - qfabvops = Mp.empty; bsarrays = Mp.empty; - bsarrayops = Mp.empty; }; + env_crbds = empty_crbindings; env_thenvs = Mp.empty; } (* -------------------------------------------------------------------- *) @@ -1123,10 +1128,7 @@ module MC = struct | Th_instance _ | Th_auto _ | Th_reduction _ - | Th_bitstring _ - | Th_bsarray _ - | Th_qfabvop _ - | Th_circuit _ -> (mc, None) + | Th_crbinding _ -> (mc, None) in let (mc, submcs) = @@ -2818,78 +2820,89 @@ end (* -------------------------------------------------------------------- *) module Circuit = struct - let rebind_bitstring_ (bs : bitstring) (circuits : circuits) : circuits = - { circuits with bitstrings = Mp.add bs.type_ bs circuits.bitstrings } + let rebind_bitstring_ (bs : crb_bitstring) (bindings : crbindings) = + { bindings with bitstrings = Mp.add bs.type_ bs bindings.bitstrings } - let rebind_bitstring (bs : bitstring) (env : env) : env = - { env with env_circ = rebind_bitstring_ bs env.env_circ } + let rebind_bitstring (bs : crb_bitstring) (env : env) : env = + { env with env_crbds = rebind_bitstring_ bs env.env_crbds } - let bind_bitstring ?(import = import0) (lc : is_local) (bs : bitstring) (env : env) : env = + let bind_bitstring ?(import = import0) (lc : is_local) (bs : crb_bitstring) (env : env) = let env = if import.im_immediate then rebind_bitstring bs env else env in - { env with env_item = mkitem import (Th_bitstring (bs, lc)) :: env.env_item; } + { env with env_item = + mkitem import (Th_crbinding (CRB_Bitstring bs, lc)) :: env.env_item; } - let rebind_bsarray_ (ba : bsarray) (circuits : circuits) : circuits = - { circuits with - bsarrays = Mp.add ba.type_ ba circuits.bsarrays; - bsarrayops = + let rebind_array_ (ba : crb_array) (bindings : crbindings) = + { bindings with + arrays = Mp.add ba.type_ ba bindings.arrays; + arrayops = List.fold_left (fun map (p, kind) -> Mp.add p kind map) - circuits.bsarrayops + bindings.arrayops [ (ba.set, SET ba.size); (ba.get, GET ba.size)]; } - let rebind_bsarray (ba : bsarray) (env : env) : env = - { env with env_circ = rebind_bsarray_ ba env.env_circ } + let rebind_array (ba : crb_array) (env : env) : env = + { env with env_crbds = rebind_array_ ba env.env_crbds } - let bind_bsarray ?(import = import0) (lc : is_local) (ba : bsarray) (env : env) : env = - let env = if import.im_immediate then rebind_bsarray ba env else env in - { env with env_item = mkitem import (Th_bsarray (ba, lc)) :: env.env_item; } + let bind_array ?(import = import0) (lc : is_local) (ba : crb_array) (env : env) = + let env = if import.im_immediate then rebind_array ba env else env in + { env with env_item = + mkitem import (Th_crbinding (CRB_Array ba, lc)) :: env.env_item; } - let rebind_qfabvop_ (op : qfabvop) (circuits : circuits) : circuits = - { circuits with - qfabvops = Mp.add op.operator op circuits.qfabvops } + let rebind_bvoperator_ (op : crb_bvoperator) (bindings : crbindings) = + { bindings with + bvoperators = Mp.add op.operator op bindings.bvoperators } - let rebind_qfabvop (op : qfabvop) (env : env) : env = - { env with env_circ = rebind_qfabvop_ op env.env_circ } + let rebind_bvoperator (op : crb_bvoperator) (env : env) = + { env with env_crbds = rebind_bvoperator_ op env.env_crbds } - let bind_qfabvop ?(import = import0) (lc : is_local) (op : qfabvop) (env : env) : env = - let env = if import.im_immediate then rebind_qfabvop op env else env in - { env with env_item = mkitem import (Th_qfabvop (op, lc)) :: env.env_item; } + let bind_bvoperator ?(import = import0) (lc : is_local) (op : crb_bvoperator) (env : env) = + let env = if import.im_immediate then rebind_bvoperator op env else env in + { env with env_item = + mkitem import (Th_crbinding (CRB_BvOperator op, lc)) :: env.env_item; } - let rebind_circuit_ (cr : circuit) (circuits : circuits) : circuits = - { circuits with - circuits = Mp.add cr.operator cr circuits.circuits } + let rebind_circuit_ (cr : crb_circuit) (bindings : crbindings) = + { bindings with + circuits = Mp.add cr.operator cr bindings.circuits } - let rebind_circuit (cr : circuit) (env : env) : env = - { env with env_circ = rebind_circuit_ cr env.env_circ } + let rebind_circuit (cr : crb_circuit) (env : env) = + { env with env_crbds = rebind_circuit_ cr env.env_crbds } - let bind_circuit ?(import = import0) (lc : is_local) (cr : circuit) (env: env) : env = + let bind_circuit ?(import = import0) (lc : is_local) (cr : crb_circuit) (env : env) = let env = if import.im_immediate then rebind_circuit cr env else env in - { env with env_item = mkitem import (Th_circuit (cr, lc)) :: env.env_item; } + { env with env_item = + mkitem import (Th_crbinding (CRB_Circuit cr, lc)) :: env.env_item; } + + let bind_crbinding ?import (lc : is_local) (crb : crbinding) (env : env) = + match crb with + | CRB_Bitstring bs -> bind_bitstring ?import lc bs env + | CRB_Array ba -> bind_array ?import lc ba env + | CRB_BvOperator op -> bind_bvoperator ?import lc op env + | CRB_Circuit cr -> bind_circuit ?import lc cr env - let lookup_bitstring_path (env: env) (k: path) : bitstring option = + let lookup_bitstring_path (env : env) (k : path) : crb_bitstring option = let k, _ = Ty.lookup (EcPath.toqsymbol k) (env) in - Mp.find_opt k env.env_circ.bitstrings + Mp.find_opt k env.env_crbds.bitstrings - let lookup_bitstring (env: env) (ty:ty) : bitstring option = + let lookup_bitstring (env : env) (ty : ty) : crb_bitstring option = match ty.ty_node with | Tconstr (p, []) -> lookup_bitstring_path env p | _ -> None - let lookup_bitstring_size_path (env: env) (pth: path) : int option = - Option.map (fun (c: bitstring) -> c.size) (lookup_bitstring_path env pth) + let lookup_bitstring_size_path (env : env) (pth : path) : int option = + Option.map (fun (c : crb_bitstring) -> c.size) (lookup_bitstring_path env pth) - let lookup_circuit_path (env: env) (v: path) : Lospecs.Ast.adef option = - Mp.find_opt v env.env_circ.circuits + let lookup_circuit_path (env : env) (v : path) : Lospecs.Ast.adef option = + Mp.find_opt v env.env_crbds.circuits |> Option.map (fun cr -> cr.circuit) - let lookup_bitstring_size (env: env) (ty: ty) : int option = - Option.map (fun (c: bitstring) -> c.size) (lookup_bitstring env ty) + let lookup_bitstring_size (env : env) (ty : ty) : int option = + Option.map (fun (c : crb_bitstring) -> c.size) (lookup_bitstring env ty) - let lookup_bsarray_path (env: env) (pth: path) : bsarray option = + let lookup_bsarray_path (env : env) (pth : path) : crb_array option = let k, _ = Ty.lookup (EcPath.toqsymbol pth) (env) in - Mp.find_opt k env.env_circ.bsarrays + Mp.find_opt k env.env_crbds.arrays - let lookup_bsarray (env: env) (ty: ty) : bsarray option = + let lookup_bsarray (env: env) (ty: ty) : crb_array option = match ty.ty_node with | Tconstr (p, [w]) -> lookup_bsarray_path env p | _ -> None @@ -2901,15 +2914,15 @@ module Circuit = struct let p, _o = Op.lookup o env in lookup_circuit_path env p - let lookup_qfabvop_path (env: env) (v: path) : qfabvop option = - Mp.find_opt v env.env_circ.qfabvops + let lookup_bvoperator_path (env: env) (v: path) : crb_bvoperator option = + Mp.find_opt v env.env_crbds.bvoperators - let lookup_qfabvop (env: env) (o: qsymbol) : qfabvop option = + let lookup_bvoperator (env: env) (o: qsymbol) : crb_bvoperator option = let p, _o = Op.lookup o env in - lookup_qfabvop_path env p + lookup_bvoperator_path env p - let lookup_bsarrayop (env: env) (pth: path) : bsarrayop option = - Mp.find_opt pth env.env_circ.bsarrayops + let lookup_bsarrayop (env: env) (pth: path) : crb_array_op option = + Mp.find_opt pth env.env_crbds.arrayops end (* -------------------------------------------------------------------- *) @@ -3084,18 +3097,18 @@ module Theory = struct (* ------------------------------------------------------------------ *) let bind_cr_th = - let for1 (_ : path) (circuits : circuits) = function - | Th_bitstring (bs, _) -> - Some (Circuit.rebind_bitstring_ bs circuits) + let for1 (_ : path) (bindings : crbindings) = function + | Th_crbinding (CRB_Bitstring bs, _) -> + Some (Circuit.rebind_bitstring_ bs bindings) - | Th_bsarray (ba, _) -> - Some (Circuit.rebind_bsarray_ ba circuits) + | Th_crbinding (CRB_Array ba, _) -> + Some (Circuit.rebind_array_ ba bindings) - | Th_qfabvop (op, _) -> - Some (Circuit.rebind_qfabvop_ op circuits) + | Th_crbinding (CRB_BvOperator op, _) -> + Some (Circuit.rebind_bvoperator_ op bindings) - | Th_circuit (circuit, _) -> - Some (Circuit.rebind_circuit_ circuit circuits) + | Th_crbinding (CRB_Circuit cr, _) -> + Some (Circuit.rebind_circuit_ cr bindings) | _ -> None in bind_base_th for1 @@ -3123,12 +3136,12 @@ module Theory = struct let env_atbase = bind_at_th thname env.env_atbase items in let env_ntbase = bind_nt_th thname env.env_ntbase items in let env_redbase = bind_rd_th thname env.env_redbase items in - let env_circ = bind_cr_th thname env.env_circ items in + let env_crbds = bind_cr_th thname env.env_crbds items in let env = { env with env_tci ; env_tc ; env_rwbase; env_atbase; env_ntbase; env_redbase; - env_circ ; } + env_crbds ; } in add_restr_th thname env items @@ -3193,11 +3206,7 @@ module Theory = struct | Th_instance _ | Th_auto _ | Th_reduction _ - | Th_bitstring _ - | Th_bsarray _ - | Th_qfabvop _ - | Th_circuit _ -> env - + | Th_crbinding _ -> env in List.fold_left import_th_item env th diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 595863d574..d0ec9f4410 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -17,7 +17,7 @@ type 'a suspension = { } (* -------------------------------------------------------------------- *) -type bsarrayop = +type crb_array_op = | GET of int | SET of int @@ -435,24 +435,25 @@ end (* -------------------------------------------------------------------- *) module Circuit : sig - val bind_bitstring : ?import:import -> is_local -> bitstring -> env -> env - val bind_bsarray : ?import:import -> is_local -> bsarray -> env -> env - val bind_qfabvop : ?import:import -> is_local -> qfabvop -> env -> env - val bind_circuit : ?import:import -> is_local -> circuit -> env -> env - - val lookup_bitstring : env -> ty -> bitstring option - val lookup_bitstring_path : env -> path -> bitstring option + val bind_bitstring : ?import:import -> is_local -> crb_bitstring -> env -> env + val bind_array : ?import:import -> is_local -> crb_array -> env -> env + val bind_bvoperator : ?import:import -> is_local -> crb_bvoperator -> env -> env + val bind_circuit : ?import:import -> is_local -> crb_circuit -> env -> env + val bind_crbinding : ?import:import -> is_local -> crbinding -> env -> env + + val lookup_bitstring : env -> ty -> crb_bitstring option + val lookup_bitstring_path : env -> path -> crb_bitstring option val lookup_bitstring_size : env -> ty -> int option val lookup_circuit : env -> qsymbol -> Lospecs.Ast.adef option val lookup_bitstring_size_path : env -> path -> int option val lookup_circuit_path : env -> path -> Lospecs.Ast.adef option - val lookup_qfabvop_path : env -> path -> qfabvop option - val lookup_qfabvop : env -> qsymbol -> qfabvop option + val lookup_bvoperator_path : env -> path -> crb_bvoperator option + val lookup_bvoperator : env -> qsymbol -> crb_bvoperator option - val lookup_bsarray : env -> ty -> bsarray option - val lookup_bsarray_path : env -> path -> bsarray option + val lookup_bsarray : env -> ty -> crb_array option + val lookup_bsarray_path : env -> path -> crb_array option val lookup_bsarray_size : env -> ty -> int option - val lookup_bsarrayop : env -> path -> bsarrayop option + val lookup_bsarrayop : env -> path -> crb_array_op option end (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 5e2ccf15ae..86deb7ed51 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3888,6 +3888,25 @@ user_red_option: (Some ("invalid option: " ^ (unloc x))) } +(* -------------------------------------------------------------------- *) +(* Circuit & bo bindings *) +cr_binding_r: +| BIND BITSTRING from_=qoident to_=qoident type_=loc(simpl_type_exp) size=uint + { CRB_Bitstring { from_; to_; type_; size; } } + +| BIND ARRAY get=qoident set=qoident tolist=qoident type_=qoident size=uint + { CRB_Array { get; set; tolist; type_; size; } } + +| BIND OP type_=loc(simpl_type_exp) operator=qoident name=loc(STRING) + { CRB_BvOperator { type_; operator; name; } } + +| BIND CIRCUIT operator=qoident circuit=loc(STRING) + { CRB_Circuit { operator; circuit; } } + +%inline cr_binding: +| locality=is_local binding=cr_binding_r + { { locality; binding; }} + (* -------------------------------------------------------------------- *) (* Search pattern *) %inline search: x=sform_h { x } @@ -3924,6 +3943,7 @@ global_action: | gprover_info { Gprover_info $1 } | addrw { Gaddrw $1 } | hint { Ghint $1 } +| cr_binding { Gcrbinding $1 } | x=loc(proofend) { Gsave x } | PRINT p=print { Gprint p } | PRINT AXIOM { Gpaxiom } @@ -3931,18 +3951,6 @@ global_action: | LOCATE x=qident { Glocate x } | WHY3 x=STRING { GdumpWhy3 x } -| local=is_local BIND BITSTRING from_=qoident to_=qoident type_=loc(simpl_type_exp) size=uint - { Gbbitstring { local; from_; to_; type_; size; } } - -| local=is_local BIND ARRAY get=qoident set=qoident tolist=qoident type_=qoident size=uint - { Gbbsarray { local; get; set; tolist; type_; size; } } - -| local=is_local BIND OP type_=loc(simpl_type_exp) operator=qoident name=loc(STRING) - { Gbqfabvop { local; type_; operator; name; } } - -| local=is_local BIND CIRCUIT operator=qoident circuit=loc(STRING) - { Gbcircuit { local; operator; circuit; } } - | PRAGMA x=pragma { Gpragma x } | PRAGMA PLUS x=pragma { Goption (x, `Bool true ) } | PRAGMA MINUS x=pragma { Goption (x, `Bool false) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 2c8eee2956..57429f6b0a 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1270,34 +1270,40 @@ type threquire = (* -------------------------------------------------------------------- *) type pbind_bitstring = - { local : is_local - ; from_ : pqsymbol + { from_ : pqsymbol ; to_ : pqsymbol ; type_ : pty ; size : EcBigInt.zint } (* -------------------------------------------------------------------- *) type pbind_array = - { local : is_local - ; get : pqsymbol + { get : pqsymbol ; set : pqsymbol ; tolist : pqsymbol ; type_ : pqsymbol ; size : EcBigInt.zint } (* -------------------------------------------------------------------- *) -type pbind_qfabvop = - { local : is_local - ; name : string located +type pbind_bvoperator = + { name : string located ; type_ : pty ; operator : pqsymbol } (* -------------------------------------------------------------------- *) type pbind_circuit = - { local : is_local - ; operator : pqsymbol + { operator : pqsymbol ; circuit : string located } +(* -------------------------------------------------------------------- *) +type pcrbinding_r = + | CRB_Bitstring of pbind_bitstring + | CRB_Array of pbind_array + | CRB_BvOperator of pbind_bvoperator + | CRB_Circuit of pbind_circuit + +(* -------------------------------------------------------------------- *) +type pcrbinding = { locality : is_local; binding : pcrbinding_r } + (* -------------------------------------------------------------------- *) type global_action = | Gmodule of pmodule_def_or_decl @@ -1336,10 +1342,7 @@ type global_action = | Gpragma of psymbol | Goption of (psymbol * [`Bool of bool | `Int of int]) | GdumpWhy3 of string - | Gbbitstring of pbind_bitstring - | Gbbsarray of pbind_array - | Gbcircuit of pbind_circuit - | Gbqfabvop of pbind_qfabvop + | Gcrbinding of pcrbinding type global = { gl_action : global_action located; diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index f995105277..24ec36a03c 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -3371,7 +3371,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = lvl (odfl "" base) (pp_list "@ " (pp_axname ppe)) p - | EcTheory.Th_bitstring (bs, lc) -> + | EcTheory.Th_crbinding (binding, lc) -> begin + match binding with + | CRB_Bitstring bs -> Format.fprintf fmt "%abind bitstring %a %a %a %d." pp_locality lc (pp_opname ppe) bs.to_ @@ -3379,7 +3381,7 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = (pp_tyname ppe) bs.type_ bs.size - | EcTheory.Th_bsarray (ba, lc) -> + | CRB_Array ba -> Format.fprintf fmt "%abind array %a %a %a %a %d." pp_locality lc (pp_tyname ppe) ba.type_ @@ -3388,7 +3390,7 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = (pp_opname ppe) ba.tolist ba.size - | EcTheory.Th_qfabvop (op, lc) -> + | CRB_BvOperator op -> let kind = match op.kind with | `Add _ -> "add" @@ -3408,9 +3410,10 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = (pp_opname ppe) op.operator kind - | EcTheory.Th_circuit (circuit, lc) -> + | CRB_Circuit cr -> Format.fprintf fmt "%abind circuit %a \"%s\"." - pp_locality lc (pp_opname ppe) circuit.operator circuit.name + pp_locality lc (pp_opname ppe) cr.operator cr.name + end (* -------------------------------------------------------------------- *) let pp_stmt_with_nums (ppe : PPEnv.t) fmt stmt = diff --git a/src/ecScope.ml b/src/ecScope.ml index 93ceacc95a..c25291d07c 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2303,12 +2303,7 @@ module Cloning = struct end (* -------------------------------------------------------------------- *) -module Circuit : sig - val add_bitstring : scope -> pbind_bitstring -> scope - val add_bsarray : scope -> pbind_array -> scope - val add_qfabvop : scope -> pbind_qfabvop -> scope - val add_circuit : scope -> pbind_circuit -> scope -end = struct +module Circuit = struct type preoperator = [`Path of path | `Int of BI.zint] type clone = { @@ -2365,7 +2360,7 @@ end = struct (proofs, scope) - let add_bitstring (scope : scope) (bs : pbind_bitstring) : scope = + let add_bitstring (scope : scope) (local : is_local) (bs : pbind_bitstring) : scope = let env = env scope in let type_ = @@ -2388,7 +2383,7 @@ end = struct let preclone = { path = EcPath.fromqsymbol (["Top"; "QFABV"], "BV") ; name = name - ; local = bs.local + ; local = local ; types_ = ["bv", bspath] ; operators = [ ("size" , `Int bs.size) @@ -2398,19 +2393,19 @@ end = struct let proofs, scope = doclone scope preclone in - let item : EcTheory.bitstring = + let item = CRB_Bitstring { from_; to_; type_ = bspath; size = BI.to_int bs.size; theory = pqname (EcEnv.root env) name; } in - let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_bitstring (item, bs.local)) in + let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_crbinding (item, local)) 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 add_bsarray (scope : scope) (local : is_local) (ba : pbind_array) : scope = let env = env scope in let bspath = @@ -2435,7 +2430,7 @@ end = struct let preclone = { path = EcPath.fromqsymbol (["Top"; "QFABV"], "A") ; name = name - ; local = ba.local + ; local = local ; types_ = ["t", bspath] ; operators = [ ("size" , `Int ba.size) @@ -2446,16 +2441,16 @@ end = struct let proofs, scope = doclone scope preclone in - let item : EcTheory.bsarray = + let item = CRB_Array { get; set; tolist; type_ = bspath; size = BI.to_int ba.size } in - let item = EcTheory.mkitem EcTheory.import0 (Th_bsarray (item, ba.local)) in + let item = EcTheory.mkitem EcTheory.import0 (Th_crbinding (item, local)) in let scope = { scope with sc_env = EcSection.add_item item scope.sc_env } in Ax.add_defer scope proofs - let add_qfabvop (scope : scope) (op : pbind_qfabvop) : scope = + let add_qfabvop (scope : scope) (local : is_local) (op : pbind_bvoperator) : scope = let env = env scope in let type_ = @@ -2479,7 +2474,7 @@ end = struct "this type is not bound to a bitstring type" | Some bitstring -> bitstring in - let (kind, subname) : EcTheory.qfabv_opkind * _ = + let (kind, subname) : EcDecl.bv_opkind * _ = match unloc op.name with | "add" -> `Add bitstring.size, "Add" | "sub" -> `Sub bitstring.size, "Sub" @@ -2505,27 +2500,27 @@ end = struct let preclone = { path = subpath ; name = name - ; local = op.local + ; local = local ; types_ = [] ; operators = ["bv" ^ unloc op.name, `Path operator] ; proofs = [] } in let proofs, scope = doclone scope preclone in - let item : EcTheory.qfabvop = + let item = CRB_BvOperator { kind = kind; type_ = bspath; operator = operator; theory = subpath; } in - let item = EcTheory.mkitem EcTheory.import0 (Th_qfabvop (item, op.local)) in + let item = EcTheory.mkitem EcTheory.import0 (Th_crbinding (item, local)) in let scope = { scope with sc_env = EcSection.add_item item scope.sc_env } in Ax.add_defer scope proofs - let add_circuit (scope : scope) (pc : pbind_circuit) : scope = + let add_circuit (scope : scope) (local : is_local) (pc : pbind_circuit) : scope = let env = env scope in let operator, opdecl = EcEnv.Op.lookup pc.operator.pl_desc env in @@ -2578,11 +2573,11 @@ end = struct (EcPrinting.pp_type ppe) codom ret end; - let item : EcTheory.circuit = { operator; circuit; name = unloc pc.circuit; } in + let item = CRB_Circuit { operator; circuit; name = unloc pc.circuit; } in let item = EcTheory.mkitem EcTheory.import0 - (EcTheory.Th_circuit (item, pc.local)) in + (EcTheory.Th_crbinding (item, local)) in { scope with sc_env = EcSection.add_item item scope.sc_env } end diff --git a/src/ecScope.mli b/src/ecScope.mli index 83b13f3024..79efbf526d 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -246,10 +246,10 @@ end (* -------------------------------------------------------------------- *) module Circuit : sig - val add_bitstring : scope -> pbind_bitstring -> scope - val add_bsarray : scope -> pbind_array -> scope - val add_qfabvop : scope -> pbind_qfabvop -> scope - val add_circuit : scope -> pbind_circuit -> scope + val add_bitstring : scope -> is_local -> pbind_bitstring -> scope + val add_bsarray : scope -> is_local -> pbind_array -> scope + val add_qfabvop : scope -> is_local -> pbind_bvoperator -> scope + val add_circuit : scope -> is_local -> pbind_circuit -> scope end (* -------------------------------------------------------------------- *) diff --git a/src/ecSection.ml b/src/ecSection.ml index a6bbb991f3..c81c9d82ac 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -22,10 +22,7 @@ type cbarg = [ | `ModuleType of path | `Typeclass of path | `Instance of tcinstance - | `Bitstring of bitstring * is_local - | `Bsarray of bsarray * is_local - | `Qfabvop of qfabvop * is_local - | `Circuit of circuit * is_local + | `Crbind of crbinding * is_local ] type cb = cbarg -> unit @@ -60,10 +57,14 @@ let pp_cbarg env fmt (who : cbarg) = | `Field _ -> Format.fprintf fmt "field instance" | `General _ -> Format.fprintf fmt "instance" end - | `Bitstring _ -> Format.fprintf fmt "bitstring binding" - | `Bsarray _ -> Format.fprintf fmt "array binding" - | `Qfabvop _ -> Format.fprintf fmt "bitstring operator binding" - | `Circuit _ -> Format.fprintf fmt "circuit binding" + | `Crbind (CRB_Bitstring _, _) -> + Format.fprintf fmt "bitstring binding" + | `Crbind (CRB_Array _, _) -> + Format.fprintf fmt "array binding" + | `Crbind (CRB_BvOperator _, _) -> + Format.fprintf fmt "bitstring operator binding" + | `Crbind (CRB_Circuit _, _) -> + Format.fprintf fmt "circuit binding" let pp_locality fmt = function | `Local -> Format.fprintf fmt "local" @@ -524,10 +525,7 @@ let locality (env : EcEnv.env) (who : cbarg) = | _ -> `Global end | `ModuleType p -> ((EcEnv.ModTy.by_path p env).tms_loca :> locality) - | `Bitstring (_, lc) -> (lc :> locality) - | `Bsarray (_, lc) -> (lc :> locality) - | `Qfabvop (_, lc) -> (lc :> locality) - | `Circuit (_, lc) -> (lc :> locality) + | `Crbind (_, lc) -> (lc :> locality) | `Instance _ -> assert false (* -------------------------------------------------------------------- *) @@ -1036,6 +1034,11 @@ let generalize_auto to_gen (n,s,ps,lc) = if ps = [] then to_gen, None else to_gen, Some (Th_auto (n,s,ps,lc)) +let generalize_crbinding (to_gen : to_gen) ((bd, lc) : crbinding * is_local) = + let item = + if lc = `Local then None else Some (Th_crbinding (bd, lc)) + in to_gen, item + (* --------------------------------------------------------------- *) let get_locality scenv = scenv.sc_loca @@ -1060,10 +1063,7 @@ let rec set_local_item item = | Th_addrw (p,ps,lc) -> Th_addrw (p, ps, set_local lc) | Th_reduction r -> Th_reduction r | Th_auto (i,s,p,lc) -> Th_auto (i, s, p, set_local lc) - | Th_bitstring (bs, lc) -> Th_bitstring (bs, set_local lc) - | Th_bsarray (ba, lc) -> Th_bsarray (ba, set_local lc) - | Th_qfabvop (op, lc) -> Th_qfabvop (op, lc) - | Th_circuit (cr, lc) -> Th_circuit (cr, lc) + | Th_crbinding (bd, lc) -> Th_crbinding (bd, set_local lc) in { item with ti_item = lcitem } @@ -1142,11 +1142,7 @@ let can_depend (cd : can_depend) (who : cbarg) = | `ModuleType _ -> cd.d_modty | `Typeclass _ -> cd.d_tc | `Instance _ -> assert false - | `Bitstring _ -> assert false (* FIXME *) - | `Bsarray _ -> assert false (* FIXME *) - | `Qfabvop _ -> assert false (* FIXME *) - | `Circuit _ -> assert false (* FIXME *) - + | `Crbind _ -> assert false (* FIXME *) let cb scenv from cd who = let env = scenv.sc_env in @@ -1329,8 +1325,8 @@ let check_instance scenv ty tci lc = let cd = { cd_glob with d_ty = [`Declare; `Global]; } in on_instance (cb scenv from cd) ty tci -let check_bitstring (scenv : scenv) ((bs, lc) : bitstring * is_local) = - let from = (lc :> locality), `Bitstring (bs, lc) in +let check_crb_bitstring (scenv : scenv) ((bs, lc) : crb_bitstring * is_local) = + let from = (lc :> locality), `Crbind (CRB_Bitstring bs, lc) in if lc = `Local then check_section scenv from else if scenv.sc_insec then begin @@ -1338,8 +1334,8 @@ let check_bitstring (scenv : scenv) ((bs, lc) : bitstring * is_local) = cb scenv from cd_glob (`Type bs.type_) end -let check_bsarray (scenv : scenv) ((ba, lc) : bsarray * is_local) = - let from = (lc :> locality), `Bsarray (ba, lc) in +let check_crb_array (scenv : scenv) ((ba, lc) : crb_array * is_local) = + let from = (lc :> locality), `Crbind (CRB_Array ba, lc) in if lc = `Local then check_section scenv from else if scenv.sc_insec then begin @@ -1347,8 +1343,8 @@ let check_bsarray (scenv : scenv) ((ba, lc) : bsarray * is_local) = cb scenv from cd_glob (`Type ba.type_) end -let check_qfabvop (scenv : scenv) ((op, lc) : qfabvop * is_local) = - let from = (lc :> locality), `Qfabvop (op, lc) in +let check_crb_bvoperator (scenv : scenv) ((op, lc) : crb_bvoperator * is_local) = + let from = (lc :> locality), `Crbind (CRB_BvOperator op, lc) in if lc = `Local then check_section scenv from else if scenv.sc_insec then begin @@ -1356,13 +1352,20 @@ let check_qfabvop (scenv : scenv) ((op, lc) : qfabvop * is_local) = cb scenv from cd_glob (`Type op.type_) end -let check_circuit (scenv : scenv) ((cr, lc) : circuit * is_local) = - let from = (lc :> locality), `Circuit (cr, lc) in +let check_crb_circuit (scenv : scenv) ((cr, lc) : crb_circuit * is_local) = + let from = (lc :> locality), `Crbind (CRB_Circuit cr, lc) in if lc = `Local then check_section scenv from else if scenv.sc_insec then cb scenv from cd_glob (`Op cr.operator) - + +let check_crbinding (scenv : scenv) ((crb, lc) : crbinding * is_local) = + match crb with + | CRB_Bitstring bs -> check_crb_bitstring scenv (bs, lc) + | CRB_Array ba -> check_crb_array scenv (ba, lc) + | CRB_BvOperator op -> check_crb_bvoperator scenv (op, lc) + | CRB_Circuit cr -> check_crb_circuit scenv (cr, lc) + (* -----------------------------------------------------------*) let enter_theory (name:symbol) (lc:is_local) (mode:thmode) scenv : scenv = if not scenv.sc_insec && lc = `Local then @@ -1402,10 +1405,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 (bs, lc) -> EcEnv.Circuit.bind_bitstring lc bs env - | Th_bsarray (ba, lc) -> EcEnv.Circuit.bind_bsarray lc ba env - | Th_qfabvop (op, lc) -> EcEnv.Circuit.bind_qfabvop lc op env - | Th_circuit (cr, lc) -> EcEnv.Circuit.bind_circuit lc cr env + | Th_crbinding (bd, lc) -> EcEnv.Circuit.bind_crbinding lc bd env | Th_theory _ -> assert false in { scenv with @@ -1420,26 +1420,20 @@ let add_th ~import (cth : EcEnv.Theory.compiled_theory) scenv = let rec generalize_th_item (to_gen : to_gen) (prefix : path) (th_item : theory_item) = let to_gen, item = match th_item.ti_item with - | Th_type tydecl -> generalize_tydecl to_gen prefix tydecl - | Th_operator opdecl -> generalize_opdecl to_gen prefix opdecl - | Th_axiom ax -> generalize_axiom to_gen prefix ax - | Th_modtype ms -> generalize_modtype to_gen ms - | Th_module me -> generalize_module to_gen prefix me - | Th_theory th -> (generalize_ctheory to_gen prefix th, None) - | Th_export (p,lc) -> generalize_export to_gen (p,lc) - | Th_instance tci -> generalize_instance to_gen tci - | Th_typeclass _ -> assert false - | Th_baserw (s,lc) -> generalize_baserw to_gen prefix (s,lc) - | Th_addrw (p,ps,lc) -> generalize_addrw to_gen (p, ps, lc) - | Th_reduction rl -> generalize_reduction to_gen rl - | Th_auto hints -> generalize_auto to_gen hints - | Th_bitstring (_, lc) - | Th_bsarray (_, lc) - | Th_qfabvop (_, lc) - | Th_circuit (_, lc) -> - let item = if lc = `Local then None else Some th_item.ti_item in - to_gen, item - + | Th_type tydecl -> generalize_tydecl to_gen prefix tydecl + | Th_operator opdecl -> generalize_opdecl to_gen prefix opdecl + | Th_axiom ax -> generalize_axiom to_gen prefix ax + | Th_modtype ms -> generalize_modtype to_gen ms + | Th_module me -> generalize_module to_gen prefix me + | Th_theory th -> (generalize_ctheory to_gen prefix th, None) + | Th_export (p,lc) -> generalize_export to_gen (p,lc) + | Th_instance tci -> generalize_instance to_gen tci + | Th_typeclass _ -> assert false + | Th_baserw (s,lc) -> generalize_baserw to_gen prefix (s,lc) + | Th_addrw (p,ps,lc) -> generalize_addrw to_gen (p, ps, lc) + | Th_reduction rl -> generalize_reduction to_gen rl + | Th_auto hints -> generalize_auto to_gen hints + | Th_crbinding (bd, lc) -> generalize_crbinding to_gen (bd, lc) in let scenv = @@ -1560,10 +1554,7 @@ let check_item scenv item = if (lc = `Local && not scenv.sc_insec) then hierror "local hint can only be declared inside section"; | Th_reduction _ -> () (* FIXME *) - | Th_bitstring (bs, lc) -> check_bitstring scenv (bs, lc) - | Th_bsarray (ba, lc) -> check_bsarray scenv (ba, lc) - | Th_qfabvop (op, lc) -> check_qfabvop scenv (op, lc) - | Th_circuit (cr, lc) -> check_circuit scenv (cr, lc) + | Th_crbinding (crb, lc) -> check_crbinding scenv (crb, lc) | Th_theory _ -> assert false let rec add_item (item : theory_item) (scenv : scenv) = diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 4abcc9d4ed..86d9f64c45 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1033,6 +1033,48 @@ let subst_tc (s : subst) tc = let tc_axs = List.map (snd_map (subst_form s)) tc.tc_axs in { tc_prt; tc_ops; tc_axs; tc_loca = tc.tc_loca } +(* -------------------------------------------------------------------- *) +let subst_crbinding (s : subst) (crb : crbinding) = + match crb with + | CRB_Bitstring bs -> + assert (not (Mp.mem bs.type_ s.sb_tydef)); + assert (not (Mp.mem bs.from_ s.sb_def)); + assert (not (Mp.mem bs.to_ s.sb_def)); + CRB_Bitstring { + type_ = subst_path s bs.type_; + from_ = subst_path s bs.from_; + to_ = subst_path s bs.to_; + size = bs.size; + theory = subst_path s bs.theory; } + + | CRB_Array ba -> + assert (not (Mp.mem ba.type_ s.sb_tydef)); + assert (not (Mp.mem ba.get s.sb_def)); + assert (not (Mp.mem ba.set s.sb_def)); + assert (not (Mp.mem ba.tolist s.sb_def)); + CRB_Array { + type_ = subst_path s ba.type_; + get = subst_path s ba.get; + set = subst_path s ba.set; + tolist = subst_path s ba.tolist; + size = ba.size; } + + | CRB_BvOperator op -> + assert (not (Mp.mem op.type_ s.sb_tydef)); + assert (not (Mp.mem op.operator s.sb_def)); + CRB_BvOperator { + kind = op.kind; + type_ = subst_path s op.type_; + operator = subst_path s op.operator; + theory = subst_path s op.theory; } + + | CRB_Circuit cr -> + assert (not (Mp.mem cr.operator s.sb_def)); + CRB_Circuit { + name = cr.name; + circuit = cr.circuit; + operator = subst_path s cr.operator; } + (* -------------------------------------------------------------------- *) (* SUBSTITUTION OVER THEORIES *) let rec subst_theory_item_r (s : subst) (item : theory_item_r) = @@ -1078,48 +1120,8 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = | Th_auto (lvl, base, ps, lc) -> Th_auto (lvl, base, List.map (subst_path s) ps, lc) - | Th_bitstring (bs, lc) -> - assert (not (Mp.mem bs.type_ s.sb_tydef)); - assert (not (Mp.mem bs.from_ s.sb_def)); - assert (not (Mp.mem bs.to_ s.sb_def)); - let bs = { - type_ = subst_path s bs.type_; - from_ = subst_path s bs.from_; - to_ = subst_path s bs.to_; - size = bs.size; - theory = subst_path s bs.theory; - } in Th_bitstring (bs, lc) - - | Th_bsarray (ba, lc) -> - assert (not (Mp.mem ba.type_ s.sb_tydef)); - assert (not (Mp.mem ba.get s.sb_def)); - assert (not (Mp.mem ba.set s.sb_def)); - assert (not (Mp.mem ba.tolist s.sb_def)); - let ba = { - type_ = subst_path s ba.type_; - get = subst_path s ba.get; - set = subst_path s ba.set; - tolist = subst_path s ba.tolist; - size = ba.size; - } in Th_bsarray (ba, lc) - - | Th_qfabvop (op, lc) -> - assert (not (Mp.mem op.type_ s.sb_tydef)); - assert (not (Mp.mem op.operator s.sb_def)); - let op = { - kind = op.kind; - type_ = subst_path s op.type_; - operator = subst_path s op.operator; - theory = subst_path s op.theory; - } in Th_qfabvop (op, lc) - - | Th_circuit (circuit, lc) -> - assert (not (Mp.mem circuit.operator s.sb_def)); - let circuit = { - name = circuit.name; - circuit = circuit.circuit; - operator = subst_path s circuit.operator; - } in Th_circuit (circuit, lc) + | Th_crbinding (bd, lc) -> + Th_crbinding (subst_crbinding s bd, lc) (* -------------------------------------------------------------------- *) and subst_theory (s : subst) (items : theory) = diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 99a5606f86..42b6408670 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -441,10 +441,7 @@ end = struct | Th_addrw _ -> (proofs, evc) | Th_reduction _ -> (proofs, evc) | Th_auto _ -> (proofs, evc) - | Th_bitstring _ -> (proofs, evc) - | Th_bsarray _ -> (proofs, evc) - | Th_qfabvop _ -> (proofs, evc) - | Th_circuit _ -> (proofs, evc) + | Th_crbinding _ -> (proofs, evc) and doit prefix (proofs, evc) dth = doit_r prefix (proofs, evc) dth.ti_item diff --git a/src/ecTheory.ml b/src/ecTheory.ml index 6a65ad2631..e7e4b03587 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -38,42 +38,7 @@ 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 (bitstring * is_local) - | Th_bsarray of (bsarray * is_local) - | Th_qfabvop of (qfabvop * is_local) - | Th_circuit of (circuit * is_local) - -and bitstring = - { type_: path; from_: path; to_: path; size: int; theory: path; } - -and bsarray = - { type_: path; get: path; set: path; tolist: path; size: int; } - -and qfabv_opkind = [ - | `Add of int - | `Sub of int - | `Mul of int - | `UDiv of int - | `URem of int - | `Shl of int - | `Shr of int - | `And of int - | `Or of int - | `Not of int - -] - -and qfabvop = - { kind : qfabv_opkind - ; type_ : path - ; operator : path - ; theory : path } - -and circuit = { - name : string; - circuit : Lospecs.Ast.adef; - operator : path; -} + | Th_crbinding of crbinding * is_local and thsource = { ths_base : EcPath.path; diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 9c443de5fd..b55c567678 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -35,44 +35,8 @@ and theory_item_r = (* reduction rule does not survive to section so no locality *) | 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 (bitstring * is_local) - | Th_bsarray of (bsarray * is_local) - | Th_qfabvop of (qfabvop * is_local) - | Th_circuit of (circuit * is_local) + | Th_crbinding of crbinding * is_local -and bitstring = - { type_: path; from_: path; to_: path; size: int; theory: path; } - -and bsarray = - { type_: path; get: path; set: path; tolist: path; size: int; } - -and qfabv_opkind = [ - | `Add of int - | `Sub of int - | `Mul of int - | `UDiv of int - | `URem of int - | `Shl of int - | `Shr of int - | `And of int - | `Or of int - | `Not of int - -] - -and qfabvop = - { kind : qfabv_opkind - ; type_ : path - ; operator : path - ; theory : path } - -and circuit = { - name : string; - circuit : Lospecs.Ast.adef; - operator : path; -} - and thsource = { ths_base : EcPath.path; } diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 63f34d0d84..333362c5ca 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -947,7 +947,7 @@ and replay_instance (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) -and replay_bitstring (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bs, lc) = +and replay_crb_bitstring (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bs, lc) = let opath = ove.ovre_opath in let npath = ove.ovre_npath in let forpath = forpath ~npath ~opath ~ops in @@ -959,8 +959,8 @@ and replay_bitstring (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bs, l let theory = bs.theory in (* FIXME *) let size = bs.size in - let bs : bitstring = { to_; from_; type_; theory; size; } in - let scope = ove.ovre_hooks.hadd_item scope import (Th_bitstring (bs, lc)) in + let bs = CRB_Bitstring { to_; from_; type_; theory; size; } in + let scope = ove.ovre_hooks.hadd_item scope import (Th_crbinding (bs, lc)) in (subst, ops, proofs, scope) @@ -968,7 +968,7 @@ and replay_bitstring (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bs, l (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) -and replay_bsarray (ove : _ ovrenv) (subst, ops, proofs, scope) (import, ba, lc) = +and replay_crb_array (ove : _ ovrenv) (subst, ops, proofs, scope) (import, ba, lc) = let opath = ove.ovre_opath in let npath = ove.ovre_npath in let forpath = forpath ~npath ~opath ~ops in @@ -980,8 +980,8 @@ and replay_bsarray (ove : _ ovrenv) (subst, ops, proofs, scope) (import, ba, lc) let type_ = ba.type_ in (* FIXME*) let size = ba.size in - let ba : bsarray = { get; set; tolist; type_; size; } in - let scope = ove.ovre_hooks.hadd_item scope import (Th_bsarray (ba, lc)) in + let ba = CRB_Array { get; set; tolist; type_; size; } in + let scope = ove.ovre_hooks.hadd_item scope import (Th_crbinding (ba, lc)) in (subst, ops, proofs, scope) @@ -989,7 +989,7 @@ and replay_bsarray (ove : _ ovrenv) (subst, ops, proofs, scope) (import, ba, lc) (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) -and replay_qfabvop (ove : _ ovrenv) (subst, ops, proofs, scope) (import, op, lc) = +and replay_crb_bvoperator (ove : _ ovrenv) (subst, ops, proofs, scope) (import, op, lc) = let opath = ove.ovre_opath in let npath = ove.ovre_npath in let forpath = forpath ~npath ~opath ~ops in @@ -1000,8 +1000,8 @@ and replay_qfabvop (ove : _ ovrenv) (subst, ops, proofs, scope) (import, op, lc) let type_ = op.type_ in (* FIXME *) let theory = op.theory in (* FIXME *) - let op : qfabvop = { kind; operator; type_; theory; } in - let scope = ove.ovre_hooks.hadd_item scope import (Th_qfabvop (op, lc)) in + let op = CRB_BvOperator { kind; operator; type_; theory; } in + let scope = ove.ovre_hooks.hadd_item scope import (Th_crbinding (op, lc)) in (subst, ops, proofs, scope) @@ -1009,7 +1009,7 @@ and replay_qfabvop (ove : _ ovrenv) (subst, ops, proofs, scope) (import, op, lc) (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) -and replay_circuit (ove : _ ovrenv) (subst, ops, proofs, scope) (import, cr, lc) = +and replay_crb_circuit (ove : _ ovrenv) (subst, ops, proofs, scope) (import, cr, lc) = let opath = ove.ovre_opath in let npath = ove.ovre_npath in let forpath = forpath ~npath ~opath ~ops in @@ -1019,14 +1019,29 @@ and replay_circuit (ove : _ ovrenv) (subst, ops, proofs, scope) (import, cr, lc) let circuit = cr.circuit in let operator = forpath cr.operator in - let cr : circuit = { name; circuit; operator; } in - let scope = ove.ovre_hooks.hadd_item scope import (Th_circuit (cr, lc)) in + let cr = CRB_Circuit { name; circuit; operator; } in + let scope = ove.ovre_hooks.hadd_item scope import (Th_crbinding (cr, lc)) in (subst, ops, proofs, scope) with InvInstPath -> (subst, ops, proofs, scope) +(* -------------------------------------------------------------------- *) +and replay_crbinding (ove : _ ovrenv) (subst, ops, proofs, scope) (import, binding, lc) = + match binding with + | CRB_Bitstring bs -> + replay_crb_bitstring ove (subst, ops, proofs, scope) (import, bs, lc) + + | CRB_Array ba -> + replay_crb_array ove (subst, ops, proofs, scope) (import, ba, lc) + + | CRB_BvOperator op -> + replay_crb_bvoperator ove (subst, ops, proofs, scope) (import, op, lc) + + | CRB_Circuit cr -> + replay_crb_circuit ove (subst, ops, proofs, scope) (import, cr, lc) + (* -------------------------------------------------------------------- *) and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item = match item.ti_item with @@ -1072,17 +1087,8 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item = | Th_instance ((typ, ty), tc, lc) -> replay_instance ove (subst, ops, proofs, scope) (item.ti_import, (typ, ty), tc, lc) - | Th_bitstring (bs, lc) -> - replay_bitstring ove (subst, ops, proofs, scope) (item.ti_import, bs, lc) - - | Th_bsarray (ba, lc) -> - replay_bsarray ove (subst, ops, proofs, scope) (item.ti_import, ba, lc) - - | Th_qfabvop (op, lc) -> - replay_qfabvop ove (subst, ops, proofs, scope) (item.ti_import, op, lc) - - | Th_circuit (cr, lc) -> - replay_circuit ove (subst, ops, proofs, scope) (item.ti_import, cr, lc) + | Th_crbinding (binding, lc) -> + replay_crbinding ove (subst, ops, proofs, scope) (item.ti_import, binding, lc) | Th_theory (ox, cth) -> begin let thmode = cth.cth_mode in