{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
{- |
Module      :  ./CASL/OMDocExport.hs
Description :  CASL-to-OMDoc conversion
Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  ewaryst.schulz@dfki.de
Stability   :  provisional
Portability :  portable

CASL implementation of the interface functions export_signToOmdoc,
export_morphismToOmdoc, export_senToOmdoc from class Logic. The actual
instantiation can be found in module "CASL.Logic_CASL".
-}

module CASL.OMDocExport
    ( exportSymToOmdoc
    , exportSenToOmdoc
    , exportTheoryToOmdoc
    , caslMetaTheory
    ) where

import OMDoc.DataTypes

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

import Common.DocUtils

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Fold
import CASL.Quantification
import CASL.OMDoc

import qualified Data.Map as Map
import Data.Maybe

-- --------------------------- TOPLEVEL Interface -----------------------------

type Env = NameMap Symbol


exportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
exportSymToOmdoc :: Env -> Symbol -> String -> Result TCElement
exportSymToOmdoc e :: Env
e sym :: Symbol
sym n :: String
n = Env -> (String, SymbType) -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e (String
n, Symbol -> SymbType
symbType Symbol
sym)


exportSenToOmdoc :: (GetRange f, Pretty f) => Env -> FORMULA f
                 -> Result TCorOMElement
exportSenToOmdoc :: Env -> FORMULA f -> Result TCorOMElement
exportSenToOmdoc e :: Env
e f :: FORMULA f
f =
    case FORMULA f
f of
        Sort_gen_ax cs :: [Constraint]
cs b :: Bool
b -> TCorOMElement -> Result TCorOMElement
forall (m :: * -> *) a. Monad m => a -> m a
return (TCorOMElement -> Result TCorOMElement)
-> TCorOMElement -> Result TCorOMElement
forall a b. (a -> b) -> a -> b
$ TCElement -> TCorOMElement
forall a b. a -> Either a b
Left (TCElement -> TCorOMElement) -> TCElement -> TCorOMElement
forall a b. (a -> b) -> a -> b
$ Env -> [Constraint] -> ADTType -> TCElement
makeADTs Env
e [Constraint]
cs
                            (if Bool
b then ADTType
Free else ADTType
Generated)
        _ -> let err :: b -> a
err = a -> b -> a
forall a b. a -> b -> a
const (a -> b -> a) -> a -> b -> a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
error "CASL extension not supported."
             in TCorOMElement -> Result TCorOMElement
forall (m :: * -> *) a. Monad m => a -> m a
return (TCorOMElement -> Result TCorOMElement)
-> TCorOMElement -> Result TCorOMElement
forall a b. (a -> b) -> a -> b
$ OMElement -> TCorOMElement
forall a b. b -> Either a b
Right (OMElement -> TCorOMElement) -> OMElement -> TCorOMElement
forall a b. (a -> b) -> a -> b
$ Record f OMElement OMElement -> FORMULA f -> OMElement
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Env -> (f -> OMElement) -> Record f OMElement OMElement
forall f.
GetRange f =>
Env -> (f -> OMElement) -> Record f OMElement OMElement
omdocRec Env
e f -> OMElement
forall b a. b -> a
err) FORMULA f
f

-- | We have to export the subsort relation because it's not given in sentences
exportTheoryToOmdoc :: (Show f, Pretty e) => SigMap Symbol -> Sign f e
                    -> [Named (FORMULA f)] -> Result [TCElement]

exportTheoryToOmdoc :: SigMap Symbol
-> Sign f e -> [Named (FORMULA f)] -> Result [TCElement]
exportTheoryToOmdoc sigm :: SigMap Symbol
sigm sig :: Sign f e
sig _ =
    [TCElement] -> Result [TCElement]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCElement] -> Result [TCElement])
