{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2SubCFOL.hs
Description :  coding out partiality
Copyright   :  (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Comorphism)

Coding out partiality (SubPCFOL= -> SubCFOL=) while keeping subsorting.
Without unique bottoms sort generation axioms are not allowed.
Then we have (SubPFOL= -> SubFOL=).
-}

module Comorphisms.CASL2SubCFOL where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic as SL hiding (bottom)
import CASL.Fold
import CASL.Project
import CASL.Simplify

import Common.Id
import Common.DocUtils
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
import Common.AS_Annotation
import Common.ProofUtils
import Common.ProofTree
import Common.Utils
import qualified Control.Monad.Fail as Fail

-- | determine the need for bottom constants
data FormulaTreatment =
    NoMembershipOrCast
  | FormulaDependent
  | SubsortBottoms
  | AllSortBottoms
    deriving Int -> FormulaTreatment -> ShowS
[FormulaTreatment] -> ShowS
FormulaTreatment -> String
(Int -> FormulaTreatment -> ShowS)
-> (FormulaTreatment -> String)
-> ([FormulaTreatment] -> ShowS)
-> Show FormulaTreatment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FormulaTreatment] -> ShowS
$cshowList :: [FormulaTreatment] -> ShowS
show :: FormulaTreatment -> String
$cshow :: FormulaTreatment -> String
showsPrec :: Int -> FormulaTreatment -> ShowS
$cshowsPrec :: Int -> FormulaTreatment -> ShowS
Show

-- | a case selector for formula treatment
treatFormula :: FormulaTreatment -> a -> a -> a -> a -> a
treatFormula :: FormulaTreatment -> a -> a -> a -> a -> a
treatFormula g :: FormulaTreatment
g a :: a
a b :: a
b c :: a
c d :: a
d = case FormulaTreatment
g of
    NoMembershipOrCast -> a
a
    FormulaDependent -> a
b
    SubsortBottoms -> a
c
    AllSortBottoms -> a
d

{- | The identity of the comorphism depending on parameters.
    'NoMembershipOrCast' reject membership test or cast to non-bottom sorts.
.   'FormulaDependent' creates a formula dependent signature translation.
    'SubsortBottoms' creates bottoms for all proper subsorts. -}
data CASL2SubCFOL = CASL2SubCFOL
    { CASL2SubCFOL -> Bool
uniqueBottom :: Bool -- ^ removes free types
    , CASL2SubCFOL -> FormulaTreatment
formulaTreatment :: FormulaTreatment
    -- ^ deal with membership tests and casts
    } deriving Int -> CASL2SubCFOL -> ShowS
[CASL2SubCFOL] -> ShowS
CASL2SubCFOL -> String
(Int -> CASL2SubCFOL -> ShowS)
-> (CASL2SubCFOL -> String)
-> ([CASL2SubCFOL] -> ShowS)
-> Show CASL2SubCFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2SubCFOL] -> ShowS
$cshowList :: [CASL2SubCFOL] -> ShowS
show :: CASL2SubCFOL -> String
$cshow :: CASL2SubCFOL -> String
showsPrec :: Int -> CASL2SubCFOL -> ShowS
$cshowsPrec :: Int -> CASL2SubCFOL -> ShowS
Show

{- | create unique bottoms, sorts with bottom depend on membership
and casts in theory sentences. -}
defaultCASL2SubCFOL :: CASL2SubCFOL
defaultCASL2SubCFOL :: CASL2SubCFOL
defaultCASL2SubCFOL = Bool -> FormulaTreatment -> CASL2SubCFOL
CASL2SubCFOL Bool
True FormulaTreatment
FormulaDependent

instance Language CASL2SubCFOL where
    language_name :: CASL2SubCFOL -> String
language_name (CASL2SubCFOL b :: Bool
b m :: FormulaTreatment
m) = "CASL2SubCFOL"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "" else "PersistentlyLiberal")
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ FormulaTreatment -> String -> String -> String -> ShowS
forall a. FormulaTreatment -> a -> a -> a -> a -> a
treatFormula FormulaTreatment
m (FormulaTreatment -> String
forall a. Show a => a -> String
show FormulaTreatment
m) "" (FormulaTreatment -> String
forall a. Show a => a -> String
show FormulaTreatment
m) (FormulaTreatment -> String
forall a. Show a => a -> String
show FormulaTreatment
m)

instance Comorphism CASL2SubCFOL
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
    sourceLogic :: CASL2SubCFOL -> CASL
sourceLogic (CASL2SubCFOL _ _) = CASL
CASL
    sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics
sourceSublogic (CASL2SubCFOL b :: Bool
b _) =
        if Bool
b then CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop else CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
          { cons_features :: SortGenerationFeatures
cons_features = Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SL.SortGen Bool
False Bool
False SortGenTotality
SL.OnlyTotal }
    targetLogic :: CASL2SubCFOL -> CASL
targetLogic (CASL2SubCFOL _ _) = CASL
CASL
    mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics
