{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL_DL2CASL.hs
Description :  Inclusion of CASL_DL into CASL
Copyright   :  (c) Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via Logic.Logic)

-}

module Comorphisms.CASL_DL2CASL
    (
     CASL_DL2CASL (..)
    )
    where

import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.ProofTree
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Control.Monad.Fail as Fail

-- CASL_DL = domain
import CASL_DL.PredefinedCASLAxioms
import CASL_DL.Logic_CASL_DL
import CASL_DL.AS_CASL_DL
import CASL_DL.Sign ()
import CASL_DL.StatAna -- DLSign
import CASL_DL.Sublogics

-- CASL = codomain
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic as Sublogic

import qualified Data.Set as Set

data CASL_DL2CASL = CASL_DL2CASL deriving Int -> CASL_DL2CASL -> ShowS
[CASL_DL2CASL] -> ShowS
CASL_DL2CASL -> String
(Int -> CASL_DL2CASL -> ShowS)
-> (CASL_DL2CASL -> String)
-> ([CASL_DL2CASL] -> ShowS)
-> Show CASL_DL2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL_DL2CASL] -> ShowS
$cshowList :: [CASL_DL2CASL] -> ShowS
show :: CASL_DL2CASL -> String
$cshow :: CASL_DL2CASL -> String
showsPrec :: Int -> CASL_DL2CASL -> ShowS
$cshowsPrec :: Int -> CASL_DL2CASL -> ShowS
Show

instance Language CASL_DL2CASL

instance Comorphism
    CASL_DL2CASL    -- comorphism
    CASL_DL         -- lid domain
    CASL_DL_SL      -- sublogics domain
    DL_BASIC_SPEC   -- Basic spec domain
    DLFORMULA       -- sentence domain
    SYMB_ITEMS      -- symbol items domain
    SYMB_MAP_ITEMS  -- symbol map items domain
    DLSign          -- signature domain
    DLMor           -- morphism domain
    Symbol          -- symbol domain
    RawSymbol       -- rawsymbol domain
    ProofTree     -- proof tree codomain
    CASL            -- lid codomain
    CASL_Sublogics  -- sublogics codomain
    CASLBasicSpec   -- Basic spec codomain
    CASLFORMULA     -- sentence codomain
    SYMB_ITEMS      -- symbol items codomain
    SYMB_MAP_ITEMS  -- symbol map items codomain
    CASLSign        -- signature codomain
    CASLMor         -- morphism codomain
    Symbol          -- symbol codomain
    RawSymbol       -- rawsymbol codomain
    ProofTree     -- proof tree domain
    where
      sourceLogic :: CASL_DL2CASL -> CASL_DL
sourceLogic CASL_DL2CASL = CASL_DL
CASL_DL
      targetLogic :: CASL_DL2CASL -> CASL
targetLogic CASL_DL2CASL = CASL
CASL
      sourceSublogic :: CASL_DL2CASL -> CASL_DL_SL
sourceSublogic CASL_DL2CASL = CASL_DL_SL
SROIQ
      mapSublogic :: CASL_DL2CASL -> CASL_DL_SL -> Maybe CASL_Sublogics
mapSublogic CASL_DL2CASL _ = 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
$ CASL_Sublogics
forall a. Lattice a => CASL_SL a
Sublogic.caslTop
                      { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
                      , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
emptyMapConsFeature }
      map_symbol :: CASL_DL2CASL -> DLSign -> Symbol -> Set Symbol
map_symbol CASL_DL2CASL _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton
      map_sentence :: CASL_DL2CASL -> DLSign -> DLFORMULA -> Result CASLFORMULA
map_sentence CASL_DL2CASL = DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence
      map_morphism :: CASL_DL2CASL -> DLMor -> Result CASLMor
map_morphism CASL_DL2CASL = DLMor -> Result CASLMor
mapMor
      map_theory :: CASL_DL2CASL
