From a7151cd08be445f8a2addb682de8c8f5e03ec4e2 Mon Sep 17 00:00:00 2001
From: Gustavo Delerue <up201804883@fc.up.pt>
Date: Wed, 24 Apr 2024 18:23:20 +0100
Subject: [PATCH] Changed syntax for bind to include path, added temp
 implementation of OPP_8 to spec

---
 libs/lospecs/specs/avx2.spec | 5 +++++
 src/ecBDep.ml                | 6 +++---
 src/ecBDep.mli               | 2 +-
 src/ecCommands.ml            | 2 +-
 src/ecParser.mly             | 2 +-
 src/ecParsetree.ml           | 2 +-
 6 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/libs/lospecs/specs/avx2.spec b/libs/lospecs/specs/avx2.spec
index c4df2ecb4..1e4e23787 100644
--- a/libs/lospecs/specs/avx2.spec
+++ b/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]
 
+
+
diff --git a/src/ecBDep.ml b/src/ecBDep.ml
index 4f9eb5ae0..a866ca226 100644
--- a/src/ecBDep.ml
+++ b/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)
diff --git a/src/ecBDep.mli b/src/ecBDep.mli
index 7d7340cde..2f9877edf 100644
--- a/src/ecBDep.mli
+++ b/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
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index b39159036..99a3b50cd 100644
--- a/src/ecCommands.ml
+++ b/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
 
diff --git a/src/ecParser.mly b/src/ecParser.mly
index b9129beb2..cd3fe0c61 100644
--- a/src/ecParser.mly
+++ b/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 }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 208e5f9cd..f4e5b71a1 100644
--- a/src/ecParsetree.ml
+++ b/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;