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 HaskCoreLiterals.
  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 AltCon a b) -> list (@triple AltCon 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 Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
  35   mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
  36
  37 Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
  38   match me with
  39   | WEVar   (weakExprVar v _)            => CoreEVar  v
  40   | WELit   lit                          => CoreELit  lit
  41   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
  42   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
  43   | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
  44                                                            (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
  45   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
  46   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
  47   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
  48   | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
  49   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
  50   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
  51                                                    ((CoreEType (TyVarTy ec))::
  52                                                      (CoreEType (weakTypeToCoreType t))::
  53                                                      (weakExprToCoreExpr e)::
  54                                                      nil)
  55                                                    (CoreEVar v)
  56   | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
  57                                                    ((CoreEType (TyVarTy ec))::
  58                                                      (CoreEType (weakTypeToCoreType t))::
  59                                                      (weakExprToCoreExpr e)::
  60                                                      nil)
  61                                                    (CoreEVar v)
  62   | WECSP   v (weakTypeVar ec _) e t     => fold_left CoreEApp
  63                                                    ((CoreEType (TyVarTy ec))::
  64                                                      (CoreEType (weakTypeToCoreType t))::
  65                                                      (weakExprToCoreExpr e)::
  66                                                      nil)
  67                                                    (CoreEVar v)
  68   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
  69   | WECase  vscrut e tbranches tc types alts  =>
  70                                             CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
  71                                               (sortAlts ((
  72                                                 fix mkCaseBranches (alts:Tree
  73                                                   ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
  74                                                 match alts with
  75                                                   | T_Leaf None              => nil
  76                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
  77                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
  78                                                     (mkTriple (ac:AltCon)
  79                                                       (app (app
  80                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
  81                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
  82                                                       (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
  83                                                       (weakExprToCoreExpr e))::nil
  84                                                 end
  85                                               ) alts))
  86   | WELetRec mlr e                       => CoreELet (CoreRec
  87                                                ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  88                                                  match mlr with
  89                                                    | T_Leaf None                        => nil
  90                                                    | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
  91                                                    | T_Branch b1 b2                     => app (mkLetBindings b1) (mkLetBindings b2)
  92                                                  end) mlr))
  93                                                (weakExprToCoreExpr e)
  94   end.
  95
  96 Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
  97   coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
  98
  99 Instance weakExprToString : ToString WeakExpr  :=
 100   { toString := fun we => toString (weakExprToCoreExpr we) }.
 101