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 WeakTypeVar*list WeakCoerVar*list WeakExprVar*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 WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
  63           {struct alts} : list WeakExprVar :=
  64           match alts with
  65             | T_Leaf  None                                  => nil
  66             | T_Leaf (Some (DEFAULT,_,_,_,e))                   => getWeakExprFreeVars e
  67             | T_Leaf (Some (LitAlt lit,_,_,_,e))                => getWeakExprFreeVars e
  68             | T_Leaf (Some ((DataAlt _ _ _ _ _ dc), tvars, cvars, evars,e))  => removeFromDistinctList' evars (getWeakExprFreeVars e)
  69             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
  70           end) alts))
  71     | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
  72       match mlr with
  73         | T_Leaf None          => cvl
  74         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
  75         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
  76       end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
  77         ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  78           match mlr with
  79             | T_Leaf None          => nil
  80             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
  81             | T_Branch b1 b2       => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
  82           end) mlr))
  83   end.
  84
  85 (* wrap lambdas around an expression until it has no free expression variables *)
  86 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
  87   fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
  88   match cvl with
  89     | nil      => me
  90     | cv::cvl' => WELam cv (closeExpression me cvl')
  91   end) me (getWeakExprFreeVars me).
  92
  93 (* messy first-order capture-avoiding substitution on CoreType's *)
  94 Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) : CoreType :=
  95   match te with
  96     | TyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te
  97     | AppTy  t1 t2            => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
  98     | FunTy    t1 t2          => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
  99     | ForAllTy  tv' t         => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
 100     | PredTy (EqPred t1 t2)   => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
 101     | PredTy (IParam ip ty)   => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
 102     | PredTy (ClassP _ c lt)  => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=
 103       match lt with
 104         | nil => nil
 105         | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
 106       end) lt))
 107     | TyConApp _ tc lt => TyConApp tc ((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   end.
 113
 114 (* calculate the CoreType of a WeakExpr *)
 115 Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
 116   match ce with
 117     | WEVar   (weakExprVar v t) => OK t
 118     | WELit   lit   => OK (haskLiteralToCoreType lit)
 119     | WEApp   e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
 120                        match t' with
 121                          | (TyConApp 2 tc (t1::t2::nil)) =>
 122                            if (tyCon_eq tc ArrowTyCon)
 123                              then OK t2
 124                              else Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
 125                          | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
 126                        end
 127     | WETyApp e t    => coreTypeOfWeakExpr e >>= fun te =>
 128                         match te with
 129                           | ForAllTy v ct => OK (replaceCoreVar ct v t)
 130                           | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
 131                         end
 132     | WECoApp e co   => coreTypeOfWeakExpr e >>= fun te =>
 133                         match te with
 134                           | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
 135                             if (tyCon_eq tc ArrowTyCon)
 136                               then OK t3
 137                               else Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
 138                           | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
 139                         end
 140     | WELam   (weakExprVar ev vt) e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon (vt::t'::nil))
 141     | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => match tv with weakTypeVar tvc _ => OK (ForAllTy tvc t') end
 142     | WECoLam (weakCoerVar cv φ₁ φ₂) e =>
 143       coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon ((PredTy (EqPred φ₁ φ₂))::t'::nil))
 144     | WELet   ev ve e            => coreTypeOfWeakExpr e
 145     | WELetRec rb e              => coreTypeOfWeakExpr e
 146     | WENote  n e                => coreTypeOfWeakExpr e
 147     | WECast  e (weakCoercion t1 t2 _) => OK t2
 148     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches
 149
 150     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
 151     | WEBrak  ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
 152                                                            OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end
 153     | WEEsc   ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
 154       match t' with
 155         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
 156           if (tyCon_eq tc hetMetCodeTypeTyCon)
 157           then if eqd_dec ecc ec' then OK t''
 158             else Error "level mismatch in escapification"
 159           else Error "ill-typed escapification"
 160         | _ => Error "ill-typed escapification"
 161       end end
 162   end.
 163