-> [TCElement] -> Result [TCElement]
forall a b. (a -> b) -> a -> b
$ ((SORT, SORT) -> TCElement) -> [(SORT, SORT)] -> [TCElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (SORT, SORT) -> TCElement
subsortToOmdoc (Env -> (SORT, SORT) -> TCElement)
-> Env -> (SORT, SORT) -> TCElement
forall a b. (a -> b) -> a -> b
$ SigMap Symbol -> Env
forall a. SigMap a -> NameMap a
sigMapSymbs SigMap Symbol
sigm)
      ([(SORT, SORT)] -> [TCElement]) -> [(SORT, SORT)] -> [TCElement]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel SORT -> [(SORT, SORT)]) -> Rel SORT -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.reflexive (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


-- ------------------------ Sentences --------------------------

subsortToOmdoc :: Env -> (SORT, SORT) -> TCElement
subsortToOmdoc :: Env -> (SORT, SORT) -> TCElement
subsortToOmdoc e :: Env
e (s1 :: SORT
s1, s2 :: SORT
s2) =
    let oms1 :: OMElement
oms1@(OMS (_, OMName n1 :: String
n1 _)) = Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s1
        oms2 :: OMElement
oms2@(OMS (_, OMName n2 :: String
n2 _)) = Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s2
    in String -> OMElement -> SymbolRole -> Maybe OMElement -> TCElement
TCSymbol (String -> [String] -> String
nameEncode "ST" [String
n1, String
n2])
           ([OMElement] -> OMElement
OMA [OMElement
const_subsortof, OMElement
oms1, OMElement
oms2]) SymbolRole
Axiom Maybe OMElement
forall a. Maybe a
Nothing


-- ------------------------ Symbol Interface --------------------------

class AsSymbol a where
    toSymbol :: a -> Symbol

instance AsSymbol SORT where
    toSymbol :: SORT -> Symbol
toSymbol = SORT -> Symbol
idToSortSymbol

instance AsSymbol (Id, OpType) where
    toSymbol :: (SORT, OpType) -> Symbol
toSymbol = (SORT -> OpType -> Symbol) -> (SORT, OpType) -> Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> OpType -> Symbol
idToOpSymbol

instance AsSymbol (Id, OP_TYPE) where
    toSymbol :: (SORT, OP_TYPE) -> Symbol
toSymbol (x :: SORT
x, y :: OP_TYPE
y) = (SORT, OpType) -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol (SORT
x, OP_TYPE -> OpType
toOpType OP_TYPE
y)

instance AsSymbol OP_SYMB where
    toSymbol :: OP_SYMB -> Symbol
toSymbol (Op_name n :: SORT
n) = String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ "AsSymbol: Unqualified OP_SYMB: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
n
    toSymbol (Qual_op_name n :: SORT
n t :: OP_TYPE
t _) = (SORT, OP_TYPE) -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol (SORT
n, OP_TYPE
t)

instance AsSymbol (Id, PredType) where
    toSymbol :: (SORT, PredType) -> Symbol
toSymbol = (SORT -> PredType -> Symbol) -> (SORT, PredType) -> Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> PredType -> Symbol
idToPredSymbol

instance AsSymbol (Id, PRED_TYPE) where
    toSymbol :: (SORT, PRED_TYPE) -> Symbol
toSymbol (x :: SORT
x, y :: PRED_TYPE
y) = (SORT, PredType) -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol (SORT
x, PRED_TYPE -> PredType
toPredType PRED_TYPE
y)

instance AsSymbol PRED_SYMB where
    toSymbol :: PRED_SYMB -> Symbol
toSymbol (Pred_name n :: SORT
n) = String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ "AsSymbol: Unqual. PRED_SYMB: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
n
    toSymbol (Qual_pred_name n :: SORT
n t :: PRED_TYPE
t _) = (SORT, PRED_TYPE) -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol (SORT
n, PRED_TYPE
t)

-- ------------------------ OMDoc Constant Interface --------------------------

class AsOMConstant a where
    toOMConstant :: Env -> a -> Result TCElement


instance AsOMConstant (String, OMElement, SymbolRole) where
    toOMConstant :: Env -> (String, OMElement, SymbolRole) -> Result TCElement
toOMConstant _ (n :: String
n, omelem :: OMElement
omelem, role :: SymbolRole
role) = TCElement -> Result TCElement
forall (m :: * -> *) a. Monad m => a -> m a
return (TCElement -> Result TCElement) -> TCElement -> Result TCElement
forall a b. (a -> b) -> a -> b
$ String -> OMElement -> SymbolRole -> Maybe OMElement -> TCElement
TCSymbol String
n OMElement
omelem SymbolRole
role Maybe OMElement
forall a. Maybe a
Nothing

instance AsOMConstant (String, OpType) where
    toOMConstant :: Env -> (String, OpType) -> Result TCElement
toOMConstant e :: Env
e (n :: String
n, ot :: OpType
ot) = Env -> (String, OMElement, SymbolRole) -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e (String
n, Env -> OpType -> OMElement
makeObjectType Env
e OpType
ot, SymbolRole
Obj)

instance AsOMConstant (String, PredType) where
    toOMConstant :: Env -> (String, PredType) -> Result TCElement
toOMConstant e :: Env
e (n :: String
n, pt :: PredType
pt) = Env -> (String, OMElement, SymbolRole) -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e (String
n, Env -> PredType -> OMElement
makePredType Env
e PredType
pt, SymbolRole
Obj)

instance AsOMConstant String where
    toOMConstant :: Env -> String -> Result TCElement
toOMConstant e :: Env
e n :: String
n = Env -> (String, OMElement, SymbolRole) -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e (String
n, OMElement
const_sort, SymbolRole
Typ)

instance AsOMConstant (String, SymbType) where
    toOMConstant :: Env -> (String, SymbType) -> Result TCElement
toOMConstant e :: Env
e (n :: String
n, st :: SymbType
st) =
        case SymbType
st of
          SortAsItemType -> Env -> String -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e String
n
          SubsortAsItemType _ -> String -> Result TCElement
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "AsOMConstant.SubsortAsItemType"
          OpAsItemType ot :: OpType
ot -> Env -> (String, OpType) -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e (String
n, OpType
ot)
          PredAsItemType pt :: PredType
pt -> Env -> (String, PredType) -> Result TCElement
forall a. AsOMConstant a => Env -> a -> Result TCElement
toOMConstant Env
e (String
n, PredType
pt)

-- ------------------------ ADT --------------------------

makeADTs :: Env -> [Constraint] -> ADTType -> TCElement
makeADTs :: Env -> [Constraint] -> ADTType -> TCElement
makeADTs e :: Env
e cs :: [Constraint]
cs b :: ADTType
b =
    [OmdADT] -> TCElement
TCADT ([OmdADT] -> TCElement) -> [OmdADT] -> TCElement
forall a b. (a -> b) -> a -> b
$ (Constraint -> OmdADT) -> [Constraint] -> [OmdADT]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> ADTType -> Constraint -> OmdADT
makeADTSortDef Env
e ADTType
b) [Constraint]
cs