mapSublogic (CASL2SubCFOL b :: Bool
b _) sl :: CASL_Sublogics
sl = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$ if CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
has_part CASL_Sublogics
sl then CASL_Sublogics
sl
        { has_part :: Bool
has_part = Bool
False -- partiality is coded out
        , cons_features :: SortGenerationFeatures
cons_features = let cf :: SortGenerationFeatures
cf = CASL_Sublogics -> SortGenerationFeatures
forall a. CASL_SL a -> SortGenerationFeatures
cons_features CASL_Sublogics
sl in case SortGenerationFeatures
cf of
          (SL.SortGen _ _ tcf :: SortGenTotality
tcf) -> SortGenerationFeatures
cf
            { totality :: SortGenTotality
totality = if Bool
b then SortGenTotality
SL.OnlyTotal else SortGenTotality -> SortGenTotality -> SortGenTotality
forall a. Ord a => a -> a -> a
max SortGenTotality
tcf SortGenTotality
SL.OnlyTotal }
            -- …in constructors, too
          _ -> SortGenerationFeatures
cf
        , has_pred :: Bool
has_pred = Bool
True
        , which_logic :: CASL_Formulas
which_logic = CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
Horn (CASL_Formulas -> CASL_Formulas) -> CASL_Formulas -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ CASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_Sublogics
sl
        , has_eq :: Bool
has_eq = Bool
True} else CASL_Sublogics
sl
    map_theory :: CASL2SubCFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory (CASL2SubCFOL b :: Bool
b m :: FormulaTreatment
m) (sig :: CASLSign
sig, sens :: [Named CASLFORMULA]
sens) =
        let fbsrts :: Set SORT
fbsrts = [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (Named CASLFORMULA -> Set SORT)
-> [Named CASLFORMULA] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> Set SORT
forall f. FORMULA f -> Set SORT
botFormulaSorts (CASLFORMULA -> Set SORT)
-> (Named CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA
-> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence) [Named CASLFORMULA]
sens
            bsrts :: Set SORT
bsrts = FormulaTreatment -> CASLSign -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom FormulaTreatment
m CASLSign
sig Set SORT
fbsrts
            sens1 :: [Named CASLFORMULA]
sens1 = Bool -> Set SORT -> CASLSign -> [Named CASLFORMULA]
forall f e.
(Ord f, TermExtension f) =>
Bool -> Set SORT -> Sign f e -> [Named (FORMULA f)]
generateAxioms Bool
b Set SORT
bsrts CASLSign
sig
            sens2 :: [Named CASLFORMULA]
sens2 =
              (Named CASLFORMULA -> Named CASLFORMULA)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula () -> ()
forall a. a -> a
id (CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Set SORT -> CASLFORMULA -> CASLFORMULA
codeFormula Bool
b Set SORT
bsrts)) [Named CASLFORMULA]
sens
        in case FormulaTreatment
m of
             NoMembershipOrCast
               | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Bool
