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 mkCoreLet => "sortAlts".
  25   Implicit Arguments sortAlts [[a][b]].
  26
  27 Variable trustMeCoercion           : CoreCoercion.
  28   Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce".
  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 Section HaskWeakToCore.
  35
  36   (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
  37   Context (hetmet_brak_var : CoreVar).
  38   Context (hetmet_esc_var  : CoreVar).
  39
  40   Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
  41     fun _ => trustMeCoercion.
  42
  43   Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar :=
  44   match me with
  45   | WEVar   (weakExprVar v _)            => CoreEVar  v
  46   | WELit   lit                          => CoreELit  lit
  47   | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2)
  48   | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t))
  49   | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr f e )
  50                                                            (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
  51   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr f e )
  52   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr f e )
  53   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr f e )
  54   | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr f e )
  55   | WECast  e co                         => CoreECast    (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co)
  56   | WEBrak  (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_brak_var)
  57                                                            (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
  58   | WEEsc   (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_esc_var)
  59                                                            (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
  60   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr f ve))  (weakExprToCoreExpr f e)
  61   | WECase  e tbranches tc types alts    => let (v,f') := next _ _ f tt  in
  62                                             CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches)
  63                                               (sortAlts ((
  64                                                 fix mkCaseBranches (alts:Tree
  65                                                   ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
  66                                                 match alts with
  67                                                   | T_Leaf None              => nil
  68                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
  69                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
  70                                                     (mkTriple (ac:AltCon)
  71                                                       (app (app
  72                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
  73                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
  74                                                       (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
  75                                                       (weakExprToCoreExpr f' e))::nil
  76                                                 end
  77                                               ) alts))
  78   | WELetRec mlr e                       => CoreELet (CoreRec
  79                                                ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  80                                                  match mlr with
  81                                                    | T_Leaf None                        => nil
  82                                                    | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil
  83                                                    | T_Branch b1 b2                     => app (mkLetBindings b1) (mkLetBindings b2)
  84                                                  end) mlr))
  85                                                (weakExprToCoreExpr f e)
  86   end.
  87
  88 End HaskWeakToCore.
  89
  90