X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrong.v;h=f9d9f3d86d1b52419c245605a17b506625432b50;hp=d688c2f66cf8a1fd5eda4f5b53fa372af45160dd;hb=4ad68fe2894b35c21f2feb7b176d2b0f146ff6d3;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index d688c2f..f9d9f3d 100644
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -20,7 +20,6 @@ Section HaskStrong.
   Context `{EQD_VV:EqDecidable VV}.
 
   (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
-
   Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
   { scbwv_exprvars          :  vec VV (sac_numExprVars sac)
   ; scbwv_exprvars_distinct :  distinct (vec2list scbwv_exprvars)
@@ -28,12 +27,11 @@ Section HaskStrong.
   ; scbwv_ξ                 := fun ξ lev =>  update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
   }.
   Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
-  (*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
+  | EGlobal: forall Γ Δ ξ   (g:Global Γ) v lev,                                                      Expr Γ Δ ξ (g v @@ lev)
 
   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
@@ -63,6 +61,7 @@ Section HaskStrong.
                Expr Γ Δ ξ (tbranches @@ l)
 
   | ELetRec  : ∀ Γ Δ ξ l τ vars,
+    distinct (leaves (mapOptionTree (@fst _ _) vars)) ->
     let ξ' := update_ξ ξ l (leaves vars) in
     ELetRecBindings Γ Δ ξ'     l vars ->
     Expr            Γ Δ ξ' (τ@@l) ->
@@ -80,7 +79,7 @@ Section HaskStrong.
   Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
     match exp with
     | EVar  Γ' _ ξ' ev              => "var."+++ toString ev
-    | EGlobal Γ' _ ξ' t wev         => "global." +++ toString (wev:CoreVar)
+    | EGlobal Γ' _ ξ'   g v _       => "global." +++ toString (g:CoreVar)
     | ELam  Γ'   _ _ tv _ _ cv e    => "\("+++ toString cv +++":t) -> "+++ exprToString e
     | ELet  Γ' _ _ t _ _ ev e1 e2   => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
     | ELit  _ _ _ lit _             => "lit."+++toString lit
@@ -93,8 +92,8 @@ Section HaskStrong.
     | ECast Γ Δ ξ t1 t2 γ l e       => "cast ("+++exprToString e+++"):t2"
     | ETyLam _ _ _ k _ _ e          => "\@_ ->"+++ exprToString e
     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
-    | ECase Γ Δ ξ l tc tbranches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
-    | ELetRec _ _ _ _ _ vars elrb e => "letrec FIXME in " +++ exprToString e
+    | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
+    | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
     end.
   Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }.