{- |
Module      :  ./CASL/OMDocImport.hs
Description :  OMDoc-to-CASL 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 omdocToSym, omdocToSen
, addOMadtToTheory, addOmdocToTheory from class Logic. The actual
instantiation can be found in module "CASL.Logic_CASL".
-}

module CASL.OMDocImport
    ( omdocToSym
    , omdocToSen
    , addOMadtToTheory
    , addOmdocToTheory
    ) where

import OMDoc.DataTypes

import Common.Id
import Common.Result
import Common.AS_Annotation
import qualified Common.Lib.Rel as Rel

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.OMDoc

import Control.Monad
import qualified Control.Monad.Fail as Fail

import qualified Data.Map as Map
import Data.List
import Data.Function (on)

-- * Environment Interface

type Env = SigMapI Symbol

symbolToSort :: Symbol -> SORT
symbolToSort :: Symbol -> SORT
symbolToSort (Symbol n :: SORT
n SortAsItemType) = SORT
n
symbolToSort s :: Symbol
s = [Char] -> SORT
forall a. HasCallStack => [Char] -> a
error ([Char] -> SORT) -> [Char] -> SORT
forall a b. (a -> b) -> a -> b
$ "symbolToSort: Nonsort encountered: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
s

symbolToOp :: Symbol -> (Id, OpType)
symbolToOp :: Symbol -> (SORT, OpType)
symbolToOp (Symbol n :: SORT
n (OpAsItemType ot :: OpType
ot)) = (SORT
n, OpType
ot)
symbolToOp s :: Symbol
s = [Char] -> (SORT, OpType)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (SORT, OpType)) -> [Char] -> (SORT, OpType)
forall a b. (a -> b) -> a -> b
$ "symbolToOp: Nonop encountered: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
s

symbolToPred :: Symbol -> (Id, PredType)
symbolToPred :: Symbol -> (SORT, PredType)
symbolToPred (Symbol n :: SORT
n (PredAsItemType pt :: PredType
pt)) = (SORT
n, PredType
pt)
symbolToPred s :: Symbol
s = [Char] -> (SORT, PredType)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (SORT, PredType)) -> [Char] -> (SORT, PredType)
forall a b. (a -> b) -> a -> b
$ "symbolToPred: Nonpred encountered: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
s

lookupSymbol :: Env -> OMName -> Symbol
lookupSymbol :: Env -> OMName -> Symbol
lookupSymbol e :: Env
e omn :: OMName
omn =
    Symbol -> OMName -> Map OMName Symbol -> Symbol
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
           ([Char] -> Symbol
forall a. HasCallStack => [Char] -> a
error ([Char] -> Symbol) -> [Char] -> Symbol
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "lookupSymbol failed for: "
                           , OMName -> [Char]
forall a. Show a => a -> [Char]
show OMName
omn, "\nmap: ", Map OMName Symbol -> [Char]
forall a. Show a => a -> [Char]
show (Map OMName Symbol -> [Char]) -> Map OMName Symbol -> [Char]
forall a b. (a -> b) -> a -> b
$ Env -> Map OMName Symbol
forall a. SigMapI a -> Map OMName a
sigMapISymbs Env
e])
       OMName
omn (Map OMName Symbol -> Symbol) -> Map OMName Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Env -> Map OMName Symbol
forall a. SigMapI a -> Map OMName a
sigMapISymbs Env
e

lookupSort :: Env -> OMName -> SORT
lookupSort :: Env -> OMName -> SORT
lookupSort e :: Env
e = Symbol -> SORT
symbolToSort (Symbol -> SORT) -> (OMName -> Symbol) -> OMName -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> OMName -> Symbol
lookupSymbol Env
e

lookupSortOMS :: String -> Env -> OMElement -> SORT
lookupSortOMS :: [Char] -> Env -> OMElement -> SORT
lookupSortOMS msg :: [Char]
msg = (Env -> OMName -> SORT) -> [Char] -> Env -> OMElement -> SORT
forall a. (Env -> OMName -> a) -> [Char] -> Env -> OMElement -> a
lookupOMS Env -> OMName -> SORT
lookupSort ([Char] -> Env -> OMElement -> SORT)
-> [Char] -> Env -> OMElement -> SORT
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "(SORT)"

