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