From 2bce2a84478ef19d21709bf3247833ee6b2e8866 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 2 Feb 2017 12:46:51 -0500 Subject: Reorder Reflection.Z.Syntax This puts all the definitions first, and then puts the interpretations after that --- src/Reflection/Z/Syntax.v | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index afdd87ba9..288876dc9 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -7,15 +7,8 @@ Export Syntax.Notations. Local Set Boolean Equality Schemes. Local Set Decidable Equality Schemes. Inductive base_type := TZ. -Definition interp_base_type (v : base_type) : Type := - match v with - | TZ => Z - end. Local Notation tZ := (Tbase TZ). -Local Notation eta x := (fst x, snd x). -Local Notation eta3 x := (eta (fst x), snd x). -Local Notation eta4 x := (eta3 (fst x), snd x). Inductive op : flat_type base_type -> flat_type base_type -> Type := | OpConst (z : Z) : op Unit tZ @@ -30,6 +23,15 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type := | Cmovne : op (tZ * tZ * tZ * tZ) tZ | Cmovle : op (tZ * tZ * tZ * tZ) tZ. +Definition interp_base_type (v : base_type) : Type := + match v with + | TZ => Z + end. + +Local Notation eta x := (fst x, snd x). +Local Notation eta3 x := (eta (fst x), snd x). +Local Notation eta4 x := (eta3 (fst x), snd x). + Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst := match f in op src dst return interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst with | OpConst v => fun _ => v -- cgit v1.2.3