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 HaskKinds.
  10 Require Import HaskCoreLiterals.
  11 Require Import HaskCoreVars.
  12 Require Import HaskCoreTypes.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskWeakVars.
  15 Require Import HaskWeakTypes.
  16
  17 Inductive WeakExpr :=
  18 | WEVar       : WeakExprVar                                                  -> WeakExpr
  19 | WELit       : HaskLiteral                                                  -> WeakExpr
  20 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  21 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  22 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
  23 | WENote      : Note                            -> WeakExpr                  -> WeakExpr
  24 | WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
  25 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
  26 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
  27 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  28 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
  29 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
  30
  31 (* the WeakType argument in WEBrak/WEEsc is used only when going back    *)
  32 (* from Weak to Core; it lets us dodge a possibly-failing type           *)
  33 (* calculation                                                           *)
  34 | WEBrak      : WeakTypeVar                     -> WeakExpr  -> WeakType     -> WeakExpr
  35 | WEEsc       : WeakTypeVar                     -> WeakExpr  -> WeakType     -> WeakExpr
  36
  37 (* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
  38 | WECase      : forall (scrutinee:WeakExpr)
  39                        (tbranches:WeakType)
  40                        (tc:TyCon)
  41                        (type_params:list WeakType)
  42                        (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
  43                        WeakExpr.
  44
  45 (* calculate the free WeakVar's in a WeakExpr *)
  46 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
  47   match me with
  48     | WELit    _        =>     nil
  49     | WEVar    cv       => cv::nil
  50     | WECast   e co     =>                            getWeakExprFreeVars e
  51     | WENote   n e      =>                            getWeakExprFreeVars e
  52     | WETyApp  e t      =>                            getWeakExprFreeVars e
  53     | WECoApp  e co     =>                            getWeakExprFreeVars e
  54     | WEBrak   ec e _   =>                            getWeakExprFreeVars e
  55     | WEEsc    ec e _   =>                            getWeakExprFreeVars e
  56     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
  57     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
  58     | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
  59     | WETyLam  cv e     => getWeakExprFreeVars e
  60     | WECoLam  cv e     => getWeakExprFreeVars e
  61
  62     (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *)
  63     | WECase scrutinee tbranches tc type_params alts =>
  64       mergeDistinctLists (getWeakExprFreeVars scrutinee) (
  65         ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
  66           {struct alts} : list WeakExprVar :=
  67           match alts with
  68             | T_Leaf  None                                  => nil
  69             | T_Leaf (Some (DEFAULT,_,_,_,e))                   => getWeakExprFreeVars e
  70             | T_Leaf (Some (LitAlt lit,_,_,_,e))                => getWeakExprFreeVars e
  71             | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e))  => removeFromDistinctList' evars (getWeakExprFreeVars e)
  72             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
  73           end) alts))
  74     | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
  75       match mlr with
  76         | T_Leaf None          => cvl
  77         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
  78         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
  79       end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
  80         ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  81           match mlr with
  82             | T_Leaf None          => nil
  83             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
  84             | T_Branch b1 b2       => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
  85           end) mlr))
  86   end.
  87
  88 (* wrap lambdas around an expression until it has no free expression variables *)
  89 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
  90   fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
  91   match cvl with
  92     | nil      => me
  93     | cv::cvl' => WELam cv (closeExpression me cvl')
  94   end) me (getWeakExprFreeVars me).
  95
  96 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
  97   (WTyCon (haskLiteralToTyCon lit)).
  98
  99 (* calculate the CoreType of a WeakExpr *)
 100 Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
 101   match ce with
 102     | WEVar   (weakExprVar v t) => OK t
 103     | WELit   lit   => OK (weakTypeOfLiteral lit)
 104     | WEApp   e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
 105                        match t' with
 106                          | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
 107                          | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
 108                        end
 109     | WETyApp e t    => weakTypeOfWeakExpr e >>= fun te =>
 110                         match te with
 111                           | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
 112                           | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
 113                         end
 114     | WECoApp e co   => weakTypeOfWeakExpr e >>= fun te =>
 115                         match te with
 116                           | WCoFunTy t1 t2 t => OK t
 117                           | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
 118                         end
 119     | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
 120     | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
 121     | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
 122     | WELet   ev ve e            => weakTypeOfWeakExpr e
 123     | WELetRec rb e              => weakTypeOfWeakExpr e
 124     | WENote  n e                => weakTypeOfWeakExpr e
 125     | WECast  e (weakCoercion t1 t2 _) => OK t2
 126     | WECase  scrutinee tbranches tc type_params alts => OK tbranches
 127
 128     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
 129     | WEBrak  ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
 130     | WEEsc   ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
 131       match t' with
 132         | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
 133           if eqd_dec ec ec' then OK t''
 134             else Error "level mismatch in escapification"
 135         | _ => Error "ill-typed escapification"
 136       end
 137   end.
 138