src/HaskWeak.v

   1 (*********************************************************************************************************************************)
   2 (* HaskWeak: a non-dependently-typed but Coq-friendly version of HaskCore                                                        *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Lists.List.
   9 Require Import HaskGeneral.
  10 Require Import HaskLiterals.
  11 Require Import HaskCoreVars.
  12 Require Import HaskCoreTypes.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskWeakVars.
  15
  16 Inductive WeakExpr :=
  17 | WEVar       : WeakExprVar                                                  -> WeakExpr
  18 | WELit       : HaskLiteral                                                  -> WeakExpr
  19 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  20 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  21 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
  22 | WENote      : Note                            -> WeakExpr                  -> WeakExpr
  23 | WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
  24 | WETyApp     : WeakExpr                        -> CoreType                  -> WeakExpr
  25 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
  26 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  27 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
  28 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
  29
  30 (* the CoreType argument is used only when going back from Weak to Core; it lets us dodge a possibly-failing type calculation *)
  31 | WEBrak      : WeakTypeVar                     -> WeakExpr  -> CoreType     -> WeakExpr
  32 | WEEsc       : WeakTypeVar                     -> WeakExpr  -> CoreType     -> WeakExpr
  33
  34 (* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
  35 | WECase      : forall (scrutinee:WeakExpr)
  36                        (tbranches:CoreType)
  37                        {n:nat}(tc:TyCon n)
  38                        (type_params:vec CoreType n)
  39                        (alts : Tree ??(AltCon*list WeakVar*WeakExpr)),
  40                        WeakExpr.
  41
  42 (* calculate the free WeakVar's in a WeakExpr *)
  43 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
  44   match me with
  45     | WELit    _        =>     nil
  46     | WEVar    cv       => cv::nil
  47     | WECast   e co     =>                            getWeakExprFreeVars e
  48     | WENote   n e      =>                            getWeakExprFreeVars e
  49     | WETyApp  e t      =>                            getWeakExprFreeVars e
  50     | WECoApp  e co     =>                            getWeakExprFreeVars e
  51     | WEBrak   ec e _   =>                            getWeakExprFreeVars e
  52     | WEEsc    ec e _   =>                            getWeakExprFreeVars e
  53     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
  54     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
  55     | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
  56     | WETyLam  cv e     => getWeakExprFreeVars e
  57     | WECoLam  cv e     => getWeakExprFreeVars e
  58
  59     (* the messy fixpoints below are required by Coq's termination conditions *)
  60     | WECase scrutinee tbranches n tc type_params alts =>
  61       mergeDistinctLists (getWeakExprFreeVars scrutinee) (
  62         ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) {struct alts} : list WeakExprVar :=
  63           match alts with
  64             | T_Leaf  None                                  => nil
  65             | T_Leaf (Some (DEFAULT,_,e))                   => getWeakExprFreeVars e
  66             | T_Leaf (Some (LitAlt lit,_,e))                => getWeakExprFreeVars e
  67             | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e))  => removeFromDistinctList'
  68               (General.filter (map (fun v => match v with
  69                                | WExprVar ev => Some ev
  70                                | WTypeVar _  => None
  71                                | WCoerVar _  => None
  72               end) vars))
  73               (getWeakExprFreeVars e)
  74             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
  75           end) alts))
  76     | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
  77       match mlr with
  78         | T_Leaf None          => cvl
  79         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
  80         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
  81       end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
  82         ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  83           match mlr with
  84             | T_Leaf None          => nil
  85             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
  86             | T_Branch b1 b2       => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
  87           end) mlr))
  88   end.
  89
  90 (* wrap lambdas around an expression until it has no free expression variables *)
  91 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
  92   fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
  93   match cvl with
  94     | nil      => me
  95     | cv::cvl' => WELam cv (closeExpression me cvl')
  96   end) me (getWeakExprFreeVars me).
  97
  98 (* messy first-order capture-avoiding substitution on CoreType's *)
  99 Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) : CoreType :=
 100   match te with
 101     | TyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te
 102     | AppTy  t1 t2            => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
 103     | FunTy    t1 t2          => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
 104     | ForAllTy  tv' t         => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
 105     | PredTy (EqPred t1 t2)   => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
 106     | PredTy (IParam ip ty)   => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
 107     | PredTy (ClassP _ c lt)  => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=
 108       match lt with
 109         | nil => nil
 110         | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
 111       end) lt))
 112     | TyConApp _ tc lt => TyConApp tc ((fix replaceCoreDistinctList (lt:list CoreType) :=
 113       match lt with
 114         | nil => nil
 115         | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
 116       end) lt)
 117   end.
 118
 119 (* calculate the CoreType of a WeakExpr *)
 120 Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
 121   match ce with
 122     | WEVar   (weakExprVar v t) => OK t
 123     | WELit   lit   => OK (haskLiteralToCoreType lit)
 124     | WEApp   e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
 125                        match t' with
 126                          | (TyConApp 2 tc (t1::t2::nil)) =>
 127                            if (tyCon_eq tc ArrowTyCon)
 128                              then OK t2
 129                              else Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
 130                          | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
 131                        end
 132     | WETyApp e t    => coreTypeOfWeakExpr e >>= fun te =>
 133                         match te with
 134                           | ForAllTy v ct => OK (replaceCoreVar ct v t)
 135                           | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
 136                         end
 137     | WECoApp e co   => coreTypeOfWeakExpr e >>= fun te =>
 138                         match te with
 139                           | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
 140                             if (tyCon_eq tc ArrowTyCon)
 141                               then OK t3
 142                               else Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
 143                           | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
 144                         end
 145     | WELam   (weakExprVar ev vt) e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon (vt::t'::nil))
 146     | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => match tv with weakTypeVar tvc _ => OK (ForAllTy tvc t') end
 147     | WECoLam (weakCoerVar cv φ₁ φ₂) e =>
 148       coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon ((PredTy (EqPred φ₁ φ₂))::t'::nil))
 149     | WELet   ev ve e            => coreTypeOfWeakExpr e
 150     | WELetRec rb e              => coreTypeOfWeakExpr e
 151     | WENote  n e                => coreTypeOfWeakExpr e
 152     | WECast  e (weakCoercion t1 t2 _) => OK t2
 153     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches
 154
 155     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
 156     | WEBrak  ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
 157                                                            OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end
 158     | WEEsc   ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
 159       match t' with
 160         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
 161           if (tyCon_eq tc hetMetCodeTypeTyCon)
 162           then if eqd_dec ecc ec' then OK t''
 163             else Error "level mismatch in escapification"
 164           else Error "ill-typed escapification"
 165         | _ => Error "ill-typed escapification"
 166       end end
 167   end.
 168