Require Import Coq.Lists.List.
Require Import General.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
-Require Import HaskCoreTypes. (* FIXME *)
-Require Import HaskCoreVars. (* FIXME *)
+Require Import HaskLiteralsAndTyCons.
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
Require Import HaskWeakTypes.
-Require Import HaskWeakVars. (* FIXME *)
-Require Import HaskCoreToWeak. (* FIXME *)
+Require Import HaskWeakVars.
+Require Import HaskWeak.
+Require Import HaskCoreToWeak.
Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
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.
Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
@InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
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).
:= 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).
Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
+Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
+ match lht with t@@l => t end.
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 Δ) :=
fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
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
(* 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
; sac_ekinds : vec Kind sac_numExTyVars
; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
-; sac_Γ := fun Γ => app (tyConKind tc) Γ
+; 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)) Δ
}.
Coercion sac_tc : StrongAltCon >-> TyCon.
-Coercion sac_altcon : StrongAltCon >-> AltCon.
+Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
end
| TArrow => "(->)"
| TAll k f => let alpha := "tv"+++n
- in "(forall "+++ alpha +++ "{:}"+++ k +++")"+++
+ in "(forall "+++ alpha +++ ":"+++ k +++")"+++
typeToString' false (S n) (f n)
- | TCode ec t => "<["+++(typeToString' true n ec)+++"]>@"+++(typeToString' false n t)
+ | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
| TyFunApp tfc lt => tfc+++"_"+++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 :=