diff options
author | 2016-09-07 14:34:22 -0700 | |
---|---|---|
committer | 2016-09-07 14:34:22 -0700 | |
commit | 780969cfd2655aec5dcdedf155d450aaf955e7d2 (patch) | |
tree | c96c8d3e2764cfed8e0969965364591239f12dd0 | |
parent | bb796b735c7804ebde4e843dfe980d8c9775d7ae (diff) |
Remove the need for coercions in well-typing of Reify
-rw-r--r-- | src/Reflection/Reify.v | 15 | ||||
-rw-r--r-- | src/Reflection/TestCase.v | 4 |
2 files changed, 6 insertions, 13 deletions
diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index d74dd673a..e202cc804 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -2,20 +2,12 @@ (** The reification procedure goes through [InputSyntax], which allows judgmental equality of the denotation of the reified term. *) Require Import Coq.Strings.String. -Require Crypto.Reflection.Syntax. -Require Crypto.Reflection.InputSyntax. +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.InputSyntax. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. -Module Export ReifyCoercions. - Global Coercion Syntax.Return : Syntax.exprf >-> Syntax.expr. - Global Coercion InputSyntax.Return : InputSyntax.exprf >-> InputSyntax.expr. - Global Coercion Syntax.Tflat : Syntax.flat_type >-> Syntax.type. -End ReifyCoercions. - -Import Syntax InputSyntax. - 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} _. @@ -224,7 +216,8 @@ Ltac reify_abs base_type_code interp_base_type op var e := (_ : 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 + let ret := reifyf_term x in + constr:(Return ret) end. Hint Extern 0 (reify_abs (@exprf ?base_type_code ?interp_base_type ?op ?var) ?e) diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 457c9fcfe..fd60e7906 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -40,9 +40,9 @@ Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op interp_op. 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 := Reify' 1%nat in unify x (fun var => Return (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' (1 + 1)%nat in unify x (fun var => Return (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. |