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 HaskWeakVars.
  13 Require Import HaskWeakTypes.
  14
  15 Inductive WeakAltCon :=
  16 | WeakDataAlt : CoreDataCon  -> WeakAltCon
  17 | WeakLitAlt  : HaskLiteral  -> WeakAltCon
  18 | WeakDEFAULT :                 WeakAltCon.
  19
  20 Inductive WeakExpr :=
  21 | WEVar       : WeakExprVar                                                  -> WeakExpr
  22 | WELit       : HaskLiteral                                                  -> WeakExpr
  23 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  24 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  25 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
  26 | WENote      : Note                            -> WeakExpr                  -> WeakExpr
  27 | WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
  28 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
  29 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
  30 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  31 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
  32 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
  33
  34 (* The WeakType argument in WEBrak/WEEsc is used only when going back      *)
  35 (* from Weak to Core; it lets us dodge a possibly-failing type             *)
  36 (* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
  37 (* or hetmet_esc identifier                                                *)
  38 | WEBrak      : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  39 | WEEsc       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  40 | WECSP       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  41
  42 | WECase      : forall (vscrut:WeakExprVar)
  43                        (scrutinee:WeakExpr)
  44                        (tbranches:WeakType)
  45                        (tc:TyCon)
  46                        (type_params:list WeakType)
  47                        (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
  48                        WeakExpr.
  49
  50 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
  51   (WTyCon (haskLiteralToTyCon lit)).
  52