X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=3179cdbd01bbb4ee8977ccf17ffd8aefcdd8c1fb;hp=d0b6ffae8e3686661f337aad4117c648e2dce21b;hb=3351499d7cb3d32c8df441426309ec6a1ef2a035;hpb=ab2e0681a81695cc2380b007f2a3314005ec1c99 diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index d0b6ffa..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 @@ -22,36 +24,46 @@ import qualified CoreSyn 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 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)) ---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 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)))) + 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")) @@ -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 ---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 @@ -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 -sanitizeForLatex [] = [] +sanitizeForLatex [] = [] 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 - 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 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: " @@ -98,12 +119,9 @@ coreKindToKind k = 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 = @@ -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) --} \ 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) +-}