better error reporting in coreTypeToWeakType; dont use Prelude_error

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

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index fbe22cb..7fb0160 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}

 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 where
 import qualified Unique
 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 where
 import qualified Unique

@@ -28,11 +29,9 @@ import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Typeable
 import Data.Bits ((.&.), shiftL, (.|.))
 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 Prelude

-import qualified Debug.Trace

 import qualified GHC.Base
 import qualified GHC.Base

-import qualified System.IO

 import qualified System.IO.Unsafe
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 import qualified System.IO.Unsafe
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]

@@ -51,16 +50,18 @@ 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
 
 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 -> 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 | Var.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coercionKind (Var.varType v)))
+                                                  (Prelude.snd (Coercion.coercionKind (Var.varType v)))
+coreVarToWeakVar _                 = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"

 
 

-errOrFail (OK x)    = x
-errOrFail (Error s) = Prelude.error s
+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 =
 
 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
 tyConOrTyFun n =

@@ -68,7 +69,9 @@ tyConOrTyFun n =
    then Prelude.Right n
    else if TyCon.isFamInstTyCon n
         then Prelude.Right n
    then Prelude.Right n
    else if TyCon.isFamInstTyCon n
         then Prelude.Right n

-        else Prelude.Left n
+        else if TyCon.isSynTyCon n
+             then Prelude.Right n
+             else Prelude.Left n

 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0

@@ -87,8 +90,9 @@ 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 :: 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"
-
+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
 coreKindToKind :: TypeRep.Kind -> Kind
 coreKindToKind k =
   case Coercion.splitKindFunTy_maybe k of

@@ -113,7 +117,7 @@ coreKindToKind k =
                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 outputableToString :: Outputable.Outputable a => a -> Prelude.String
                  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))
+outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))

 
 coreViewDeep :: Type.Type -> Type.Type
 coreViewDeep t =
 
 coreViewDeep :: Type.Type -> Type.Type
 coreViewDeep t =

@@ -130,11 +134,9 @@ coreViewDeep t =
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
 
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
 

-coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
-coreCoercionToWeakCoercion c =
- WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
-   where
-    (t1,t2) = Coercion.coercionKind c
+getSourceAndTargetTypesOfCoercion :: Type.Type -> (Type.Type,Type.Type)
+getSourceAndTargetTypesOfCoercion c = Coercion.coercionKind (Coercion.typeKind c)
+

 {-
 -- REMEMBER: cotycon applications may be oversaturated
  case c of
 {-
 -- REMEMBER: cotycon applications may be oversaturated
  case c of

@@ -178,17 +180,19 @@ weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 | WCoUnsafe  t1 t2                   => (t1,t2)
 -}
 
 | WCoUnsafe  t1 t2                   => (t1,t2)
 -}
 

+{-# NOINLINE trace #-}
+trace :: Prelude.String -> a -> a
+trace msg x = x

 
 --trace = Debug.Trace.trace
 --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)
--}
+--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 =
 
 {-  -- used for extracting strings WITHOUT the patch for Coq
 bin2ascii =