abstract out the kind of environment classifiers (ECKind)

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

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 04e1055..122db2a 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,14 +10,13 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
 Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.

-Require Import HaskCoreTypes.

 Require Import HaskCoreVars.
 
 Open Scope string_scope.
 Require Import HaskCoreVars.
 
 Open Scope string_scope.

@@ -95,7 +94,7 @@ Notation " ` x " := (@fixkind _ x) (at level 100).
 
 Ltac matchThings T1 T2 S :=
   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
 
 Ltac matchThings T1 T2 S :=
   destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];

-   [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
+   [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].

 
 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
   intros.
 
 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
   intros.

@@ -116,7 +115,7 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 
 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
 
 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
   refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=

-  addErrorMessage ("weakTypeToType " +++ t)
+  addErrorMessage ("weakTypeToType " +++ toString t)

   match t with
     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
     | WTyCon      tc    => let case_WTyCon := tt    in _
   match t with
     | WFunTyCon         => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
     | WTyCon      tc    => let case_WTyCon := tt    in _

@@ -125,7 +124,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
     | WAppTy  t1 t2     => let case_WAppTy := tt    in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
     | WTyVarTy  v       => let case_WTyVarTy := tt  in φ v >>= fun v' => _
     | WForAllTy wtv t   => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _

-    | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
+    | WCodeTy ec tbody  => let case_WCodeTy := tt   in weakTypeToType _ φ tbody
+                                 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _

     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
       weakTypeToType _ φ t1 >>= fun t1' =>
       weakTypeToType _ φ t2 >>= fun t2' =>
     | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt  in
       weakTypeToType _ φ t1 >>= fun t1' =>
       weakTypeToType _ φ t2 >>= fun t2' =>

@@ -147,6 +147,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
         end
       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
   end ); clear weakTypeToType.
         end
       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
   end ); clear weakTypeToType.

+  apply ConcatenableString.

 
   destruct case_WTyVarTy.
     apply (addErrorMessage "case_WTyVarTy").
 
   destruct case_WTyVarTy.
     apply (addErrorMessage "case_WTyVarTy").

@@ -157,7 +158,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply (addErrorMessage "case_WAppTy").
     destruct t1' as  [k1' t1'].
     destruct t2' as [k2' t2'].
     apply (addErrorMessage "case_WAppTy").
     destruct t1' as  [k1' t1'].
     destruct t2' as [k2' t2'].

-    set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
+    set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
+      toString t2'+++" of kind "+++toString k2') as err.

     destruct k1';
       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
     destruct k1';
       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));

@@ -175,7 +177,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.

-    apply TyFunApp.
+    apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).

     apply lt'.
     apply X.
 
     apply lt'.
     apply X.
 

@@ -222,9 +224,6 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply h.
     Defined.
     
     apply h.
     Defined.
     

-
-Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
-

 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 Section StrongAltCon.
   Context (tc : TyCon)(dc:DataCon tc).
 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
 Section StrongAltCon.
   Context (tc : TyCon)(dc:DataCon tc).

@@ -260,7 +259,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine
 
 Definition mkStrongAltCon : @StrongAltCon tc.
   refine

-   {| sac_altcon      := DataAlt dc
+   {| sac_altcon      := WeakDataAlt dc

     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
     ; sac_ekinds      := dataConExKinds dc
     ; sac_numCoerVars := length (dataConCoerKinds dc)
     ; sac_numExprVars := length (dataConFieldTypes dc)
     ; sac_ekinds      := dataConExKinds dc

@@ -349,13 +348,13 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
   
 End StrongAltCon.
 
   
 End StrongAltCon.
 

-Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
+Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).

   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.
   set (eqd_dec tc tc') as eqpf; destruct eqpf;
     [ idtac
   destruct alt.
   set (c:DataCon _) as dc.
   set ((dataConTyCon c):TyCon) as tc' in *.
   set (eqd_dec tc tc') as eqpf; destruct eqpf;
     [ idtac

-      | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
+      | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.

   apply OK.
   eapply mkStrongAltConPlusJunk.
   simpl in *.
   apply OK.
   eapply mkStrongAltConPlusJunk.
   simpl in *.

@@ -363,14 +362,14 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP
 
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
 
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds  := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil

-                    ; sac_altcon := LitAlt h
+                    ; sac_altcon := WeakLitAlt h

                     |} |}.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
                     |} |}.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
   apply OK; refine {| sacpj_sac := {| 
                      sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil

-                      ; sac_altcon := DEFAULT |} |}.
+                      ; sac_altcon := WeakDEFAULT |} |}.

             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.
             intro; intro φ; apply φ.
             intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
             rewrite weakCK'_nil_inert. apply ψ.

