Add Named.InterpSideConditions

1 files changed, 52 insertions, 0 deletions

diff --git a/src/Compilers/Named/InterpSideConditions.v b/src/Compilers/Named/InterpSideConditions.v
new file mode 100644
index 000000000..a2f965435
--- /dev/null
+++ b/src/Compilers/Named/InterpSideConditions.v
@@ -0,0 +1,52 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
+Require Import Crypto.Util.PointedProp.
+Require Import Crypto.Util.Notations.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {Name : Type}
+          {interp_base_type : base_type_code -> Type}
+          {Context : Context Name interp_base_type}
+          (interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d)
+          (interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop).
+
+  Local Notation exprf := (@exprf base_type_code op Name).
+  Local Notation expr := (@expr base_type_code op Name).
+
+  Fixpoint interpf_side_conditions_gen {t} (ctx : Context) (e : exprf t)
+    : option (pointed_Prop * interp_flat_type interp_base_type t)
+    := match e with
+       | TT => Some (trivial, tt)
+       | Var t' x => option_map (fun v => (trivial, v)) (lookupb t' ctx x)
+       | Op t1 tR opc args
+         => match @interpf_side_conditions_gen _ ctx args with
+            | Some (args_cond, argsv)
+              => Some (args_cond /\ interped_op_side_conditions _ _ opc argsv, interp_op _ _ opc argsv)
+            | None => None
+            end
+       | LetIn _ n ex _ eC
+         => match @interpf_side_conditions_gen _ ctx ex with
+            | Some (x_cond, x)
+              => match @interpf_side_conditions_gen _ (extend ctx n x) eC with
+                 | Some (c_cond, cv)
+                   => Some (x_cond /\ c_cond, cv)
+                 | None => None
+                 end
+            | None => None
+            end
+       | Pair _ ex _ ey
+         => match @interpf_side_conditions_gen _ ctx ex, @interpf_side_conditions_gen _ ctx ey with
+            | Some (x_cond, xv), Some (y_cond, yv) => Some (x_cond /\ y_cond, (xv, yv))
+            | None, _ | _, None => None
+            end
+       end%pointed_prop.
+  Definition interpf_side_conditions {t} ctx e : option pointed_Prop
+    := option_map (@fst _ _) (@interpf_side_conditions_gen t ctx e).
+  Definition interp_side_conditions {t} ctx (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop
+    := fun x => interpf_side_conditions (extend ctx (Abs_name e) x) (invert_Abs e).
+  Definition InterpSideConditions {t} (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop
+    := interp_side_conditions empty e.
+End language.