add EGlobal/RGlobal for CoreVars whose binder we cannot see

[coq-hetmet.git] / src / HaskProof.v

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 7ae3462..354e559 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -14,8 +14,9 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskCoreLiterals.
+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
@@ -40,8 +41,8 @@ Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
   Tree ??(LeveledHaskType Γ ★) ->
   UJudg Γ Δ.
   Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
-  Notation "'ext_tree_left'"    := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (ctx,,t)  s end).
-  Notation "'ext_tree_right'"   := (fun ctx j => match j with mkUJudg t s => mkUJudg _ _ (t,,ctx) s end).
+  Definition ext_tree_left  {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
+  Definition ext_tree_right {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
 
 (* we can turn a UJudg into a Judg by simply internalizing the index *)
 Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
@@ -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 Γ Δ (σ₁∼∼∼σ₂) ->