update for new GHC coercion representation

[coq-hetmet.git] / src / Extraction-prefix.hs

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 28ea4f1..09f4b34 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,22 +1,15 @@
-{-# OPTIONS_GHC -fno-warn-unused-binds  #-}
-module Extraction ( coqCoreToStringPass )
+{-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
+module CoqPass ( coqPassCoreToString, coqPassCoreToCore )

 where
 where

---import HsSyn
---import TcType
---import CoreFVs
---import CoreUtils
---import Var
---import BasicTypes
---import Bag
---import VarSet
---import SrcLoc
---import Data.List
-
+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 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 Name
 import qualified Literal
 import qualified Type

@@ -26,53 +19,134 @@ import qualified TyCon
 import qualified Coercion
 import qualified Var
 import qualified Id
 import qualified Coercion
 import qualified Var
 import qualified Id

+import qualified Pair

 import qualified FastString
 import qualified BasicTypes
 import qualified DataCon
 import qualified CoreSyn
 import qualified FastString
 import qualified BasicTypes
 import qualified DataCon
 import qualified CoreSyn

+import qualified CoreUtils

 import qualified Class
 import qualified Data.Char 
 import qualified Class
 import qualified Data.Char 

-
+import qualified Data.List
+import qualified Data.Ord
+import qualified Data.Typeable

 import Data.Bits ((.&.), shiftL, (.|.))
 import Data.Bits ((.&.), shiftL, (.|.))

-import Prelude ( (++), (+), (==), Show, show, Char )
+import Prelude ( (++), (+), (==), Show, show, (.), ($) )
+import qualified Prelude
+import qualified GHC.Base
+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
+
+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

 
 

-dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc)
+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

 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 nat2int (S x) = 1 + (nat2int x)
 
 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 nat2int (S x) = 1 + (nat2int x)
 

-nat2string :: Nat -> Prelude.String
-nat2string n = show (nat2int n)
+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 :: Prelude.String -> Prelude.String

-sanitizeForLatex []    = []
+sanitizeForLatex []      = []

 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
 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 =
 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 -> 
       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)))
                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
                                                                                (Outputable.showSDoc (Outputable.ppr k)))

-coreVarSort :: Var.Var -> CoreVarSort
-coreVarSort v | Id.isId     v = CoreExprVar (Var.varType{-AsType-} v)
-coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v))
-coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v)
-coreVarSort v | otherwise     = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
+outputableToString :: Outputable.Outputable a => a -> Prelude.String
+outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
+
+coreViewDeep :: Type.Type -> Type.Type
+coreViewDeep t =
+    case t of
+      TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
+      TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
+      TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
+      TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
+      TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
+                        in case Type.coreView t' of
+                               Prelude.Nothing     -> t'
+                               Prelude.Just    t'' -> t''
+      TypeRep.PredTy p         -> case Type.coreView t of
+                               Prelude.Nothing     -> TypeRep.PredTy p
+                               Prelude.Just    t'  -> t'
+
+{-# NOINLINE trace #-}
+trace :: Prelude.String -> a -> a
+trace msg x = x

 
 

-outputableToString :: Outputable -> String
-outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr 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)