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 HaskLiterals.
  12 Require Import HaskTyCons.
  13 Require Import HaskCoreVars.
  14 Require Import HaskCoreTypes.
  15 Require Import HaskCore.
  16 Require Import HaskWeakVars.
  17 Require Import HaskWeakTypes.
  18 Require Import HaskWeak.
  19 Require Import HaskCoreToWeak.
  20
  21 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
  22   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
  23
  24 Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).
  25   Extract Inlined Constant sortAlts => "sortAlts".
  26   Implicit Arguments sortAlts [[a][b]].
  27
  28 Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
  29   match wa with
  30   | WeakDataAlt cdc => DataAlt cdc
  31   | WeakLitAlt  lit => LitAlt lit
  32   | WeakDEFAULT     => DEFAULT
  33   end.
  34
  35 Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
  36   match wt with
  37     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
  38     | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
  39     | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
  40                                            | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
  41                                            | t1'             => AppTy t1' (weakTypeToCoreType t2)
  42                                          end
  43     | WTyCon    tc                    => TyConApp tc nil
  44     | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
  45     | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
  46     | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
  47     | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
  48     | WFunTyCon                       => TyConApp ArrowTyCon nil
  49     | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
  50     | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
  51                                             (weakTypeToCoreType t3)
  52   end.
  53
  54 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
  55   CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
  56
  57 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
  58   match me with
  59   | WEVar   (weakExprVar v _)            => CoreEVar  v
  60   | WELit   lit                          => CoreELit  lit
  61   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
  62   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
  63   | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co))
  64   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
  65   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
  66   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
  67   | WECoLam (weakCoerVar cv   _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
  68   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
  69   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
  70                                                    ((CoreEType (TyVarTy ec))::
  71                                                      (CoreEType (weakTypeToCoreType t))::
  72                                                      (weakExprToCoreExpr e)::
  73                                                      nil)
  74                                                    (CoreEVar v)
  75   | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
  76                                                    ((CoreEType (TyVarTy ec))::
  77                                                      (CoreEType (weakTypeToCoreType t))::
  78                                                      (weakExprToCoreExpr e)::
  79                                                      nil)
  80                                                    (CoreEVar v)
  81   | WECSP   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   (*
  88   | WEKappa     v e      => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappa"
  89   | WEKappaApp  e1 e2    => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappaApp"
  90   *)
  91   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
  92   | WECase  vscrut escrut tbranches tc types alts  =>
  93                                             CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
  94                                               (sortAlts ((
  95                                                 fix mkCaseBranches (alts:Tree
  96                                                   ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
  97                                                 match alts with
  98                                                   | T_Leaf None              => nil
  99                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
 100                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
 101                                                     (mkTriple (weakAltConToCoreAltCon ac)
 102                                                       (app (app
 103                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
 104                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
 105                                                       (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
 106                                                       (weakExprToCoreExpr e))::nil
 107                                                 end
 108                                               ) alts))
 109   | WELetRec mlr e                       => CoreELet (CoreRec
 110                                                ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
 111                                                  match mlr with
 112                                                    | T_Leaf None                        => nil
 113                                                    | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
 114                                                    | T_Branch b1 b2                     => app (mkLetBindings b1) (mkLetBindings b2)
 115                                                  end) mlr))
 116                                                (weakExprToCoreExpr e)
 117   end.
 118
 119 Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
 120   coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
 121
 122 Instance weakExprToString : ToString WeakExpr  :=
 123   { toString := fun we => toString (weakExprToCoreExpr we) }.
 124
 125