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/InputSyntax.v | 130 ++++++++++++++++++++++ src/Reflection/InterpProofs.v | 29 +++++ src/Reflection/Linearize.v | 101 +++++++++++++++++ src/Reflection/ReifyDirect.v | 212 +++++++++++++++++++++++++++++++++++ src/Reflection/ReifyExact.v | 249 ++++++++++++++++++++++++++++++++++++++++++ src/Reflection/Syntax.v | 198 +++++++++++++++++++++++++++++++++ src/Reflection/TestCase.v | 114 +++++++++++++++++++ 7 files changed, 1033 insertions(+) create mode 100644 src/Reflection/InputSyntax.v create mode 100644 src/Reflection/InterpProofs.v create mode 100644 src/Reflection/Linearize.v create mode 100644 src/Reflection/ReifyDirect.v create mode 100644 src/Reflection/ReifyExact.v create mode 100644 src/Reflection/Syntax.v create mode 100644 src/Reflection/TestCase.v (limited to 'src') diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v new file mode 100644 index 000000000..fda06683a --- /dev/null +++ b/src/Reflection/InputSyntax.v @@ -0,0 +1,130 @@ +(** * PHOAS Representation of Gallina which allows exact denotation *) +Require Import Coq.Strings.String. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.InterpProofs. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +(** We parameterize the language over a type of basic type codes (for + things like [Z], [word], [bool]), as well as a type of n-ary + operations returning one value, and n-ary operations returning two + values. *) +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). + Local Notation Tbase := (@Tbase base_type_code). + + Section expr_param. + Context (interp_base_type : base_type_code -> Type). + Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). + Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type). + Section expr. + Context {var : flat_type -> Type}. + + (** N.B. [Let] destructures pairs *) + Inductive exprf : flat_type -> Type := + | Const {t : flat_type} : interp_type t -> exprf t + | Var {t} : var t -> exprf t + | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR + | Let : forall {tx}, exprf tx -> forall {tC}, (var tx -> exprf tC) -> exprf tC + | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2) + | 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). + Global Coercion Return : exprf >-> expr. + End expr. + + Definition Expr (t : type) := forall var, @expr var t. + + Section interp. + Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). + + Fixpoint interpf {t} (e : @exprf interp_flat_type t) : interp_flat_type t + := match e in exprf t return interp_flat_type t with + | Const _ x => x + | Var _ x => x + | Op _ _ op args => @interp_op _ _ op (@interpf _ args) + | Let _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) + | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) + | MatchPair _ _ ex _ eC => match @interpf _ ex with pair x y => @interpf _ (eC x y) end + end. + Fixpoint interp {t} (e : @expr interp_type t) : interp_type t + := match e in expr t return interp_type t with + | Return _ x => interpf x + | Abs _ _ f => fun x => @interp _ (f x) + end. + + Definition Interp {t} (E : Expr t) : interp_type t := interp (E _). + End interp. + + Section compile. + Context {var : base_type_code -> Type}. + + Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code interp_base_type op var t + := match e in exprf t return @Syntax.exprf _ _ _ _ t with + | Const _ x => Syntax.Const x + | Var _ x => Syntax.SmartVar x + | Op _ _ op args => Syntax.Op op (@compilef _ args) + | Let _ ex _ eC => Syntax.Let (@compilef _ ex) (fun x => @compilef _ (eC x)) + | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey) + | MatchPair _ _ ex _ eC => Syntax.Let (@compilef _ ex) (fun xy => @compilef _ (eC (fst xy) (snd xy))) + end. + + Fixpoint compile {t} (e : @expr (interp_flat_type_gen var) t) : @Syntax.expr base_type_code interp_base_type op var t + := match e in expr t return @Syntax.expr _ _ _ _ t with + | Return _ x => Syntax.Return (compilef x) + | Abs a _ f => Syntax.Abs (fun x : var a => @compile _ (f x)) + end. + End compile. + + Definition Compile {t} (e : Expr t) : Syntax.Expr base_type_code interp_base_type op t + := fun var => compile (e _). + + Section compile_correct. + 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. + Proof. + induction e; + repeat match goal with + | _ => reflexivity + | _ => progress simpl in * + | _ => rewrite interpf_SmartVar + | _ => rewrite <- surjective_pairing + | _ => progress rewrite_hyp * + | [ |- context[let (x, y) := ?v in _] ] + => rewrite (surjective_pairing v); cbv beta iota + end. + Qed. + + Lemma Compile_correct {t : flat_type} (e : @Expr t) + : Syntax.Interp base_type_code interp_base_type op interp_op (Compile e) = Interp interp_op e. + Proof. + unfold Interp, Compile, Syntax.Interp; simpl. + 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 *) + | Return _ _ => _ + end. + apply compilef_correct. + Qed. + End compile_correct. + End expr_param. +End language. + +Global Arguments Const {_ _ _ _ _} _. +Global Arguments Var {_ _ _ _ _} _. +Global Arguments Op {_ _ _ _ _ _} _ _. +Global Arguments Let {_ _ _ _ _} _ {_} _. +Global Arguments MatchPair {_ _ _ _ _ _} _ {_} _. +Global Arguments Pair {_ _ _ _ _} _ {_} _. +Global Arguments Return {_ _ _ _ _} _. +Global Arguments Abs {_ _ _ _ _ _} _. 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. diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v new file mode 100644 index 000000000..3e70f5ba7 --- /dev/null +++ b/src/Reflection/Linearize.v @@ -0,0 +1,101 @@ +(** * Linearize: Place all and only operations in let binders *) +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Util.Tactics. + +Local Open Scope ctype_scope. +Section language. + Context (base_type_code : Type). + Context (interp_base_type : base_type_code -> Type). + Context (op : flat_type base_type_code -> flat_type 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. + 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). + + Section with_var. + Context {var : base_type_code -> Type}. + Local Notation exprf := (@exprf base_type_code interp_base_type op var). + Local Notation expr := (@expr base_type_code interp_base_type op var). + + Section under_lets. + Fixpoint let_bind_const {t} (e : interp_flat_type t) {struct t} + : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC + := match t return forall (e : interp_flat_type t) {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with + | Prod A B => fun e _ C => @let_bind_const A (fst e) _ (fun x => + @let_bind_const B (snd e) _ (fun y => + C (x, y))) + | Syntax.Tbase _ => fun e _ C => Let (Const e) C + end e. + + Fixpoint under_letsf {t} (e : exprf t) + : forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC + := match e in Syntax.exprf _ _ _ t return forall {tC} (C : interp_flat_type_gen var t -> exprf tC), exprf tC with + | Let _ ex _ eC + => fun _ C => @under_letsf _ ex _ (fun v => @under_letsf _ (eC v) _ C) + | Const _ x => fun _ C => let_bind_const x C + | Var _ x => fun _ C => C x + | Op _ _ op args as e => fun _ C => Let e C + | Pair A x B y => fun _ C => @under_letsf A x _ (fun x => + @under_letsf B y _ (fun y => + C (x, y))) + end. + End under_lets. + + Fixpoint linearizef {t} (e : exprf t) : exprf t + := match e in Syntax.exprf _ _ _ t return exprf t with + | Let _ ex _ eC + => under_letsf (@linearizef _ ex) (fun x => @linearizef _ (eC x)) + | Const _ x => Const x + | Var _ x => Var x + | Op _ _ op args + => under_letsf (@linearizef _ args) (fun args => Let (Op op (SmartVar args)) SmartVar) + | Pair A ex B ey + => under_letsf (@linearizef _ ex) (fun x => + under_letsf (@linearizef _ ey) (fun y => + SmartVar (t:=Prod A B) (x, y))) + end. + + Fixpoint linearize {t} (e : expr t) : expr t + := match e in Syntax.expr _ _ _ t return expr t with + | Return _ x => linearizef x + | Abs _ _ f => Abs (fun x => @linearize _ (f x)) + end. + End with_var. + + Section inline. + Context {var : base_type_code -> Type}. + Local Notation exprf := (@exprf base_type_code interp_base_type op). + Local Notation expr := (@expr base_type_code interp_base_type op). + + Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t + := match e in Syntax.exprf _ _ _ t return @exprf var t with + | Let _ ex tC eC + => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with + | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x) + | ex => fun eC => Let ex (fun x => eC (SmartVarVar x)) + end (fun x => @inline_constf _ (eC x)) + | Var _ x => x + | Const _ x => Const x + | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey) + | Op _ _ op args => Op op (@inline_constf _ args) + end. + + Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t + := match e in Syntax.expr _ _ _ t return @expr var t with + | Return _ x => Return (inline_constf x) + | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x))) + end. + End inline. + + Definition Linearize {t} (e : Expr t) : Expr t + := fun var => linearize (e _). + Definition InlineConst {t} (e : Expr t) : Expr t + := fun var => inline_const (e _). +End language. + +Arguments Linearize {_ _ _ _} _ var. +Arguments InlineConst {_ _ _ _} _ var. diff --git a/src/Reflection/ReifyDirect.v b/src/Reflection/ReifyDirect.v new file mode 100644 index 000000000..41eb86a1f --- /dev/null +++ b/src/Reflection/ReifyDirect.v @@ -0,0 +1,212 @@ +(** * Direct reification of PHOAS Representation of Gallina *) +(** The reification procedure introduces extra [let]s and [match]es, + so we don't get something syntactically equal. Without primitive + projections, we don't get something judgmentally equal. *) +Require Import Coq.Strings.String. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. +Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. +Arguments reify_var_for_in_is _ {T} _ _ {eT} _. + +(** [reify] assumes that operations can be reified via the [reify_op] + typeclass, which gets passed the type family of operations, the + expression which is headed by an operation, and expects resolution + to fill in a number of arguments (which [reifyf] will + automatically curry), as well as the reified operator. + + We also assume that types can be reified via the [reify] typeclass + with arguments [reify type ]. *) +Class reify_op {opTF} (op_family : opTF) {opExprT} (opExpr : opExprT) (nargs : nat) {opT} (reified_op : opT) + := Build_reify_op : True. +Ltac strip_type_cast term := lazymatch term with ?term' => term' end. +Ltac reify_type T := + lazymatch T with + | (?A -> ?B)%type + => let a := reify_type A in + let b := reify_type B in + constr:(@Arrow _ a b) + | prod ?A ?B + => let a := reify_type A in + let b := reify_type B in + constr:(@Prod _ a b) + | _ + => let v := strip_type_cast (_ : reify type T) in + constr:(Tbase v) + end. +Ltac reify_base_type T := + let t := reify_type T in + lazymatch t with + | Tbase ?t => t + | ?t => t + end. + +Ltac reifyf_var x mkVar := + lazymatch goal with + | _ : reify_var_for_in_is _ x ?t ?v |- _ => mkVar t v + | _ => lazymatch x with + | fst ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with + | Prod ?A ?B => mkVar A (fst v) + end) + | snd ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with + | Prod ?A ?B => mkVar B (snd v) + end) + end + end. + +Inductive reify_result_helper := +| finished_value {T} (res : T) +| op_info {T} (res : T) +| reification_unsuccessful. + +(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get + more debugging. *) +Ltac reify_debug_level := constr:(0). +Module Import ReifyDebugNotations. + Open Scope string_scope. +End ReifyDebugNotations. + +Ltac debug_enter_reifyf e := + let lvl := reify_debug_level in + match lvl with + | S (S _) => cidtac2 "reifyf: Attempting to reify:" e + | _ => constr:(Set) + end. + +Ltac debug_enter_reify_rec := + let lvl := reify_debug_level in + match lvl with + | S _ => idtac_goal + | _ => idtac + end. +Ltac debug_leave_reify_rec e := + let lvl := reify_debug_level in + match lvl with + | S _ => idtac "reifyf success:" e "" + | _ => idtac + end. + +Ltac reifyf base_type_code interp_base_type op var e := + let reify_rec e := reifyf base_type_code interp_base_type op var e in + let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in + let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in + let mkVar T ex := constr:(SmartVar (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in + let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in + let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in + let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in + let dummy := debug_enter_reifyf e in + lazymatch e with + | let x := ?ex in @?eC x => + let ex := reify_rec ex in + let eC := reify_rec eC in + mkLet ex eC + | pair ?a ?b => + let a := reify_rec a in + let b := reify_rec b in + mkPair a b + | (fun x : ?T => ?C) => + let t := reify_type T in + (* Work around Coq 8.5 and 8.6 bug *) + (* *) + (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) + (* even if its Gallina name matches a Ltac in this tactic. *) + let maybe_x := fresh x in + let not_x := fresh x in + lazymatch constr:(fun (x : T) (not_x : interp_flat_type_gen var t) (_ : reify_var_for_in_is base_type_code x t not_x) => + (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) + with fun _ v _ => @?C v => C end + | match ?ev with pair a b => @?eC a b end => + let v := reify_rec ev in + let C := reify_rec eC in + let C := lazymatch C + with (fun (a : ?A) (b : ?B) => ?C) => constr:(fun ab : prod A B => match fst ab, snd ab with a, b => C end) end in + mkLet v C + | ?x => + let t := lazymatch type of x with ?t => reify_type t end in + let retv := match constr:(Set) with + | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv) + | _ => let r := constr:(_ : reify_op op x _ _) in + let t := type of r in + constr:(op_info t) + | _ => let c := mkConst t x in + constr:(finished_value c) + | _ => constr:(reification_unsuccessful) + end in + lazymatch retv with + | finished_value ?v => v + | op_info (reify_op _ _ ?nargs ?op_code) + => let tR := (let tR := type of x in reify_type tR) in + lazymatch nargs with + | 1%nat + => lazymatch x with + | ?f ?x0 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + mkOp a0T tR op_code a0 + end + | 2%nat + => lazymatch x with + | ?f ?x0 ?x1 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + let a1T := (let t := type of x1 in reify_type t) in + let a1 := reify_rec x1 in + let args := mkPair a0 a1 in + mkOp (@Prod _ a0T a1T) tR op_code args + end + | 3%nat + => lazymatch x with + | ?f ?x0 ?x1 ?x2 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + let a1T := (let t := type of x1 in reify_type t) in + let a1 := reify_rec x1 in + let a2T := (let t := type of x2 in reify_type t) in + let a2 := reify_rec x2 in + let args := let a01 := mkPair a0 a1 in mkPair a01 a2 in + mkOp (@Prod _ (@Prod _ a0T a1T) a2T) tR op_code args + end + | _ => cfail2 "Unsupported number of operation arguments in reifyf:"%string nargs + end + | reification_unsuccessful + => cfail2 "Failed to reify:"%string x + end + end. + +Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. + +(** For reification including [Abs] *) +Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T. +Ltac reify_abs base_type_code interp_base_type op var e := + let reify_rec e := reify_abs base_type_code interp_base_type op var e in + let reifyf_term e := reifyf base_type_code interp_base_type op var e in + let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in + let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in + let dummy := debug_enter_reifyf e in + lazymatch e with + | (fun x : ?T => ?C) => + let t := reify_base_type T in + (* Work around Coq 8.5 and 8.6 bug *) + (* *) + (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) + (* even if its Gallina name matches a Ltac in this tactic. *) + let maybe_x := fresh x in + let not_x := fresh x in + lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) => + (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) + with fun _ v _ => @?C v => mkAbs t C end + | ?x => + reifyf_term x + end. + +Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. + +Ltac Reify base_type_code interp_base_type op e := + lazymatch constr:(fun (var : base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with + (fun var => ?C) => constr:(fun (var : base_type_code -> Type) => C) (* copy the term but not the type cast *) + end. diff --git a/src/Reflection/ReifyExact.v b/src/Reflection/ReifyExact.v new file mode 100644 index 000000000..1eac17675 --- /dev/null +++ b/src/Reflection/ReifyExact.v @@ -0,0 +1,249 @@ +(** * Exact reification of PHOAS Representation of Gallina *) +(** The reification procedure goes through [InputSyntax], which allows + judgmental equality of the denotation of the reified term. *) +Require Import Coq.Strings.String. +Require Import Crypto.Reflection.Syntax. +Require Export Crypto.Reflection.InputSyntax. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. +Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. +Arguments reify_var_for_in_is _ {T} _ _ {eT} _. + +(** [reify] assumes that operations can be reified via the [reify_op] + typeclass, which gets passed the type family of operations, the + expression which is headed by an operation, and expects resolution + to fill in a number of arguments (which [reifyf] will + automatically curry), as well as the reified operator. + + We also assume that types can be reified via the [reify] typeclass + with arguments [reify type ]. *) +Class reify_op {opTF} (op_family : opTF) {opExprT} (opExpr : opExprT) (nargs : nat) {opT} (reified_op : opT) + := Build_reify_op : True. +Ltac strip_type_cast term := lazymatch term with ?term' => term' end. +Ltac reify_type T := + lazymatch T with + | (?A -> ?B)%type + => let a := reify_type A in + let b := reify_type B in + constr:(@Arrow _ a b) + | prod ?A ?B + => let a := reify_type A in + let b := reify_type B in + constr:(@Prod _ a b) + | _ + => let v := strip_type_cast (_ : reify type T) in + constr:(Tbase v) + end. +Ltac reify_base_type T := + let t := reify_type T in + lazymatch t with + | Tbase ?t => t + | ?t => t + end. + +Ltac reifyf_var x mkVar := + lazymatch goal with + | _ : reify_var_for_in_is _ x ?t ?v |- _ => mkVar t v + | _ => lazymatch x with + | fst ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with + | Prod ?A ?B => mkVar A (fst v) + end) + | snd ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with + | Prod ?A ?B => mkVar B (snd v) + end) + end + end. + +Inductive reify_result_helper := +| finished_value {T} (res : T) +| op_info {T} (res : T) +| reification_unsuccessful. + +(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get + more debugging. *) +Ltac reify_debug_level := constr:(0). +Module Import ReifyDebugNotations. + Open Scope string_scope. +End ReifyDebugNotations. + +Ltac debug_enter_reifyf e := + let lvl := reify_debug_level in + match lvl with + | S (S _) => cidtac2 "reifyf: Attempting to reify:" e + | _ => constr:(Set) + end. +Ltac debug_enter_reify_abs e := + let lvl := reify_debug_level in + match lvl with + | S (S _) => cidtac2 "reify_abs: Attempting to reify:" e + | _ => constr:(Set) + end. + +Ltac debug_enter_reify_rec := + let lvl := reify_debug_level in + match lvl with + | S _ => idtac_goal + | _ => idtac + end. +Ltac debug_leave_reify_rec e := + let lvl := reify_debug_level in + match lvl with + | S _ => idtac "reifyf success:" e "" + | _ => idtac + end. + +Ltac reifyf base_type_code interp_base_type op var e := + let reify_rec e := reifyf base_type_code interp_base_type op var e in + let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in + let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in + let mkVar T ex := constr:(Var (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in + let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in + let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in + let mkMatchPair tC ex eC := constr:(MatchPair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (tC:=tC) ex eC) in + let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in + let dummy := debug_enter_reifyf e in + lazymatch e with + | let x := ?ex in @?eC x => + let ex := reify_rec ex in + let eC := reify_rec eC in + mkLet ex eC + | pair ?a ?b => + let a := reify_rec a in + let b := reify_rec b in + mkPair a b + | (fun x : ?T => ?C) => + let t := reify_type T in + (* Work around Coq 8.5 and 8.6 bug *) + (* *) + (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) + (* even if its Gallina name matches a Ltac in this tactic. *) + let maybe_x := fresh x in + let not_x := fresh x in + lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) => + (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) + with fun _ v _ => @?C v => C end + | match ?ev with pair a b => @?eC a b end => + let t := (let T := match type of eC with _ -> _ -> ?T => T end in reify_type T) in + let v := reify_rec ev in + let C := reify_rec eC in + mkMatchPair t v C + | ?x => + let t := lazymatch type of x with ?t => reify_type t end in + let retv := match constr:(Set) with + | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv) + | _ => let r := constr:(_ : reify_op op x _ _) in + let t := type of r in + constr:(op_info t) + | _ => let c := mkConst t x in + constr:(finished_value c) + | _ => constr:(reification_unsuccessful) + end in + lazymatch retv with + | finished_value ?v => v + | op_info (reify_op _ _ ?nargs ?op_code) + => let tR := (let tR := type of x in reify_type tR) in + lazymatch nargs with + | 1%nat + => lazymatch x with + | ?f ?x0 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + mkOp a0T tR op_code a0 + end + | 2%nat + => lazymatch x with + | ?f ?x0 ?x1 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + let a1T := (let t := type of x1 in reify_type t) in + let a1 := reify_rec x1 in + let args := mkPair a0 a1 in + mkOp (@Prod _ a0T a1T) tR op_code args + end + | 3%nat + => lazymatch x with + | ?f ?x0 ?x1 ?x2 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + let a1T := (let t := type of x1 in reify_type t) in + let a1 := reify_rec x1 in + let a2T := (let t := type of x2 in reify_type t) in + let a2 := reify_rec x2 in + let args := let a01 := mkPair a0 a1 in mkPair a01 a2 in + mkOp (@Prod _ (@Prod _ a0T a1T) a2T) tR op_code args + end + | _ => cfail2 "Unsupported number of operation arguments in reifyf:"%string nargs + end + | reification_unsuccessful + => cfail2 "Failed to reify:"%string x + end + end. + +Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. + +(** For reification including [Abs] *) +Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T. +Ltac reify_abs base_type_code interp_base_type op var e := + let reify_rec e := reify_abs base_type_code interp_base_type op var e in + let reifyf_term e := reifyf base_type_code interp_base_type op var e in + let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in + let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in + let dummy := debug_enter_reify_abs e in + lazymatch e with + | (fun x : ?T => ?C) => + let t := reify_base_type T in + (* Work around Coq 8.5 and 8.6 bug *) + (* *) + (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) + (* even if its Gallina name matches a Ltac in this tactic. *) + let maybe_x := fresh x in + let not_x := fresh x in + lazymatch constr:(fun (x : T) (not_x : var (Tbase t)) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) => + (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) + with fun _ v _ => @?C v => mkAbs t C end + | ?x => + reifyf_term x + end. + +Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. + +Ltac Reify' base_type_code interp_base_type op e := + lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with + (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *) + end. +Ltac Reify base_type_code interp_base_type op e := + let r := Reify' base_type_code interp_base_type op e in + constr:(InputSyntax.Compile base_type_code interp_base_type op r). + +Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. +Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. + +Ltac Reify_rhs base_type_code interp_base_type op interp_op := + let rhs := rhs_of_goal in + let RHS := Reify base_type_code interp_base_type op rhs in + transitivity (Syntax.Interp base_type_code interp_base_type op interp_op RHS); + [ + | etransitivity; (* first we strip off the [InputSyntax.Compile] + bit; Coq is bad at inferring the type, so we + help it out by providing it *) + [ lazymatch goal with + | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] + => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e) + end + | ((* now we unfold the interpretation function, including the + parameterized bits; we assume that [hnf] is enough to unfold + the interpretation functions that we're parameterized + over. *) + lazymatch goal with + | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ] + => let interp_base_type' := (eval hnf in interp_base_type) in + let interp_op' := (eval hnf in interp_op) in + change interp_base_type with interp_base_type'; + change interp_op with interp_op' + end; + cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type_gen interp interpf]; simplify_projections; reflexivity) ] ]. diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v new file mode 100644 index 000000000..a60f0d76f --- /dev/null +++ b/src/Reflection/Syntax.v @@ -0,0 +1,198 @@ +(** * PHOAS Representation of Gallina *) +Require Import Coq.Strings.String. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +(** We parameterize the language over a type of basic type codes (for + things like [Z], [word], [bool]), as well as a type of n-ary + operations returning one value, and n-ary operations returning two + values. *) +Delimit Scope ctype_scope with ctype. +Local Open Scope ctype_scope. +Delimit Scope expr_scope with expr. +Local Open Scope expr_scope. +Section language. + Context (base_type_code : Type). + + Inductive flat_type := Tbase (_ : base_type_code) | Prod (x y : flat_type). + Bind Scope ctype_scope with flat_type. + + Inductive type := Tflat (_ : flat_type) | Arrow (x : base_type_code) (y : type). + Bind Scope ctype_scope with type. + + Global Coercion Tflat : flat_type >-> type. + Infix "*" := Prod : ctype_scope. + Notation "A -> B" := (Arrow A B) : ctype_scope. + Local Coercion Tbase : base_type_code >-> flat_type. + + Section interp. + Section type. + Context (interp_flat_type : flat_type -> Type). + Fixpoint interp_type_gen (t : type) := + match t with + | Tflat t => interp_flat_type t + | Arrow x y => (interp_flat_type x -> interp_type_gen y)%type + end. + End type. + Section flat_type. + Context (interp_base_type : base_type_code -> Type). + Fixpoint interp_flat_type_gen (t : flat_type) := + match t with + | Tbase t => interp_base_type t + | Prod x y => prod (interp_flat_type_gen x) (interp_flat_type_gen y) + end. + Definition interp_type := interp_type_gen interp_flat_type_gen. + End flat_type. + End interp. + + Section expr_param. + Context (interp_base_type : base_type_code -> Type). + Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type). + Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type). + Section expr. + Context {var : base_type_code -> Type}. + + (** N.B. [Let] destructures pairs *) + Inductive exprf : flat_type -> Type := + | Const {t : flat_type} : interp_type t -> exprf t + | Var {t} : var t -> exprf t + | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR + | Let : forall {tx}, exprf tx -> forall {tC}, (interp_flat_type_gen var tx -> exprf tC) -> exprf tC + | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2). + Bind Scope expr_scope with exprf. + Inductive expr : type -> Type := + | Return {t} : exprf t -> expr t + | Abs {src dst} : (var src -> expr dst) -> expr (src -> dst). + Bind Scope expr_scope with expr. + Global Coercion Return : exprf >-> expr. + Fixpoint smart_interp_flat_map {f g} + (h : forall x, f x -> g (Tbase x)) + (pair : forall A B, g A -> g B -> g (Prod A B)) + {t} + : interp_flat_type_gen f t -> g t + := match t return interp_flat_type_gen f t -> g t with + | Tbase _ => h _ + | Prod A B => fun v => pair _ _ + (@smart_interp_flat_map f g h pair A (fst v)) + (@smart_interp_flat_map f g h pair B (snd v)) + end. + (** [SmartVar] is like [Var], except that it inserts + pair-projections and [Pair] as necessary to handle + [flat_type], and not just [base_type_code] *) + Definition SmartVar {t} : interp_flat_type_gen var t -> exprf t + := @smart_interp_flat_map var exprf (fun t => Var) (fun A B x y => Pair x y) t. + Definition SmartVarVar {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t + := @smart_interp_flat_map var (interp_flat_type_gen exprf) (fun t => Var) (fun A B x y => pair x y) t. + Definition SmartConst {t} : interp_flat_type t -> interp_flat_type_gen exprf t + := @smart_interp_flat_map _ (interp_flat_type_gen exprf) (fun t => Const) (fun A B x y => pair x y) t. + End expr. + + Definition Expr (t : type) := forall var, @expr var t. + + Section interp. + Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). + + Fixpoint interpf {t} (e : @exprf interp_flat_type t) : interp_flat_type t + := match e in exprf t return interp_flat_type t with + | Const _ x => x + | Var _ x => x + | Op _ _ op args => @interp_op _ _ op (@interpf _ args) + | Let _ ex _ eC => let x := @interpf _ ex in @interpf _ (eC x) + | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) + end. + Fixpoint interp {t} (e : @expr interp_type t) : interp_type t + := match e in expr t return interp_type t with + | Return _ x => interpf x + | Abs _ _ f => fun x => @interp _ (f x) + end. + + Definition Interp {t} (E : Expr t) : interp_type t := interp (E _). + End interp. + + Section map. + Context {var1 var2 : base_type_code -> Type}. + Context (fvar12 : forall t, var1 t -> var2 t) + (fvar21 : forall t, var2 t -> var1 t). + + Fixpoint mapf_interp_flat_type_gen {t} (e : interp_flat_type_gen var2 t) {struct t} + : interp_flat_type_gen var1 t + := match t return interp_flat_type_gen _ t -> interp_flat_type_gen _ t with + | Tbase _ => fvar21 _ + | Prod x y => fun xy => (@mapf_interp_flat_type_gen _ (fst xy), + @mapf_interp_flat_type_gen _ (snd xy)) + end e. + + Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t + := match e in exprf t return exprf t with + | Const _ x => Const x + | Var _ x => Var (fvar12 _ x) + | Op _ _ op args => Op op (@mapf _ args) + | Let _ ex _ eC => Let (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type_gen x))) + | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey) + end. + End map. + + Section wf. + Context {var1 var2 : base_type_code -> Type}. + + Local Notation eP := (fun t => var1 t * var2 t)%type (only parsing). + Local Notation "x == y" := (existT eP _ (x, y)). + Fixpoint flatten_binding_list {t} (x : interp_flat_type_gen var1 t) (y : interp_flat_type_gen var2 t) : list (sigT eP) + := (match t return interp_flat_type_gen var1 t -> interp_flat_type_gen var2 t -> list _ with + | Tbase _ => fun x y => (x == y) :: nil + | Prod t0 t1 => fun x y => @flatten_binding_list _ (fst x) (fst y) ++ @flatten_binding_list _ (snd x) (snd y) + end x y)%list. + + Inductive wff : list (sigT eP) -> forall {t}, @exprf var1 t -> @exprf var2 t -> Prop := + | WfConst : forall t G n, @wff G t (Const n) (Const n) + | WfVar : forall G (t : base_type_code) x x', List.In (x == x') G -> @wff G t (Var x) (Var x') + | WfOp : forall G {t} {tR} (e : @exprf var1 t) (e' : @exprf var2 t) op, + wff G e e' + -> wff G (Op (tR := tR) op e) (Op (tR := tR) op e') + | WfLet : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> @exprf var1 t2) e2', + wff G e1 e1' + -> (forall x1 x2, wff (flatten_binding_list x1 x2 ++ G) (e2 x1) (e2' x2)) + -> wff G (Let e1 e2) (Let e1' e2') + | WfPair : forall G {t1} {t2} (e1: @exprf var1 t1) (e2: @exprf var1 t2) + (e1': @exprf var2 t1) (e2': @exprf var2 t2), + wff G e1 e1' + -> wff G e2 e2' + -> wff G (Pair e1 e2) (Pair e1' e2'). + Inductive wf : list (sigT eP) -> forall {t}, @expr var1 t -> @expr var2 t -> Prop := + | WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e') + | WfAbs : forall A B G e e', + (forall x x', @wf ((x == x') :: G) B (e x) (e' x')) + -> @wf G (A -> B) (Abs e) (Abs e'). + End wf. + + Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2). + + Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E. + End expr_param. +End language. +Global Arguments Prod {_} _ _. +Global Arguments Arrow {_} _ _. +Global Arguments Tbase {_} _. +Infix "*" := (@Prod _) : ctype_scope. +Notation "A -> B" := (@Arrow _ A B) : ctype_scope. + +Ltac admit_Wf := apply Wf_admitted. + +Global Arguments Const {_ _ _ _ _} _. +Global Arguments Var {_ _ _ _ _} _. +Global Arguments SmartVar {_ _ _ _ _} _. +Global Arguments SmartVarVar {_ _ _ _ _} _. +Global Arguments SmartConst {_ _ _ _ _} _. +Global Arguments Op {_ _ _ _ _ _} _ _. +Global Arguments Let {_ _ _ _ _} _ {_} _. +Global Arguments Pair {_ _ _ _ _} _ {_} _. +Global Arguments Return {_ _ _ _ _} _. +Global Arguments Abs {_ _ _ _ _ _} _. +Global Arguments interp_flat_type_gen {_} _ _. +Global Arguments interp_type {_} _ _. + +Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope. +Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. +Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v new file mode 100644 index 000000000..cbcf46753 --- /dev/null +++ b/src/Reflection/TestCase.v @@ -0,0 +1,114 @@ +Require Import Crypto.Reflection.Syntax. +Require Crypto.Reflection.InputSyntax. +Require Crypto.Reflection.ReifyDirect. +Require Crypto.Reflection.ReifyExact. +Require Crypto.Reflection.Linearize. + +Module Direct. + Export ReifyDirect. + + Import ReifyDebugNotations. + + Inductive base_type := Tnat. + Definition interp_base_type (v : base_type) : Type := + match v with + | Tnat => nat + end. + Local Notation tnat := (Tbase Tnat). + Inductive op : flat_type base_type -> flat_type base_type -> Type := + | Add : op (Prod tnat tnat) tnat + | Mul : op (Prod tnat tnat) tnat. + + Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I. + Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I. + Global Instance: reify type nat := Tnat. + + Ltac Reify e := ReifyDirect.Reify base_type interp_base_type op e. + + (*Ltac reify_debug_level ::= constr:(2).*) + + Goal (base_type -> Type) -> False. + intro var. + let x := reifyf base_type interp_base_type op var 1%nat in pose x. + let x := Reify 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1). + let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. + let x := Reify (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))). + let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. + let x := Reify (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). + let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. + let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. + let x := Reify (fun x => let '(a, b) := (1, 1) in a + x)%nat in + unify x (fun var => Abs (fun x0 => + let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in + Let (Pair c1 c1) + (fun ab : var Tnat * var Tnat => Op Add (Pair (Var (fst ab)) (Var x0))))). + Abort. +End Direct. + +Module Exact. + Export ReifyExact. + Import InputSyntax. + + Import ReifyDebugNotations. + + Inductive base_type := Tnat. + Definition interp_base_type (v : base_type) : Type := + match v with + | Tnat => nat + end. + Local Notation tnat := (Tbase Tnat). + Inductive op : flat_type base_type -> flat_type base_type -> Type := + | Add : op (Prod tnat tnat) tnat + | Mul : op (Prod tnat tnat) tnat. + Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst + := match f with + | Add => fun xy => fst xy + snd xy + | Mul => fun xy => fst xy * snd xy + end%nat. + + Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I. + Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I. + Global Instance: reify type nat := Tnat. + + Ltac Reify' e := ReifyExact.Reify' base_type interp_base_type op e. + Ltac Reify e := ReifyExact.Reify base_type interp_base_type op e. + Ltac Reify_rhs := ReifyExact.Reify_rhs base_type interp_base_type op interp_op. + + (*Ltac reify_debug_level ::= constr:(2).*) + + Goal (flat_type base_type -> Type) -> False. + intro var. + let x := reifyf base_type interp_base_type op var 1%nat in pose x. + let x := Reify' 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1). + let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. + let x := Reify' (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))). + let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. + let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). + let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. + let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. + let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x. + let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in + unify x (fun var => Abs (fun x' => + let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in + MatchPair (tC:=tnat) (Pair c1 c1) + (fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))). + let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. + let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. + Abort. + + Goal (0 = let x := 1+2 in x*3)%nat. + Reify_rhs. + Abort. + + Goal (0 = let x := 1 in let y := 2 in x * y)%nat. + Reify_rhs. + Abort. + + Import Linearize. + + Goal True. + let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in + pose (InlineConst (Linearize x)) as e. + vm_compute in e. + Abort. +End Exact. -- cgit v1.2.3 From 93398f3889a094cc1862f8cad2d23f5661c4f852 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 3 Sep 2016 16:59:19 -0700 Subject: A helper lemma for [Wf] This method allows a proof term that's linear in the term being proven well-founded, rather than exponential in it. By factoring out all of the reasoning about expressions, we can incur overhead equal to (the number of constants) + (the number of let-bindings) + (the number of variables used), all without mentioning the term itself; [vm_compute] can do the appropriate reduction for us. --- _CoqProject | 1 + src/Reflection/TestCase.v | 52 +++++++ src/Reflection/WfReflective.v | 306 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 359 insertions(+) create mode 100644 src/Reflection/WfReflective.v (limited to 'src') diff --git a/_CoqProject b/_CoqProject index ae4bea90f..144b187e7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -70,6 +70,7 @@ src/Reflection/ReifyDirect.v src/Reflection/ReifyExact.v src/Reflection/Syntax.v src/Reflection/TestCase.v +src/Reflection/WfReflective.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v src/Spec/Encoding.v diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index cbcf46753..056ec44f3 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -3,6 +3,7 @@ Require Crypto.Reflection.InputSyntax. Require Crypto.Reflection.ReifyDirect. Require Crypto.Reflection.ReifyExact. Require Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.WfReflective. Module Direct. Export ReifyDirect. @@ -96,6 +97,7 @@ Module Exact. let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. Abort. + Goal (0 = let x := 1+2 in x*3)%nat. Reify_rhs. Abort. @@ -111,4 +113,54 @@ Module Exact. pose (InlineConst (Linearize x)) as e. vm_compute in e. Abort. + + Definition example_expr : Syntax.Expr base_type interp_base_type op (Tbase Tnat). + Proof. + let x := Reify (let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in + exact x. + Defined. + + Definition base_type_eq_semidec_transparent : forall t1 t2, option (t1 = t2) + := fun t1 t2 => match t1, t2 with + | Tnat, Tnat => Some eq_refl + end. + Lemma base_type_eq_semidec_is_dec : forall t1 t2, + base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2. + Proof. + intros t1 t2; destruct t1, t2; simpl; intros; congruence. + Qed. + Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop + := fun x y => match x, y with + | Add, Add => Some trivial + | Add, _ => None + | Mul, Mul => Some trivial + | Mul, _ => None + end. + Lemma op_beq_bl t1 tR (x y : op t1 tR) + : match op_beq t1 tR x y with + | Some p => to_prop p + | None => False + end -> x = y. + Proof. + destruct x; simpl. + { refine match y with Add => _ | _ => _ end; tauto. } + { refine match y with Add => _ | _ => _ end; tauto. } + Qed. + + Lemma example_expr_wf : Wf _ _ _ example_expr. + Proof. + cbv beta delta [example_expr Wf]. + intros var1 var2. + repeat match goal with |- wf _ _ _ _ _ _ => constructor; intros end. + revert var1 var2. + vm_compute. + let Hwf := fresh "Hwf" in + lazymatch goal with + | [ |- forall var1' var2', @wff ?base_type ?interp_base_type ?op var1' var2' (@?G var1' var2') ?t (@?e1 var1') (@?e2 var2') ] + => intros var1 var2; pose proof (@reflect_wff base_type interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 (G var1 var2) t t (e1 _) (e2 _)) as Hwf + end. + revert Hwf; vm_compute. + intro Hwf; apply Hwf; clear Hwf. + tauto. + Qed. End Exact. diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v new file mode 100644 index 000000000..c34acfb24 --- /dev/null +++ b/src/Reflection/WfReflective.v @@ -0,0 +1,306 @@ +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. + +Inductive pointed_Prop := trivial | inject (_ : Prop). +Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop + := match x, y with + | trivial, trivial => trivial + | trivial, inject p => inject p + | inject p, trivial => inject p + | inject p, inject q => inject (p /\ q) + end. +Definition to_prop (x : pointed_Prop) : Prop + := match x with + | trivial => True + | inject p => p + end. + +Local Infix "/\" := and_pointed_Prop : type_scope. + +Definition f_equal2 {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H : x1 = y1) + := match H in (_ = y) return (x2 = y2 -> f x1 x2 = f y y2) with + | eq_refl => + fun H0 : x2 = y2 => + match H0 in (_ = y) return (f x1 x2 = f x1 y) with + | eq_refl => eq_refl + end + end. + +Section language. + Context (base_type_code : Type). + Context (interp_base_type : base_type_code -> Type). + Context (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)). + Context (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2). + Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop). + Context (op_beq_bl : forall t1 tR x y, match op_beq t1 tR x y with + | Some p => to_prop p + | _ => False + end -> x = y). + Context {var1 var2 : base_type_code -> Type}. + + Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing). + + 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 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). + + (*Fixpoint eq_interp_flat_type (t1 t2 : flat_type) + : interp_flat_type t1 -> interp_flat_type t2 -> option pointed_Prop + := match t1, t2 return interp_flat_type t1 -> interp_flat_type t2 -> option _ with + | Prod A B, Prod A' B' + => fun x y => match @eq_interp_flat_type A A' (fst x) (fst y), + @eq_interp_flat_type B B' (snd x) (snd y) with + | Some p, Some q => Some (p /\ q) + | _, _ => None + end + | Prod _ _, _ => fun _ _ => None + | Syntax.Tbase t1, Syntax.Tbase t2 + => fun x y => base_type_eq_and_cast t1 t2 x y (*Some (exists pf : t1 = t2, eq_rect _ interp_base_type x _ pf = y)*) + | Syntax.Tbase _, _ => fun _ _ => None + end.*) + Fixpoint flat_type_eq_semidec_transparent (t1 t2 : flat_type) : option (t1 = t2) + := match t1, t2 return option (t1 = t2) with + | Syntax.Tbase t1, Syntax.Tbase t2 + => option_map (@f_equal _ _ Tbase _ _) + (base_type_eq_semidec_transparent t1 t2) + | Syntax.Tbase _, _ => None + | Prod A B, Prod A' B' + => match flat_type_eq_semidec_transparent A A', flat_type_eq_semidec_transparent B B' with + | Some p, Some q => Some (f_equal2 Prod p q) + | _, _ => None + end + | Prod _ _, _ => None + end. + Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : option pointed_Prop + := match flat_type_eq_semidec_transparent t1 t1', flat_type_eq_semidec_transparent tR tR' with + | Some p, Some q + => match p in (_ = t1'), q in (_ = tR') return op t1' tR' -> _ with + | eq_refl, eq_refl => fun y => op_beq _ _ x y + end y + | _, _ => None + end. + + Definition eq_type_and_var : sigT eP -> sigT eP -> option pointed_Prop + := fun x y => + let 'existT (t1, t2) (a, b) := x in + let 'existT (t1', t2') (a', b') := y in + match base_type_eq_semidec_transparent t1 t1', base_type_eq_semidec_transparent t2 t2' with + | Some p, Some q + => Some (inject (and (eq_rect _ var1 a _ p = a') (eq_rect _ var2 b _ q = b'))) + | _, _ => None + end. + + + Definition duplicate_type (ls : list (sigT (fun t => var1 t * var2 t)%type)) : list (sigT eP) + := List.map (fun v => existT eP (projT1 v, projT1 v) (projT2 v)) ls. + + Lemma duplicate_type_app ls ls' + : (duplicate_type (ls ++ ls') = duplicate_type ls ++ duplicate_type ls')%list. + Proof. apply List.map_app. Qed. + Lemma duplicate_type_length ls + : List.length (duplicate_type ls) = List.length ls. + Proof. apply List.map_length. Qed. + (** TODO: Clean up this proof *) + Lemma base_type_eq_dec : forall t1 t2 : base_type_code, {t1 = t2} + {t1 <> t2}. + Proof. + intros t1 t2; destruct (base_type_eq_semidec_transparent t1 t2) eqn:H; + [ left; assumption | right; auto using base_type_eq_semidec_is_dec ]. + Qed. + Lemma duplicae_type_in t v ls + : List.In (existT _ (t, t) v) (duplicate_type ls) -> List.In (existT _ t v) ls. + Proof. + unfold duplicate_type; intro H. + apply List.in_map_iff in H. + destruct H as [ [t' ?] [? ?] ]. + simpl in *. + inversion_sigma; subst. + match goal with H : _ |- _ => generalize (path_prod_eta H) end. + let x := match goal with |- ?x = _ -> _ => x end in + generalize (fst_path x); generalize (snd_path x); simpl. + intro; subst; intro H'; intros; subst. + assert (H' = eq_refl) by apply UIP_dec, base_type_eq_dec. + subst; simpl; assumption. + Qed. + Lemma duplicate_type_not_in G t t0 v (H : base_type_eq_semidec_transparent t t0 = None) + : ~List.In (existT _ (t, t0) v) (duplicate_type G). + Proof. + apply base_type_eq_semidec_is_dec in H. + clear -H. + intro H'. + induction G as [|? ? IHG]; simpl in *; try tauto. + destruct H'; intuition eauto; congruence. + Qed. + + Definition preflatten_binding_list2 t1 t2 : option (forall (x : interp_flat_type_gen var1 t1) (y : interp_flat_type_gen var2 t2), list (sigT (fun t => var1 t * var2 t)%type)) + := match flat_type_eq_semidec_transparent t1 t2 with + | Some p + => Some (fun x y + => let x := eq_rect _ (interp_flat_type_gen var1) x _ p in + flatten_binding_list base_type_code x y) + | None => None + end. + 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). + 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 + let base := fst ret in + let b := snd ret in + let ret := @natize_interp_flat_type_gen _ A base (fst v) in + let base := fst ret in + let a := snd ret in + (base, (a, b)) + | Syntax.Tbase t => fun v => (S base, (base, v)) + end v. + 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. + revert base; induction t; simpl; [ reflexivity | ]. + intros; rewrite List.app_length, <- plus_assoc. + rewrite_hyp <- ?*; reflexivity. + Qed. + Lemma length_natize_interp_flat_type_gen2 {t} (base : nat) (v1 : interp_flat_type_gen var1 t) (v2 : interp_flat_type_gen var2 t) + : fst (natize_interp_flat_type_gen base v2) = length (flatten_binding_list base_type_code v1 v2) + base. + Proof. + revert base; induction t; simpl; [ reflexivity | ]. + intros; rewrite List.app_length, <- plus_assoc. + rewrite_hyp <- ?*; reflexivity. + Qed. + + Fixpoint unnatize_exprf {var t} (base : nat) (e : @exprf (fun t => nat * var t)%type t) : @exprf var t + := match e in @Syntax.exprf _ _ _ _ t return exprf t with + | Const _ x => Const x + | Var _ x => Var (snd x) + | Op _ _ op args => Op op (@unnatize_exprf _ _ base args) + | Let _ ex _ eC => Let (@unnatize_exprf _ _ base ex) (fun x => let v := natize_interp_flat_type_gen base x in + @unnatize_exprf _ _ (fst v) (eC (snd v))) + | Pair _ x _ y => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y) + end. + + Fixpoint reflect_wffT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) + {t1 t2 : flat_type} + (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2) + {struct e1} + : option pointed_Prop + := match e1, e2 return option _ with + | Const t0 x, Const t1 y + => match flat_type_eq_semidec_transparent t0 t1 with + | Some p => Some (inject (eq_rect _ interp_flat_type x _ p = y)) + | None => None + 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 + | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y)) + | _, _ => None + end + | Var _ _, _ => None + | Op t1 tR op args, Op t1' tR' op' args' + => match @reflect_wffT G t1 t1' args args', op_beq' t1 tR t1' tR' op op' with + | Some p, Some q => Some (p /\ q) + | _, _ => None + end + | Op _ _ _ _, _ => None + | Let tx ex tC eC, Let tx' ex' tC' eC' + => match @reflect_wffT G tx tx' ex ex', @flatten_binding_list2 tx tx', flat_type_eq_semidec_transparent tC tC' with + | Some p, Some G0, Some _ + => Some (p /\ inject (forall (x : interp_flat_type_gen var1 tx) (x' : interp_flat_type_gen var2 tx'), + match @reflect_wffT (G0 x x' ++ G)%list _ _ + (eC (snd (natize_interp_flat_type_gen (List.length G) x))) + (eC' (snd (natize_interp_flat_type_gen (List.length G) x'))) with + | Some p => to_prop p + | None => False + end)) + | _, _, _ => None + end + | Let _ _ _ _, _ => None + | Pair tx ex ty ey, Pair tx' ex' ty' ey' + => match @reflect_wffT G tx tx' ex ex', @reflect_wffT G ty ty' ey ey' with + | Some p, Some q => Some (p /\ q) + | _, _ => None + end + | Pair _ _ _ _, _ => None + end. + + Local Ltac handle_op_beq_correct := + repeat match goal with + | [ H : op_beq ?t1 ?tR ?x ?y = _ |- _ ] + => let H' := fresh in + pose proof (op_beq_bl t1 tR x y) as H'; rewrite H in H'; clear H + end. + Local Ltac t_step := + match goal with + | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, preflatten_binding_list2, option_map in * + | _ => progress simpl in * + | _ => progress break_match + | _ => progress subst + | _ => progress inversion_option + | _ => congruence + | _ => tauto + | _ => progress intros + | _ => progress handle_op_beq_correct + | _ => progress specialize_by tauto + | [ H : forall x x', _ |- wff _ _ _ (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ] + => specialize (H x1 x2) + | [ H : and _ _ |- _ ] => destruct H + | [ H : context[duplicate_type (_ ++ _)%list] |- _ ] + => rewrite duplicate_type_app in H + | [ H : context[List.length (duplicate_type _)] |- _ ] + => rewrite duplicate_type_length in H + | [ H : context[List.length (_ ++ _)%list] |- _ ] + => rewrite List.app_length in H + | [ |- wff _ _ _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ] + => erewrite length_natize_interp_flat_type_gen1, length_natize_interp_flat_type_gen2; eassumption + | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption + | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H + | [ H : List.In _ (duplicate_type _) |- _ ] => apply duplicae_type_in in H + | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match + | [ H : inject _ = inject _ |- _ ] => inversion H; clear H + | [ |- wff _ _ _ _ _ _ ] => constructor + | _ => progress unfold and_pointed_Prop in * + end. + Local Ltac t := repeat t_step. + Fixpoint reflect_wff (G : list (sigT (fun t => var1 t * var2 t)%type)) + {t1 t2 : flat_type} + (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2) + {struct e1} + : match reflect_wffT (duplicate_type G) e1 e2 with + | Some p => to_prop p + | None => False + end + -> match flat_type_eq_semidec_transparent t1 t2 with + | Some p => @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) + | None => False + end. + Proof. + destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ], + e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ intros [] ]; + [ clear reflect_wff + | clear reflect_wff + | specialize (reflect_wff G _ _ args args') + | pose proof (reflect_wff G _ _ ex ex'); + pose proof (fun x x' + => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with + | Some G0 + => reflect_wff + (G0 x x' ++ G)%list _ _ + (eC (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x))) + (eC' (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x'))) + | None => I + end); + clear reflect_wff + | pose proof (reflect_wff G _ _ ex ex'); pose proof (reflect_wff G _ _ ey ey'); clear reflect_wff ]. + { t. } + { t. } + { t. } + { t. } + { t. } + Qed. +End language. -- cgit v1.2.3 From 28fc98d1caa4bad57ea13cce3715062f892c5f78 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 10:49:43 -0700 Subject: Remove ReifyDirect It's probably not going to be used --- _CoqProject | 2 +- src/Reflection/Reify.v | 249 +++++++++++++++++++++++++++++++++++++++ src/Reflection/ReifyDirect.v | 212 --------------------------------- src/Reflection/ReifyExact.v | 249 --------------------------------------- src/Reflection/TestCase.v | 275 ++++++++++++++++++------------------------- 5 files changed, 364 insertions(+), 623 deletions(-) create mode 100644 src/Reflection/Reify.v delete mode 100644 src/Reflection/ReifyDirect.v delete mode 100644 src/Reflection/ReifyExact.v (limited to 'src') diff --git a/_CoqProject b/_CoqProject index 144b187e7..ed58ac302 100644 --- a/_CoqProject +++ b/_CoqProject @@ -66,8 +66,8 @@ src/ModularArithmetic/Montgomery/ZProofs.v src/Reflection/InputSyntax.v src/Reflection/InterpProofs.v src/Reflection/Linearize.v +src/Reflection/Reify.v src/Reflection/ReifyDirect.v -src/Reflection/ReifyExact.v src/Reflection/Syntax.v src/Reflection/TestCase.v src/Reflection/WfReflective.v diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v new file mode 100644 index 000000000..1eac17675 --- /dev/null +++ b/src/Reflection/Reify.v @@ -0,0 +1,249 @@ +(** * Exact reification of PHOAS Representation of Gallina *) +(** The reification procedure goes through [InputSyntax], which allows + judgmental equality of the denotation of the reified term. *) +Require Import Coq.Strings.String. +Require Import Crypto.Reflection.Syntax. +Require Export Crypto.Reflection.InputSyntax. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. +Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. +Arguments reify_var_for_in_is _ {T} _ _ {eT} _. + +(** [reify] assumes that operations can be reified via the [reify_op] + typeclass, which gets passed the type family of operations, the + expression which is headed by an operation, and expects resolution + to fill in a number of arguments (which [reifyf] will + automatically curry), as well as the reified operator. + + We also assume that types can be reified via the [reify] typeclass + with arguments [reify type ]. *) +Class reify_op {opTF} (op_family : opTF) {opExprT} (opExpr : opExprT) (nargs : nat) {opT} (reified_op : opT) + := Build_reify_op : True. +Ltac strip_type_cast term := lazymatch term with ?term' => term' end. +Ltac reify_type T := + lazymatch T with + | (?A -> ?B)%type + => let a := reify_type A in + let b := reify_type B in + constr:(@Arrow _ a b) + | prod ?A ?B + => let a := reify_type A in + let b := reify_type B in + constr:(@Prod _ a b) + | _ + => let v := strip_type_cast (_ : reify type T) in + constr:(Tbase v) + end. +Ltac reify_base_type T := + let t := reify_type T in + lazymatch t with + | Tbase ?t => t + | ?t => t + end. + +Ltac reifyf_var x mkVar := + lazymatch goal with + | _ : reify_var_for_in_is _ x ?t ?v |- _ => mkVar t v + | _ => lazymatch x with + | fst ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with + | Prod ?A ?B => mkVar A (fst v) + end) + | snd ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with + | Prod ?A ?B => mkVar B (snd v) + end) + end + end. + +Inductive reify_result_helper := +| finished_value {T} (res : T) +| op_info {T} (res : T) +| reification_unsuccessful. + +(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get + more debugging. *) +Ltac reify_debug_level := constr:(0). +Module Import ReifyDebugNotations. + Open Scope string_scope. +End ReifyDebugNotations. + +Ltac debug_enter_reifyf e := + let lvl := reify_debug_level in + match lvl with + | S (S _) => cidtac2 "reifyf: Attempting to reify:" e + | _ => constr:(Set) + end. +Ltac debug_enter_reify_abs e := + let lvl := reify_debug_level in + match lvl with + | S (S _) => cidtac2 "reify_abs: Attempting to reify:" e + | _ => constr:(Set) + end. + +Ltac debug_enter_reify_rec := + let lvl := reify_debug_level in + match lvl with + | S _ => idtac_goal + | _ => idtac + end. +Ltac debug_leave_reify_rec e := + let lvl := reify_debug_level in + match lvl with + | S _ => idtac "reifyf success:" e "" + | _ => idtac + end. + +Ltac reifyf base_type_code interp_base_type op var e := + let reify_rec e := reifyf base_type_code interp_base_type op var e in + let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in + let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in + let mkVar T ex := constr:(Var (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in + let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in + let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in + let mkMatchPair tC ex eC := constr:(MatchPair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (tC:=tC) ex eC) in + let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in + let dummy := debug_enter_reifyf e in + lazymatch e with + | let x := ?ex in @?eC x => + let ex := reify_rec ex in + let eC := reify_rec eC in + mkLet ex eC + | pair ?a ?b => + let a := reify_rec a in + let b := reify_rec b in + mkPair a b + | (fun x : ?T => ?C) => + let t := reify_type T in + (* Work around Coq 8.5 and 8.6 bug *) + (* *) + (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) + (* even if its Gallina name matches a Ltac in this tactic. *) + let maybe_x := fresh x in + let not_x := fresh x in + lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) => + (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) + with fun _ v _ => @?C v => C end + | match ?ev with pair a b => @?eC a b end => + let t := (let T := match type of eC with _ -> _ -> ?T => T end in reify_type T) in + let v := reify_rec ev in + let C := reify_rec eC in + mkMatchPair t v C + | ?x => + let t := lazymatch type of x with ?t => reify_type t end in + let retv := match constr:(Set) with + | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv) + | _ => let r := constr:(_ : reify_op op x _ _) in + let t := type of r in + constr:(op_info t) + | _ => let c := mkConst t x in + constr:(finished_value c) + | _ => constr:(reification_unsuccessful) + end in + lazymatch retv with + | finished_value ?v => v + | op_info (reify_op _ _ ?nargs ?op_code) + => let tR := (let tR := type of x in reify_type tR) in + lazymatch nargs with + | 1%nat + => lazymatch x with + | ?f ?x0 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + mkOp a0T tR op_code a0 + end + | 2%nat + => lazymatch x with + | ?f ?x0 ?x1 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + let a1T := (let t := type of x1 in reify_type t) in + let a1 := reify_rec x1 in + let args := mkPair a0 a1 in + mkOp (@Prod _ a0T a1T) tR op_code args + end + | 3%nat + => lazymatch x with + | ?f ?x0 ?x1 ?x2 + => let a0T := (let t := type of x0 in reify_type t) in + let a0 := reify_rec x0 in + let a1T := (let t := type of x1 in reify_type t) in + let a1 := reify_rec x1 in + let a2T := (let t := type of x2 in reify_type t) in + let a2 := reify_rec x2 in + let args := let a01 := mkPair a0 a1 in mkPair a01 a2 in + mkOp (@Prod _ (@Prod _ a0T a1T) a2T) tR op_code args + end + | _ => cfail2 "Unsupported number of operation arguments in reifyf:"%string nargs + end + | reification_unsuccessful + => cfail2 "Failed to reify:"%string x + end + end. + +Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. + +(** For reification including [Abs] *) +Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T. +Ltac reify_abs base_type_code interp_base_type op var e := + let reify_rec e := reify_abs base_type_code interp_base_type op var e in + let reifyf_term e := reifyf base_type_code interp_base_type op var e in + let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in + let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in + let dummy := debug_enter_reify_abs e in + lazymatch e with + | (fun x : ?T => ?C) => + let t := reify_base_type T in + (* Work around Coq 8.5 and 8.6 bug *) + (* *) + (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) + (* even if its Gallina name matches a Ltac in this tactic. *) + let maybe_x := fresh x in + let not_x := fresh x in + lazymatch constr:(fun (x : T) (not_x : var (Tbase t)) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) => + (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) + with fun _ v _ => @?C v => mkAbs t C end + | ?x => + reifyf_term x + end. + +Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) +=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. + +Ltac Reify' base_type_code interp_base_type op e := + lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with + (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *) + end. +Ltac Reify base_type_code interp_base_type op e := + let r := Reify' base_type_code interp_base_type op e in + constr:(InputSyntax.Compile base_type_code interp_base_type op r). + +Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. +Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. + +Ltac Reify_rhs base_type_code interp_base_type op interp_op := + let rhs := rhs_of_goal in + let RHS := Reify base_type_code interp_base_type op rhs in + transitivity (Syntax.Interp base_type_code interp_base_type op interp_op RHS); + [ + | etransitivity; (* first we strip off the [InputSyntax.Compile] + bit; Coq is bad at inferring the type, so we + help it out by providing it *) + [ lazymatch goal with + | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] + => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e) + end + | ((* now we unfold the interpretation function, including the + parameterized bits; we assume that [hnf] is enough to unfold + the interpretation functions that we're parameterized + over. *) + lazymatch goal with + | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ] + => let interp_base_type' := (eval hnf in interp_base_type) in + let interp_op' := (eval hnf in interp_op) in + change interp_base_type with interp_base_type'; + change interp_op with interp_op' + end; + cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type_gen interp interpf]; simplify_projections; reflexivity) ] ]. diff --git a/src/Reflection/ReifyDirect.v b/src/Reflection/ReifyDirect.v deleted file mode 100644 index 41eb86a1f..000000000 --- a/src/Reflection/ReifyDirect.v +++ /dev/null @@ -1,212 +0,0 @@ -(** * Direct reification of PHOAS Representation of Gallina *) -(** The reification procedure introduces extra [let]s and [match]es, - so we don't get something syntactically equal. Without primitive - projections, we don't get something judgmentally equal. *) -Require Import Coq.Strings.String. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.Notations. - -Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. -Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. -Arguments reify_var_for_in_is _ {T} _ _ {eT} _. - -(** [reify] assumes that operations can be reified via the [reify_op] - typeclass, which gets passed the type family of operations, the - expression which is headed by an operation, and expects resolution - to fill in a number of arguments (which [reifyf] will - automatically curry), as well as the reified operator. - - We also assume that types can be reified via the [reify] typeclass - with arguments [reify type ]. *) -Class reify_op {opTF} (op_family : opTF) {opExprT} (opExpr : opExprT) (nargs : nat) {opT} (reified_op : opT) - := Build_reify_op : True. -Ltac strip_type_cast term := lazymatch term with ?term' => term' end. -Ltac reify_type T := - lazymatch T with - | (?A -> ?B)%type - => let a := reify_type A in - let b := reify_type B in - constr:(@Arrow _ a b) - | prod ?A ?B - => let a := reify_type A in - let b := reify_type B in - constr:(@Prod _ a b) - | _ - => let v := strip_type_cast (_ : reify type T) in - constr:(Tbase v) - end. -Ltac reify_base_type T := - let t := reify_type T in - lazymatch t with - | Tbase ?t => t - | ?t => t - end. - -Ltac reifyf_var x mkVar := - lazymatch goal with - | _ : reify_var_for_in_is _ x ?t ?v |- _ => mkVar t v - | _ => lazymatch x with - | fst ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with - | Prod ?A ?B => mkVar A (fst v) - end) - | snd ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with - | Prod ?A ?B => mkVar B (snd v) - end) - end - end. - -Inductive reify_result_helper := -| finished_value {T} (res : T) -| op_info {T} (res : T) -| reification_unsuccessful. - -(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get - more debugging. *) -Ltac reify_debug_level := constr:(0). -Module Import ReifyDebugNotations. - Open Scope string_scope. -End ReifyDebugNotations. - -Ltac debug_enter_reifyf e := - let lvl := reify_debug_level in - match lvl with - | S (S _) => cidtac2 "reifyf: Attempting to reify:" e - | _ => constr:(Set) - end. - -Ltac debug_enter_reify_rec := - let lvl := reify_debug_level in - match lvl with - | S _ => idtac_goal - | _ => idtac - end. -Ltac debug_leave_reify_rec e := - let lvl := reify_debug_level in - match lvl with - | S _ => idtac "reifyf success:" e "" - | _ => idtac - end. - -Ltac reifyf base_type_code interp_base_type op var e := - let reify_rec e := reifyf base_type_code interp_base_type op var e in - let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in - let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in - let mkVar T ex := constr:(SmartVar (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in - let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in - let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in - let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in - let dummy := debug_enter_reifyf e in - lazymatch e with - | let x := ?ex in @?eC x => - let ex := reify_rec ex in - let eC := reify_rec eC in - mkLet ex eC - | pair ?a ?b => - let a := reify_rec a in - let b := reify_rec b in - mkPair a b - | (fun x : ?T => ?C) => - let t := reify_type T in - (* Work around Coq 8.5 and 8.6 bug *) - (* *) - (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) - (* even if its Gallina name matches a Ltac in this tactic. *) - let maybe_x := fresh x in - let not_x := fresh x in - lazymatch constr:(fun (x : T) (not_x : interp_flat_type_gen var t) (_ : reify_var_for_in_is base_type_code x t not_x) => - (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) - with fun _ v _ => @?C v => C end - | match ?ev with pair a b => @?eC a b end => - let v := reify_rec ev in - let C := reify_rec eC in - let C := lazymatch C - with (fun (a : ?A) (b : ?B) => ?C) => constr:(fun ab : prod A B => match fst ab, snd ab with a, b => C end) end in - mkLet v C - | ?x => - let t := lazymatch type of x with ?t => reify_type t end in - let retv := match constr:(Set) with - | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv) - | _ => let r := constr:(_ : reify_op op x _ _) in - let t := type of r in - constr:(op_info t) - | _ => let c := mkConst t x in - constr:(finished_value c) - | _ => constr:(reification_unsuccessful) - end in - lazymatch retv with - | finished_value ?v => v - | op_info (reify_op _ _ ?nargs ?op_code) - => let tR := (let tR := type of x in reify_type tR) in - lazymatch nargs with - | 1%nat - => lazymatch x with - | ?f ?x0 - => let a0T := (let t := type of x0 in reify_type t) in - let a0 := reify_rec x0 in - mkOp a0T tR op_code a0 - end - | 2%nat - => lazymatch x with - | ?f ?x0 ?x1 - => let a0T := (let t := type of x0 in reify_type t) in - let a0 := reify_rec x0 in - let a1T := (let t := type of x1 in reify_type t) in - let a1 := reify_rec x1 in - let args := mkPair a0 a1 in - mkOp (@Prod _ a0T a1T) tR op_code args - end - | 3%nat - => lazymatch x with - | ?f ?x0 ?x1 ?x2 - => let a0T := (let t := type of x0 in reify_type t) in - let a0 := reify_rec x0 in - let a1T := (let t := type of x1 in reify_type t) in - let a1 := reify_rec x1 in - let a2T := (let t := type of x2 in reify_type t) in - let a2 := reify_rec x2 in - let args := let a01 := mkPair a0 a1 in mkPair a01 a2 in - mkOp (@Prod _ (@Prod _ a0T a1T) a2T) tR op_code args - end - | _ => cfail2 "Unsupported number of operation arguments in reifyf:"%string nargs - end - | reification_unsuccessful - => cfail2 "Failed to reify:"%string x - end - end. - -Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) -=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. - -(** For reification including [Abs] *) -Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T. -Ltac reify_abs base_type_code interp_base_type op var e := - let reify_rec e := reify_abs base_type_code interp_base_type op var e in - let reifyf_term e := reifyf base_type_code interp_base_type op var e in - let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in - let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in - let dummy := debug_enter_reifyf e in - lazymatch e with - | (fun x : ?T => ?C) => - let t := reify_base_type T in - (* Work around Coq 8.5 and 8.6 bug *) - (* *) - (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) - (* even if its Gallina name matches a Ltac in this tactic. *) - let maybe_x := fresh x in - let not_x := fresh x in - lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) => - (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) - with fun _ v _ => @?C v => mkAbs t C end - | ?x => - reifyf_term x - end. - -Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) -=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. - -Ltac Reify base_type_code interp_base_type op e := - lazymatch constr:(fun (var : base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with - (fun var => ?C) => constr:(fun (var : base_type_code -> Type) => C) (* copy the term but not the type cast *) - end. diff --git a/src/Reflection/ReifyExact.v b/src/Reflection/ReifyExact.v deleted file mode 100644 index 1eac17675..000000000 --- a/src/Reflection/ReifyExact.v +++ /dev/null @@ -1,249 +0,0 @@ -(** * Exact reification of PHOAS Representation of Gallina *) -(** The reification procedure goes through [InputSyntax], which allows - judgmental equality of the denotation of the reified term. *) -Require Import Coq.Strings.String. -Require Import Crypto.Reflection.Syntax. -Require Export Crypto.Reflection.InputSyntax. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.Tactics. -Require Import Crypto.Util.Notations. - -Class reify {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify : T. -Definition reify_var_for_in_is base_type_code {T} (x : T) (t : flat_type base_type_code) {eT} (e : eT) := False. -Arguments reify_var_for_in_is _ {T} _ _ {eT} _. - -(** [reify] assumes that operations can be reified via the [reify_op] - typeclass, which gets passed the type family of operations, the - expression which is headed by an operation, and expects resolution - to fill in a number of arguments (which [reifyf] will - automatically curry), as well as the reified operator. - - We also assume that types can be reified via the [reify] typeclass - with arguments [reify type ]. *) -Class reify_op {opTF} (op_family : opTF) {opExprT} (opExpr : opExprT) (nargs : nat) {opT} (reified_op : opT) - := Build_reify_op : True. -Ltac strip_type_cast term := lazymatch term with ?term' => term' end. -Ltac reify_type T := - lazymatch T with - | (?A -> ?B)%type - => let a := reify_type A in - let b := reify_type B in - constr:(@Arrow _ a b) - | prod ?A ?B - => let a := reify_type A in - let b := reify_type B in - constr:(@Prod _ a b) - | _ - => let v := strip_type_cast (_ : reify type T) in - constr:(Tbase v) - end. -Ltac reify_base_type T := - let t := reify_type T in - lazymatch t with - | Tbase ?t => t - | ?t => t - end. - -Ltac reifyf_var x mkVar := - lazymatch goal with - | _ : reify_var_for_in_is _ x ?t ?v |- _ => mkVar t v - | _ => lazymatch x with - | fst ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with - | Prod ?A ?B => mkVar A (fst v) - end) - | snd ?x' => reifyf_var x' ltac:(fun t v => lazymatch t with - | Prod ?A ?B => mkVar B (snd v) - end) - end - end. - -Inductive reify_result_helper := -| finished_value {T} (res : T) -| op_info {T} (res : T) -| reification_unsuccessful. - -(** Change this with [Ltac reify_debug_level ::= constr:(1).] to get - more debugging. *) -Ltac reify_debug_level := constr:(0). -Module Import ReifyDebugNotations. - Open Scope string_scope. -End ReifyDebugNotations. - -Ltac debug_enter_reifyf e := - let lvl := reify_debug_level in - match lvl with - | S (S _) => cidtac2 "reifyf: Attempting to reify:" e - | _ => constr:(Set) - end. -Ltac debug_enter_reify_abs e := - let lvl := reify_debug_level in - match lvl with - | S (S _) => cidtac2 "reify_abs: Attempting to reify:" e - | _ => constr:(Set) - end. - -Ltac debug_enter_reify_rec := - let lvl := reify_debug_level in - match lvl with - | S _ => idtac_goal - | _ => idtac - end. -Ltac debug_leave_reify_rec e := - let lvl := reify_debug_level in - match lvl with - | S _ => idtac "reifyf success:" e "" - | _ => idtac - end. - -Ltac reifyf base_type_code interp_base_type op var e := - let reify_rec e := reifyf base_type_code interp_base_type op var e in - let mkLet ex eC := constr:(Let (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex eC) in - let mkPair ex ey := constr:(Pair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) ex ey) in - let mkVar T ex := constr:(Var (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in - let mkConst T ex := constr:(Const (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t:=T) ex) in - let mkOp T retT op_code args := constr:(Op (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (t1:=T) (tR:=retT) op_code args) in - let mkMatchPair tC ex eC := constr:(MatchPair (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (tC:=tC) ex eC) in - let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in - let dummy := debug_enter_reifyf e in - lazymatch e with - | let x := ?ex in @?eC x => - let ex := reify_rec ex in - let eC := reify_rec eC in - mkLet ex eC - | pair ?a ?b => - let a := reify_rec a in - let b := reify_rec b in - mkPair a b - | (fun x : ?T => ?C) => - let t := reify_type T in - (* Work around Coq 8.5 and 8.6 bug *) - (* *) - (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) - (* even if its Gallina name matches a Ltac in this tactic. *) - let maybe_x := fresh x in - let not_x := fresh x in - lazymatch constr:(fun (x : T) (not_x : var t) (_ : reify_var_for_in_is base_type_code x t not_x) => - (_ : reify reify_tag C)) (* [C] here is an open term that references "x" by name *) - with fun _ v _ => @?C v => C end - | match ?ev with pair a b => @?eC a b end => - let t := (let T := match type of eC with _ -> _ -> ?T => T end in reify_type T) in - let v := reify_rec ev in - let C := reify_rec eC in - mkMatchPair t v C - | ?x => - let t := lazymatch type of x with ?t => reify_type t end in - let retv := match constr:(Set) with - | _ => let retv := reifyf_var x mkVar in constr:(finished_value retv) - | _ => let r := constr:(_ : reify_op op x _ _) in - let t := type of r in - constr:(op_info t) - | _ => let c := mkConst t x in - constr:(finished_value c) - | _ => constr:(reification_unsuccessful) - end in - lazymatch retv with - | finished_value ?v => v - | op_info (reify_op _ _ ?nargs ?op_code) - => let tR := (let tR := type of x in reify_type tR) in - lazymatch nargs with - | 1%nat - => lazymatch x with - | ?f ?x0 - => let a0T := (let t := type of x0 in reify_type t) in - let a0 := reify_rec x0 in - mkOp a0T tR op_code a0 - end - | 2%nat - => lazymatch x with - | ?f ?x0 ?x1 - => let a0T := (let t := type of x0 in reify_type t) in - let a0 := reify_rec x0 in - let a1T := (let t := type of x1 in reify_type t) in - let a1 := reify_rec x1 in - let args := mkPair a0 a1 in - mkOp (@Prod _ a0T a1T) tR op_code args - end - | 3%nat - => lazymatch x with - | ?f ?x0 ?x1 ?x2 - => let a0T := (let t := type of x0 in reify_type t) in - let a0 := reify_rec x0 in - let a1T := (let t := type of x1 in reify_type t) in - let a1 := reify_rec x1 in - let a2T := (let t := type of x2 in reify_type t) in - let a2 := reify_rec x2 in - let args := let a01 := mkPair a0 a1 in mkPair a01 a2 in - mkOp (@Prod _ (@Prod _ a0T a1T) a2T) tR op_code args - end - | _ => cfail2 "Unsupported number of operation arguments in reifyf:"%string nargs - end - | reification_unsuccessful - => cfail2 "Failed to reify:"%string x - end - end. - -Hint Extern 0 (reify (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) -=> (debug_enter_reify_rec; let e := reifyf base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. - -(** For reification including [Abs] *) -Class reify_abs {varT} (var : varT) {eT} (e : eT) {T : Type} := Build_reify_abs : T. -Ltac reify_abs base_type_code interp_base_type op var e := - let reify_rec e := reify_abs base_type_code interp_base_type op var e in - let reifyf_term e := reifyf base_type_code interp_base_type op var e in - let mkAbs src ef := constr:(Abs (base_type_code:=base_type_code) (interp_base_type:=interp_base_type) (op:=op) (var:=var) (src:=src) ef) in - let reify_tag := constr:(@exprf base_type_code interp_base_type op var) in - let dummy := debug_enter_reify_abs e in - lazymatch e with - | (fun x : ?T => ?C) => - let t := reify_base_type T in - (* Work around Coq 8.5 and 8.6 bug *) - (* *) - (* Avoid re-binding the Gallina variable referenced by Ltac [x] *) - (* even if its Gallina name matches a Ltac in this tactic. *) - let maybe_x := fresh x in - let not_x := fresh x in - lazymatch constr:(fun (x : T) (not_x : var (Tbase t)) (_ : reify_var_for_in_is base_type_code x (Tbase t) not_x) => - (_ : reify_abs reify_tag C)) (* [C] here is an open term that references "x" by name *) - with fun _ v _ => @?C v => mkAbs t C end - | ?x => - reifyf_term x - end. - -Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) -=> (debug_enter_reify_rec; let e := reify_abs base_type_code interp_base_type op var e in debug_leave_reify_rec e; eexact e) : typeclass_instances. - -Ltac Reify' base_type_code interp_base_type op e := - lazymatch constr:(fun (var : flat_type base_type_code -> Type) => (_ : reify_abs (@exprf base_type_code interp_base_type op var) e)) with - (fun var => ?C) => constr:(fun (var : flat_type base_type_code -> Type) => C) (* copy the term but not the type cast *) - end. -Ltac Reify base_type_code interp_base_type op e := - let r := Reify' base_type_code interp_base_type op e in - constr:(InputSyntax.Compile base_type_code interp_base_type op r). - -Ltac lhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => LHS end. -Ltac rhs_of_goal := lazymatch goal with |- ?R ?LHS ?RHS => RHS end. - -Ltac Reify_rhs base_type_code interp_base_type op interp_op := - let rhs := rhs_of_goal in - let RHS := Reify base_type_code interp_base_type op rhs in - transitivity (Syntax.Interp base_type_code interp_base_type op interp_op RHS); - [ - | etransitivity; (* first we strip off the [InputSyntax.Compile] - bit; Coq is bad at inferring the type, so we - help it out by providing it *) - [ lazymatch goal with - | [ |- @Syntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op (@Tflat _ ?t) (@Compile _ _ _ _ ?e) = _ ] - => exact (@InputSyntax.Compile_correct base_type_code interp_base_type op interp_op t e) - end - | ((* now we unfold the interpretation function, including the - parameterized bits; we assume that [hnf] is enough to unfold - the interpretation functions that we're parameterized - over. *) - lazymatch goal with - | [ |- @InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e = _ ] - => let interp_base_type' := (eval hnf in interp_base_type) in - let interp_op' := (eval hnf in interp_op) in - change interp_base_type with interp_base_type'; - change interp_op with interp_op' - end; - cbv iota beta delta [InputSyntax.Interp interp_type interp_type_gen interp_flat_type_gen interp interpf]; simplify_projections; reflexivity) ] ]. diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 056ec44f3..1db00b9cc 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -1,166 +1,119 @@ Require Import Crypto.Reflection.Syntax. -Require Crypto.Reflection.InputSyntax. -Require Crypto.Reflection.ReifyDirect. -Require Crypto.Reflection.ReifyExact. +Require Export Crypto.Reflection.Reify. +Require Import Crypto.Reflection.InputSyntax. Require Crypto.Reflection.Linearize. Require Import Crypto.Reflection.WfReflective. -Module Direct. - Export ReifyDirect. - - Import ReifyDebugNotations. - - Inductive base_type := Tnat. - Definition interp_base_type (v : base_type) : Type := - match v with - | Tnat => nat - end. - Local Notation tnat := (Tbase Tnat). - Inductive op : flat_type base_type -> flat_type base_type -> Type := - | Add : op (Prod tnat tnat) tnat - | Mul : op (Prod tnat tnat) tnat. - - Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I. - Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I. - Global Instance: reify type nat := Tnat. - - Ltac Reify e := ReifyDirect.Reify base_type interp_base_type op e. - - (*Ltac reify_debug_level ::= constr:(2).*) - - Goal (base_type -> Type) -> False. - intro var. - let x := reifyf base_type interp_base_type op var 1%nat in pose x. - let x := Reify 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1). - let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. - let x := Reify (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))). - let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. - let x := Reify (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). - let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. - let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. - let x := Reify (fun x => let '(a, b) := (1, 1) in a + x)%nat in - unify x (fun var => Abs (fun x0 => - let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in - Let (Pair c1 c1) - (fun ab : var Tnat * var Tnat => Op Add (Pair (Var (fst ab)) (Var x0))))). - Abort. -End Direct. - -Module Exact. - Export ReifyExact. - Import InputSyntax. - - Import ReifyDebugNotations. - - Inductive base_type := Tnat. - Definition interp_base_type (v : base_type) : Type := - match v with - | Tnat => nat - end. - Local Notation tnat := (Tbase Tnat). - Inductive op : flat_type base_type -> flat_type base_type -> Type := - | Add : op (Prod tnat tnat) tnat - | Mul : op (Prod tnat tnat) tnat. - Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst - := match f with - | Add => fun xy => fst xy + snd xy - | Mul => fun xy => fst xy * snd xy - end%nat. - - Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I. - Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I. - Global Instance: reify type nat := Tnat. - - Ltac Reify' e := ReifyExact.Reify' base_type interp_base_type op e. - Ltac Reify e := ReifyExact.Reify base_type interp_base_type op e. - Ltac Reify_rhs := ReifyExact.Reify_rhs base_type interp_base_type op interp_op. - - (*Ltac reify_debug_level ::= constr:(2).*) - - Goal (flat_type base_type -> Type) -> False. - intro var. - let x := reifyf base_type interp_base_type op var 1%nat in pose x. - let x := Reify' 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1). - let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. - let x := Reify' (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))). - let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. - let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). - let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. - let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. - let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x. - let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in - unify x (fun var => Abs (fun x' => - let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in - MatchPair (tC:=tnat) (Pair c1 c1) - (fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))). - let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. - let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. - Abort. - - - Goal (0 = let x := 1+2 in x*3)%nat. - Reify_rhs. - Abort. - - Goal (0 = let x := 1 in let y := 2 in x * y)%nat. - Reify_rhs. - Abort. - - Import Linearize. - - Goal True. - let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in - pose (InlineConst (Linearize x)) as e. - vm_compute in e. - Abort. - - Definition example_expr : Syntax.Expr base_type interp_base_type op (Tbase Tnat). - Proof. - let x := Reify (let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in - exact x. - Defined. - - Definition base_type_eq_semidec_transparent : forall t1 t2, option (t1 = t2) - := fun t1 t2 => match t1, t2 with - | Tnat, Tnat => Some eq_refl - end. - Lemma base_type_eq_semidec_is_dec : forall t1 t2, - base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2. - Proof. - intros t1 t2; destruct t1, t2; simpl; intros; congruence. - Qed. - Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop - := fun x y => match x, y with - | Add, Add => Some trivial - | Add, _ => None - | Mul, Mul => Some trivial - | Mul, _ => None +Import ReifyDebugNotations. + +Inductive base_type := Tnat. +Definition interp_base_type (v : base_type) : Type := + match v with + | Tnat => nat + end. +Local Notation tnat := (Tbase Tnat). +Inductive op : flat_type base_type -> flat_type base_type -> Type := +| Add : op (Prod tnat tnat) tnat +| Mul : op (Prod tnat tnat) tnat. +Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst + := match f with + | Add => fun xy => fst xy + snd xy + | Mul => fun xy => fst xy * snd xy + end%nat. + +Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I. +Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I. +Global Instance: reify type nat := Tnat. + +Ltac Reify' e := Reify.Reify' base_type interp_base_type op e. +Ltac Reify e := Reify.Reify base_type interp_base_type op e. +Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op interp_op. + +(*Ltac reify_debug_level ::= constr:(2).*) + +Goal (flat_type base_type -> Type) -> False. + intro var. + let x := reifyf base_type interp_base_type op var 1%nat in pose x. + let x := Reify' 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1). + let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x. + let x := Reify' (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))). + let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x. + let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))). + let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x. + let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x. + let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x. + let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in + unify x (fun var => Abs (fun x' => + let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in + MatchPair (tC:=tnat) (Pair c1 c1) + (fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))). + let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. + let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x. +Abort. + + +Goal (0 = let x := 1+2 in x*3)%nat. + Reify_rhs. +Abort. + +Goal (0 = let x := 1 in let y := 2 in x * y)%nat. + Reify_rhs. +Abort. + +Import Linearize. + +Goal True. + let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in + pose (InlineConst (Linearize x)) as e. + vm_compute in e. +Abort. + +Definition example_expr : Syntax.Expr base_type interp_base_type op (Tbase Tnat). +Proof. + let x := Reify (let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in + exact x. +Defined. + +Definition base_type_eq_semidec_transparent : forall t1 t2, option (t1 = t2) + := fun t1 t2 => match t1, t2 with + | Tnat, Tnat => Some eq_refl end. - Lemma op_beq_bl t1 tR (x y : op t1 tR) - : match op_beq t1 tR x y with - | Some p => to_prop p - | None => False - end -> x = y. - Proof. - destruct x; simpl. - { refine match y with Add => _ | _ => _ end; tauto. } - { refine match y with Add => _ | _ => _ end; tauto. } - Qed. - - Lemma example_expr_wf : Wf _ _ _ example_expr. - Proof. - cbv beta delta [example_expr Wf]. - intros var1 var2. - repeat match goal with |- wf _ _ _ _ _ _ => constructor; intros end. - revert var1 var2. - vm_compute. - let Hwf := fresh "Hwf" in - lazymatch goal with - | [ |- forall var1' var2', @wff ?base_type ?interp_base_type ?op var1' var2' (@?G var1' var2') ?t (@?e1 var1') (@?e2 var2') ] - => intros var1 var2; pose proof (@reflect_wff base_type interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 (G var1 var2) t t (e1 _) (e2 _)) as Hwf - end. - revert Hwf; vm_compute. - intro Hwf; apply Hwf; clear Hwf. - tauto. - Qed. -End Exact. +Lemma base_type_eq_semidec_is_dec : forall t1 t2, + base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2. +Proof. + intros t1 t2; destruct t1, t2; simpl; intros; congruence. +Qed. +Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop + := fun x y => match x, y with + | Add, Add => Some trivial + | Add, _ => None + | Mul, Mul => Some trivial + | Mul, _ => None + end. +Lemma op_beq_bl t1 tR (x y : op t1 tR) + : match op_beq t1 tR x y with + | Some p => to_prop p + | None => False + end -> x = y. +Proof. + destruct x; simpl. + { refine match y with Add => _ | _ => _ end; tauto. } + { refine match y with Add => _ | _ => _ end; tauto. } +Qed. + +Lemma example_expr_wf : Wf _ _ _ example_expr. +Proof. + cbv beta delta [example_expr Wf]. + intros var1 var2. + repeat match goal with |- wf _ _ _ _ _ _ => constructor; intros end. + revert var1 var2. + vm_compute. + let Hwf := fresh "Hwf" in + lazymatch goal with + | [ |- forall var1' var2', @wff ?base_type ?interp_base_type ?op var1' var2' (@?G var1' var2') ?t (@?e1 var1') (@?e2 var2') ] + => intros var1 var2; pose proof (@reflect_wff base_type interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 (G var1 var2) t t (e1 _) (e2 _)) as Hwf + end. + revert Hwf; vm_compute. + intro Hwf; apply Hwf; clear Hwf. + tauto. +Qed. -- cgit v1.2.3 From 7aeb1054f646c838b109b27160e224191ac75bd4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 10:50:45 -0700 Subject: Fix for 8.4 compatibility --- src/Reflection/Syntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index a60f0d76f..d13eb1a42 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -64,7 +64,7 @@ Section language. Bind Scope expr_scope with exprf. Inductive expr : type -> Type := | Return {t} : exprf t -> expr t - | Abs {src dst} : (var src -> expr dst) -> expr (src -> dst). + | Abs {src dst} : (var src -> expr dst) -> expr (Arrow src dst). Bind Scope expr_scope with expr. Global Coercion Return : exprf >-> expr. Fixpoint smart_interp_flat_map {f g} -- cgit v1.2.3 From 876eb569ba2d315b600adf363ef8fcd4e528d746 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 12:22:53 -0700 Subject: More 8.4 fixes (apparently rebinding [->] doesn't work) --- src/Reflection/Syntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index d13eb1a42..8e4274559 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -164,7 +164,7 @@ Section language. | WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e') | WfAbs : forall A B G e e', (forall x x', @wf ((x == x') :: G) B (e x) (e' x')) - -> @wf G (A -> B) (Abs e) (Abs e'). + -> @wf G (Arrow A B) (Abs e) (Abs e'). End wf. Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2). -- cgit v1.2.3 From 71253e65b115f6332c544476bfe680a8d3f18568 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 14:15:18 -0700 Subject: Add comments to WfReflective, handle Expr In addition to much better documentation in WfReflective, we now also have a single tactic that handles goals of [Wf], on [Expr]. --- src/Reflection/Syntax.v | 10 ++ src/Reflection/TestCase.v | 28 ++-- src/Reflection/WfReflective.v | 376 ++++++++++++++++++++++++++++++++---------- 3 files changed, 312 insertions(+), 102 deletions(-) (limited to 'src') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 8e4274559..5e20426f7 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -67,6 +67,16 @@ Section language. | Abs {src dst} : (var src -> expr dst) -> expr (Arrow src dst). Bind Scope expr_scope with expr. Global Coercion Return : exprf >-> expr. + (** Sometimes, we want to deal with partially-interpreted + expressions, things like [prod (exprf A) (exprf B)] rather + than [exprf (Prod A B)], or like [prod (var A) (var B)] when + we start with the type [Prod A B]. These convenience + functions let us recurse on the type in only one place, and + replace one kind of pairing operator (be it [pair] or [Pair] + or anything else) with another kind, and simultaneously + mapping a function over the base values (e.g., [Var] (for + turning [var] into [exprf]) or [Const] (for turning + [interp_base_type] into [exprf])). *) Fixpoint smart_interp_flat_map {f g} (h : forall x, f x -> g (Tbase x)) (pair : forall A B, g A -> g B -> g (Prod A B)) diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 1db00b9cc..7511bb750 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -101,19 +101,19 @@ Proof. { refine match y with Add => _ | _ => _ end; tauto. } Qed. -Lemma example_expr_wf : Wf _ _ _ example_expr. +Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl. + +Lemma example_expr_wf_slow : Wf _ _ _ example_expr. Proof. - cbv beta delta [example_expr Wf]. - intros var1 var2. - repeat match goal with |- wf _ _ _ _ _ _ => constructor; intros end. - revert var1 var2. - vm_compute. - let Hwf := fresh "Hwf" in - lazymatch goal with - | [ |- forall var1' var2', @wff ?base_type ?interp_base_type ?op var1' var2' (@?G var1' var2') ?t (@?e1 var1') (@?e2 var2') ] - => intros var1 var2; pose proof (@reflect_wff base_type interp_base_type base_type_eq_semidec_transparent base_type_eq_semidec_is_dec op op_beq op_beq_bl var1 var2 (G var1 var2) t t (e1 _) (e2 _)) as Hwf - end. - revert Hwf; vm_compute. - intro Hwf; apply Hwf; clear Hwf. - tauto. + Time (vm_compute; intros; + repeat match goal with + | [ |- wf _ _ _ _ _ _ ] => constructor; intros + | [ |- wff _ _ _ _ _ _ ] => constructor; intros + | [ |- List.In _ _ ] => vm_compute + | [ |- ?x = ?x \/ _ ] => left; reflexivity + | [ |- ?x = ?y \/ _ ] => right + end). (* 0.036 s *) Qed. + +Lemma example_expr_wf : Wf _ _ _ example_expr. +Proof. Time reflect_Wf. (* 0.008 s *) Qed. diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v index c34acfb24..35bdf140c 100644 --- a/src/Reflection/WfReflective.v +++ b/src/Reflection/WfReflective.v @@ -1,47 +1,85 @@ -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. +(** * A reflective Version of [Wf] proofs *) +(** Because every constructor of [Syntax.wff] stores the syntax tree + being proven well-formed, a proof that a syntax tree is + well-formed is quadratic in the size of the syntax tree. (Tacking + an extra term on to the head of the syntax tree requires an extra + constructor of [Syntax.wff], and that constructor stores the + entirety of the new syntax tree.) + + In practice, this makes proving well-formedness of large trees + very slow. To remedy this, we provide an alternative type + ([reflect_wffT]) that implies [Syntax.wff], but is only linear in + the size of the syntax tree, with a coefficient less than 1. + + The idea is that, since we already know the syntax-tree arguments + to the constructors (and, moreover, already fully know the shape + of the [Syntax.wff] proof, because it will exactly match the shape + of the syntax tree), the proof doesn't have to store any of that + information. It only has to store the genuinely new information + in [Syntax.wff], namely, that the constants don't depend on the + [var] argument (i.e., that the constants in the same location in + the two expressions are equal), and that there are no free nor + mismatched variables (i.e., that the variables in the same + location in the two expressions are in the relevant list of + binders). We can make the further optimization of storing the + location in the list of each binder, so that all that's left to + verify is that the locations line up correctly. + + Since there is no way to assign list locations (De Bruijn indices) + after the fact (that is, once we have an [exprf var t] rather than + an [Expr t]), we instead start from an expression where [var] is + enriched with De Bruijn indices, and talk about [Syntax.wff] of + that expression stripped of its De Bruijn indices. Since this + procedure is only expected to work on concrete syntax trees, we + will be able to simply check by unification to check that + stripping the indices results in the term that we started with. -Inductive pointed_Prop := trivial | inject (_ : Prop). -Definition and_pointed_Prop (x y : pointed_Prop) : pointed_Prop - := match x, y with - | trivial, trivial => trivial - | trivial, inject p => inject p - | inject p, trivial => inject p - | inject p, inject q => inject (p /\ q) - end. -Definition to_prop (x : pointed_Prop) : Prop - := match x with - | trivial => True - | inject p => p - end. + The interface of this file is that, to prove a [Syntax.Wf] goal, + you invoke the tactic [reflect_Wf base_type_eq_semidec_is_dec + op_beq_bl], where: -Local Infix "/\" := and_pointed_Prop : type_scope. + - [base_type_eq_semidec_is_dec : forall t1 t2, + base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2] for + some [base_type_eq_semidec_transparent : forall t1 t2 : + base_type_code, option (t1 = t2)], and + + - [op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) + -> x = y] for some [op_beq : forall t1 tR, op t1 tR -> op t1 tR + -> option pointed_Prop] *) + +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 Export Crypto.Util.PointedProp. (* export for the [bool >-> option pointed_Prop] coercion *) +Require Export Crypto.Util.FixCoqMistakes. -Definition f_equal2 {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H : x1 = y1) - := match H in (_ = y) return (x2 = y2 -> f x1 x2 = f y y2) with - | eq_refl => - fun H0 : x2 = y2 => - match H0 in (_ = y) return (f x1 x2 = f x1 y) with - | eq_refl => eq_refl - end - end. Section language. + (** To be able to optimize away so much of the [Syntax.wff] proof, + we must be able to decide a few things: equality of base types, + and equality of operator codes. Since we will be casting across + the equality proofs of base types, we require that this + semi-decider give transparent proofs. (This requirement is not + enforced, but it will block [vm_compute] when trying to use the + lemma in this file.) *) Context (base_type_code : Type). Context (interp_base_type : base_type_code -> Type). Context (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)). Context (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2). Context (op : flat_type base_type_code -> flat_type base_type_code -> Type). + (** In practice, semi-deciding equality of operators should either + return [Some trivial] or [None], and not make use of the + generality of [pointed_Prop]. However, we need to use + [pointed_Prop] internally because we need to talk about equality + of things of type [var t], for [var : base_type_code -> Type]. + It does not hurt to allow extra generality in [op_beq]. *) Context (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop). - Context (op_beq_bl : forall t1 tR x y, match op_beq t1 tR x y with - | Some p => to_prop p - | _ => False - end -> x = y). + Context (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y). Context {var1 var2 : base_type_code -> Type}. Local Notation eP := (fun t => var1 (fst t) * var2 (snd t))%type (only parsing). + (* convenience notations that fill in some arguments used across the section *) Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). Let Tbase := @Tbase base_type_code. @@ -49,21 +87,17 @@ Section language. 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). + Local Notation expr := (@expr base_type_code interp_base_type op). - (*Fixpoint eq_interp_flat_type (t1 t2 : flat_type) - : interp_flat_type t1 -> interp_flat_type t2 -> option pointed_Prop - := match t1, t2 return interp_flat_type t1 -> interp_flat_type t2 -> option _ with - | Prod A B, Prod A' B' - => fun x y => match @eq_interp_flat_type A A' (fst x) (fst y), - @eq_interp_flat_type B B' (snd x) (snd y) with - | Some p, Some q => Some (p /\ q) - | _, _ => None - end - | Prod _ _, _ => fun _ _ => None - | Syntax.Tbase t1, Syntax.Tbase t2 - => fun x y => base_type_eq_and_cast t1 t2 x y (*Some (exists pf : t1 = t2, eq_rect _ interp_base_type x _ pf = y)*) - | Syntax.Tbase _, _ => fun _ _ => None - end.*) + Local Ltac inversion_base_type_code_step := + match goal with + | [ H : ?x = ?x :> base_type_code |- _ ] + => assert (H = eq_refl) by eapply UIP_dec, dec_rel_of_semidec_rel, base_type_eq_semidec_is_dec; subst H + | [ H : ?x = ?y :> base_type_code |- _ ] => subst x || subst y + end. + Local Ltac inversion_base_type_code := repeat inversion_base_type_code_step. + + (* lift [base_type_eq_semidec_transparent] across [flat_type] *) Fixpoint flat_type_eq_semidec_transparent (t1 t2 : flat_type) : option (t1 = t2) := match t1, t2 return option (t1 = t2) with | Syntax.Tbase t1, Syntax.Tbase t2 @@ -77,6 +111,41 @@ Section language. end | Prod _ _, _ => None end. + Fixpoint type_eq_semidec_transparent (t1 t2 : type) : option (t1 = t2) + := match t1, t2 return option (t1 = t2) with + | Syntax.Tflat t1, Syntax.Tflat t2 + => option_map (@f_equal _ _ (@Tflat _) _ _) + (flat_type_eq_semidec_transparent t1 t2) + | Syntax.Tflat _, _ => None + | Arrow A B, Arrow A' B' + => match base_type_eq_semidec_transparent A A', type_eq_semidec_transparent B B' with + | Some p, Some q => Some (f_equal2 (@Arrow base_type_code) p q) + | _, _ => None + end + | Arrow _ _, _ => None + end. + Lemma base_type_eq_semidec_transparent_refl t : base_type_eq_semidec_transparent t t = Some eq_refl. + Proof. + clear -base_type_eq_semidec_is_dec. + pose proof (base_type_eq_semidec_is_dec t t). + destruct (base_type_eq_semidec_transparent t t); intros; try intuition congruence. + inversion_base_type_code; reflexivity. + Qed. + Lemma flat_type_eq_semidec_transparent_refl t : flat_type_eq_semidec_transparent t t = Some eq_refl. + Proof. + clear -base_type_eq_semidec_is_dec. + induction t as [t | A B IHt]; simpl. + { rewrite base_type_eq_semidec_transparent_refl; reflexivity. } + { rewrite_hyp !*; reflexivity. } + Qed. + Lemma type_eq_semidec_transparent_refl t : type_eq_semidec_transparent t t = Some eq_refl. + Proof. + clear -base_type_eq_semidec_is_dec. + induction t as [t | A B IHt]; simpl. + { rewrite flat_type_eq_semidec_transparent_refl; reflexivity. } + { rewrite base_type_eq_semidec_transparent_refl; rewrite_hyp !*; reflexivity. } + Qed. + Definition op_beq' t1 tR t1' tR' (x : op t1 tR) (y : op t1' tR') : option pointed_Prop := match flat_type_eq_semidec_transparent t1 t1', flat_type_eq_semidec_transparent tR tR' with | Some p, Some q @@ -86,16 +155,44 @@ Section language. | _, _ => None end. - Definition eq_type_and_var : sigT eP -> sigT eP -> option pointed_Prop - := fun x y => - let 'existT (t1, t2) (a, b) := x in - let 'existT (t1', t2') (a', b') := y in - match base_type_eq_semidec_transparent t1 t1', base_type_eq_semidec_transparent t2 t2' with - | Some p, Some q - => Some (inject (and (eq_rect _ var1 a _ p = a') (eq_rect _ var2 b _ q = b'))) - | _, _ => None - end. + (** While [Syntax.wff] is parameterized over a list of [sigT (fun t + => var1 t * var2 t)], it is simpler here to make everything + heterogenous, rather than trying to mix homogenous and + heterogenous things.† Thus we parameterize our [reflect_wffT] + over a list of [sigT (fun t => var1 (fst t) * var2 (snd t))], + and write a function ([duplicate_type]) that turns the former + into the latter. + + † This is an instance of the general theme that abstraction + barriers are important. Here we enforce the abstraction + barrier that our input decision procedures are homogenous, but + all of our internal code is strictly heterogenous. This + allows us to contain the conversions between homogenous and + heterogenous code to a few functions: [op_beq'], + [eq_type_and_var], [eq_type_and_const], and to the statement + about [Syntax.wff] itself. *) + + Definition eq_semidec_and_gen {T} (semidec : forall x y : T, option (x = y)) + (t t' : T) (f : T -> Type) (x : f t) (x' : f t') + : option pointed_Prop + := match semidec t t' with + | Some p + => Some (inject (eq_rect _ f x _ p = x')) + | None => None + end. + (* Here is where we use the generality of [pointed_Prop], to say + that two things of type [var1] are equal, and two things of type + [var2] are equal. *) + Definition eq_type_and_var : sigT eP -> sigT eP -> option pointed_Prop + := fun x y => (eq_semidec_and_gen + base_type_eq_semidec_transparent _ _ var1 (fst (projT2 x)) (fst (projT2 y)) + /\ eq_semidec_and_gen + base_type_eq_semidec_transparent _ _ var2 (snd (projT2 x)) (snd (projT2 y)))%option_pointed_prop. + Definition eq_type_and_const (t t' : flat_type) (x : interp_flat_type t) (y : interp_flat_type t') + : option pointed_Prop + := eq_semidec_and_gen + flat_type_eq_semidec_transparent _ _ interp_flat_type x y. Definition duplicate_type (ls : list (sigT (fun t => var1 t * var2 t)%type)) : list (sigT eP) := List.map (fun v => existT eP (projT1 v, projT1 v) (projT2 v)) ls. @@ -106,35 +203,21 @@ Section language. Lemma duplicate_type_length ls : List.length (duplicate_type ls) = List.length ls. Proof. apply List.map_length. Qed. - (** TODO: Clean up this proof *) - Lemma base_type_eq_dec : forall t1 t2 : base_type_code, {t1 = t2} + {t1 <> t2}. - Proof. - intros t1 t2; destruct (base_type_eq_semidec_transparent t1 t2) eqn:H; - [ left; assumption | right; auto using base_type_eq_semidec_is_dec ]. - Qed. Lemma duplicae_type_in t v ls : List.In (existT _ (t, t) v) (duplicate_type ls) -> List.In (existT _ t v) ls. Proof. - unfold duplicate_type; intro H. - apply List.in_map_iff in H. - destruct H as [ [t' ?] [? ?] ]. - simpl in *. - inversion_sigma; subst. - match goal with H : _ |- _ => generalize (path_prod_eta H) end. - let x := match goal with |- ?x = _ -> _ => x end in - generalize (fst_path x); generalize (snd_path x); simpl. - intro; subst; intro H'; intros; subst. - assert (H' = eq_refl) by apply UIP_dec, base_type_eq_dec. - subst; simpl; assumption. + unfold duplicate_type; rewrite List.in_map_iff. + intros [ [? ?] [? ?] ]. + inversion_sigma; inversion_prod; inversion_base_type_code; subst; simpl. + assumption. Qed. Lemma duplicate_type_not_in G t t0 v (H : base_type_eq_semidec_transparent t t0 = None) : ~List.In (existT _ (t, t0) v) (duplicate_type G). Proof. apply base_type_eq_semidec_is_dec in H. - clear -H. - intro H'. - induction G as [|? ? IHG]; simpl in *; try tauto. - destruct H'; intuition eauto; congruence. + clear -H; intro H'. + induction G as [|? ? IHG]; simpl in *; destruct H'; + intuition; congruence. Qed. Definition preflatten_binding_list2 t1 t2 : option (forall (x : interp_flat_type_gen var1 t1) (y : interp_flat_type_gen var2 t2), list (sigT (fun t => var1 t * var2 t)%type)) @@ -147,6 +230,7 @@ Section language. end. 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} : 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 @@ -174,15 +258,23 @@ Section language. rewrite_hyp <- ?*; reflexivity. Qed. + (* This function strips De Bruijn indices from expressions *) Fixpoint unnatize_exprf {var t} (base : nat) (e : @exprf (fun t => nat * var t)%type t) : @exprf var t := match e in @Syntax.exprf _ _ _ _ t return exprf t with | Const _ x => Const x | Var _ x => Var (snd x) | Op _ _ op args => Op op (@unnatize_exprf _ _ base args) - | Let _ ex _ eC => Let (@unnatize_exprf _ _ base ex) (fun x => let v := natize_interp_flat_type_gen base x in - @unnatize_exprf _ _ (fst v) (eC (snd v))) + | Let _ ex _ eC => Let (@unnatize_exprf _ _ base ex) + (fun x => let v := natize_interp_flat_type_gen base x in + @unnatize_exprf _ _ (fst v) (eC (snd v))) | Pair _ x _ y => Pair (@unnatize_exprf _ _ base x) (@unnatize_exprf _ _ base y) end. + Fixpoint unnatize_expr {var t} (base : nat) (e : @expr (fun t => nat * var t)%type t) : @expr var t + := match e in @Syntax.expr _ _ _ _ t return expr t with + | Return _ x => unnatize_exprf base x + | Abs tx tR f => Abs (fun x : var tx => let v := natize_interp_flat_type_gen (t:=tx) base x in + @unnatize_expr _ _ (fst v) (f (snd v))) + end. Fixpoint reflect_wffT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) {t1 t2 : flat_type} @@ -204,7 +296,7 @@ Section language. | Var _ _, _ => None | Op t1 tR op args, Op t1' tR' op' args' => match @reflect_wffT G t1 t1' args args', op_beq' t1 tR t1' tR' op op' with - | Some p, Some q => Some (p /\ q) + | Some p, Some q => Some (p /\ q)%pointed_prop | _, _ => None end | Op _ _ _ _, _ => None @@ -227,7 +319,31 @@ Section language. | _, _ => None end | Pair _ _ _ _, _ => None - end. + end%pointed_prop. + + Fixpoint reflect_wfT (G : list (sigT (fun t => var1 (fst t) * var2 (snd t))%type)) + {t1 t2 : type} + (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2) + {struct e1} + : option pointed_Prop + := match e1, e2 return option _ with + | Return _ x, Return _ y + => reflect_wffT G x y + | Return _ _, _ => None + | Abs tx tR f, Abs tx' tR' f' + => match @flatten_binding_list2 tx tx', type_eq_semidec_transparent tR tR' with + | Some G0, Some _ + => Some (inject (forall (x : interp_flat_type_gen var1 tx) (x' : interp_flat_type_gen var2 tx'), + match @reflect_wfT (G0 x x' ++ G)%list _ _ + (f (snd (natize_interp_flat_type_gen (List.length G) x))) + (f' (snd (natize_interp_flat_type_gen (List.length G) x'))) with + | Some p => to_prop p + | None => False + end)) + | _, _ => None + end + | Abs _ _ _, _ => None + end%pointed_prop. Local Ltac handle_op_beq_correct := repeat match goal with @@ -237,18 +353,23 @@ Section language. end. Local Ltac t_step := match goal with - | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, preflatten_binding_list2, option_map in * + | _ => progress unfold eq_type_and_var, op_beq', flatten_binding_list2, preflatten_binding_list2, option_map, and_option_pointed_Prop, eq_semidec_and_gen in * | _ => progress simpl in * | _ => progress break_match | _ => progress subst | _ => progress inversion_option + | _ => progress inversion_pointed_Prop | _ => congruence | _ => tauto | _ => progress intros | _ => progress handle_op_beq_correct | _ => progress specialize_by tauto + | [ v : sigT _ |- _ ] => destruct v + | [ v : prod _ _ |- _ ] => destruct v | [ H : forall x x', _ |- wff _ _ _ (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ] => specialize (H x1 x2) + | [ H : forall x x', _ |- wf _ _ _ (existT _ _ (?x1, ?x2) :: _)%list _ _ ] + => specialize (H x1 x2) | [ H : and _ _ |- _ ] => destruct H | [ H : context[duplicate_type (_ ++ _)%list] |- _ ] => rewrite duplicate_type_app in H @@ -258,11 +379,14 @@ Section language. => rewrite List.app_length in H | [ |- wff _ _ _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ] => erewrite length_natize_interp_flat_type_gen1, length_natize_interp_flat_type_gen2; eassumption + | [ |- wf _ _ _ _ (unnatize_exprf (fst _) _) (unnatize_exprf (fst _) _) ] + => erewrite length_natize_interp_flat_type_gen1, length_natize_interp_flat_type_gen2; eassumption + | [ |- @wf _ _ _ _ _ _ (Syntax.Tflat _ _) _ _ ] => constructor + | [ |- @wf _ _ _ _ _ _ _ (Syntax.Abs _) (Syntax.Abs _) ] => constructor | [ H : base_type_eq_semidec_transparent _ _ = None |- False ] => eapply duplicate_type_not_in; eassumption | [ H : List.nth_error _ _ = Some _ |- _ ] => apply List.nth_error_In in H | [ H : List.In _ (duplicate_type _) |- _ ] => apply duplicae_type_in in H | [ H : context[match _ with _ => _ end] |- _ ] => revert H; progress break_match - | [ H : inject _ = inject _ |- _ ] => inversion H; clear H | [ |- wff _ _ _ _ _ _ ] => constructor | _ => progress unfold and_pointed_Prop in * end. @@ -271,17 +395,15 @@ Section language. {t1 t2 : flat_type} (e1 : @exprf (fun t => nat * var1 t)%type t1) (e2 : @exprf (fun t => nat * var2 t)%type t2) {struct e1} - : match reflect_wffT (duplicate_type G) e1 e2 with - | Some p => to_prop p - | None => False - end - -> match flat_type_eq_semidec_transparent t1 t2 with - | Some p => @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) - | None => False - end. + : match reflect_wffT (duplicate_type G) e1 e2, flat_type_eq_semidec_transparent t1 t2 with + | Some reflective_obligation, Some p + => to_prop reflective_obligation + -> @wff base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ exprf (unnatize_exprf (List.length G) e1) _ p) (unnatize_exprf (List.length G) e2) + | _, _ => True + end. Proof. destruct e1 as [ | | ? ? ? args | tx ex tC eC | ? ex ? ey ], - e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ intros [] ]; + e2 as [ | | ? ? ? args' | tx' ex' tC' eC' | ? ex' ? ey' ]; simpl; try solve [ exact I ]; [ clear reflect_wff | clear reflect_wff | specialize (reflect_wff G _ _ args args') @@ -303,4 +425,82 @@ Section language. { t. } { t. } Qed. + Fixpoint reflect_wf (G : list (sigT (fun t => var1 t * var2 t)%type)) + {t1 t2 : type} + (e1 : @expr (fun t => nat * var1 t)%type t1) (e2 : @expr (fun t => nat * var2 t)%type t2) + : match reflect_wfT (duplicate_type G) e1 e2, type_eq_semidec_transparent t1 t2 with + | Some reflective_obligation, Some p + => to_prop reflective_obligation + -> @wf base_type_code interp_base_type op var1 var2 G t2 (eq_rect _ expr (unnatize_expr (List.length G) e1) _ p) (unnatize_expr (List.length G) e2) + | _, _ => True + end. + Proof. + destruct e1 as [ t1 e1 | tx tR f ], + e2 as [ t2 e2 | tx' tR' f' ]; simpl; try solve [ exact I ]; + [ clear reflect_wf; + pose proof (@reflect_wff G t1 t2 e1 e2) + | pose proof (fun x x' + => match preflatten_binding_list2 tx tx' as v return match v with Some _ => _ | None => True end with + | Some G0 + => reflect_wf + (G0 x x' ++ G)%list _ _ + (f (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x))) + (f' (snd (natize_interp_flat_type_gen (length (duplicate_type G)) x'))) + | None => I + end); + clear reflect_wf ]. + { t. } + { t. } + Qed. End language. + +Section Wf. + Context (base_type_code : Type) + (interp_base_type : base_type_code -> Type) + (base_type_eq_semidec_transparent : forall t1 t2 : base_type_code, option (t1 = t2)) + (base_type_eq_semidec_is_dec : forall t1 t2, base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2) + (op : flat_type base_type_code -> flat_type base_type_code -> Type) + (op_beq : forall t1 tR, op t1 tR -> op t1 tR -> option pointed_Prop) + (op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y) + {t : type base_type_code} + (e : @Expr base_type_code interp_base_type op t). + + (** Leads to smaller proofs, but is less generally applicable *) + Theorem reflect_Wf_unnatize + : (forall var1 var2, + prop_of_option (@reflect_wfT base_type_code interp_base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _))) + -> Wf _ _ _ (fun var => unnatize_expr base_type_code interp_base_type op 0 (e (fun t => (nat * var t)%type))). + 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. + edestruct reflect_wfT; simpl in *; tauto. + Qed. + + (** Leads to larger proofs (an extra constant factor which is the + size of the expression tree), but more generally applicable *) + Theorem reflect_Wf + : (forall var1 var2, + unnatize_expr base_type_code interp_base_type op 0 (e (fun t => (nat * var1 t)%type)) = e _ + /\ prop_of_option (@reflect_wfT base_type_code interp_base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil t t (e _) (e _))) + -> Wf _ _ _ e. + Proof. + intros H var1 var2. + rewrite <- (proj1 (H var1 var2)), <- (proj1 (H var2 var2)). + apply reflect_Wf_unnatize, H. + Qed. +End Wf. + + +Ltac generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := + lazymatch goal with + | [ |- @Wf ?base_type_code ?interp_base_type ?op ?t ?e ] + => generalize (@reflect_Wf_unnatize base_type_code interp_base_type _ base_type_eq_semidec_is_dec op _ op_beq_bl t e) + end. +Ltac use_reflect_Wf := vm_compute; let H := fresh in intro H; apply H; clear H. +Ltac fin_reflect_Wf := repeat constructor. +(** The tactic [reflect_Wf] is the main tactic of this file, used to + prove [Syntax.Wf] goals *) +Ltac reflect_Wf base_type_eq_semidec_is_dec op_beq_bl := + generalize_reflect_Wf base_type_eq_semidec_is_dec op_beq_bl; + use_reflect_Wf; fin_reflect_Wf. -- 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') 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 From 03625062aadec037ef8738d9655ef69089a812f9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 15:31:12 -0700 Subject: Update comment with Andres' suggestion --- src/Reflection/Syntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 5e20426f7..d14705979 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -54,7 +54,7 @@ Section language. Section expr. Context {var : base_type_code -> Type}. - (** N.B. [Let] destructures pairs *) + (** N.B. [Let] binds the components of a pair to separate variables, and does so recursively *) Inductive exprf : flat_type -> Type := | Const {t : flat_type} : interp_type t -> exprf t | Var {t} : var t -> exprf t -- cgit v1.2.3