refactoring

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 

src/ecCircuits.mli

@@ -6,7 +6,7 @@ open EcEnv
 
 (* -------------------------------------------------------------------- *)
 module Map = Batteries.Map
-
+  
 (* -------------------------------------------------------------------- *)
 val blocks : 'a list -> int -> 'a list list
 

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

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

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