lookupPred :: Env -> OMName -> (Id, PredType)
lookupPred :: Env -> OMName -> (SORT, PredType)
lookupPred e :: Env
e = Symbol -> (SORT, PredType)
symbolToPred (Symbol -> (SORT, PredType))
-> (OMName -> Symbol) -> OMName -> (SORT, PredType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> OMName -> Symbol
lookupSymbol Env
e

lookupPredOMS :: String -> Env -> OMElement -> (Id, PredType)
lookupPredOMS :: [Char] -> Env -> OMElement -> (SORT, PredType)
lookupPredOMS msg :: [Char]
msg = (Env -> OMName -> (SORT, PredType))
-> [Char] -> Env -> OMElement -> (SORT, PredType)
forall a. (Env -> OMName -> a) -> [Char] -> Env -> OMElement -> a
lookupOMS Env -> OMName -> (SORT, PredType)
lookupPred ([Char] -> Env -> OMElement -> (SORT, PredType))
-> [Char] -> Env -> OMElement -> (SORT, PredType)
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "(PRED)"

lookupOp :: Env -> OMName -> (Id, OpType)
lookupOp :: Env -> OMName -> (SORT, OpType)
lookupOp e :: Env
e = Symbol -> (SORT, OpType)
symbolToOp (Symbol -> (SORT, OpType))
-> (OMName -> Symbol) -> OMName -> (SORT, OpType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> OMName -> Symbol
lookupSymbol Env
e

lookupOpOMS :: String -> Env -> OMElement -> (Id, OpType)
lookupOpOMS :: [Char] -> Env -> OMElement -> (SORT, OpType)
lookupOpOMS msg :: [Char]
msg = (Env -> OMName -> (SORT, OpType))
-> [Char] -> Env -> OMElement -> (SORT, OpType)
forall a. (Env -> OMName -> a) -> [Char] -> Env -> OMElement -> a
lookupOMS Env -> OMName -> (SORT, OpType)
lookupOp ([Char] -> Env -> OMElement -> (SORT, OpType))
-> [Char] -> Env -> OMElement -> (SORT, OpType)
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "(Op)"

lookupOMS :: (Env -> OMName -> a) -> String -> Env -> OMElement -> a
lookupOMS :: (Env -> OMName -> a) -> [Char] -> Env -> OMElement -> a
lookupOMS f :: Env -> OMName -> a
f msg :: [Char]
msg e :: Env
e oms :: OMElement
oms@(OMS (cd :: OMCD
cd, omn :: OMName
omn)) =
    if OMCD -> Bool
cdIsEmpty OMCD
cd then Env -> OMName -> a
f Env
e OMName
omn
    else [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
msg, ": lookupOMS: Nonempty cd in const: "
                        , OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
oms]
lookupOMS _ msg :: [Char]
msg _ ome :: OMElement
ome =
    [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]
msg, ": lookupOMS: Nonsymbol: ", OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
ome]

toOpSymb :: (Id, OpType) -> OP_SYMB
toOpSymb :: (SORT, OpType) -> OP_SYMB
toOpSymb (i :: SORT
i, t :: OpType
t) = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i (OpType -> OP_TYPE
toOP_TYPE OpType
t) Range
nullRange

toPredSymb :: (Id, PredType) -> PRED_SYMB
toPredSymb :: (SORT, PredType) -> PRED_SYMB
toPredSymb (i :: SORT
i, t :: PredType
t) = SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
i (PredType -> PRED_TYPE
toPRED_TYPE PredType
t) Range
nullRange

-- * TOPLEVEL Interface

-- | A TCSymbols is transformed to a CASL symbol with given name.
omdocToSym :: Env -> TCElement -> String -> Result Symbol
omdocToSym :: Env -> TCElement -> [Char] -> Result Symbol
omdocToSym e :: Env
e sym :: TCElement
sym@(TCSymbol _ ctp :: OMElement
ctp srole :: SymbolRole
srole _) n :: [Char]
n =
    case SymbolRole
srole of
      Typ | OMElement
ctp OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_sort -> Symbol -> Result Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Result Symbol) -> Symbol -> Result Symbol
forall a b. (a -> b) -> a -> b
$ SORT -> Symbol
idToSortSymbol (SORT -> Symbol) -> SORT -> Symbol
forall a b. (a -> b) -> a -> b
$ [Char] -> SORT
nameToId [Char]
n
          | Bool
otherwise -> [Char] -> Result Symbol
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result Symbol) -> [Char] -> Result Symbol
forall a b. (a -> b) -> a -> b
$ "omdocToSym: No sorttype for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TCElement -> [Char]
forall a. Show a => a -> [Char]
show TCElement
sym
      Obj -> Symbol -> Result Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Result Symbol) -> Symbol -> Result Symbol
forall a b. (a -> b) -> a -> b
$
             case Env -> OMElement -> Either OpType PredType
omdocToType Env
e OMElement
ctp of
               Left ot :: OpType
ot -> SORT -> OpType -> Symbol
idToOpSymbol ([Char] -> SORT
nameToId [Char]
n) OpType
ot
               Right pt :: PredType
pt -> SORT -> PredType -> Symbol
idToPredSymbol ([Char] -> SORT
nameToId [Char]
n) PredType
pt
      _ -> [Char] -> Result Symbol
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result Symbol) -> [Char] -> Result Symbol
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omdocToSym: only type or object are allowed as"
                         , " symbol roles, but found: ", SymbolRole -> [Char]
forall a. Show a => a -> [Char]
show SymbolRole
srole ]

omdocToSym _ sym :: TCElement
sym _ = [Char] -> Result Symbol
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result Symbol) -> [Char] -> Result Symbol
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omdocToSym: only TCSymbol is allowed,"
                                   , " but found: ", TCElement -> [Char]
forall a. Show a => a -> [Char]
show TCElement
sym ]


omdocToSen :: Env -> TCElement -> String
           -> Result (Maybe (Named (FORMULA f)))
omdocToSen :: Env -> TCElement -> [Char] -> Result (Maybe (Named (FORMULA f)))
omdocToSen e :: Env
e (TCSymbol _ t :: OMElement
t sr :: SymbolRole
sr _) n :: [Char]
n =
    case [Char] -> Maybe ([Char], [[Char]])
