X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=224d70b54f624160c7013dfd97a1638a51a3d9bf;hp=1bab8f5ea992798fee03625f45cbb2d2997beadd;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321 diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 1bab8f5..224d70b 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -8,11 +8,12 @@ Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import General. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreTypes. Require Import HaskCoreVars. Require Import HaskWeakTypes. Require Import HaskWeakVars. +Require Import HaskWeak. Require Import HaskCoreToWeak. Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". @@ -20,7 +21,6 @@ Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Const Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta". Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys". -(* FIXME: might be a better idea to panic here than simply drop things that look wrong *) Definition dataConExTyVars cdc := filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). Opaque dataConExTyVars. @@ -52,28 +52,7 @@ Inductive DataCon : TyCon -> Type := Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon. (*Opaque DataCon.*) -Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool. - intros. - destruct dc1. - destruct dc2. - exact (if eqd_dec cdc cdc0 then true else false). - Defined. - -Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2). - -Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc). - intros. - apply Build_EqDecidable. - intros. - set (trust_compare_datacons _ v1 v2) as x. - set (compare_datacons tc v1 v2) as y. - assert (y=compare_datacons tc v1 v2). reflexivity. - destruct y; rewrite <- H in x. - left; auto. - right; auto. - Defined. - -Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc). +Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc). (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *) Section Raw. @@ -99,27 +78,25 @@ Section Raw. Inductive RawCoercionKind : Type := mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind. - Section CV. - - (* the PHOAS type which stands for coercion variables of System FC *) - - - (* Figure 7: γ, δ *) - Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *). -(* - | CoVar : CV -> RawHaskCoer (* g *) - | CoType : RawHaskType -> RawHaskCoer (* τ *) - | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) - | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) - | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) - | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) - | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) - | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) - | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) - | CoLeft : RawHaskCoer -> RawHaskCoer (* left *) - | CoRight : RawHaskCoer -> RawHaskCoer (* right *). -*) - End CV. + (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *) + Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := . + (* + * This has been disabled until we manage to reconcile SystemFC's + * coercions with what GHC actually implements (they are not the + * same!) + * + | CoVar : CV -> RawHaskCoer (* g *) + | CoType : RawHaskType -> RawHaskCoer (* τ *) + | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) + | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) + | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) + | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) + | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) + | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) + | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) + | CoLeft : RawHaskCoer -> RawHaskCoer (* left *) + | CoRight : RawHaskCoer -> RawHaskCoer (* right *). + *) End Raw. Implicit Arguments TCon [ [TV] ]. @@ -184,7 +161,7 @@ Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV := fun TV env => σ TV env (cv TV env). Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:= fun TV env => @TCode TV (TVar (v TV env)) (t TV env). -Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc)) +Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc)) := fun TV ite => TCon tc. Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ := fun TV ite => TApp (t1 TV ite) (t2 TV ite). @@ -314,13 +291,6 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ apply weakCK. apply IHκ. Defined. -(* -Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := - match κ as K return list (HaskCoercionKind (app K Γ)) with - | nil => hck - | _ => map weakCK' hck - end. -*) Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := map weakCK' hck. Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) := @@ -329,17 +299,13 @@ Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv T forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂ := fun TV ite tv => (f TV (weakITE ite) tv). -(* I keep mixing up left/right folds *) -(* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *) -(*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*) - Fixpoint caseType0 {Γ}(lk:list Kind) : IList _ (HaskType Γ) lk -> - HaskType Γ (fold_right KindTypeFunction ★ lk) -> + HaskType Γ (fold_right KindArrow ★ lk) -> HaskType Γ ★ := match lk as LK return IList _ (HaskType Γ) LK -> - HaskType Γ (fold_right KindTypeFunction ★ LK) -> + HaskType Γ (fold_right KindArrow ★ LK) -> HaskType Γ ★ with | nil => fun _ ht => ht @@ -352,7 +318,7 @@ Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) (* like a GHC DataCon, but using PHOAS representation for types and coercions *) Record StrongAltCon {tc:TyCon} := { sac_tc := tc -; sac_altcon : AltCon +; sac_altcon : WeakAltCon ; sac_numExTyVars : nat ; sac_numCoerVars : nat ; sac_numExprVars : nat @@ -364,7 +330,7 @@ Record StrongAltCon {tc:TyCon} := ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ }. Coercion sac_tc : StrongAltCon >-> TyCon. -Coercion sac_altcon : StrongAltCon >-> AltCon. +Coercion sac_altcon : StrongAltCon >-> WeakAltCon. Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ. @@ -384,13 +350,35 @@ Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18). Fixpoint update_ξ `{EQD_VV:EqDecidable VV}{Γ} (ξ:VV -> LeveledHaskType Γ ★) - (vt:list (VV * LeveledHaskType Γ ★)) + (lev:HaskLevel Γ) + (vt:list (VV * HaskType Γ ★)) : VV -> LeveledHaskType Γ ★ := match vt with | nil => ξ - | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' + | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v' end. +Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v, + not (In v (map (@fst _ _) varstypes)) -> + (update_ξ ξ lev varstypes) v = ξ v. + intros. + induction varstypes. + reflexivity. + simpl. + destruct a. + destruct (eqd_dec v0 v). + subst. + simpl in H. + assert False. + apply H. + auto. + inversion H0. + apply IHvarstypes. + unfold not; intros. + apply H. + simpl. + auto. + Defined. (***************************************************************************************************) @@ -490,7 +478,9 @@ end. Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) := compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)). -(* This is not provable in Coq's logic because the Coq function space +(* The PHOAS axioms + * + * This is not provable in Coq's logic because the Coq function space * is "too big" - although its only definable inhabitants are Coq * functions, it is not provable in Coq that all function space * inhabitants are definable (i.e. there are no "exotic" inhabitants). @@ -545,7 +535,7 @@ Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ). (* ToString instance for PHOAS types *) Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string := match t with - | TVar _ v => "tv" +++ v + | TVar _ v => "tv" +++ toString v | TCon tc => toString tc | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~" +++typeToString' false n t2+++")=>" @@ -562,11 +552,12 @@ Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) else (typeToString' true n t1)+++" "+++(typeToString' false n t2) end | TArrow => "(->)" - | TAll k f => let alpha := "tv"+++n - in "(forall "+++ alpha +++ "{:}"+++ k +++")"+++ + | TAll k f => let alpha := "tv"+++ toString n + in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++ typeToString' false (S n) (f n) - | TCode ec t => "<["+++(typeToString' true n ec)+++"]>@"+++(typeToString' false n t) - | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]" + | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec) + | TyFunApp tfc 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 := match t with