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