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 HaskCore.
  12 Require Import HaskCoreVars.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskCoreTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeakTypes.
  17
  18 Inductive WeakExpr :=
  19 | WEVar       : WeakExprVar                                                  -> WeakExpr
  20 | WELit       : HaskLiteral                                                  -> WeakExpr
  21 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  22 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  23 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
  24 | WENote      : Note                            -> WeakExpr                  -> WeakExpr
  25 | WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
  26 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
  27 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
  28 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  29 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
  30 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
  31
  32 (* The WeakType argument in WEBrak/WEEsc is used only when going back      *)
  33 (* from Weak to Core; it lets us dodge a possibly-failing type             *)
  34 (* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
  35 (* or hetmet_esc identifier                                                *)
  36 | WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  37 | WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  38
  39 | WECase      : forall (vscrut:WeakExprVar)
  40                        (scrutinee:WeakExpr)
  41                        (tbranches:WeakType)
  42                        (tc:TyCon)
  43                        (type_params:list WeakType)
  44                        (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
  45                        WeakExpr.
  46
  47 (* calculate the free WeakVar's in a WeakExpr *)
  48 (*
  49 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
  50   match me with
  51     | WELit    _        =>     nil
  52     | WEVar    cv       => cv::nil
  53     | WECast   e co     =>                            getWeakExprFreeVars e
  54     | WENote   n e      =>                            getWeakExprFreeVars e
  55     | WETyApp  e t      =>                            getWeakExprFreeVars e
  56     | WECoApp  e co     =>                            getWeakExprFreeVars e
  57     | WEBrak   ec e _   =>                            getWeakExprFreeVars e
  58     | WEEsc    ec e _   =>                            getWeakExprFreeVars e
  59     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
  60     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
  61     | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
  62     | WETyLam  cv e     => getWeakExprFreeVars e
  63     | WECoLam  cv e     => getWeakExprFreeVars e
  64
  65     (* the messy fixpoints below are required by Coq's termination conditions; trust me, I tried to get rid of them *)
  66     | WECase scrutinee tbranches tc type_params alts =>
  67       mergeDistinctLists (getWeakExprFreeVars scrutinee) (
  68         ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
  69           {struct alts} : list WeakExprVar :=
  70           match alts with
  71             | T_Leaf  None                                  => nil
  72             | T_Leaf (Some (DEFAULT,_,_,_,e))                   => getWeakExprFreeVars e
  73             | T_Leaf (Some (LitAlt lit,_,_,_,e))                => getWeakExprFreeVars e
  74             | T_Leaf (Some ((DataAlt dc), tvars, cvars, evars,e))  => removeFromDistinctList' evars (getWeakExprFreeVars e)
  75             | T_Branch b1 b2                        => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
  76           end) alts))
  77     | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
  78       match mlr with
  79         | T_Leaf None          => cvl
  80         | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
  81         | T_Branch b1 b2       => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
  82       end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
  83         ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
  84           match mlr with
  85             | T_Leaf None          => nil
  86             | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
  87             | T_Branch b1 b2       => mergeDistinctLists (getWeakExprFreeVarsLetRec b1) (getWeakExprFreeVarsLetRec b2)
  88           end) mlr))
  89   end.
  90
  91 (* wrap lambdas around an expression until it has no free expression variables *)
  92 Definition makeClosedExpression : WeakExpr -> WeakExpr :=
  93   fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
  94   match cvl with
  95     | nil      => me
  96     | cv::cvl' => WELam cv (closeExpression me cvl')
  97   end) me (getWeakExprFreeVars me).
  98 *)
  99 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
 100   (WTyCon (haskLiteralToTyCon lit)).
 101
 102 Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
 103   Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".