From 5d42cb2462795fc0feadf8fd9b2c701e1cd1a8b0 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:41:48 -0800 Subject: [PATCH] add HaskWeakToStrong --- src/HaskWeakToStrong.v | 695 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 695 insertions(+) create mode 100644 src/HaskWeakToStrong.v diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v new file mode 100644 index 0000000..13fe7a5 --- /dev/null +++ b/src/HaskWeakToStrong.v @@ -0,0 +1,695 @@ +(*********************************************************************************************************************************) +(* HaskWeakToStrong: convert HaskWeak to HaskStrong *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.Init.Specif. +Require Import HaskKinds. +Require Import HaskCoreLiterals. +Require Import HaskWeakTypes. +Require Import HaskWeakVars. +Require Import HaskWeak. +Require Import HaskStrongTypes. +Require Import HaskStrong. +Require Import HaskCoreTypes. + +Definition upφ {Γ}(tv:WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) : (WeakTypeVar -> HaskTyVar ((tv:Kind)::Γ)) := + fun tv' => + if eqd_dec tv tv' + then FreshHaskTyVar (tv:Kind) + else fun TV ite => φ tv' TV (weakITE ite). + + + +Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) + : (WeakTypeVar -> HaskTyVar (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). + induction tvs. + apply φ. + simpl. + apply upφ. + apply IHtvs. + Defined. + +Open Scope string_scope. + +Fixpoint weakTypeToType {Γ:TypeEnv}(φ:WeakTypeVar -> HaskTyVar Γ)(t:WeakType) : HaskType Γ := + match t with + | WTyVarTy v => fun TV env => @TVar TV (φ v TV env) + | WCoFunTy t1 t2 t3 => (weakTypeToType φ t1) ∼∼ (weakTypeToType φ t2) ⇒ (weakTypeToType φ t3) + | WFunTyCon => fun TV env => TArrow + | WTyCon tc => fun TV env => TCon tc + | WTyFunApp tc lt => fun TV env => fold_left TApp (map (fun t => weakTypeToType φ t TV env) lt) (TCon tc) (* FIXME *) + | WClassP c lt => fun TV env => fold_left TApp (map (fun t=> weakTypeToType φ t TV env) lt) (TCon (classTyCon c)) + | WIParam _ ty => weakTypeToType φ ty + | WForAllTy wtv t => (fun TV env => TAll (wtv:Kind) (fun tv => weakTypeToType (@upφ Γ wtv φ) t TV (tv:::env))) + | WAppTy t1 t2 => fun TV env => TApp (weakTypeToType φ t1 TV env) (weakTypeToType φ t2 TV env) + | WCodeTy ec tbody => fun TV env => TCode (TVar (φ ec TV env)) (weakTypeToType φ tbody TV env) + end. + + +Definition substPhi0 {Γ:TypeEnv}(κ:Kind)(θ:HaskType Γ) : HaskType (κ::Γ) -> HaskType Γ. + intro ht. + refine (substT _ θ). + clear θ. + unfold HaskType in ht. + intros. + apply ht. + apply vec_cons; [ idtac | apply env ]. + apply X. + Defined. + +Definition substPhi {Γ:TypeEnv}(κ:list Kind)(θ:vec (HaskType Γ) (length κ)) : HaskType (app κ Γ) -> HaskType Γ. + induction κ. + intro q; apply q. + simpl. + intro q. + apply IHκ. + inversion θ; subst; auto. + inversion θ; subst. + apply (substPhi0 _ (weakT' X) q). + Defined. + +Definition substφ {Γ}{n}(ltypes:vec (HaskType Γ) n)(Γ':vec _ n)(ht:HaskType (app (vec2list Γ') Γ)) : HaskType Γ. + apply (@substPhi Γ (vec2list Γ')). + rewrite vec2list_len. + apply ltypes. + apply ht. + Defined. + +(* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *) +Record StrongAltConPlusJunk {tc:TyCon} := +{ sacpj_sac : @StrongAltCon tc +; sacpj_φ : forall Γ (φ:WeakTypeVar -> HaskTyVar Γ ), (WeakTypeVar -> HaskTyVar (sac_Γ sacpj_sac Γ)) +; sacpj_ψ : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ), + (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))) +}. +Implicit Arguments StrongAltConPlusJunk [ ]. +Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon. + +(* yes, I know, this is really clumsy *) +Variable emptyφ : WeakTypeVar -> HaskTyVar nil. + Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")". + +Definition mkPhi (lv:list WeakTypeVar) + : (WeakTypeVar -> HaskTyVar (map (fun x:WeakTypeVar => x:Kind) lv)). + set (upφ'(Γ:=nil) lv emptyφ) as φ'. + rewrite <- app_nil_end in φ'. + apply φ'. + Defined. + +Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)). +Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)). + +(* information about a datacon/literal/default which is common to all instances of a branch with that tag *) +Section StrongAltCon. + Context (tc : TyCon)(dc:DataCon tc). + +Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ). + intro avars. + intro ct. + set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'. + set (@substφ _ _ avars') as q. + set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'. + set (@weakTypeToType _ φ' ct) as t. + set (@weakT'' _ Γ t) as t'. + set (@lamer _ _ _ t') as t''. + fold (tyConKinds tc) in t''. + fold (dataConExKinds dc) in t''. + apply (q (tyConKinds tc)). + unfold tyConKinds. + unfold dataConExKinds. + rewrite <- vec2list_map_list2vec. + rewrite <- vec2list_map_list2vec. + rewrite vec2list_list2vec. + rewrite vec2list_list2vec. + apply t''. + Defined. + +Definition mkStrongAltCon : @StrongAltCon tc. + refine + {| sac_altcon := DataAlt dc + ; sac_numCoerVars := length (dataConCoerKinds dc) + ; sac_numExprVars := length (dataConFieldTypes dc) + ; sac_akinds := tyConKinds tc + ; sac_ekinds := dataConExKinds dc + ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _ + ; sac_types := fun Γ avars => let case_sac_types := tt in _ + |}. + + destruct case_sac_coercions. + refine (vec_map _ (list2vec (dataConCoerKinds dc))). + intro. + destruct X. + apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)). + + destruct case_sac_types. + refine (vec_map _ (list2vec (dataConFieldTypes dc))). + intro X. + apply (weakTypeToType' avars). + apply X. + Defined. + +Lemma weakCV' : forall {Γ}{Δ} Γ', + HaskCoVar Γ Δ + -> HaskCoVar (app Γ' Γ) (weakCK'' Δ). + intros. + unfold HaskCoVar in *. + intros; apply (X TV CV). + apply vec_chop' in env; auto. + unfold InstantiatedCoercionEnv in *. + unfold weakCK'' in cenv. + destruct Γ'. + apply cenv. + rewrite <- map_preserves_length in cenv. + apply cenv. + Defined. + +Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. + refine + {| sacpj_sac := mkStrongAltCon + ; sacpj_φ := fun Γ φ => (fun htv => weakV' (φ htv)) + ; sacpj_ψ := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv))) + |}. + intro. + unfold sac_Γ. + unfold HaskCoVar in *. + intros. + apply (x TV CV env). + simpl in cenv. + unfold sac_Δ in *. + unfold InstantiatedCoercionEnv in *. + apply vec_chop' in cenv. + apply cenv. + Defined. +End StrongAltCon. + +Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc). + destruct alt. + set (c:DataCon _) as dc. + set ((dataConTyCon c):TyCon) as tc' in *. + set (eqd_dec tc tc') as eqpf; destruct eqpf; + [ idtac + | apply (Error ("in a case of tycon "+++tyConToString tc+++", found a branch with datacon "+++dataConToString dc)) ]; subst. + apply OK. + eapply mkStrongAltConPlusJunk. + simpl in *. + apply dc. + + apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc + ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil + ; sac_altcon := LitAlt h + |} |}. + intro; intro φ; apply φ. + intro; intro; intro; intro ψ; apply ψ. + apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc + ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil + ; sac_altcon := DEFAULT |} |}. + intro; intro φ; apply φ. + intro; intro; intro; intro ψ; apply ψ. +Defined. + +Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ) := + match mlr with + | T_Leaf None => [] + | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)] + | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ)) + end. + +Open Scope string_scope. +Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end. + +Definition Indexed_Bind T f t (e:@Indexed T f t) : forall Q, (forall t, f t -> ???Q) -> ???Q. +intros. +destruct e; subst. +apply (Error error_message). +apply (X t f0). +Defined. +Notation "a >>>= b" := (@Indexed_Bind _ _ _ a _ b) (at level 20). + +Definition DoublyIndexed_Bind T f t (e:@Indexed T (fun z => ???(f z)) t) : forall Q, (forall t, f t -> ???Q) -> ???Q. + intros. + eapply Indexed_Bind. + apply e. + intros. + destruct X0. + apply (Error error_message). + apply (X t0 f0). + Defined. + +Notation "a >>>>= b" := (@DoublyIndexed_Bind _ _ _ a _ b) (at level 20). + +Ltac matchTypes T1 T2 S := + destruct (eqd_dec T1 T2) as [matchTypes_pf|]; + [ idtac | apply (Error ("type mismatch in "+++S+++": " +++ (weakTypeToString T1) +++ " and " +++ (weakTypeToString T2))) ]. +Ltac matchTypeVars T1 T2 S := + destruct (eqd_dec T1 T2) as [matchTypeVars_pf|]; + [ idtac | apply (Error ("type variable mismatch in"+++S)) ]. +Ltac matchLevs L1 L2 S := + destruct (eqd_dec L1 L2) as [matchLevs_pf|]; + [ idtac | apply (Error ("level mismatch in "+++S)) ]. + + +Definition cure {Γ}(ξ:WeakExprVar -> WeakType * list WeakTypeVar)(φ:WeakTypeVar->HaskTyVar Γ) + : WeakExprVar->LeveledHaskType Γ := + fun wtv => weakTypeToType φ (fst (ξ wtv)) @@ map φ (snd (ξ wtv)). + +Definition weakExprVarToWeakType : WeakExprVar -> WeakType := + fun wev => match wev with weakExprVar _ t => t end. + Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType. + +Fixpoint upξ (ξ:WeakExprVar -> WeakType * list WeakTypeVar) + (evs:list WeakExprVar) + (lev:list WeakTypeVar) : + (WeakExprVar -> WeakType * list WeakTypeVar) := + fun wev => + match evs with + | nil => ξ wev + | a::b => if eqd_dec wev a then ((wev:WeakType),lev) else upξ ξ b lev wev + end. + +Variable weakCoercionToHaskCoercion : forall Γ Δ, WeakCoercion -> HaskCoercion Γ Δ. + +Notation "'checkit' ( Y ) X" := (match weakTypeOfWeakExpr Y as CTE return + CTE=weakTypeOfWeakExpr Y -> forall Γ Δ φ ψ ξ lev, Indexed _ CTE with + | Error s => fun _ _ _ _ _ _ _ => Indexed_Error _ s + | OK cte => fun cte_pf => (fun x Γ Δ φ ψ ξ lev => Indexed_OK _ _ (x Γ Δ φ ψ ξ lev)) X + end (refl_equal _)) (at level 10). + + +(* equality lemmas I have yet to prove *) + +Lemma upξ_lemma Γ ξ v lev φ + : cure(Γ:=Γ) (upξ ξ (v :: nil) lev) φ = update_ξ (cure ξ φ) ((v,weakTypeToType φ v @@ map φ lev)::nil). + admit. + Qed. + +(* this is tricky because of the test for ModalBoxTyCon is a type index for tc and because the fold is a left-fold *) + +Lemma letrec_lemma : forall Γ ξ φ rb lev, +let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in +(cure ξ' φ) = ( + update_ξ (cure ξ φ) + (map + (fun x : WeakExprVar * HaskType Γ => + ⟨fst x, snd x @@ map φ lev ⟩) (leaves (mLetRecTypesVars rb φ)))). +admit. +Qed. + +Lemma case_lemma1 tc Γ avars' (sac:StrongAltConPlusJunk tc) vars ξ φ lev : +(@scbwv_ξ WeakExprVar WeakExprVarEqDecidable tc Γ avars' + {| scbwv_sac := sac; scbwv_exprvars := vars |} + (@cure Γ ξ φ) (@map WeakTypeVar (HaskTyVar Γ) φ lev)) + = (cure ξ (sacpj_φ sac Γ φ)). + admit. + Qed. +Lemma case_lemma2 tc Γ (sac:@StrongAltConPlusJunk tc) φ lev : + (map (sacpj_φ sac Γ φ) lev) = weakL' (map φ lev). + admit. + Qed. +Lemma case_lemma3 Γ φ t tc (sac:@StrongAltConPlusJunk tc) : + (weakT' (weakTypeToType φ t) = weakTypeToType (sacpj_φ sac Γ φ) t). + admit. + Qed. +Lemma case_lemma4 Γ φ (tc:TyCon) avars0 : forall Q1 Q2, (@weakTypeToType Γ φ Q2)=Q1 -> + fold_left HaskAppT (map (weakTypeToType φ) avars0) Q1 = + weakTypeToType φ (fold_left WAppTy avars0 Q2). + induction avars0; intros. + simpl. + symmetry; auto. + simpl. + set (IHavars0 (HaskAppT Q1 (weakTypeToType φ a)) (WAppTy Q2 a)) as z. + rewrite z. + reflexivity. + rewrite <- H. + simpl. + auto. + Qed. + +(* for now... *) +Axiom assume_all_coercions_well_formed : forall Γ (Δ:CoercionEnv Γ) t1 t2 co, Δ ⊢ᴄᴏ co : t1 ∼ t2. +Axiom assume_all_types_well_formed : forall Γ t x, Γ ⊢ᴛy t : x. + +Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) : + WeakCoerVar -> HaskCoVar Γ (κ::Δ). + intros. + unfold HaskCoVar. + intros. + apply (ψ X TV CV env). + inversion cenv; auto. + Defined. + +Lemma substRaw {Γ}{κ} : HaskType (κ::Γ) -> (∀ TV, @InstantiatedTypeEnv TV Γ -> TV -> @RawHaskType TV). + intro ht. + intro TV. + intro env. + intro tv. + apply ht. + apply (tv:::env). + Defined. + +Lemma substRaw_lemma : forall (Γ:TypeEnv) (φ:WeakTypeVar->HaskTyVar Γ) wt tsubst wtv, + substT (substRaw (weakTypeToType (upφ wtv φ) wt)) (weakTypeToType φ tsubst) = + weakTypeToType φ (replaceWeakTypeVar wt wtv tsubst). + admit. + Qed. + +Definition weakExprToStrongExpr : forall + (ce:WeakExpr) + (Γ:TypeEnv) + (Δ:CoercionEnv Γ) + (φ:WeakTypeVar->HaskTyVar Γ) + (ψ:WeakCoerVar->HaskCoVar Γ Δ) + (ξ:WeakExprVar->WeakType * list WeakTypeVar) + (lev:list WeakTypeVar) + , + Indexed (fun t' => ???(@Expr _ WeakExprVarEqDecidable Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev)))) + (weakTypeOfWeakExpr ce). + refine (( + fix weakExprToStrongExpr (ce:WeakExpr) {struct ce} : forall Γ Δ φ ψ ξ lev, + Indexed (fun t' => ???(Expr Γ Δ (cure ξ φ) (weakTypeToType φ t' @@ (map φ lev)))) (weakTypeOfWeakExpr ce) := + (match ce as CE return (forall Γ Δ φ ψ ξ lev, Indexed _ (weakTypeOfWeakExpr CE)) + with + | WEVar v => let case_WEVar := tt in checkit (WEVar v) (fun Γ Δ φ ψ ξ lev => _) + | WELit lit => let case_WELit := tt in checkit (WELit lit) (fun Γ Δ φ ψ ξ lev => _) + | WEApp e1 e2 => let case_WEApp := tt in checkit (WEApp e1 e2) (fun Γ Δ φ ψ ξ lev => + weakExprToStrongExpr e1 Γ Δ φ ψ ξ lev >>>>= fun te1 e1' => + ((weakExprToStrongExpr e2 Γ Δ φ ψ ξ lev) >>>>= fun te2 e2' => _)) + | WETyApp e t => let case_WETyApp := tt in + checkit (WETyApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) + | WECoApp e t => let case_WECoApp := tt in + checkit (WECoApp e t) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) + | WELam ev e => let case_WELam := tt in + checkit (WELam ev e) (fun Γ Δ φ ψ ξ lev => + let ξ' := @upξ ξ (ev::nil) lev in + weakExprToStrongExpr e Γ Δ φ ψ ξ' lev >>>>= fun te' e' => _) + | WECoLam cv e => let case_WECoLam := tt in + checkit (WECoLam cv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e)) + | WEBrak ec e tbody => let case_WEBrak := tt in + checkit (WEBrak ec e tbody) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ (ec::lev) >>>>= fun te' e' => _) + | WEEsc ec e tbody => + checkit (WEEsc ec e tbody) (fun Γ Δ φ ψ ξ lev => + match lev as LEV return lev=LEV -> _ with + | nil => let case_WEEsc_bogus := tt in _ + | ec'::lev' => fun ecpf => weakExprToStrongExpr e Γ Δ φ ψ ξ lev' >>>>= fun te' e' => let case_WEEsc := tt in _ + end (refl_equal _)) + | WETyLam tv e => let case_WETyLam := tt in + checkit (WETyLam tv e) (fun Γ Δ φ ψ ξ lev => (fun e' => _) (weakExprToStrongExpr e)) + | WENote n e => let case_WENote := tt in + checkit (WENote n e) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) + | WECast e co => let case_WECast := tt in + checkit (WECast e co) (fun Γ Δ φ ψ ξ lev => weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => _) + | WELet v ve e => let case_WELet := tt in + checkit (WELet v ve e) (fun Γ Δ φ ψ ξ lev => + let ξ' := upξ ξ (v::nil) lev in + ((weakExprToStrongExpr e Γ Δ φ ψ ξ lev) + >>>>= (fun te' e' => ((weakExprToStrongExpr ve Γ Δ φ ψ ξ' lev) >>>>= (fun vet' ve' => _))))) + + | WELetRec rb e => + checkit (WELetRec rb e) (fun Γ Δ φ ψ ξ lev => +let ξ' := upξ ξ (map (@fst _ _) (leaves (mLetRecTypesVars rb φ))) lev in + ((fix mLetRecBindingsToELetRecBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) : forall Γ Δ φ ψ ξ lev, + ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars mlr φ)) := + match mlr as MLR return forall Γ Δ φ ψ ξ lev, + ???(ELetRecBindings Γ Δ (cure ξ φ) (map φ lev) (mLetRecTypesVars MLR φ)) with + | T_Leaf None => fun Γ Δ φ ψ ξ lev => OK (ELR_nil _ _ _ _) + | T_Leaf (Some (cv,e)) => fun Γ Δ φ ψ ξ lev => + let case_mlr_leaf := tt in weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun me => _ + | T_Branch b1 b2 => + fun Γ Δ φ ψ ξ lev => + mLetRecBindingsToELetRecBindings b1 Γ Δ φ ψ ξ lev >>= fun x1' => + mLetRecBindingsToELetRecBindings b2 Γ Δ φ ψ ξ lev >>= fun x2' => + OK (ELR_branch _ _ _ _ _ _ x1' x2') + end) rb Γ Δ φ ψ ξ' lev) >>= fun rb' => (weakExprToStrongExpr e Γ Δ φ ψ ξ' lev) + >>>>= fun et' e' => + let case_MLLetRec := tt in _) + + | WECase e tbranches tc avars alts => + checkit (WECase e tbranches tc avars alts) (fun Γ Δ φ ψ ξ lev => + list2vecOrFail avars _ (fun _ _ => "number of types provided did not match the tycon's number of universal tyvars in Case") + >>= fun avars0 => + let avars' := vec_map (@weakTypeToType Γ φ) avars0 in + let tbranches' := @weakTypeToType Γ φ tbranches in + ((fix caseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) + : + ???(Tree ??{ scb : StrongCaseBranchWithVVs WeakExprVar _ tc avars' + & Expr (sac_Γ scb Γ) + (sac_Δ scb Γ avars' (weakCK'' Δ)) + (scbwv_ξ scb (cure ξ φ) (map φ lev)) + (weakLT' (tbranches'@@(map φ lev))) }) := + match alts with + | T_Leaf None => OK [] + | T_Branch b1 b2 => caseBranches b1 >>= fun b1' => caseBranches b2 >>= fun b2' => OK (b1',,b2') + | T_Leaf (Some (alt,tvars,cvars,vvars,e')) => + mkStrongAltConPlusJunk' tc alt >>= fun sac => + list2vecOrFail vvars (sac_numExprVars (sac:@StrongAltCon tc)) + (fun _ _ => "number of expression variables provided did not match the datacon's number of fields") >>= fun vars => + let scb := @Build_StrongCaseBranchWithVVs WeakExprVar _ tc Γ avars' sac vars in + let rec + := @weakExprToStrongExpr e' + (sac_Γ scb Γ) + (sac_Δ scb Γ avars' (weakCK'' Δ)) + (sacpj_φ sac Γ φ) + (let case_psi := tt in _) + ξ + lev in (let case_ECase_leaf := tt in _) + end + ) alts) >>= fun alts' => + weakExprToStrongExpr e Γ Δ φ ψ ξ lev >>>>= fun te' e' => + let case_ECase := tt in _) + end))); clear weakExprToStrongExpr. + + destruct case_WEVar; intros. + matchTypes cte (fst (ξ v)) "HaskWeak EVar". + rewrite matchTypes_pf. + matchLevs (snd (ξ v)) lev "HaskWeak EVar". + rewrite <- matchLevs_pf. + apply OK. + apply (EVar _ _ (cure ξ φ)). + + destruct case_WELit; intros. + matchTypes (WTyCon (haskLiteralToTyCon lit)) cte "HaskWeak ELit". + rewrite <- matchTypes_pf. + apply OK. + replace (weakTypeToType φ (WTyCon (haskLiteralToTyCon lit))) with (@literalType lit Γ); [ idtac | reflexivity]. + apply ELit. + + destruct case_WELet; intros. + unfold ξ' in ve'. + matchTypes te' v "HaskWeak ELet". + rename matchTypes_pf into matchTypes_pf'. + matchTypes cte vet' "HaskWeak ELet". + apply OK. + eapply ELet. + apply e'. + rewrite matchTypes_pf'. + rewrite matchTypes_pf. + rewrite upξ_lemma in ve'. + apply ve'. + + destruct case_mlr_leaf; intros. + simpl. + destruct cv. + matchTypes me w "HaskWeak LetRec". + apply OK. + apply ELR_leaf. + rewrite <- matchTypes_pf. + apply X. + + destruct case_MLLetRec; intros. + matchTypes et' cte "HaskWeak LetRec". + apply OK. + unfold ξ' in rb'. + rewrite (letrec_lemma Γ ξ φ rb lev) in rb'. + apply (@ELetRec WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) (weakTypeToType φ cte) _ rb'). + rewrite <- (letrec_lemma Γ ξ φ rb lev). + rewrite <- matchTypes_pf. + apply e'. + + destruct case_WECast; intros. + apply OK. + apply (fun pf => @ECast WeakExprVar _ Γ Δ (cure ξ φ) (weakCoercionToHaskCoercion Γ Δ co) _ _ (map φ lev) pf e'). + apply assume_all_coercions_well_formed. + + destruct case_WENote; intros. + matchTypes te' cte "HaskWeak ENote". + apply OK. + apply ENote. + apply n. + rewrite <- matchTypes_pf. + apply e'. + + destruct case_WEApp; intros. + matchTypes te1 (WAppTy (WAppTy WFunTyCon te2) cte) "HaskWeak EApp". + inversion cte_pf. + destruct (weakTypeOfWeakExpr e1); try apply (Error error_message). + simpl in H0. + destruct w; try apply (Error error_message); inversion H0. + destruct w1; try apply (Error error_message); inversion H0. + destruct w1_1; try apply (Error error_message); inversion H0. + clear H0 H1 H2. + rewrite matchTypes_pf in e1'. + simpl in e1'. + rewrite <- H3. + apply (OK (EApp _ _ _ _ _ _ e1' e2')). + + destruct case_WETyApp; intros. + inversion cte_pf. + destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0. + clear H1. + destruct w; inversion H0. + simpl in cte_pf. + clear cte_pf. + rename w0 into wt. + rename t into tsubst. + rename w into wtv. + set (@ETyApp WeakExprVar _ Γ Δ wtv + (substRaw (weakTypeToType (upφ wtv φ) wt)) + (weakTypeToType φ tsubst) + (cure ξ φ) + (map φ lev) + (assume_all_types_well_formed _ _ _) + ) as q. + + (* really messy –– but it works! *) + matchTypes te' (WForAllTy wtv wt) "HaskWeak ETyApp". + apply OK. + rewrite substRaw_lemma in q. + apply q. + clear q H1 H0. + rewrite matchTypes_pf in e'. + simpl in e'. + unfold HaskTAll. + unfold substRaw. + apply e'. + + destruct case_WECoApp; intros. + inversion cte_pf. + destruct (weakTypeOfWeakExpr e); simpl in *; inversion H0. + clear H1. + destruct w; inversion H0. + subst. + destruct t as [ct1 ct2 cc]. + set (@ECoApp WeakExprVar _ Γ Δ (weakCoercionToHaskCoercion Γ Δ (weakCoercion ct1 ct2 cc)) + (weakTypeToType φ ct1) (weakTypeToType φ ct2) (weakTypeToType φ te') (cure ξ φ) (map φ lev)) as q. + matchTypes w3 te' "HaskWeak ECoApp". + rewrite matchTypes_pf. + clear matchTypes_pf. + matchTypes (WCoFunTy ct1 ct2 te') te' "HaskWeak ECoApp". + apply OK. + apply q. + apply assume_all_coercions_well_formed. + clear q H0 cte_pf. + rewrite <- matchTypes_pf in e'. + simpl in e'. + apply e'. + + destruct case_WELam; intros. + simpl in cte_pf. + destruct ev as [evv evt]. + destruct (weakTypeOfWeakExpr e); simpl in cte_pf; inversion cte_pf; try apply (Error error_message). + matchTypes te' w "HaskWeak ELam". + rewrite <- matchTypes_pf. + apply OK. + simpl. + eapply ELam. + apply assume_all_types_well_formed. + unfold ξ' in e'. + rewrite upξ_lemma in e'. + apply e'. + + destruct case_WETyLam; intros. + inversion cte_pf. + destruct tv. + destruct (weakTypeOfWeakExpr e). + inversion H0. + inversion H0. + set (e' (k::Γ) (weakCE Δ) (upφ (weakTypeVar c k) φ) (fun x => weakCV (ψ x)) ξ lev) as e''. + inversion e''; try apply (Error error_message). + inversion X; try apply (Error error_message). + apply (Error "FIXME: HaskWeakToStrong: type lambda not yet implemented"). + + destruct case_WECoLam; intros. + inversion cte_pf. + destruct cv. + destruct (weakTypeOfWeakExpr e). + inversion H0. + inversion H0. + set (e' Γ (weakTypeToType φ w ∼∼∼ weakTypeToType φ w0 :: Δ) φ (weakψ ψ) ξ lev) as q. + inversion q. + destruct X; try apply (Error error_message). + set (kindOfType (weakTypeToType φ w)) as qq. + destruct qq; try apply (Error error_message). + apply OK. + apply ECoLam with (κ:=k). + apply assume_all_types_well_formed. + apply assume_all_types_well_formed. + fold (@weakTypeToType Γ). + apply e0. + + destruct case_WEBrak; intros. + simpl in cte_pf. + destruct ec as [ecv eck]. + destruct (weakTypeOfWeakExpr e); inversion cte_pf; try apply (Error error_message). + simpl. + matchTypes te' w "HaskWeak EBrak". + apply OK. + apply EBrak. + rewrite matchTypes_pf in e'. + apply e'. + + destruct case_WEEsc_bogus; intros. + apply (Error "attempt to use escape symbol at level zero"). + + destruct case_WEEsc; intros. + rewrite ecpf. + clear ecpf lev. + matchTypes te' (WCodeTy ec' cte) "HaskWeak EEsc". + apply OK. + apply EEsc. + rewrite matchTypes_pf in e'. + simpl in e'. + apply e'. + + destruct case_psi. + apply (sacpj_ψ sac Γ Δ avars' ψ). + + destruct case_ECase_leaf. + inversion rec; try apply (Error error_message). + destruct X; try apply (Error error_message). + matchTypes tbranches t "HaskWeak ECase". + apply OK. + apply T_Leaf. + apply Some. + apply (existT _ {| scbwv_sac := scb ; scbwv_exprvars := vars |}). + simpl. + unfold tbranches'. + rewrite matchTypes_pf. + rewrite case_lemma1. + rewrite <- case_lemma2. + rewrite case_lemma3. + apply e0. + + destruct case_ECase; intros. + matchTypes cte tbranches "HaskWeak ECase". + rewrite matchTypes_pf. + clear matchTypes_pf. + matchTypes te' (fold_left WAppTy (vec2list avars0) (WTyCon tc)) "HaskWeak ECase". + apply OK. + apply (fun e => @ECase WeakExprVar _ Γ Δ (cure ξ φ) (map φ lev) tc _ _ e alts'). + unfold caseType. + unfold avars'. + replace (fold_left HaskAppT (vec2list (vec_map (weakTypeToType φ) avars0)) (HaskTCon tc)) + with (weakTypeToType φ (fold_left WAppTy (vec2list avars0) (WTyCon tc))). + rewrite <- matchTypes_pf. + apply e'. + symmetry. + rewrite <- vec2list_map_list2vec. + apply case_lemma4. + apply tc. + reflexivity. + Defined. -- 1.7.10.4