-> (DLSign, [Named DLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory CASL_DL2CASL = (DLSign, [Named DLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
trTheory
      isInclusionComorphism :: CASL_DL2CASL -> Bool
isInclusionComorphism CASL_DL2CASL = Bool
True
      has_model_expansion :: CASL_DL2CASL -> Bool
has_model_expansion CASL_DL2CASL = Bool
True

{- | mapping of morphims, we just forget the
additional features -}
mapMor :: DLMor -> Result CASLMor
mapMor :: DLMor -> Result CASLMor
mapMor inMor :: DLMor
inMor =
    let
        ms :: CASLSign
ms = DLSign -> CASLSign
trSign (DLSign -> CASLSign) -> DLSign -> CASLSign
forall a b. (a -> b) -> a -> b
$ DLMor -> DLSign
forall f e m. Morphism f e m -> Sign f e
msource DLMor
inMor
        mt :: CASLSign
mt = DLSign -> CASLSign
trSign (DLSign -> CASLSign) -> DLSign -> CASLSign
forall a b. (a -> b) -> a -> b
$ DLMor -> DLSign
forall f e m. Morphism f e m -> Sign f e
mtarget DLMor
inMor
        sm :: Sort_map
sm = DLMor -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map DLMor
inMor
        fm :: Op_map
fm = DLMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map DLMor
inMor
        pm :: Pred_map
pm = DLMor -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map DLMor
inMor
    in CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism () CASLSign
ms CASLSign
mt)
        { sort_map :: Sort_map
sort_map = Sort_map
sm
        , op_map :: Op_map
op_map = Op_map
fm
        , pred_map :: Pred_map
pred_map = Pred_map
pm }

-- | we forget additional information in the signature
projectToCASL :: DLSign -> CASLSign
projectToCASL :: DLSign -> CASLSign
projectToCASL dls :: DLSign
dls = DLSign
dls
                    {
                      sentences :: [Named CASLFORMULA]
sentences = []
                    , extendedInfo :: ()
extendedInfo = ()
                    }

{- | Thing is established as the TopSort of all sorts
defined in the CASL_DL spec, a predefined signature
is added -}
trSign :: DLSign -> CASLSign
trSign :: DLSign -> CASLSign
trSign inSig :: DLSign
inSig =
    let
        inC :: CASLSign
inC = DLSign -> CASLSign
projectToCASL DLSign
inSig CASLSign -> CASLSign -> CASLSign
`uniteCASLSign` CASLSign
predefSign
        inSorts :: Set SORT
inSorts = DLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet DLSign
inSig
        inData :: Set SORT
inData = CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
predefSign
    in
      CASLSign
inC
      {
        sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
thing
          (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
dataS
          (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> Set SORT -> Rel SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
`Rel.insertDiffPair` SORT
dataS)
                  ((SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> Set SORT -> Rel SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
`Rel.insertDiffPair` SORT
thing)
                   (CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CASLSign
inC) Set SORT
inSorts)
          (Set SORT -> Rel SORT) -> Set SORT -> Rel 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
dataS Set SORT
inData
      }

-- * translation of the signature predefined axioms are added

-- | Translation of theories
trTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->
            Result (CASLSign, [Named (FORMULA ())])
trTheory :: (DLSign, [Named DLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
trTheory (inSig :: DLSign
inSig, inForms :: [Named DLFORMULA]
inForms) = do
      [Named CASLFORMULA]
outForms <- (Named DLFORMULA -> Result (Named CASLFORMULA))
-> [Named DLFORMULA] -> Result [Named CASLFORMULA]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> Named DLFORMULA -> Result (Named CASLFORMULA)
trNamedSentence DLSign
inSig) [Named DLFORMULA]
inForms
      (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (DLSign -> CASLSign
trSign DLSign
inSig, [Named CASLFORMULA]
predefinedAxioms [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
outForms)

-- | translation of named sentences
trNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->
                   Result (Named (FORMULA ()))
trNamedSentence :: DLSign -> Named DLFORMULA -> Result (Named CASLFORMULA)
trNamedSentence inSig :: DLSign
inSig inForm :: Named DLFORMULA
inForm = do
        CASLFORMULA
outSen <- DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig (DLFORMULA -> Result CASLFORMULA)
-> DLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Named DLFORMULA -> DLFORMULA
forall s a. SenAttr s a -> s
sentence Named DLFORMULA
inForm
        Named CASLFORMULA -> Result (Named CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CASLFORMULA -> Result (Named CASLFORMULA))
-> Named CASLFORMULA -> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ (DLFORMULA -> CASLFORMULA) -> Named DLFORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (CASLFORMULA -> DLFORMULA -> CASLFORMULA
forall a b. a -> b -> a
const CASLFORMULA
outSen) Named DLFORMULA
inForm

-- | translation of sentences
trSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())
trSentence :: DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence inSig :: DLSign
inSig inF :: DLFORMULA
inF =
      case DLFORMULA
inF of
        Quantification qf :: QUANTIFIER
qf vs :: [VAR_DECL]
vs frm :: DLFORMULA
frm rn :: Range
rn ->
            do
              CASLFORMULA
outF <- DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig DLFORMULA
frm
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
qf [VAR_DECL]
vs CASLFORMULA
outF Range
rn)
        Junction j :: Junctor
j fns :: [DLFORMULA]
fns rn :: Range
rn ->
            do
              [CASLFORMULA]
outF <- (DLFORMULA -> Result CASLFORMULA)
-> [DLFORMULA] -> Result [CASLFORMULA]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig) [DLFORMULA]
fns
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j [CASLFORMULA]
outF Range
rn)
        Relation f1 :: DLFORMULA
f1 c :: Relation
c f2 :: DLFORMULA
f2 rn :: Range
rn ->
            do
              CASLFORMULA
out1 <- DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig DLFORMULA
f1
              CASLFORMULA
out2 <- DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig DLFORMULA
f2
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
out1 Relation
c CASLFORMULA
out2 Range
rn)
        Negation frm :: DLFORMULA
frm rn :: Range
rn ->
            do
              CASLFORMULA
outF <- DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig DLFORMULA
frm
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
outF Range
rn)
        Atom b :: Bool
b rn :: Range
rn -> CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
Atom Bool
b Range
rn)
        Predication pr :: PRED_SYMB