@@ -402,13 +401,13 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex
   destruct τ' as [τ' l'].
   destruct (eqd_dec l l'); [ idtac
     | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
   destruct τ' as [τ' l'].
   destruct (eqd_dec l l'); [ idtac
     | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++

-                    "  got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
-                    "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
+                    "  got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
+                    "  wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")

     )) ].
   destruct (eqd_dec τ τ'); [ idtac
     | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
     )) ].
   destruct (eqd_dec τ τ'); [ idtac
     | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++

-                    "  got: " +++τ+++eol+++
-                    "  wanted: "+++τ'
+                    "  got: " +++toString τ+++eol+++
+                    "  wanted: "+++toString τ'

     )) ].
   subst.
   apply OK.
     )) ].
   subst.
   apply OK.

@@ -455,12 +454,87 @@ match lk as LK return ???(IList Kind (HaskType Γ) LK) with
               end
 end.
 
               end
 end.
 

+Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
+  match vars with
+    | nil => ig
+    | v::vars' =>
+      fun v' =>
+        if eqd_dec v v'
+          then false
+            else update_ig ig vars' v'
+  end.
+
+(* does the specified variable occur free in the expression? *)
+Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
+  match me with
+    | WELit    _        => false
+    | WEVar    cv       => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
+    | WECast   e co     =>                            doesWeakVarOccur wev e
+    | WENote   n e      =>                            doesWeakVarOccur wev e
+    | WETyApp  e t      =>                            doesWeakVarOccur wev e
+    | WECoApp  e co     =>                            doesWeakVarOccur wev e
+    | WEBrak _ ec e _   =>                            doesWeakVarOccur wev e
+    | WEEsc  _ ec e _   =>                            doesWeakVarOccur wev e
+    | WECSP  _ ec e _   =>                            doesWeakVarOccur wev e
+    | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
+    | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+    | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+    | WETyLam  cv e     => doesWeakVarOccur wev e
+    | WECoLam  cv e     => doesWeakVarOccur wev e
+    | WECase vscrut escrut tbranches tc avars alts =>
+      doesWeakVarOccur wev escrut ||
+      if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
+        ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
+          match alts with
+            | T_Leaf  None                                         => false
+            | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
+            | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
+            | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
+            | T_Branch b1 b2                                       => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
+          end) alts)
+    | WELetRec mlr e =>
+      doesWeakVarOccur wev e ||
+      (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
+      match mlr with
+        | T_Leaf None          => false
+        | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+        | T_Branch b1 b2       => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
+      end) mlr
+  end.
+Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
+  (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool := 
+  match alts with
+    | T_Leaf  None                                             => false
+    | T_Leaf (Some (WeakDEFAULT,_,_,_,e))                      => doesWeakVarOccur wev e
+    | T_Leaf (Some (WeakLitAlt lit,_,_,_,e))                   => doesWeakVarOccur wev e
+    | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e))  => doesWeakVarOccur wev e  (* FIXME!!! *)
+    | T_Branch b1 b2                                           => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
+  end.
+
+Definition checkDistinct :
+  forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
+  intros.
+  set (distinct_decidable lv) as q.
+  destruct q.
+  exact (OK d).
+  exact (Error "checkDistinct failed").
+  Defined.
+
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+  refine {| glob_kinds := nil |}.
+  apply wev.
+  intros.
+  apply τ.
+  Defined.
+

 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)
 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)

+    (ig:CoreVar -> bool)

     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ),
     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ),
     WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).

