From: Adam Megacz Date: Mon, 9 May 2011 04:21:45 +0000 (-0700) Subject: allow rank-1 polymorphic types for globals X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=e4fcbccb71fc54544e9acc62e95d1d15ec86294b allow rank-1 polymorphic types for globals --- diff --git a/src/HaskProof.v b/src/HaskProof.v index a5e4abd..8e4be3f 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -73,7 +73,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := (* SystemFC rules *) | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]] -| RGlobal : ∀ Γ Δ τ l, WeakExprVar -> Rule [ ] [Γ>Δ> [] |- [τ @@l]] +| RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v @@l]] | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 4773eff..edac1aa 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -101,7 +101,7 @@ Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath ; let body := t1'+++(rawLatexMath " ")+++t2' in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body) end - | TyFunApp tfc lt => bind rest = typeListToRawLatexMath false lt + | TyFunApp tfc _ _ lt => bind rest = typeListToRawLatexMath false lt ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++ (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++ (rawLatexMath "}")+++ diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 3aee219..b14a53e 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -569,7 +569,6 @@ Section HaskProofToStrong. destruct case_RGlobal. apply ILeaf; simpl; intros; refine (return ILeaf _ _). apply EGlobal. - apply wev. destruct case_RLam. apply ILeaf. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 478985d..f9d9f3d 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -31,7 +31,7 @@ Section HaskStrong. Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type := (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *) - | EGlobal: ∀ Γ Δ ξ t, WeakExprVar -> Expr Γ Δ ξ t + | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v @@ lev) | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) @@ -79,7 +79,7 @@ Section HaskStrong. Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string := match exp with | EVar Γ' _ ξ' ev => "var."+++ toString ev - | EGlobal Γ' _ ξ' t wev => "global." +++ toString (wev:CoreVar) + | EGlobal Γ' _ ξ' g v _ => "global." +++ toString (g:CoreVar) | ELam Γ' _ _ tv _ _ cv e => "\("+++ toString cv +++":t) -> "+++ exprToString e | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2 | ELit _ _ _ lit _ => "lit."+++toString lit diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 13f4907..8cd5688 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -519,7 +519,7 @@ Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstype Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := match exp as E in Expr Γ Δ ξ τ with - | EGlobal Γ Δ ξ _ _ => [] + | EGlobal Γ Δ ξ _ _ _ => [] | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2) @@ -929,7 +929,7 @@ Definition expr2proof : refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] := match exp as E in Expr Γ Δ ξ τ with - | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _ + | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _ | EVar Γ Δ ξ ev => let case_EVar := tt in _ | ELit Γ Δ ξ lit lev => let case_ELit := tt in _ | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in @@ -983,8 +983,7 @@ Definition expr2proof : destruct case_EGlobal. apply nd_rule. simpl. - destruct t as [t lev]. - apply (RGlobal _ _ _ _ wev). + apply (RGlobal _ _ _ g). destruct case_EVar. apply nd_rule. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 79d954c..42790b3 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -61,7 +61,7 @@ Section HaskStrongToWeak. | WTyVarTy ec => return WCodeTy ec t2' | _ => failM "impossible" end - | TyFunApp tfc tls => bind tls' = rawHaskTypeListToWeakType tls + | TyFunApp tfc _ _ tls => bind tls' = rawHaskTypeListToWeakType tls ; return WTyFunApp tfc tls' end with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) := @@ -111,7 +111,8 @@ Section HaskStrongToWeak. -> UniqM WeakExpr := match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with | EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end - | EGlobal Γ' _ ξ' t wev => fun ite => return WEVar wev + | EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v)) + ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g)) | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite ; bind ev' = mkWeakExprVar tv' ; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 224d70b..7ce04fb 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -69,7 +69,7 @@ Section Raw. | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *) | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *) | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *) - | TyFunApp : ∀ tf, RawHaskTypeList (fst (tyFunKind tf)) -> RawHaskType (snd (tyFunKind tf)) (* S_n *) + | TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *) with RawHaskTypeList : list Kind -> Type := | TyFunApp_nil : RawHaskTypeList nil | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl). @@ -168,27 +168,31 @@ Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskTy Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ := fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite). -(* PHOAS substitution on types *) -Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁) - : @HaskType Γ κ₂ := -fun TV env => - (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ := +Section Flatten. + Context {TV:Kind -> Type }. +Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ := match exp with | TVar _ x => x - | TAll _ y => TAll _ (fun v => flattenT _ (y (TVar v))) - | TApp _ _ x y => TApp (flattenT _ x) (flattenT _ y) + | TAll _ y => TAll _ (fun v => flattenT (y (TVar v))) + | TApp _ _ x y => TApp (flattenT x) (flattenT y) | TCon tc => TCon tc - | TCoerc _ t1 t2 t => TCoerc (flattenT _ t1) (flattenT _ t2) (flattenT _ t) + | TCoerc _ t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t) | TArrow => TArrow - | TCode v e => TCode (flattenT _ v) (flattenT _ e) - | TyFunApp tfc lt => TyFunApp tfc (flattenTyFunApp _ lt) + | TCode v e => TCode (flattenT v) (flattenT e) + | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt) end with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk := match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with | TyFunApp_nil => TyFunApp_nil - | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest) - end - for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)). + | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT t) (flattenTyFunApp _ rest) + end. +End Flatten. + +(* PHOAS substitution on types *) +Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁) + : @HaskType Γ κ₂ := + fun TV env => + flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)). Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20). Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20). @@ -197,6 +201,13 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) := match lht with t@@l => t end. +Structure Global Γ := +{ glob_wv : WeakExprVar +; glob_kinds : list Kind +; glob_tf : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★ +}. +Coercion glob_tf : Global >-> Funclass. +Coercion glob_wv : Global >-> WeakExprVar. @@ -461,7 +472,7 @@ match t1 with | TArrow => match t2 with TArrow => true | _ => false end | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end | TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end -| TyFunApp tfc lt => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end +| TyFunApp tfc kl k lt => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end end with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool := match t1 with @@ -556,7 +567,7 @@ Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++ typeToString' false (S n) (f n) | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec) - | TyFunApp tfc lt => toString tfc+++ "_" +++ toString n+++" ["+++ + | TyFunApp tfc kl k lt => toString tfc+++ "_" +++ toString n+++" ["+++ (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]" end with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string := diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 6d4bf16..b9ac068 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -176,7 +176,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) apply OK. eapply haskTypeOfSomeKind. unfold HaskType; intros. - apply TyFunApp. + apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))). apply lt'. apply X. @@ -519,6 +519,14 @@ Definition checkDistinct : 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 Γ) @@ -544,7 +552,7 @@ Definition weakExprToStrongExpr : forall match we with | WEVar v => if ig v - then OK (EGlobal Γ Δ ξ (τ@@lev) 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)