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
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
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
44 | WECase : forall (vscrut:WeakExprVar)
48 (type_params:list WeakType)
49 (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
52 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
53 (WTyCon (haskLiteralToTyCon lit)).