X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=d77d07417da9cc5e691cc37c165173c8368b968f;hp=bbc9cc786313e536048f4fc26e94874a89c0b5cf;hb=0bcb62ecea66324c01f73264ee7cbb4b441ada7c;hpb=b3214686b18b2d6f6905394494da8d1c17587bdb

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index bbc9cc7..d77d074 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,7 +10,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
@@ -18,9 +19,7 @@ Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreVars.
-
-(* can remove *)
-Require Import HaskStrongToWeak.
+Require Import HaskCoreTypes.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
@@ -97,7 +96,7 @@ Notation " ` x " := (@fixkind _ x) (at level 100).
 
 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.
@@ -118,7 +117,7 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
 
 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 _
@@ -127,7 +126,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 => _
-    | 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' =>
@@ -149,6 +149,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
         end
       ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in  _
   end ); clear weakTypeToType.
+  apply ConcatenableString.
 
   destruct case_WTyVarTy.
     apply (addErrorMessage "case_WTyVarTy").
@@ -159,7 +160,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     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))));
@@ -177,7 +179,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
-    apply TyFunApp.
+    apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
     apply lt'.
     apply X.
 
@@ -354,7 +356,7 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAlt
   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 *.
@@ -401,13 +403,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+++
-                    "  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+++
-                    "  got: " +++τ+++eol+++
-                    "  wanted: "+++τ'
+                    "  got: " +++toString τ+++eol+++
+                    "  wanted: "+++toString τ'
     )) ].
   subst.
   apply OK.
@@ -415,7 +417,7 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex
   Defined.
 
 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
-  match wcv with weakCoerVar _ κ _ _ => κ end.
+  match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
   Coercion coVarKind : WeakCoerVar >-> Kind.
 
 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
@@ -511,7 +513,22 @@ Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
     | T_Branch b1 b2                                           => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
   end.
 
-(*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
+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)
@@ -534,14 +551,14 @@ Definition weakExprToStrongExpr : forall
     (τ:HaskType Γ ★)
     (lev:HaskLevel Γ)
     (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) )  :=
-    addErrorMessage ("in weakExprToStrongExpr " +++ we)
+    addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
     match we with
 
     | WEVar   v                         => if ig v
-                                              then OK (EGlobal Γ Δ ξ (τ@@lev) v)
-                                              else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ 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 =>
@@ -596,7 +613,7 @@ Definition weakExprToStrongExpr : forall
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun 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 =>
@@ -612,10 +629,10 @@ Definition weakExprToStrongExpr : forall
                                                            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
+    | WECoLam cv e                      => let (_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>
                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
@@ -645,8 +662,9 @@ Definition weakExprToStrongExpr : forall
                 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
         end) rb
       in binds >>= fun binds' =>
+         checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
            weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>       
-             OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+             OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
 
     | WECase vscrut escrut tbranches tc avars alts =>
         weakTypeOfWeakExpr escrut >>= fun tscrut =>
@@ -680,8 +698,8 @@ Definition weakExprToStrongExpr : forall
 
                     weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
                       castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
-    end)); try clear binds.
-
+    end)); try clear binds; try apply ConcatenableString.
+  
     destruct case_some.
     apply (addErrorMessage "case_some").
       simpl.
@@ -701,6 +719,8 @@ Definition weakExprToStrongExpr : forall
         destruct (ξ c).
         simpl.
       apply e1.
+      rewrite mapleaves.
+      apply rb_distinct.
 
     destruct case_pf.
       set (distinct_decidable (vec2list exprvars')) as dec.