X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=e70e17dd0d33d855f5202a5d3510298a73cdd9a7;hp=13fe7a5477f45927e6320fa014b9381d52696390;hb=8c26722a1ee110077968a8a166eb7130266b2035;hpb=b8f6adf700fa3c67feefaea3d2cf5c4626300489 diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 13fe7a5..e70e17d 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -17,17 +17,23 @@ Require Import HaskWeak. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreTypes. +Require Import HaskCoreVars. -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). - +Open Scope string_scope. +Definition TyVarResolver Γ := forall wt:WeakTypeVar, HaskTyVar Γ wt. +Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ. +Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). + unfold TyVarResolver. + refine (fun tv' => + if eqd_dec tv tv' + then let fresh := @FreshHaskTyVar Γ tv in _ + else fun TV ite => φ tv' TV (weakITE ite)). + rewrite <- _H; apply fresh. + Defined. -Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) - : (WeakTypeVar -> HaskTyVar (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). +Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) + : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). induction tvs. apply φ. simpl. @@ -35,56 +41,35 @@ Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:WeakTypeVar -> HaskTyVar Γ) 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 Γ. +Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'. intro ht. refine (substT _ θ). clear θ. unfold HaskType in ht. intros. apply ht. - apply vec_cons; [ idtac | apply env ]. + apply ICons; [ idtac | apply env ]. apply X. Defined. -Definition substPhi {Γ:TypeEnv}(κ:list Kind)(θ:vec (HaskType Γ) (length κ)) : HaskType (app κ Γ) -> HaskType Γ. - induction κ. +Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. + induction lk. intro q; apply q. simpl. intro q. - apply IHκ. + apply IHlk. 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. + eapply substPhi. + eapply weakT'. + apply X. + apply q. 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 Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ)) ; sacpj_ψ : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ), (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))) }. @@ -92,11 +77,11 @@ Implicit Arguments StrongAltConPlusJunk [ ]. Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon. (* yes, I know, this is really clumsy *) -Variable emptyφ : WeakTypeVar -> HaskTyVar nil. +Variable emptyφ : TyVarResolver 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)). + : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)). set (upφ'(Γ:=nil) lv emptyφ) as φ'. rewrite <- app_nil_end in φ'. apply φ'. @@ -105,10 +90,134 @@ Definition mkPhi (lv:list WeakTypeVar) 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)). +Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ. +Notation " ` x " := (@fixkind _ x) (at level 100). + +Ltac matchThings T1 T2 S := + destruct (eqd_dec T1 T2) as [matchTypeVars_pf|]; + [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ]. + +Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★). + intros. + unfold InstantiatedTypeEnv in ite. + apply X. + apply (X0::::ite). + Defined. + +Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★. + intro. + unfold HaskType. + intros. + apply (TAll κ). + eapply mkTAll'. + apply X. + apply X0. + Defined. + +Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ). + refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) := + match t with + | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow)) + | WTyCon tc => let case_WTyCon := tt in _ + | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented" + | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented" + | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _ + | WTyVarTy v => let case_WTyVarTy := tt in _ + | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _ + | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => _ + | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in + weakTypeToType _ φ t1 >>= fun t1' => + weakTypeToType _ φ t2 >>= fun t2' => + weakTypeToType _ φ t3 >>= fun t3' => _ + | WTyFunApp tc lt => + ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType) + { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) := + match lt with + | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with + | nil => OK (fun TV _ => TyFunApp_nil) + | _ => Error "WTyFunApp not applied to enough types" + end + | tx::lt' => weakTypeToType Γ φ tx >>= fun t' => + match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with + | nil => Error "WTyFunApp applied to too many types" + | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' => + let case_weakTypeListToTypeList := tt in _ + end + end + ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _ + end ); clear weakTypeToType. + + destruct case_WTyVarTy. + apply OK. + exact (haskTypeOfSomeKind (fun TV env => TVar (φ v TV env))). + + destruct case_WAppTy. + destruct t1' as [k1' t1']. + destruct t2' as [k2' t2']. + destruct k1'; + try (matchThings k1'1 k2' "Kind mismatch in WAppTy: "; + subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env)))); + apply (Error "Kind mismatch in WAppTy:: "). + + destruct case_weakTypeListToTypeList. + destruct t' as [ k' t' ]. + matchThings k k' "Kind mismatch in weakTypeListToTypeList". + subst. + apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))). + + destruct case_WTyFunApp. + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply TyFunApp. + apply lt'. + apply X. + + destruct case_WTyCon. + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply (TCon tc). + + destruct case_WCodeTy. + destruct tbody'. + matchThings κ ★ "Kind mismatch in WCodeTy: ". + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply TCode. + apply (TVar (φ (@fixkind ★ ec) TV X)). + subst. + apply h. + apply X. + + destruct case_WCoFunTy. + destruct t1' as [ k1' t1' ]. + destruct t2' as [ k2' t2' ]. + destruct t3' as [ k3' t3' ]. + matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy". + subst. + matchThings k3' ★ "Kind mismatch in result of WCoFunTy". + subst. + apply OK. + apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')). + + destruct case_WForAllTy. + destruct t1. + matchThings ★ κ "Kind mismatch in WForAllTy: ". + subst. + apply OK. + apply (@haskTypeOfSomeKind _ ★). + apply (@mkTAll wtv). + apply h. + Defined. + + + (* 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. @@ -186,15 +295,16 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. 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 (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; subst. apply OK. eapply mkStrongAltConPlusJunk. simpl in *. @@ -212,127 +322,20 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP intro; intro φ; apply φ. intro; intro; intro; intro ψ; apply ψ. Defined. - -Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ) := +Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) := match mlr with - | T_Leaf None => [] + | T_Leaf None => [] | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)] - | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ)) + | 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. +(*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*) Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) : WeakCoerVar -> HaskCoVar Γ (κ::Δ). @@ -343,353 +346,111 @@ Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ 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). +(* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *) +Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ) + : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ'). + intros. + destruct τ as [τ l]. + destruct τ' as [τ' l']. + destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ]. + destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ]. + subst. + apply OK. + apply e. 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 weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ). + intros. + set (weakTypeToType φ t) as wt. + destruct wt; try apply (Error error_message). + destruct h. + matchThings κ κ0 "Kind mismatch in weakTypeToType': ". + subst. + apply OK. + apply h. + Defined. 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). + (φ:TyVarResolver Γ) + (ψ:CoVarResolver Γ Δ) + (ξ:WeakExprVar -> LeveledHaskType Γ ★) + (τ:HaskType Γ ★) + (lev:HaskLevel Γ), + WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ). 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. + fix weakExprToStrongExpr + (Γ:TypeEnv) + (Δ:CoercionEnv Γ) + (φ:TyVarResolver Γ) + (ψ:CoVarResolver Γ Δ) + (ξ:WeakExprVar -> LeveledHaskType Γ ★) + (τ:HaskType Γ ★) + (lev:HaskLevel Γ) + (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) ) := + match we with + + | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v) + + | WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev) + + | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv => + weakTypeOfWeakExpr e >>= fun t => + weakTypeToType' φ t ★ >>= fun τ' => + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' => + castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e') + + | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => + castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e') + + | WEEsc ec e tbody => weakTypeToType' φ tbody ★ >>= fun tbody' => + match lev with + | nil => Error "ill-leveled escapification" + | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e + >>= fun e' => + castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e') + end + | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') + + | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv => + weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' => + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody + >>= fun ebody' => + OK (ELet _ _ _ tv _ lev v ve' ebody') + + | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 => + weakTypeToType' φ t2 ★ >>= fun t2' => + weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' => + weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' => + OK (EApp _ _ _ _ _ _ e1' e2') + + | WETyLam tv e => let φ' := upφ tv φ in + weakTypeOfWeakExpr e >>= fun te => + weakTypeToType' φ' te ★ >>= fun τ' => + weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e + >>= fun e' => + castExpr "WETyLam1" _ e' >>= fun e'' => + castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'') + + | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => + match te with + | WForAllTy wtv te' => + let φ' := upφ wtv φ in + weakTypeToType' φ' te' ★ >>= fun te'' => + weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' => + weakTypeToType' φ t wtv >>= fun t' => + castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e') + | _ => Error ("weakTypeToType: WETyApp body with type "+++te) + end + + (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two + * to get them back working again *) + | WECoApp e t => Error "weakExprToStrongExpr: WECoApp not yet implemented" + | WECoLam cv e => Error "weakExprToStrongExpr: WECoLam not yet implemented" + | WECast e co => Error "weakExprToStrongExpr: WECast not yet implemented" + | WELetRec rb e => Error "weakExprToStrongExpr: WELetRec not yet implemented" + | WECase e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase not yet implemented" + end)). + Defined. +