X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=c3e90a43763c820af3ea4c561b465986d05a73ad;hp=9607d5f87d6f19359bf2d62898fdd4af2e228325;hb=5cb97fa6ed28f55ca888bdadc4f145396cc02236;hpb=24445b56cb514694c603c342d77cbc8329a4b0aa

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 9607d5f..c3e90a4 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -8,7 +8,8 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -20,19 +21,38 @@ Require Import HaskCoreToWeak.
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 
-Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
+Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
-Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
-    Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
+Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
+  match wa with
+  | WeakDataAlt cdc => DataAlt cdc
+  | WeakLitAlt  lit => LitAlt lit
+  | WeakDEFAULT     => DEFAULT
+  end.
 
-(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
-Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
-  Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
+Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
+  match wt with
+    | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
+    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
+    | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
+                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
+                                           | t1'             => AppTy t1' (weakTypeToCoreType t2)
+                                         end
+    | WTyCon    tc                    => TyConApp tc nil
+    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
+    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
+    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
+    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
+    | WFunTyCon                       => TyConApp ArrowTyCon nil
+    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
+    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
+                                            (weakTypeToCoreType t3)
+  end.
 
 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
-  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
+  CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
@@ -40,12 +60,11 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   | WELit   lit                          => CoreELit  lit
   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
-  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
-                                                           (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
+  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co))
   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
-  | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
+  | WECoLam (weakCoerVar cv   _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
                                                    ((CoreEType (TyVarTy ec))::
@@ -66,16 +85,16 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                                      nil)
                                                    (CoreEVar v)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
-  | WECase  vscrut e tbranches tc types alts  =>
-                                            CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
+  | WECase  vscrut escrut tbranches tc types alts  =>
+                                            CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 
-                                                  ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+                                                  ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
                                                 match alts with
                                                   | T_Leaf None              => nil
                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
-                                                    (mkTriple (ac:AltCon)
+                                                    (mkTriple (weakAltConToCoreAltCon ac)
                                                       (app (app 
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
@@ -99,3 +118,4 @@ Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
 Instance weakExprToString : ToString WeakExpr  :=
   { toString := fun we => toString (weakExprToCoreExpr we) }.
 
+