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

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 38a4304..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).
@@ -467,6 +464,55 @@ Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
             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 ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
+
 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
@@ -500,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')
@@ -524,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')
@@ -585,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))
@@ -605,28 +651,25 @@ Definition weakExprToStrongExpr : forall
     | WECase vscrut escrut tbranches tc avars alts =>
         weakTypeOfWeakExpr escrut >>= fun tscrut =>
           weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
-(*
-            let ξ'  := update_ξ  ξ  (((vscrut:CoreVar),tscrut'@@lev)::nil) in
-            let ig' := update_ig ig ((vscrut:CoreVar)::nil) in
-*)
-            let ξ'  := ξ in
-            let ig' := ig in
-              mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+            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' =>
                   (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))))
+                              (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        =>
@@ -635,16 +678,9 @@ Definition weakExprToStrongExpr : forall
                             OK (b1',,b2')
                     end) alts >>= fun tree =>
 
-                  weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
-                    castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ' lev tc tbranches' avars' escrut' tree)
-(*
-                  weakExprToStrongExpr Γ Δ φ ψ ξ ig tscrut' lev escrut >>= fun escrut' =>
-                    castExpr we "ECaseScrut" (caseType tc avars' @@  lev) (EVar Γ Δ ξ' vscrut) >>= fun evscrut' =>
-                      castExpr we "ECase" (τ@@lev)
-                      (ELet Γ Δ ξ tscrut' tbranches' lev (vscrut:CoreVar) escrut'
-                        (ECase Γ Δ ξ' lev tc tbranches' avars' evscrut' tree))
-*)
-    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.
 
     destruct case_some.
     apply (addErrorMessage "case_some").
@@ -658,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'.