1 (*********************************************************************************************************************************)
2 (* HaskWeak: a non-dependently-typed but Coq-friendly version of HaskCore *)
3 (*********************************************************************************************************************************)
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.
14 Inductive WeakAltCon :=
15 | WeakDataAlt : CoreDataCon -> WeakAltCon
16 | WeakLitAlt : HaskLiteral -> WeakAltCon
17 | WeakDEFAULT : WeakAltCon.
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
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
41 | WECase : forall (vscrut:WeakExprVar)
45 (type_params:list WeakType)
46 (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
49 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
50 (WTyCon (haskLiteralToTyCon lit)).