makeADTSortDef :: Env -> ADTType -> Constraint -> OmdADT
makeADTSortDef :: Env -> ADTType -> Constraint -> OmdADT
makeADTSortDef e :: Env
e b :: ADTType
b (Constraint s :: SORT
s l :: [(OP_SYMB, [Int])]
l _) =
    String -> ADTType -> [OmdADT] -> OmdADT
ADTSortDef (Env -> SORT -> String
forall a. AsSymbol a => Env -> a -> String
omn Env
e SORT
s) ADTType
b ([OmdADT] -> OmdADT) -> [OmdADT] -> OmdADT
forall a b. (a -> b) -> a -> b
$
    ((OP_SYMB, [Int]) -> OmdADT) -> [(OP_SYMB, [Int])] -> [OmdADT]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OP_SYMB -> OmdADT
makeADTConstructor Env
e (OP_SYMB -> OmdADT)
-> ((OP_SYMB, [Int]) -> OP_SYMB) -> (OP_SYMB, [Int]) -> OmdADT
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])]
l

makeADTConstructor :: Env -> OP_SYMB -> OmdADT
makeADTConstructor :: Env -> OP_SYMB -> OmdADT
makeADTConstructor e :: Env
e os :: OP_SYMB
os@(Qual_op_name n :: SORT
n (Op_type _ args :: [SORT]
args _ _) _) =
    if SORT -> Bool
isInjName SORT
n then OMQualName -> OmdADT
ADTInsort (OMQualName -> OmdADT) -> OMQualName -> OmdADT
forall a b. (a -> b) -> a -> b
$ Env -> SORT -> OMQualName
forall a. AsSymbol a => Env -> a -> OMQualName
omqn Env
e (SORT -> OMQualName) -> SORT -> OMQualName
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT
forall a. [a] -> a
head [SORT]
args
    else String -> [OmdADT] -> OmdADT
