{- |
Module      :  ./CASL/ToSExpr.hs
Description :  translate CASL to S-Expressions
Copyright   :  (c) C. Maeder, DFKI 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

translation of CASL to S-Expressions
-}

module CASL.ToSExpr where

import CASL.Fold
import CASL.Morphism
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Quantification

import Common.SExpr
import Common.Result
import Common.Id
import qualified Common.Lib.MapSet as MapSet

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

predToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
predToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
predToSSymbol sign :: Sign f e
sign p :: PRED_SYMB
p = case PRED_SYMB
p of
    Pred_name _ -> [Char] -> SExpr
forall a. HasCallStack => [Char] -> a
error "predToSSymbol"
    Qual_pred_name i :: PRED_NAME
i t :: PRED_TYPE
t _ -> Sign f e -> PRED_NAME -> PredType -> SExpr
forall f e. Sign f e -> PRED_NAME -> PredType -> SExpr
predIdToSSymbol Sign f e
sign PRED_NAME
i (PredType -> SExpr) -> PredType -> SExpr
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> PredType
toPredType PRED_TYPE
t

predIdToSSymbol :: Sign f e -> Id -> PredType -> SExpr
predIdToSSymbol :: Sign f e -> PRED_NAME -> PredType -> SExpr
predIdToSSymbol sign :: Sign f e
sign i :: PRED_NAME
i t :: PredType
t =
    case PredType -> [PredType] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex PredType
