X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=bbc9cc786313e536048f4fc26e94874a89c0b5cf;hb=32436fdf380f7f2efc7a70896268509e7b3e0d6f;hp=aeb42b122d77dc61e00e93a98ccf321e6cd4d7e9;hpb=adc57ef5613ef2c5befc28071c5e2ae71859e14c;p=coq-hetmet.git

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index aeb42b1..bbc9cc7 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -224,9 +224,6 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     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).
@@ -549,7 +546,7 @@ Definition weakExprToStrongExpr : forall
     | WELam   ev ebody                  => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
                                              weakTypeOfWeakExpr ebody >>= fun tbody =>
                                                weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
-                                                 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
+                                                 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')
@@ -573,7 +570,7 @@ Definition weakExprToStrongExpr : forall
 
     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>
                                              weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
-                                               weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil))
+                                               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')
@@ -634,7 +631,7 @@ Definition weakExprToStrongExpr : forall
                                                        (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
 
     | WELetRec rb   e                   =>
-      let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in
+      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))
@@ -659,16 +656,17 @@ Definition weakExprToStrongExpr : forall
             else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
                 weakTypeToTypeOfKind φ tbranches ★  >>= fun tbranches' =>
                   (fix mkTree (t:Tree ??(WeakAltCon*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))}) := 
+                      ??{ 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' =>
-                            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' ψ)
                               (scbwv_ξ scb ξ lev)
                               (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
@@ -682,7 +680,7 @@ Definition weakExprToStrongExpr : forall
 
                     weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
                       castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
-    end)).
+    end)); try clear binds.
 
     destruct case_some.
     apply (addErrorMessage "case_some").
@@ -696,9 +694,21 @@ Definition weakExprToStrongExpr : forall
       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.
 
+    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.
+      exists sac.
       exists scb.
       apply ebranch'.