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
  24 (* TO DO: add a WEWhere and use the source location to detect which one the user used *)
  25 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
  26 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
  27 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
  28 | WENote      : Note                            -> WeakExpr                  -> WeakExpr
  29 | WEApp       : WeakExpr                        -> WeakExpr                  -> WeakExpr
  30 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
  31 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
  32 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
  33 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
  34 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
  35
  36 (* The WeakType argument in WEBrak/WEEsc is used only when going back      *)
  37 (* from Weak to Core; it lets us dodge a possibly-failing type             *)
  38 (* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
  39 (* or hetmet_esc identifier                                                *)
  40 | WEBrak      : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  41 | WEEsc       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  42 | WECSP       : WeakExprVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
  43
  44 | WECase      : forall (vscrut:WeakExprVar)
  45                        (scrutinee:WeakExpr)
  46                        (tbranches:WeakType)
  47                        (tc:TyCon)
  48                        (type_params:list WeakType)
  49                        (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
  50                        WeakExpr.
  51
  52 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
  53   (WTyCon (haskLiteralToTyCon lit)).
  54