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