@@ -471,70 +545,73 @@ Definition weakExprToStrongExpr : forall
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)
     (φ:TyVarResolver Γ)
     (ψ:CoVarResolver Γ Δ)
     (ξ:CoreVar -> LeveledHaskType Γ ★)

+    (ig:CoreVar -> bool)

     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=

-    addErrorMessage ("in weakExprToStrongExpr " +++ we)
+    addErrorMessage ("in weakExprToStrongExpr " +++ toString we)

     match we with
 
     match we with
 

-    | WEVar   v                         => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
+    | WEVar   v                         => if ig v
+                                              then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
+                                              else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)

 
 

-    | WELit   lit                       => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
+    | WELit   lit                       => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)

 
     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
 
     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>

-                                                 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
+                                                 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
+                                                 let ig' := update_ig ig ((ev:CoreVar)::nil) in
+                                                   weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>

                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 
     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
                                                      castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
 
     | WEBrak  _ ec e tbody              => φ (`ec) >>= fun ec' =>
                                              weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>

-                                               weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
+                                               weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>

                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 
     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
                                            match lev with
                                              | nil       => Error "ill-leveled escapification"
                                                  castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
 
     | WEEsc   _ ec e tbody              => φ ec >>= fun ec'' =>
                                            weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
                                            match lev with
                                              | nil       => Error "ill-leveled escapification"

-                                             | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
+                                             | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e

                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
                                            end
 
     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 
                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
                                            end
 
     | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
 

-    | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
+    | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')

 
     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
 
     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>

-                                             weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
-                                               weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
+                                             weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
+                                               weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
+                                                    (update_ig ig ((v:CoreVar)::nil)) τ lev ebody

                                                >>= fun ebody' =>
                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 
     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
                                                >>= fun ebody' =>
                                                  OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
 
     | WEApp   e1 e2                     => weakTypeOfWeakExpr e2 >>= fun t2 =>
                                              weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>

-                                               weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
-                                                 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
+                                               weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
+                                                 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>

                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 
     | WETyLam tv e                      => let φ' := upφ tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
                                                  weakExprToStrongExpr _ (weakCE Δ) φ'
                                                    OK (EApp _ _ _ _ _ _ e1' e2')
 
     | WETyLam tv e                      => let φ' := upφ tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
                                                  weakExprToStrongExpr _ (weakCE Δ) φ'

-                                                    (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
-                                                 >>= fun e' =>
-                                                   castExpr we "WETyLam1" _ e' >>= fun e'' =>
-                                                     castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
+                                                   (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
+                                                     >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')

 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with
                                              | WForAllTy wtv te' =>
                                                let φ' := upφ wtv φ in
                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with
                                              | WForAllTy wtv te' =>
                                                let φ' := upφ wtv φ in
                                                  weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>

-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
+                                                   weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>

                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
                                                      weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
                                                        castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')

-                                             | _                 => Error ("weakTypeToType: WETyApp body with type "+++te)
+                                             | _                 => Error ("weakTypeToType: WETyApp body with type "+++toString te)

                                            end
 
     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>
                                            end
 
     | WECoApp e co                     => weakTypeOfWeakExpr e >>= fun te =>

@@ -545,12 +622,12 @@ Definition weakExprToStrongExpr : forall
                                                    haskTypeOfSomeKind κ t1'' =>
                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
                                                    haskTypeOfSomeKind κ t1'' =>
                                                    weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
                                                      weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>

-                                                       weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
+                                                       weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>

                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
                                                            OK (ECoApp Γ Δ κ t1'' t2''
                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
                                                  end
                                                          castExpr we "WECoApp" _ e' >>= fun e'' =>
                                                            OK (ECoApp Γ Δ κ t1'' t2''
                                                              (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
                                                  end

-                                             | _                 => Error ("weakTypeToType: WECoApp body with type "+++te)
+                                             | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)

                                            end
 
     | WECoLam cv e                      => let (_,_,t1,t2) := cv in
                                            end
 
     | WECoLam cv e                      => let (_,_,t1,t2) := cv in

@@ -558,66 +635,69 @@ Definition weakExprToStrongExpr : forall
                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
                                                  weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>

-                                                   weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
+                                                   weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>

                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 
     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 
     | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
                                              weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
                                                weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>

-                                                   weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
+                                                   weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>

                                                      castExpr we "WECast" _ 
                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 
     | WELetRec rb   e                   =>
                                                      castExpr we "WECast" _ 
                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 
     | WELetRec rb   e                   =>

-      let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
-      in let binds := 
+      let ξ' := update_ξ ξ lev _ in
+      let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
+      let binds := 

         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
         match t with
           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)
         (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
           : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
         match t with
           | T_Leaf None           => let case_nil := tt in OK (ELR_nil _ _ _ _)

-          | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
+          | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)

           | T_Branch b1 b2        =>
             binds b1 >>= fun b1' =>
               binds b2 >>= fun b2' =>
                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
         end) rb
       in binds >>= fun binds' =>
           | T_Branch b1 b2        =>
             binds b1 >>= fun b1' =>
               binds b2 >>= fun b2' =>
                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
         end) rb
       in binds >>= fun binds' =>

-           weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>       
-             OK (ELetRec Γ Δ ξ lev τ _ binds' e')
-
-    | WECase vscrut ve tbranches tc avars alts =>
-        weakTypeToTypeOfKind φ (vscrut:WeakType) ★  >>= fun tv =>
-          weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
-            let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
-              mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+         checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
+           weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>       
+             OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
+
+    | WECase vscrut escrut tbranches tc avars alts =>
+        weakTypeOfWeakExpr escrut >>= fun tscrut =>
+          weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
+            if doesWeakVarOccurAlts vscrut alts
+            then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
+            else mkAvars avars (tyConKind tc) φ >>= fun avars' =>

                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>

-                  (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
-                      ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
-                        Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@  lev))}) := 
+                  (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+                      ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
+                        Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@  lev))}}) := 

                     match t with
                       | T_Leaf None           => OK []
                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => 
                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
                           >>= fun exprvars' =>
                     match t with
                       | T_Leaf None           => OK []
                       | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => 
                         mkStrongAltConPlusJunk' tc ac >>= fun sac =>
                           list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
                           >>= fun exprvars' =>

-                            let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
-                              weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
+                            (let case_pf := tt in _) >>= fun pf =>
+                            let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
+                              weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)

                               (sacpj_ψ sac _ _ avars' ψ)
                               (sacpj_ψ sac _ _ avars' ψ)

-                              (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+                              (scbwv_ξ scb ξ lev)
+                              (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
+                              (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>

                                 let case_case := tt in OK [ _ ]
                       | T_Branch b1 b2        =>
                         mkTree b1 >>= fun b1' =>
                           mkTree b2 >>= fun b2' =>
                             OK (b1',,b2')
                     end) alts >>= fun tree =>
                                 let case_case := tt in OK [ _ ]
                       | T_Branch b1 b2        =>
                         mkTree b1 >>= fun b1' =>
                           mkTree b2 >>= fun b2' =>
                             OK (b1',,b2')
                     end) alts >>= fun tree =>

-                  castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
-                      castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
-                        >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
-
-
-
-    end)).

 
 

+                    weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
+                      castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
+    end)); try clear binds; try apply ConcatenableString.
+  

     destruct case_some.
     apply (addErrorMessage "case_some").
       simpl.
     destruct case_some.
     apply (addErrorMessage "case_some").
       simpl.

@@ -630,9 +710,23 @@ Definition weakExprToStrongExpr : forall
       destruct e''; try apply (Error error_message).
       apply OK.
       apply ELR_leaf.
       destruct e''; try apply (Error error_message).
       apply OK.
       apply ELR_leaf.

+      unfold ξ'.
+      simpl.
+      induction (leaves (varsTypes rb φ)).
+        simpl; auto.
+        destruct (ξ c).
+        simpl.

       apply e1.
       apply e1.

+      rewrite mapleaves.
+      apply rb_distinct.
+
+    destruct case_pf.
+      set (distinct_decidable (vec2list exprvars')) as dec.
+      destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].
+      apply OK; auto.

 
     destruct case_case.
 
     destruct case_case.

+      exists sac.

       exists scb.
       apply ebranch'.
 
       exists scb.
       apply ebranch'.