ADTConstr (Env -> OP_SYMB -> String
forall a. AsSymbol a => Env -> a -> String
omn Env
e OP_SYMB
os) ([OmdADT] -> OmdADT) -> [OmdADT] -> OmdADT
forall a b. (a -> b) -> a -> b
$ (SORT -> OmdADT) -> [SORT] -> [OmdADT]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> SORT -> OmdADT
makeADTArgument Env
e) [SORT]
args

makeADTConstructor _ (Op_name (Id _ _ r :: Range
r)) =
    String -> Range -> OmdADT
forall a. String -> Range -> a
sfail "makeADTConstructor: No_qual_op" Range
r

-- TODO: support for selectors
makeADTArgument :: Env -> SORT -> OmdADT
makeADTArgument :: Env -> SORT -> OmdADT
makeADTArgument e :: Env
e s :: SORT
s = OMElement -> Maybe OmdADT -> OmdADT
ADTArg (Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s) Maybe OmdADT
forall a. Maybe a
Nothing


-- ------------------------ UTILS --------------------------

findInEnv :: UniqName -> Env -> Symbol -> UniqName
findInEnv :: UniqName -> Env -> Symbol -> UniqName
findInEnv err :: UniqName
err m :: Env
m x :: Symbol
x = UniqName -> Maybe UniqName -> UniqName
forall a. a -> Maybe a -> a
fromMaybe (case Symbol -> SymbType
symbType Symbol
x of
     OpAsItemType o :: OpType
o -> UniqName -> Symbol -> Env -> UniqName
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault UniqName
err
        Symbol
x { symbType :: SymbType
symbType = OpType -> SymbType
OpAsItemType
            (OpType -> SymbType) -> OpType -> SymbType
forall a b. (a -> b) -> a -> b
$ (if OpType -> Bool
isTotal OpType
o then OpType -> OpType
mkPartial else OpType -> OpType
mkTotal) OpType
o } Env
m
     _ -> UniqName
err) (Maybe UniqName -> UniqName) -> Maybe UniqName -> UniqName
forall a b. (a -> b) -> a -> b
$ Symbol -> Env -> Maybe UniqName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
x Env
m

sfail :: String -> Range -> a
sfail :: String -> Range -> a
sfail s :: String
s r :: Range
r = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ Diagnosis -> String
forall a. Show a => a -> String
show (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("unexpected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s) Range
r)

omn :: AsSymbol a => Env -> a -> String
omn :: Env -> a -> String
omn e :: Env
e x :: a
x = let s :: Symbol
s = a -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol a
x
              err :: a
err = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omn: No mapping for ", Symbol -> String
forall a. Show a => a -> String
show Symbol
s, "\n"
                                   , "--------------------------------\n"
                                   , Env -> String
forall a. Show a => a -> String
show Env
e]
          in UniqName -> String
nameToString (UniqName -> String) -> UniqName -> String
forall a b. (a -> b) -> a -> b
$ UniqName -> Env -> Symbol -> UniqName
findInEnv UniqName
forall a. a
err Env
e Symbol
s

omqn :: AsSymbol a => Env -> a -> OMQualName
omqn :: Env -> a -> OMQualName
omqn e :: Env
e x :: a
x = let s :: Symbol
s = a -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol a
x
               err :: a
err = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omqn: No mapping for ", Symbol -> String
forall a. Show a => a -> String
show Symbol
s, "\n"
                                    , "--------------------------------\n"
                                    , Env -> String
forall a. Show a => a -> String
show Env
e]
           in UniqName -> OMQualName
mkSimpleQualName (UniqName -> OMQualName) -> UniqName -> OMQualName
forall a b. (a -> b) -> a -> b
$ UniqName -> Env -> Symbol -> UniqName
findInEnv UniqName
forall a. a
err Env
e Symbol
s

oms :: AsSymbol a => Env -> a -> OMElement
oms :: Env -> a -> OMElement
oms e :: Env
e x :: a
x = let s :: Symbol
s = a -> Symbol
forall a. AsSymbol a => a -> Symbol
toSymbol a
x
              err :: a
err = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "oms: No mapping for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
s
          in UniqName -> OMElement
simpleOMS (UniqName -> OMElement) -> UniqName -> OMElement
forall a b. (a -> b) -> a -> b
$ UniqName -> Env -> Symbol -> UniqName
findInEnv UniqName
forall a. a
err Env
e Symbol
s


