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
34 | WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
35 | WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
37 (* The WeakType argument in WEBrak/WEEsc is used only when going back *)
38 (* from Weak to Core; it lets us dodge a possibly-failing type *)
39 (* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *)
40 (* or hetmet_esc identifier *)
41 | WEBrak : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
42 | WEEsc : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
43 | WECSP : WeakExprVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
45 | WECase : forall (vscrut:WeakExprVar)
49 (type_params:list WeakType)
50 (alts : Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)),
53 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
54 (WTyCon (haskLiteralToTyCon lit)).
57 Fixpoint weakExprVarOccursFree (wvf:WeakExprVar)(we:WeakExpr) : bool :=
59 | WEVar wv => if eqd_dec (wvf:CoreVar) (wv:CoreVar) then true else false
61 | WEApp e1 e2 => weakExprVarOccursFree wvf e1 || weakExprVarOccursFree wvf e2
62 | WETyApp e t => weakExprVarOccursFree wvf e
63 | WECoApp e co => weakExprVarOccursFree wvf e
64 | WENote n e => weakExprVarOccursFree wvf e
65 | WELam ev e => if eqd_dec (wvf:CoreVar) (ev:CoreVar) then false else weakExprVarOccursFree wvf e
66 | WETyLam tv e => weakExprVarOccursFree wvf e
67 | WECoLam cv e => weakExprVarOccursFree wvf e
68 | WECast e co => weakExprVarOccursFree wvf e
69 | WEBrak v wtv e t => weakExprVarOccursFree wvf e
70 | WEEsc v wtv e t => weakExprVarOccursFree wvf e
71 | WECSP v wtv e t => weakExprVarOccursFree wvf e
72 | WELet v ebind ebody => weakExprVarOccursFree wvf ebind
73 || if eqd_dec (wvf:CoreVar) (v:CoreVar) then false else weakExprVarOccursFree wvf ebody
74 | WECase vs es tb tc tys alts =>
75 if weakExprVarOccursFree wvf es
77 else (fix weakExprVarOccursFreeBranches (alts:Tree ??(_)) : bool :=
79 | T_Leaf None => false
80 | T_Leaf (Some (_,_,_,v',e')) =>
81 if fold_left bor (map (fun v'':WeakExprVar => if eqd_dec (wvf:CoreVar) (v'':CoreVar) then true else false ) v') false
83 else weakExprVarOccursFree wvf e'
84 | T_Branch b1 b2 => weakExprVarOccursFreeBranches b1 ||
85 weakExprVarOccursFreeBranches b2
87 | WELetRec mlr e => false
90 (* some very simple-minded cleanups to produce "prettier" expressions *)
91 Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr :=
93 | WEVar wv => WEVar wv
94 | WELit lit => WELit lit
95 | WEApp e1 e2 => WEApp (simplifyWeakExpr e1) (simplifyWeakExpr e2)
96 | WETyApp e t => WETyApp (simplifyWeakExpr e ) t
97 | WECoApp e co => CoreEApp (simplifyWeakExpr e ) co
98 | WENote n e => CoreENote n (simplifyWeakExpr e )
99 | WELam ev e => CoreELam ev (simplifyWeakExpr e )
100 | WETyLam tv e => CoreELam tv (simplifyWeakExpr e )
101 | WECoLam cv e => CoreELam cv (simplifyWeakExpr e )
102 | WECast e co => CoreECast (simplifyWeakExpr e ) co
103 | WEBrak v wtv e t => WEBrak v wtv (simplifyWeakExpr e ) t
104 | WEEsc v wtv e t => WEEsc v wtv (simplifyWeakExpr e ) t
105 | WECSP v wtv e t => WECSP v wtv (simplifyWeakExpr e ) t
106 | WELet v ebind ebody => WELet v (simplifyWeakExpr ebind) (simplifyWeakExpr ebody)
107 | WECase vs es tb tc tys alts => WECase vs es tb tc tys (* FIXME alts *)
108 (* un-letrec-ify multi branch letrecs *)
109 | WELetRec mlr e => WELetRec mlr (simplifyWeakExpr e )