1 (*********************************************************************************************************************************)
2 (* HaskWeakToStrong: convert HaskWeak to HaskStrong *)
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 HaskWeakTypes.
15 Require Import HaskWeakVars.
16 Require Import HaskWeak.
17 Require Import HaskStrongTypes.
18 Require Import HaskStrong.
19 Require Import HaskCoreTypes.
21 Definition upφ {Γ}(tv:WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) : (WeakTypeVar -> HaskTyVar ((tv:Kind)::Γ)) :=
24 then FreshHaskTyVar (tv:Kind)
25 else fun TV ite => φ tv' TV (weakITE ite).
29 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ)
30 : (WeakTypeVar -> HaskTyVar (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
38 Open Scope string_scope.
40 Fixpoint weakTypeToType {Γ:TypeEnv}(φ:WeakTypeVar -> HaskTyVar Γ)(t:WeakType) : HaskType Γ :=
42 | WTyVarTy v => fun TV env => @TVar TV (φ v TV env)
43 | WCoFunTy t1 t2 t3 => (weakTypeToType φ t1) ∼∼ (weakTypeToType φ t2) ⇒ (weakTypeToType φ t3)
44 | WFunTyCon => fun TV env => TArrow
45 | WTyCon tc => fun TV env => TCon tc
46 | WTyFunApp tc lt => fun TV env => fold_left TApp (map (fun t => weakTypeToType φ t TV env) lt) (TCon tc) (* FIXME *)
47 | WClassP c lt => fun TV env => fold_left TApp (map (fun t=> weakTypeToType φ t TV env) lt) (TCon (classTyCon c))
48 | WIParam _ ty => weakTypeToType φ ty
49 | WForAllTy wtv t => (fun TV env => TAll (wtv:Kind) (fun tv => weakTypeToType (@upφ Γ wtv φ) t TV (tv:::env)))
50 | WAppTy t1 t2 => fun TV env => TApp (weakTypeToType φ t1 TV env) (weakTypeToType φ t2 TV env)
51 | WCodeTy ec tbody => fun TV env => TCode (TVar (φ ec TV env)) (weakTypeToType φ tbody TV env)
55 Definition substPhi0 {Γ:TypeEnv}(κ:Kind)(θ:HaskType Γ) : HaskType (κ::Γ) -> HaskType Γ.
59 unfold HaskType in ht.
62 apply vec_cons; [ idtac | apply env ].
66 Definition substPhi {Γ:TypeEnv}(κ:list Kind)(θ:vec (HaskType Γ) (length κ)) : HaskType (app κ Γ) -> HaskType Γ.
72 inversion θ; subst; auto.
74 apply (substPhi0 _ (weakT' X) q).
77 Definition substφ {Γ}{n}(ltypes:vec (HaskType Γ) n)(Γ':vec _ n)(ht:HaskType (app (vec2list Γ') Γ)) : HaskType Γ.
78 apply (@substPhi Γ (vec2list Γ')).
84 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
85 Record StrongAltConPlusJunk {tc:TyCon} :=
86 { sacpj_sac : @StrongAltCon tc
87 ; sacpj_φ : forall Γ (φ:WeakTypeVar -> HaskTyVar Γ ), (WeakTypeVar -> HaskTyVar (sac_Γ sacpj_sac Γ))
88 ; sacpj_ψ : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
89 (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)))
91 Implicit Arguments StrongAltConPlusJunk [ ].
92 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
94 (* yes, I know, this is really clumsy *)
95 Variable emptyφ : WeakTypeVar -> HaskTyVar nil.
96 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
98 Definition mkPhi (lv:list WeakTypeVar)
99 : (WeakTypeVar -> HaskTyVar (map (fun x:WeakTypeVar => x:Kind) lv)).
100 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
101 rewrite <- app_nil_end in φ'.
105 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
106 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
108 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
109 Section StrongAltCon.
110 Context (tc : TyCon)(dc:DataCon tc).
112 Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
115 set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
116 set (@substφ _ _ avars') as q.
117 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
118 set (@weakTypeToType _ φ' ct) as t.
119 set (@weakT'' _ Γ t) as t'.
120 set (@lamer _ _ _ t') as t''.
121 fold (tyConKinds tc) in t''.
122 fold (dataConExKinds dc) in t''.
123 apply (q (tyConKinds tc)).
125 unfold dataConExKinds.
126 rewrite <- vec2list_map_list2vec.
127 rewrite <- vec2list_map_list2vec.
128 rewrite vec2list_list2vec.
129 rewrite vec2list_list2vec.
133 Definition mkStrongAltCon : @StrongAltCon tc.
135 {| sac_altcon := DataAlt dc
136 ; sac_numCoerVars := length (dataConCoerKinds dc)
137 ; sac_numExprVars := length (dataConFieldTypes dc)
138 ; sac_akinds := tyConKinds tc
139 ; sac_ekinds := dataConExKinds dc
140 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
141 ; sac_types := fun Γ avars => let case_sac_types := tt in _
144 destruct case_sac_coercions.
145 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
148 apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
150 destruct case_sac_types.
151 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
153 apply (weakTypeToType' avars).
157 Lemma weakCV' : forall {Γ}{Δ} Γ',
159 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
161 unfold HaskCoVar in *.
162 intros; apply (X TV CV).
163 apply vec_chop' in env; auto.
164 unfold InstantiatedCoercionEnv in *.
165 unfold weakCK'' in cenv.
168 rewrite <- map_preserves_length in cenv.
172 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
174 {| sacpj_sac := mkStrongAltCon
175 ; sacpj_φ := fun Γ φ => (fun htv => weakV' (φ htv))
176 ; sacpj_ψ := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
180 unfold HaskCoVar in *.
185 unfold InstantiatedCoercionEnv in *.
186 apply vec_chop' in cenv.
191 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
193 set (c:DataCon _) as dc.
194 set ((dataConTyCon c):TyCon) as tc' in *.
195 set (eqd_dec tc tc') as eqpf; destruct eqpf;
197 | apply (Error ("in a case of tycon "+++tyConToString tc+++", found a branch with datacon "+++dataConToString dc)) ]; subst.
199 eapply mkStrongAltConPlusJunk.
203 apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
204 ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
205 ; sac_altcon := LitAlt h
207 intro; intro φ; apply φ.
208 intro; intro; intro; intro ψ; apply ψ.
209 apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
210 ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
211 ; sac_altcon := DEFAULT |} |}.
212 intro; intro φ; apply φ.
213 intro; intro; intro; intro ψ; apply ψ.
216 Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ) :=
219 | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
220 | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
223 Open Scope string_scope.
224 Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end.
226 Definition Indexed_Bind T f t (e:@Indexed T f t) : forall Q, (forall t, f t -> ???Q) -> ???Q.
229 apply (Error error_message).
232 Notation "a >>>= b" := (@Indexed_Bind _ _ _ a _ b) (at level 20).
234 Definition DoublyIndexed_Bind T f t (e:@Indexed T (fun z => ???(f z)) t) : forall Q, (forall t, f t -> ???Q) -> ???Q.
240 apply (Error error_message).
244 Notation "a >>>>= b" := (@DoublyIndexed_Bind _ _ _ a _ b) (at level 20).
246 Ltac matchTypes T1 T2 S :=
247 destruct (eqd_dec T1 T2) as [matchTypes_pf|];
248 [ idtac | apply (Error ("type mismatch in "+++S+++": " +++ (weakTypeToString T1) +++ " and " +++ (weakTypeToString T2))) ].
249 Ltac matchTypeVars T1 T2 S :=
250 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
251 [ idtac | apply (Error ("type variable mismatch in"+++S)) ].
252 Ltac matchLevs L1 L2 S :=
253 destruct (eqd_dec L1 L2) as [matchLevs_pf|];
254 [ idtac | apply (Error ("level mismatch in "+++S)) ].
257 Definition cure {Γ}(ξ:WeakExprVar -> WeakType * list WeakTypeVar)(φ:WeakTypeVar->HaskTyVar Γ)
258 : WeakExprVar->LeveledHaskType Γ :=
259 fun wtv => weakTypeToType φ (fst (ξ wtv)) @@ map φ (snd (ξ wtv)).
261 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
262 fun wev => match wev with weakExprVar _ t => t end.
263 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
265 Fixpoint upξ (ξ:WeakExprVar -> WeakType * list WeakTypeVar)
266 (evs:list WeakExprVar)
267 (lev:list WeakTypeVar) :
268 (WeakExprVar -> WeakType * list WeakTypeVar) :=
272 | a::b => if eqd_dec wev a then ((wev:WeakType),lev) else upξ ξ b lev wev
275 Variable weakCoercionToHaskCoercion : forall Γ Δ, WeakCoercion -> HaskCoercion Γ Δ.
277 Notation "'checkit' ( Y ) X" := (match weakTypeOfWeakExpr Y as CTE return
278 CTE=weakTypeOfWeakExpr Y -> forall Γ Δ φ ψ ξ lev, Indexed _ CTE with
279 | Error s => fun _ _ _ _ _ _ _ => Indexed_Error _ s
280 | OK cte => fun cte_pf => (fun x Γ Δ φ ψ ξ lev => Indexed_OK _ _ (x Γ Δ φ ψ ξ lev)) X
281 end (refl_equal _)) (at level 10).
284 (* equality lemmas I have yet to prove *)
286 Lemma upξ_lemma Γ ξ v lev φ
287 : cure(Γ:=Γ) (upξ ξ (v :: nil) lev) φ = update_ξ (cure ξ φ) ((v,weakTypeToType φ v @@ map φ lev)::nil).
291 (* this is tricky because of the test for ModalBoxTyCon is a type index for tc and because the fold is a left-fold *)
293 Lemma letrec_lemma : forall Γ ξ φ rb lev,
294 let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in
298 (fun x : WeakExprVar * HaskType Γ =>
299 ⟨fst x, snd x @@ map φ lev ⟩) (leaves (mLetRecTypesVars rb φ)))).
303 Lemma case_lemma1 tc Γ avars' (sac:StrongAltConPlusJunk tc) vars ξ φ lev :
304 (@scbwv_ξ WeakExprVar WeakExprVarEqDecidable tc Γ avars'
305 {| scbwv_sac := sac; scbwv_exprvars := vars |}
306 (@cure Γ ξ φ) (@map WeakTypeVar (HaskTyVar Γ) φ lev))
307 = (cure ξ (sacpj_φ sac Γ φ)).
310 Lemma case_lemma2 tc Γ (sac:@StrongAltConPlusJunk tc) φ lev :
311 (map (sacpj_φ sac Γ φ) lev) = weakL' (map φ lev).
314 Lemma case_lemma3 Γ φ t tc (sac:@StrongAltConPlusJunk tc) :
315 (weakT' (weakTypeToType φ t) = weakTypeToType (sacpj_φ sac Γ φ) t).
318 Lemma case_lemma4 Γ φ (tc:TyCon) avars0 : forall Q1 Q2, (@weakTypeToType Γ φ Q2)=Q1 ->
319 fold_left HaskAppT (map (weakTypeToType φ) avars0) Q1 =
320 weakTypeToType φ (fold_left WAppTy avars0 Q2).
321 induction avars0; intros.
325 set (IHavars0 (HaskAppT Q1 (weakTypeToType φ a)) (WAppTy Q2 a)) as z.
334 Axiom assume_all_coercions_well_formed : forall Γ (Δ:CoercionEnv Γ) t1 t2 co, Δ ⊢ᴄᴏ co : t1 ∼ t2.
335 Axiom assume_all_types_well_formed : forall Γ t x, Γ ⊢ᴛy t : x.
337 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
338 WeakCoerVar -> HaskCoVar Γ (κ::Δ).
342 apply (ψ X TV CV env).
343 inversion cenv; auto.
346 Lemma substRaw {Γ}{κ} : HaskType (κ::Γ) -> (∀ TV, @InstantiatedTypeEnv TV Γ -> TV -> @RawHaskType TV).
355 Lemma substRaw_lemma : forall (Γ:TypeEnv) (φ:WeakTypeVar->HaskTyVar Γ) wt tsubst wtv,
356 substT (substRaw (weakTypeToType (upφ wtv φ) wt)) (weakTypeToType φ tsubst) =
357 weakTypeToType φ (replaceWeakTypeVar wt wtv tsubst).
361 Definition weakExprToStrongExpr : forall
365 (φ:WeakTypeVar->HaskTyVar Γ)
366 (ψ:WeakCoerVar->HaskCoVar Γ Δ)
367 (ξ:WeakExprVar->WeakType * list WeakTypeVar)
368 (lev:list WeakTypeVar)
370 Indexed (fun t' => ???(@Expr _ WeakExprVarEqDecidable Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev))))
371 (weakTypeOfWeakExpr ce).
373 fix weakExprToStrongExpr (ce:WeakExpr) {struct ce} : forall Γ Δ φ ψ ξ lev,
374 Indexed (fun t' => ???(Expr Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev)))) (weakTypeOfWeakExpr ce) :=
375 (match ce as CE return (forall Γ Δ φ ψ ξ lev, Indexed _ (weakTypeOfWeakExpr CE))
377 | WEVar v => let case_WEVar := tt in checkit (WEVar v) (fun Γ Δ φ ψ ξ lev => _)
378 | WELit lit => let case_WELit := tt in checkit (WELit lit) (fun Γ Δ φ ψ ξ lev => _)
379 | WEApp e1 e2 => let case_WEApp := tt in checkit (WEApp e1 e2) (fun Γ Δ φ ψ ξ lev =>
380 weakExprToStrongExpr e1 Γ Δ φ ψ ξ lev >>>>= fun te1 e1' =>
381 ((weakExprToStrongExpr e2 Γ Δ φ ψ ξ lev) >>>>= fun te2 e2' => _))
382 | WETyApp e t => let case_WETyApp := tt in
383 checkit (WETyApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
384 | WECoApp e t => let case_WECoApp := tt in
385 checkit (WECoApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
386 | WELam ev e => let case_WELam := tt in
387 checkit (WELam ev e) (fun Γ Δ φ ψ ξ lev =>
388 let ξ' := @upξ ξ (ev::nil) lev in
389 weakExprToStrongExpr e Γ Δ φ ψ ξ' lev >>>>= fun te' e' => _)
390 | WECoLam cv e => let case_WECoLam := tt in
391 checkit (WECoLam cv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e))
392 | WEBrak ec e tbody => let case_WEBrak := tt in
393 checkit (WEBrak ec e tbody) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ (ec::lev) >>>>= fun te' e' => _)
394 | WEEsc ec e tbody =>
395 checkit (WEEsc ec e tbody) (fun Γ Δ φ ψ ξ lev =>
396 match lev as LEV return lev=LEV -> _ with
397 | nil => let case_WEEsc_bogus := tt in _
398 | ec'::lev' => fun ecpf => weakExprToStrongExpr e Γ Δ φ ψ ξ lev' >>>>= fun te' e' => let case_WEEsc := tt in _
400 | WETyLam tv e => let case_WETyLam := tt in
401 checkit (WETyLam tv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e))
402 | WENote n e => let case_WENote := tt in
403 checkit (WENote n e) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
404 | WECast e co => let case_WECast := tt in
405 checkit (WECast e co) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _)
406 | WELet v ve e => let case_WELet := tt in
407 checkit (WELet v ve e) (fun Γ Δ φ ψ ξ lev =>
408 let ξ' := upξ ξ (v::nil) lev in
409 ((weakExprToStrongExpr e Γ Δ φ ψ ξ lev)
410 >>>>= (fun te' e' => ((weakExprToStrongExpr ve Γ Δ φ ψ ξ' lev) >>>>= (fun vet' ve' => _)))))
413 checkit (WELetRec rb e) (fun Γ Δ φ ψ ξ lev =>
414 let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in
415 ((fix mLetRecBindingsToELetRecBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) : forall Γ Δ φ ψ ξ lev,
416 ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars mlr φ)) :=
417 match mlr as MLR return forall Γ Δ φ ψ ξ lev,
418 ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars MLR φ)) with
419 | T_Leaf None => fun Γ Δ φ ψ ξ lev => OK (ELR_nil _ _ _ _)
420 | T_Leaf (Some (cv,e)) => fun Γ Δ φ ψ ξ lev =>
421 let case_mlr_leaf := tt in weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun me => _
424 mLetRecBindingsToELetRecBindings b1 Γ Δ φ ψ ξ lev >>= fun x1' =>
425 mLetRecBindingsToELetRecBindings b2 Γ Δ φ ψ ξ lev >>= fun x2' =>
426 OK (ELR_branch _ _ _ _ _ _ x1' x2')
427 end) rb Γ Δ φ ψ ξ' lev) >>= fun rb' => (weakExprToStrongExpr e Γ Δ φ ψ ξ' lev)
429 let case_MLLetRec := tt in _)
431 | WECase e tbranches tc avars alts =>
432 checkit (WECase e tbranches tc avars alts) (fun Γ Δ φ ψ ξ lev =>
433 list2vecOrFail avars _ (fun _ _ => "number of types provided did not match the tycon's number of universal tyvars in Case")
435 let avars' := vec_map (@weakTypeToType Γ φ) avars0 in
436 let tbranches' := @weakTypeToType Γ φ tbranches in
437 ((fix caseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr))
439 ???(Tree ??{ scb : StrongCaseBranchWithVVs WeakExprVar _ tc avars'
441 (sac_Δ scb Γ avars' (weakCK'' Δ))
442 (scbwv_ξ scb (cure ξ φ) (map φ lev))
443 (weakLT' (tbranches'@@(map φ lev))) }) :=
445 | T_Leaf None => OK []
446 | T_Branch b1 b2 => caseBranches b1 >>= fun b1' => caseBranches b2 >>= fun b2' => OK (b1',,b2')
447 | T_Leaf (Some (alt,tvars,cvars,vvars,e')) =>
448 mkStrongAltConPlusJunk' tc alt >>= fun sac =>
449 list2vecOrFail vvars (sac_numExprVars (sac:@StrongAltCon tc))
450 (fun _ _ => "number of expression variables provided did not match the datacon's number of fields") >>= fun vars =>
451 let scb := @Build_StrongCaseBranchWithVVs WeakExprVar _ tc Γ avars' sac vars in
453 := @weakExprToStrongExpr e'
455 (sac_Δ scb Γ avars' (weakCK'' Δ))
457 (let case_psi := tt in _)
459 lev in (let case_ECase_leaf := tt in _)
461 ) alts) >>= fun alts' =>
462 weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' =>
463 let case_ECase := tt in _)
464 end))); clear weakExprToStrongExpr.
466 destruct case_WEVar; intros.
467 matchTypes cte (fst (ξ v)) "HaskWeak EVar".
468 rewrite matchTypes_pf.
469 matchLevs (snd (ξ v)) lev "HaskWeak EVar".
470 rewrite <- matchLevs_pf.
472 apply (EVar _ _ (cure ξ φ)).
474 destruct case_WELit; intros.
475 matchTypes (WTyCon (haskLiteralToTyCon lit)) cte "HaskWeak ELit".
476 rewrite <- matchTypes_pf.
478 replace (weakTypeToType φ (WTyCon (haskLiteralToTyCon lit))) with (@literalType lit Γ); [ idtac | reflexivity].
481 destruct case_WELet; intros.
483 matchTypes te' v "HaskWeak ELet".
484 rename matchTypes_pf into matchTypes_pf'.
485 matchTypes cte vet' "HaskWeak ELet".
489 rewrite matchTypes_pf'.
490 rewrite matchTypes_pf.
491 rewrite upξ_lemma in ve'.
494 destruct case_mlr_leaf; intros.
497 matchTypes me w "HaskWeak LetRec".
500 rewrite <- matchTypes_pf.
503 destruct case_MLLetRec; intros.
504 matchTypes et' cte "HaskWeak LetRec".
507 rewrite (letrec_lemma Γ ξ φ rb lev) in rb'.
508 apply (@ELetRec WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) (weakTypeToType φ cte) _ rb').
509 rewrite <- (letrec_lemma Γ ξ φ rb lev).
510 rewrite <- matchTypes_pf.
513 destruct case_WECast; intros.
515 apply (fun pf => @ECast WeakExprVar _ Γ Δ (cure ξ φ) (weakCoercionToHaskCoercion Γ Δ co) _ _ (map φ lev) pf e').
516 apply assume_all_coercions_well_formed.
518 destruct case_WENote; intros.
519 matchTypes te' cte "HaskWeak ENote".
523 rewrite <- matchTypes_pf.
526 destruct case_WEApp; intros.
527 matchTypes te1 (WAppTy (WAppTy WFunTyCon te2) cte) "HaskWeak EApp".
529 destruct (weakTypeOfWeakExpr e1); try apply (Error error_message).
531 destruct w; try apply (Error error_message); inversion H0.
532 destruct w1; try apply (Error error_message); inversion H0.
533 destruct w1_1; try apply (Error error_message); inversion H0.
535 rewrite matchTypes_pf in e1'.
538 apply (OK (EApp _ _ _ _ _ _ e1' e2')).
540 destruct case_WETyApp; intros.
542 destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0.
544 destruct w; inversion H0.
548 rename t into tsubst.
550 set (@ETyApp WeakExprVar _ Γ Δ wtv
551 (substRaw (weakTypeToType (upφ wtv φ) wt))
552 (weakTypeToType φ tsubst)
555 (assume_all_types_well_formed _ _ _)
558 (* really messy –– but it works! *)
559 matchTypes te' (WForAllTy wtv wt) "HaskWeak ETyApp".
561 rewrite substRaw_lemma in q.
564 rewrite matchTypes_pf in e'.
570 destruct case_WECoApp; intros.
572 destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0.
574 destruct w; inversion H0.
576 destruct t as [ct1 ct2 cc].
577 set (@ECoApp WeakExprVar _ Γ Δ (weakCoercionToHaskCoercion Γ Δ (weakCoercion ct1 ct2 cc))
578 (weakTypeToType φ ct1) (weakTypeToType φ ct2) (weakTypeToType φ te') (cure ξ φ) (map φ lev)) as q.
579 matchTypes w3 te' "HaskWeak ECoApp".
580 rewrite matchTypes_pf.
582 matchTypes (WCoFunTy ct1 ct2 te') te' "HaskWeak ECoApp".
585 apply assume_all_coercions_well_formed.
587 rewrite <- matchTypes_pf in e'.
591 destruct case_WELam; intros.
593 destruct ev as [evv evt].
594 destruct (weakTypeOfWeakExpr e); simpl in cte_pf; inversion cte_pf; try apply (Error error_message).
595 matchTypes te' w "HaskWeak ELam".
596 rewrite <- matchTypes_pf.
600 apply assume_all_types_well_formed.
602 rewrite upξ_lemma in e'.
605 destruct case_WETyLam; intros.
608 destruct (weakTypeOfWeakExpr e).
611 set (e' (k::Γ) (weakCE Δ) (upφ (weakTypeVar c k) φ) (fun x => weakCV (ψ x)) ξ lev) as e''.
612 inversion e''; try apply (Error error_message).
613 inversion X; try apply (Error error_message).
614 apply (Error "FIXME: HaskWeakToStrong: type lambda not yet implemented").
616 destruct case_WECoLam; intros.
619 destruct (weakTypeOfWeakExpr e).
622 set (e' Γ (weakTypeToType φ w ∼∼∼ weakTypeToType φ w0 :: Δ) φ (weakψ ψ) ξ lev) as q.
624 destruct X; try apply (Error error_message).
625 set (kindOfType (weakTypeToType φ w)) as qq.
626 destruct qq; try apply (Error error_message).
628 apply ECoLam with (κ:=k).
629 apply assume_all_types_well_formed.
630 apply assume_all_types_well_formed.
631 fold (@weakTypeToType Γ).
634 destruct case_WEBrak; intros.
636 destruct ec as [ecv eck].
637 destruct (weakTypeOfWeakExpr e); inversion cte_pf; try apply (Error error_message).
639 matchTypes te' w "HaskWeak EBrak".
642 rewrite matchTypes_pf in e'.
645 destruct case_WEEsc_bogus; intros.
646 apply (Error "attempt to use escape symbol at level zero").
648 destruct case_WEEsc; intros.
651 matchTypes te' (WCodeTy ec' cte) "HaskWeak EEsc".
654 rewrite matchTypes_pf in e'.
659 apply (sacpj_ψ sac Γ Δ avars' ψ).
661 destruct case_ECase_leaf.
662 inversion rec; try apply (Error error_message).
663 destruct X; try apply (Error error_message).
664 matchTypes tbranches t "HaskWeak ECase".
668 apply (existT _ {| scbwv_sac := scb ; scbwv_exprvars := vars |}).
671 rewrite matchTypes_pf.
673 rewrite <- case_lemma2.
677 destruct case_ECase; intros.
678 matchTypes cte tbranches "HaskWeak ECase".
679 rewrite matchTypes_pf.
681 matchTypes te' (fold_left WAppTy (vec2list avars0) (WTyCon tc)) "HaskWeak ECase".
683 apply (fun e => @ECase WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) tc _ _ e alts').
686 replace (fold_left HaskAppT (vec2list (vec_map (weakTypeToType φ) avars0)) (HaskTCon tc))
687 with (weakTypeToType φ (fold_left WAppTy (vec2list avars0) (WTyCon tc))).
688 rewrite <- matchTypes_pf.
691 rewrite <- vec2list_map_list2vec.