Changed syntax for bind to include path, added temp implementation of…

… OPP_8 to spec

libs/lospecs/specs/avx2.spec

@@ -6,6 +6,9 @@ AND_u256(a@256, b@256) -> @256 =
 ADD_8(a@8, b@8) -> @8 =
  add<8>(a, b)
 
+OPP_8(a@8) -> @8 =
+ add<8>(xor<8>(a, 255), 1)
+
 # Intel intrinsic: _mm256_permutexvar_epi32
 VPERMD(widx@256, w@256) -> @256 =
   map<32, 8>(
@@ -215,3 +218,5 @@ COMPRESS(w@16) -> @4 =
       1665)
   , 80635), 28)[@4|0]
 
+
+

src/ecBDep.ml

@@ -608,13 +608,13 @@ and int_of_form (env: env) (f: EcAst.form) : int =
 
 (* EXPORTED FUNCTIONS *)
 (* -------------------------------------------------------------------- *)
-let bind_circuit (env: env) (op: psymbol) (c: string) : env = 
+let bind_circuit (env: env) (op: pqsymbol) (c: string) : env = 
   let c = begin 
     try C.func_from_spec c 
     with Not_found -> Format.eprintf "Unknown circuit\n"; raise BDepError
   end in
-  let (op, t) = EcEnv.Op.lookup ([], op.pl_desc) env in
-  let fmt = EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env) in
+  let (op, t) = EcEnv.Op.lookup op.pl_desc env in
+  (* let fmt = EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env) in *)
   let rec uncurry_ty (ty: ty) : ty list = 
     match ty.ty_node with
     | Tfun (t1, t2) -> (uncurry_ty t1) @ (uncurry_ty t2)

src/ecBDep.mli

@@ -7,7 +7,7 @@ open EcTypes
 val bind_bitstring : env -> pqsymbol -> int -> env
 
 (* -------------------------------------------------------------------- *)
-val bind_circuit : env -> psymbol -> string -> env 
+val bind_circuit : env -> pqsymbol -> string -> env 
 
 (* -------------------------------------------------------------------- *)
 val bdep : env -> pgamepath -> psymbol -> int -> int-> string list -> psymbol -> unit

src/ecCommands.ml

@@ -642,7 +642,7 @@ and process_bind_bitstring (scope : EcScope.scope) (tq: pqsymbol) (w: int) =
   let env = EcBDep.bind_bitstring (EcScope.env scope) tq w 
   in EcScope.Circ.update_env env scope
 
-and process_bind_circuit (scope: EcScope.scope) (op: psymbol) (c: string) = 
+and process_bind_circuit (scope: EcScope.scope) (op: pqsymbol) (c: string) = 
   let env = EcBDep.bind_circuit (EcScope.env scope) op c in
   EcScope.Circ.update_env env scope
 

src/ecParser.mly

@@ -4044,7 +4044,7 @@ global_action:
 | BIND BITSTRING t=qident w=uint 
   { Gbindb (t, (BI.to_int w)) } (* FIXME: Check if int conversions should be here *)
 
-| BIND CIRCUIT f=oident c=STRING
+| BIND CIRCUIT f=qoident c=STRING
   { Gbindc (f, c) }
 
 | PRAGMA       x=pragma { Gpragma x }

src/ecParsetree.ml

@@ -1310,7 +1310,7 @@ type global_action =
   | GdumpWhy3    of string
   | Gbdep        of pgamepath * psymbol * int * int * (string list) * psymbol
   | Gbindb       of pqsymbol * int
-  | Gbindc       of psymbol * string
+  | Gbindc       of pqsymbol * string
 
 type global = {
   gl_action : global_action located;