X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=d8dcf42003abbef5304e67118b85579ade405d90;hp=13fe7a5477f45927e6320fa014b9381d52696390;hb=4c5c94487aa2bf5489371f112607f0a4c4f01a94;hpb=5d42cb2462795fc0feadf8fd9b2c701e1cd1a8b0 diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 13fe7a5..d8dcf42 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -10,117 +10,251 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. +Require Import HaskWeakToCore. Require Import HaskStrongTypes. Require Import HaskStrong. +Require Import HaskCoreVars. +Require Import HaskCoreToWeak. 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). - +Open Scope string_scope. +Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). +Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ). +Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). + unfold TyVarResolver. + refine (fun tv' => + if eqd_dec tv tv' + then let fresh := @FreshHaskTyVar Γ tv in OK _ + else φ tv' >>= fun tv'' => OK (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 upPhi2 {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) + : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). induction tvs. apply φ. simpl. - apply upφ. + apply upPhi. 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 substphi {Γ: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 Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ), - (WeakCoerVar -> HaskCoVar _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))) +; sacpj_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ)) +; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta sacpj_sac Γ atypes (weakCK'' Δ)) }. 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)). - set (upφ'(Γ:=nil) lv emptyφ) as φ'. - rewrite <- app_nil_end in φ'. - apply φ'. + : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)). + set (upPhi2(Γ:=nil) lv emptyφ) as φ2. + rewrite <- app_nil_end in φ2. + apply φ2. 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)). +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 +++ toString T1 +++ " " +++ toString 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 Γ) := + addErrorMessage ("weakTypeToType " +++ toString t) + 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 φ v >>= fun v' => _ + | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upPhi wtv φ) t >>= fun t => _ + | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody + >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _ + | 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"(* +++ eol +++ + " tyCon= " +++ toString tc +++ eol +++ + " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++ + " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++ + " types= " +++ toString lt +++ eol*)) + | 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. + apply ConcatenableString. + + destruct case_WTyVarTy. + apply (addErrorMessage "case_WTyVarTy"). + apply OK. + exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))). + + destruct case_WAppTy. + apply (addErrorMessage "case_WAppTy"). + destruct t1' as [k1' t1']. + destruct t2' as [k2' t2']. + set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++ + toString t2'+++" of kind "+++toString k2') as err. + 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: "+++err)). + + destruct case_weakTypeListToTypeList. + apply (addErrorMessage "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 (addErrorMessage "case_WTyFunApp"). + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))). + apply lt'. + apply X. + + destruct case_WTyCon. + apply (addErrorMessage "case_WTyCon"). + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply (TCon tc). + + destruct case_WCodeTy. + apply (addErrorMessage "case_WCodeTy"). + destruct tbody'. + matchThings κ ★ "Kind mismatch in WCodeTy: ". + apply OK. + eapply haskTypeOfSomeKind. + unfold HaskType; intros. + apply TCode. + apply (TVar (ec' TV X)). + subst. + apply h. + apply X. + + destruct case_WCoFunTy. + apply (addErrorMessage "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. + apply (addErrorMessage "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)) Γ). +Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds 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''. + apply (addErrorMessage "weakTypeToType'"). + set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'. + set (@substphi _ _ avars') as q. + set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2. + set (@weakTypeToType _ φ2 ct) as t. + destruct t as [|t]; try apply (Error error_message). + destruct t as [tk t]. + matchThings tk ★ "weakTypeToType'". + subst. + apply OK. + set (@weakT'' _ Γ _ t) as t'. + set (@lamer _ _ _ _ t') as t''. fold (tyConKinds tc) in t''. fold (dataConExKinds dc) in t''. - apply (q (tyConKinds tc)). + apply q. + clear q. unfold tyConKinds. unfold dataConExKinds. rewrite <- vec2list_map_list2vec. @@ -132,10 +266,9 @@ Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType Definition mkStrongAltCon : @StrongAltCon tc. refine - {| sac_altcon := DataAlt dc + {| sac_altcon := WeakDataAlt 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 _ @@ -145,25 +278,48 @@ Definition mkStrongAltCon : @StrongAltCon tc. refine (vec_map _ (list2vec (dataConCoerKinds dc))). intro. destruct X. - apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)). + unfold tyConKind in avars. + set (@weakTypeToType' Γ) as q. + unfold tyConKinds in q. + rewrite <- vec2list_map_list2vec in q. + rewrite vec2list_list2vec in q. + apply ( + match + q avars w >>= fun t1 => + q avars w0 >>= fun t2 => + OK (mkHaskCoercionKind t1 t2) + with + | Error s => Prelude_error s + | OK y => y + end). destruct case_sac_types. refine (vec_map _ (list2vec (dataConFieldTypes dc))). intro X. - apply (weakTypeToType' avars). - apply X. + unfold tyConKind in avars. + set (@weakTypeToType' Γ) as q. + unfold tyConKinds in q. + rewrite <- vec2list_map_list2vec in q. + rewrite vec2list_list2vec in q. + set (q avars X) as y. + apply (match y with + | Error s =>Prelude_error s + | OK y' => y' + end). Defined. - + + Lemma weakCV' : forall {Γ}{Δ} Γ', HaskCoVar Γ Δ -> HaskCoVar (app Γ' Γ) (weakCK'' Δ). intros. unfold HaskCoVar in *. intros; apply (X TV CV). - apply vec_chop' in env; auto. + apply ilist_chop' in env; auto. unfold InstantiatedCoercionEnv in *. unfold weakCK'' in cenv. destruct Γ'. + rewrite <- map_preserves_length in cenv. apply cenv. rewrite <- map_preserves_length in cenv. apply cenv. @@ -172,524 +328,412 @@ Lemma weakCV' : forall {Γ}{Δ} Γ', 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))) + ; sacpj_phi := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv')) + ; sacpj_psi := + fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv'))) |}. intro. - unfold sac_Γ. + unfold sac_gamma. unfold HaskCoVar in *. intros. apply (x TV CV env). simpl in cenv. - unfold sac_Δ in *. + unfold sac_delta in *. unfold InstantiatedCoercionEnv in *. apply vec_chop' in cenv. apply cenv. Defined. + + Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ. + intros. + induction Δ. + reflexivity. + simpl. + rewrite IHΔ. + reflexivity. + Qed. + End StrongAltCon. -Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc). +Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@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 "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; 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 + apply OK; refine {| sacpj_sac := {| + sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil + ; sac_altcon := WeakLitAlt 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; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. + rewrite weakCK'_nil_inert. apply ψ. + apply OK; refine {| sacpj_sac := {| + sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil + ; sac_altcon := WeakDEFAULT |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ; apply ψ. + intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. + rewrite weakCK'_nil_inert. 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 weakExprVarToWeakType : WeakExprVar -> WeakType := + fun wev => match wev with weakExprVar _ t => t end. + Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType. -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). +Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ. -Definition DoublyIndexed_Bind T f t (e:@Indexed T (fun z => ???(f z)) t) : forall Q, (forall t, f t -> ???Q) -> ???Q. +Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) : + WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)). intros. - eapply Indexed_Bind. - apply e. + refine (ψ X >>= _). + unfold HaskCoVar. intros. - destruct X0. - apply (Error error_message). - apply (X t0 f0). + apply OK. + intros. + inversion cenv; auto. Defined. -Notation "a >>>>= b" := (@DoublyIndexed_Bind _ _ _ a _ b) (at level 20). +(* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *) +Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l) + : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l'). + apply (addErrorMessage ("castExpr " +++ err_msg)). + intros. + destruct (eqd_dec l l'); [ idtac + | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++ + " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++ + " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "") + )) ]. + destruct (eqd_dec τ τ'); [ idtac + | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++ + " got: " +++toString τ+++eol+++ + " wanted: "+++toString τ' + )) ]. + subst. + apply OK. + apply e. + Defined. -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 coVarKind (wcv:WeakCoerVar) : Kind := + match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end. + Coercion coVarKind : WeakCoerVar >-> Kind. +Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ). + intros. + set (weakTypeToType φ t) as wt. + destruct wt; try apply (Error error_message). + destruct h. + matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in "). + subst. + apply OK. + apply h. + Defined. -Definition cure {Γ}(ξ:WeakExprVar -> WeakType * list WeakTypeVar)(φ:WeakTypeVar->HaskTyVar Γ) - : WeakExprVar->LeveledHaskType Γ := - fun wtv => weakTypeToType φ (fst (ξ wtv)) @@ map φ (snd (ξ wtv)). +Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) := + match t with + | T_Leaf None => [] + | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with + | OK t' => [((wev:CoreVar),t')] + | _ => [] + end + | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ) + end. -Definition weakExprVarToWeakType : WeakExprVar -> WeakType := - fun wev => match wev with weakExprVar _ t => t end. - Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType. +Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) := +match lk as LK return ???(IList Kind (HaskType Γ) LK) with + | nil => match wtl with + | nil => OK INil + | _ => Error "length mismatch in mkAvars" + end + | k::lk' => match wtl with + | nil => Error "length mismatch in mkAvars" + | wt::wtl' => + weakTypeToTypeOfKind φ wt k >>= fun t => + mkAvars wtl' lk' φ >>= fun rest => + OK (ICons _ _ t rest) + end +end. + +Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool := + match vars with + | nil => ig + | v::vars' => + fun v' => + if eqd_dec v v' + then false + else update_ig ig vars' v' + end. -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 +(* does the specified variable occur free in the expression? *) +Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool := + match me with + | WELit _ => false + | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false + | WECast e co => doesWeakVarOccur wev e + | WENote n e => doesWeakVarOccur wev e + | WETyApp e t => doesWeakVarOccur wev e + | WECoApp e co => doesWeakVarOccur wev e + | WEBrak _ ec e _ => doesWeakVarOccur wev e + | WEEsc _ ec e _ => doesWeakVarOccur wev e + | WECSP _ ec e _ => doesWeakVarOccur wev e + | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2) + | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2 + | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e + | WETyLam cv e => doesWeakVarOccur wev e + | WECoLam cv e => doesWeakVarOccur wev e + | WECase vscrut escrut tbranches tc avars alts => + doesWeakVarOccur wev escrut || + if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else + ((fix doesWeakVarOccurAlts alts {struct alts} : bool := + match alts with + | T_Leaf None => false + | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *) + | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2 + end) alts) + | WELetRec mlr e => + doesWeakVarOccur wev e || + (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool := + match mlr with + | T_Leaf None => false + | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e + | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2 + end) mlr + end. +Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar) + (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool := + match alts with + | T_Leaf None => false + | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e + | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *) + | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2 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 Γ (κ::Δ). +Definition checkDistinct : + forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv). intros. - unfold HaskCoVar. - intros. - apply (ψ X TV CV env). - inversion cenv; auto. + set (distinct_decidable lv) as q. + destruct q. + exact (OK d). + exact (Error "checkDistinct failed"). Defined. -Lemma substRaw {Γ}{κ} : HaskType (κ::Γ) -> (∀ TV, @InstantiatedTypeEnv TV Γ -> TV -> @RawHaskType TV). - intro ht. - intro TV. - intro env. - intro tv. - apply ht. - apply (tv:::env). +(* FIXME: check the kind of the type of the weakexprvar to support >0 *) +Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ. + refine {| glob_kinds := nil |}. + apply wev. + intros. + apply τ. 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). + (φ:TyVarResolver Γ) + (ψ:CoVarResolver Γ Δ) + (ξ:CoreVar -> LeveledHaskType Γ ★) + (ig:CoreVar -> bool) + (τ:HaskType Γ ★) + (lev:HaskLevel Γ), + WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ 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. + fix weakExprToStrongExpr + (Γ:TypeEnv) + (Δ:CoercionEnv Γ) + (φ:TyVarResolver Γ) + (ψ:CoVarResolver Γ Δ) + (ξ:CoreVar -> LeveledHaskType Γ ★) + (ig:CoreVar -> bool) + (τ:HaskType Γ ★) + (lev:HaskLevel Γ) + (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) := + addErrorMessage ("in weakExprToStrongExpr " +++ toString we) + match we with + + | WEVar v => if ig v + then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ τ lev) + else castExpr we ("WEVar "+++toString (v:CoreVar)) τ lev (EVar Γ Δ ξ v) + + | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev) + + | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv => + weakTypeOfWeakExpr ebody >>= fun tbody => + weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => + let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in + let ig' := update_ig ig ((ev:CoreVar)::nil) in + weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' => + castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody') + + | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' => + weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' => + castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e') + + | WEEsc _ ec e tbody => φ ec >>= fun ec'' => + weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => + match lev with + | nil => Error "ill-leveled escapification" + | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e + >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e') + end + + | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage" + + | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e') + + | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => + weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => + weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil)) + (update_ig ig ((v:CoreVar)::nil)) τ lev ebody + >>= fun ebody' => + OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') + + | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 => + weakTypeToTypeOfKind φ t2 ★ >>= fun t2' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' => + OK (EApp _ _ _ _ _ _ e1' e2') + + | WETyLam tv e => let φ2 := upPhi tv φ in + weakTypeOfWeakExpr e >>= fun te => + weakTypeToTypeOfKind φ2 te ★ >>= fun τ' => + weakExprToStrongExpr _ (weakCE Δ) φ2 + (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e + >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e') + + | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => + match te with + | WForAllTy wtv te' => + let φ2 := upPhi wtv φ in + weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' => + weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' => + castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e') + | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te) + end + + | WECoApp e co => weakTypeOfWeakExpr e >>= fun te => + match te with + | WCoFunTy t1 t2 t3 => + weakTypeToType φ t1 >>= fun t1' => + match t1' with + haskTypeOfSomeKind κ t1'' => + weakTypeToTypeOfKind φ t2 κ >>= fun t2'' => + weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' => + castExpr we "WECoApp" _ _ e' >>= fun e'' => + OK (ECoApp Γ Δ κ t1'' t2'' + (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'') + end + | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te) + end + + | WECoLam cv e => let (_,t1,t2) := cv in + weakTypeOfWeakExpr e >>= fun te => + weakTypeToTypeOfKind φ te ★ >>= fun te' => + weakTypeToTypeOfKind φ t1 cv >>= fun t1' => + weakTypeToTypeOfKind φ t2 cv >>= fun t2' => + weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' => + castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') + + | WECast e co => let (t1,t2) := weakCoercionTypes co in + weakTypeToTypeOfKind φ t1 ★ >>= fun t1' => + weakTypeToTypeOfKind φ t2 ★ >>= fun t2' => + weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' => + castExpr we "WECast" _ _ + (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') + + | WELetRec rb e => + let ξ' := update_xi ξ lev _ in + let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in + let binds := + (fix binds (t:Tree ??(WeakExprVar * WeakExpr)) + : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) := + match t with + | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _) + | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e) + | T_Branch b1 b2 => + binds b1 >>= fun b1' => + binds b2 >>= fun b2' => + OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2') + end) rb + in binds >>= fun binds' => + checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct => + weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' => + OK (ELetRec Γ Δ ξ lev τ _ _ binds' e') + + | WECase vscrut escrut tbranches tc avars alts => + weakTypeOfWeakExpr escrut >>= fun tscrut => + weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' => + if doesWeakVarOccurAlts vscrut alts + then Error "encountered a Case which actually used its binder - these should have been desugared away!!" + else mkAvars avars (tyConKind tc) φ >>= fun avars' => + weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => + (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree + ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac & + Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) := + match t with + | T_Leaf None => OK [] + | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => + mkStrongAltConPlusJunk' tc ac >>= fun sac => + list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") + >>= fun exprvars' => + (let case_pf := tt in _) >>= fun pf => + let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in + weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ) + (sacpj_psi sac _ _ avars' ψ) + (scbwv_xi scb ξ lev) + (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb)))) + (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => + let case_case := tt in OK [ _ ] + | T_Branch b1 b2 => + mkTree b1 >>= fun b1' => + mkTree b2 >>= fun b2' => + OK (b1',,b2') + end) alts >>= fun tree => + + weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' => + castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree) + end)); try clear binds; try apply ConcatenableString. + + destruct case_some. + apply (addErrorMessage "case_some"). simpl. - destruct cv. - matchTypes me w "HaskWeak LetRec". + destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message). + matchThings h (unlev (ξ' wev)) "LetRec". + destruct wev. + rewrite matchTypeVars_pf. + clear matchTypeVars_pf. + set (e' (unlev (ξ' (weakExprVar c w)))) as e''. + destruct e''; try apply (Error error_message). 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. + unfold ξ'. 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'. + induction (leaves (varsTypes rb φ)). + simpl; auto. + destruct (ξ c). + simpl. + apply e1. + rewrite mapleaves. + apply rb_distinct. + + destruct case_pf. + set (distinct_decidable (vec2list exprvars')) as dec. + destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ]. + apply OK; auto. + + destruct case_case. + exists sac. + exists scb. + apply ebranch'. - destruct case_WEEsc_bogus; intros. - apply (Error "attempt to use escape symbol at level zero"). + Defined. - 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.