-{-# 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
import qualified Data.Ord
import qualified Data.Typeable
import Data.Bits ((.&.), shiftL, (.|.))
-import Prelude ( (++), (+), (==), Show, show, Char, (.) )
+import Prelude ( (++), (+), (==), Show, show, Char, (.), ($) )
import qualified Prelude
+import qualified Debug.Trace
import qualified GHC.Base
-
--- used for extracting strings
-bin2ascii =
- (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
- let f b i = if b then 1 `shiftL` i else 0
- in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
+import qualified System.IO
+import qualified System.IO.Unsafe
getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
getTyConTyVars tc =
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
coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
where
natToString :: Nat -> Prelude.String
natToString n = show (nat2int n)
--- only needs to sanitize characters which might appear in Haskell identifiers
sanitizeForLatex :: Prelude.String -> Prelude.String
sanitizeForLatex [] = []
sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
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
+--
+-- The "subkinding" in GHC is not dealt with in System FC, and dealing
+-- with it is not actually as simple as you'd think.
+--
-- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
-- else if (Coercion.isOpenTypeKind k) then KindOpenType
-- else if (Coercion.isArgTypeKind k) then KindArgType
-- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
+--
else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
outputableToString :: Outputable.Outputable a => a -> Prelude.String
outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
--- I'm leaving this here (commented out) in case I ever need it again)
---checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
---checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
-
coreViewDeep :: Type.Type -> Type.Type
coreViewDeep t =
case t of
(TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
(TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
(TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1"
--- (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+ (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
_ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
_ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
-- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
| WCoLeft c => Prelude_error "FIXME WCoLeft"
| WCoRight c => Prelude_error "FIXME WCoRight"
| WCoUnsafe t1 t2 => (t1,t2)
--}
\ No newline at end of file
+-}
+
+
+--trace = Debug.Trace.trace
+--trace msg x = x
+trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
+{-
+trace s x = x
+trace msg x = System.IO.Unsafe.unsafePerformIO $
+ (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
+trace msg x = System.IO.Unsafe.unsafePerformIO $
+ (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
+-}
+
+{- -- used for extracting strings WITHOUT the patch for Coq
+bin2ascii =
+ (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
+ let f b i = if b then 1 `shiftL` i else 0
+ in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
+-}
+
+-- I'm leaving this here (commented out) in case I ever need it again)
+--checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
+--checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
projects / coq-hetmet.git / blobdiff