errOrFail (OK x) = x
errOrFail (Error s) = Prelude.error s
+rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
+rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
+ ,
+ coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
+ where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
+
tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
tyConOrTyFun n =
if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
then Prelude.Right n
else if TyCon.isFamInstTyCon n
then Prelude.Right n
- else Prelude.Left n
+ else if TyCon.isSynTyCon n
+ then Prelude.Right n
+ else Prelude.Left n
nat2int :: Nat -> Prelude.Int
nat2int O = 0
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
+Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
+ split_list lwt (length (fst (tyFunKind tf))) >>=
+ fun argsrest =>
+ let (args,rest) := argsrest in
+ OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
+
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
match ct with
| TyVarTy cv => match coreVarToWeakVar cv with
| a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
end) lct)
in match tyConOrTyFun tc_ with
- | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
+ | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
| inl tc => if eqd_dec tc ModalBoxTyCon
then match lct with
| ((TyVarTy ec)::tbody::nil) =>
end
| tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
- | nil => Error "WTyFunApp applied to too many types"
+ | nil => Error ("WTyFunApp applied to too many types"(* +++ eol +++
+ " tyCon= " +++ toString tc +++ eol +++
+ " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++
+ " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
+ " types= " +++ toString lt +++ eol*))
| k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
let case_weakTypeListToTypeList := tt in _
end
try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
apply (Error ("Kind mismatch in WAppTy: "+++err)).
-
+
destruct case_weakTypeListToTypeList.
apply (addErrorMessage "case_weakTypeListToTypeList").
destruct t' as [ k' t' ].
Opaque tyConTyVars.
Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
-Variable rawTyFunKind : CoreTyCon -> Kind. Extract Inlined Constant rawTyFunKind => "(coreKindToKind . TyCon.tyConKind)".
+Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".
Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
- splitKind (rawTyFunKind tc).
+ rawTyFunKind tc.
Instance WeakVarToString : ToString WeakVar :=
{ toString := fun x => toString (weakVarToCoreVar x) }.