coreKindToKind :: TypeRep.Kind -> Kind
coreKindToKind k =
case Coercion.splitKindFunTy_maybe k of
- Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
+ Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
Prelude.Nothing ->
- if (Coercion.isLiftedTypeKind k) then KindType
- else if (Coercion.isUnliftedTypeKind k) then KindType
- else if (Coercion.isArgTypeKind k) then KindType
- else if (Coercion.isUbxTupleKind k) then KindType
- else if (Coercion.isOpenTypeKind k) then KindType
+ if (Coercion.isLiftedTypeKind k) then KindStar
+ else if (Coercion.isUnliftedTypeKind k) then KindStar
+ else if (Coercion.isArgTypeKind k) then KindStar
+ else if (Coercion.isUbxTupleKind k) then KindStar
+ else if (Coercion.isOpenTypeKind k) then KindStar
-- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
-- else if (Coercion.isOpenTypeKind k) then KindOpenType
-- else if (Coercion.isArgTypeKind k) then KindArgType
Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
:= tv::::ite.
-Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
+Definition coercionToWeakCoercion : forall Γ Δ κ t1 t2 (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2)), WeakCoercion.
+ admit.
+ Defined.
Section strongExprToWeakExpr.
| ENote _ _ _ _ n e => fun ite => WENote n (strongExprToWeakExpr ftv fcv fev e ite)
| ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv fev e ite) (typeToWeakType ftv τ ite)
| ELetRec _ _ _ _ _ vars elrb e => fun ite => WELetRec (exprLetRec2WeakExprLetRec ftv fcv fev elrb ite)(strongExprToWeakExpr ftv fcv fev e ite)
- | ECast Γ Δ ξ t1 t2 γ l e => fun ite => Prelude_error "FIXME: strongExprToWeakExpr.ECast not implemented"
- | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => Prelude_error "FIXME: strongExprToWeakExpr.ECoApp not implemented"
+ | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
+ | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv fev e ite) (coercionToWeakCoercion _ _ _ _ _ γ)
| ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite =>
let (ev,fev') := next _ _ fev (typeToWeakType ftv (unlev (caseType tc atypes @@ l)) ite) in
WECase
(weakTypeToCoreType t3)
end.
-Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
- mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion.
+ admit.
+ Defined.
+ (*mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).*)
Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
match me with
(*| WCoTFApp : ∀ n, TyFunConst n -> vec WeakCoercion n -> WeakCoercion (* S_n γⁿ *)*)
.
-Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
match wc with
| WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2)
-| WCoType t => Prelude_error "FIXME WCoType"
-| WCoApp c1 c2 => Prelude_error "FIXME WCoApp"
-| WCoAppT c t => Prelude_error "FIXME WCoAppT"
-| WCoAll k f => Prelude_error "FIXME WCoAll"
+| WCoType t => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
+| WCoApp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
+| WCoAppT c t => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
+| WCoAll k f => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
| WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
-| WCoComp c1 c2 => Prelude_error "FIXME WCoComp"
-| WCoLeft c => Prelude_error "FIXME WCoLeft"
-| WCoRight c => Prelude_error "FIXME WCoRight"
+| WCoComp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
+| WCoLeft c => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
+| WCoRight c => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
| WCoUnsafe t1 t2 => (t1,t2)
end.