1 (*********************************************************************************************************************************)
2 (* HaskStrongToWeak: convert HaskStrong to HaskWeak *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskCoreLiterals.
14 Require Import HaskCoreVars.
15 Require Import HaskCoreTypes.
16 Require Import HaskCore.
17 Require Import HaskWeakTypes.
18 Require Import HaskWeakVars.
19 Require Import HaskWeak.
20 Require Import HaskStrongTypes.
21 Require Import HaskStrong.
23 Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
24 : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
25 match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) *
26 (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
27 | nil => (f,(vec_nil,ite))
29 let (f',varsite') := mfresh f lk' ite
30 in let (vars,ite') := varsite'
31 in let (v,f'') := next _ _ f' k
32 in (f'',((v:::vars),v::::ite'))
35 Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
36 {struct rht} : WeakType :=
38 | TVar _ v => WTyVarTy v
39 | TCon tc => WTyCon tc
40 | TCoerc _ t1 t2 t3 => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3)
42 | TApp _ _ t1 t2 => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2)
43 | TAll k rht' => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv))
45 match (rawHaskTypeToWeakType f t1) with
46 | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2)
47 | impossible => impossible (* TODO: find a way to convince Coq this can't happen *)
49 | TyFunApp tfc tls => WTyFunApp tfc (rawHaskTypeListToWeakType f tls)
51 with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) :=
54 | TyFunApp_cons κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl')
57 Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
58 {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
59 rawHaskTypeToWeakType f (τ _ φ).
61 (* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
62 * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
64 Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
65 {Γ}{Δ}{ξ}{lev}(exp:@Expr VV eqVV Γ Δ ξ lev) : { ξ' : HH -> LeveledHaskType Γ & @Expr HH eqHH Γ Δ ξ' lev }.
69 Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
72 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
74 Section strongExprToWeakExpr.
76 Context (hetmet_brak : CoreVar).
77 Context (hetmet_esc : CoreVar).
79 Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
80 (ftv:Fresh Kind (fun _ => WeakTypeVar))
81 (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
82 (fev:Fresh WeakType (fun _ => WeakExprVar))
83 (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
84 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
85 match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
86 | EVar Γ' _ ξ' ev => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★ (unlev (ξ' ev)) ite))
87 | ELit _ _ _ lit _ => fun ite => WELit lit
88 | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv fev e1 ite) (strongExprToWeakExpr ftv fcv fev e2 ite)
89 | ELam Γ' _ _ _ t _ cv e => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv fev e ite)
90 | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv fev e1 ite) (strongExprToWeakExpr ftv fcv fev e2 ite)
91 | EEsc Γ' _ _ ec t _ e => fun ite => WEEsc hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv t ite)
92 | EBrak Γ' _ _ ec t _ e => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv t ite)
93 | ENote _ _ _ _ n e => fun ite => WENote n (strongExprToWeakExpr ftv fcv fev e ite)
94 | ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv τ ite)
95 | ELetRec _ _ _ _ _ vars elrb e => fun ite => WELetRec (exprLetRec2WeakExprLetRec ftv fcv fev elrb ite)(strongExprToWeakExpr ftv fcv fev e ite)
96 | ECast Γ Δ ξ t1 t2 γ l e => fun ite => Prelude_error "FIXME: strongExprToWeakExpr.ECast not implemented"
97 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => Prelude_error "FIXME: strongExprToWeakExpr.ECoApp not implemented"
98 | ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite =>
99 let (ev,fev') := next _ _ fev (typeToWeakType ftv (unlev (caseType tc atypes @@ l)) ite) in
102 (strongExprToWeakExpr ftv fcv fev' e ite)
103 (@typeToWeakType ftv Γ _ tbranches ite)
105 (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes))
107 (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
109 (sac_Δ scb Γ atypes (weakCK'' Δ))
110 (update_ξ (weakLT'○ξ) (vec2list (vec_map
111 (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
112 (weakLT' (tbranches@@l)) })
113 : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
116 | T_Leaf (Some x) => let (scb,e) := x in
117 let (ftv',evarsite') := mfresh ftv _ ite in
119 let (evars,ite') := evarsite' in
123 map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)),
124 strongExprToWeakExpr ftv' fcv' fev' e ite'
126 | T_Branch b1 b2 => (caseBranches b1),,(caseBranches b2)
129 | ETyLam _ _ _ k _ _ e => fun ite =>
130 let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv fev e (updateITE tv ite))
131 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite =>
132 let t1' := typeToWeakType ftv σ₁ ite in
133 let t2' := typeToWeakType ftv σ₂ ite in
134 let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' fev e ite)
136 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars}
137 (ftv:Fresh Kind (fun _ => WeakTypeVar))
138 (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
139 (fev:Fresh WeakType (fun _ => WeakExprVar))
140 (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars)
141 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) :=
142 match elrb as E in ELetRecBindings G D X L V
143 return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with
144 | ELR_nil _ _ _ _ => fun ite => []
145 | ELR_leaf _ _ ξ' cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv fev e ite))]
146 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv fev b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv fev b2 ite)
148 End strongExprToWeakExpr.