-- ------------------------ TYPES --------------------------

-- | Given an operator or predicate signature we construct the according type
makeType :: Env -> OpKind -> [SORT] -> Maybe SORT -> OMElement
makeType :: Env -> OpKind -> [SORT] -> Maybe SORT -> OMElement
makeType e :: Env
e _ [] (Just r :: SORT
r) = Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
r
makeType e :: Env
e total :: OpKind
total domain :: [SORT]
domain range :: Maybe SORT
range =
    if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
args then OMElement
funtypeconstr else [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ OMElement
funtypeconstr OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: (SORT -> OMElement) -> [SORT] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e) [SORT]
args
        where
          args :: [SORT]
args = [SORT]
domain [SORT] -> [SORT] -> [SORT]
forall a. [a] -> [a] -> [a]
++ Maybe SORT -> [SORT]
forall a. Maybe a -> [a]
maybeToList Maybe SORT
range
          funtypeconstr :: OMElement
funtypeconstr = case (OpKind
total, Maybe SORT
range) of
                            (Total, Nothing) -> OMElement
const_predtype
                            (Total, _) -> OMElement
const_funtype
                            _ -> OMElement
const_partialfuntype

makePredType :: Env -> PredType -> OMElement
makePredType :: Env -> PredType -> OMElement
makePredType e :: Env
e (PredType predargs :: [SORT]
predargs) =
    Env -> OpKind -> [SORT] -> Maybe SORT -> OMElement
makeType Env
e OpKind
Total [SORT]
predargs Maybe SORT
forall a. Maybe a
Nothing

makeObjectType :: Env -> OpType -> OMElement
makeObjectType :: Env -> OpType -> OMElement
makeObjectType e :: Env
e (OpType opkind :: OpKind
opkind opargs :: [SORT]
opargs oprange :: SORT
oprange) =
    Env -> OpKind -> [SORT] -> Maybe SORT -> OMElement
makeType Env
e OpKind
opkind [SORT]
opargs (SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
oprange)

-- ------------------------ TERMS --------------------------

appOrConst :: AsSymbol a => Env -> a -> [OMElement] -> OMElement
appOrConst :: Env -> a -> [OMElement] -> OMElement
appOrConst e :: Env
e o :: a
o [] = Env -> a -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e a
o
appOrConst e :: Env
e o :: a
o ts :: [OMElement]
ts = [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ Env -> a -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e a
o OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: [OMElement]
ts

-- | The object e1 and its type e2
makeTyped :: OMElement -- ^ e1
          -> OMElement -- ^ e2
          -> OMElement
makeTyped :: OMElement -> OMElement -> OMElement
makeTyped e1 :: OMElement
e1 e2 :: OMElement
e2 = OMElement -> OMAttribute -> OMElement
OMATTT OMElement
e1 (OMAttribute -> OMElement) -> OMAttribute -> OMElement
forall a b. (a -> b) -> a -> b
$ OMElement -> OMElement -> OMAttribute
OMAttr OMElement
const_type OMElement
e2

varToOmdoc :: Token -> OMElement
varToOmdoc :: Token -> OMElement
varToOmdoc v :: Token
v = OMName -> OMElement
OMV (OMName -> OMElement) -> OMName -> OMElement
forall a b. (a -> b) -> a -> b
$ String -> OMName
mkSimpleName (String -> OMName) -> String -> OMName
forall a b. (a -> b) -> a -> b
$ Token -> String
tokStr Token
v

-- | typed vars can only be typed by a single sort (first order)
varDeclToOMDoc :: Env -> (VAR, SORT) -> OMElement
varDeclToOMDoc :: Env -> (Token, SORT) -> OMElement
varDeclToOMDoc e :: Env
e (v :: Token
v, s :: SORT
s) = OMElement -> OMElement -> OMElement
makeTyped (Token -> OMElement
varToOmdoc Token
v) (OMElement -> OMElement) -> OMElement -> OMElement
forall a b. (a -> b) -> a -> b
$ Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s

omdocRec :: GetRange f => Env -> (f -> OMElement)
         -> Record f OMElement OMElement
omdocRec :: Env -> (f -> OMElement) -> Record f OMElement OMElement
omdocRec e :: Env
e mf :: f -> OMElement
mf = 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 -> SORT -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> SORT -> OP_TYPE -> a -> a)
-> (FORMULA f -> SORT -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> Token -> SORT -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> Token -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> SORT -> 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] -> OMElement -> Range -> OMElement
foldQuantification = \ _ q :: QUANTIFIER
q vs :: [VAR_DECL]
vs f :: OMElement
f _ ->
      let s :: OMElement