nameDecode [Char]
n of
      Just _ ->
          Maybe (Named (FORMULA f)) -> Result (Maybe (Named (FORMULA f)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Named (FORMULA f))
forall a. Maybe a
Nothing -- don't translate encoded names here
      Nothing ->
          let ns :: SenAttr (FORMULA f) [Char]
ns = [Char] -> FORMULA f -> SenAttr (FORMULA f) [Char]
forall a s. a -> s -> SenAttr s a
makeNamed [Char]
n (FORMULA f -> SenAttr (FORMULA f) [Char])
-> FORMULA f -> SenAttr (FORMULA f) [Char]
forall a b. (a -> b) -> a -> b
$ Env -> OMElement -> FORMULA f
forall f. Env -> OMElement -> FORMULA f
omdocToFormula Env
e OMElement
t
              res :: Bool -> m (Maybe (SenAttr (FORMULA f) [Char]))
res b :: Bool
b = Maybe (SenAttr (FORMULA f) [Char])
-> m (Maybe (SenAttr (FORMULA f) [Char]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SenAttr (FORMULA f) [Char])
 -> m (Maybe (SenAttr (FORMULA f) [Char])))
-> Maybe (SenAttr (FORMULA f) [Char])
-> m (Maybe (SenAttr (FORMULA f) [Char]))
forall a b. (a -> b) -> a -> b
$ SenAttr (FORMULA f) [Char] -> Maybe (SenAttr (FORMULA f) [Char])
forall a. a -> Maybe a
Just (SenAttr (FORMULA f) [Char] -> Maybe (SenAttr (FORMULA f) [Char]))
-> SenAttr (FORMULA f) [Char] -> Maybe (SenAttr (FORMULA f) [Char])
forall a b. (a -> b) -> a -> b
$ SenAttr (FORMULA f) [Char]
forall f. SenAttr (FORMULA f) [Char]
ns { isAxiom :: Bool
isAxiom = Bool
b }
          in case SymbolRole
sr of
               Axiom -> Bool -> Result (Maybe (Named (FORMULA f)))
forall (m :: * -> *) f.
Monad m =>
Bool -> m (Maybe (SenAttr (FORMULA f) [Char]))
res Bool
True
               Theorem -> Bool -> Result (Maybe (Named (FORMULA f)))
forall (m :: * -> *) f.
Monad m =>
Bool -> m (Maybe (SenAttr (FORMULA f) [Char]))
res Bool
False
               _ -> Maybe (Named (FORMULA f)) -> Result (Maybe (Named (FORMULA f)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Named (FORMULA f))
forall a. Maybe a
Nothing

omdocToSen _ sym :: TCElement
sym _ = [Char] -> Result (Maybe (Named (FORMULA f)))
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result (Maybe (Named (FORMULA f))))
-> [Char] -> Result (Maybe (Named (FORMULA f)))
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omdocToSen: only TCSymbol is allowed,"
                                   , " but found: ", TCElement -> [Char]
forall a. Show a => a -> [Char]
show TCElement
sym ]


-- | Sort generation constraints are added as named formulas.
addOMadtToTheory :: Env
                 -> (Sign f e, [Named (FORMULA f)]) -> [[OmdADT]]
                 -> Result (Sign f e, [Named (FORMULA f)])
addOMadtToTheory :: Env
-> (Sign f e, [Named (FORMULA f)])
-> [[OmdADT]]
-> Result (Sign f e, [Named (FORMULA f)])
addOMadtToTheory e :: Env
e (sig :: Sign f e
sig, nsens :: [Named (FORMULA f)]
nsens) adts :: [[OmdADT]]
adts = do
    [Named (FORMULA f)]
sgcs <- ([OmdADT] -> Result (Named (FORMULA f)))
-> [[OmdADT]] -> Result [Named (FORMULA f)]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (Env -> [OmdADT] -> Result (Named (FORMULA f))
forall f. Env -> [OmdADT] -> Result (Named (FORMULA f))
omdocToSortGenConstraint Env
e) [[OmdADT]]
adts
    (Sign f e, [Named (FORMULA f)])
