diff options
author | Jason Gross <jagro@google.com> | 2016-09-05 20:46:07 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-09-05 20:46:07 -0700 |
commit | a476968e7cc5b38e9de14837eae23c81ff4b88d7 (patch) | |
tree | 1764a31b8fc4235572b847a38c7a4577299ebad7 /src | |
parent | c7e14293503029ad8df45f495947d5b5e3c91a8a (diff) |
Better implicits for interpf, pointwise-lifting of rels over interp_type_gen
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/InputSyntax.v | 2 | ||||
-rw-r--r-- | src/Reflection/InterpProofs.v | 2 | ||||
-rw-r--r-- | src/Reflection/Syntax.v | 9 |
3 files changed, 11 insertions, 2 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 98faeaa44..4a5dc810b 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -90,7 +90,7 @@ Section language. Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). Lemma compilef_correct {t} (e : @exprf interp_flat_type t) - : Syntax.interpf base_type_code interp_base_type op interp_op (compilef e) = interpf interp_op e. + : Syntax.interpf interp_op (compilef e) = interpf interp_op e. Proof. induction e; repeat match goal with diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index 5790178e7..2d4ad5e0f 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -16,7 +16,7 @@ Section language. Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). Lemma interpf_SmartVar t v - : Syntax.interpf base_type_code interp_base_type op interp_op (SmartVar (t:=t) v) = v. + : Syntax.interpf interp_op (SmartVar (t:=t) v) = v. Proof. unfold SmartVar; induction t; repeat match goal with diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index cc816f58f..6d632342b 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -34,6 +34,15 @@ Section language. | Tflat t => interp_flat_type t | Arrow x y => (interp_flat_type x -> interp_type_gen y)%type end. + Section rel. + Context (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop). + Fixpoint interp_type_gen_rel_pointwise (t : type) + : interp_type_gen t -> interp_type_gen t -> Prop := + match t with + | Tflat t => R t + | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x) + end. + End rel. End type. Section flat_type. Context (interp_base_type : base_type_code -> Type). |