From 38e0c88fa03d930293f980681fa34a667402a20d Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 13 May 2011 20:31:50 -0700 Subject: [PATCH] improve detection of type function kinds, mainly their saturation needs --- src/Extraction-prefix.hs | 10 +++++++++- src/HaskCoreToWeak.v | 8 +++++++- src/HaskWeakToStrong.v | 8 ++++++-- src/HaskWeakVars.v | 4 ++-- 4 files changed, 24 insertions(+), 6 deletions(-) diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 0775229..f11e63b 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -64,13 +64,21 @@ errOrFail :: OrError t -> t 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 diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 78223cf..ccd4973 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -29,6 +29,12 @@ Variable hetmet_brak_name : CoreName. Extract Inlined Constant he 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 @@ -45,7 +51,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | 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) => diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index d77d074..7dd93ad 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -142,7 +142,11 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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 @@ -166,7 +170,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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' ]. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 896aff4..3fb7a4b 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -49,10 +49,10 @@ Definition tyConTyVars (tc:CoreTyCon) := 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) }. -- 1.7.10.4