t ([PredType] -> Maybe Int)
-> (MapSet PRED_NAME PredType -> [PredType])
-> MapSet PRED_NAME PredType
-> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList (Set PredType -> [PredType])
-> (MapSet PRED_NAME PredType -> Set PredType)
-> MapSet PRED_NAME PredType
-> [PredType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_NAME -> MapSet PRED_NAME PredType -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup PRED_NAME
i (MapSet PRED_NAME PredType -> Maybe Int)
-> MapSet PRED_NAME PredType -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap Sign f e
sign of
      Nothing -> [Char] -> SExpr
forall a. HasCallStack => [Char] -> a
error "predIdToSSymbol"
      Just n :: Int
n -> Int -> PRED_NAME -> SExpr
idToSSymbol (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) PRED_NAME
i

opToSSymbol :: Sign f e -> OP_SYMB -> SExpr
opToSSymbol :: Sign f e -> OP_SYMB -> SExpr
opToSSymbol sign :: Sign f e
sign o :: OP_SYMB
o = case OP_SYMB
o of
    Op_name _ -> [Char] -> SExpr
forall a. HasCallStack => [Char] -> a
error "opToSSymbol"
    Qual_op_name i :: PRED_NAME
i t :: OP_TYPE
t _ -> Sign f e -> PRED_NAME -> OpType -> SExpr
forall f e. Sign f e -> PRED_NAME -> OpType -> SExpr
opIdToSSymbol Sign f e
sign PRED_NAME
i (OpType -> SExpr) -> OpType -> SExpr
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
t

opIdToSSymbol :: Sign f e -> Id -> OpType -> SExpr
opIdToSSymbol :: Sign f e -> PRED_NAME -> OpType -> SExpr
opIdToSSymbol sign :: Sign f e
sign i :: PRED_NAME
i t :: OpType
t = case (OpType -> Bool) -> [OpType] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex
      (([PRED_NAME] -> [PRED_NAME] -> Bool)
-> (OpType -> [PRED_NAME]) -> OpType -> OpType -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on [PRED_NAME] -> [PRED_NAME] -> Bool
forall a. Eq a => a -> a -> Bool
(==) OpType -> [PRED_NAME]
opSorts OpType
t) ([OpType] -> Maybe Int)
-> (MapSet PRED_NAME OpType -> [OpType])
-> MapSet PRED_NAME OpType
-> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList
      (Set OpType -> [OpType])
-> (MapSet PRED_NAME OpType -> Set OpType)
-> MapSet PRED_NAME OpType
-> [OpType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_NAME -> MapSet PRED_NAME OpType -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup PRED_NAME
i (MapSet PRED_NAME OpType -> Maybe Int)
-> MapSet PRED_NAME OpType -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap Sign f e
sign of
        Nothing -> [Char] -> SExpr
forall a. HasCallStack => [Char] -> a
error ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ "opIdToSSymbol " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PRED_NAME -> [Char]
forall a. Show a => a -> [Char]
show PRED_NAME
i
        Just n :: Int
n -> Int -> PRED_NAME -> SExpr
idToSSymbol (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) PRED_NAME
i

sortToSSymbol :: Id -> SExpr
sortToSSymbol :: PRED_NAME -> SExpr
sortToSSymbol = Int -> PRED_NAME -> SExpr
idToSSymbol 0

varToSSymbol :: Token -> SExpr
varToSSymbol :: Token -> SExpr
varToSSymbol = [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> (Token -> [Char]) -> Token -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> [Char]
transToken

varDeclToSExpr :: (VAR, SORT) -> SExpr
varDeclToSExpr :: (Token, PRED_NAME) -> SExpr
varDeclToSExpr (v :: Token
v, s :: PRED_NAME
s) =
  [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "vardecl-indet", Token -> SExpr
varToSSymbol Token
v, PRED_NAME -> SExpr
sortToSSymbol PRED_NAME
s]

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

sRec :: GetRange f => Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
sRec :: Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
sRec sign :: Sign a e
sign mf :: f -> SExpr
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 -> PRED_NAME -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> PRED_NAME -> OP_TYPE -> a -> a)
-> (FORMULA f -> PRED_NAME -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> Token -> PRED_NAME -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> PRED_NAME -> Range -> b)
-> (TERM f -> b -> PRED_NAME -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> Token -> b)
-> (TERM f -> PRED_NAME -> Range -> b)
-> (TERM f -> PRED_NAME -> 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] -> SExpr -> Range -> SExpr
foldQuantification = \ _ q :: QUANTIFIER
q vs :: [VAR_DECL]
vs f :: SExpr
f _ ->
        let s :: SExpr
s = [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ case QUANTIFIER
q of
              Universal -> "all"
              Existential -> "ex"
              Unique_existential -> "ex1"
            vl :: SExpr
vl = [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ ((Token, PRED_NAME) -> SExpr) -> [(Token, PRED_NAME)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Token, PRED_NAME) -> SExpr
varDeclToSExpr ([(Token, PRED_NAME)] -> [SExpr])
-> [(Token, PRED_NAME)] -> [SExpr]
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, PRED_NAME)]
flatVAR_DECLs [VAR_DECL]
vs
        in [SExpr] -> SExpr
SList [SExpr
s, SExpr
vl, SExpr
f]
    , foldJunction :: FORMULA f -> Junctor -> [SExpr] -> Range -> SExpr
foldJunction = \ _ j :: Junctor
j fs :: [SExpr]
fs _ -> [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol (case Junctor
j of
        Con -> "and"
        Dis -> "or") SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
fs
    , foldRelation :: FORMULA f -> SExpr -> Relation -> SExpr -> Range -> SExpr
foldRelation = \ _ f1 :: SExpr
f1 c :: Relation
c f2 :: SExpr
f2 _ -> [SExpr] -> SExpr
SList
        [ [Char] -> SExpr
SSymbol (if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence then "equiv" else "implies"), SExpr
f1, SExpr
f2]
    , foldNegation :: FORMULA f -> SExpr -> Range -> SExpr
foldNegation = \ _ f :: SExpr
f _ -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "not", SExpr
f]
    , foldAtom :: FORMULA f -> Bool -> Range -> SExpr
foldAtom = \ _ b :: Bool
b _ -> [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ if Bool
b then "true" else "false"
    , foldPredication :: FORMULA f -> PRED_SYMB -> [SExpr] -> Range -> SExpr
foldPredication = \ _ p :: PRED_SYMB
p ts :: [SExpr]
ts _ ->
        [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "papply" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign a e -> PRED_SYMB -> SExpr
forall f e. Sign f e -> PRED_SYMB -> SExpr
predToSSymbol Sign a e
sign PRED_SYMB
p SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
ts
    , foldDefinedness :: FORMULA f -> SExpr -> Range -> SExpr
foldDefinedness = \ _ t :: SExpr
t _ -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "def", SExpr
t]
    , foldEquation :: FORMULA f -> SExpr -> Equality -> SExpr -> Range -> SExpr
foldEquation = \ _ t1 :: SExpr
t1 e :: Equality
e t2 :: SExpr
t2 _ -> [SExpr] -> SExpr
SList
        [ [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ if Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Existl then "eeq" else "eq", SExpr
t1, SExpr
t2]
    , foldMembership :: FORMULA f -> SExpr -> PRED_NAME -> Range -> SExpr
foldMembership = \ _ t :: SExpr
t s :: PRED_NAME
s _ ->
        [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "member", SExpr
t, PRED_NAME -> SExpr
sortToSSymbol PRED_NAME
s]
    , foldMixfix_formula :: FORMULA f -> SExpr -> SExpr
foldMixfix_formula = \ t :: FORMULA f
t _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_formula" (Range -> SExpr) -> Range -> SExpr
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange FORMULA f
t
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> SExpr
foldSort_gen_ax = \ _ cs :: [Constraint]
cs b :: Bool
b ->
      let (srts :: [PRED_NAME]
srts, ops :: [OP_SYMB]
ops, _) = [Constraint] -> ([PRED_NAME], [OP_SYMB], [(PRED_NAME, PRED_NAME)])
recover_Sort_gen_ax [Constraint]
cs in
      [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol ((if Bool
b then "freely-" else "") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "generated")
        SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (case [PRED_NAME]
srts of
            [s :: PRED_NAME
s] -> PRED_NAME -> SExpr
sortToSSymbol PRED_NAME
s
            _ -> [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (PRED_NAME -> SExpr) -> [PRED_NAME] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map PRED_NAME -> SExpr
sortToSSymbol [PRED_NAME]
srts)
        SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (OP_SYMB -> SExpr) -> [OP_SYMB] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Sign a e -> OP_SYMB -> SExpr
forall f e. Sign f e -> OP_SYMB -> SExpr
opToSSymbol Sign a e
sign) [OP_SYMB]
ops
    , foldQuantOp :: FORMULA f -> PRED_NAME -> OP_TYPE -> SExpr -> SExpr
foldQuantOp = \ _ o :: PRED_NAME
o _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail ("QuantOp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PRED_NAME -> [Char]
forall a. Show a => a -> [Char]
show PRED_NAME
o) (Range -> SExpr) -> Range -> SExpr
forall a b. (a -> b) -> a -> b
$ PRED_NAME -> Range
forall a. GetRange a => a -> Range
getRange PRED_NAME
o
    , foldQuantPred :: FORMULA f -> PRED_NAME -> PRED_TYPE -> SExpr -> SExpr
foldQuantPred = \ _ p :: PRED_NAME
p _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail ("QuantPred " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PRED_NAME -> [Char]
forall a. Show a => a -> [Char]
show PRED_NAME
p) (Range -> SExpr) -> Range -> SExpr
forall a b. (a -> b) -> a -> b
$ PRED_NAME -> Range
forall a. GetRange a => a -> Range
getRange PRED_NAME
p
    , foldExtFORMULA :: FORMULA f -> f -> SExpr
foldExtFORMULA = (f -> SExpr) -> FORMULA f -> f -> SExpr
forall a b. a -> b -> a
const f -> SExpr
mf
    , foldQual_var :: TERM f -> Token -> PRED_NAME -> Range -> SExpr
foldQual_var = \ _ v :: Token
v _ _ ->
        [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "varterm", Token -> SExpr
varToSSymbol Token
v]
    , foldApplication :: TERM f -> OP_SYMB -> [SExpr] -> Range -> SExpr
foldApplication = \ _ o :: OP_SYMB
o ts :: [SExpr]
ts _ ->
        [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "fapply" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign a e -> OP_SYMB -> SExpr
forall f e. Sign f e -> OP_SYMB -> SExpr
opToSSymbol Sign a e
sign OP_SYMB
o SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
ts
    , foldSorted_term :: TERM f -> SExpr -> PRED_NAME -> Range -> SExpr
foldSorted_term = \ _ r :: SExpr
r _ _ -> SExpr
r
    , foldCast :: TERM f -> SExpr -> PRED_NAME -> Range -> SExpr
foldCast = \ _ t :: SExpr
t s :: PRED_NAME
s _ -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "cast", SExpr
t, PRED_NAME -> SExpr
sortToSSymbol PRED_NAME
s]
    , foldConditional :: TERM f -> SExpr -> SExpr -> SExpr -> Range -> SExpr
foldConditional = \ _ e :: SExpr
e f :: SExpr
f t :: SExpr
t _ -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "condition", SExpr
e, SExpr
f, SExpr
t]
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> SExpr
foldMixfix_qual_pred = \ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_qual_pred" (Range -> SExpr) -> (PRED_SYMB -> Range) -> PRED_SYMB -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_SYMB -> Range
forall a. GetRange a => a -> Range
getRange
    , foldMixfix_term :: TERM f -> [SExpr] -> SExpr
foldMixfix_term = \ t :: TERM f
t _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_term" (Range -> SExpr) -> Range -> SExpr
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 -> SExpr
foldMixfix_token = \ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_token" (Range -> SExpr) -> (Token -> Range) -> Token -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Range
tokPos
    , foldMixfix_sorted_term :: TERM f -> PRED_NAME -> Range -> SExpr
foldMixfix_sorted_term = \ _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_sorted_term"
    , foldMixfix_cast :: TERM f -> PRED_NAME -> Range -> SExpr
foldMixfix_cast = \ _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_cast"
    , foldMixfix_parenthesized :: TERM f -> [SExpr] -> Range -> SExpr
foldMixfix_parenthesized = \ _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_parenthesized"
    , foldMixfix_bracketed :: TERM f -> [SExpr] -> Range -> SExpr
foldMixfix_bracketed = \ _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_bracketed"
    , foldMixfix_braced :: TERM f -> [SExpr] -> Range -> SExpr
foldMixfix_braced = \ _ _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Mixfix_braced"
    , foldExtTERM :: TERM f -> f -> SExpr
foldExtTERM = (f -> SExpr) -> TERM f -> f -> SExpr
forall a b. a -> b -> a
const f -> SExpr
mf }

signToSExprs :: Sign a e -> [SExpr]
signToSExprs :: Sign a e -> [SExpr]
signToSExprs sign :: Sign a e
sign = Sign a e -> SExpr
forall a e. Sign a e -> SExpr
sortSignToSExprs Sign a e
sign
  SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign a e -> MapSet PRED_NAME PredType -> [SExpr]
forall a e. Sign a e -> MapSet PRED_NAME PredType -> [SExpr]
predMapToSExprs Sign a e
sign (Sign a e -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap Sign a e
sign) [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ Sign a e -> MapSet PRED_NAME OpType -> [SExpr]
forall a e. Sign a e -> MapSet PRED_NAME OpType -> [SExpr]
opMapToSExprs Sign a e
sign (Sign a e -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap Sign a e
sign)

sortSignToSExprs :: Sign a e -> SExpr
sortSignToSExprs :: Sign a e -> SExpr
sortSignToSExprs sign :: Sign a e
sign =
    [SExpr] -> SExpr
SList ([Char] -> SExpr
SSymbol "sorts"
      SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (PRED_NAME -> SExpr) -> [PRED_NAME] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map PRED_NAME -> SExpr
sortToSSymbol (Set PRED_NAME -> [PRED_NAME]
forall a. Set a -> [a]
Set.toList (Set PRED_NAME -> [PRED_NAME]) -> Set PRED_NAME -> [PRED_NAME]
forall a b. (a -> b) -> a -> b
$ Sign a e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign a e
sign))

predMapToSExprs :: Sign a e -> PredMap -> [SExpr]
predMapToSExprs :: Sign a e -> MapSet PRED_NAME PredType -> [SExpr]
predMapToSExprs sign :: Sign a e
sign =
    ((PRED_NAME, PredType) -> SExpr)
-> [(PRED_NAME, PredType)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: PRED_NAME
p, t :: PredType
t) ->
       [SExpr] -> SExpr
SList [ [Char] -> SExpr
SSymbol "predicate"
             , Sign a e -> PRED_NAME -> PredType -> SExpr
forall f e. Sign f e -> PRED_NAME -> PredType -> SExpr
predIdToSSymbol Sign a e
sign PRED_NAME
p PredType
t
             , [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (PRED_NAME -> SExpr) -> [PRED_NAME] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map PRED_NAME -> SExpr
sortToSSymbol ([PRED_NAME] -> [SExpr]) -> [PRED_NAME] -> [SExpr]
forall a b. (a -> b) -> a -> b
$ PredType -> [PRED_NAME]
predArgs PredType
t ])
      ([(PRED_NAME, PredType)] -> [SExpr])
-> (MapSet PRED_NAME PredType -> [(PRED_NAME, PredType)])
-> MapSet PRED_NAME PredType
-> [SExpr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet PRED_NAME PredType -> [(PRED_NAME, PredType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList

opMapToSExprs :: Sign a e -> OpMap -> [SExpr]
opMapToSExprs :: Sign a e -> MapSet PRED_NAME OpType -> [SExpr]
opMapToSExprs sign :: Sign a e
sign =
    ((PRED_NAME, OpType) -> SExpr) -> [(PRED_NAME, OpType)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: PRED_NAME
p, t :: OpType
t) ->
       [SExpr] -> SExpr
SList [ [Char] -> SExpr
SSymbol "function"
             , Sign a e -> PRED_NAME -> OpType -> SExpr
forall f e. Sign f e -> PRED_NAME -> OpType -> SExpr
opIdToSSymbol Sign a e
sign PRED_NAME
p OpType
t
             , [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (PRED_NAME -> SExpr) -> [PRED_NAME] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map PRED_NAME -> SExpr
sortToSSymbol ([PRED_NAME] -> [SExpr]) -> [PRED_NAME] -> [SExpr]
forall a b. (a -> b) -> a -> b
$ OpType -> [PRED_NAME]
opArgs OpType
t
             , PRED_NAME -> SExpr
sortToSSymbol (PRED_NAME -> SExpr) -> PRED_NAME -> SExpr
forall a b. (a -> b) -> a -> b
$ OpType -> PRED_NAME
opRes OpType
t ])
      ([(PRED_NAME, OpType)] -> [SExpr])
-> (MapSet PRED_NAME OpType -> [(PRED_NAME, OpType)])
-> MapSet PRED_NAME OpType
-> [SExpr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet PRED_NAME OpType -> [(PRED_NAME, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList

morToSExprs :: Morphism f e m -> [SExpr]
morToSExprs :: Morphism f e m -> [SExpr]
morToSExprs m :: Morphism f e m
m =
  let src :: Sign f e
src = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m
      tar :: Sign f e
tar = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
m
      sm :: Sort_map
sm = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m
  in ((PRED_NAME, PRED_NAME) -> SExpr)
-> [(PRED_NAME, PRED_NAME)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: PRED_NAME
s, t :: PRED_NAME
t) -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "map", PRED_NAME -> SExpr
sortToSSymbol PRED_NAME
s, PRED_NAME -> SExpr
sortToSSymbol PRED_NAME
t])
     (Sort_map -> [(PRED_NAME, PRED_NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList Sort_map
sm)
     [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ (PRED_NAME -> Set OpType -> [SExpr] -> [SExpr])
-> [SExpr] -> Map PRED_NAME (Set OpType) -> [SExpr]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: PRED_NAME
i s :: Set OpType
s -> case Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
s of
          [] -> [SExpr] -> [SExpr]
forall a. a -> a
id
          ot :: OpType
ot : _ -> let (j :: PRED_NAME
j, nt :: OpType
nt) = Sort_map -> Op_map -> (PRED_NAME, OpType) -> (PRED_NAME, OpType)
mapOpSym Sort_map
sm (Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m) (PRED_NAME
i, OpType
ot) in
             if PRED_NAME
i PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
j then [SExpr] -> [SExpr]
forall a. a -> a
id else
               ([SExpr] -> SExpr
SList [ [Char] -> SExpr
SSymbol "map", Sign f e -> PRED_NAME -> OpType -> SExpr
forall f e. Sign f e -> PRED_NAME -> OpType -> SExpr
opIdToSSymbol Sign f e
src PRED_NAME
i OpType
ot
                      , Sign f e -> PRED_NAME -> OpType -> SExpr
forall f e. Sign f e -> PRED_NAME -> OpType -> SExpr
opIdToSSymbol Sign f e
tar PRED_NAME
j OpType
nt] SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
:)) []
        (MapSet PRED_NAME OpType -> Map PRED_NAME (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet PRED_NAME OpType -> Map PRED_NAME (Set OpType))
-> MapSet PRED_NAME OpType -> Map PRED_NAME (Set OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet PRED_NAME OpType
forall f e. Sign f e -> MapSet PRED_NAME OpType
opMap Sign f e
src)
     [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ (PRED_NAME -> Set PredType -> [SExpr] -> [SExpr])
-> [SExpr] -> Map PRED_NAME (Set PredType) -> [SExpr]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: PRED_NAME
i s :: Set PredType
s -> case Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
s of
          [] -> [SExpr] -> [SExpr]
forall a. a -> a
id
          ot :: PredType
ot : _ -> let (j :: PRED_NAME
j, nt :: PredType
nt) = Sort_map
-> Pred_map -> (PRED_NAME, PredType) -> (PRED_NAME, PredType)
mapPredSym Sort_map
sm (Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m) (PRED_NAME
i, PredType
ot) in
             if PRED_NAME
i PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
j then [SExpr] -> [SExpr]
forall a. a -> a
id else
               ([SExpr] -> SExpr
SList [ [Char] -> SExpr
SSymbol "map", Sign f e -> PRED_NAME -> PredType -> SExpr
forall f e. Sign f e -> PRED_NAME -> PredType -> SExpr
predIdToSSymbol Sign f e
src PRED_NAME
i PredType
ot
                      , Sign f e -> PRED_NAME -> PredType -> SExpr
forall f e. Sign f e -> PRED_NAME -> PredType -> SExpr
predIdToSSymbol Sign f e
tar PRED_NAME
j PredType
nt] SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
:)) []
        (MapSet PRED_NAME PredType -> Map PRED_NAME (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet PRED_NAME PredType -> Map PRED_NAME (Set PredType))
-> MapSet PRED_NAME PredType -> Map PRED_NAME (Set PredType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap Sign f e
src)