X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=3179cdbd01bbb4ee8977ccf17ffd8aefcdd8c1fb;hp=5a657bc26ffce107a3a7b7f209b8e09dfe86f6b1;hb=3351499d7cb3d32c8df441426309ec6a1ef2a035;hpb=635ee434c9edbad1bc6c9bf5ba2b91cb8c51be8e

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 5a657bc..3179cdb 100644
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,11 +1,13 @@
-{-# 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
@@ -26,15 +28,19 @@ import qualified Data.List
 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
+import qualified System.IO
+import qualified System.IO.Unsafe
 
--- used for extracting strings
+{-  -- 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))
+-}
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 getTyConTyVars tc =
@@ -44,8 +50,13 @@ 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
@@ -82,16 +93,21 @@ 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
 --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
 --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
 --                 else if (Coercion.isArgTypeKind k)      then KindArgType
@@ -162,4 +178,16 @@ weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 | 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)
+-}