From e43e4322481d1d90b74896de5cea886b1f87cca7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 1 Sep 2016 16:14:33 -0700 Subject: PHOAS syntax We also have linearization of function application / lets, constant-inlining, and reification. This closes #58. --- src/Reflection/InterpProofs.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/Reflection/InterpProofs.v (limited to 'src/Reflection/InterpProofs.v') diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v new file mode 100644 index 000000000..3565dbd40 --- /dev/null +++ b/src/Reflection/InterpProofs.v @@ -0,0 +1,29 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Util.Tactics. + +Local Open Scope ctype_scope. +Section language. + Context (base_type_code : Type). + + Local Notation flat_type := (flat_type base_type_code). + Local Notation type := (type base_type_code). + Let Tbase := @Tbase base_type_code. + Local Coercion Tbase : base_type_code >-> flat_type. + Context (interp_base_type : base_type_code -> Type). + Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). + Let interp_type := interp_type interp_base_type. + Let interp_flat_type := interp_flat_type_gen interp_base_type. + 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. + Proof. + unfold SmartVar; induction t; + repeat match goal with + | _ => reflexivity + | _ => progress simpl in * + | _ => progress rewrite_hyp * + | _ => rewrite <- surjective_pairing + end. + Qed. +End language. -- cgit v1.2.3 From f789524d8e0542d8ff9ff1357ffa2261509c7bfa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 14:31:23 -0700 Subject: More 8.4 fixes --- src/Reflection/InputSyntax.v | 4 ++-- src/Reflection/InterpProofs.v | 2 +- src/Reflection/Linearize.v | 2 +- src/Reflection/WfReflective.v | 11 ++++++----- 4 files changed, 10 insertions(+), 9 deletions(-) (limited to 'src/Reflection/InterpProofs.v') diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index fda06683a..c3c796d75 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -36,7 +36,7 @@ Section language. | MatchPair : forall {t1 t2}, exprf (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> exprf tC) -> exprf tC. Inductive expr : type -> Type := | Return {t} : exprf t -> expr t - | Abs {src dst} : (var (Tbase src) -> expr dst) -> expr (src -> dst). + | Abs {src dst} : (var (Tbase src) -> expr dst) -> expr (Arrow src dst). Global Coercion Return : exprf >-> expr. End expr. @@ -111,7 +111,7 @@ Section language. pose (e (interp_flat_type_gen interp_base_type)) as E. repeat match goal with |- context[e ?f] => change (e f) with E end. refine match E with - | Abs _ _ _ => idProp (* small inversions *) + | Abs _ _ _ => fun x : Prop => x (* small inversions *) | Return _ _ => _ end. apply compilef_correct. diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v index 3565dbd40..5790178e7 100644 --- a/src/Reflection/InterpProofs.v +++ b/src/Reflection/InterpProofs.v @@ -8,7 +8,7 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> flat_type. + Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Context (interp_base_type : base_type_code -> Type). Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). Let interp_type := interp_type interp_base_type. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v index 3e70f5ba7..b3ce3249b 100644 --- a/src/Reflection/Linearize.v +++ b/src/Reflection/Linearize.v @@ -11,7 +11,7 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> flat_type. + Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Let interp_type := interp_type interp_base_type. Let interp_flat_type := interp_flat_type_gen interp_base_type. Local Notation Expr := (@Expr base_type_code interp_base_type op). diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index 35bdf140c..34a139643 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -49,7 +49,7 @@ Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec. Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable. +Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil. Require Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *) Require Export Crypto.Util.FixCoqMistakes. @@ -83,7 +83,7 @@ Section language. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> flat_type. + Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Local Notation interp_type := (interp_type interp_base_type). Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type). Local Notation exprf := (@exprf base_type_code interp_base_type op). @@ -231,7 +231,7 @@ Section language. Definition flatten_binding_list2 t1 t2 : option (forall (x : interp_flat_type_gen var1 t1) (y : interp_flat_type_gen var2 t2), list (sigT eP)) := option_map (fun f x y => duplicate_type (f x y)) (preflatten_binding_list2 t1 t2). (** This function adds De Bruijn indices to variables *) - Fixpoint natize_interp_flat_type_gen {var t} (base : nat) (v : interp_flat_type_gen var t) {struct t} + Fixpoint natize_interp_flat_type_gen var t (base : nat) (v : interp_flat_type_gen var t) {struct t} : nat * interp_flat_type_gen (fun t : base_type_code => nat * var t)%type t := match t return interp_flat_type_gen var t -> nat * interp_flat_type_gen _ t with | Prod A B => fun v => let ret := @natize_interp_flat_type_gen _ B base (snd v) in @@ -243,6 +243,7 @@ Section language. (base, (a, b)) | Syntax.Tbase t => fun v => (S base, (base, v)) end v. + Arguments natize_interp_flat_type_gen {var t} _ _. Lemma length_natize_interp_flat_type_gen1 {t} (base : nat) (v1 : interp_flat_type_gen var1 t) (v2 : interp_flat_type_gen var2 t) : fst (natize_interp_flat_type_gen base v1) = length (flatten_binding_list base_type_code v1 v2) + base. Proof. @@ -289,7 +290,7 @@ Section language. end | Const _ _, _ => None | Var t0 x, Var t1 y - => match Nat.eqb (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with + => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y)) | _, _ => None end @@ -473,7 +474,7 @@ Section Wf. Proof. intros H var1 var2; specialize (H var1 var2). pose proof (@reflect_wf base_type_code interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 nil t t (e _) (e _)) as H'. - rewrite type_eq_semidec_transparent_refl in H' by assumption. + rewrite type_eq_semidec_transparent_refl in H' by assumption; simpl in *. edestruct reflect_wfT; simpl in *; tauto. Qed. -- cgit v1.2.3