src/HaskWeakToCore.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeakToCore: convert HaskWeak to HaskCore                                                                                  *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import Coq.Lists.List.
  10 Require Import HaskKinds.
  11 Require Import HaskLiteralsAndTyCons.
  12 Require Import HaskCoreVars.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskCore.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeakTypes.
  17 Require Import HaskWeak.
  18 Require Import HaskCoreToWeak.
  19
  20 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
  21   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
  22
  23 Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).
  24   Extract Inlined Constant sortAlts => "sortAlts".
  25   Implicit Arguments sortAlts [[a][b]].
  26
  27 Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
  28     Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
  29
  30 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
  31 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
  32   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
  33
  34 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
  35 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
  36
  37 Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
  38   match wa with
  39   | WeakDataAlt cdc => DataAlt cdc
  40   | WeakLitAlt  lit => LitAlt lit
  41   | WeakDEFAULT     => DEFAULT
  42   end.
  43
  44 Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
  45   match wt with
  46     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
  47     | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
  48     | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
  49                                            | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
  50                                            | t1'             => AppTy t1' (weakTypeToCoreType t2)
  51                                          end
  52     | WTyCon    tc                    => TyConApp tc nil
  53     | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
  54     | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
  55     | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
  56     | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
  57     | WFunTyCon                       => TyConApp ArrowTyCon nil
  58     | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
  59     | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
  60                                             (weakTypeToCoreType t3)
  61   end.
  62
  63 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion.
  64   admit.
  65   Defined.
  66   (*mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).*)
  67
  68 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
  69   match me with
  70   | WEVar   (weakExprVar v _)            => CoreEVar  v
  71   | WELit   lit                          => CoreELit  lit
  72   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
  73   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
  74   | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
  75                                                            (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
  76   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
  77   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
  78   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
  79   | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
  80   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
  81   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
  82                                                    ((CoreEType (TyVarTy ec))::
  83                                                      (CoreEType (weakTypeToCoreType t))::
  84                                                      (weakExprToCoreExpr e)::
  85                                                      nil)
  86                                                    (CoreEVar v)
  87   | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
  88                                                    ((CoreEType (TyVarTy ec))::
  89                                                      (CoreEType (weakTypeToCoreType t))::
  90                                                      (weakExprToCoreExpr e)::
  91                                                      nil)
  92                                                    (CoreEVar v)
  93   | WECSP   v (weakTypeVar ec _) e t     => fold_left CoreEApp
  94                                                    ((CoreEType (TyVarTy ec))::
  95                                                      (CoreEType (weakTypeToCoreType t))::
  96                                                      (weakExprToCoreExpr e)::
  97                                                      nil)
  98                                                    (CoreEVar v)
  99   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
 100   | WECase  vscrut e tbranches tc types alts  =>
 101                                             CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
 102                                               (sortAlts ((
 103                                                 fix mkCaseBranches (alts:Tree
 104                                                   ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 105                                                 match alts with
 106                                                   | T_Leaf None              => nil
 107                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
 108                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
 109                                                     (mkTriple (weakAltConToCoreAltCon ac)
 110                                                       (app (app
 111                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
 112                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
 113                                                       (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
 114                                                       (weakExprToCoreExpr e))::nil
 115                                                 end
 116                                               ) alts))
 117   | WELetRec mlr e                       => CoreELet (CoreRec
 118                                                ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
 119                                                  match mlr with
 120                                                    | T_Leaf None                        => nil
 121                                                    | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
 122                                                    | T_Branch b1 b2                     => app (mkLetBindings b1) (mkLetBindings b2)
 123                                                  end) mlr))
 124                                                (weakExprToCoreExpr e)
 125   end.
 126
 127 Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
 128   coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
 129
 130 Instance weakExprToString : ToString WeakExpr  :=
 131   { toString := fun we => toString (weakExprToCoreExpr we) }.
 132
 133