From e4e860f8b10a1b8ce1ab207f12c7ef50e36332c4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Sep 2016 11:50:23 -0700 Subject: Key on the head of the operation in reification Hopefully fixes #62 Also, don't export InputSyntax in Reify --- src/Reflection/Reify.v | 5 +++-- src/Reflection/TestCase.v | 6 +++--- 2 files changed, 6 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/Reflection/Reify.v b/src/Reflection/Reify.v index 58ebd5da5..d5d2b219e 100644 --- a/src/Reflection/Reify.v +++ b/src/Reflection/Reify.v @@ -3,7 +3,7 @@ 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.Reflection.InputSyntax. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. @@ -134,7 +134,8 @@ Ltac reifyf base_type_code interp_base_type op var e := 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 op_head := head x in + let r := constr:(_ : reify_op op op_head _ _) in let t := type of r in constr:(op_info t) | _ => let c := mkConst t x in diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index 17580aa5d..457c9fcfe 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -26,9 +26,9 @@ Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base | Sub => 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: forall x y, reify_op op (x - y)%nat 2 Sub := fun _ _ => I. +Global Instance: reify_op op plus 2 Add := I. +Global Instance: reify_op op mult 2 Mul := I. +Global Instance: reify_op op minus 2 Sub := I. Global Instance: reify type nat := Tnat. Ltac Reify' e := Reify.Reify' base_type interp_base_type op e. -- cgit v1.2.3