--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
projects / coq-hetmet.git / commitdiff