-{-# OPTIONS_GHC -fno-warn-unused-binds #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
where
+import qualified Unique
+import qualified Kind
+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 Coercion
import qualified Var
import qualified Id
+import qualified Pair
import qualified FastString
import qualified BasicTypes
import qualified DataCon
import qualified Data.Ord
import qualified Data.Typeable
import Data.Bits ((.&.), shiftL, (.|.))
-import Prelude ( (++), (+), (==), Show, show, Char, (.) )
+import Prelude ( (++), (+), (==), Show, show, (.), ($) )
import qualified Prelude
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))
---bin2ascii' =
--- (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
---shiftAscii =
--- \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)
-
--- crude way of casting Coq "error monad" into Haskell exceptions
-errOrFail :: OrError a -> a
-errOrFail (OK x) = x
-errOrFail (Error s) = Prelude.error s
+import qualified System.IO.Unsafe
getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
-getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
+getTyConTyVars tc =
+ if TyCon.isFunTyCon tc
+ then []
+ else if TyCon.isPrimTyCon 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))))
-coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
-coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
- (Prelude.error "FIXME") (Prelude.error "FIXME"))
-coreVarToWeakVar _ =
- Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
+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!"
-tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
---FIXME: go back to this
---tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n
-tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n
+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)
-tyFunResultKind :: TyCon.TyCon -> Kind
-tyFunResultKind tc = coreKindToKind (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
nat2int :: Nat -> Prelude.Int
nat2int O = 0
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 [] = []
sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
-sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
-
+sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
+
+kindToCoreKind :: Kind -> TypeRep.Kind
+kindToCoreKind KindStar = Kind.liftedTypeKind
+kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
+kindToCoreKind k = Prelude.error ((Prelude.++)
+ "kindToCoreKind does not know how to handle kind "
+ (kindToString k))
coreKindToKind :: TypeRep.Kind -> Kind
coreKindToKind k =
- case Coercion.splitKindFunTy_maybe k of
- Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
+ case Kind.splitKindFunTy_maybe k of
+ Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
Prelude.Nothing ->
- if (Coercion.isLiftedTypeKind k) then KindType
- 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"
+ if (Kind.isLiftedTypeKind k) then KindStar
+ else if (Kind.isUnliftedTypeKind k) then KindStar
+ else if (Kind.isArgTypeKind k) then KindStar
+ else if (Kind.isUbxTupleKind k) then KindStar
+ else if (Kind.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 (Kind.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
(Outputable.showSDoc (Outputable.ppr k)))
outputableToString :: Outputable.Outputable a => a -> Prelude.String
-outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
-
--- TO DO: I think we can remove this now
-checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
-checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
-
---showType t = outputableToString (Type.expandTypeSynonyms t)
-showType t = outputableToString (coreViewDeep t)
+outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
coreViewDeep :: Type.Type -> Type.Type
coreViewDeep t =
Prelude.Nothing -> TypeRep.PredTy p
Prelude.Just t' -> t'
--- FIXME: cotycon applications may be oversaturated
-coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
-coreCoercionToWeakCoercion c =
- case c of
- TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
- TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
- TypeRep.TyConApp tc t ->
- case TyCon.isCoercionTyCon_maybe tc of
- Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
- Prelude.Just (_, ctcd) ->
- case (ctcd,t) of
- (TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
- (TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x)
- (TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
- (TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
--- FIXME (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
- (TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
- (TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
- (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)"
- _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
- _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
--- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
--- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
--- CoreSyn.Type t -> WCoType (coreTypeToWeakType t)
-
-{-
-weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
-| 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"
-| 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"
-| WCoUnsafe t1 t2 => (t1,t2)
--}
\ No newline at end of file
+{-# NOINLINE trace #-}
+trace :: Prelude.String -> a -> a
+trace msg x = x
+
+--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)
+
+-- 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