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 (*
  47 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
  48   match me with
  49     | WELit    _        =>     nil
  50     | WEVar    cv       => cv::nil
  51     | WECast   e co     =>                            getWeakExprFreeVars e
  52     | WENote   n e      =>                            getWeakExprFreeVars e
  53     | WETyApp  e t      =>                            getWeakExprFreeVars e
  54     | WECoApp  e co     =>                            getWeakExprFreeVars e
  55     | WEBrak   ec e _   =>                            getWeakExprFreeVars e
  56     | WEEsc    ec e _   =>                            getWeakExprFreeVars e
  57     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
  58     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
  59     | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
  60     | WETyLam  cv e     => getWeakExprFreeVars e
  61     | WECoLam  cv e     => getWeakExprFreeVars e
  62
  63     (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *)
  64     | WECase scrutinee tbranches tc type_params alts =>
  65       mergeDistinctLists (getWeakExprFreeVars scrutinee) (
  66         ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
  67           {struct alts} : list WeakExprVar :=
  68           match alts with
  69             | T_Leaf  None                                  => nil
  70             | T_Leaf (Some (DEFAULT,_,_,_,e))                   => getWeakExprFreeVars e
  71             | T_Leaf (Some (LitAlt lit,_,_,_,e))                => getWeakExprFreeVars e
  72             | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e))  => removeFromDistinctList' evars (getWeakExprFreeVars e)
  73             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
  74           end) alts))
  75     | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
  76       match mlr with
  77         | T_Leaf None          => cvl
  78         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
  79         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
  80       end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
  81         ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  82           match mlr with
  83             | T_Leaf None          => nil
  84             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
  85             | T_Branch b1 b2       => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
  86           end) mlr))
  87   end.
  88
  89 (* wrap lambdas around an expression until it has no free expression variables *)
  90 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
  91   fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
  92   match cvl with
  93     | nil      => me
  94     | cv::cvl' => WELam cv (closeExpression me cvl')
  95   end) me (getWeakExprFreeVars me).
  96 *)
  97 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
  98   (WTyCon (haskLiteralToTyCon lit)).
  99
 100 (* calculate the CoreType of a WeakExpr *)
 101 Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
 102   match ce with
 103     | WEVar   (weakExprVar v t) => OK t
 104     | WELit   lit   => OK (weakTypeOfLiteral lit)
 105     | WEApp   e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
 106                        match t' with
 107                          | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
 108                          | _ => Error ("found non-function type "+++t'+++" in EApp")
 109                        end
 110     | WETyApp e t    => weakTypeOfWeakExpr e >>= fun te =>
 111                         match te with
 112                           | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
 113                           | _ => Error ("found non-forall type "+++te+++" in ETyApp")
 114                         end
 115     | WECoApp e co   => weakTypeOfWeakExpr e >>= fun te =>
 116                         match te with
 117                           | WCoFunTy t1 t2 t => OK t
 118                           | _ => Error ("found non-coercion type "+++te+++" in ETyApp")
 119                         end
 120     | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
 121     | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
 122     | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
 123     | WELet   ev ve e            => weakTypeOfWeakExpr e
 124     | WELetRec rb e              => weakTypeOfWeakExpr e
 125     | WENote  n e                => weakTypeOfWeakExpr e
 126     | WECast  e (weakCoercion t1 t2 _) => OK t2
 127     | WECase  scrutinee tbranches tc type_params alts => OK tbranches
 128
 129     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
 130     | WEBrak  ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
 131     | WEEsc   ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
 132       match t' with
 133         | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
 134           if eqd_dec ec ec' then OK t''
 135             else Error "level mismatch in escapification"
 136         | _ => Error "ill-typed escapification"
 137       end
 138   end.
 139