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