{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
module Comorphisms.HasCASL2THFP_P where
import Logic.Logic as Logic
import Logic.Comorphism
import Common.ProofTree
import Common.Result
import Common.Id
import Common.AS_Annotation
import Common.Utils (number)
import Common.DocUtils
import HasCASL.Logic_HasCASL
import HasCASL.Sublogic
import HasCASL.Le as HCLe
import HasCASL.As as HCAs
import HasCASL.AsUtils
import HasCASL.Builtin
import THF.As as THFAs
import THF.Logic_THF
import THF.Cons as THFCons
import THF.Sign as THFSign
import THF.Translate
import THF.HasCASL2THF0Buildins
import THF.Utils (typeToUnitaryType, typeToBinaryType,
typeToTopLevelType)
import qualified THF.Sublogic as SL
import Control.Monad
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Char (toLower)
import Data.Maybe
data HasCASL2THFP_P = HasCASL2THFP_P deriving Int -> HasCASL2THFP_P -> ShowS
[HasCASL2THFP_P] -> ShowS
HasCASL2THFP_P -> String
(Int -> HasCASL2THFP_P -> ShowS)
-> (HasCASL2THFP_P -> String)
-> ([HasCASL2THFP_P] -> ShowS)
-> Show HasCASL2THFP_P
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HasCASL2THFP_P] -> ShowS
$cshowList :: [HasCASL2THFP_P] -> ShowS
show :: HasCASL2THFP_P -> String
$cshow :: HasCASL2THFP_P -> String
showsPrec :: Int -> HasCASL2THFP_P -> ShowS
$cshowsPrec :: Int -> HasCASL2THFP_P -> ShowS
Show
instance Language HasCASL2THFP_P
instance Comorphism HasCASL2THFP_P
HasCASL Sublogic
BasicSpec Sentence SymbItems SymbMapItems
Env Morphism Symbol RawSymbol ()
THF SL.THFSl
BasicSpecTHF THFFormula () ()
SignTHF MorphismTHF SymbolTHF () ProofTree where
sourceLogic :: HasCASL2THFP_P -> HasCASL
sourceLogic HasCASL2THFP_P = HasCASL
HasCASL
sourceSublogic :: HasCASL2THFP_P -> Sublogic
sourceSublogic HasCASL2THFP_P = Sublogic
reqSubLogicForTHFP
targetLogic :: HasCASL2THFP_P -> THF
targetLogic HasCASL2THFP_P = THF
THF
mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl
mapSublogic HasCASL2THFP_P _ = THFSl -> Maybe THFSl
forall a. a -> Maybe a
Just THFSl
SL.tHFP_P
map_theory :: HasCASL2THFP_P
-> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula])
map_theory HasCASL2THFP_P = (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula])
transTheory
map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF
map_symbol HasCASL2THFP_P env :: Env
env s :: Symbol
s = String -> Result (Set SymbolTHF) -> Set SymbolTHF
forall a. String -> Result a -> a
propagateErrors "" (Result (Set SymbolTHF) -> Set SymbolTHF)
-> Result (Set SymbolTHF) -> Set SymbolTHF
forall a b. (a -> b) -> a -> b
$
Env -> Symbol -> Result (Set SymbolTHF)
transSymbol Env
env Symbol
s
has_model_expansion :: HasCASL2THFP_P -> Bool
has_model_expansion HasCASL2THFP_P = Bool
True
reqSubLogicForTHFP :: Sublogic
reqSubLogicForTHFP :: Sublogic
reqSubLogicForTHFP = Sublogic :: Bool
-> Bool
-> Bool
-> Bool
-> Classes
-> Bool
-> Bool
-> Bool
-> Formulas
-> Sublogic
Sublogic
{ has_sub :: Bool
has_sub = Bool
False
, has_part :: Bool
has_part = Bool
False
, has_eq :: Bool
has_eq = Bool
True
, has_pred :: Bool
has_pred = Bool
True
, type_classes :: Classes
type_classes = Classes
NoClasses
, has_polymorphism :: Bool
has_polymorphism = Bool
False
, has_type_constructors :: Bool
has_type_constructors = Bool
False
, has_products :: Bool
has_products = Bool
True
, which_logic :: Formulas
which_logic = Formulas
HOL }
transTheory :: (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula])
transTheory :: (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula])
transTheory (env :: Env
env, hcnsl :: [Named Sentence]
hcnsl) = do
(typs :: TypeMap
typs, icm :: Map Id Constant
icm) <- TypeMap -> Result (TypeMap, Map Id Constant)
transTypeMap (TypeMap -> Result (TypeMap, Map Id Constant))
-> TypeMap -> Result (TypeMap, Map Id Constant)
forall a b. (a -> b) -> a -> b
$ Env -> TypeMap
HCLe.typeMap Env
env
ConstMap
cons <- Assumps -> Map Id Constant -> Result ConstMap
transAssumps (Env -> Assumps
HCLe.assumps Env
env) Map Id Constant
icm
(nsl :: [Named THFFormula]
nsl, ids :: IdSet
ids) <- (([Named THFFormula], IdSet)
-> Named Sentence -> Result ([Named THFFormula], IdSet))
-> ([Named THFFormula], IdSet)
-> [Named Sentence]
-> Result ([Named THFFormula], IdSet)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Map Id Constant
-> ([Named THFFormula], IdSet)
-> Named Sentence
-> Result ([Named THFFormula], IdSet)
fNSen Map Id Constant
icm) ([], IdSet
forall a. Set a
Set.empty) [Named Sentence]
hcnsl
let ax :: [Named THFFormula]
ax = IdSet -> [Named THFFormula]
preDefAxioms IdSet
ids [Named THFFormula] -> [Named THFFormula] -> [Named THFFormula]
forall a. [a] -> [a] -> [a]
++ [Named THFFormula] -> [Named THFFormula]
forall a. [a] -> [a]
reverse [Named THFFormula]
nsl
aCons :: ConstMap
aCons = ConstMap -> ConstMap -> ConstMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ConstMap
cons (IdSet -> ConstMap
preDefHCAssumps IdSet
ids)
SymbolMap
syms <- TypeMap -> ConstMap -> Result SymbolMap
mkSymbolMap TypeMap
typs ConstMap
aCons
let sig :: SignTHF
sig = SignTHF
THFSign.emptySign { types :: TypeMap
types = TypeMap
typs
, consts :: ConstMap
consts = ConstMap
aCons
, symbols :: SymbolMap
symbols = SymbolMap
syms }
(SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
forall (m :: * -> *) a. Monad m => a -> m a
return (SignTHF
sig , [Named THFFormula]
ax)
where
fNSen :: IdConstantMap -> ([Named THFFormula], IdSet)
-> Named Sentence -> Result ([Named THFFormula], IdSet)
fNSen :: Map Id Constant
-> ([Named THFFormula], IdSet)
-> Named Sentence
-> Result ([Named THFFormula], IdSet)
fNSen icm :: Map Id Constant
icm p :: ([Named THFFormula], IdSet)
p@(nsl :: [Named THFFormula]
nsl, ids :: IdSet
ids) hcns :: Named Sentence
hcns = case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
hcns of
Formula _ -> do
(ns :: Named THFFormula
ns, nids :: IdSet
nids) <- Maybe (Map Id Constant)
-> IdSet
-> Env
-> Named Sentence
-> Result (Named THFFormula, IdSet)
transNamedSentence (Map Id Constant -> Maybe (Map Id Constant)
forall a. a -> Maybe a
Just Map Id Constant
icm) IdSet
ids Env
env Named Sentence
hcns
([Named THFFormula], IdSet) -> Result ([Named THFFormula], IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named THFFormula
ns Named THFFormula -> [Named THFFormula] -> [Named THFFormula]
forall a. a -> [a] -> [a]
: [Named THFFormula]
nsl, IdSet
nids)
s :: Sentence
s -> do
[Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Sentence -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "ignoring" Sentence
s]
([Named THFFormula], IdSet) -> Result ([Named THFFormula], IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named THFFormula], IdSet)
p
transTypeMap :: HCLe.TypeMap -> Result (THFSign.TypeMap, Map.Map Id Constant)
transTypeMap :: TypeMap -> Result (TypeMap, Map Id Constant)
transTypeMap tm :: TypeMap
tm = ((TypeMap, Map Id Constant)
-> (Id, TypeInfo) -> Result (TypeMap, Map Id Constant))
-> (TypeMap, Map Id Constant)
-> [(Id, TypeInfo)]
-> Result (TypeMap, Map Id Constant)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (TypeMap, Map Id Constant)
-> (Id, TypeInfo) -> Result (TypeMap, Map Id Constant)
trans (TypeMap
forall k a. Map k a
Map.empty, Map Id Constant
forall k a. Map k a
Map.empty) (TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList TypeMap
tm)
where
trans :: (THFSign.TypeMap, Map.Map Id Constant) -> (Id, HCLe.TypeInfo)
-> Result (THFSign.TypeMap, Map.Map Id Constant)
trans :: (TypeMap, Map Id Constant)
-> (Id, TypeInfo) -> Result (TypeMap, Map Id Constant)
trans (ttm :: TypeMap
ttm, icm :: Map Id Constant
icm) (i :: Id
i, ti :: TypeInfo
ti) = do
Constant
c <- Id -> Result Constant
transTypeId Id
i
TypeInfo
ti' <- TypeInfo -> Constant -> Result TypeInfo
transTypeInfo TypeInfo
ti Constant
c
(TypeMap, Map Id Constant) -> Result (TypeMap, Map Id Constant)
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c TypeInfo
ti' TypeMap
ttm, Id -> Constant -> Map Id Constant -> Map Id Constant
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Constant
c Map Id Constant
icm)
transTypeInfo :: HCLe.TypeInfo -> THFAs.Constant -> Result THFSign.TypeInfo
transTypeInfo :: TypeInfo -> Constant -> Result TypeInfo
transTypeInfo ti :: TypeInfo
ti c :: Constant
c = RawKind -> Result Kind
transRawKind (TypeInfo -> RawKind
HCLe.typeKind TypeInfo
ti)
Result Kind -> (Kind -> Result TypeInfo) -> Result TypeInfo
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ tk :: Kind
tk -> TypeInfo -> Result TypeInfo
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo :: Constant -> Name -> Kind -> Annotations -> TypeInfo
THFSign.TypeInfo
{ typeId :: Constant
THFSign.typeId = Constant
c
, typeName :: Name
THFSign.typeName = Constant -> Name
mkTypesName Constant
c
, typeKind :: Kind
THFSign.typeKind = Kind
tk
, typeAnno :: Annotations
THFSign.typeAnno = Annotations
THFAs.Null }
transRawKind :: HCAs.RawKind -> Result THFCons.Kind
transRawKind :: RawKind -> Result Kind
transRawKind rk :: RawKind
rk = case RawKind
rk of
ClassKind () -> Kind -> Result Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
Kind
_ -> String -> Range -> Result Kind
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Type constructors are not supported!" Range
nullRange
transAssumps :: HCLe.Assumps -> Map.Map Id Constant -> Result THFSign.ConstMap
transAssumps :: Assumps -> Map Id Constant -> Result ConstMap
transAssumps am :: Assumps
am icm :: Map Id Constant
icm = (ConstMap -> (Id, Set OpInfo) -> Result ConstMap)
-> ConstMap -> [(Id, Set OpInfo)] -> Result ConstMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ConstMap -> (Id, Set OpInfo) -> Result ConstMap
insertConsts ConstMap
forall k a. Map k a
Map.empty (Assumps -> [(Id, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList Assumps
am)
where
insertConsts :: THFSign.ConstMap -> (Id, Set.Set OpInfo)
-> Result THFSign.ConstMap
insertConsts :: ConstMap -> (Id, Set OpInfo) -> Result ConstMap
insertConsts m :: ConstMap
m (name :: Id
name, ops :: Set OpInfo
ops) = case Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ops of
[OpInfo ts :: TypeScheme
ts _ _] -> do
Type
ty <- TypeScheme -> Result Type
transOp TypeScheme
ts
Constant
c <- Id -> Result Constant
transAssumpId Id
name
let ci :: ConstInfo
ci = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
THFSign.ConstInfo
{ constId :: Constant
THFSign.constId = Constant
c
, constName :: Name
THFSign.constName = Constant -> Name
mkConstsName Constant
c
, constType :: Type
THFSign.constType = Type
ty
, constAnno :: Annotations
THFSign.constAnno = Annotations
THFAs.Null }
ConstMap -> Result ConstMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstMap -> Result ConstMap) -> ConstMap -> Result ConstMap
forall a b. (a -> b) -> a -> b
$ Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c ConstInfo
ci ConstMap
m
infos :: [OpInfo]
infos -> (ConstMap -> (OpInfo, Int) -> Result ConstMap)
-> ConstMap -> [(OpInfo, Int)] -> Result ConstMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ m' :: ConstMap
m' (OpInfo ts :: TypeScheme
ts _ _, i :: Int
i) -> do
Type
ty <- TypeScheme -> Result Type
transOp TypeScheme
ts
Constant
c <- Id -> Int -> Result Constant
transAssumpsId Id
name Int
i
let ci :: ConstInfo
ci = ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
THFSign.ConstInfo
{ constId :: Constant
THFSign.constId = Constant
c
, constName :: Name
THFSign.constName = Constant -> Name
mkConstsName Constant
c
, constType :: Type
THFSign.constType = Type
ty
, constAnno :: Annotations
THFSign.constAnno = Annotations
THFAs.Null }
ConstMap -> Result ConstMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstMap -> Result ConstMap) -> ConstMap -> Result ConstMap
forall a b. (a -> b) -> a -> b
$ Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c ConstInfo
ci ConstMap
m'
) ConstMap
m ([OpInfo] -> [(OpInfo, Int)]
forall a. [a] -> [(a, Int)]
number [OpInfo]
infos)
transOp :: TypeScheme -> Result THFCons.Type
transOp :: TypeScheme -> Result Type
transOp (TypeScheme _ op :: Type
op _) = Map Id Constant -> Type -> Result Type
transType Map Id Constant
icm Type
op
type IdConstantMap = Map.Map Id THFAs.Constant
genIdConstantMap :: Env -> Result IdConstantMap
genIdConstantMap :: Env -> Result (Map Id Constant)
genIdConstantMap e :: Env
e = (Map Id Constant -> (Id, TypeInfo) -> Result (Map Id Constant))
-> Map Id Constant -> [(Id, TypeInfo)] -> Result (Map Id Constant)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ icm :: Map Id Constant
icm (i :: Id
i, _) -> do
Constant
c <- Id -> Result Constant
transTypeId Id
i
Map Id Constant -> Result (Map Id Constant)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Id Constant -> Result (Map Id Constant))
-> Map Id Constant -> Result (Map Id Constant)
forall a b. (a -> b) -> a -> b
$ Id -> Constant -> Map Id Constant -> Map Id Constant
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Constant
c Map Id Constant
icm)
Map Id Constant
forall k a. Map k a
Map.empty (TypeMap -> [(Id, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList (Env -> TypeMap
HCLe.typeMap Env
e))
transType :: IdConstantMap -> HCAs.Type -> Result THFCons.Type
transType :: Map Id Constant -> Type -> Result Type
transType icm :: Map Id Constant
icm hct :: Type
hct = case Type -> (Type, [Type])
getTypeAppl Type
hct of
(TypeName tid :: Id
tid _ n :: Int
n, tys :: [Type]
tys)
| [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys Bool -> Bool -> Bool
&& Id
tid Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
unitTypeId -> Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
OType
| Id -> Bool
isProductId Id
tid -> ([Type] -> Type) -> Result [Type] -> Result Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Type] -> Type
ProdType (Result [Type] -> Result Type) -> Result [Type] -> Result Type
forall a b. (a -> b) -> a -> b
$
(Type -> Result Type) -> [Type] -> Result [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Id Constant -> Type -> Result Type
transType Map Id Constant
icm) [Type]
tys
| [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length [Type]
tys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
&& Id
tid Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
if Type -> Bool
isUnitType (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
forall a. [a] -> a
head [Type]
tys
then Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
OType
else String -> Range -> Result Type
forall a. String -> Range -> Result a
fatal_error "THF0 does not support partiality." Range
nullRange
| [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length [Type]
tys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 -> if Id -> Bool
isArrow Id
tid then do
[ts1 :: Type
ts1, ts2 :: Type
ts2] <- (Type -> Result Type) -> [Type] -> Result [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Id Constant -> Type -> Result Type
transType Map Id Constant
icm) [Type]
tys
case Type
ts1 of
THFCons.MapType _ _ ->
Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type) -> Type -> Result Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
THFCons.MapType (Type -> Type
THFCons.ParType Type
ts1) Type
ts2
_ -> Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
THFCons.MapType Type
ts1 Type
ts2)
else String -> Range -> Result Type
forall a. String -> Range -> Result a
fatal_error ("Application of Types in Constants is not " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"possible in THF0: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
tid) (Id -> Range
forall a. GetRange a => a -> Range
getRange Id
tid)
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys ->
Result Type
-> (Constant -> Result Type) -> Maybe Constant -> Result Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Range -> Result Type
forall a. String -> Range -> Result a
fatal_error ("unknown Type" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
tid) Range
nullRange)
(Type -> Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Result Type)
-> (Constant -> Type) -> Constant -> Result Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Type
THFCons.CType) (Id -> Map Id Constant -> Maybe Constant
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
tid Map Id Constant
icm)
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys -> (Token -> Type) -> Result Token -> Result Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> Type
THFCons.VType (Id -> Result Token
transVarId Id
tid)
t :: (Type, [Type])
t -> String -> Range -> Result Type
forall a. String -> Range -> Result a
fatal_error ("transType: Not a translatable type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Type, [Type]) -> String
forall a. Show a => a -> String
show (Type, [Type])
t)
(Type -> Range
forall a. GetRange a => a -> Range
getRange Type
hct)
isUnitType :: HCAs.Type -> Bool
isUnitType :: Type -> Bool
isUnitType t :: Type
t = case Type
t of
TypeName i :: Id
i _ _ -> Id -> Id -> Bool
myEqId Id
i Id
unitTypeId
_ -> Bool
False
insLast :: THFCons.Type -> THFCons.Type -> THFCons.Type
insLast :: Type -> Type -> Type
insLast it :: Type
it t :: Type
t = case Type
t of
MapType t1 :: Type
t1 t2 :: Type
t2 -> Type -> Type -> Type
MapType Type
t1 (Type -> Type -> Type
insLast Type
it Type
t2)
t1 :: Type
t1 -> Type -> Type -> Type
MapType Type
t1 Type
it
mkSymbolMap :: THFSign.TypeMap -> THFSign.ConstMap -> Result THFSign.SymbolMap
mkSymbolMap :: TypeMap -> ConstMap -> Result SymbolMap
mkSymbolMap tm :: TypeMap
tm cm :: ConstMap
cm = (SymbolMap -> (Constant, ConstInfo) -> Result SymbolMap)
-> SymbolMap -> [(Constant, ConstInfo)] -> Result SymbolMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SymbolMap -> (Constant, ConstInfo) -> Result SymbolMap
ins ((TypeInfo -> SymbolTHF) -> TypeMap -> SymbolMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map TypeInfo -> SymbolTHF
typeInfoToSymbol TypeMap
tm) (ConstMap -> [(Constant, ConstInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList ConstMap
cm)
where
ins :: THFSign.SymbolMap -> (THFAs.Constant, THFSign.ConstInfo)
-> Result THFSign.SymbolMap
ins :: SymbolMap -> (Constant, ConstInfo) -> Result SymbolMap
ins sm :: SymbolMap
sm (c :: Constant
c, ci :: ConstInfo
ci) = if Constant -> SymbolMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Constant
c SymbolMap
sm then
String -> Range -> Result SymbolMap
forall a. String -> Range -> Result a
fatal_error ("Two symbols with the same name detected: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Doc -> String
forall a. Show a => a -> String
show (Constant -> Doc
forall a. Pretty a => a -> Doc
pretty Constant
c)) Range
nullRange
else SymbolMap -> Result SymbolMap
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbolMap -> Result SymbolMap) -> SymbolMap -> Result SymbolMap
forall a b. (a -> b) -> a -> b
$ Constant -> SymbolTHF -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c (ConstInfo -> SymbolTHF
constInfoToSymbol ConstInfo
ci) SymbolMap
sm
typeInfoToSymbol :: THFSign.TypeInfo -> THFCons.SymbolTHF
typeInfoToSymbol :: TypeInfo -> SymbolTHF
typeInfoToSymbol ti :: TypeInfo
ti = Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
THFCons.Symbol
{ symId :: Constant
THFCons.symId = TypeInfo -> Constant
THFSign.typeId TypeInfo
ti
, symName :: Name
THFCons.symName = TypeInfo -> Name
THFSign.typeName TypeInfo
ti
, symType :: SymbolType
THFCons.symType = Kind -> SymbolType
THFCons.ST_Type (Kind -> SymbolType) -> Kind -> SymbolType
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Kind
THFSign.typeKind TypeInfo
ti }
constInfoToSymbol :: THFSign.ConstInfo -> THFCons.SymbolTHF
constInfoToSymbol :: ConstInfo -> SymbolTHF
constInfoToSymbol ci :: ConstInfo
ci = Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
THFCons.Symbol
{ symId :: Constant
THFCons.symId = ConstInfo -> Constant
THFSign.constId ConstInfo
ci
, symName :: Name
THFCons.symName = ConstInfo -> Name
THFSign.constName ConstInfo
ci
, symType :: SymbolType
THFCons.symType = Type -> SymbolType
THFCons.ST_Const (Type -> SymbolType) -> Type -> SymbolType
forall a b. (a -> b) -> a -> b
$ ConstInfo -> Type
THFSign.constType ConstInfo
ci }
transSymbol :: Env -> Symbol -> Result (Set.Set SymbolTHF)
transSymbol :: Env -> Symbol -> Result (Set SymbolTHF)
transSymbol sig1 :: Env
sig1 sym1 :: Symbol
sym1 = case Symbol -> SymbolType
HCLe.symType Symbol
sym1 of
TypeAsItemType rk :: RawKind
rk ->
case Result Constant -> Maybe Constant
forall a. Result a -> Maybe a
maybeResult (Id -> Result Constant
transTypeId (Id -> Result Constant) -> Id -> Result Constant
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
HCLe.symName Symbol
sym1) of
Nothing -> Set SymbolTHF -> Result (Set SymbolTHF)
forall (m :: * -> *) a. Monad m => a -> m a
return Set SymbolTHF
forall a. Set a
Set.empty
Just c :: Constant
c -> do
Kind
rk' <- RawKind -> Result Kind
transRawKind RawKind
rk
Set SymbolTHF -> Result (Set SymbolTHF)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set SymbolTHF -> Result (Set SymbolTHF))
-> Set SymbolTHF -> Result (Set SymbolTHF)
forall a b. (a -> b) -> a -> b
$ SymbolTHF -> Set SymbolTHF
forall a. a -> Set a
Set.singleton Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
THFCons.Symbol
{ symId :: Constant
THFCons.symId = Constant
c
, symName :: Name
THFCons.symName = Constant -> Name
mkTypesName Constant
c
, symType :: SymbolType
THFCons.symType = Kind -> SymbolType
ST_Type Kind
rk' }
OpAsItemType ts :: TypeScheme
ts -> Set SymbolTHF -> Result (Set SymbolTHF)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set SymbolTHF -> Result (Set SymbolTHF))
-> Set SymbolTHF -> Result (Set SymbolTHF)
forall a b. (a -> b) -> a -> b
$ TypeScheme
-> (Map Id Constant -> TypeScheme -> Result Type) -> Set SymbolTHF
tsHelper TypeScheme
ts Map Id Constant -> TypeScheme -> Result Type
tsOpType
PredAsItemType ts :: TypeScheme
ts -> Set SymbolTHF -> Result (Set SymbolTHF)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set SymbolTHF -> Result (Set SymbolTHF))
-> Set SymbolTHF -> Result (Set SymbolTHF)
forall a b. (a -> b) -> a -> b
$ TypeScheme
-> (Map Id Constant -> TypeScheme -> Result Type) -> Set SymbolTHF
tsHelper TypeScheme
ts Map Id Constant -> TypeScheme -> Result Type
tsPredType
_ -> Set SymbolTHF -> Result (Set SymbolTHF)
forall (m :: * -> *) a. Monad m => a -> m a
return Set SymbolTHF
forall a. Set a
Set.empty
where
tsOpType :: IdConstantMap -> TypeScheme -> Result THFCons.Type
tsOpType :: Map Id Constant -> TypeScheme -> Result Type
tsOpType icm :: Map Id Constant
icm (TypeScheme _ t :: Type
t _) = Map Id Constant -> Type -> Result Type
transType Map Id Constant
icm Type
t
tsPredType :: IdConstantMap -> TypeScheme -> Result THFCons.Type
tsPredType :: Map Id Constant -> TypeScheme -> Result Type
tsPredType icm :: Map Id Constant
icm (TypeScheme _ t :: Type
t _) = (Type -> Type) -> Result Type -> Result Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> Type -> Type
insLast Type
OType)
(Map Id Constant -> Type -> Result Type
transType Map Id Constant
icm Type
t)
tsHelper :: TypeScheme -> (IdConstantMap -> TypeScheme
-> Result THFCons.Type) -> Set.Set SymbolTHF
tsHelper :: TypeScheme
-> (Map Id Constant -> TypeScheme -> Result Type) -> Set SymbolTHF
tsHelper ts :: TypeScheme
ts f :: Map Id Constant -> TypeScheme -> Result Type
f = case Id -> Assumps -> Maybe (Set OpInfo)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Symbol -> Id
HCLe.symName Symbol
sym1) (Env -> Assumps
assumps Env
sig1) of
Just a :: Set OpInfo
a
| Set OpInfo -> Int
forall a. Set a -> Int
Set.size Set OpInfo
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 -> Set SymbolTHF
forall a. Set a
Set.empty
| Set OpInfo -> Int
forall a. Set a -> Int
Set.size Set OpInfo
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 -> TypeScheme
-> Result Constant
-> (Map Id Constant -> TypeScheme -> Result Type)
-> Set SymbolTHF
tsHelper2 TypeScheme
ts
(Id -> Result Constant
transAssumpId (Id -> Result Constant) -> Id -> Result Constant
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
HCLe.symName Symbol
sym1) Map Id Constant -> TypeScheme -> Result Type
f
| Set OpInfo -> Int
forall a. Set a -> Int
Set.size Set OpInfo
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 -> case TypeScheme -> [(TypeScheme, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup TypeScheme
ts ([TypeScheme] -> [(TypeScheme, Int)]
forall a. [a] -> [(a, Int)]
number
((OpInfo -> TypeScheme) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> TypeScheme
HCLe.opType (Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
a))) of
Nothing -> Set SymbolTHF
forall a. Set a
Set.empty
Just num :: Int
num -> TypeScheme
-> Result Constant
-> (Map Id Constant -> TypeScheme -> Result Type)
-> Set SymbolTHF
tsHelper2 TypeScheme
ts
(Id -> Int -> Result Constant
transAssumpsId (Symbol -> Id
HCLe.symName Symbol
sym1) Int
num) Map Id Constant -> TypeScheme -> Result Type
f
_ -> TypeScheme
-> Result Constant
-> (Map Id Constant -> TypeScheme -> Result Type)
-> Set SymbolTHF
tsHelper2 TypeScheme
ts (Id -> Result Constant
transAssumpId (Id -> Result Constant) -> Id -> Result Constant
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
HCLe.symName Symbol
sym1) Map Id Constant -> TypeScheme -> Result Type
f
tsHelper2 :: TypeScheme -> Result THFAs.Constant -> (IdConstantMap
-> TypeScheme -> Result THFCons.Type) -> Set.Set SymbolTHF
tsHelper2 :: TypeScheme
-> Result Constant
-> (Map Id Constant -> TypeScheme -> Result Type)
-> Set SymbolTHF
tsHelper2 t :: TypeScheme
t rc :: Result Constant
rc f :: Map Id Constant -> TypeScheme -> Result Type
f = case Result Constant -> Maybe Constant
forall a. Result a -> Maybe a
maybeResult Result Constant
rc of
Nothing -> Set SymbolTHF
forall a. Set a
Set.empty
Just c :: Constant
c -> case Result (Map Id Constant) -> Maybe (Map Id Constant)
forall a. Result a -> Maybe a
maybeResult (Env -> Result (Map Id Constant)
genIdConstantMap Env
sig1) of
Nothing -> Set SymbolTHF
forall a. Set a
Set.empty
Just icm :: Map Id Constant
icm -> case Result Type -> Maybe Type
forall a. Result a -> Maybe a
maybeResult (Map Id Constant -> TypeScheme -> Result Type
f Map Id Constant
icm TypeScheme
t) of
Nothing -> Set SymbolTHF
forall a. Set a
Set.empty
Just tt :: Type
tt -> SymbolTHF -> Set SymbolTHF
forall a. a -> Set a
Set.singleton
Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
THFCons.Symbol { symId :: Constant
THFCons.symId = Constant
c
, symName :: Name
THFCons.symName = Constant -> Name
mkConstsName Constant
c
, symType :: SymbolType
THFCons.symType = Type -> SymbolType
ST_Const Type
tt }
transNamedSentence :: Maybe IdConstantMap -> IdSet -> Env -> Named Sentence
-> Result (Named THFFormula, IdSet)
transNamedSentence :: Maybe (Map Id Constant)
-> IdSet
-> Env
-> Named Sentence
-> Result (Named THFFormula, IdSet)
transNamedSentence micm :: Maybe (Map Id Constant)
micm ids :: IdSet
ids sig :: Env
sig ns' :: Named Sentence
ns' = do
Map Id Constant
icm <- Result (Map Id Constant)
-> (Map Id Constant -> Result (Map Id Constant))
-> Maybe (Map Id Constant)
-> Result (Map Id Constant)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Env -> Result (Map Id Constant)
genIdConstantMap Env
sig) Map Id Constant -> Result (Map Id Constant)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map Id Constant)
micm
let ns :: Named Sentence
ns = ShowS -> Named Sentence -> Named Sentence
forall a b s. (a -> b) -> SenAttr s a -> SenAttr s b
reName (\ n :: String
n -> case String
n of
[] -> String
n
x :: Char
x : xs :: String
xs -> Char -> Char
toLower Char
x Char -> ShowS
forall a. a -> [a] -> [a]
: String
xs) Named Sentence
ns'
case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
ns of
Formula term :: Term
term -> do
(lf :: THFLogicFormula
lf, nids :: IdSet
nids) <- Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
sig Map Id Constant
icm IdSet
ids Term
term
(Named THFFormula, IdSet) -> Result (Named THFFormula, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Named Sentence
ns {sentence :: THFFormula
sentence = THFLogicFormula -> THFFormula
TF_THF_Logic_Formula THFLogicFormula
lf
, senAttr :: String
senAttr = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe (ShowS
forall a. HasCallStack => String -> a
error "THF.transNamedSentence")
(Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
transToTHFString (Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
ns) }
, IdSet
nids)
_ -> String -> Result (Named THFFormula, IdSet)
forall a. HasCallStack => String -> a
error "Data types or program equations are not allowed in THF0."
getFormulaRole :: Named HCLe.Sentence -> FormulaRole
getFormulaRole :: Named Sentence -> FormulaRole
getFormulaRole ns :: Named Sentence
ns =
if Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named Sentence
ns
then if Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
wasTheorem Named Sentence
ns then FormulaRole
Theorem else FormulaRole
Axiom
else FormulaRole
Lemma
transTerm :: Env -> IdConstantMap -> IdSet -> HCAs.Term
-> Result (THFLogicFormula, IdSet)
transTerm :: Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm e :: Env
e icm :: Map Id Constant
icm ids :: IdSet
ids t :: Term
t = case Term
t of
QuantifiedTerm q :: Quantifier
q gcdl :: [GenVarDecl]
gcdl t1 :: Term
t1 r :: Range
r -> (THFQuantifiedFormula -> THFLogicFormula)
-> Result (THFQuantifiedFormula, IdSet)
-> Result (THFLogicFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap (THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (THFUnitaryFormula -> THFLogicFormula)
-> (THFQuantifiedFormula -> THFUnitaryFormula)
-> THFQuantifiedFormula
-> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
THFQuantifiedFormula -> THFUnitaryFormula
TUF_THF_Quantified_Formula) (Env
-> Map Id Constant
-> IdSet
-> Quantifier
-> [GenVarDecl]
-> Term
-> Range
-> Result (THFQuantifiedFormula, IdSet)
transQuantifiedTerm Env
e Map Id Constant
icm IdSet
ids Quantifier
q [GenVarDecl]
gcdl Term
t1 Range
r)
LambdaTerm tl :: [Term]
tl p :: Partiality
p t1 :: Term
t1 r :: Range
r -> Env
-> Map Id Constant
-> IdSet
-> [Term]
-> Partiality
-> Term
-> Range
-> Result (THFLogicFormula, IdSet)
transLamdaTerm Env
e Map Id Constant
icm IdSet
ids [Term]
tl Partiality
p Term
t1 Range
r
TypedTerm t1 :: Term
t1 tq :: TypeQual
tq ty :: Type
ty r :: Range
r -> Term -> TypeQual -> Type -> Range -> Result Term
redTypedTerm Term
t1 TypeQual
tq Type
ty Range
r Result Term
-> (Term -> Result (THFLogicFormula, IdSet))
-> Result (THFLogicFormula, IdSet)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
e Map Id Constant
icm IdSet
ids
ApplTerm t1 :: Term
t1 t2 :: Term
t2 r :: Range
r -> Env
-> Map Id Constant
-> IdSet
-> Term
-> Term
-> Range
-> Result (THFLogicFormula, IdSet)
transApplTerm Env
e Map Id Constant
icm IdSet
ids Term
t1 Term
t2 Range
r
QualVar (VarDecl i :: Id
i _ _ _) -> (Token -> THFLogicFormula)
-> Result Token -> Result THFLogicFormula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (THFUnitaryFormula -> THFLogicFormula)
-> (Token -> THFUnitaryFormula) -> Token -> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFAtom -> THFUnitaryFormula
TUF_THF_Atom
(THFAtom -> THFUnitaryFormula)
-> (Token -> THFAtom) -> Token -> THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> THFAtom
T0A_Variable) (Id -> Result Token
transVarId Id
i) Result THFLogicFormula
-> (THFLogicFormula -> Result (THFLogicFormula, IdSet))
-> Result (THFLogicFormula, IdSet)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ lf :: THFLogicFormula
lf -> (THFLogicFormula, IdSet) -> Result (THFLogicFormula, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFLogicFormula
lf, IdSet
ids))
QualOp ob :: OpBrand
ob pid :: PolyId
pid ts :: TypeScheme
ts tl :: [Type]
tl ik :: InstKind
ik r :: Range
r -> (Constant -> THFLogicFormula)
-> Result (Constant, IdSet) -> Result (THFLogicFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap (THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula
(THFUnitaryFormula -> THFLogicFormula)
-> (Constant -> THFUnitaryFormula) -> Constant -> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFAtom -> THFUnitaryFormula
TUF_THF_Atom (THFAtom -> THFUnitaryFormula)
-> (Constant -> THFAtom) -> Constant -> THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> THFAtom
T0A_Constant) (Env
-> IdSet
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Result (Constant, IdSet)
transQualOp Env
e IdSet
ids OpBrand
ob PolyId
pid TypeScheme
ts [Type]
tl InstKind
ik Range
r)
TupleTerm ts' :: [Term]
ts' _ -> do
(ts :: [THFLogicFormula]
ts, nids :: IdSet
nids) <- (([THFLogicFormula], IdSet)
-> Term -> Result ([THFLogicFormula], IdSet))
-> ([THFLogicFormula], IdSet)
-> [Term]
-> Result ([THFLogicFormula], IdSet)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (ts :: [THFLogicFormula]
ts, ids' :: IdSet
ids') t' :: Term
t' -> do
(t'' :: THFLogicFormula
t'', ids'' :: IdSet
ids'') <- Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
e Map Id Constant
icm IdSet
ids' Term
t'
([THFLogicFormula], IdSet) -> Result ([THFLogicFormula], IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return ([THFLogicFormula]
ts [THFLogicFormula] -> [THFLogicFormula] -> [THFLogicFormula]
forall a. [a] -> [a] -> [a]
++ [THFLogicFormula
t''], IdSet
ids'')) ([], IdSet
ids) [Term]
ts'
(THFLogicFormula, IdSet) -> Result (THFLogicFormula, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (THFUnitaryFormula -> THFLogicFormula)
-> ([THFLogicFormula] -> THFUnitaryFormula)
-> [THFLogicFormula]
-> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFLogicFormula] -> THFUnitaryFormula
TUF_THF_Tuple ([THFLogicFormula] -> THFLogicFormula)
-> [THFLogicFormula] -> THFLogicFormula
forall a b. (a -> b) -> a -> b
$ [THFLogicFormula]
ts, IdSet
nids)
TermToken _ ->
String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "Missing translation for term tokens." (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t)
AsPattern {} ->
String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "As patterns are not supported in THF0." (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t)
LetTerm {} ->
String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "Let terms are not supported in THF0." (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t)
CaseTerm {} ->
String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "Case statements are not supported in THF." (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t)
_ ->
String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "HasCASL2THF0.transTerm" (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t)
redTypedTerm :: HCAs.Term -> TypeQual -> HCAs.Type -> Range -> Result HCAs.Term
redTypedTerm :: Term -> TypeQual -> Type -> Range -> Result Term
redTypedTerm t1 :: Term
t1 tq1 :: TypeQual
tq1 _ r1 :: Range
r1 =
if TypeQual -> [TypeQual] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem TypeQual
tq1 [TypeQual
Inferred, TypeQual
OfType]
then case Term
t1 of
TypedTerm t2 :: Term
t2 tq2 :: TypeQual
tq2 ty2 :: Type
ty2 r2 :: Range
r2 -> Term -> TypeQual -> Type -> Range -> Result Term
redTypedTerm Term
t2 TypeQual
tq2 Type
ty2 Range
r2
_ -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t1
else String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Typed terms are not supported in THF0." Range
r1
transQualOp :: Env -> IdSet -> OpBrand -> PolyId -> TypeScheme
-> [HCAs.Type] -> InstKind -> Range -> Result (Constant, IdSet)
transQualOp :: Env
-> IdSet
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Result (Constant, IdSet)
transQualOp e :: Env
e ids :: IdSet
ids _ (PolyId i :: Id
i _ _) ts :: TypeScheme
ts _ _ r :: Range
r = do
let nids :: IdSet
nids = if Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i (((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList) then Id -> IdSet -> IdSet
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
i IdSet
ids else IdSet
ids
case Id -> Assumps -> Maybe (Set OpInfo)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i (Env -> Assumps
assumps Env
e) of
Just s :: Set OpInfo
s
| Set OpInfo -> Int
forall a. Set a -> Int
Set.size Set OpInfo
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 -> String -> Range -> Result (Constant, IdSet)
forall a. String -> Range -> Result a
fatal_error ("unknown op: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i) Range
r
| Set OpInfo -> Int
forall a. Set a -> Int
Set.size Set OpInfo
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 -> Id -> Result Constant
transAssumpId Id
i Result Constant
-> (Constant -> Result (Constant, IdSet))
-> Result (Constant, IdSet)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ c :: Constant
c -> (Constant, IdSet) -> Result (Constant, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant
c, IdSet
nids))
| Set OpInfo -> Int
forall a. Set a -> Int
Set.size Set OpInfo
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 -> case TypeScheme -> [(TypeScheme, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup TypeScheme
ts ([TypeScheme] -> [(TypeScheme, Int)]
forall a. [a] -> [(a, Int)]
number
((OpInfo -> TypeScheme) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> TypeScheme
HCLe.opType (Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
s))) of
Nothing -> String -> Range -> Result (Constant, IdSet)
forall a. String -> Range -> Result a
fatal_error ("unknown op: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i) Range
r
Just num :: Int
num ->
Id -> Int -> Result Constant
transAssumpsId Id
i Int
num Result Constant
-> (Constant -> Result (Constant, IdSet))
-> Result (Constant, IdSet)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ c :: Constant
c -> (Constant, IdSet) -> Result (Constant, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant
c, IdSet
nids))
_ -> Id -> Result Constant
transAssumpId Id
i Result Constant
-> (Constant -> Result (Constant, IdSet))
-> Result (Constant, IdSet)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ c :: Constant
c -> (Constant, IdSet) -> Result (Constant, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant
c, IdSet
nids))
transApplTerm :: Env -> IdConstantMap -> IdSet -> HCAs.Term -> HCAs.Term
-> Range -> Result (THFLogicFormula, IdSet)
transApplTerm :: Env
-> Map Id Constant
-> IdSet
-> Term
-> Term
-> Range
-> Result (THFLogicFormula, IdSet)
transApplTerm e :: Env
e icm :: Map Id Constant
icm ids :: IdSet
ids t1 :: Term
t1 t2 :: Term
t2 r :: Range
r = do
let at :: Term
at = Term -> Term -> Range -> Term
ApplTerm Term
t1 Term
t2 Range
r
case Term -> Maybe (Term, Id, [Term])
myGetAppl Term
at of
Nothing -> String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error
("unexpected Term Application: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Term
at "") Range
r
Just (t3 :: Term
t3, i :: Id
i, tl1 :: [Term]
tl1)
| Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i [Id
exEq, Id
andId, Id
orId, Id
eqvId, Id
implId, Id
infixIf, Id
resId] ->
case [Term]
tl1 of
[TupleTerm tl2 :: [Term]
tl2 _] ->
([THFUnitaryFormula] -> THFLogicFormula)
-> Result ([THFUnitaryFormula], IdSet)
-> Result (THFLogicFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap (THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula (THFBinaryFormula -> THFLogicFormula)
-> ([THFUnitaryFormula] -> THFBinaryFormula)
-> [THFUnitaryFormula]
-> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple
(THFBinaryTuple -> THFBinaryFormula)
-> ([THFUnitaryFormula] -> THFBinaryTuple)
-> [THFUnitaryFormula]
-> THFBinaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula ([THFUnitaryFormula] -> THFBinaryTuple)
-> ([THFUnitaryFormula] -> [THFUnitaryFormula])
-> [THFUnitaryFormula]
-> THFBinaryTuple
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. [a] -> [a]
reverse)
((([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet))
-> ([THFUnitaryFormula], IdSet)
-> [Term]
-> Result ([THFUnitaryFormula], IdSet)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet)
fTrmToUf ([], IdSet
ids) (Term
t3 Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
tl2))
_ -> String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error ("unexpected arguments " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Term] -> String
forall a. Show a => a -> String
show [Term]
tl1 String -> ShowS
forall a. [a] -> [a] -> [a]
++
" for the function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i) Range
r
| Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
eqId -> case [Term]
tl1 of
[TupleTerm tl2 :: [Term]
tl2 _] -> do
(ufs :: [THFUnitaryFormula]
ufs, ids' :: IdSet
ids') <- (([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet))
-> ([THFUnitaryFormula], IdSet)
-> [Term]
-> Result ([THFUnitaryFormula], IdSet)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet)
fTrmToUf ([], IdSet
ids) [Term]
tl2
(uf1 :: THFUnitaryFormula
uf1, uf2 :: THFUnitaryFormula
uf2) <- case [THFUnitaryFormula]
ufs of
[uf1 :: THFUnitaryFormula
uf1, uf2 :: THFUnitaryFormula
uf2] -> (THFUnitaryFormula, THFUnitaryFormula)
-> Result (THFUnitaryFormula, THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula
uf1, THFUnitaryFormula
uf2)
_ -> String -> Range -> Result (THFUnitaryFormula, THFUnitaryFormula)
forall a. String -> Range -> Result a
fatal_error ("equality needs " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"exactly 2 arguments") Range
r
(THFLogicFormula, IdSet) -> Result (THFLogicFormula, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula (THFBinaryFormula -> THFLogicFormula)
-> THFBinaryFormula -> THFLogicFormula
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula
-> THFPairConnective -> THFUnitaryFormula -> THFBinaryFormula
TBF_THF_Binary_Pair
THFUnitaryFormula
uf1 THFPairConnective
Infix_Equality THFUnitaryFormula
uf2, IdSet
ids')
_ -> String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error ("unexpected arguments " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Term] -> String
forall a. Show a => a -> String
show [Term]
tl1 String -> ShowS
forall a. [a] -> [a] -> [a]
++
" for equality") Range
r
| Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
whenElse ->
case [Term]
tl1 of
[TupleTerm [then_ :: Term
then_, cond :: Term
cond, else_ :: Term
else_] _] ->
let then_' :: Term
then_' = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId
([Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Term -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Term
then_, Term -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Term
cond])
Term
cond Term
then_
else_' :: Term
else_' = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
andId
([Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ [[Pos]] -> [Pos]
joinRanges [Term -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Term
else_, Term -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Term
cond])
(Term -> Term -> Range -> Term
ApplTerm (Id -> TypeScheme -> Term
mkOpTerm Id
negId TypeScheme
notType)
Term
cond (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
cond)) Term
else_
in Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
e Map Id Constant
icm IdSet
ids (Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
r Term
then_' Term
else_')
_ -> String -> Range -> Result (THFLogicFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "invalid whenElse" Range
r
| Bool
otherwise -> ([THFUnitaryFormula] -> THFLogicFormula)
-> Result ([THFUnitaryFormula], IdSet)
-> Result (THFLogicFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap (THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula (THFBinaryFormula -> THFLogicFormula)
-> ([THFUnitaryFormula] -> THFBinaryFormula)
-> [THFUnitaryFormula]
-> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple
(THFBinaryTuple -> THFBinaryFormula)
-> ([THFUnitaryFormula] -> THFBinaryTuple)
-> [THFUnitaryFormula]
-> THFBinaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula ([THFUnitaryFormula] -> THFBinaryTuple)
-> ([THFUnitaryFormula] -> [THFUnitaryFormula])
-> [THFUnitaryFormula]
-> THFBinaryTuple
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. [a] -> [a]
reverse)
((([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet))
-> ([THFUnitaryFormula], IdSet)
-> [Term]
-> Result ([THFUnitaryFormula], IdSet)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet)
fTrmToUf ([], IdSet
ids) (Term
t3 Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
tl1))
where
fTrmToUf :: ([THFUnitaryFormula], IdSet) -> HCAs.Term
-> Result ([THFUnitaryFormula], IdSet)
fTrmToUf :: ([THFUnitaryFormula], IdSet)
-> Term -> Result ([THFUnitaryFormula], IdSet)
fTrmToUf (ufl :: [THFUnitaryFormula]
ufl, oids :: IdSet
oids) t :: Term
t = do
(uf :: THFUnitaryFormula
uf, nids :: IdSet
nids) <- (THFLogicFormula -> THFUnitaryFormula)
-> Result (THFLogicFormula, IdSet)
-> Result (THFUnitaryFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap THFLogicFormula -> THFUnitaryFormula
lfToUf (Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
e Map Id Constant
icm IdSet
oids Term
t)
([THFUnitaryFormula], IdSet) -> Result ([THFUnitaryFormula], IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula
uf THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula]
ufl, IdSet
nids)
myGetAppl :: HCAs.Term -> Maybe (HCAs.Term, Id, [HCAs.Term])
myGetAppl :: Term -> Maybe (Term, Id, [Term])
myGetAppl = ([Term] -> [Term])
-> Maybe (Term, Id, [Term]) -> Maybe (Term, Id, [Term])
forall c a b. (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM [Term] -> [Term]
forall a. [a] -> [a]
reverse (Maybe (Term, Id, [Term]) -> Maybe (Term, Id, [Term]))
-> (Term -> Maybe (Term, Id, [Term]))
-> Term
-> Maybe (Term, Id, [Term])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe (Term, Id, [Term])
getRevAppl where
thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM :: (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM f :: c -> c
f = ((a, b, c) -> (a, b, c)) -> Maybe (a, b, c) -> Maybe (a, b, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \ (a :: a
a, b :: b
b, c :: c
c) -> (a
a, b
b, c -> c
f c
c))
getRevAppl :: HCAs.Term -> Maybe (HCAs.Term, Id, [HCAs.Term])
getRevAppl :: Term -> Maybe (Term, Id, [Term])
getRevAppl t :: Term
t = case Term
t of
TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> case TypeQual
q of
InType -> Maybe (Term, Id, [Term])
forall a. Maybe a
Nothing
_ -> Term -> Maybe (Term, Id, [Term])
getRevAppl Term
trm
QualVar (VarDecl i :: Id
i _ _ _) -> (Term, Id, [Term]) -> Maybe (Term, Id, [Term])
forall a. a -> Maybe a
Just (Term
t, Id
i, [])
QualOp _ (PolyId i :: Id
i _ _) _ _ _ _ -> (Term, Id, [Term]) -> Maybe (Term, Id, [Term])
forall a. a -> Maybe a
Just (Term
t, Id
i, [])
ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> ([Term] -> [Term])
-> Maybe (Term, Id, [Term]) -> Maybe (Term, Id, [Term])
forall c a b. (c -> c) -> Maybe (a, b, c) -> Maybe (a, b, c)
thrdM (Term
t2 Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:) (Maybe (Term, Id, [Term]) -> Maybe (Term, Id, [Term]))
-> Maybe (Term, Id, [Term]) -> Maybe (Term, Id, [Term])
forall a b. (a -> b) -> a -> b
$ Term -> Maybe (Term, Id, [Term])
getRevAppl Term
t1
_ -> Maybe (Term, Id, [Term])
forall a. Maybe a
Nothing
transLamdaTerm :: Env -> IdConstantMap -> IdSet -> [HCAs.Term] -> Partiality
-> HCAs.Term -> Range -> Result (THFLogicFormula, IdSet)
transLamdaTerm :: Env
-> Map Id Constant
-> IdSet
-> [Term]
-> Partiality
-> Term
-> Range
-> Result (THFLogicFormula, IdSet)
transLamdaTerm e :: Env
e icm :: Map Id Constant
icm ids :: IdSet
ids tl :: [Term]
tl _ t :: Term
t _ = do
[THFVariable]
vl <- (Term -> Result THFVariable) -> [Term] -> Result [THFVariable]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Result THFVariable
trVar [Term]
tl
(uf :: THFUnitaryFormula
uf, nids :: IdSet
nids) <- (THFLogicFormula -> THFUnitaryFormula)
-> Result (THFLogicFormula, IdSet)
-> Result (THFUnitaryFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap THFLogicFormula -> THFUnitaryFormula
lfToUf (Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
e Map Id Constant
icm IdSet
ids Term
t)
(THFLogicFormula, IdSet) -> Result (THFLogicFormula, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (THFUnitaryFormula -> THFLogicFormula)
-> THFUnitaryFormula -> THFLogicFormula
forall a b. (a -> b) -> a -> b
$ [THFVariable] -> THFUnitaryFormula -> THFUnitaryFormula
T0UF_THF_Abstraction [THFVariable]
vl THFUnitaryFormula
uf, IdSet
nids)
where
trVar :: HCAs.Term -> Result THFVariable
trVar :: Term -> Result THFVariable
trVar t1 :: Term
t1 = case Term
t1 of
TypedTerm t2 :: Term
t2 tq :: TypeQual
tq ty :: Type
ty r :: Range
r -> Term -> TypeQual -> Type -> Range -> Result Term
redTypedTerm Term
t2 TypeQual
tq Type
ty Range
r Result Term -> (Term -> Result THFVariable) -> Result THFVariable
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term -> Result THFVariable
trVar
QualVar vd :: VarDecl
vd -> Map Id Constant -> VarDecl -> Result THFVariable
transVarDecl Map Id Constant
icm VarDecl
vd
_ -> String -> Range -> Result THFVariable
forall a. String -> Range -> Result a
fatal_error ("Unexpected term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
t1
String -> ShowS
forall a. [a] -> [a] -> [a]
++ " Expected variable.") (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t1)
transQuantifiedTerm :: Env -> IdConstantMap -> IdSet -> HCAs.Quantifier
-> [HCAs.GenVarDecl] -> HCAs.Term -> Range
-> Result (THFAs.THFQuantifiedFormula, IdSet)
transQuantifiedTerm :: Env
-> Map Id Constant
-> IdSet
-> Quantifier
-> [GenVarDecl]
-> Term
-> Range
-> Result (THFQuantifiedFormula, IdSet)
transQuantifiedTerm e :: Env
e icm :: Map Id Constant
icm ids :: IdSet
ids q :: Quantifier
q gcdl :: [GenVarDecl]
gcdl t :: Term
t r :: Range
r = case Quantifier
q of
Universal -> Quantifier -> Result (THFQuantifiedFormula, IdSet)
tqHelper Quantifier
T0Q_ForAll
Existential -> Quantifier -> Result (THFQuantifiedFormula, IdSet)
tqHelper Quantifier
T0Q_Exists
Unique ->
String -> Range -> Result (THFQuantifiedFormula, IdSet)
forall a. String -> Range -> Result a
fatal_error "Unique quantifications are not supported yet." Range
r
where
tqHelper :: THFAs.Quantifier
-> Result (THFAs.THFQuantifiedFormula, IdSet)
tqHelper :: Quantifier -> Result (THFQuantifiedFormula, IdSet)
tqHelper quant :: Quantifier
quant = do
[THFVariable]
vl <- (GenVarDecl -> Result THFVariable)
-> [GenVarDecl] -> Result [THFVariable]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Id Constant -> GenVarDecl -> Result THFVariable
transGenVatDecl Map Id Constant
icm) [GenVarDecl]
gcdl
(THFLogicFormula -> THFQuantifiedFormula)
-> Result (THFLogicFormula, IdSet)
-> Result (THFQuantifiedFormula, IdSet)
forall a b. (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap (Quantifier
-> [THFVariable] -> THFUnitaryFormula -> THFQuantifiedFormula
T0QF_THF_Quantified_Var Quantifier
quant [THFVariable]
vl (THFUnitaryFormula -> THFQuantifiedFormula)
-> (THFLogicFormula -> THFUnitaryFormula)
-> THFLogicFormula
-> THFQuantifiedFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFLogicFormula -> THFUnitaryFormula
lfToUf)
(Env
-> Map Id Constant
-> IdSet
-> Term
-> Result (THFLogicFormula, IdSet)
transTerm Env
e Map Id Constant
icm IdSet
ids Term
t)
transGenVatDecl :: IdConstantMap -> GenVarDecl
-> Result THFVariable
transGenVatDecl :: Map Id Constant -> GenVarDecl -> Result THFVariable
transGenVatDecl icm :: Map Id Constant
icm gvd :: GenVarDecl
gvd = case GenVarDecl
gvd of
GenVarDecl vd :: VarDecl
vd -> Map Id Constant -> VarDecl -> Result THFVariable
transVarDecl Map Id Constant
icm VarDecl
vd
GenTypeVarDecl (TypeArg _ _ _ _ _ _ r :: Range
r) ->
String -> Range -> Result THFVariable
forall a. String -> Range -> Result a
fatal_error "GenTypeVarDecl not supported" Range
r
transVarDecl :: IdConstantMap -> VarDecl -> Result THFVariable
transVarDecl :: Map Id Constant -> VarDecl -> Result THFVariable
transVarDecl icm :: Map Id Constant
icm (VarDecl i :: Id
i t :: Type
t _ _) = do
Token
v <- Id -> Result Token
transVarId Id
i
THFTopLevelType
tlt <- Map Id Constant -> Type -> Result Type
transType Map Id Constant
icm Type
t Result Type
-> (Type -> Result THFTopLevelType) -> Result THFTopLevelType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Result THFTopLevelType
typeToTopLevelType
THFVariable -> Result THFVariable
forall (m :: * -> *) a. Monad m => a -> m a
return (THFVariable -> Result THFVariable)
-> THFVariable -> Result THFVariable
forall a b. (a -> b) -> a -> b
$ Token -> THFTopLevelType -> THFVariable
TV_THF_Typed_Variable Token
v THFTopLevelType
tlt
genTuple :: [THFCons.Type] -> Result THFAs.THFBinaryType
genTuple :: [Type] -> Result THFBinaryType
genTuple ts :: [Type]
ts = case [Type]
ts of
[] -> String -> Range -> Result THFBinaryType
forall a. String -> Range -> Result a
fatal_error "Empty product type" Range
nullRange
[tp :: Type
tp] -> Type -> Result THFBinaryType
typeToBinaryType Type
tp
_ -> ([THFUnitaryType] -> THFBinaryType)
-> Result [THFUnitaryType] -> Result THFBinaryType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [THFUnitaryType] -> THFBinaryType
TBT_THF_Xprod_Type (Result [THFUnitaryType] -> Result THFBinaryType)
-> Result [THFUnitaryType] -> Result THFBinaryType
forall a b. (a -> b) -> a -> b
$ (Type -> Result THFUnitaryType)
-> [Type] -> Result [THFUnitaryType]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR Type -> Result THFUnitaryType
typeToUnitaryType [Type]
ts
lfToUf :: THFLogicFormula -> THFUnitaryFormula
lfToUf :: THFLogicFormula -> THFUnitaryFormula
lfToUf lf :: THFLogicFormula
lf = case THFLogicFormula
lf of
TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> THFUnitaryFormula
uf
_ -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par THFLogicFormula
lf
type IdSet = Set.Set Id
myFmap :: (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap :: (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)
myFmap fun :: a -> b
fun res :: Result (a, IdSet)
res = do
(something :: a
something, ids :: IdSet
ids) <- Result (a, IdSet)
res
(b, IdSet) -> Result (b, IdSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
fun a
something, IdSet
ids)