forall a. Set a -> Bool
Set.null (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
fbsrts Set SORT
bsrts ->
                 String -> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "CASL2SubCFOL: unexpected membership test or cast"
             _ -> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return
                 ( Set SORT -> CASLSign -> CASLSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig Set SORT
bsrts CASLSign
sig
                 , [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [Named a] -> [Named a]
nameAndDisambiguate ([Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Named CASLFORMULA]
sens1 [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
sens2)
    map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor
map_morphism (CASL2SubCFOL _ m :: FormulaTreatment
m) mor :: CASLMor
mor@Morphism {msource :: forall f e m. Morphism f e m -> Sign f e
msource = CASLSign
src, mtarget :: forall f e m. Morphism f e m -> Sign f e
mtarget = CASLSign
tar}
        = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return
        CASLMor
mor { msource :: CASLSign
msource = Set SORT -> CASLSign -> CASLSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig (FormulaTreatment -> CASLSign -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom FormulaTreatment
m CASLSign
src Set SORT
forall a. Set a
Set.empty) CASLSign
src
            , mtarget :: CASLSign
mtarget = Set SORT -> CASLSign -> CASLSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig (FormulaTreatment -> CASLSign -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom FormulaTreatment
m CASLSign
tar Set SORT
forall a. Set a
Set.empty) CASLSign
tar
            , op_map :: Op_map
op_map = ((SORT, OpKind) -> (SORT, OpKind)) -> Op_map -> Op_map
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (i :: SORT
i, _) -> (SORT
i, OpKind
Total)) (Op_map -> Op_map) -> Op_map -> Op_map
forall a b. (a -> b) -> a -> b
$ CASLMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map CASLMor
mor }
    map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
map_sentence (CASL2SubCFOL b :: Bool
b m :: FormulaTreatment
m) sig :: CASLSign
sig sen :: CASLFORMULA
sen = let
        fbsrts :: Set SORT
fbsrts = CASLFORMULA -> Set SORT
forall f. FORMULA f -> Set SORT
botFormulaSorts CASLFORMULA
sen
        bsrts :: Set SORT
bsrts = FormulaTreatment -> CASLSign -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom FormulaTreatment
m CASLSign
sig Set SORT
fbsrts
        in case FormulaTreatment
m of
             NoMembershipOrCast
               | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Bool
forall a. Set a -> Bool
Set.null (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
fbsrts Set SORT
bsrts ->
                 String -> Result CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result CASLFORMULA) -> String -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "CASL2SubCFOL: unexpected membership test or cast:\n"
                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ CASLFORMULA -> ShowS
forall a. Pretty a => a -> ShowS
showDoc CASLFORMULA
sen ""
             _ -> CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula () -> ()
forall a. a -> a
id (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Bool -> Set SORT -> CASLFORMULA -> CASLFORMULA
codeFormula Bool
b Set SORT
bsrts CASLFORMULA
sen
    map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol
map_symbol (CASL2SubCFOL _ _) _ s :: Symbol
s =
      Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton Symbol
s { symbType :: SymbType
symbType = SymbType -> SymbType
totalizeSymbType (SymbType -> SymbType) -> SymbType -> SymbType
forall a b. (a -> b) -> a -> b
$ Symbol -> SymbType
symbType Symbol
s }
    has_model_expansion :: CASL2SubCFOL -> Bool
has_model_expansion (CASL2SubCFOL _ _) = Bool
True
    is_weakly_amalgamable :: CASL2SubCFOL -> Bool
is_weakly_amalgamable (CASL2SubCFOL _ _) = Bool
True

totalizeSymbType :: SymbType -> SymbType
totalizeSymbType :: SymbType -> SymbType
totalizeSymbType t :: SymbType
t = case SymbType
t of
  OpAsItemType ot :: OpType
ot -> OpType -> SymbType
OpAsItemType (OpType -> SymbType) -> OpType -> SymbType
forall a b. (a -> b) -> a -> b
$ OpType -> OpType
mkTotal OpType
ot
  _ -> SymbType
t

sortsWithBottom :: FormulaTreatment -> Sign f e -> Set.Set SORT -> Set.Set SORT
sortsWithBottom :: FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom m :: FormulaTreatment
m sig :: Sign f e
sig formBotSrts :: Set SORT
formBotSrts =
    let bsrts :: Set SORT
bsrts = FormulaTreatment
-> Set SORT -> Set SORT -> Set SORT -> Set SORT -> Set SORT
forall a. FormulaTreatment -> a -> a -> a -> a -> a
treatFormula FormulaTreatment
m Set SORT
forall a. Set a
Set.empty Set SORT
formBotSrts
          (Rel SORT -> Set SORT
forall a. Rel a -> Set a
Rel.keysSet (Rel SORT -> Set SORT)
-> (Rel SORT -> Rel SORT) -> Rel SORT -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.rmNullSets (Rel SORT -> Set SORT) -> Rel SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig) (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig)
        ops :: Set OpType
ops = MapSet SORT OpType -> Set OpType
forall b a. Ord b => MapSet a b -> Set b
MapSet.elems (MapSet SORT OpType -> Set OpType)
-> MapSet SORT OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f e
sig
        -- all supersorts inherit the same bottom element
        allSortsWithBottom :: Set SORT -> Set SORT
allSortsWithBottom s :: Set SORT
s =
            [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT
s Set SORT -> [Set SORT] -> [Set SORT]
forall a. a -> [a] -> [a]
: (SORT -> Set SORT) -> [SORT] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
`supersortsOf` Sign f e
sig) (Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
s)
        resSortsOfPartialFcts :: Set SORT
resSortsOfPartialFcts =
            Set SORT -> Set SORT
allSortsWithBottom (Set SORT -> Set SORT)
-> (Set OpType -> Set SORT) -> Set OpType -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set SORT
bsrts
               (Set SORT -> Set SORT)
-> (Set OpType -> Set SORT) -> Set OpType -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpType -> SORT) -> Set OpType -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map OpType -> SORT
opRes (Set OpType -> Set SORT) -> Set OpType -> Set SORT
forall a b. (a -> b) -> a -> b
$ (OpType -> Bool) -> Set OpType -> Set OpType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter OpType -> Bool
isPartial Set OpType
ops
        collect :: Set SORT -> Set SORT
collect given :: Set SORT
given =
            let more :: Set SORT
more = Set SORT -> Set SORT
allSortsWithBottom (Set SORT -> Set SORT)
-> (Set OpType -> Set SORT) -> Set OpType -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpType -> SORT) -> Set OpType -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map OpType -> SORT
opRes (Set OpType -> Set SORT) -> Set OpType -> Set SORT
forall a b. (a -> b) -> a -> b
$ (OpType -> Bool) -> Set OpType -> Set OpType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter
                      ((SORT -> Bool) -> [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SORT
given) ([SORT] -> Bool) -> (OpType -> [SORT]) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> [SORT]
opArgs) Set OpType
ops
            in if Set SORT -> Set SORT -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set SORT
more Set SORT
given then Set SORT
given
               else Set SORT -> Set SORT
collect (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set SORT
more Set SORT
given
     in Set SORT -> Set SORT
collect Set SORT
resSortsOfPartialFcts

defPred :: Id
defPred :: SORT
defPred = String -> SORT
genName "defined"

defined :: TermExtension f => Set.Set SORT -> TERM f -> Range -> FORMULA f
defined :: Set SORT -> TERM f -> Range -> FORMULA f
defined bsorts :: Set SORT
bsorts t :: TERM f
t ps :: Range
ps = let s :: SORT
s = TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM f
t in
  if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s Set SORT
bsorts then PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
         (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
defPred ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT
s] Range
nullRange) Range
nullRange) [TERM f
t] Range
ps
  else Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
True Range
ps

defVards :: TermExtension f => Set.Set SORT -> [VAR_DECL] -> FORMULA f
defVards :: Set SORT -> [VAR_DECL] -> FORMULA f
defVards bs :: Set SORT
bs = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f)
-> ([VAR_DECL] -> [FORMULA f]) -> [VAR_DECL] -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR_DECL -> [FORMULA f]) -> [VAR_DECL] -> [FORMULA f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Set SORT -> VAR_DECL -> [FORMULA f]
forall f. TermExtension f => Set SORT -> VAR_DECL -> [FORMULA f]
defVars Set SORT
bs)

