{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CFOL2IsabelleHOL.hs
Description :  embedding from CASL (CFOL) to Isabelle-HOL
Copyright   :  (c) Till Mossakowski and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

The embedding comorphism from CASL to Isabelle-HOL.
-}

module Comorphisms.CFOL2IsabelleHOL
    ( CFOL2IsabelleHOL (..)
    , transTheory
    , transVar
    , typeToks
    , mapSen
    , IsaTheory
    , SignTranslator
    , FormulaTranslator
    , getAssumpsToks
    , formTrCASL
    , quantifyIsa
    , quantify
    , transFORMULA
    , transSort
    , transRecord
    , transOpSymb
    ) where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.Morphism
import CASL.Quantification
import CASL.Fold
import CASL.Induction
import CASL.ToDoc

import Isabelle.IsaSign as IsaSign hiding (qname)
import Isabelle.IsaConsts
import Isabelle.Logic_Isabelle
import Isabelle.Translate

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.Utils
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List

-- | The identity of the comorphism
data CFOL2IsabelleHOL = CFOL2IsabelleHOL deriving Int -> CFOL2IsabelleHOL -> ShowS
[CFOL2IsabelleHOL] -> ShowS
CFOL2IsabelleHOL -> String
(Int -> CFOL2IsabelleHOL -> ShowS)
-> (CFOL2IsabelleHOL -> String)
-> ([CFOL2IsabelleHOL] -> ShowS)
-> Show CFOL2IsabelleHOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CFOL2IsabelleHOL] -> ShowS
$cshowList :: [CFOL2IsabelleHOL] -> ShowS
show :: CFOL2IsabelleHOL -> String
$cshow :: CFOL2IsabelleHOL -> String
showsPrec :: Int -> CFOL2IsabelleHOL -> ShowS
$cshowsPrec :: Int -> CFOL2IsabelleHOL -> ShowS
Show

-- Isabelle theories
type IsaTheory = (IsaSign.Sign, [Named IsaSign.Sentence])

-- extended signature translation
type SignTranslator f e = CASL.Sign.Sign f e -> e -> IsaTheory -> IsaTheory

-- extended signature translation for CASL
sigTrCASL :: SignTranslator () ()
sigTrCASL :: SignTranslator () ()
sigTrCASL _ _ = IsaTheory -> IsaTheory
forall a. a -> a
id

-- extended formula translation
type FormulaTranslator f e = CASL.Sign.Sign f e -> Set.Set String -> f -> Term

-- extended formula translation for CASL
formTrCASL :: FormulaTranslator () ()
formTrCASL :: FormulaTranslator () ()
formTrCASL _ _ = String -> () -> Term
forall a. HasCallStack => String -> a
error "CFOL2IsabelleHOL: No extended formulas allowed in CASL"

instance Language CFOL2IsabelleHOL where
  language_name :: CFOL2IsabelleHOL -> String
language_name CFOL2IsabelleHOL = "CASL2Isabelle"

instance Comorphism CFOL2IsabelleHOL
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               Isabelle () () IsaSign.Sentence () ()
               IsaSign.Sign
               IsabelleMorphism () () () where
    sourceLogic :: CFOL2IsabelleHOL -> CASL
sourceLogic CFOL2IsabelleHOL = CASL
CASL
    sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics
sourceSublogic CFOL2IsabelleHOL = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cFol
    targetLogic :: CFOL2IsabelleHOL -> Isabelle
targetLogic CFOL2IsabelleHOL = Isabelle
Isabelle
    mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe ()
