projects / coq-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
get rid of vec_{fst,snd} axioms
[coq-hetmet.git] / src / Extraction-prefix.hs
diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index d0b6ffa..3179cdb 100644 (file)
--- 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
 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
@@ -22,36 +24,46 @@ import qualified CoreSyn
 import qualified CoreUtils
 import qualified Class
 import qualified Data.Char 
 import qualified CoreUtils
 import qualified Class
 import qualified Data.Char 
+import qualified Data.List
+import qualified Data.Ord
 import qualified Data.Typeable
 import Data.Bits ((.&.), shiftL, (.|.))
 import qualified Data.Typeable
 import Data.Bits ((.&.), shiftL, (.|.))
-import Prelude ( (++), (+), (==), Show, show, Char, (.) )
+import Prelude ( (++), (+), (==), Show, show, Char, (.), ($) )
 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
 
 
--- 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))
 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
+-}
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 
 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,a,b)] -> [(CoreSyn.AltCon,a,b)]
-sortAlts x = x -- FIXME
+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
 
 -- 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))))
 
 -- 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 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"))
@@ -59,12 +71,12 @@ coreVarToWeakVar _                 =
    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
 
 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
    Prelude.error "Var.Var that is neither an expression variable, 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
-
-tyFunResultKind :: TyCon.TyCon -> Kind
-tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc)
+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 Prelude.Left n
 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0
@@ -75,22 +87,31 @@ natToString n = show (nat2int n)
 
 -- only needs to sanitize characters which might appear in Haskell identifiers
 sanitizeForLatex :: Prelude.String -> Prelude.String
 
 -- 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 ('_':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          = 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
 
 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 -> 
       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
+                      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
+--                 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: "
                  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: "
@@ -98,12 +119,9 @@ coreKindToKind k =
 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 
 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)
+-- 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)
 
 coreViewDeep :: Type.Type -> Type.Type
 coreViewDeep t =
 
 coreViewDeep :: Type.Type -> Type.Type
 coreViewDeep t =
@@ -160,4 +178,16 @@ 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
+-}
+
+
+--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)
+-}
Coq proofs and code accompanying the HetMet extensions for GHC