From: Adam Megacz Date: Fri, 24 Jun 2011 11:29:27 +0000 (-0700) Subject: allow quantification over any tyvar in the environment, not just the first X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=489b12c6c491b96c37839610d33fbdf666ee527f;hp=6282ce834832ba35e81d8019cae1ca38d187d07e allow quantification over any tyvar in the environment, not just the first --- diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index dd07482..c7625b8 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -46,7 +46,6 @@ Set Printing Width 130. *) Section HaskFlattener. - Ltac eqd_dec_refl' := match goal with | [ |- context[@eqd_dec ?T ?V ?X ?X] ] => @@ -232,12 +231,12 @@ Section HaskFlattener. flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)). Axiom flatten_commutes_with_HaskTApp : - forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), - flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) = - HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ). + forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), + flatten_type (HaskTApp (weakF_ σ) (FreshHaskTyVar_ κ)) = + HaskTApp (weakF_ (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar_(n:=n) κ). - Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t, - flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t). + Axiom flatten_commutes_with_weakLT : forall n (Γ:TypeEnv) κ t, + flatten_leveled_type (weakLT_(n:=n)(Γ:=Γ)(κ:=κ) t) = weakLT_(n:=n)(Γ:=Γ)(κ:=κ) (flatten_leveled_type t). Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v, flatten_type (g v) = g v. @@ -407,6 +406,9 @@ Section HaskFlattener. apply precompose. Defined. + + + (* useful for cutting down on the pretty-printed noise Notation "` x" := (take_lev _ x) (at level 20). @@ -864,7 +866,7 @@ Section HaskFlattener. | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _ | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _ - | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _ + | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _ | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ @@ -1161,8 +1163,8 @@ Section HaskFlattener. rewrite flatten_commutes_with_HaskTApp. eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ]. simpl. - set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a. - set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'. + set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT_(n:=n)(κ:=κ)) Σ)) as a. + set (mapOptionTree (weakLT_(n:=n)(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'. assert (a=q'). unfold a. unfold q'. diff --git a/src/HaskProof.v b/src/HaskProof.v index 84eaa0b..7f15825 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -74,8 +74,8 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ] | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l] -| RAbsT : ∀ Γ Δ Σ κ σ l, - Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)] +| RAbsT : ∀ Γ Δ Σ κ σ l n, + Rule [(list_ins n κ Γ)> (weakCE_ Δ) > mapOptionTree weakLT_ Σ |- [ HaskTApp (weakF_ σ) (FreshHaskTyVar_ _) ]@(weakL_ l)] [Γ>Δ > Σ |- [HaskTAll κ σ ]@l] | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l, @@ -131,7 +131,7 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l) | Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q ) | Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q ) -| Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q ) +| Flat_RAbsT : ∀ Γ Σ κ σ a q n , Rule_Flat (RAbsT Γ Σ κ σ a q n) | Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q ) | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l) | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 ) diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 716a983..e85bb39 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -184,7 +184,7 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | RGlobal _ _ _ _ _ => "Global" | RLam _ _ _ _ _ _ => "Abs" | RCast _ _ _ _ _ _ _ => "Cast" - | RAbsT _ _ _ _ _ _ => "AbsT" + | RAbsT _ _ _ _ _ _ _ => "AbsT" | RAppT _ _ _ _ _ _ _ => "AppT" | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo" | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo" diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index f50c586..ab10fd8 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -760,7 +760,7 @@ Section HaskProofToStrong. | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ | RLam Γ Δ Σ tx te x => let case_RLam := tt in _ | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _ - | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _ + | RAbsT Γ Δ Σ κ σ a n => let case_RAbsT := tt in _ | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ @@ -940,12 +940,12 @@ Section HaskProofToStrong. apply (ileaf X). destruct case_RAbsT. - apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. + apply ILeaf; simpl; intros; refine (X_ (weakLT_ ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon. rewrite mapOptionTree_compose. rewrite <- H. reflexivity. apply ileaf in X. simpl in *. - apply ETyLam. + apply (ETyLam _ _ _ _ _ _ n). apply X. destruct case_RAppCo. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index eaf1341..0d1cecb 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -226,7 +226,7 @@ Section HaskSkolemizer. | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _ | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _ | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _ - | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _ + | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _ | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ @@ -472,7 +472,10 @@ Section HaskSkolemizer. destruct case_RAbsT. simpl. - destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ]. + destruct lev; simpl. + apply nd_rule. + apply SFlat. + apply (@RAbsT Γ Δ Σ κ σ nil n). apply (Prelude_error "RAbsT at depth>0"). destruct case_RAppCo. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 874b368..6629511 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -47,8 +47,8 @@ Section HaskStrong. | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l - | ETyLam : ∀ Γ Δ ξ κ σ l, - Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l + | ETyLam : ∀ Γ Δ ξ κ σ l n, + Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l | ECase : forall Γ Δ ξ l tc tbranches atypes, Expr Γ Δ ξ (caseType tc atypes) l -> Tree ??{ sac : _ @@ -90,7 +90,7 @@ Section HaskStrong. | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")" | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)" | ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2" - | ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e + | ETyLam _ _ _ k _ _ _ e => "\@_ ->"+++ exprToString e | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => "\~_ ->"+++ exprToString e | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME" | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 8ae0d09..e93ddd9 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -520,7 +520,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : | EBrak Γ Δ ξ ec t lev e => expr2antecedent e | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e | ENote Γ Δ ξ t l n e => expr2antecedent e - | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e + | ETyLam Γ Δ ξ κ σ l n e => expr2antecedent e | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e @@ -1117,7 +1117,7 @@ Definition expr2proof : | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) - | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ETyLam Γ Δ ξ κ σ l n e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index deb7adc..8bb52e1 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -79,6 +79,18 @@ Section HaskStrongToWeak. Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) := tv::::ite. + Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) + : InstantiatedTypeEnv TV (list_ins n κ Γ). + rewrite list_ins_app. + rewrite <- (list_take_drop _ Γ n) in ite. + apply ilist_app. + apply ilist_chop in ite; auto. + apply ICons. + apply tv. + apply ilist_chop' in ite. + apply ite. + Defined. + Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)) : UniqM WeakCoercion := bind t1' = @typeToWeakType Γ κ t1 ite @@ -144,8 +156,8 @@ Section HaskStrongToWeak. | ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ ; return WECast e' c' - | ETyLam _ _ _ k _ _ e => fun ite => bind tv = mkWeakTypeVar k - ; bind e' = exprToWeakExpr χ e (updateITE tv ite) + | ETyLam _ _ _ k _ _ n e => fun ite => bind tv = mkWeakTypeVar k + ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite) ; return WETyLam tv e' | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite ; bind t2' = typeToWeakType σ₂ ite diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index e5a10ba..46d74cc 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -155,6 +155,7 @@ Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@Ins Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ. Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env. + Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★ := fun TV env => TAll κ (σ TV env). Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) @@ -350,21 +351,41 @@ Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:Instanti unfold InstantiatedCoercionEnv; simpl. apply vec_cons; auto. Defined. + (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *) -Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ - := ilist_tail ite. +Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := ilist_tail ite. +Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ. +Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv := fun TV ite => (cv' TV (weakITE ite)). +Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ := fun TV ite => lt TV (weakITE ite). +Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt. +Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ := match lt with t @@ l => weakT t @@ weakL l end. +Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) + : InstantiatedCoercionEnv TV CV Γ Δ. + intros. + unfold InstantiatedCoercionEnv; intros. + unfold InstantiatedCoercionEnv in ice. + unfold weakCE in ice. + simpl in ice. + rewrite <- map_preserves_length in ice. + apply ice. + Defined. +Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ). + unfold HaskCoercionKind in *. + intros. + apply hck; clear hck. + inversion X; subst; auto. + Defined. +Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := + fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)). +Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : + forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂ + := fun TV ite tv => (f TV (weakITE ite) tv). + + Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ. induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined. -Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) - := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ. -Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv - := fun TV ite => (cv' TV (weakITE ite)). Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv. induction κ; auto. apply weakV; auto. Defined. -Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ - := fun TV ite => lt TV (weakITE ite). -Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) - := map weakV lt. Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂. induction κ; auto. apply weakT; auto. Defined. Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂. @@ -375,34 +396,12 @@ Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) apply lt. apply X. Defined. -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 weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ). induction κ; auto. apply weakL; auto. Defined. -Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ - := match lt with t @@ l => weakT t @@ weakL l end. Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂ := match lt with t @@ l => weakT' t @@ weakL' l end. Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ). induction κ; auto. apply weakCE; auto. Defined. -Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) - : InstantiatedCoercionEnv TV CV Γ Δ. - intros. - unfold InstantiatedCoercionEnv; intros. - unfold InstantiatedCoercionEnv in ice. - unfold weakCE in ice. - simpl in ice. - rewrite <- map_preserves_length in ice. - apply ice. - Defined. -Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ). - unfold HaskCoercionKind in *. - intros. - apply hck; clear hck. - inversion X; subst; auto. - Defined. Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ). induction κ; auto. apply weakCK. @@ -410,11 +409,80 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Defined. Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := map weakCK' hck. -Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := - fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)). -Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : - forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂ - := fun TV ite tv => (f TV (weakITE ite) tv). + +Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ. + rewrite list_ins_app in ite. + set (weakITE' ite) as ite'. + set (ilist_chop ite) as a. + rewrite <- (list_take_drop _ Γ n). + apply ilist_app; auto. + inversion ite'; auto. + Defined. + +Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv. + unfold HaskTyVar; intros. + unfold HaskTyVar in cv'. + apply (cv' TV). + apply weakITE_ in env. + apply env. + Defined. + +Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂. + unfold HaskType; intros. + apply lt. + apply weakITE_ in X. + apply X. + Defined. +Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ). + unfold HaskLevel; intros. + unfold HaskLevel in lev. + eapply map. + apply weakV_. + apply lev. + Defined. +Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ := + match lt with t@@l => weakT_ t @@ weakL_ l end. +Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ). + unfold HaskCoercionKind; intros. + unfold HaskCoercionKind in hck. + apply hck. + apply weakITE_ in X. + apply X. + Defined. +Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ. +Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) : + forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂. + intros. + apply f. + apply weakITE_ in env. + apply env. + apply X. + Defined. +Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ). + unfold HaskCoVar; intros. + unfold HaskCoVar in cv'. + apply (cv' TV). + apply weakITE_ in env. + apply env. + unfold InstantiatedCoercionEnv. + unfold InstantiatedCoercionEnv in cenv. + replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv. + apply cenv. + unfold weakCE_. + rewrite <- map_preserves_length. + reflexivity. + Defined. + +Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ. + intros. + unfold HaskTyVar. + intros. + rewrite list_ins_app in env. + apply weakITE' in env. + inversion env; subst; auto. + Defined. + + Fixpoint caseType0 {Γ}(lk:list Kind) : IList _ (HaskType Γ) lk -> diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index d8dcf42..0acc0af 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -26,6 +26,11 @@ Open Scope string_scope. 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 upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). unfold TyVarResolver. refine (fun tv' => @@ -604,9 +609,11 @@ Definition weakExprToStrongExpr : forall | 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') + 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