s = case QUANTIFIER
q of
                Universal -> OMElement
const_forall
                Existential -> OMElement
const_exists
                Unique_existential -> OMElement
const_existsunique
          vl :: [OMElement]
vl = ((Token, SORT) -> OMElement) -> [(Token, SORT)] -> [OMElement]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Token, SORT) -> OMElement
varDeclToOMDoc Env
e) ([(Token, SORT)] -> [OMElement]) -> [(Token, SORT)] -> [OMElement]
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, SORT)]
flatVAR_DECLs [VAR_DECL]
vs
      in OMElement -> [OMElement] -> OMElement -> OMElement
OMBIND OMElement
s [OMElement]
vl OMElement
f
    , foldJunction :: FORMULA f -> Junctor -> [OMElement] -> Range -> OMElement
foldJunction = \ _ j :: Junctor
j fs :: [OMElement]
fs _ -> [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ case Junctor
j of
          Con -> OMElement
const_and
          Dis -> OMElement
const_or
        OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: [OMElement]
fs
    , foldRelation :: FORMULA f
-> OMElement -> Relation -> OMElement -> Range -> OMElement
foldRelation = \ _ f1 :: OMElement
f1 c :: Relation
c f2 :: OMElement
f2 _ -> [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ case Relation
c of
          Implication -> OMElement
const_implies
          RevImpl -> OMElement
const_implied
          Equivalence -> OMElement
const_equivalent
        OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: [OMElement
f1, OMElement
f2]
    , foldNegation :: FORMULA f -> OMElement -> Range -> OMElement
foldNegation = \ _ f :: OMElement
f _ -> [OMElement] -> OMElement
OMA [OMElement
const_not, OMElement
f]
    , foldAtom :: FORMULA f -> Bool -> Range -> OMElement
foldAtom = \ _ b :: Bool
b _ -> if Bool
b then OMElement
const_true else OMElement
const_false
    , foldPredication :: FORMULA f -> PRED_SYMB -> [OMElement] -> Range -> OMElement
foldPredication = \ _ p :: PRED_SYMB
p ts :: [OMElement]
ts _ -> Env -> PRED_SYMB -> [OMElement] -> OMElement
forall a. AsSymbol a => Env -> a -> [OMElement] -> OMElement
appOrConst Env
e PRED_SYMB
p [OMElement]
ts
    , foldDefinedness :: FORMULA f -> OMElement -> Range -> OMElement
foldDefinedness = \ _ t :: OMElement
t _ -> [OMElement] -> OMElement
OMA [OMElement
const_def, OMElement
t]
    , foldEquation :: FORMULA f
-> OMElement -> Equality -> OMElement -> Range -> OMElement
foldEquation = \ _ t1 :: OMElement
t1 r :: Equality
r t2 :: OMElement
t2 _ -> [OMElement] -> OMElement
OMA ([OMElement] -> OMElement) -> [OMElement] -> OMElement
forall a b. (a -> b) -> a -> b
$ case Equality
r of
          Existl -> OMElement
const_eeq
          Strong -> OMElement
const_eq
        OMElement -> [OMElement] -> [OMElement]
forall a. a -> [a] -> [a]
: [OMElement
t1, OMElement
t2]
    , foldMembership :: FORMULA f -> OMElement -> SORT -> Range -> OMElement
foldMembership = \ _ t :: OMElement
t s :: SORT
s _ -> [OMElement] -> OMElement
OMA [OMElement
const_in, OMElement
t, Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s]
    , foldMixfix_formula :: FORMULA f -> OMElement -> OMElement
foldMixfix_formula = \ t :: FORMULA f
t _ -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_formula" (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange FORMULA f
t
    , foldQuantOp :: FORMULA f -> SORT -> OP_TYPE -> OMElement -> OMElement
foldQuantOp = \ _ o :: SORT
o _ _ -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail ("QuantOp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
o) (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ SORT -> Range
forall a. GetRange a => a -> Range
getRange SORT
o
    , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> OMElement -> OMElement
foldQuantPred = \ _ p :: SORT
p _ _ -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail ("QuantPred " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
p) (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ SORT -> Range
forall a. GetRange a => a -> Range
getRange SORT
p
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> OMElement
foldSort_gen_ax = \ t :: FORMULA f
t _ _ -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail
                        "Sort generating axioms should be filtered out before!"
                        (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange FORMULA f
t
    , foldExtFORMULA :: FORMULA f -> f -> OMElement
foldExtFORMULA = (f -> OMElement) -> FORMULA f -> f -> OMElement
forall a b. a -> b -> a
const f -> OMElement
mf
    , foldQual_var :: TERM f -> Token -> SORT -> Range -> OMElement
foldQual_var = \ _ v :: Token
v _ _ -> Token -> OMElement
varToOmdoc Token
v
    , foldApplication :: TERM f -> OP_SYMB -> [OMElement] -> Range -> OMElement
foldApplication = \ _ o :: OP_SYMB
o ts :: [OMElement]
ts _ -> Env -> OP_SYMB -> [OMElement] -> OMElement
forall a. AsSymbol a => Env -> a -> [OMElement] -> OMElement
appOrConst Env
e OP_SYMB
o [OMElement]
ts
    , foldSorted_term :: TERM f -> OMElement -> SORT -> Range -> OMElement
foldSorted_term = \ _ r :: OMElement
r s :: SORT
s _ -> OMElement -> OMElement -> OMElement
makeTyped OMElement
r (OMElement -> OMElement) -> OMElement -> OMElement
forall a b. (a -> b) -> a -> b
$ Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s
    , foldCast :: TERM f -> OMElement -> SORT -> Range -> OMElement
foldCast = \ _ t :: OMElement
t s :: SORT
s _ -> [OMElement] -> OMElement
OMA [OMElement
const_cast, OMElement
t, Env -> SORT -> OMElement
forall a. AsSymbol a => Env -> a -> OMElement
oms Env
e SORT
s]
    , foldConditional :: TERM f -> OMElement -> OMElement -> OMElement -> Range -> OMElement
foldConditional = \ _ e' :: OMElement
e' f :: OMElement
f t :: OMElement
t _ -> [OMElement] -> OMElement
OMA [OMElement
const_if, OMElement
e', OMElement
f, OMElement
t]
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> OMElement
foldMixfix_qual_pred = \ _ p :: PRED_SYMB
p -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_qual_pred" (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> Range
forall a. GetRange a => a -> Range
getRange PRED_SYMB
p
    , foldMixfix_term :: TERM f -> [OMElement] -> OMElement
foldMixfix_term = \ t :: TERM f
t _ -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_term" (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ TERM f -> Range
forall a. GetRange a => a -> Range
getRange TERM f
t
    , foldMixfix_token :: TERM f -> Token -> OMElement
foldMixfix_token = \ _ t :: Token
t -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_token" (Range -> OMElement) -> Range -> OMElement
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t
    , foldMixfix_sorted_term :: TERM f -> SORT -> Range -> OMElement
foldMixfix_sorted_term = \ _ _ r :: Range
r -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_sorted_term" Range
r
    , foldMixfix_cast :: TERM f -> SORT -> Range -> OMElement
foldMixfix_cast = \ _ _ r :: Range
r -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_cast" Range
r
    , foldMixfix_parenthesized :: TERM f -> [OMElement] -> Range -> OMElement
foldMixfix_parenthesized = \ _ _ r :: Range
r -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_parenthesized" Range
r
    , foldMixfix_bracketed :: TERM f -> [OMElement] -> Range -> OMElement
foldMixfix_bracketed = \ _ _ r :: Range
r -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_bracketed" Range
r
    , foldMixfix_braced :: TERM f -> [OMElement] -> Range -> OMElement
foldMixfix_braced = \ _ _ r :: Range
r -> String -> Range -> OMElement
forall a. String -> Range -> a
sfail "Mixfix_braced" Range
r
    , foldExtTERM :: TERM f -> f -> OMElement
foldExtTERM = (f -> OMElement) -> TERM f -> f -> OMElement
forall a b. a -> b -> a
const f -> OMElement
mf }