From 55b011d85e1477a5b591fa74cc65316b9a49364e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 16 May 2017 23:07:25 -0400
Subject: Flip argument order on interp for easier Proper lemmas

---
 src/Compilers/Named/Syntax.v        | 18 +++++++++---------
 src/Compilers/Named/WfInterp.v      |  4 ++--
 src/Specific/FancyMachine256/Core.v |  2 +-
 3 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'src')

diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v
index 34ba1f48f..4cc4ccbf2 100644
--- a/src/Compilers/Named/Syntax.v
+++ b/src/Compilers/Named/Syntax.v
@@ -41,30 +41,30 @@ Module Export Named.
               (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
 
       Fixpoint interpf
-               (ctx : Context) {t} (e : exprf t)
+               {t} (ctx : Context) (e : exprf t)
         : option (interp_flat_type t)
         := match e in exprf t return option (interp_flat_type t) with
            | Var t' x => lookupb t' ctx x
            | TT => Some tt
            | Pair _ ex _ ey
-             => match @interpf ctx _ ex, @interpf ctx _ ey with
+             => match @interpf _ ctx ex, @interpf _ ctx ey with
                 | Some xv, Some yv => Some (xv, yv)%core
                 | None, _ | _, None => None
                 end
            | Op _ _ opc args
-             => option_map (@interp_op _ _ opc) (@interpf ctx _ args)
+             => option_map (@interp_op _ _ opc) (@interpf _ ctx args)
            | LetIn _ n ex _ eC
-             => match @interpf ctx _ ex with
+             => match @interpf _ ctx ex with
                 | Some xv
                   => dlet x := xv in
-                     @interpf (extend ctx n x) _ eC
+                     @interpf _ (extend ctx n x) eC
                 | None => None
                 end
            end.
 
-      Definition interp (ctx : Context) {t} (e : expr t)
+      Definition interp {t} (ctx : Context) (e : expr t)
         : interp_flat_type (domain t) -> option (interp_flat_type (codomain t))
-        := fun v => @interpf (extend ctx (Abs_name e) v) _ (invert_Abs e).
+        := fun v => @interpf _ (extend ctx (Abs_name e) v) (invert_Abs e).
 
       Definition Interp {t} (e : expr t)
         : interp_flat_type (domain t) -> option (interp_flat_type (codomain t))
@@ -81,8 +81,8 @@ Global Arguments Pair {_ _ _ _} _ {_} _.
 Global Arguments Abs {_ _ _ _ _} _ _.
 Global Arguments invert_Abs {_ _ _ _} _.
 Global Arguments Abs_name {_ _ _ _} _.
-Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _.
-Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _.
+Global Arguments interpf {_ _ _ _ _ interp_op t ctx} _.
+Global Arguments interp {_ _ _ _ _ interp_op t ctx} _ _.
 Global Arguments Interp {_ _ _ _ _ interp_op t} _ _.
 
 Notation "'nlet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope.
diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v
index 580dcb438..e9cd8737c 100644
--- a/src/Compilers/Named/WfInterp.v
+++ b/src/Compilers/Named/WfInterp.v
@@ -15,7 +15,7 @@ Section language.
 
   Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t}
         (Hwf : prop_of_option (wff ctx e))
-    : @interpf base_type_code interp_base_type op Name Context interp_op ctx t e <> None.
+    : @interpf base_type_code interp_base_type op Name Context interp_op t ctx e <> None.
   Proof using Type.
     revert dependent ctx; induction e;
       repeat first [ progress intros
@@ -34,7 +34,7 @@ Section language.
   Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t}
         (Hwf : wf ctx e)
         v
-    : @interp base_type_code interp_base_type op Name Context interp_op ctx t e v <> None.
+    : @interp base_type_code interp_base_type op Name Context interp_op t ctx e v <> None.
   Proof using Type.
     destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto.
   Qed.
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index e28196f43..49d7a2b87 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -243,7 +243,7 @@ Section assemble.
   Definition DefaultAssembleSyntax {t} e := @AssembleSyntax t e (DefaultRegisters e).
 
   Definition Interp {t} e v
-    := invert_Some (@Named.interp base_type interp_base_type op Register RegisterContext interp_op empty t e v).
+    := invert_Some (@Named.Interp base_type interp_base_type op Register RegisterContext interp_op t e v).
 End assemble.
 
 Export Compilers.Named.Syntax.
-- 
cgit v1.2.3