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 b144116..7fb0160 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,11 +1,14 @@
-{-# 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
 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 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,15 +29,10 @@ 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 GHC.Base
 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))
+import qualified System.IO.Unsafe

 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 getTyConTyVars tc =
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 getTyConTyVars tc =

@@ -44,20 +42,26 @@ getTyConTyVars tc =
        then []
        else TyCon.tyConTyVars 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 :: [(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
-
--- 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
-  errOrFail (OK x)    = x
-  errOrFail (Error s) = Prelude.error s
-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!"
+sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
+
+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!"
+
+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 =

@@ -65,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

@@ -74,7 +80,6 @@ nat2int (S x) = 1 + (nat2int x)
 natToString :: Nat -> Prelude.String
 natToString 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 []      = []
 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
 sanitizeForLatex :: Prelude.String -> Prelude.String
 sanitizeForLatex []      = []
 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)

@@ -82,6 +87,12 @@ sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
 sanitizeForLatex (c:x)   = c:(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 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

@@ -92,20 +103,21 @@ coreKindToKind k =
                  else if (Coercion.isArgTypeKind k)      then KindStar
                  else if (Coercion.isUbxTupleKind k)     then KindStar
                  else if (Coercion.isOpenTypeKind 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.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: "
                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 outputableToString :: Outputable.Outputable a => a -> Prelude.String
                  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: "
                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 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)
+outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))

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

@@ -122,30 +134,34 @@ coreViewDeep t =
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
 
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
 

--- FIXME: cotycon applications may be oversaturated
-coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
-coreCoercionToWeakCoercion c =
+getSourceAndTargetTypesOfCoercion :: Type.Type -> (Type.Type,Type.Type)
+getSourceAndTargetTypesOfCoercion c = Coercion.coercionKind (Coercion.typeKind c)
+
+{-
+-- REMEMBER: cotycon applications may be oversaturated

  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
  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.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (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)
         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.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.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)"
+              (TyCon.CoAxiom _ _ _ , _   ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+              ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))

               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
               _ -> 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)
 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)

@@ -162,4 +178,29 @@ weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 | WCoUnsafe  t1 t2                   => (t1,t2)
 | 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)
+
+
+{-  -- 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)