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