X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=f0a8300886a15eb82d1d717982d37e7dcb693d92;hp=9de00e34564e51ba250c606753782c3290a32942;hb=bcb16a7fa1ff772f12807c4587609fd756b7762e;hpb=a9bbdf55d01ad494d42018c0eaa252da1d7b5d97

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 9de00e3..f0a8300 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -7,13 +7,15 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
-Require Import HaskGeneral.
-Require Import HaskLiterals.
+Require Import HaskKinds.
+Require Import HaskCoreLiterals.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
+Require Import HaskWeakTypes.
 Require Import HaskWeak.
+Require Import HaskCoreToWeak.
 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
@@ -22,8 +24,8 @@ Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple A
   Extract Inlined Constant mkCoreLet => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
-Variable unsafeCoerce           : CoreCoercion.
-  Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
+Variable trustMeCoercion           : CoreCoercion.
+  Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce".
 
 (* 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.
@@ -31,13 +33,8 @@ Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
 
 (* a dummy variable which is never referenced but needed for a binder *)
 Variable dummyVariable : CoreVar.
-
-Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
-match wv with
-| WExprVar (weakExprVar v _   ) => v
-| WTypeVar (weakTypeVar v _   ) => v
-| WCoerVar (weakCoerVar v _ _ ) => v
-end.
+  (* FIXME this doesn't actually work *)
+  Extract Inlined Constant dummyVariable => "(Prelude.error ""dummyVariable"")".
 
 Section HaskWeakToCore.
 
@@ -45,15 +42,16 @@ Section HaskWeakToCore.
   Context (hetmet_brak_var : CoreVar).
   Context (hetmet_esc_var  : CoreVar).
 
+  (* FIXME: do something more intelligent here *)
   Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
-    fun _ => unsafeCoerce.
+    fun _ => trustMeCoercion.
 
   Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit
   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
-  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType t)
+  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
   | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
                                                            (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
@@ -61,17 +59,25 @@ Section HaskWeakToCore.
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
   | WECoLam (weakCoerVar cv _ _) e       => CoreELam  cv (weakExprToCoreExpr e )
   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
-  | WEBrak  (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_brak_var) (CoreEType (TyVarTy ec))) (CoreEType t)
-  | WEEsc   (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType t)
+  | WEBrak  (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_brak_var)
+                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
+  | WEEsc   (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_esc_var)
+                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
-  | WECase  e tbranches n tc types alts  => CoreECase (weakExprToCoreExpr e) dummyVariable tbranches
+  | WECase  e tbranches tc types alts    => CoreECase (weakExprToCoreExpr e) dummyVariable (weakTypeToCoreType tbranches)
                                               (sortAlts ((
-                                                fix mkCaseBranches (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) :=
+                                                fix mkCaseBranches (alts:Tree 
+                                                  ??(AltCon*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,lwv,e)) =>
-                                                    (mkTriple ac (map weakVarToCoreVar lwv) (weakExprToCoreExpr e))::nil
+                                                  | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
+                                                    (mkTriple (ac:AltCon)
+                                                      (app (app 
+                                                        (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
+                                                        (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
+                                                      (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
+                                                      (weakExprToCoreExpr e))::nil
                                                 end
                                               ) alts))
   | WELetRec mlr e                       => CoreELet (CoreRec
@@ -84,4 +90,6 @@ Section HaskWeakToCore.
                                                (weakExprToCoreExpr e)
   end.
 
-End HaskWeakToCore.
\ No newline at end of file
+End HaskWeakToCore.
+
+