pr trm :: [TERM DL_FORMULA]
trm rn :: Range
rn ->
            do
              [TERM ()]
ot <- (TERM DL_FORMULA -> Result (TERM ()))
-> [TERM DL_FORMULA] -> Result [TERM ()]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig) [TERM DL_FORMULA]
trm
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
pr [TERM ()]
ot Range
rn)
        Definedness tm :: TERM DL_FORMULA
tm rn :: Range
rn ->
            do
              TERM ()
ot <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
tm
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Range -> FORMULA f
Definedness TERM ()
ot Range
rn)
        Equation t1 :: TERM DL_FORMULA
t1 e :: Equality
e t2 :: TERM DL_FORMULA
t2 rn :: Range
rn ->
            do
              TERM ()
ot1 <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
t1
              TERM ()
ot2 <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
t2
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM ()
ot1 Equality
e TERM ()
ot2 Range
rn)
        Membership t1 :: TERM DL_FORMULA
t1 st :: SORT
st rn :: Range
rn ->
            do
              TERM ()
ot <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
t1
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> SORT -> Range -> CASLFORMULA
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM ()
ot SORT
st Range
rn)
        Mixfix_formula trm :: TERM DL_FORMULA
trm ->
             do
              TERM ()
ot <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
trm
              CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> CASLFORMULA
forall f. TERM f -> FORMULA f
Mixfix_formula TERM ()
ot)
        Unparsed_formula str :: String
str rn :: Range
rn ->
            CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Range -> CASLFORMULA
forall f. String -> Range -> FORMULA f
Unparsed_formula String
str Range
rn)
        Sort_gen_ax cstr :: [Constraint]
cstr ft :: Bool
ft ->
            CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> Bool -> CASLFORMULA
forall f. [Constraint] -> Bool -> FORMULA f
Sort_gen_ax [Constraint]
cstr Bool
ft)
        QuantOp {} -> String -> Result CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "CASL_DL2CASL.QuantOp"
        QuantPred {} -> String -> Result CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "CASL_DL2CASL.QuantPred"
        ExtFORMULA form :: DL_FORMULA
form ->
            case DL_FORMULA
form of
              Cardinality {} ->
                    String -> Result CASLFORMULA
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Mapping of cardinality not implemented"

-- | translation of terms
trTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm inSig :: DLSign
inSig inF :: TERM DL_FORMULA
inF =
    case TERM DL_FORMULA
inF of
      Qual_var v :: VAR
v s :: SORT
s rn :: Range
rn -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (VAR -> SORT -> Range -> TERM ()
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
s Range
rn)
      Application os :: OP_SYMB
os tms :: [TERM DL_FORMULA]
tms rn :: Range
rn ->
          do
            [TERM ()]
