X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=d0b6ffae8e3686661f337aad4117c648e2dce21b;hb=273645efdb974dd04042e6c59bbedbe0ad658298;hp=595b8d1ac3adc999283a68d5328c003977998766;hpb=5a0761840d89b82cdacb0bf9215fd41aba847b68;p=coq-hetmet.git diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 595b8d1..d0b6ffa 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -1,18 +1,7 @@ {-# OPTIONS_GHC -fno-warn-unused-binds #-} -module Extraction ( coqCoreToStringPass ) +module CoqPass ( coqPassCoreToString, coqPassCoreToCore ) where ---import HsSyn ---import TcType ---import CoreFVs ---import CoreUtils ---import MkCore ---import Var ---import BasicTypes ---import Bag ---import VarSet ---import SrcLoc ---import Data.List - +import qualified MkCore import qualified TysWiredIn import qualified TysPrim import qualified Outputable @@ -30,20 +19,59 @@ import qualified FastString import qualified BasicTypes import qualified DataCon import qualified CoreSyn +import qualified CoreUtils import qualified Class import qualified Data.Char - +import qualified Data.Typeable import Data.Bits ((.&.), shiftL, (.|.)) -import Prelude ( (++), (+), (==), Show, show, Char ) +import Prelude ( (++), (+), (==), Show, show, Char, (.) ) +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)) +--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 + +sortAlts :: [(CoreSyn.AltCon,a,b)] -> [(CoreSyn.AltCon,a,b)] +sortAlts x = x -- FIXME + +-- 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)))) +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!" -dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc) +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) nat2int :: Nat -> Prelude.Int nat2int O = 0 nat2int (S x) = 1 + (nat2int x) -nat2string :: Nat -> Prelude.String -nat2string 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 @@ -58,7 +86,7 @@ coreKindToKind k = case Coercion.splitKindFunTy_maybe k of Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2) Prelude.Nothing -> - if (Coercion.isLiftedTypeKind k) then KindType + 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 @@ -67,12 +95,69 @@ coreKindToKind k = 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))) -coreVarSort :: Var.Var -> CoreVarSort -coreVarSort v | Id.isId v = CoreExprVar (Var.varType{-AsType-} v) -coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v)) -coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v) -coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" - -outputableToString :: Outputable -> String +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) + +coreViewDeep :: Type.Type -> Type.Type +coreViewDeep t = + case t of + TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv + TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res) + TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg) + TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg) + TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys) + in case Type.coreView t' of + Prelude.Nothing -> t' + Prelude.Just t'' -> t'' + TypeRep.PredTy p -> case Type.coreView t of + Prelude.Nothing -> TypeRep.PredTy p + Prelude.Just t' -> t' + +-- FIXME: cotycon applications may be oversaturated +coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion +coreCoercionToWeakCoercion c = + 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.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.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)" + _ -> 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) + +{- +weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type +| WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2) +| WCoType t => Prelude_error "FIXME WCoType" +| WCoApp c1 c2 => Prelude_error "FIXME WCoApp" +| WCoAppT c t => Prelude_error "FIXME WCoAppT" +| WCoAll k f => Prelude_error "FIXME WCoAll" +| WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2) +| WCoComp c1 c2 => Prelude_error "FIXME WCoComp" +| WCoLeft c => Prelude_error "FIXME WCoLeft" +| WCoRight c => Prelude_error "FIXME WCoRight" +| WCoUnsafe t1 t2 => (t1,t2) +-} \ No newline at end of file