defVars :: TermExtension f => Set.Set SORT -> VAR_DECL -> [FORMULA f]
defVars :: Set SORT -> VAR_DECL -> [FORMULA f]
defVars bs :: Set SORT
bs (Var_decl vns :: [VAR]
vns s :: SORT
s _) = (VAR -> FORMULA f) -> [VAR] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (Set SORT -> SORT -> VAR -> FORMULA f
forall f. TermExtension f => Set SORT -> SORT -> VAR -> FORMULA f
defVar Set SORT
bs SORT
s) [VAR]
vns

defVar :: TermExtension f => Set.Set SORT -> SORT -> Token -> FORMULA f
defVar :: Set SORT -> SORT -> VAR -> FORMULA f
defVar bs :: Set SORT
bs s :: SORT
s v :: VAR
v = Set SORT -> TERM f -> Range -> FORMULA f
forall f.
TermExtension f =>
Set SORT -> TERM f -> Range -> FORMULA f
defined Set SORT
bs (VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
s Range
nullRange) Range
nullRange

totalizeOpSymb :: OP_SYMB -> OP_SYMB
totalizeOpSymb :: OP_SYMB -> OP_SYMB
totalizeOpSymb o :: OP_SYMB
o = case OP_SYMB
o of
    Qual_op_name i :: SORT
i (Op_type _ args :: [SORT]
args res :: SORT
res ps :: Range
ps) qs :: Range
qs ->
        SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
args SORT
res Range
ps) Range
qs
    _ -> OP_SYMB
o

addBottomAlt :: Constraint -> Constraint
addBottomAlt :: Constraint -> Constraint
addBottomAlt c :: Constraint
c = let t :: OP_TYPE
t = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (Constraint -> SORT
newSort Constraint
c) Range
nullRange in Constraint
c
    {opSymbs :: [(OP_SYMB, [Int])]
opSymbs = Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
c [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a. [a] -> [a] -> [a]
++ [(SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (OP_TYPE -> SORT
uniqueBotName OP_TYPE
t) OP_TYPE
t Range
nullRange, [])]}

argSorts :: Constraint -> Set.Set SORT
argSorts :: Constraint -> Set SORT
argSorts c :: Constraint
c = [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ ((OP_SYMB, [Int]) -> Set SORT) -> [(OP_SYMB, [Int])] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (OP_SYMB -> Set SORT
argsOpSymb (OP_SYMB -> Set SORT)
-> ((OP_SYMB, [Int]) -> OP_SYMB) -> (OP_SYMB, [Int]) -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OP_SYMB, [Int]) -> OP_SYMB
forall a b. (a, b) -> a
fst) ([(OP_SYMB, [Int])] -> [Set SORT])
-> [(OP_SYMB, [Int])] -> [Set SORT]
forall a b. (a -> b) -> a -> b
$ Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
c
    where argsOpSymb :: OP_SYMB -> Set SORT
argsOpSymb op :: OP_SYMB
op = case OP_SYMB
op of
              Qual_op_name _ ot :: OP_TYPE
ot _ -> [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ([SORT] -> Set SORT) -> [SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
ot
              _ -> String -> Set SORT
forall a. HasCallStack => String -> a
error "argSorts"

totalizeConstraint :: Set.Set SORT -> Constraint -> Constraint
totalizeConstraint :: Set SORT -> Constraint -> Constraint
totalizeConstraint bsrts :: Set SORT
bsrts c :: Constraint
c =
    (if SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Constraint -> SORT
newSort Constraint
c) Set SORT
bsrts then Constraint -> Constraint
addBottomAlt else Constraint -> Constraint
forall a. a -> a
id)
    Constraint
c { opSymbs :: [(OP_SYMB, [Int])]
opSymbs = ((OP_SYMB, [Int]) -> (OP_SYMB, [Int]))
-> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (o :: OP_SYMB
o, is :: [Int]
is) -> (OP_SYMB -> OP_SYMB
totalizeOpSymb OP_SYMB
o, [Int]
is)) ([(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])])
-> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> a -> b
$ Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
c }

botType :: SORT -> OpType
botType :: SORT -> OpType
botType = SORT -> OpType
sortToOpType

-- | Add projections to the signature
encodeSig :: Set.Set SORT -> Sign f e -> Sign f e
encodeSig :: Set SORT -> Sign f e -> Sign f e
encodeSig bsorts :: Set SORT
bsorts sig :: Sign f e
sig = if Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
bsorts then Sign f e
sig else
    Sign f e
sig { opMap :: MapSet SORT OpType
opMap = MapSet SORT OpType
projOpMap, predMap :: PredMap
predMap = PredMap
newpredMap } where
   newTotalMap :: MapSet SORT OpType
newTotalMap = (OpType -> OpType) -> MapSet SORT OpType -> MapSet SORT OpType
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map OpType -> OpType
mkTotal (MapSet SORT OpType -> MapSet SORT OpType)
-> MapSet SORT OpType -> MapSet SORT OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f e
sig
   botOpMap :: MapSet SORT OpType
botOpMap = (OpType -> MapSet SORT OpType -> MapSet SORT OpType)
-> MapSet SORT OpType -> Set OpType -> MapSet SORT OpType
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ bt :: OpType
bt -> SORT -> OpType -> MapSet SORT OpType -> MapSet SORT OpType
addOpTo (OP_TYPE -> SORT
uniqueBotName (OP_TYPE -> SORT) -> OP_TYPE -> SORT
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
bt) OpType
bt)
       MapSet SORT OpType
