update for new GHC coercion representation

[coq-hetmet.git] / src / HaskWeakToCore.v

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 9de00e3..c3e90a4 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -7,71 +7,99 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.

-Require Import HaskGeneral.
+Require Import HaskKinds.

 Require Import HaskLiterals.
 Require Import HaskLiterals.

+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.

+Require Import HaskWeakTypes.

 Require Import HaskWeak.
 Require Import HaskWeak.

+Require Import HaskCoreToWeak.

 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 
 
 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).
-  Extract Inlined Constant mkCoreLet => "sortAlts".
+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]].
 
   Implicit Arguments sortAlts [[a][b]].
 

-Variable unsafeCoerce           : CoreCoercion.
-  Extract Inlined Constant unsafeCoerce => "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.
-  Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
-
-(* 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.
-
-Section HaskWeakToCore.
+Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
+  match wa with
+  | WeakDataAlt cdc => DataAlt cdc
+  | WeakLitAlt  lit => LitAlt lit
+  | WeakDEFAULT     => DEFAULT
+  end.

 
 

-  (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
-  Context (hetmet_brak_var : CoreVar).
-  Context (hetmet_esc_var  : CoreVar).
+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 : WeakCoercion -> CoreCoercion :=
-    fun _ => unsafeCoerce.
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+  CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).

 
 

-  Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
+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)
   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)
-  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
-                                                           (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
+  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
+  | 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 )
   | 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)
   | 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  v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)
+  | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)
+  | WECSP   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)

   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
   | 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  vscrut escrut tbranches tc types alts  =>
+                                            CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)

                                               (sortAlts ((
                                               (sortAlts ((

-                                                fix mkCaseBranches (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) :=
+                                                fix mkCaseBranches (alts:Tree 
+                                                  ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=

                                                 match alts with
                                                   | T_Leaf None              => nil
                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
                                                 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 (weakAltConToCoreAltCon ac)
+                                                      (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
                                                 end
                                               ) alts))
   | WELetRec mlr e                       => CoreELet (CoreRec

@@ -84,4 +112,10 @@ Section HaskWeakToCore.
                                                (weakExprToCoreExpr e)
   end.
 
                                                (weakExprToCoreExpr e)
   end.
 

-End HaskWeakToCore.
\ No newline at end of file
+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
+
+Instance weakExprToString : ToString WeakExpr  :=
+  { toString := fun we => toString (weakExprToCoreExpr we) }.
+
+