Require Import General.
Require Import HaskKinds.
Require Import HaskCoreLiterals.
-Require Import HaskCoreTypes. (* FIXME *)
-Require Import HaskCoreVars. (* FIXME *)
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
Require Import HaskWeakTypes.
-Require Import HaskWeakVars. (* FIXME *)
-Require Import HaskCoreToWeak. (* FIXME *)
+Require Import HaskWeakVars.
+Require Import HaskCoreToWeak.
Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
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).
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 κ₂) :
; 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)) Δ
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 :=