X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=0acc0af06f750046066236e227305f253a00d48b;hp=a15b81daf63c06e54552cbd899d3756bf79707a7;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=ee5aaad57d76400e9b8736d4a12d2804f99f329c diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index a15b81d..0acc0af 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -10,34 +10,42 @@ 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 HaskCoreTypes. Require Import HaskCoreVars. +Require Import HaskCoreToWeak. +Require Import HaskCoreTypes. Open Scope string_scope. -Definition TyVarResolver Γ := forall wt:WeakTypeVar, HaskTyVar Γ wt. -Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ. +Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). +Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ). + +Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ. + rewrite <- ass_app in lt. + exact lt. + Defined. -Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). +Definition upPhi {Γ}(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)). + 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)(φ:TyVarResolver Γ) +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. @@ -52,7 +60,7 @@ Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ: apply X. Defined. -Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. +Definition substphi {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. induction lk. intro q; apply q. simpl. @@ -69,9 +77,8 @@ Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ (* 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 Γ (φ:TyVarResolver Γ ), (TyVarResolver (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. @@ -82,9 +89,9 @@ Variable emptyφ : TyVarResolver nil. Definition mkPhi (lv:list WeakTypeVar) : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)). - set (upφ'(Γ:=nil) lv emptyφ) as φ'. - rewrite <- app_nil_end in φ'. - apply φ'. + 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)). @@ -95,7 +102,7 @@ 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)) ]. + [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ]. Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★). intros. @@ -116,15 +123,17 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★. 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 _ - | 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' => _ + | 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' => @@ -139,59 +148,73 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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" + | 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))). + 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:: "). - + 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. + 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 (φ (@fixkind ★ ec) TV X)). + 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' ]. @@ -203,6 +226,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')). destruct case_WForAllTy. + apply (addErrorMessage "case_WForAllTy"). destruct t1. matchThings ★ κ "Kind mismatch in WForAllTy: ". subst. @@ -212,9 +236,6 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) apply h. Defined. - -Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error". - (* 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). @@ -223,10 +244,11 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★). intro avars. intro ct. + apply (addErrorMessage "weakTypeToType'"). set (ilmap (@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 (@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'". @@ -249,7 +271,7 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds Definition mkStrongAltCon : @StrongAltCon tc. refine - {| sac_altcon := DataAlt dc + {| sac_altcon := WeakDataAlt dc ; sac_numCoerVars := length (dataConCoerKinds dc) ; sac_numExprVars := length (dataConFieldTypes dc) ; sac_ekinds := dataConExKinds dc @@ -311,16 +333,17 @@ 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. @@ -337,13 +360,13 @@ Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. 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 "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; 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 *. @@ -351,16 +374,16 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConP apply OK; refine {| sacpj_sac := {| sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil - ; sac_altcon := LitAlt h + ; sac_altcon := WeakLitAlt h |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + 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 := DEFAULT |} |}. + ; sac_altcon := WeakDEFAULT |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. rewrite weakCK'_nil_inert. apply ψ. Defined. @@ -370,38 +393,47 @@ Definition weakExprVarToWeakType : WeakExprVar -> WeakType := Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ. -Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) : - WeakCoerVar -> HaskCoVar Γ (κ::Δ). +Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) : + WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)). intros. + refine (ψ X >>= _). unfold HaskCoVar. intros. - apply (ψ X TV CV env). + apply OK. + intros. inversion cenv; auto. Defined. (* 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 _ CoreVarEqDecidable Γ Δ ξ τ) - : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ'). +Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l) + : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l'). + apply (addErrorMessage ("castExpr " +++ err_msg)). 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 "+++τ')) ]. + 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. Definition coVarKind (wcv:WeakCoerVar) : Kind := - match wcv with weakCoerVar _ κ _ _ => κ end. + match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end. Coercion coVarKind : WeakCoerVar >-> Kind. -Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ). +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 weakTypeToType'': ". + matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in "). subst. apply OK. apply h. @@ -410,14 +442,13 @@ Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakTyp Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) := match t with | T_Leaf None => [] - | T_Leaf (Some (wev,e)) => match weakTypeToType'' φ wev ★ with - | Error _ => [] + | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with | OK t' => [((wev:CoreVar),t')] + | _ => [] end | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ) end. - 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 @@ -427,21 +458,96 @@ match lk as LK return ???(IList Kind (HaskType Γ) LK) with | k::lk' => match wtl with | nil => Error "length mismatch in mkAvars" | wt::wtl' => - weakTypeToType'' φ wt k >>= fun t => + 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. + +(* 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. + +Definition checkDistinct : + forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv). + intros. + set (distinct_decidable lv) as q. + destruct q. + exact (OK d). + exact (Error "checkDistinct failed"). + Defined. + +(* 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. + Definition weakExprToStrongExpr : forall (Γ:TypeEnv) (Δ:CoercionEnv Γ) (φ:TyVarResolver Γ) (ψ:CoVarResolver Γ Δ) (ξ:CoreVar -> LeveledHaskType Γ ★) + (ig:CoreVar -> bool) (τ:HaskType Γ ★) (lev:HaskLevel Γ), - WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ). + WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ). refine (( fix weakExprToStrongExpr (Γ:TypeEnv) @@ -449,149 +555,165 @@ Definition weakExprToStrongExpr : forall (φ:TyVarResolver Γ) (ψ:CoVarResolver Γ Δ) (ξ:CoreVar -> LeveledHaskType Γ ★) + (ig:CoreVar -> bool) (τ:HaskType Γ ★) (lev:HaskLevel Γ) - (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) := + (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) := + addErrorMessage ("in weakExprToStrongExpr " +++ toString we) match we with - | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v) + | 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 "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev) + | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev) - | WELam ev e => weakTypeToType'' φ ev ★ >>= fun tv => - weakTypeOfWeakExpr e >>= fun t => - weakTypeToType'' φ t ★ >>= fun τ' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil)) - τ' _ e >>= fun e' => - castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e') + | 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 => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => - castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e') + | 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 => weakTypeToType'' φ tbody ★ >>= fun tbody' => + | WEEsc _ ec e tbody => φ ec >>= fun ec'' => + weakTypeToTypeOfKind φ 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') + | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e + >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' 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:CoreVar),tv@@lev)::nil)) τ lev ebody + | 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 => - weakTypeToType'' φ t2 ★ >>= fun t2' => - weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' => - weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' => + 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 φ' := upφ tv φ in + | WETyLam tv e => let φ2 := upPhi 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'') + weakTypeToTypeOfKind φ2 te ★ >>= fun τ' => + weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2 + (fun x => (ψ x) >>= fun y => + OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e + >>= fun e' => castExpr we "WETyLam2" _ _ + (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 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) + 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 - (* 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 co => weakTypeOfWeakExpr e >>= fun te => match te with | WCoFunTy t1 t2 t3 => weakTypeToType φ t1 >>= fun t1' => match t1' with haskTypeOfSomeKind κ t1'' => - weakTypeToType'' φ t2 κ >>= fun t2'' => - weakTypeToType'' φ t3 ★ >>= fun t3'' => - weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' => - castExpr "WECoApp" _ e' >>= fun e'' => + 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 "+++te) + | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te) end - | WECoLam cv e => let (_,_,t1,t2) := cv in + | WECoLam cv e => let (_,t1,t2) := cv in weakTypeOfWeakExpr e >>= fun te => - weakTypeToType'' φ te ★ >>= fun te' => - weakTypeToType'' φ t1 cv >>= fun t1' => - weakTypeToType'' φ t2 cv >>= fun t2' => - weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' => - castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') - - | WECast e co => let (κ,t1,t2,_) := co in - weakTypeToType'' φ t1 ★ >>= fun t1' => - weakTypeToType'' φ t2 ★ >>= fun t2' => - weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' => - castExpr "WECast" _ + 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_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) - in let binds := + 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 Γ Δ φ ψ ξ' τ lev e) + | 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' => - weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' => - OK (ELetRec Γ Δ ξ lev τ _ binds' e') - - | WECase vscrut e tbranches tc avars alts => - mkAvars avars (tyConKind tc) φ >>= fun avars' => - weakTypeToType'' φ tbranches ★ >>= fun tbranches' => - let ξ' := update_ξ ξ (((vscrut:CoreVar), _ @@lev)::nil) in -(fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree - ??{scb - : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' - & - Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) - (scbwv_ξ scb ξ' lev) (weakLT' (tbranches' @@ 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 scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in - weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ) - (scbwv_ξ scb ξ' lev) (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 Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' => - castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun evar => - castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' evar tree) >>= fun ecase' => - OK (ELet _ _ _ _ _ lev (vscrut:CoreVar) e' ecase') - end)). - + 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 (weakTypeToType'' φ wev ★); try apply (Error error_message). + destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message). matchThings h (unlev (ξ' wev)) "LetRec". destruct wev. rewrite matchTypeVars_pf. @@ -600,11 +722,25 @@ Definition weakExprToStrongExpr : forall destruct e''; try apply (Error error_message). apply OK. apply ELR_leaf. + unfold ξ'. + simpl. + 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. - clear mkTree t o p e p0 p1 p2 alts weakExprToStrongExpr ebranch. + exists sac. exists scb. apply ebranch'. + Defined.