mapSublogic cid :: CFOL2IsabelleHOL
cid sl :: CASL_Sublogics
sl = if CASL_Sublogics
sl CASL_Sublogics -> CASL_Sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` CFOL2IsabelleHOL -> CASL_Sublogics
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1
sourceSublogic CFOL2IsabelleHOL
cid
                       then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: CFOL2IsabelleHOL
-> (CASLSign, [Named CASLFORMULA]) -> Result IsaTheory
map_theory CFOL2IsabelleHOL = IsaTheory -> Result IsaTheory
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTheory -> Result IsaTheory)
-> ((CASLSign, [Named CASLFORMULA]) -> IsaTheory)
-> (CASLSign, [Named CASLFORMULA])
-> Result IsaTheory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignTranslator () ()
-> FormulaTranslator () ()
-> (CASLSign, [Named CASLFORMULA])
-> IsaTheory
forall f e.
FormExtension f =>
SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> IsaTheory
transTheory SignTranslator () ()
sigTrCASL FormulaTranslator () ()
formTrCASL
    map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence
map_sentence CFOL2IsabelleHOL sign :: CASLSign
sign =
      Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (CASLFORMULA -> Sentence) -> CASLFORMULA -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FormulaTranslator () ()
-> CASLSign -> Set String -> CASLFORMULA -> Sentence
forall f e.
FormulaTranslator f e
-> Sign f e -> Set String -> FORMULA f -> Sentence
mapSen FormulaTranslator () ()
formTrCASL CASLSign
sign (CASLSign -> Set String
forall f e. Sign f e -> Set String
typeToks CASLSign
sign)
    has_model_expansion :: CFOL2IsabelleHOL -> Bool
has_model_expansion CFOL2IsabelleHOL = Bool
True
    is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool
is_weakly_amalgamable CFOL2IsabelleHOL = Bool
True
    isInclusionComorphism :: CFOL2IsabelleHOL -> Bool
isInclusionComorphism CFOL2IsabelleHOL = Bool
True

-- -------------------------- Signature -----------------------------
baseSign :: BaseSig
baseSign :: BaseSig
baseSign = BaseSig
Main_thy

typeToks :: CASL.Sign.Sign f e -> Set.Set String
typeToks :: Sign f e -> Set String
typeToks = (Id -> String) -> Set Id -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Id -> BaseSig -> String
`showIsaTypeT` BaseSig
baseSign) (Set Id -> Set String)
-> (Sign f e -> Set Id) -> Sign f e -> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet

transTheory :: FormExtension f => SignTranslator f e ->
               FormulaTranslator f e ->
               (CASL.Sign.Sign f e, [Named (FORMULA f)])
                   -> IsaTheory
transTheory :: SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> IsaTheory
transTheory trSig :: SignTranslator f e
trSig trForm :: FormulaTranslator f e
trForm (sign :: Sign f e
sign, sens :: [Named (FORMULA f)]
sens) =
  SignTranslator f e
trSig Sign f e
sign (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
sign) (Sign
IsaSign.emptySign {
    baseSig :: BaseSig
baseSig = BaseSig
baseSign,
    tsig :: TypeSig
tsig = TypeSig
emptyTypeSig {arities :: Arities
arities =
               (Id -> Arities -> Arities) -> Arities -> Set Id -> Arities
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ s :: Id
s -> let s1 :: String
s1 = Id -> BaseSig -> String
showIsaTypeT Id
s BaseSig
baseSign in
                                 String -> [(IsaClass, [(Typ, Sort)])] -> Arities -> Arities
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s1 [(IsaClass
isaTerm, [])])
                               Arities
forall k a. Map k a
Map.empty (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sign)},
    constTab :: ConstTab
constTab = (Id -> Set PredType -> ConstTab -> ConstTab)
-> ConstTab -> Map Id (Set PredType) -> ConstTab
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id -> Set PredType -> ConstTab -> ConstTab
insertPreds
                ((Id -> Set OpType -> ConstTab -> ConstTab)
-> ConstTab -> Map Id (Set OpType) -> ConstTab
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id -> Set OpType -> ConstTab -> ConstTab
insertOps ConstTab
forall k a. Map k a
Map.empty
                 (Map Id (Set OpType) -> ConstTab)
-> (MapSet Id OpType -> Map Id (Set OpType))
-> MapSet Id OpType
-> ConstTab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id OpType -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id OpType -> ConstTab) -> MapSet Id OpType -> ConstTab
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sign) (Map Id (Set PredType) -> ConstTab)
-> (MapSet Id PredType -> Map Id (Set PredType))
-> MapSet Id PredType
-> ConstTab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id PredType -> ConstTab) -> MapSet Id PredType -> ConstTab
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sign,
    domainTab :: DomainTab
domainTab = DomainTab
dtDefs},
         ((FORMULA f, Int) -> SenAttr Sentence String)
-> [(FORMULA f, Int)] -> [SenAttr Sentence String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: FORMULA f
s, n :: Int
n) -> String -> Sentence -> SenAttr Sentence String
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_induction_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) (Sentence -> SenAttr Sentence String)
-> Sentence -> SenAttr Sentence String
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Sentence
myMapSen FORMULA f
s)
              ([FORMULA f] -> [(FORMULA f, Int)]
forall a. [a] -> [(a, Int)]
number [FORMULA f]
gens) [SenAttr Sentence String]
-> [SenAttr Sentence String] -> [SenAttr Sentence String]
forall a. [a] -> [a] -> [a]
++
         (Named (FORMULA f) -> SenAttr Sentence String)
-> [Named (FORMULA f)] -> [SenAttr Sentence String]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> Sentence)
-> Named (FORMULA f) -> SenAttr Sentence String
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed FORMULA f -> Sentence
myMapSen) [Named (FORMULA f)]
real_sens)
     -- for now, no new sentences
  where
    gens :: [FORMULA f]
gens =
        (([Constraint], Bool) -> FORMULA f)
-> [([Constraint], Bool)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map ([Constraint] -> FORMULA f
forall f. FormExtension f => [Constraint] -> FORMULA f
inductionScheme ([Constraint] -> FORMULA f)
-> (([Constraint], Bool) -> [Constraint])
-> ([Constraint], Bool)
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint], Bool) -> [Constraint]
forall a b. (a, b) -> a
fst) [([Constraint], Bool)]
genTypes
    tyToks :: Set String
tyToks = Sign f e -> Set String
forall f e. Sign f e -> Set String
typeToks Sign f e
sign
    myMapSen :: FORMULA f -> Sentence
myMapSen = Term -> Sentence
mkSen (Term -> Sentence) -> (FORMULA f -> Term) -> FORMULA f -> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> FORMULA f
-> Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> FORMULA f
-> Term
transFORMULA Sign f e
sign Set String
tyToks FormulaTranslator f e
trForm (Sign f e -> Set String
forall f e. Sign f e -> Set String
getAssumpsToks Sign f e
sign)
    (real_sens :: [Named (FORMULA f)]
real_sens, sort_gen_axs :: [([Constraint], Bool)]
sort_gen_axs) = (Named (FORMULA f)
 -> ([Named (FORMULA f)], [([Constraint], Bool)])
 -> ([Named (FORMULA f)], [([Constraint], Bool)]))
-> ([Named (FORMULA f)], [([Constraint], Bool)])
-> [Named (FORMULA f)]
-> ([Named (FORMULA f)], [([Constraint], Bool)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ s :: Named (FORMULA f)
s (rs :: [Named (FORMULA f)]
rs, cs :: [([Constraint], Bool)]
cs) -> case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
s of
                Sort_gen_ax c :: [Constraint]
c b :: Bool
b -> ([Named (FORMULA f)]
rs, ([Constraint]
c, Bool
b) ([Constraint], Bool)
-> [([Constraint], Bool)] -> [([Constraint], Bool)]
forall a. a -> [a] -> [a]
: [([Constraint], Bool)]
cs)
                _ -> (Named (FORMULA f)
s Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: [Named (FORMULA f)]
rs, [([Constraint], Bool)]
cs)) ([], []) [Named (FORMULA f)]
sens
    unique_sort_gen_axs :: [([Constraint], Bool)]
unique_sort_gen_axs = (([Constraint], Bool) -> Set Id)
-> [([Constraint], Bool)] -> [([Constraint], Bool)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn ([Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id)
-> (([Constraint], Bool) -> [Id]) -> ([Constraint], Bool) -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint -> Id) -> [Constraint] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Id
newSort ([Constraint] -> [Id])
-> (([Constraint], Bool) -> [Constraint])
-> ([Constraint], Bool)
-> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint], Bool) -> [Constraint]
forall a b. (a, b) -> a
fst)
                          [([Constraint], Bool)]
sort_gen_axs
    (freeTypes :: [([Constraint], Bool)]
freeTypes, genTypes :: [([Constraint], Bool)]
genTypes) = (([Constraint], Bool) -> Bool)
-> [([Constraint], Bool)]
-> ([([Constraint], Bool)], [([Constraint], Bool)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ([Constraint], Bool) -> Bool
forall a b. (a, b) -> b
snd [([Constraint], Bool)]
unique_sort_gen_axs
    dtDefs :: DomainTab
dtDefs = Sign f e -> Set String -> [[Constraint]] -> DomainTab
forall f e. Sign f e -> Set String -> [[Constraint]] -> DomainTab
makeDtDefs Sign f e
sign Set String
tyToks ([[Constraint]] -> DomainTab) -> [[Constraint]] -> DomainTab
forall a b. (a -> b) -> a -> b
$ (([Constraint], Bool) -> [Constraint])
-> [([Constraint], Bool)] -> [[Constraint]]
forall a b. (a -> b) -> [a] -> [b]
map ([Constraint], Bool) -> [Constraint]
forall a b. (a, b) -> a
fst [([Constraint], Bool)]
freeTypes
    ga :: GlobalAnnos
ga = Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign
    insertOps :: Id -> Set OpType -> ConstTab -> ConstTab
insertOps op :: Id
op ts :: Set OpType
ts m :: ConstTab
m = if Set OpType -> Bool
forall a. Set a -> Bool
isSingleton Set OpType
ts then
      let t :: OpType
t = Set OpType -> OpType
forall a. Set a -> a
Set.findMin Set OpType
ts in VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
              (Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
False GlobalAnnos
ga ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
t) Id
op BaseSig
baseSign Set String
tyToks)
              (OpType -> Typ
transOpType OpType
t) ConstTab
m
      else (ConstTab -> (OpType, Int) -> ConstTab)
-> ConstTab -> [(OpType, Int)] -> ConstTab
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m1 :: ConstTab
m1 (t :: OpType
t, i :: Int
i) -> VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
             (Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT Bool
False GlobalAnnos
ga ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
t) Id
op Int
i BaseSig
baseSign Set String
tyToks)
             (OpType -> Typ
transOpType OpType
t) ConstTab
m1) ConstTab
m ([(OpType, Int)] -> ConstTab) -> [(OpType, Int)] -> ConstTab
forall a b. (a -> b) -> a -> b
$ [OpType] -> [(OpType, Int)]
forall a. [a] -> [(a, Int)]
number ([OpType] -> [(OpType, Int)]) -> [OpType] -> [(OpType, Int)]
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
ts
    insertPreds :: Id -> Set PredType -> ConstTab -> ConstTab
insertPreds pre :: Id
pre ts :: Set PredType
ts m :: ConstTab
m = if Set PredType -> Bool
forall a. Set a -> Bool
isSingleton Set PredType
ts then
      let t :: PredType
t = Set PredType -> PredType
forall a. Set a -> a
Set.findMin Set PredType
ts in VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
              (Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
True GlobalAnnos
ga ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
t) Id
pre BaseSig
baseSign Set String
tyToks)
              (PredType -> Typ
transPredType PredType
t) ConstTab
m
      else (ConstTab -> (PredType, Int) -> ConstTab)
-> ConstTab -> [(PredType, Int)] -> ConstTab
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m1 :: ConstTab
m1 (t :: PredType
t, i :: Int
i) -> VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
             (Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT Bool
True GlobalAnnos
ga ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
t) Id
pre Int
i BaseSig
baseSign Set String
tyToks)
             (PredType -> Typ
transPredType PredType
t) ConstTab
m1) ConstTab
m ([(PredType, Int)] -> ConstTab) -> [(PredType, Int)] -> ConstTab
forall a b. (a -> b) -> a -> b
$ [PredType] -> [(PredType, Int)]
forall a. [a] -> [(a, Int)]
number ([PredType] -> [(PredType, Int)])
-> [PredType] -> [(PredType, Int)]
forall a b. (a -> b) -> a -> b
$ Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
ts

makeDtDefs :: CASL.Sign.Sign f e -> Set.Set String -> [[Constraint]]
           -> [[(Typ, [(VName, [Typ])])]]
makeDtDefs :: Sign f e -> Set String -> [[Constraint]] -> DomainTab
makeDtDefs sign :: Sign f e
sign = ([Constraint] -> [(Typ, [(VName, [Typ])])])
-> [[Constraint]] -> DomainTab
forall a b. (a -> b) -> [a] -> [b]
map (([Constraint] -> [(Typ, [(VName, [Typ])])])
 -> [[Constraint]] -> DomainTab)
-> (Set String -> [Constraint] -> [(Typ, [(VName, [Typ])])])
-> Set String
-> [[Constraint]]
-> DomainTab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> Set String -> [Constraint] -> [(Typ, [(VName, [Typ])])]
forall f e.
Sign f e -> Set String -> [Constraint] -> [(Typ, [(VName, [Typ])])]
makeDtDef Sign f e
sign

makeDtDef :: CASL.Sign.Sign f e -> Set.Set String -> [Constraint]
          -> [(Typ, [(VName, [Typ])])]
makeDtDef :: Sign f e -> Set String -> [Constraint] -> [(Typ, [(VName, [Typ])])]
makeDtDef sign :: Sign f e
sign tyToks :: Set String
tyToks constrs :: [Constraint]
constrs = (Id -> (Typ, [(VName, [Typ])]))
-> [Id] -> [(Typ, [(VName, [Typ])])]
forall a b. (a -> b) -> [a] -> [b]
map Id -> (Typ, [(VName, [Typ])])
makeDt [Id]
srts where
    (srts :: [Id]
srts, ops :: [OP_SYMB]
ops, _maps :: [(Id, Id)]
_maps) = [Constraint] -> ([Id], [OP_SYMB], [(Id, Id)])
recover_Sort_gen_ax [Constraint]
constrs
    makeDt :: Id -> (Typ, [(VName, [Typ])])
makeDt s :: Id
s = (Id -> Typ
transSort Id
s, (OP_SYMB -> (VName, [Typ])) -> [OP_SYMB] -> [(VName, [Typ])]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> (VName, [Typ])
makeOp ((OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter (Id -> OP_SYMB -> Bool
hasTheSort Id
s) [OP_SYMB]
ops))
    makeOp :: OP_SYMB -> (VName, [Typ])
makeOp opSym :: OP_SYMB
opSym = (Sign f e -> Set String -> OP_SYMB -> VName
forall f e. Sign f e -> Set String -> OP_SYMB -> VName
transOpSymb Sign f e
sign Set String
tyToks OP_SYMB
opSym, OP_SYMB -> [Typ]
transArgs OP_SYMB
opSym)
    hasTheSort :: Id -> OP_SYMB -> Bool
hasTheSort s :: Id
s (Qual_op_name _ ot :: OP_TYPE
ot _) = Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== OP_TYPE -> Id
res_OP_TYPE OP_TYPE
ot
    hasTheSort _ _ = String -> Bool
forall a. HasCallStack => String -> a
error "CFOL2IsabelleHOL.hasTheSort"
    transArgs :: OP_SYMB -> [Typ]
transArgs (Qual_op_name _ ot :: OP_TYPE
ot _) = (Id -> Typ) -> [Id] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Typ
transSort ([Id] -> [Typ]) -> [Id] -> [Typ]
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [Id]
args_OP_TYPE OP_TYPE
ot
    transArgs _ = String -> [Typ]
forall a. HasCallStack => String -> a
error "CFOL2IsabelleHOL.transArgs"

transSort :: SORT -> Typ
transSort :: Id -> Typ
transSort s :: Id
s = String -> Sort -> [Typ] -> Typ
Type (Id -> BaseSig -> String
showIsaTypeT Id
s BaseSig
baseSign) [] []

transOpType :: OpType -> Typ
transOpType :: OpType -> Typ
transOpType ot :: OpType
ot = [Typ] -> Typ -> Typ
mkCurryFunType ((Id -> Typ) -> [Id] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Typ
transSort ([Id] -> [Typ]) -> [Id] -> [Typ]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
ot)
                 (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ Id -> Typ
transSort (OpType -> Id
opRes OpType
ot)

transPredType :: PredType -> Typ
transPredType :: PredType -> Typ
transPredType pt :: PredType
pt = [Typ] -> Typ -> Typ
mkCurryFunType ((Id -> Typ) -> [Id] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Typ
transSort ([Id] -> [Typ]) -> [Id] -> [Typ]
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
pt) Typ
boolType

-- ---------------------------- Formulas ------------------------------

getAssumpsToks :: CASL.Sign.Sign f e -> Set.Set String
getAssumpsToks :: Sign f e -> Set String
getAssumpsToks sign :: Sign f e
sign = (Id -> Set OpType -> Set String -> Set String)
-> Set String -> Map Id (Set OpType) -> Set String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i ops :: Set OpType
ops s :: Set String
s ->
    Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set String
s (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ [Set String] -> Set String
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
        ([Set String] -> Set String) -> [Set String] -> Set String
forall a b. (a -> b) -> a -> b
$ ((OpType, Int) -> Set String) -> [(OpType, Int)] -> [Set String]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, o :: Int
o) -> Id -> Int -> BaseSig -> Set String
getConstIsaToks Id
i Int
o BaseSig
baseSign)
              ([(OpType, Int)] -> [Set String])
-> [(OpType, Int)] -> [Set String]
forall a b. (a -> b) -> a -> b
$ [OpType] -> [(OpType, Int)]
forall a. [a] -> [(a, Int)]
number ([OpType] -> [(OpType, Int)]) -> [OpType] -> [(OpType, Int)]
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
ops)
    ((Id -> Set PredType -> Set String -> Set String)
-> Set String -> Map Id (Set PredType) -> Set String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ( \ i :: Id
i prds :: Set PredType
prds s :: Set String
s ->
    Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set String
s (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ [Set String] -> Set String
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
        ([Set String] -> Set String) -> [Set String] -> Set String
forall a b. (a -> b) -> a -> b
$ ((PredType, Int) -> Set String)
-> [(PredType, Int)] -> [Set String]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (_, o :: Int
o) -> Id -> Int -> BaseSig -> Set String
getConstIsaToks Id
i Int
o BaseSig
baseSign)
              ([(PredType, Int)] -> [Set String])
-> [(PredType, Int)] -> [Set String]
forall a b. (a -> b) -> a -> b
$ [PredType] -> [(PredType, Int)]
forall a. [a] -> [(a, Int)]
number ([PredType] -> [(PredType, Int)])
-> [PredType] -> [(PredType, Int)]
forall a b. (a -> b) -> a -> b
$ Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
prds) Set String
forall a. Set a
Set.empty (Map Id (Set PredType) -> Set String)
-> (MapSet Id PredType -> Map Id (Set PredType))
-> MapSet Id PredType
-> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap
    (MapSet Id PredType -> Set String)
-> MapSet Id PredType -> Set String
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sign)
    (Map Id (Set OpType) -> Set String)
-> (MapSet Id OpType -> Map Id (Set OpType))
-> MapSet Id OpType
-> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id OpType -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id OpType -> Set String) -> MapSet Id OpType -> Set String
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sign

transVar :: Set.Set String -> VAR -> String
transVar :: Set String -> VAR -> String
transVar toks :: Set String
toks v :: VAR
v = let
    s :: String
s = Id -> BaseSig -> String
showIsaConstT (VAR -> Id
simpleIdToId VAR
v) BaseSig
baseSign
    renVar :: ShowS
renVar t :: String
t = if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
t Set String
toks then ShowS
renVar ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "X_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t else String
t
    in ShowS
renVar String
s

quantifyIsa :: String -> (String, Typ) -> Term -> Term
quantifyIsa :: String -> (String, Typ) -> Term -> Term
quantifyIsa q :: String
q (v :: String
v, _) phi :: Term
phi =
  Term -> Term -> Term
termAppl (String -> Term
conDouble String
q) (Term -> Term -> Continuity -> Term
Abs (String -> Term
mkFree String
v) Term
phi Continuity
NotCont)

quantify :: Set.Set String -> QUANTIFIER -> (VAR, SORT) -> Term -> Term
quantify :: Set String -> QUANTIFIER -> (VAR, Id) -> Term -> Term
quantify toks :: Set String
toks q :: QUANTIFIER
q (v :: VAR
v, t :: Id
t) =
  String -> (String, Typ) -> Term -> Term
quantifyIsa (QUANTIFIER -> String
qname QUANTIFIER
q) (Set String -> VAR -> String
transVar Set String
toks VAR
v, Id -> Typ
transSort Id
t)
  where
  qname :: QUANTIFIER -> String
qname Universal = String
allS
  qname Existential = String
exS
  qname Unique_existential = String
ex1S

transOpSymb :: CASL.Sign.Sign f e -> Set.Set String -> OP_SYMB -> VName
transOpSymb :: Sign f e -> Set String -> OP_SYMB -> VName
transOpSymb sign :: Sign f e
sign tyToks :: Set String
tyToks qo :: OP_SYMB
qo = case OP_SYMB
qo of
 Qual_op_name op :: Id
op ot :: OP_TYPE
ot _ -> let
  ga :: GlobalAnnos
ga = Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign
  l :: Int
l = [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [Id]
args_OP_TYPE OP_TYPE
ot
  in case Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList (Set OpType -> [OpType])
-> (MapSet Id OpType -> Set OpType) -> MapSet Id OpType -> [OpType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> MapSet Id OpType -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
op (MapSet Id OpType -> [OpType]) -> MapSet Id OpType -> [OpType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sign of
    [] -> String -> VName
forall a. HasCallStack => String -> a
error (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ "CASL2Isabelle unknown op: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
op
    [_] -> Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
False GlobalAnnos
ga Int
l Id
op BaseSig
baseSign Set String
tyToks
    ots :: [OpType]
ots -> case OpType -> [OpType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (OP_TYPE -> OpType
toOpType OP_TYPE
ot) [OpType]
ots of
      Just i :: Int
i -> Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT Bool
False GlobalAnnos
ga Int
l Id
op (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) BaseSig
baseSign Set String
tyToks
      Nothing -> String -> VName
forall a. HasCallStack => String -> a
error (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ "CASL2Isabelle unknown type for op: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
op
 Op_name op :: Id
op -> String -> VName
forall a. HasCallStack => String -> a
error (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ "CASL2Isabelle: unqualified op: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
op

transPredSymb :: CASL.Sign.Sign f e -> Set.Set String -> PRED_SYMB -> VName
transPredSymb :: Sign f e -> Set String -> PRED_SYMB -> VName
transPredSymb sign :: Sign f e
sign tyToks :: Set String
tyToks qp :: PRED_SYMB
qp =
 let ga :: GlobalAnnos
ga = Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign
     d :: VName
d = Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
True GlobalAnnos
ga (-1) (PRED_SYMB -> Id
predSymbName PRED_SYMB
qp) BaseSig
baseSign Set String
tyToks
             -- for predicate names in induction schemes
 in case PRED_SYMB
qp of
 Qual_pred_name p :: Id
p pt :: PRED_TYPE
pt@(Pred_type args :: [Id]
args _) _ -> let
  l :: Int
l = [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args
  in case Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList (Set PredType -> [PredType])
-> (MapSet Id PredType -> Set PredType)
-> MapSet Id PredType
-> [PredType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> MapSet Id PredType -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
p (MapSet Id PredType -> [PredType])
-> MapSet Id PredType -> [PredType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sign of
    [] -> VName
d
    [_] -> Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT Bool
True GlobalAnnos
ga Int
l Id
p BaseSig
baseSign Set String
tyToks
    pts :: [PredType]
pts -> case PredType -> [PredType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex (PRED_TYPE -> PredType
toPredType PRED_TYPE
pt) [PredType]
pts of
      Just i :: Int
i -> Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT Bool
True GlobalAnnos
ga Int
l Id
p (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) BaseSig
baseSign Set String
tyToks
      Nothing -> VName
d
 Pred_name _ -> VName
d

mapSen :: FormulaTranslator f e -> CASL.Sign.Sign f e -> Set.Set String
       -> FORMULA f -> Sentence
mapSen :: FormulaTranslator f e
-> Sign f e -> Set String -> FORMULA f -> Sentence
mapSen trForm :: FormulaTranslator f e
trForm sign :: Sign f e
sign tyToks :: Set String
tyToks =
    Term -> Sentence
mkSen (Term -> Sentence) -> (FORMULA f -> Term) -> FORMULA f -> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> FORMULA f
-> Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> FORMULA f
-> Term
transFORMULA Sign f e
sign Set String
tyToks FormulaTranslator f e
trForm (Sign f e -> Set String
forall f e. Sign f e -> Set String
getAssumpsToks Sign f e
sign)

transRecord :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e
            -> Set.Set String -> Record f Term Term
transRecord :: Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
transRecord sign :: Sign f e
sign tyToks :: Set String
tyToks tr :: FormulaTranslator f e
tr toks :: Set String
toks = Record :: forall f a b.
(FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a)
-> (FORMULA f -> Junctor -> [a] -> Range -> a)
-> (FORMULA f -> a -> Relation -> a -> Range -> a)
-> (FORMULA f -> a -> Range -> a)
-> (FORMULA f -> Bool -> Range -> a)
-> (FORMULA f -> PRED_SYMB -> [b] -> Range -> a)
-> (FORMULA f -> b -> Range -> a)
-> (FORMULA f -> b -> Equality -> b -> Range -> a)
-> (FORMULA f -> b -> Id -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> Id -> OP_TYPE -> a -> a)
-> (FORMULA f -> Id -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> VAR -> Id -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> Id -> Range -> b)
-> (TERM f -> b -> Id -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> VAR -> b)
-> (TERM f -> Id -> Range -> b)
-> (TERM f -> Id -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> f -> b)
-> Record f a b
Record
    { foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> Term -> Range -> Term
foldQuantification = \ _ qu :: QUANTIFIER
qu vdecl :: [VAR_DECL]
vdecl phi :: Term
phi _ ->
          ((VAR, Id) -> Term -> Term) -> Term -> [(VAR, Id)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set String -> QUANTIFIER -> (VAR, Id) -> Term -> Term
quantify Set String
toks QUANTIFIER
qu) Term
phi ([VAR_DECL] -> [(VAR, Id)]
flatVAR_DECLs [VAR_DECL]
vdecl)
    , foldJunction :: FORMULA f -> Junctor -> [Term] -> Range -> Term
foldJunction = \ _ j :: Junctor
j phis :: [Term]
phis _ -> let
          (n :: Term
n, op :: Term -> Term -> Term
op) = case Junctor
j of
              Con -> (Term
true, Term -> Term -> Term
binConj)
              Dis -> (Term
false, Term -> Term -> Term
binDisj)
          in if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
phis then Term
n else (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
op [Term]
phis
    , foldRelation :: FORMULA f -> Term -> Relation -> Term -> Range -> Term
foldRelation = \ _ phi1 :: Term
phi1 c :: Relation
c phi2 :: Term
phi2 _ -> (if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence
         then Term -> Term -> Term
binEqv else Term -> Term -> Term
binImpl) Term
phi1 Term
phi2
    , foldNegation :: FORMULA f -> Term -> Range -> Term
foldNegation = \ _ phi :: Term
phi _ -> Term -> Term -> Term
termAppl Term
notOp Term
phi
    , foldAtom :: FORMULA f -> Bool -> Range -> Term
foldAtom = \ _ b :: Bool
b _ -> if Bool
b then Term
true else Term
false
    , foldPredication :: FORMULA f -> PRED_SYMB -> [Term] -> Range -> Term
foldPredication = \ _ psymb :: PRED_SYMB
psymb args :: [Term]
args _ ->
          (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
termAppl (VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set String -> PRED_SYMB -> VName
forall f e. Sign f e -> Set String -> PRED_SYMB -> VName
transPredSymb Sign f e
sign Set String
tyToks PRED_SYMB
psymb) [Term]
args
    , foldDefinedness :: FORMULA f -> Term -> Range -> Term
foldDefinedness = \ _ _ _ -> Term
true -- totality assumed
    , foldEquation :: FORMULA f -> Term -> Equality -> Term -> Range -> Term
foldEquation = \ _ t1 :: Term
t1 _ t2 :: Term
t2 _ -> Term -> Term -> Term
binEq Term
t1 Term
t2 -- equal types assumed
    , foldMembership :: FORMULA f -> Term -> Id -> Range -> Term
foldMembership = \ _ _ _ _ -> Term
true -- no subsorting assumed
    , foldMixfix_formula :: FORMULA f -> Term -> Term
foldMixfix_formula = String -> FORMULA f -> Term -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_formula"
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> Term
foldSort_gen_ax = String -> FORMULA f -> [Constraint] -> Bool -> Term
forall a. HasCallStack => String -> a
error "transRecord: Sort_gen_ax"
    , foldQuantOp :: FORMULA f -> Id -> OP_TYPE -> Term -> Term
foldQuantOp = String -> FORMULA f -> Id -> OP_TYPE -> Term -> Term
forall a. HasCallStack => String -> a
error "transRecord: QuantOp"
    , foldQuantPred :: FORMULA f -> Id -> PRED_TYPE -> Term -> Term
foldQuantPred = String -> FORMULA f -> Id -> PRED_TYPE -> Term -> Term
forall a. HasCallStack => String -> a
error "transRecord: QuantPred"
    , foldExtFORMULA :: FORMULA f -> f -> Term
foldExtFORMULA = \ _ -> FormulaTranslator f e
tr Sign f e
sign Set String
tyToks
    , foldQual_var :: TERM f -> VAR -> Id -> Range -> Term
foldQual_var = \ _ v :: VAR
v _ _ -> String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Set String -> VAR -> String
transVar Set String
toks VAR
v
    , foldApplication :: TERM f -> OP_SYMB -> [Term] -> Range -> Term
foldApplication = \ _ opsymb :: OP_SYMB
opsymb args :: [Term]
args _ ->
          (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
termAppl (VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set String -> OP_SYMB -> VName
forall f e. Sign f e -> Set String -> OP_SYMB -> VName
transOpSymb Sign f e
sign Set String
tyToks OP_SYMB
opsymb) [Term]
args
    , foldSorted_term :: TERM f -> Term -> Id -> Range -> Term
foldSorted_term = \ _ t :: Term
t _ _ -> Term
t -- no subsorting assumed
    , foldCast :: TERM f -> Term -> Id -> Range -> Term
foldCast = \ _ t :: Term
t _ _ -> Term
t -- no subsorting assumed
    , foldConditional :: TERM f -> Term -> Term -> Term -> Range -> Term
foldConditional = \ _ t1 :: Term
t1 phi :: Term
phi t2 :: Term
t2 _ -> -- equal types assumed
          Term -> Term -> Term -> Continuity -> Term
If Term
phi Term
t1 Term
t2 Continuity
NotCont
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> Term
foldMixfix_qual_pred = String -> TERM f -> PRED_SYMB -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_qual_pred"
    , foldMixfix_term :: TERM f -> [Term] -> Term
foldMixfix_term = String -> TERM f -> [Term] -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_term"
    , foldMixfix_token :: TERM f -> VAR -> Term
foldMixfix_token = String -> TERM f -> VAR -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_token"
    , foldMixfix_sorted_term :: TERM f -> Id -> Range -> Term
foldMixfix_sorted_term = String -> TERM f -> Id -> Range -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_sorted_term"
    , foldMixfix_cast :: TERM f -> Id -> Range -> Term
foldMixfix_cast = String -> TERM f -> Id -> Range -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_cast"
    , foldMixfix_parenthesized :: TERM f -> [Term] -> Range -> Term
foldMixfix_parenthesized = String -> TERM f -> [Term] -> Range -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_parenthesized"
    , foldMixfix_bracketed :: TERM f -> [Term] -> Range -> Term
foldMixfix_bracketed = String -> TERM f -> [Term] -> Range -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_bracketed"
    , foldMixfix_braced :: TERM f -> [Term] -> Range -> Term
foldMixfix_braced = String -> TERM f -> [Term] -> Range -> Term
forall a. HasCallStack => String -> a
error "transRecord: Mixfix_braced"
    , foldExtTERM :: TERM f -> f -> Term
foldExtTERM = String -> TERM f -> f -> Term
forall a. HasCallStack => String -> a
error "transRecord: ExtTERM"
    }

transFORMULA :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e
             -> Set.Set String -> FORMULA f -> Term
transFORMULA :: Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> FORMULA f
-> Term
transFORMULA sign :: Sign f e
sign tyToks :: Set String
tyToks tr :: FormulaTranslator f e
tr = Record f Term Term -> FORMULA f -> Term
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f Term Term -> FORMULA f -> Term)
-> (Set String -> Record f Term Term)
-> Set String
-> FORMULA f
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
transRecord Sign f e
sign Set String
tyToks FormulaTranslator f e
tr