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 HaskLiterals.
  11 Require Import HaskTyCons.
  12 Require Import HaskCoreVars.
  13 Require Import HaskWeakVars.
  14 Require Import HaskWeakTypes.
  15
  16 Inductive WeakAltCon :=
  17 | WeakDataAlt : CoreDataCon  -> WeakAltCon
  18 | WeakLitAlt  : HaskLiteral  -> WeakAltCon
  19 | WeakDEFAULT :                 WeakAltCon.
  20
  21 Inductive WeakExpr :=
  22 | WEVar       : WeakExprVar                                                  -> WeakExpr
  23 | WELit       : HaskLiteral                                                  -> WeakExpr
  24
  25 (* TO DO: add a WEWhere and use the source location to detect which one the user used *)
  26 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  27 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  28 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
  29 | WENote      : Note                            -> WeakExpr                  -> WeakExpr
  30 | WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
  31 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
  32 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
  33 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  34 (*
  35 | WEKappa     : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  36 | WEKappaApp  : WeakExpr                        -> WeakExpr                  -> WeakExpr
  37 *)
  38 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
  39 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
  40
  41 (* The WeakType argument in WEBrak/WEEsc is used only when going back      *)
  42 (* from Weak to Core; it lets us dodge a possibly-failing type             *)
  43 (* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
  44 (* or hetmet_esc identifier                                                *)
  45 | WEBrak      : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  46 | WEEsc       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  47 | WECSP       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  48
  49 | WECase      : forall (vscrut:WeakExprVar)
  50                        (scrutinee:WeakExpr)
  51                        (tbranches:WeakType)
  52                        (tc:TyCon)
  53                        (type_params:list WeakType)
  54                        (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
  55                        WeakExpr.
  56
  57 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
  58   (WTyCon (haskLiteralToTyCon lit)).
  59
  60 (*
  61 Fixpoint weakExprVarOccursFree (wvf:WeakExprVar)(we:WeakExpr) : bool :=
  62   match we with
  63   | WEVar   wv                           => if eqd_dec (wvf:CoreVar) (wv:CoreVar) then true else false
  64   | WELit   lit                          => false
  65   | WEApp   e1 e2                        => weakExprVarOccursFree wvf e1 || weakExprVarOccursFree wvf e2
  66   | WETyApp e t                          => weakExprVarOccursFree wvf e
  67   | WECoApp e co                         => weakExprVarOccursFree wvf e
  68   | WENote  n e                          => weakExprVarOccursFree wvf e
  69   | WELam   ev e                         => if eqd_dec (wvf:CoreVar) (ev:CoreVar) then false else weakExprVarOccursFree wvf e
  70   | WETyLam tv e                         => weakExprVarOccursFree wvf e
  71   | WECoLam cv e                         => weakExprVarOccursFree wvf e
  72   | WECast  e co                         => weakExprVarOccursFree wvf e
  73   | WEBrak  v wtv e t                    => weakExprVarOccursFree wvf e
  74   | WEEsc   v wtv e t                    => weakExprVarOccursFree wvf e
  75   | WECSP   v wtv e t                    => weakExprVarOccursFree wvf e
  76   | WELet   v ebind ebody                => weakExprVarOccursFree wvf ebind
  77                                             || if eqd_dec (wvf:CoreVar) (v:CoreVar) then false else weakExprVarOccursFree wvf ebody
  78   | WECase  vs es tb tc tys alts         =>
  79     if weakExprVarOccursFree wvf es
  80       then true
  81       else (fix weakExprVarOccursFreeBranches (alts:Tree ??(_)) : bool :=
  82         match alts with
  83           | T_Leaf None     => false
  84           | T_Leaf (Some (_,_,_,v',e')) =>
  85             if fold_left bor (map (fun v'':WeakExprVar => if eqd_dec (wvf:CoreVar) (v'':CoreVar) then true else false ) v') false
  86               then false
  87               else weakExprVarOccursFree wvf e'
  88           | T_Branch b1 b2  => weakExprVarOccursFreeBranches b1 ||
  89             weakExprVarOccursFreeBranches b2
  90         end) alts
  91   | WELetRec mlr e                       => false
  92   end.
  93
  94 (* some very simple-minded cleanups to produce "prettier" expressions *)
  95 Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr :=
  96   match me with
  97   | WEVar   wv                           => WEVar wv
  98   | WELit   lit                          => WELit lit
  99   | WEApp   e1 e2                        => WEApp        (simplifyWeakExpr e1) (simplifyWeakExpr e2)
 100   | WETyApp e t                          => WETyApp      (simplifyWeakExpr e ) t
 101   | WECoApp e co                         => CoreEApp     (simplifyWeakExpr e ) co
 102   | WENote  n e                          => CoreENote n  (simplifyWeakExpr e )
 103   | WELam   ev e                         => CoreELam  ev (simplifyWeakExpr e )
 104   | WETyLam tv e                         => CoreELam  tv (simplifyWeakExpr e )
 105   | WECoLam cv e                         => CoreELam  cv (simplifyWeakExpr e )
 106   | WECast  e co                         => CoreECast    (simplifyWeakExpr e ) co
 107   | WEBrak  v wtv e t                    => WEBrak v wtv (simplifyWeakExpr e ) t
 108   | WEEsc   v wtv e t                    => WEEsc  v wtv (simplifyWeakExpr e ) t
 109   | WECSP   v wtv e t                    => WECSP  v wtv (simplifyWeakExpr e ) t
 110   | WELet   v ebind ebody                => WELet  v (simplifyWeakExpr ebind) (simplifyWeakExpr ebody)
 111   | WECase  vs es tb tc tys alts         => WECase vs es tb tc tys (* FIXME alts *)
 112   (* un-letrec-ify multi branch letrecs *)
 113   | WELetRec mlr e                       => WELetRec mlr (simplifyWeakExpr e )
 114   end.
 115 *)