--- to do: this could be moved into Coq
-coreVarToWeakVar :: Var.Var -> WeakVar
-coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
-coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
-coreVarToWeakVar v | Var.isCoVar v = Prelude.error "FIXME coerVarSort not fully implemented"
-coreVarToWeakVar _ =
- Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
+cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
+cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
+cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
+cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
+
+sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
+sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
+
+coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult
+coreVarToWeakVar v | Id.isId v = CVTWVR_EVar (Var.varType v)
+coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v))
+coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v))
+coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"
+
+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 if TyCon.isSynTyCon n
+ then Prelude.Right n
+ else Prelude.Left n