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 HaskCoreVars.
13 Require Import HaskWeakVars.
14 Require Import HaskWeakTypes.
16 Inductive WeakAltCon :=
17 | WeakDataAlt : CoreDataCon -> WeakAltCon
18 | WeakLitAlt : HaskLiteral -> WeakAltCon
19 | WeakDEFAULT : WeakAltCon.
22 | WEVar : WeakExprVar -> WeakExpr
23 | WELit : HaskLiteral -> WeakExpr
25 (* TO DO: add a WEWhere and use the source location to detect which one the user used *)
26 | WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr
27 | WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr
28 | WECast : WeakExpr -> WeakCoercion -> WeakExpr
29 | WENote : Note -> WeakExpr -> WeakExpr
30 | WEApp : WeakExpr -> WeakExpr -> WeakExpr
31 | WETyApp : WeakExpr -> WeakType -> WeakExpr
32 | WECoApp : WeakExpr -> WeakCoercion -> WeakExpr
33 | WELam : WeakExprVar -> WeakExpr -> WeakExpr
35 | WEKappa : WeakExprVar -> WeakExpr -> WeakExpr
36 | WEKappaApp : WeakExpr -> WeakExpr -> WeakExpr
38 | WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
39 | WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
41 (* The WeakType argument in WEBrak/WEEsc is used only when going back *)
42 (* from Weak to Core; it lets us dodge a possibly-failing type *)
43 (* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *)
44 (* or hetmet_esc identifier *)
45 | WEBrak : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
46 | WEEsc : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
47 | WECSP : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
49 | WECase : forall (vscrut:WeakExprVar)
53 (type_params:list WeakType)
54 (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
57 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
58 (WTyCon (haskLiteralToTyCon lit)).
61 Fixpoint weakExprVarOccursFree (wvf:WeakExprVar)(we:WeakExpr) : bool :=
63 | WEVar wv => if eqd_dec (wvf:CoreVar) (wv:CoreVar) then true else false
65 | WEApp e1 e2 => weakExprVarOccursFree wvf e1 || weakExprVarOccursFree wvf e2
66 | WETyApp e t => weakExprVarOccursFree wvf e
67 | WECoApp e co => weakExprVarOccursFree wvf e
68 | WENote n e => weakExprVarOccursFree wvf e
69 | WELam ev e => if eqd_dec (wvf:CoreVar) (ev:CoreVar) then false else weakExprVarOccursFree wvf e
70 | WETyLam tv e => weakExprVarOccursFree wvf e
71 | WECoLam cv e => weakExprVarOccursFree wvf e
72 | WECast e co => weakExprVarOccursFree wvf e
73 | WEBrak v wtv e t => weakExprVarOccursFree wvf e
74 | WEEsc v wtv e t => weakExprVarOccursFree wvf e
75 | WECSP v wtv e t => weakExprVarOccursFree wvf e
76 | WELet v ebind ebody => weakExprVarOccursFree wvf ebind
77 || if eqd_dec (wvf:CoreVar) (v:CoreVar) then false else weakExprVarOccursFree wvf ebody
78 | WECase vs es tb tc tys alts =>
79 if weakExprVarOccursFree wvf es
81 else (fix weakExprVarOccursFreeBranches (alts:Tree ??(_)) : bool :=
83 | T_Leaf None => false
84 | T_Leaf (Some (_,_,_,v',e')) =>
85 if fold_left bor (map (fun v'':WeakExprVar => if eqd_dec (wvf:CoreVar) (v'':CoreVar) then true else false ) v') false
87 else weakExprVarOccursFree wvf e'
88 | T_Branch b1 b2 => weakExprVarOccursFreeBranches b1 ||
89 weakExprVarOccursFreeBranches b2
91 | WELetRec mlr e => false
94 (* some very simple-minded cleanups to produce "prettier" expressions *)
95 Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr :=
97 | WEVar wv => WEVar wv
98 | WELit lit => WELit lit
99 | WEApp e1 e2 => WEApp (simplifyWeakExpr e1) (simplifyWeakExpr e2)
100 | WETyApp e t => WETyApp (simplifyWeakExpr e ) t
101 | WECoApp e co => CoreEApp (simplifyWeakExpr e ) co
102 | WENote n e => CoreENote n (simplifyWeakExpr e )
103 | WELam ev e => CoreELam ev (simplifyWeakExpr e )
104 | WETyLam tv e => CoreELam tv (simplifyWeakExpr e )
105 | WECoLam cv e => CoreELam cv (simplifyWeakExpr e )
106 | WECast e co => CoreECast (simplifyWeakExpr e ) co
107 | WEBrak v wtv e t => WEBrak v wtv (simplifyWeakExpr e ) t
108 | WEEsc v wtv e t => WEEsc v wtv (simplifyWeakExpr e ) t
109 | WECSP v wtv e t => WECSP v wtv (simplifyWeakExpr e ) t
110 | WELet v ebind ebody => WELet v (simplifyWeakExpr ebind) (simplifyWeakExpr ebody)
111 | WECase vs es tb tc tys alts => WECase vs es tb tc tys (* FIXME alts *)
112 (* un-letrec-ify multi branch letrecs *)
113 | WELetRec mlr e => WELetRec mlr (simplifyWeakExpr e )