ot <- (TERM DL_FORMULA -> Result (TERM ()))
-> [TERM DL_FORMULA] -> Result [TERM ()]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig) [TERM DL_FORMULA]
tms
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os [TERM ()]
ot Range
rn)
      Sorted_term trm :: TERM DL_FORMULA
trm st :: SORT
st rn :: Range
rn ->
          do
            TERM ()
ot <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
trm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
ot SORT
st Range
rn)
      Cast trm :: TERM DL_FORMULA
trm st :: SORT
st rn :: Range
rn ->
          do
            TERM ()
ot <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
trm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Cast TERM ()
ot SORT
st Range
rn)
      Conditional t1 :: TERM DL_FORMULA
t1 frm :: DLFORMULA
frm t2 :: TERM DL_FORMULA
t2 rn :: Range
rn ->
          do
            TERM ()
ot1 <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
t1
            TERM ()
ot2 <- DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig TERM DL_FORMULA
t2
            CASLFORMULA
of1 <- DLSign -> DLFORMULA -> Result CASLFORMULA
trSentence DLSign
inSig DLFORMULA
frm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> CASLFORMULA -> TERM () -> Range -> TERM ()
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM ()
ot1 CASLFORMULA
of1 TERM ()
ot2 Range
rn)
      Unparsed_term str :: String
str rn :: Range
rn -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Range -> TERM ()
forall f. String -> Range -> TERM f
Unparsed_term String
str Range
rn)
      Mixfix_qual_pred ps :: PRED_SYMB
ps -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_SYMB -> TERM ()
forall f. PRED_SYMB -> TERM f
Mixfix_qual_pred PRED_SYMB
ps)
      Mixfix_term trm :: [TERM DL_FORMULA]
trm ->
          do
            [TERM ()]
ot <- (TERM DL_FORMULA -> Result (TERM ()))
-> [TERM DL_FORMULA] -> Result [TERM ()]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig) [TERM DL_FORMULA]
trm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([TERM ()] -> TERM ()
forall f. [TERM f] -> TERM f
Mixfix_term [TERM ()]
ot)
      Mixfix_token tok :: VAR
tok -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (VAR -> TERM ()
forall f. VAR -> TERM f
Mixfix_token VAR
tok)
      Mixfix_sorted_term st :: SORT
st rn :: Range
rn -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT -> Range -> TERM ()
forall f. SORT -> Range -> TERM f
Mixfix_sorted_term SORT
st Range
rn)
      Mixfix_cast st :: SORT
st rn :: Range
rn -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT -> Range -> TERM ()
forall f. SORT -> Range -> TERM f
Mixfix_cast SORT
st Range
rn)
      Mixfix_parenthesized trm :: [TERM DL_FORMULA]
trm rn :: Range
rn ->
          do
            [TERM ()]
ot <- (TERM DL_FORMULA -> Result (TERM ()))
-> [TERM DL_FORMULA] -> Result [TERM ()]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig) [TERM DL_FORMULA]
trm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([TERM ()] -> Range -> TERM ()
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM ()]
ot Range
rn)
      Mixfix_bracketed trm :: [TERM DL_FORMULA]
trm rn :: Range
rn ->
          do
            [TERM ()]
ot <- (TERM DL_FORMULA -> Result (TERM ()))
-> [TERM DL_FORMULA] -> Result [TERM ()]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig) [TERM DL_FORMULA]
trm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([TERM ()] -> Range -> TERM ()
forall f. [TERM f] -> Range -> TERM f
Mixfix_bracketed [TERM ()]
ot Range
rn)
      Mixfix_braced trm :: [TERM DL_FORMULA]
trm rn :: Range
rn ->
          do
            [TERM ()]
ot <- (TERM DL_FORMULA -> Result (TERM ()))
-> [TERM DL_FORMULA] -> Result [TERM ()]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (DLSign -> TERM DL_FORMULA -> Result (TERM ())
trTerm DLSign
inSig) [TERM DL_FORMULA]
trm
            TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ([TERM ()] -> Range -> TERM ()
forall f. [TERM f] -> Range -> TERM f
Mixfix_braced [TERM ()]
ot Range
rn)
      ExtTERM _ -> TERM () -> Result (TERM ())
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Result (TERM ())) -> TERM () -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ () -> TERM ()
forall f. f -> TERM f
ExtTERM ()