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 HaskLiterals.
11 Require Import HaskTyCons.
12 Require Import HaskWeakVars.
13 Require Import HaskWeakTypes.
15 Inductive WeakAltCon :=
16 | WeakDataAlt : CoreDataCon -> WeakAltCon
17 | WeakLitAlt : HaskLiteral -> WeakAltCon
18 | WeakDEFAULT : WeakAltCon.
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
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
42 | WECase : forall (vscrut:WeakExprVar)
46 (type_params:list WeakType)
47 (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
50 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
51 (WTyCon (haskLiteralToTyCon lit)).