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 HaskGeneral.
   9 Require Import HaskLiterals.
  10 Require Import HaskCoreVars.
  11 Require Import HaskCoreTypes.
  12
  13 Inductive WeakExpr :=
  14 | WEVar       : CoreVar                                                  -> WeakExpr
  15 | WELit       : HaskLiteral                                              -> WeakExpr
  16 | WELet       : CoreVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  17 | WELetRec    : Tree ??(CoreVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  18 | WECast      : WeakExpr                    -> CoreCoercion              -> WeakExpr
  19 | WENote      : Note                        -> WeakExpr                  -> WeakExpr
  20 | WEApp       : WeakExpr                    -> WeakExpr                  -> WeakExpr
  21 | WETyApp     : WeakExpr                    -> CoreType                  -> WeakExpr
  22 | WECoApp     : WeakExpr                    -> CoreCoercion              -> WeakExpr
  23 | WELam       : CoreVar                     -> WeakExpr                  -> WeakExpr
  24 | WETyLam     : CoreVar                     -> WeakExpr                  -> WeakExpr
  25 | WECoLam     : CoreVar                     -> WeakExpr                  -> WeakExpr
  26 | WEBrak      : CoreVar                     -> WeakExpr                  -> WeakExpr
  27 | WEEsc       : CoreVar                     -> WeakExpr                  -> WeakExpr
  28 | WECase      : forall (scrutinee:WeakExpr)
  29                        (tbranches:CoreType)
  30                        {n:nat}(tc:TyCon n)
  31                        (type_params:vec CoreType n)
  32                        (alts : Tree ??(AltCon*list CoreVar*WeakExpr)),
  33                        WeakExpr.
  34
  35 (* calculate the free CoreVar's in a WeakExpr *)
  36 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar :=
  37   match me with
  38     | WELit    _        =>     nil
  39     | WEVar    cv       => cv::nil
  40     | WECast   e co     =>                            getWeakExprFreeVars e
  41     | WENote   n e      =>                            getWeakExprFreeVars e
  42     | WETyApp  e t      =>                            getWeakExprFreeVars e
  43     | WECoApp  e co     =>                            getWeakExprFreeVars e
  44     | WEBrak   ec e     =>                            getWeakExprFreeVars e
  45     | WEEsc    ec e     =>                            getWeakExprFreeVars e
  46     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
  47     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
  48     | WELam    cv e     => removeFromDistinctList cv (getWeakExprFreeVars e)
  49     | WETyLam  cv e     => removeFromDistinctList cv (getWeakExprFreeVars e)
  50     | WECoLam  cv e     => removeFromDistinctList cv (getWeakExprFreeVars e)
  51
  52     (* the messy fixpoints below are required by Coq's termination conditions *)
  53     | WECase scrutinee tbranches n tc type_params alts =>
  54       mergeDistinctLists (getWeakExprFreeVars scrutinee) (
  55         ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list CoreVar*WeakExpr)) {struct alts} : list CoreVar :=
  56           match alts with
  57             | T_Leaf  None                                  => nil
  58             | T_Leaf (Some (DEFAULT,_,e))                   => getWeakExprFreeVars e
  59             | T_Leaf (Some (LitAlt lit,_,e))                => getWeakExprFreeVars e
  60             | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e))  => removeFromDistinctList' vars (getWeakExprFreeVars e)
  61             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
  62           end) alts))
  63     | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr))(cvl:list CoreVar) :=
  64       match mlr with
  65         | T_Leaf None          => cvl
  66         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
  67         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
  68       end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
  69         ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr)) :=
  70           match mlr with
  71             | T_Leaf None          => nil
  72             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
  73             | T_Branch b1 b2       => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
  74           end) mlr))
  75   end.
  76
  77 (* wrap lambdas around an expression until it has no free variables *)
  78 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
  79   fun me => (fix closeExpression (me:WeakExpr)(cvl:list CoreVar) :=
  80   match cvl with
  81     | nil      => me
  82     | cv::cvl' => WELam cv (closeExpression me cvl')
  83   end) me (getWeakExprFreeVars me).
  84
  85 (* messy first-order capture-avoiding substitution on CoreType's *)
  86 Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) :=
  87   match te with
  88     | TyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te
  89     | AppTy    t1 t2          => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
  90     | FunTy    t1 t2          => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
  91     | ForAllTy tv' t          => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
  92     | PredTy (EqPred t1 t2)   => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
  93     | PredTy (IParam ip ty)   => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
  94     | PredTy (ClassP _ c lt)  => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=
  95       match lt with
  96         | nil => nil
  97         | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
  98       end) lt))
  99     | TyConApp _ tc lt => TyConApp tc ((fix replaceCoreDistinctList (lt:list CoreType) :=
 100       match lt with
 101         | nil => nil
 102         | h::t => (replaceCoreVar h tv tsubst)::(replaceCoreDistinctList t)
 103       end) lt)
 104   end.
 105
 106 (* calculate the CoreType of a WeakExpr *)
 107 Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
 108   match ce with
 109     | WEVar   v     => match coreVarSort v with
 110                          | CoreExprVar t => OK t
 111                          | CoreTypeVar _ => Error "found tyvar in expression"
 112                          | CoreCoerVar _ => Error "found coercion variable in expression"
 113                        end
 114     | WELit   lit   => OK (haskLiteralToCoreType lit)
 115     | WEApp   e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
 116                        match t' with
 117                          | FunTy t1 t2 => OK t2
 118                          | (TyConApp 2 tc (t1::t2::nil)) =>
 119                            if (tyCon_eq tc ArrowTyCon)
 120                              then OK t2
 121                              else Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
 122                          | _ => Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
 123                        end
 124     | WETyApp e t    => coreTypeOfWeakExpr e >>= fun te =>
 125                         match te with
 126                           | ForAllTy v ct => match coreVarSort v with
 127                                                | CoreExprVar _ => Error "found an expression variable inside an forall-type!"
 128                                                | CoreTypeVar _ => OK (replaceCoreVar ct v t)
 129                                                | CoreCoerVar _ => Error "found a coercion variable inside an forall-type!"
 130                                              end
 131                           | _ => Error ("found non-forall type "+++(coreTypeToString te)+++" in ETyApp")
 132                         end
 133     | WECoApp e co   => coreTypeOfWeakExpr e >>= fun te =>
 134                         match te with
 135                           | FunTy (PredTy (EqPred t1 t2)) t3 => OK t3
 136                           | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
 137                             if (tyCon_eq tc ArrowTyCon)
 138                               then OK t3
 139                               else Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
 140                           | _ => Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
 141                         end
 142     | WELam   ev e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort ev with
 143                                                | CoreExprVar vt => OK (FunTy vt t')
 144                                                | CoreTypeVar _  => Error "found a type variable in a WELam!"
 145                                                | CoreCoerVar _  => Error "found a coercion variable in a WELam!"
 146                                              end
 147     | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => OK (ForAllTy tv t')
 148     | WECoLam cv e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort cv with
 149                                                | CoreExprVar vt => Error "found an expression variable in a WECoLam!"
 150                                                | CoreTypeVar _  => Error "found a type variable in a WECoLam!"
 151                                                | CoreCoerVar (φ₁,φ₂) => OK (FunTy (PredTy (EqPred φ₁ φ₂)) t')
 152                                              end
 153     | WELet   ev ve e            => coreTypeOfWeakExpr e
 154     | WELetRec rb e              => coreTypeOfWeakExpr e
 155     | WENote  n e                => coreTypeOfWeakExpr e
 156     | WECast  e co               => OK (snd (coreCoercionKind co))
 157     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches
 158     | WEBrak  ec e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ec)::t'::nil))
 159     | WEEsc   ec e => coreTypeOfWeakExpr e >>= fun t' =>
 160       match t' with
 161         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
 162           if (tyCon_eq tc hetMetCodeTypeTyCon)
 163           then if eqd_dec ec ec' then OK t''
 164             else Error "level mismatch in escapification"
 165           else Error "ill-typed escapification"
 166         | _ => Error "ill-typed escapification"
 167       end
 168   end.
 169