diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-09 16:59:33 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-10 12:14:14 -0500 |
commit | 08dbb0d546d0c5f0b7e900f8167d367350d7b465 (patch) | |
tree | 0e2e647418817318ec30b732076d38e12a9b2541 /src/Reflection | |
parent | f1ac045cc7c6f0bdbc164fd33f158bc301f764a5 (diff) |
Add ApplicationRelations
Diffstat (limited to 'src/Reflection')
-rw-r--r-- | src/Reflection/ApplicationRelations.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Reflection/ApplicationRelations.v b/src/Reflection/ApplicationRelations.v new file mode 100644 index 000000000..9a1daa97e --- /dev/null +++ b/src/Reflection/ApplicationRelations.v @@ -0,0 +1,28 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. + +Section language. + Context {base_type1 base_type2 : Type} + {interp_base_type1 : base_type1 -> Type} + {interp_base_type2 : base_type2 -> Type} + {op1 : flat_type base_type1 -> flat_type base_type1 -> Type} + {op2 : flat_type base_type2 -> flat_type base_type2 -> Type} + {interp_op1 : forall src dst, op1 src dst -> interp_flat_type interp_base_type1 src -> interp_flat_type interp_base_type1 dst} + {interp_op2 : forall src dst, op2 src dst -> interp_flat_type interp_base_type2 src -> interp_flat_type interp_base_type2 dst} + (R : forall t1 t2, interp_base_type1 t1 -> interp_base_type2 t2 -> Prop). + + Fixpoint rel_interp_all_binders_for' {t1 : type base_type1} {t2 : type base_type2} + : interp_all_binders_for' t1 interp_base_type1 -> interp_all_binders_for' t2 interp_base_type2 -> Prop + := match t1, t2 return interp_all_binders_for' t1 _ -> interp_all_binders_for' t2 _ -> Prop with + | Tflat T1, Tflat T2 => fun _ _ => True + | Arrow A1 B1, Arrow A2 B2 + => fun x y => R _ _ (fst x) (fst y) /\ @rel_interp_all_binders_for' _ _ (snd x) (snd y) + | Tflat _, _ + | Arrow _ _, _ + => fun _ _ => False + end. + Definition rel_interp_all_binders_for {t1 : type base_type1} {t2 : type base_type2} + (x : interp_all_binders_for t1 interp_base_type1) (y : interp_all_binders_for t2 interp_base_type2) + : Prop + := rel_interp_all_binders_for' (interp_all_binders_for_to' x) (interp_all_binders_for_to' y). +End language. |