From ff9fafbf161b4f12688d5986518be874d39ab3ee Mon Sep 17 00:00:00 2001
From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Wed, 16 Mar 2011 01:52:39 -0700
Subject: [PATCH] add EGlobal/RGlobal for CoreVars whose binder we cannot see

---
 src/HaskProof.v         |    2 ++
 src/HaskProofToLatex.v  |    1 +
 src/HaskStrong.v        |    4 ++++
 src/HaskStrongToProof.v |    9 +++++++++
 4 files changed, 16 insertions(+)

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 6474665..354e559 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -16,6 +16,7 @@ Require Import HaskKinds.
 Require Import HaskCoreTypes.
 Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
+Require Import HaskWeakVars.
 
 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
  * in any context of that shape.  Notice that the succedent contains a tree of types rather than a single type; think
@@ -90,6 +91,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 (* SystemFC rules *)
 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
+| RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 25e2523..015d02e 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -174,6 +174,7 @@ Section ToLatex.
       | RNote         _ _ _             => "Note"
       | RLit          _ _ _ _           => "Lit"
       | RVar          _ _ _ _           => "Var"
+      | RGlobal       _ _ _ _ _         => "Global"
       | RLam          _ _ _ _ _ _       => "Abs"
       | RCast         _ _ _ _ _ _ _     => "Cast"
       | RAbsT         _ _ _ _ _ _       => "AbsT"
diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 8efd0af..611a4c8 100644
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -31,6 +31,10 @@ Section HaskStrong.
   Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.
 
   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
+
+  (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
+  | EGlobal: ∀ Γ Δ ξ t,       WeakExprVar ->                                                         Expr Γ Δ ξ t
+
   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
   | EApp   : ∀ Γ Δ ξ t1 t2 l,        Expr Γ Δ ξ (t2--->t1 @@ l)   -> Expr Γ Δ ξ (t2 @@ l)         -> Expr Γ Δ ξ (t1 @@ l)
diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 1efc666..143be0b 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -69,6 +69,7 @@ Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with
+  | EGlobal  Γ Δ ξ _ _                            => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
@@ -585,6 +586,7 @@ Definition expr2proof  :
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with
+    | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 
@@ -630,6 +632,12 @@ Definition expr2proof  :
     end
 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 
+    destruct case_EGlobal.
+      apply nd_rule.
+      simpl.
+      destruct t as [t lev].
+      apply (RGlobal _ _ _ _ wev).
+
     destruct case_EVar.
       apply nd_rule.
       unfold mapOptionTree; simpl.
@@ -704,6 +712,7 @@ Definition expr2proof  :
       auto.
 
     destruct case_ENote.
+      destruct t.
       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.
-- 
1.7.10.4