{-# OPTIONS_GHC -fno-warn-unused-binds #-}
module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
where
+import qualified Unique
+import qualified UniqSupply
import qualified MkCore
import qualified TysWiredIn
import qualified TysPrim
import qualified Outputable
import qualified PrelNames
+import qualified OccName
import qualified Name
import qualified Literal
import qualified Type
then []
else TyCon.tyConTyVars tc
+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 (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x
+sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
-- to do: this could be moved into Coq
coreVarToWeakVar :: Var.Var -> WeakVar
sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
+kindToCoreKind :: Kind -> TypeRep.Kind
+kindToCoreKind KindStar = TypeRep.liftedTypeKind
+kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
+kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that"
+
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