-> Result (Sign f e, [Named (FORMULA f)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign f e
sig, [Named (FORMULA f)]
nsens [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [Named (FORMULA f)]
sgcs)


-- | The subsort relation is recovered from exported sentences.
addOmdocToTheory :: Env -> (Sign f e, [Named (FORMULA f)]) -> [TCElement]
                 -> Result (Sign f e, [Named (FORMULA f)])
addOmdocToTheory :: Env
-> (Sign f e, [Named (FORMULA f)])
-> [TCElement]
-> Result (Sign f e, [Named (FORMULA f)])
addOmdocToTheory e :: Env
e (sig :: Sign f e
sig, nsens :: [Named (FORMULA f)]
nsens) tcs :: [TCElement]
tcs = do
  Rel SORT
srel <- Env -> [TCElement] -> Result (Rel SORT)
omdocToSortRel Env
e [TCElement]
tcs
  (Sign f e, [Named (FORMULA f)])
-> Result (Sign f e, [Named (FORMULA f)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign f e
sig { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure Rel SORT
srel }, [Named (FORMULA f)]
nsens)


-- * Algebraic Data Types

omdocToSortGenConstraint :: Env -> [OmdADT] -> Result (Named (FORMULA f))
omdocToSortGenConstraint :: Env -> [OmdADT] -> Result (Named (FORMULA f))
omdocToSortGenConstraint e :: Env
e sortdefs :: [OmdADT]
sortdefs = do
  -- take the last type as the type of all constraints
  let (t :: ADTType
t, cs :: [Constraint]
cs) = (ADTType -> OmdADT -> (ADTType, Constraint))
-> ADTType -> [OmdADT] -> (ADTType, [Constraint])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL ((OmdADT -> (ADTType, Constraint))
-> ADTType -> OmdADT -> (ADTType, Constraint)
forall a b. a -> b -> a
const ((OmdADT -> (ADTType, Constraint))
 -> ADTType -> OmdADT -> (ADTType, Constraint))
-> (OmdADT -> (ADTType, Constraint))
-> ADTType
-> OmdADT
-> (ADTType, Constraint)
forall a b. (a -> b) -> a -> b
$ Env -> OmdADT -> (ADTType, Constraint)
mkConstraint Env
e) ADTType
Generated [OmdADT]
sortdefs
  -- TODO: do we take newSort or origSort?
  Named (FORMULA f) -> Result (Named (FORMULA f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Named (FORMULA f) -> Result (Named (FORMULA f)))
-> Named (FORMULA f) -> Result (Named (FORMULA f))
forall a b. (a -> b) -> a -> b
$ FORMULA f -> [SORT] -> Named (FORMULA f)
forall f. FORMULA f -> [SORT] -> Named (FORMULA f)
toSortGenNamed ([Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax [Constraint]
cs (Bool -> FORMULA f) -> Bool -> FORMULA f
forall a b. (a -> b) -> a -> b
$ ADTType
t ADTType -> ADTType -> Bool
forall a. Eq a => a -> a -> Bool
== ADTType
Free) ([SORT] -> Named (FORMULA f)) -> [SORT] -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ (Constraint -> SORT) -> [Constraint] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> SORT
newSort [Constraint]
cs

mkConstraint :: Env -> OmdADT -> (ADTType, Constraint)
mkConstraint :: Env -> OmdADT -> (ADTType, Constraint)
mkConstraint e :: Env
e (ADTSortDef nm :: [Char]
nm t :: ADTType
t constrs :: [OmdADT]
constrs) =
    let s :: SORT
s = Env -> OMName -> SORT
lookupSort Env
e (OMName -> SORT) -> OMName -> SORT
forall a b. (a -> b) -> a -> b
$ [Char] -> OMName
mkSimpleName [Char]
nm
        l :: [(OP_SYMB, [Int])]
l = (OmdADT -> (OP_SYMB, [Int])) -> [OmdADT] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> SORT -> OmdADT -> (OP_SYMB, [Int])
mkConstructor Env
e SORT
s) [OmdADT]
constrs
    in (ADTType
t, SORT -> [(OP_SYMB, [Int])] -> SORT -> Constraint
Constraint SORT
s [(OP_SYMB, [Int])]
l SORT
s)

mkConstraint _ _ = [Char] -> (ADTType, Constraint)
forall a. HasCallStack => [Char] -> a
error "mkConstraint: Malformed ADT expression"

mkConstructor :: Env -> SORT -> OmdADT -> (OP_SYMB, [Int])
mkConstructor :: Env -> SORT -> OmdADT -> (OP_SYMB, [Int])
mkConstructor e :: Env
e s :: SORT
s (ADTConstr nm :: [Char]
nm args :: [OmdADT]
args) =
    let opn :: SORT
opn = [Char] -> SORT
nameToId ([Char] -> SORT) -> [Char] -> SORT
forall a b. (a -> b) -> a -> b
$ Env -> OMName -> [Char]
forall a. SigMapI a -> OMName -> [Char]
lookupNotation Env
e (OMName -> [Char]) -> OMName -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> OMName
mkSimpleName [Char]
nm
        l :: [SORT]
l = (OmdADT -> SORT) -> [OmdADT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> OmdADT -> SORT
mkArg Env
e) [OmdADT]
args
    in (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
opn (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
l SORT
s Range
nullRange) Range
nullRange, [0])


{- we have to create the name of this injection because we throw it away
during the export -}
mkConstructor e :: Env
e s :: SORT
s (ADTInsort (_, omn :: OMName
omn)) =
    let argsort :: SORT
argsort = Env -> OMName -> SORT
lookupSort Env
e OMName
omn
        opn :: SORT
opn = SORT -> SORT -> SORT
mkUniqueInjName SORT
argsort SORT
s
    in (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
opn (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT
argsort] SORT
s Range
nullRange) Range
nullRange, [0])

mkConstructor _ _ _ = [Char] -> (OP_SYMB, [Int])
forall a. HasCallStack => [Char] -> a
error "mkConstructor: Malformed ADT expression"

mkArg :: Env -> OmdADT -> SORT
mkArg :: Env -> OmdADT -> SORT
mkArg e :: Env
e (ADTArg oms :: OMElement
oms _) = [Char] -> Env -> OMElement -> SORT
lookupSortOMS "mkArg" Env
e OMElement
oms

mkArg _ _ = [Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "mkArg: Malformed ADT expression"


-- * Subsort Relation

omdocToSortRel :: Env -> [TCElement] -> Result (Rel.Rel SORT)
omdocToSortRel :: Env -> [TCElement] -> Result (Rel SORT)
omdocToSortRel e :: Env
e = (Rel SORT -> TCElement -> Result (Rel SORT))
-> Rel SORT -> [TCElement] -> Result (Rel SORT)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Env -> Rel SORT -> TCElement -> Result (Rel SORT)
addMaybeToSortRel Env
e) Rel SORT
forall a. Rel a
Rel.empty

addMaybeToSortRel :: Env -> Rel.Rel SORT -> TCElement -> Result (Rel.Rel SORT)
addMaybeToSortRel :: Env -> Rel SORT -> TCElement -> Result (Rel SORT)
addMaybeToSortRel e :: Env
e r :: Rel SORT
r (TCSymbol n :: [Char]
n (OMA [sof :: OMElement
sof, oms1 :: OMElement
oms1, oms2 :: OMElement
oms2]) Axiom _) =
    case [Char] -> Maybe ([Char], [[Char]])
nameDecode [Char]
n of
      Just ("ST", _)
          | OMElement
sof OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_subsortof ->
              let s1 :: SORT
s1 = [Char] -> Env -> OMElement -> SORT
lookupSortOMS "addMaybeToSortRel: s1" Env
e OMElement
oms1
                  s2 :: SORT
s2 = [Char] -> Env -> OMElement -> SORT
lookupSortOMS "addMaybeToSortRel: s2" Env
e OMElement
oms2
              in Rel SORT -> Result (Rel SORT)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rel SORT -> Result (Rel SORT)) -> Rel SORT -> Result (Rel SORT)
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertKeyOrPair SORT
s1 SORT
s2 Rel SORT
r
          | Bool
otherwise ->
              do
                () -> [Char] -> Range -> Result ()
forall a. a -> [Char] -> Range -> Result a
warning () ("Use of subsortof in a non ST Statement: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n)
                        Range
nullRange
                Rel SORT -> Result (Rel SORT)
forall (m :: * -> *) a. Monad m => a -> m a
return Rel SORT
r
      _ -> Rel SORT -> Result (Rel SORT)
forall (m :: * -> *) a. Monad m => a -> m a
return Rel SORT
r

addMaybeToSortRel _ r :: Rel SORT
r _ = Rel SORT -> Result (Rel SORT)
forall (m :: * -> *) a. Monad m => a -> m a
return Rel SORT
r


-- * Types

omdocToType :: Env -> OMElement -> Either OpType PredType
omdocToType :: Env -> OMElement -> Either OpType PredType
omdocToType e :: Env
e (OMA (c :: OMElement
c : args :: [OMElement]
args)) =
    let sorts :: [SORT]
sorts = (OMElement -> SORT) -> [OMElement] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Env -> OMElement -> SORT
lookupSortOMS "omdocToType" Env
e) [OMElement]
args
        opargs :: [SORT]
opargs = [SORT] -> [SORT]
forall a. [a] -> [a]
init [SORT]
sorts
        oprange :: SORT
oprange = [SORT] -> SORT
forall a. [a] -> a
last [SORT]
sorts
        res :: Either OpType PredType
res | OMElement
c OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_predtype = PredType -> Either OpType PredType
forall a b. b -> Either a b
Right (PredType -> Either OpType PredType)
-> PredType -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType [SORT]
sorts
            | OMElement
c OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_partialfuntype = OpType -> Either OpType PredType
forall a b. a -> Either a b
Left (OpType -> Either OpType PredType)
-> OpType -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Partial [SORT]
opargs SORT
oprange
            | OMElement
c OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_funtype = OpType -> Either OpType PredType
forall a b. a -> Either a b
Left (OpType -> Either OpType PredType)
-> OpType -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Total [SORT]
opargs SORT
oprange
            | Bool
otherwise = [Char] -> Either OpType PredType
forall a. HasCallStack => [Char] -> a
error ([Char] -> Either OpType PredType)
-> [Char] -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ "omdocToType: unknown type constructor: "
                          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
c
    in Either OpType PredType
res

omdocToType e :: Env
e oms :: OMElement
oms@(OMS _)
    | OMElement
oms OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_predtype = PredType -> Either OpType PredType
forall a b. b -> Either a b
Right (PredType -> Either OpType PredType)
-> PredType -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType []
    | Bool
otherwise = OpType -> Either OpType PredType
forall a b. a -> Either a b
Left (OpType -> Either OpType PredType)
-> OpType -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Total [] (SORT -> OpType) -> SORT -> OpType
forall a b. (a -> b) -> a -> b
$ [Char] -> Env -> OMElement -> SORT
lookupSortOMS "omdocToType" Env
e OMElement
oms

omdocToType _ ome :: OMElement
ome = [Char] -> Either OpType PredType
forall a. HasCallStack => [Char] -> a
error ([Char] -> Either OpType PredType)
-> [Char] -> Either OpType PredType
forall a b. (a -> b) -> a -> b
$ "omdocToType: Non-supported element: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
ome


-- * Terms and Formulas

type VarMap = Map.Map VAR SORT

type TermEnv = (Env, VarMap)

mkImplication, mkImplied, mkEquivalence
                 , mkNegation :: [FORMULA f] -> FORMULA f

mkImplication :: [FORMULA f] -> FORMULA f
mkImplication [x :: FORMULA f
x, y :: FORMULA f
y] = FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl FORMULA f
x FORMULA f
y
mkImplication _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed implication"
mkImplied :: [FORMULA f] -> FORMULA f
mkImplied [x :: FORMULA f
x, y :: FORMULA f
y] = Relation -> FORMULA f -> FORMULA f -> FORMULA f
forall f. Relation -> FORMULA f -> FORMULA f -> FORMULA f
mkRel Relation
RevImpl FORMULA f
x FORMULA f
y
mkImplied _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed if"
mkEquivalence :: [FORMULA f] -> FORMULA f
mkEquivalence [x :: FORMULA f
x, y :: FORMULA f
y] = FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv FORMULA f
x FORMULA f
y
mkEquivalence _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed equivalence"
mkNegation :: [FORMULA f] -> FORMULA f
mkNegation [x :: FORMULA f
x] = FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg FORMULA f
x
mkNegation _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed negation"

mkDefinedness, mkExistl_equation, mkStrong_equation
    :: [TERM f] -> FORMULA f

mkDefinedness :: [TERM f] -> FORMULA f
mkDefinedness [x :: TERM f
x] = TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
x Range
nullRange
mkDefinedness _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed definedness"
mkExistl_equation :: [TERM f] -> FORMULA f
mkExistl_equation [x :: TERM f
x, y :: TERM f
y] = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkExEq TERM f
x TERM f
y
mkExistl_equation _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed existl equation"
mkStrong_equation :: [TERM f] -> FORMULA f
mkStrong_equation [x :: TERM f
x, y :: TERM f
y] = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
x TERM f
y
mkStrong_equation _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed strong equation"

-- Quantification, Predication and Membership are handled inside omdocToFormula

-- Term construction functions
mkT2 :: (OMElement -> a) -> (OMElement -> b) -> (a -> b -> Range -> TERM f)
     -> [OMElement] -> TERM f
mkT2 :: (OMElement -> a)
-> (OMElement -> b)
-> (a -> b -> Range -> TERM f)
-> [OMElement]
-> TERM f
mkT2 f :: OMElement -> a
f g :: OMElement -> b
g c :: a -> b -> Range -> TERM f
c l :: [OMElement]
l = case [OMElement]
l of
                 [x :: OMElement
x, y :: OMElement
y] -> a -> b -> Range -> TERM f
c (OMElement -> a
f OMElement
x) (OMElement -> b
g OMElement
y) Range
nullRange
                 _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error "mkT2: 2 arguments expected"

mkT3 :: (OMElement -> a) -> (OMElement -> b) -> (OMElement -> c)
     -> (a -> b -> c -> Range -> TERM f) -> [OMElement] -> TERM f
mkT3 :: (OMElement -> a)
-> (OMElement -> b)
-> (OMElement -> c)
-> (a -> b -> c -> Range -> TERM f)
-> [OMElement]
-> TERM f
mkT3 f :: OMElement -> a
f g :: OMElement -> b
g h :: OMElement -> c
h c :: a -> b -> c -> Range -> TERM f
c l :: [OMElement]
l = case [OMElement]
l of
                   [x :: OMElement
x, y :: OMElement
y, z :: OMElement
z] -> a -> b -> c -> Range -> TERM f
c (OMElement -> a
f OMElement
x) (OMElement -> b
g OMElement
y) (OMElement -> c
h OMElement
z) Range
nullRange
                   _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error "mkT3: 3 arguments expected"


-- Formula construction functions
mkFF :: TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF :: TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF e :: TermEnv
e f :: [FORMULA f] -> FORMULA f
f l :: [OMElement]
l = [FORMULA f] -> FORMULA f
f ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (OMElement -> FORMULA f) -> [OMElement] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (TermEnv -> OMElement -> FORMULA f
forall f. TermEnv -> OMElement -> FORMULA f
omdocToFormula' TermEnv
e) [OMElement]
l

mkTF :: TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF :: TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF e :: TermEnv
e f :: [TERM f] -> FORMULA f
f l :: [OMElement]
l = [TERM f] -> FORMULA f
f ([TERM f] -> FORMULA f) -> [TERM f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (OMElement -> TERM f) -> [OMElement] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e) [OMElement]
l

getQuantifier :: OMElement -> QUANTIFIER
getQuantifier :: OMElement -> QUANTIFIER
getQuantifier oms :: OMElement
oms
    | OMElement
oms OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_forall = QUANTIFIER
Universal
    | OMElement
oms OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_exists = QUANTIFIER
Existential
    | OMElement
oms OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_existsunique = QUANTIFIER
Unique_existential
    | Bool
otherwise = [Char] -> QUANTIFIER
forall a. HasCallStack => [Char] -> a
error ([Char] -> QUANTIFIER) -> [Char] -> QUANTIFIER
forall a b. (a -> b) -> a -> b
$ "getQuantifier: unrecognized quantifier " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
oms

mkBinder :: TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f
mkBinder :: TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f
mkBinder te :: TermEnv
te@(e :: Env
e, _) q :: QUANTIFIER
q vars :: [OMElement]
vars body :: OMElement
body =
    let (vm' :: VarMap
vm', vardecls :: [VAR_DECL]
vardecls) = TermEnv -> [OMElement] -> (VarMap, [VAR_DECL])
toVarDecls TermEnv
te [OMElement]
vars
        bd :: FORMULA f
bd = TermEnv -> OMElement -> FORMULA f
forall f. TermEnv -> OMElement -> FORMULA f
omdocToFormula' (Env
e, VarMap
vm') OMElement
body
    in QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vardecls FORMULA f
forall f. FORMULA f
bd Range
nullRange

toVarDecls :: TermEnv -> [OMElement] -> (VarMap, [VAR_DECL])
toVarDecls :: TermEnv -> [OMElement] -> (VarMap, [VAR_DECL])
toVarDecls (e :: Env
e, vm :: VarMap
vm) l :: [OMElement]
l =
    let f :: VarMap -> OMElement -> (VarMap, (VAR, SORT))
f acc :: VarMap
acc x :: OMElement
x = let (v :: VAR
v, s :: SORT
s) = Env -> OMElement -> (VAR, SORT)
toVarDecl Env
e OMElement
x
                      acc' :: VarMap
acc' = VAR -> SORT -> VarMap -> VarMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
v SORT
s VarMap
acc
                  in (VarMap
acc', (VAR
v, SORT
s))
        (vm' :: VarMap
vm', l' :: [(VAR, SORT)]
l') = (VarMap -> OMElement -> (VarMap, (VAR, SORT)))
-> VarMap -> [OMElement] -> (VarMap, [(VAR, SORT)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL VarMap -> OMElement -> (VarMap, (VAR, SORT))
f VarMap
vm [OMElement]
l
        -- group by same sort
        l'' :: [[(VAR, SORT)]]
l'' = ((VAR, SORT) -> (VAR, SORT) -> Bool)
-> [(VAR, SORT)] -> [[(VAR, SORT)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
(==) (SORT -> SORT -> Bool)
-> ((VAR, SORT) -> SORT) -> (VAR, SORT) -> (VAR, SORT) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`Data.Function.on` (VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd) [(VAR, SORT)]
l'
        -- the lists returned by groupBy are never empty, so head will succeed
        g :: [(VAR, SORT)] -> VAR_DECL
g vsl :: [(VAR, SORT)]
vsl = [VAR] -> SORT -> Range -> VAR_DECL
Var_decl (((VAR, SORT) -> VAR) -> [(VAR, SORT)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, SORT) -> VAR
forall a b. (a, b) -> a
fst [(VAR, SORT)]
vsl) ((VAR, SORT) -> SORT
forall a b. (a, b) -> b
snd ((VAR, SORT) -> SORT) -> (VAR, SORT) -> SORT
forall a b. (a -> b) -> a -> b
$ [(VAR, SORT)] -> (VAR, SORT)
forall a. [a] -> a
head [(VAR, SORT)]
vsl) Range
nullRange
    in (VarMap
vm', ([(VAR, SORT)] -> VAR_DECL) -> [[(VAR, SORT)]] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map [(VAR, SORT)] -> VAR_DECL
g [[(VAR, SORT)]]
l'')

-- in CASL we expect all bound vars to be attributed (typed)
toVarDecl :: Env -> OMElement -> (VAR, SORT)
toVarDecl :: Env -> OMElement -> (VAR, SORT)
toVarDecl e :: Env
e (OMATTT (OMV v :: OMName
v) (OMAttr ct :: OMElement
ct t :: OMElement
t))
    | OMElement
ct OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_type = ([Char] -> VAR
nameToToken ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ OMName -> [Char]
name OMName
v, [Char] -> Env -> OMElement -> SORT
lookupSortOMS "toVarDecl" Env
e OMElement
t)
    | Bool
otherwise = [Char] -> (VAR, SORT)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (VAR, SORT)) -> [Char] -> (VAR, SORT)
forall a b. (a -> b) -> a -> b
$ "toVarDecl: unrecognized attribution " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
ct

toVarDecl _ _ = [Char] -> (VAR, SORT)
forall a. HasCallStack => [Char] -> a
error "toVarDecl: bound variables should be attributed."

-- Toplevel entry point
omdocToFormula :: Env -> OMElement -> FORMULA f
omdocToFormula :: Env -> OMElement -> FORMULA f
omdocToFormula e :: Env
e = TermEnv -> OMElement -> FORMULA f
forall f. TermEnv -> OMElement -> FORMULA f
omdocToFormula' (Env
e, VarMap
forall k a. Map k a
Map.empty)


-- Functions with given VarMap

-- omdocToTerm has no toplevel entry point
omdocToTerm' :: TermEnv -> OMElement -> TERM f
omdocToTerm' :: TermEnv -> OMElement -> TERM f
omdocToTerm' e :: TermEnv
e@(ie :: Env
ie, vm :: VarMap
vm) f :: OMElement
f =
    case OMElement
f of
      OMA (h :: OMElement
h : args :: [OMElement]
args)
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_cast ->
              (OMElement -> TERM f)
-> (OMElement -> SORT)
-> (TERM f -> SORT -> Range -> TERM f)
-> [OMElement]
-> TERM f
forall a b f.
(OMElement -> a)
-> (OMElement -> b)
-> (a -> b -> Range -> TERM f)
-> [OMElement]
-> TERM f
mkT2 (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e) ([Char] -> Env -> OMElement -> SORT
lookupSortOMS "omdocToTerm: Cast" Env
ie)
                   TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Cast [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_if ->
              (OMElement -> TERM f)
-> (OMElement -> FORMULA f)
-> (OMElement -> TERM f)
-> (TERM f -> FORMULA f -> TERM f -> Range -> TERM f)
-> [OMElement]
-> TERM f
forall a b c f.
(OMElement -> a)
-> (OMElement -> b)
-> (OMElement -> c)
-> (a -> b -> c -> Range -> TERM f)
-> [OMElement]
-> TERM f
mkT3 (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e) (TermEnv -> OMElement -> FORMULA f
forall f. TermEnv -> OMElement -> FORMULA f
omdocToFormula' TermEnv
e) (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e)
                   TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional [OMElement]
args
          -- all other heads mean application
          | Bool
otherwise ->
              let os :: OP_SYMB
os = (SORT, OpType) -> OP_SYMB
toOpSymb ((SORT, OpType) -> OP_SYMB) -> (SORT, OpType) -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ [Char] -> Env -> OMElement -> (SORT, OpType)
lookupOpOMS "omdocToTerm" Env
ie OMElement
h
                  args' :: [TERM f]
args' = (OMElement -> TERM f) -> [OMElement] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e) [OMElement]
args
              in OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os [TERM f]
forall f. [TERM f]
args' Range
nullRange
      OMS _ -> let os :: OP_SYMB
os = (SORT, OpType) -> OP_SYMB
toOpSymb ((SORT, OpType) -> OP_SYMB) -> (SORT, OpType) -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ [Char] -> Env -> OMElement -> (SORT, OpType)
lookupOpOMS "omdocToTerm-OMS:" Env
ie OMElement
f
               in OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os [] Range
nullRange
      OMV omn :: OMName
omn -> let var :: VAR
var = [Char] -> VAR
nameToToken ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ OMName -> [Char]
name OMName
omn
                     -- lookup the type of the variable in the varmap
                     s :: SORT
s = SORT -> VAR -> VarMap -> SORT
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                         ([Char] -> SORT
forall a. HasCallStack => [Char] -> a
error ([Char] -> SORT) -> [Char] -> SORT
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "omdocToTerm': Variable not in "
                                         , "varmap: ", VAR -> [Char]
forall a. Show a => a -> [Char]
show VAR
var ]) VAR
var VarMap
vm
                 in VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
var SORT
s Range
nullRange
      OMATTT ome :: OMElement
ome (OMAttr ct :: OMElement
ct t :: OMElement
t)
          | OMElement
ct OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_type ->
              -- same as cast
              (OMElement -> TERM f)
-> (OMElement -> SORT)
-> (TERM f -> SORT -> Range -> TERM f)
-> [OMElement]
-> TERM f
forall a b f.
(OMElement -> a)
-> (OMElement -> b)
-> (a -> b -> Range -> TERM f)
-> [OMElement]
-> TERM f
mkT2 (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e) ([Char] -> Env -> OMElement -> SORT
lookupSortOMS "omdocToTerm: Sorted" Env
ie)
                   TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term [OMElement
ome, OMElement
t]
          | Bool
otherwise -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error ([Char] -> TERM f) -> [Char] -> TERM f
forall a b. (a -> b) -> a -> b
$ "omdocToTerm: unrecognized attribution "
                         [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
ct
      _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error ([Char] -> TERM f) -> [Char] -> TERM f
forall a b. (a -> b) -> a -> b
$ "omdocToTerm: no valid term " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
f


omdocToFormula' :: TermEnv -> OMElement -> FORMULA f
omdocToFormula' :: TermEnv -> OMElement -> FORMULA f
omdocToFormula' e :: TermEnv
e@(ie :: Env
ie, _) f :: OMElement
f =
    case OMElement
f of
      OMA (h :: OMElement
h : args :: [OMElement]
args)
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_in ->
              case [OMElement]
args of
                [x :: OMElement
x, s :: OMElement
s] ->
                    TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership (TermEnv -> OMElement -> TERM f
forall f. TermEnv -> OMElement -> TERM f
omdocToTerm' TermEnv
e OMElement
x) ([Char] -> Env -> OMElement -> SORT
lookupSortOMS
                                                   "omdocToFormula"
                                                  Env
ie OMElement
s) Range
nullRange
                _ -> [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "Malformed membership"
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_and ->
              TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF TermEnv
e [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_or ->
              TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF TermEnv
e [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
disjunct [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_implies ->
              TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF TermEnv
e [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
mkImplication [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_implied ->
              TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF TermEnv
e [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
mkImplied [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_equivalent ->
              TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF TermEnv
e [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
mkEquivalence [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_not ->
              TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([FORMULA f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkFF TermEnv
e [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
mkNegation [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_def ->
              TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF TermEnv
e [TERM f] -> FORMULA f
forall f. [TERM f] -> FORMULA f
mkDefinedness [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_eeq ->
              TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF TermEnv
e [TERM f] -> FORMULA f
forall f. [TERM f] -> FORMULA f
mkExistl_equation [OMElement]
args
          | OMElement
h OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_eq ->
              TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF TermEnv
e [TERM f] -> FORMULA f
forall f. [TERM f] -> FORMULA f
mkStrong_equation [OMElement]
args
          -- all other heads mean predication
          | Bool
otherwise ->
              let ps :: PRED_SYMB
ps = (SORT, PredType) -> PRED_SYMB
toPredSymb ((SORT, PredType) -> PRED_SYMB) -> (SORT, PredType) -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [Char] -> Env -> OMElement -> (SORT, PredType)
lookupPredOMS "omdocToFormula" Env
ie OMElement
h
                  g :: [TERM f] -> FORMULA f
g l :: [TERM f]
l = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
ps [TERM f]
l Range
nullRange in
              TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
forall f.
TermEnv -> ([TERM f] -> FORMULA f) -> [OMElement] -> FORMULA f
mkTF TermEnv
e [TERM f] -> FORMULA f
forall f. [TERM f] -> FORMULA f
g [OMElement]
args

      OMBIND binder :: OMElement
binder args :: [OMElement]
args body :: OMElement
body ->
          TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f
forall f.
TermEnv -> QUANTIFIER -> [OMElement] -> OMElement -> FORMULA f
mkBinder TermEnv
e (OMElement -> QUANTIFIER
getQuantifier OMElement
binder) [OMElement]
args OMElement
body

      OMS _ | OMElement
f OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_true -> FORMULA f
forall f. FORMULA f
trueForm
            | OMElement
f OMElement -> OMElement -> Bool
forall a. Eq a => a -> a -> Bool
== OMElement
const_false -> FORMULA f
forall f. FORMULA f
falseForm
            -- Propositional Constants (0-ary predicates):
            | Bool
otherwise ->
                PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication ((SORT, PredType) -> PRED_SYMB
toPredSymb
                             ((SORT, PredType) -> PRED_SYMB) -> (SORT, PredType) -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [Char] -> Env -> OMElement -> (SORT, PredType)
lookupPredOMS
                                   ("omdocToFormula: can't handle constant "
                                    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
f) Env
ie OMElement
f) [] Range
nullRange
      _ -> [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error ([Char] -> FORMULA f) -> [Char] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ "omdocToFormula: no valid formula " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OMElement -> [Char]
forall a. Show a => a -> [Char]
show OMElement
f