Require Import Coq.Lists.List.
Require Import General.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreTypes.
Require Import HaskCoreVars.
Require Import HaskWeakTypes.
Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
-Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
+Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConTheta".
Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
Definition dataConExTyVars cdc :=
- filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
+ filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (dataConExVars_ cdc)).
Opaque dataConExTyVars.
Definition dataConCoerKinds cdc :=
filter (map (fun x => match x with EqPred t1 t2 =>
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 ★)
Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
+Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
+
Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
match lht with t@@l => t end.
Coercion glob_tf : Global >-> Funclass.
Coercion glob_wv : Global >-> WeakExprVar.
+(* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
+(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
+Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
+ match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
+ | KindStar => fun x' =>
+ match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
+ list (RawHaskType _ KindStar) with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => a::b
+ | _ => fun _ _ => nil
+ end
+ | _ => fun _ _ => nil
+ end x''
+ | _ => fun _ => nil
+ end
+ | _ => fun _ _ => nil
+ end
+ | _ => fun _ _ => nil
+ end) x (take_arg_types y)
+ | _ => nil
+ end.
+
+Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
+ match exp as E in RawHaskType _ K return nat with
+ | TApp κ₁ κ₂ x y =>
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
+ | KindStar => fun x' =>
+ match x' return nat -> nat with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun a b => S b
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end x''
+ | _ => fun _ => 0
+ end
+ | _ => fun _ _ => 0
+ end
+ | _ => fun _ _ => 0
+ end) x (count_arg_types y)
+ | _ => 0
+ end.
+
+ Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
+ intros.
+ induction Γ.
+ apply INil.
+ apply ICons; auto.
+ apply tt.
+ Defined.
+
+Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
+ fun pf =>
+ fun TV ite =>
+ match take_arg_types (ht TV ite) with
+ | nil => Prelude_error "impossible"
+ | x::y => x
+ end.
+
+(* From (t1->(t2->(t3-> ... t))), return t *)
+(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
+Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
+ match exp as E in RawHaskType _ K return RawHaskType _ K with
+ | TApp κ₁ κ₂ x y =>
+ let q :=
+ (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
+ | KindStar =>
+ match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
+ | KindStar => fun x' =>
+ match x' return (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+ | TApp κ₁'' κ₂'' w'' x'' =>
+ match κ₂'' as K2'' return RawHaskType TV K2'' -> (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
+ | KindStar =>
+ match w'' with
+ | TArrow => fun _ b => Some b
+ | _ => fun _ b => None
+ end
+ | _ => fun _ b => None
+ end x''
+ | _ => fun _ => None
+ end
+ | _ => fun _ _ => None
+ end
+ | _ => fun _ _ => None
+ end) x (drop_arg_types y)
+ in match q with
+ | None => TApp x y
+ | Some y => y
+ end
+ | b => b
+ end.
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 Γ κ) κ₂.
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.
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 ->
; sac_numExprVars : nat
; sac_ekinds : vec Kind sac_numExTyVars
; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
-; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
-; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
-; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
-; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
+; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ
+; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
+; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
+; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
}.
Coercion sac_tc : StrongAltCon >-> TyCon.
Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
-Fixpoint update_ξ
+Fixpoint update_xi
`{EQD_VV:EqDecidable VV}{Γ}
(ξ:VV -> LeveledHaskType Γ ★)
(lev:HaskLevel Γ)
: VV -> LeveledHaskType Γ ★ :=
match vt with
| nil => ξ
- | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
+ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
end.
-Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
not (In v (map (@fst _ _) varstypes)) ->
- (update_ξ ξ lev varstypes) v = ξ v.
+ (update_xi ξ lev varstypes) v = ξ v.
intros.
induction varstypes.
reflexivity.
Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
{ toString := typeToString }.
+
+Definition TBool {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp BoolTyCon _ _ TyFunApp_nil.
+Definition TInt {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp IntTyCon _ _ TyFunApp_nil.
projects / coq-hetmet.git / blobdiff