{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/HasCASL2THFP_P.hs
Description :  Comorphism from HasCASL to THF
Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Alexis.Tsogias@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from HasCASL to THFP_P.
-}

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

-- Question: are the remaining symbol variants translatable?

-- | The identity of the comorphism
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 -- topLogic
    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
    -- isInclusionComorphism HasCASL2THF0_ST = True
    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 }

-- Translation of a Theory

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

-- Translation methods for the components a signature

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

-- a mapping between ids of hascasl types and their representation in THF
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

{- method used to add a type to the tail of a type
it is used e.g. to transform Types of predicates into function types
by adding the boolean-Type OType to the tail.
Example:
insLast OType (OType > A > IType)  -->  OType > A > IType > OType -}
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 }


-- Transation of Symbols

{- Not supported symbols:
 ClassAsItemType RawKind
 SuperClassSymbol Kind
 SuperTypeSymbol Id
 TypeKindInstance Kind
 TypeAliasSymbol Type
-}

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 }


-- Translating methods for Sentences

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)

{- | decompose an 'ApplTerm' into an application of an operation and a
     list of arguments -}
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
            {- two possible translatione for uniqueness:
            1. Ex: x . P(x) /\ Not (Ex : x,y . (P(x) /\ P(y) /\ not (x = y)))
            2. Ex: x . (All : y . (P(y) <=> x = y)) -}
    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

-- THFLogicFormula to THFUnitaryFormula
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

-- Helper

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)