newTotalMap (Set OpType -> MapSet SORT OpType)
-> Set OpType -> MapSet SORT OpType
forall a b. (a -> b) -> a -> b
$ (SORT -> OpType) -> Set SORT -> Set OpType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SORT -> OpType
botType Set SORT
bsorts
   defType :: SORT -> PredType
defType x :: SORT
x = PredType :: [SORT] -> PredType
PredType {predArgs :: [SORT]
predArgs = [SORT
x]}
   defTypes :: Set PredType
defTypes = (SORT -> PredType) -> Set SORT -> Set PredType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SORT -> PredType
defType Set SORT
bsorts
   newpredMap :: PredMap
newpredMap = (Set PredType -> Set PredType) -> SORT -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
(Set b -> Set b) -> a -> MapSet a b -> MapSet a b
MapSet.update (Set PredType -> Set PredType -> Set PredType
forall a b. a -> b -> a
const Set PredType
defTypes) SORT
defPred (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sig
   rel :: Rel SORT
rel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig
   total :: (SORT, SORT) -> OpType
total (s :: SORT
s, s' :: SORT
s') = [SORT] -> SORT -> OpType
mkTotOpType [SORT
s'] SORT
s
   setprojOptype :: Set OpType
setprojOptype = ((SORT, SORT) -> OpType) -> Set (SORT, SORT) -> Set OpType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (SORT, SORT) -> OpType
total (Set (SORT, SORT) -> Set OpType) -> Set (SORT, SORT) -> Set OpType
forall a b. (a -> b) -> a -> b
$ ((SORT, SORT) -> Bool) -> Set (SORT, SORT) -> Set (SORT, SORT)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ( \ (s :: SORT
s, _) ->
       SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s Set SORT
bsorts) (Set (SORT, SORT) -> Set (SORT, SORT))
-> Set (SORT, SORT) -> Set (SORT, SORT)
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Set (SORT, SORT)
forall a. Ord a => Rel a -> Set (a, a)
Rel.toSet Rel SORT
rel
   projOpMap :: MapSet SORT OpType
projOpMap = (OpType -> MapSet SORT OpType -> MapSet SORT OpType)
-> MapSet SORT OpType -> Set OpType -> MapSet SORT OpType
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ t :: OpType
t -> SORT -> OpType -> MapSet SORT OpType -> MapSet SORT OpType
addOpTo (OP_TYPE -> SORT
uniqueProjName (OP_TYPE -> SORT) -> OP_TYPE -> SORT
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
t) OpType
t)
       MapSet SORT OpType
botOpMap Set OpType
setprojOptype

-- | Make the name for the non empty axiom from s to s' to s''
mkNonEmptyAxiomName :: SORT -> String
mkNonEmptyAxiomName :: SORT -> String
mkNonEmptyAxiomName = String -> SORT -> String
mkAxNameSingle "nonEmpty"

-- | Make the name for the not defined bottom axiom
mkNotDefBotAxiomName :: SORT -> String
mkNotDefBotAxiomName :: SORT -> String
mkNotDefBotAxiomName = String -> SORT -> String
mkAxNameSingle "notDefBottom"

-- | Make the name for the totality axiom
mkTotalityAxiomName :: OP_NAME -> String
mkTotalityAxiomName :: SORT -> String
mkTotalityAxiomName f :: SORT
f = "ga_strictness_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
f

generateAxioms :: (Ord f, TermExtension f) =>
  Bool -> Set.Set SORT -> Sign f e -> [Named (FORMULA f)]
generateAxioms :: Bool -> Set SORT -> Sign f e -> [Named (FORMULA f)]
generateAxioms uniqBot :: Bool
uniqBot bsorts :: Set SORT
bsorts sig :: Sign f e
sig = (SORT -> [Named (FORMULA f)]) -> [SORT] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ s :: SORT
s -> let
      vx :: VAR_DECL
vx = String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
s
      xt :: TERM f
xt = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vx
      hasBot :: Bool
hasBot = SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s Set SORT
bsorts
      prj :: TERM f -> TERM f
prj z :: TERM f
z = OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique OpKind
Total Range
nullRange TERM f
z SORT
s
      df :: TERM f -> FORMULA f
df z :: TERM f
z = Set SORT -> TERM f -> Range -> FORMULA f
forall f.
TermExtension f =>
Set SORT -> TERM f -> Range -> FORMULA f
defined Set SORT
bsorts TERM f
z Range
nullRange
      in (SORT -> [Named (FORMULA f)]) -> [SORT] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ s' :: SORT
s' ->
      [String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (String -> SORT -> SORT -> String
mkAxName "total_projection_injectivity" SORT
s' SORT
s)
      (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ let xv :: VAR_DECL
xv = String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
s'
            yv :: VAR_DECL
yv = String -> SORT -> VAR_DECL
mkVarDeclStr "y" SORT
s'
            tx :: TERM f
tx = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
xv
            ty :: TERM f
ty = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
yv
            px :: TERM f
px = TERM f -> TERM f
forall f. TermExtension f => TERM f -> TERM f
prj TERM f
forall f. TERM f
tx
            py :: TERM f
py = TERM f -> TERM f
forall f. TermExtension f => TERM f -> TERM f
prj TERM f
forall f. TERM f
ty
            epxy :: FORMULA f
epxy = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
px TERM f
py
      -- forall x,y:s' . d(pr(x)) /\\ d(pr(y)) /\\ pr(x)=pr(y) => x=y
        in [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
xv, VAR_DECL
yv]
           (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (if Bool
hasBot then [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [TERM f -> FORMULA f
forall f. TermExtension f => TERM f -> FORMULA f
df TERM f
px, TERM f -> FORMULA f
forall f. TermExtension f => TERM f -> FORMULA f
df TERM f
py, FORMULA f
epxy]
                    else FORMULA f
epxy) (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
forall f. TERM f
tx TERM f
forall f. TERM f
ty
            -- forall x:s . d(x) => pr(x)=x
      , String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (String -> SORT -> SORT -> String
mkAxName "total_projection" SORT
s' SORT
s)
      (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ let eq :: FORMULA f
eq = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (TERM f -> TERM f
forall f. TermExtension f => TERM f -> TERM f
prj (TERM f -> TERM f) -> TERM f -> TERM f
forall a b. (a -> b) -> a -> b
$ TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
forall f. TERM f
xt SORT
s' Range
nullRange) TERM f
forall f. TERM f
xt
        in [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vx]
               (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ if Bool
hasBot then FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (TERM f -> FORMULA f
forall f. TermExtension f => TERM f -> FORMULA f
df TERM f
forall f. TERM f
xt) FORMULA f
eq else FORMULA f
eq]) (SORT -> [SORT]
minSupers SORT
s)
         -- exists x:s . d(x)
      [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> String
mkNonEmptyAxiomName SORT
s)
         (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Existential [VAR_DECL
vx] (TERM f -> FORMULA f
forall f. TermExtension f => TERM f -> FORMULA f
df TERM f
forall f. TERM f
xt) Range
nullRange
         | Bool
hasBot]
      [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> String
mkNotDefBotAxiomName SORT
s)
         (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ let bty :: OP_TYPE
bty = OpType -> OP_TYPE
toOP_TYPE (OpType -> OP_TYPE) -> OpType -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ SORT -> OpType
botType SORT
s
               bt :: TERM f
bt = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp (OP_TYPE -> SORT
uniqueBotName OP_TYPE
bty) OP_TYPE
bty) []
           in if Bool
uniqBot then
              -- forall x:s . not d(x) <=> x=bottom
              [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vx]
              (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> FORMULA f
forall f. TermExtension f => TERM f -> FORMULA f
df TERM f
forall f. TERM f
xt) (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
forall f. TERM f
xt TERM f
forall f. TERM f
bt
              else FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> FORMULA f
forall f. TermExtension f => TERM f -> FORMULA f
df TERM f
forall f. TERM f
bt -- not d(bottom)
         | Bool
hasBot]) [SORT]
sortList
   [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Named (FORMULA f) -> Bool) -> Named (FORMULA f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Bool
forall f. FORMULA f -> Bool
is_True_atom (FORMULA f -> Bool)
-> (Named (FORMULA f) -> FORMULA f) -> Named (FORMULA f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence)
   ((Named (FORMULA f) -> Named (FORMULA f))
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> FORMULA f) -> Named (FORMULA f) -> Named (FORMULA f)
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((FORMULA f -> FORMULA f)
 -> Named (FORMULA f) -> Named (FORMULA f))
-> (FORMULA f -> FORMULA f)
-> Named (FORMULA f)
-> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ (f -> f) -> FORMULA f -> FORMULA f
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula f -> f
forall a. a -> a
id)
    ([Named (FORMULA f)] -> [Named (FORMULA f)])
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> Named (FORMULA f))
-> [(SORT, OpType)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: SORT
f, typ :: OpType
typ) ->
      let vs :: [VAR_DECL]
vs = ((SORT, Int) -> VAR_DECL) -> [(SORT, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, i :: Int
i) -> String -> SORT -> VAR_DECL
mkVarDeclStr ("x_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) SORT
s)
              ([(SORT, Int)] -> [VAR_DECL]) -> [(SORT, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ [SORT] -> [(SORT, Int)]
forall a. [a] -> [(a, Int)]
number ([SORT] -> [(SORT, Int)]) -> [SORT] -> [(SORT, Int)]
forall a b. (a -> b) -> a -> b
$ OpType -> [SORT]
opArgs OpType
typ
      in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> String
mkTotalityAxiomName SORT
f)
      -- forall x_i:s_i . d f(x_1, ..., x_n) {<}=> d x_1 /\\ ... /\\ d x_n
         (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vs
           (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (if OpType -> Bool
isTotal OpType
typ then FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv else FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl)
            (Set SORT -> TERM f -> Range -> FORMULA f
forall f.
TermExtension f =>
Set SORT -> TERM f -> Range -> FORMULA f
defined Set SORT
bsorts
             (OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
f (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE (OpType -> OP_TYPE) -> OpType -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ OpType -> OpType
mkTotal OpType
typ)
                      ([TERM f] -> TERM f) -> [TERM f] -> TERM f
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs) Range
nullRange)
            (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Set SORT -> [VAR_DECL] -> FORMULA f
forall f. TermExtension f => Set SORT -> [VAR_DECL] -> FORMULA f
defVards Set SORT
bsorts [VAR_DECL]
vs) [(SORT, OpType)]
opList
    [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ ((SORT, PredType) -> Named (FORMULA f))
-> [(SORT, PredType)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: SORT
p, typ :: PredType
typ) ->
      let vs :: [VAR_DECL]
vs = ((SORT, Int) -> VAR_DECL) -> [(SORT, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, i :: Int
i) -> String -> SORT -> VAR_DECL
mkVarDeclStr ("x_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) SORT
s)
              ([(SORT, Int)] -> [VAR_DECL]) -> [(SORT, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ [SORT] -> [(SORT, Int)]
forall a. [a] -> [(a, Int)]
number ([SORT] -> [(SORT, Int)]) -> [SORT] -> [(SORT, Int)]
forall a b. (a -> b) -> a -> b
$ PredType -> [SORT]
predArgs PredType
typ
      in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_predicate_strictness_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
p)
      -- forall x_i:s_i . p(x_1, ..., x_n) => d x_1 /\\ ... /\\ d x_n
         (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vs
           (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
            (PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
p (PredType -> PRED_TYPE
toPRED_TYPE PredType
typ) Range
nullRange)
                      ((VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs) Range
nullRange)
            (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Set SORT -> [VAR_DECL] -> FORMULA f
forall f. TermExtension f => Set SORT -> [VAR_DECL] -> FORMULA f
defVards Set SORT
bsorts [VAR_DECL]
vs) [(SORT, PredType)]
predList)
    where
        rel1 :: Rel SORT
rel1 = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig
        sccs :: [Set SORT]
sccs = Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel SORT
rel1
        rel2 :: Rel SORT
rel2 = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Rel SORT -> Rel SORT
forall a. Ord a => [Set a] -> Rel a -> Rel a
Rel.collaps [Set SORT]
sccs Rel SORT
rel1
        isos :: SORT -> Set SORT
isos so :: SORT
so = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
so (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (Set SORT -> Bool) -> [Set SORT] -> [Set SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
so) [Set SORT]
sccs
        minSupers :: SORT -> [SORT]
minSupers so :: SORT
so = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.delete SORT
so (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union (SORT -> Set SORT
isos SORT
so)
          (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (SORT -> Set SORT) -> [SORT] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Set SORT
isos ([SORT] -> [Set SORT]) -> [SORT] -> [Set SORT]
forall a b. (a -> b) -> a -> b
$ Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> SORT -> Set SORT
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel SORT
rel2 SORT
so
        sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
bsorts
        opList :: [(SORT, OpType)]
opList = MapSet SORT OpType -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (MapSet SORT OpType -> [(SORT, OpType)])
-> MapSet SORT OpType -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f e
sig
        predList :: [(SORT, PredType)]
predList = PredMap -> [(SORT, PredType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (PredMap -> [(SORT, PredType)]) -> PredMap -> [(SORT, PredType)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sig

codeRecord :: TermExtension f => Bool -> Set.Set SORT -> (f -> f)
  -> Record f (FORMULA f) (TERM f)
codeRecord :: Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeRecord uniBot :: Bool
uniBot bsrts :: Set SORT
bsrts mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
    { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ _ q :: QUANTIFIER
q vs :: [VAR_DECL]
vs qf :: FORMULA f
qf ps :: Range
ps ->
      case QUANTIFIER
q of
      Universal -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs
        (FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (Set SORT -> [VAR_DECL] -> FORMULA f
forall f. TermExtension f => Set SORT -> [VAR_DECL] -> FORMULA f
defVards Set SORT
bsrts [VAR_DECL]
vs) Relation
Implication FORMULA f
qf Range
ps) Range
ps
      _ -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs (Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [Set SORT -> [VAR_DECL] -> FORMULA f
forall f. TermExtension f => Set SORT -> [VAR_DECL] -> FORMULA f
defVards Set SORT
bsrts [VAR_DECL]
vs, FORMULA f
qf] Range
ps) Range
ps
    , foldDefinedness :: FORMULA f -> TERM f -> Range -> FORMULA f
foldDefinedness = (TERM f -> Range -> FORMULA f)
-> FORMULA f -> TERM f -> Range -> FORMULA f
forall a b. a -> b -> a
const ((TERM f -> Range -> FORMULA f)
 -> FORMULA f -> TERM f -> Range -> FORMULA f)
-> (TERM f -> Range -> FORMULA f)
-> FORMULA f
-> TERM f
-> Range
-> FORMULA f
forall a b. (a -> b) -> a -> b
$ Set SORT -> TERM f -> Range -> FORMULA f
forall f.
TermExtension f =>
Set SORT -> TERM f -> Range -> FORMULA f
defined Set SORT
bsrts
    , foldEquation :: FORMULA f -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
foldEquation = \ _ t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 ps :: Range
ps -> if Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Existl then
      Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t1 Equality
Strong TERM f
t2 Range
ps,
                  Set SORT -> TERM f -> Range -> FORMULA f
forall f.
TermExtension f =>
Set SORT -> TERM f -> Range -> FORMULA f
defined Set SORT
bsrts TERM f
t1 Range
ps] Range
ps else TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t1 Equality
e TERM f
t2 Range
ps
    , foldMembership :: FORMULA f -> TERM f -> SORT -> Range -> FORMULA f
foldMembership = \ _ t :: TERM f
t s :: SORT
s ps :: Range
ps ->
          Set SORT -> TERM f -> Range -> FORMULA f
forall f.
TermExtension f =>
Set SORT -> TERM f -> Range -> FORMULA f
defined Set SORT
bsrts (OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique OpKind
Total Range
ps TERM f
t SORT
s) Range
ps
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> FORMULA f
foldSort_gen_ax = \ _ cs :: [Constraint]
cs b :: Bool
b ->
          [Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax ((Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Set SORT -> Constraint -> Constraint
totalizeConstraint Set SORT
bsrts) [Constraint]
cs)
              (Bool -> FORMULA f) -> Bool -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Bool
b Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
uniBot Bool -> Bool -> Bool
|| Set SORT -> Bool
forall a. Set a -> Bool
Set.null (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set SORT
bsrts
                (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ([SORT] -> Set SORT) -> [SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (Constraint -> SORT) -> [Constraint] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> SORT
newSort [Constraint]
cs))
    , foldApplication :: TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f
foldApplication = (OP_SYMB -> [TERM f] -> Range -> TERM f)
-> TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall a b. a -> b -> a
const ((OP_SYMB -> [TERM f] -> Range -> TERM f)
 -> TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f)
-> (OP_SYMB -> [TERM f] -> Range -> TERM f)
-> TERM f
-> OP_SYMB
-> [TERM f]
-> Range
-> TERM f
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (OP_SYMB -> [TERM f] -> Range -> TERM f)
-> (OP_SYMB -> OP_SYMB) -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> OP_SYMB
totalizeOpSymb
    , foldCast :: TERM f -> TERM f -> SORT -> Range -> TERM f
foldCast = \ _ t :: TERM f
t s :: SORT
s ps :: Range
ps -> OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique OpKind
Total Range
ps TERM f
t SORT
s }

codeFormula :: Bool -> Set.Set SORT -> FORMULA () -> FORMULA ()
codeFormula :: Bool -> Set SORT -> CASLFORMULA -> CASLFORMULA
codeFormula b :: Bool
b bsorts :: Set SORT
bsorts = Record () CASLFORMULA (TERM ()) -> CASLFORMULA -> CASLFORMULA
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Bool -> Set SORT -> (() -> ()) -> Record () CASLFORMULA (TERM ())
forall f.
TermExtension f =>
Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeRecord Bool
b Set SORT
bsorts ((() -> ()) -> Record () CASLFORMULA (TERM ()))
-> (() -> ()) -> Record () CASLFORMULA (TERM ())
forall a b. (a -> b) -> a -> b
$ String -> () -> ()
forall a. HasCallStack => String -> a
error "CASL2SubCFol")

codeTerm :: Bool -> Set.Set SORT -> TERM () -> TERM ()
codeTerm :: Bool -> Set SORT -> TERM () -> TERM ()
codeTerm b :: Bool
b bsorts :: Set SORT
bsorts = Record () CASLFORMULA (TERM ()) -> TERM () -> TERM ()
forall f a b. Record f a b -> TERM f -> b
foldTerm (Bool -> Set SORT -> (() -> ()) -> Record () CASLFORMULA (TERM ())
forall f.
TermExtension f =>
Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeRecord Bool
b Set SORT
bsorts ((() -> ()) -> Record () CASLFORMULA (TERM ()))
-> (() -> ()) -> Record () CASLFORMULA (TERM ())
forall a b. (a -> b) -> a -> b
$ String -> () -> ()
forall a. HasCallStack => String -> a
error "CASL2SubCFol")

-- | find sorts that need a bottom in membership formulas and casts

botSorts :: (f -> Set.Set SORT) -> Record f (Set.Set SORT) (Set.Set SORT)
botSorts :: (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
botSorts mf :: f -> Set SORT
mf = ((f -> Set SORT)
-> ([Set SORT] -> Set SORT)
-> Set SORT
-> Record f (Set SORT) (Set SORT)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord f -> Set SORT
mf [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set SORT
forall a. Set a
Set.empty)
     { foldMembership :: FORMULA f -> Set SORT -> SORT -> Range -> Set SORT
foldMembership = \ _ _ s :: SORT
s _ -> SORT -> Set SORT
forall a. a -> Set a
Set.singleton SORT
s
     , foldCast :: TERM f -> Set SORT -> SORT -> Range -> Set SORT
foldCast = \ _ _ s :: SORT
s _ -> SORT -> Set SORT
forall a. a -> Set a
Set.singleton SORT
s }

botFormulaSorts :: FORMULA f -> Set.Set SORT
botFormulaSorts :: FORMULA f -> Set SORT
botFormulaSorts = Record f (Set SORT) (Set SORT) -> FORMULA f -> Set SORT
forall f a b. Record f a b -> FORMULA f -> a
foldFormula ((f -> Set SORT) -> Record f (Set SORT) (Set SORT)
forall f. (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
botSorts ((f -> Set SORT) -> Record f (Set SORT) (Set SORT))
-> (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
forall a b. (a -> b) -> a -> b
$ Set SORT -> f -> Set SORT
forall a b. a -> b -> a
const Set SORT
forall a. Set a
Set.empty)

botTermSorts :: TERM f -> Set.Set SORT
botTermSorts :: TERM f -> Set SORT
botTermSorts = Record f (Set SORT) (Set SORT) -> TERM f -> Set SORT
forall f a b. Record f a b -> TERM f -> b
foldTerm ((f -> Set SORT) -> Record f (Set SORT) (Set SORT)
forall f. (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
botSorts ((f -> Set SORT) -> Record f (Set SORT) (Set SORT))
-> (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
forall a b. (a -> b) -> a -> b
$ Set SORT -> f -> Set SORT
forall a b. a -> b -> a
const Set SORT
forall a. Set a
Set.empty)