{- |
Module      :  ./VSE/ToSExpr.hs
Description :  translate VSE 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 VSE to S-Expressions
-}

module VSE.ToSExpr where

import VSE.As
import VSE.Ana
import VSE.Fold

import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign
import CASL.ToSExpr

import Common.AS_Annotation
import Common.Id
import Common.LibName
import Common.ProofUtils
import Common.SExpr
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Char (toLower)
import Data.List (sortBy)
import Data.Ord (comparing)

addUniformRestr :: Sign f Procs -> [Named Sentence]
  -> (Sign f Procs, [Named Sentence])
addUniformRestr :: Sign f Procs
-> [Named Sentence] -> (Sign f Procs, [Named Sentence])
addUniformRestr sig :: Sign f Procs
sig nsens :: [Named Sentence]
nsens = let
  namedConstr :: [Named Sentence]
namedConstr = (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ ns :: Named Sentence
ns -> case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
ns of
                                ExtFORMULA
                                 (Ranged
                                   (RestrictedConstraint {})
                                  _) -> Bool
True
                                _ -> Bool
False ) [Named Sentence]
nsens
  restrConstr :: [Sentence]
restrConstr = (Named Sentence -> Sentence) -> [Named Sentence] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence [Named Sentence]
namedConstr
  restrToSExpr :: (Map Id Profile, [Named Sentence])
-> Sentence -> (Map Id Profile, [Named Sentence])
restrToSExpr (procs :: Map Id Profile
procs, tSens :: [Named Sentence]
tSens)
               (ExtFORMULA
                 (Ranged (RestrictedConstraint constrs :: [Constraint]
constrs restr :: Map Id Id
restr _flag :: Bool
_flag) _r :: Range
_r)) =
   let
    (genSorts :: [Id]
genSorts, genOps :: [OP_SYMB]
genOps, _maps :: [(Id, Id)]
_maps) = [Constraint] -> ([Id], [OP_SYMB], [(Id, Id)])
recover_Sort_gen_ax [Constraint]
constrs
    genUniform :: t Id -> [OP_SYMB] -> Id -> [Named Sentence]
genUniform sorts :: t Id
sorts ops :: [OP_SYMB]
ops s :: Id
s = let
      hasResSort :: Id -> OP_SYMB -> Bool
hasResSort sn :: Id
sn ~(Qual_op_name _ opType :: OP_TYPE
opType _) = OP_TYPE -> Id
res_OP_TYPE OP_TYPE
opType Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
sn
      argLength :: OP_SYMB -> Int
argLength ~(Qual_op_name _ (Op_type _ args :: [Id]
args _ _) _) = [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args
      ctors :: [OP_SYMB]
ctors = (OP_SYMB -> OP_SYMB -> Ordering) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((OP_SYMB -> Int) -> OP_SYMB -> OP_SYMB -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing OP_SYMB -> Int
argLength) ([OP_SYMB] -> [OP_SYMB]) -> [OP_SYMB] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter (Id -> OP_SYMB -> Bool
hasResSort Id
s) [OP_SYMB]
ops
      genCodeForCtor :: OP_SYMB -> Program -> Program
genCodeForCtor ~(Qual_op_name ctor :: Id
ctor (Op_type _ args :: [Id]
args sn :: Id
sn _) _) prg :: Program
prg = let
        decls :: [(Token, Id)]
decls = [Id] -> [(Token, Id)]
genVars [Id]
args
        vs :: [VAR_DECL]
vs = ((Token, Id) -> VAR_DECL) -> [(Token, Id)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Token
i, a :: Id
a) -> [Token] -> Id -> Range -> VAR_DECL
Var_decl [Token
i] Id
a Range
nullRange) [(Token, Id)]
decls
        recCalls :: [Program]
recCalls = ((Token, Id) -> Program) -> [(Token, Id)] -> [Program]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Token
i, x :: Id
x) ->
                         PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> PlainProgram
Call (PRED_SYMB -> [TERM ()] -> Range -> FORMULA ()
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                        (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                          (Id -> Id
gnUniformName Id
s)
                                         ([Id] -> Range -> PRED_TYPE
Pred_type [Id
x] Range
nullRange) Range
nullRange)
                                        [Token -> Id -> Range -> TERM ()
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
i Id
x Range
nullRange] Range
nullRange
                                      )) Range
nullRange) ([(Token, Id)] -> [Program]) -> [(Token, Id)] -> [Program]
forall a b. (a -> b) -> a -> b
$
                   ((Token, Id) -> Bool) -> [(Token, Id)] -> [(Token, Id)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Id -> t Id -> Bool) -> t Id -> Id -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Id -> t Id -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem t Id
sorts (Id -> Bool) -> ((Token, Id) -> Id) -> (Token, Id) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token, Id) -> Id
forall a b. (a, b) -> b
snd) [(Token, Id)]
decls
        recCallsSeq :: Program
recCallsSeq = if [Program] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Program]
recCalls then PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip Range
nullRange else
                      (Program -> Program -> Program) -> [Program] -> Program
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ p1 :: Program
p1 p2 :: Program
p2 -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p1 Program
p2) Range
nullRange) [Program]
recCalls
        in case [Program]
recCalls of
         [] -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (
                [VAR_DECL] -> Program -> PlainProgram
Block ([Token] -> Id -> Range -> VAR_DECL
Var_decl [Token
yVar] Id
s Range
nullRange VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
vs)
              (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq
                (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                   (Token -> TERM () -> PlainProgram
Assign Token
yVar (Token -> Id -> Range -> TERM ()
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
xVar Id
sn Range
nullRange)
                    ) Range
nullRange)
                (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                   (Token -> TERM () -> PlainProgram
Assign
                                     Token
yVar
                                     (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                                      (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                                      Id
ctor
                                     (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
args Id
sn Range
nullRange)
                                     Range
nullRange)
                                      ((VAR_DECL -> TERM ()) -> [VAR_DECL] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs)
                                      Range
nullRange))
                                   Range
nullRange)
                        (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If (TERM () -> TERM () -> FORMULA ()
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                               (OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl
                                 (
                                  Id -> OP_TYPE -> OP_SYMB
mkQualOp
                                   (Id -> Id
gnEqName Id
s)
                                   (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s]
                                    Id
uBoolean Range
nullRange)
                                 ) [Token -> Id -> TERM ()
forall f. Token -> Id -> TERM f
mkVarTerm Token
xVar Id
s, Token -> Id -> TERM ()
forall f. Token -> Id -> TERM f
mkVarTerm Token
yVar Id
s])
                               TERM ()
forall f. TERM f
aTrue)
                          (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip Range
nullRange)
                          Program
prg) Range
nullRange))
                Range
nullRange )) Range
nullRange) ) Range
nullRange
         _ -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (
                 [VAR_DECL] -> Program -> PlainProgram
Block ([Token] -> Id -> Range -> VAR_DECL
Var_decl [Token
yVar] Id
s Range
nullRange VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
vs)
                (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Token -> TERM () -> PlainProgram
Assign Token
yVar
                                      (Token -> Id -> Range -> TERM ()
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
xVar Id
sn Range
nullRange)
                                     ) Range
nullRange)
                             (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                              (Program -> Program -> PlainProgram
Seq Program
recCallsSeq
                               (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq
                                  (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                    (Token -> TERM () -> PlainProgram
Assign
                                      Token
yVar
                                     (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                                      (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
                                     Id
ctor
                                     (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id]
args Id
sn Range
nullRange)
                                     Range
nullRange)
                                      ((VAR_DECL -> TERM ()) -> [VAR_DECL] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs)
                                      Range
nullRange))
                                   Range
nullRange)
                                (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If (TERM () -> TERM () -> FORMULA ()
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                                 ( OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl
                                 ( Id -> OP_TYPE -> OP_SYMB
mkQualOp
                                   (Id -> Id
gnEqName Id
s)
                                   (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Partial [Id
s, Id
s]
                                    Id
uBoolean Range
nullRange)
                                 ) [Token -> Id -> TERM ()
forall f. Token -> Id -> TERM f
mkVarTerm Token
xVar Id
s, Token -> Id -> TERM ()
forall f. Token -> Id -> TERM f
mkVarTerm Token
yVar Id
s])
                                TERM ()
forall f. TERM f
aTrue)
                               (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Skip Range
nullRange) Program
prg) Range
nullRange))
                               Range
nullRange )) Range
nullRange)) Range
nullRange) ) Range
nullRange
                             in
     [[Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$
     VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs [
      ProcKind -> Id -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
Proc (Id -> Id
gnUniformName Id
s) [Token
xVar]
      (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (
        [VAR_DECL] -> Program -> PlainProgram
Block [] ( (OP_SYMB -> Program -> Program) -> Program -> [OP_SYMB] -> Program
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr OP_SYMB -> Program -> Program
genCodeForCtor (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged PlainProgram
Abort Range
nullRange)
                   [OP_SYMB]
ctors)
              ) Range
nullRange
      )
      Range
nullRange])
     Range
nullRange,
     ([Char] -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$
     QUANTIFIER -> [VAR_DECL] -> Sentence -> Range -> Sentence
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [[Token] -> Id -> Range -> VAR_DECL
Var_decl [Token
xVar] Id
s Range
nullRange]
      (Sentence -> Sentence -> Sentence
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
       ( Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
          (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond ( PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
            (FORMULA () -> PlainProgram
Call (FORMULA () -> PlainProgram) -> FORMULA () -> PlainProgram
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM ()] -> Range -> FORMULA ()
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
              (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                (Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Id -> Id
gnRestrName Id
s) Id
s Map Id Id
restr)
                ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
               [Token -> Id -> Range -> TERM ()
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
xVar Id
s Range
nullRange] Range
nullRange) Range
nullRange)
            Sentence
forall f. FORMULA f
trueForm)
          Range
nullRange)
       ( Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
          (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
Diamond (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
            (FORMULA () -> PlainProgram
Call (FORMULA () -> PlainProgram) -> FORMULA () -> PlainProgram
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM ()] -> Range -> FORMULA ()
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
              (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name (Id -> Id
gnUniformName Id
s)
                ([Id] -> Range -> PRED_TYPE
Pred_type [Id
s] Range
nullRange) Range
nullRange)
               [Token -> Id -> Range -> TERM ()
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
xVar Id
s Range
nullRange] Range
nullRange) Range
nullRange)
            Sentence
forall f. FORMULA f
trueForm)
          Range
nullRange)) Range
nullRange) {isAxiom :: Bool
isAxiom = Bool
False}]
    procDefs :: [Named Sentence]
procDefs = (Id -> [Named Sentence]) -> [Id] -> [Named Sentence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Id] -> [OP_SYMB] -> Id -> [Named Sentence]
forall (t :: * -> *).
Foldable t =>
t Id -> [OP_SYMB] -> Id -> [Named Sentence]
genUniform [Id]
genSorts [OP_SYMB]
genOps) [Id]
genSorts
    procs' :: Map Id Profile
procs' = [(Id, Profile)] -> Map Id Profile
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Profile)] -> Map Id Profile)
-> [(Id, Profile)] -> Map Id Profile
forall a b. (a -> b) -> a -> b
$
             (Id -> (Id, Profile)) -> [Id] -> [(Id, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: Id
s -> (Id -> Id
gnUniformName Id
s,
                         [Procparam] -> Maybe Id -> Profile
Profile [Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s] Maybe Id
forall a. Maybe a
Nothing)) [Id]
genSorts
   in
    (Map Id Profile -> Map Id Profile -> Map Id Profile
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Id Profile
procs Map Id Profile
procs', [Named Sentence]
tSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
procDefs)
  restrToSExpr _ _ = [Char] -> (Map Id Profile, [Named Sentence])
forall a. HasCallStack => [Char] -> a
error "should not be anything than restricted constraints"
  (newProcs :: Map Id Profile
newProcs, trSens :: [Named Sentence]
trSens) = ((Map Id Profile, [Named Sentence])
 -> Sentence -> (Map Id Profile, [Named Sentence]))
-> (Map Id Profile, [Named Sentence])
-> [Sentence]
-> (Map Id Profile, [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Map Id Profile, [Named Sentence])
-> Sentence -> (Map Id Profile, [Named Sentence])
restrToSExpr (Map Id Profile
forall k a. Map k a
Map.empty, []) [Sentence]
restrConstr
                            in
 (Sign f Procs
sig {
   predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
addMapSet (Sign f Procs -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f Procs
sig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Procs -> PredMap
procsToPredMap (Procs -> PredMap) -> Procs -> PredMap
forall a b. (a -> b) -> a -> b
$ Map Id Profile -> Procs
Procs Map Id Profile
newProcs,

   extendedInfo :: Procs
extendedInfo = Map Id Profile -> Procs
Procs (Map Id Profile -> Procs) -> Map Id Profile -> Procs
forall a b. (a -> b) -> a -> b
$ Map Id Profile -> Map Id Profile -> Map Id Profile
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Id Profile
newProcs (Procs -> Map Id Profile
procsMap (Procs -> Map Id Profile) -> Procs -> Map Id Profile
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo Sign f Procs
sig)},
  [Named Sentence] -> [Named Sentence]
forall a. [Named a] -> [Named a]
nameAndDisambiguate ([Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$
    [Named Sentence]
trSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Named Sentence -> Bool) -> Named Sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named Sentence -> [Named Sentence] -> Bool)
-> [Named Sentence] -> Named Sentence -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Named Sentence -> [Named Sentence] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Named Sentence]
namedConstr) [Named Sentence]
nsens)

namedSenToSExpr :: Sign f Procs -> Named Sentence -> SExpr
namedSenToSExpr :: Sign f Procs -> Named Sentence -> SExpr
namedSenToSExpr sig :: Sign f Procs
sig ns :: Named Sentence
ns =
  [SExpr] -> SExpr
SList
    [ [Char] -> SExpr
SSymbol "asentence"
    , [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
transString ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Named Sentence -> [Char]
forall s a. SenAttr s a -> a
senAttr Named Sentence
ns
    , [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ if Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named Sentence
ns then "axiom" else "obligation"
    , [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ if Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named Sentence
ns then "proved" else "open"
    , Sign f Procs -> Sentence -> SExpr
forall f. Sign f Procs -> Sentence -> SExpr
senToSExpr Sign f Procs
sig (Sentence -> SExpr) -> Sentence -> SExpr
forall a b. (a -> b) -> a -> b
$ Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
ns ]

senToSExpr :: Sign f Procs -> Sentence -> SExpr
senToSExpr :: Sign f Procs -> Sentence -> SExpr
senToSExpr sig :: Sign f Procs
sig s :: Sentence
s = let ns :: SExpr
ns = Sign f Procs -> Sentence -> SExpr
forall f. Sign f Procs -> Sentence -> SExpr
sentenceToSExpr Sign f Procs
sig Sentence
s in case Sentence
s of
    ExtFORMULA (Ranged (Defprocs _) _) ->
        [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "defprocs-sentence", SExpr
ns]
    Sort_gen_ax _ _ ->
        [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "generatedness-sentence", SExpr
ns]
    _ -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "formula-sentence", SExpr
ns]

sentenceToSExpr :: Sign f Procs -> Sentence -> SExpr
sentenceToSExpr :: Sign f Procs -> Sentence -> SExpr
sentenceToSExpr sign :: Sign f Procs
sign = let sig :: Sign f Procs
sig = (Procs -> Procs -> Procs)
-> Sign f Procs -> Sign f Procs -> Sign f Procs
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig Procs -> Procs -> Procs
forall a b. a -> b -> a
const Sign f Procs
sign Sign f Procs
forall f. Sign f Procs
boolSig in
  Record (Ranged VSEforms) SExpr SExpr -> Sentence -> SExpr
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record (Ranged VSEforms) SExpr SExpr -> Sentence -> SExpr)
-> Record (Ranged VSEforms) SExpr SExpr -> Sentence -> SExpr
forall a b. (a -> b) -> a -> b
$ Sign f Procs
-> (Ranged VSEforms -> SExpr)
-> Record (Ranged VSEforms) SExpr SExpr
forall f a e.
GetRange f =>
Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
sRec Sign f Procs
sig ((Ranged VSEforms -> SExpr)
 -> Record (Ranged VSEforms) SExpr SExpr)
-> (Ranged VSEforms -> SExpr)
-> Record (Ranged VSEforms) SExpr SExpr
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Ranged VSEforms -> SExpr
forall f. Sign f Procs -> Ranged VSEforms -> SExpr
dlFormulaToSExpr Sign f Procs
sig

dlFormulaToSExpr :: Sign f Procs -> Dlformula -> SExpr
dlFormulaToSExpr :: Sign f Procs -> Ranged VSEforms -> SExpr
dlFormulaToSExpr sig :: Sign f Procs
sig = Sign f Procs -> VSEforms -> SExpr
forall f. Sign f Procs -> VSEforms -> SExpr
vseFormsToSExpr Sign f Procs
sig (VSEforms -> SExpr)
-> (Ranged VSEforms -> VSEforms) -> Ranged VSEforms -> SExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged VSEforms -> VSEforms
forall a. Ranged a -> a
unRanged

vseFormsToSExpr :: Sign f Procs -> VSEforms -> SExpr
vseFormsToSExpr :: Sign f Procs -> VSEforms -> SExpr
vseFormsToSExpr sig :: Sign f Procs
sig vf :: VSEforms
vf = case VSEforms
vf of
  Dlformula b :: BoxOrDiamond
b p :: Program
p s :: Sentence
s ->
    [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ case BoxOrDiamond
b of
         Box -> "box"
         Diamond -> "diamond", Sign f Procs -> Program -> SExpr
forall f. Sign f Procs -> Program -> SExpr
progToSExpr Sign f Procs
sig Program
p, Sign f Procs -> Sentence -> SExpr
forall f. Sign f Procs -> Sentence -> SExpr
sentenceToSExpr Sign f Procs
sig Sentence
s]
  Defprocs ds :: [Defproc]
ds ->
    [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "defprocs" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (Defproc -> SExpr) -> [Defproc] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f Procs -> Defproc -> SExpr
forall f. Sign f Procs -> Defproc -> SExpr
defprocToSExpr Sign f Procs
sig) [Defproc]
ds
  RestrictedConstraint {} ->
   [Char] -> SExpr
forall a. HasCallStack => [Char] -> a
error "restricted constraints should be handled separately"

vDeclToSExpr :: Sign f Procs -> VarDecl -> SExpr
vDeclToSExpr :: Sign f Procs -> VarDecl -> SExpr
vDeclToSExpr sig :: Sign f Procs
sig (VarDecl v :: Token
v s :: Id
s m :: Maybe (TERM ())
m _) =
  let vd :: SExpr
vd@(SList [_, w :: SExpr
w, ty :: SExpr
ty]) = (Token, Id) -> SExpr
varDeclToSExpr (Token
v, Id
s) in
  case Maybe (TERM ())
m of
    Nothing -> SExpr
vd
    Just trm :: TERM ()
trm -> [SExpr] -> SExpr
SList [ [Char] -> SExpr
SSymbol "vardecl", SExpr
w, SExpr
ty
                      , Record () SExpr SExpr -> TERM () -> SExpr
forall f a b. Record f a b -> TERM f -> b
foldTerm (Sign f Procs -> (() -> SExpr) -> Record () SExpr SExpr
forall f a e.
GetRange f =>
Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
sRec Sign f Procs
sig ((() -> SExpr) -> Record () SExpr SExpr)
-> (() -> SExpr) -> Record () SExpr SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> () -> SExpr
forall a. HasCallStack => [Char] -> a
error "vDeclToSExpr") TERM ()
trm ]

procIdToSSymbol :: Sign f Procs -> Id -> SExpr
procIdToSSymbol :: Sign f Procs -> Id -> SExpr
procIdToSSymbol sig :: Sign f Procs
sig n :: Id
n = case Id -> Sign f Procs -> Maybe Profile
forall f. Id -> Sign f Procs -> Maybe Profile
lookupProc Id
n Sign f Procs
sig of
        Nothing -> [Char] -> SExpr
forall a. HasCallStack => [Char] -> a
error "procIdToSSymbol"
        Just pr :: Profile
pr -> case Profile -> Maybe OpType
profileToOpType Profile
pr of
          Just ot :: OpType
ot -> Sign f Procs -> Id -> OpType -> SExpr
forall f e. Sign f e -> Id -> OpType -> SExpr
opIdToSSymbol Sign f Procs
sig Id
n OpType
ot
          _ -> Sign f Procs -> Id -> PredType -> SExpr
forall f e. Sign f e -> Id -> PredType -> SExpr
predIdToSSymbol Sign f Procs
sig Id
n (PredType -> SExpr) -> PredType -> SExpr
forall a b. (a -> b) -> a -> b
$ Profile -> PredType
profileToPredType Profile
pr

progToSExpr :: Sign f Procs -> Program -> SExpr
progToSExpr :: Sign f Procs -> Program -> SExpr
progToSExpr sig :: Sign f Procs
sig = let
  pRec :: Record () SExpr SExpr
pRec = Sign f Procs -> (() -> SExpr) -> Record () SExpr SExpr
forall f a e.
GetRange f =>
Sign a e -> (f -> SExpr) -> Record f SExpr SExpr
sRec Sign f Procs
sig ([Char] -> () -> SExpr
forall a. HasCallStack => [Char] -> a
error "progToSExpr")
  termToSExpr :: TERM () -> SExpr
termToSExpr = Record () SExpr SExpr -> TERM () -> SExpr
forall f a b. Record f a b -> TERM f -> b
foldTerm Record () SExpr SExpr
pRec
  formToSExpr :: FORMULA () -> SExpr
formToSExpr = Record () SExpr SExpr -> FORMULA () -> SExpr
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record () SExpr SExpr
pRec
  in FoldRec SExpr -> Program -> SExpr
forall a. FoldRec a -> Program -> a
foldProg FoldRec :: forall a.
(Program -> a)
-> (Program -> a)
-> (Program -> Token -> TERM () -> a)
-> (Program -> FORMULA () -> a)
-> (Program -> TERM () -> a)
-> (Program -> [VAR_DECL] -> a -> a)
-> (Program -> a -> a -> a)
-> (Program -> FORMULA () -> a -> a -> a)
-> (Program -> FORMULA () -> a -> a)
-> FoldRec a
FoldRec
  { foldAbort :: Program -> SExpr
foldAbort = SExpr -> Program -> SExpr
forall a b. a -> b -> a
const (SExpr -> Program -> SExpr) -> SExpr -> Program -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "abort"
  , foldSkip :: Program -> SExpr
foldSkip = SExpr -> Program -> SExpr
forall a b. a -> b -> a
const (SExpr -> Program -> SExpr) -> SExpr -> Program -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "skip"
  , foldAssign :: Program -> Token -> TERM () -> SExpr
foldAssign = \ _ v :: Token
v t :: TERM ()
t ->
      [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "assign", Token -> SExpr
varToSSymbol Token
v, TERM () -> SExpr
termToSExpr TERM ()
t]
  , foldCall :: Program -> FORMULA () -> SExpr
foldCall = \ (Ranged _ r :: Range
r) f :: FORMULA ()
f ->
      case FORMULA ()
f of
        Predication (Qual_pred_name i :: Id
i _ _) ts :: [TERM ()]
ts _ ->
          [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "call" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign f Procs -> Id -> SExpr
forall f. Sign f Procs -> Id -> SExpr
procIdToSSymbol Sign f Procs
sig Id
i SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: (TERM () -> SExpr) -> [TERM ()] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map TERM () -> SExpr
termToSExpr [TERM ()]
ts
        _ -> [Char] -> Range -> SExpr
forall a. [Char] -> Range -> a
sfail "Call" Range
r
  , foldReturn :: Program -> TERM () -> SExpr
foldReturn = \ _ t :: TERM ()
t -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "return", TERM () -> SExpr
termToSExpr TERM ()
t]
  , foldBlock :: Program -> [VAR_DECL] -> SExpr -> SExpr
foldBlock = \ ~(Ranged (Block vs :: [VAR_DECL]
vs p :: Program
p) _) _ _ ->
      let (vds :: [VarDecl]
vds, q :: Program
q) = [VarDecl] -> Program -> ([VarDecl], Program)
addInits ([VAR_DECL] -> [VarDecl]
toVarDecl [VAR_DECL]
vs) Program
p
          ps :: SExpr
ps = Sign f Procs -> Program -> SExpr
forall f. Sign f Procs -> Program -> SExpr
progToSExpr Sign f Procs
sig Program
q
          nvs :: [SExpr]
nvs = (VarDecl -> SExpr) -> [VarDecl] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f Procs -> VarDecl -> SExpr
forall f. Sign f Procs -> VarDecl -> SExpr
vDeclToSExpr Sign f Procs
sig) [VarDecl]
vds
      in if [SExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SExpr]
nvs then SExpr
ps else [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "vblock", [SExpr] -> SExpr
SList [SExpr]
nvs, SExpr
ps]
  , foldSeq :: Program -> SExpr -> SExpr -> SExpr
foldSeq = \ _ s1 :: SExpr
s1 s2 :: SExpr
s2 -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "seq", SExpr
s1, SExpr
s2]
  , foldIf :: Program -> FORMULA () -> SExpr -> SExpr -> SExpr
foldIf = \ _ c :: FORMULA ()
c s1 :: SExpr
s1 s2 :: SExpr
s2 -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "if", FORMULA () -> SExpr
formToSExpr FORMULA ()
c, SExpr
s1, SExpr
s2]
  , foldWhile :: Program -> FORMULA () -> SExpr -> SExpr
foldWhile = \ _ c :: FORMULA ()
c s :: SExpr
s -> [SExpr] -> SExpr
SList [[Char] -> SExpr
SSymbol "while", FORMULA () -> SExpr
formToSExpr FORMULA ()
c, SExpr
s] }

defprocToSExpr :: Sign f Procs -> Defproc -> SExpr
defprocToSExpr :: Sign f Procs -> Defproc -> SExpr
defprocToSExpr sig :: Sign f Procs
sig (Defproc k :: ProcKind
k n :: Id
n vs :: [Token]
vs p :: Program
p _) = [SExpr] -> SExpr
SList
    [ [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ case ProcKind
k of
        Proc -> "defproc"
        Func -> "deffuncproc"
    , Sign f Procs -> Id -> SExpr
forall f. Sign f Procs -> Id -> SExpr
procIdToSSymbol Sign f Procs
sig Id
n
    , [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (Token -> SExpr) -> [Token] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map Token -> SExpr
varToSSymbol [Token]
vs
    , Sign f Procs -> Program -> SExpr
forall f. Sign f Procs -> Program -> SExpr
progToSExpr Sign f Procs
sig Program
p ]

paramToSExpr :: Procparam -> SExpr
paramToSExpr :: Procparam -> SExpr
paramToSExpr (Procparam k :: Paramkind
k s :: Id
s) = [SExpr] -> SExpr
SList
  [ [Char] -> SExpr
SSymbol ([Char] -> SExpr) -> [Char] -> SExpr
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Paramkind -> [Char]
forall a. Show a => a -> [Char]
show Paramkind
k
  , Id -> SExpr
sortToSSymbol Id
s ]

procsToSExprs :: (Id -> Bool) -> Sign f Procs -> [SExpr]
procsToSExprs :: (Id -> Bool) -> Sign f Procs -> [SExpr]
procsToSExprs f :: Id -> Bool
f sig :: Sign f Procs
sig =
    ((Id, Profile) -> SExpr) -> [(Id, Profile)] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: Id
n, pr :: Profile
pr@(Profile as :: [Procparam]
as _)) -> case Profile -> Maybe OpType
profileToOpType Profile
pr of
      Nothing -> [SExpr] -> SExpr
SList
        [ [Char] -> SExpr
SSymbol "procedure"
        , Sign f Procs -> Id -> PredType -> SExpr
forall f e. Sign f e -> Id -> PredType -> SExpr
predIdToSSymbol Sign f Procs
sig Id
n (PredType -> SExpr) -> PredType -> SExpr
forall a b. (a -> b) -> a -> b
$ Profile -> PredType
profileToPredType Profile
pr
        , [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (Procparam -> SExpr) -> [Procparam] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map Procparam -> SExpr
paramToSExpr [Procparam]
as ]
      Just ot :: OpType
ot -> [SExpr] -> SExpr
SList
        [ [Char] -> SExpr
SSymbol "funcprocedure"
        , Sign f Procs -> Id -> OpType -> SExpr
forall f e. Sign f e -> Id -> OpType -> SExpr
opIdToSSymbol Sign f Procs
sig Id
n OpType
ot
        , [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (Id -> SExpr) -> [Id] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SExpr
sortToSSymbol ([Id] -> [SExpr]) -> [Id] -> [SExpr]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
ot
        , Id -> SExpr
sortToSSymbol (Id -> SExpr) -> Id -> SExpr
forall a b. (a -> b) -> a -> b
$ OpType -> Id
opRes OpType
ot ])
    ([(Id, Profile)] -> [SExpr]) -> [(Id, Profile)] -> [SExpr]
forall a b. (a -> b) -> a -> b
$ Map Id Profile -> [(Id, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Id Profile -> [(Id, Profile)])
-> Map Id Profile -> [(Id, Profile)]
forall a b. (a -> b) -> a -> b
$ (Id -> Profile -> Bool) -> Map Id Profile -> Map Id Profile
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ i :: Id
i _ -> Id -> Bool
f Id
i)
    (Map Id Profile -> Map Id Profile)
-> Map Id Profile -> Map Id Profile
forall a b. (a -> b) -> a -> b
$ Procs -> Map Id Profile
procsMap (Procs -> Map Id Profile) -> Procs -> Map Id Profile
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo Sign f Procs
sig

vseSignToSExpr :: Sign f Procs -> SExpr
vseSignToSExpr :: Sign f Procs -> SExpr
vseSignToSExpr sig :: Sign f Procs
sig =
  let e :: Procs
e = Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo Sign f Procs
sig in
    [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "signature" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign f Procs -> SExpr
forall a e. Sign a e -> SExpr
sortSignToSExprs Sign f Procs
sig
      SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign f Procs -> PredMap -> [SExpr]
forall a e. Sign a e -> PredMap -> [SExpr]
predMapToSExprs Sign f Procs
sig (PredMap -> PredMap -> PredMap
diffMapSet (Sign f Procs -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f Procs
sig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Procs -> PredMap
procsToPredMap Procs
e)
      [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ Sign f Procs -> OpMap -> [SExpr]
forall a e. Sign a e -> OpMap -> [SExpr]
opMapToSExprs Sign f Procs
sig (OpMap -> OpMap -> OpMap
diffOpMapSet (Sign f Procs -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f Procs
sig) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Procs -> OpMap
procsToOpMap Procs
e)
      [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ (Id -> Bool) -> Sign f Procs -> [SExpr]
forall f. (Id -> Bool) -> Sign f Procs -> [SExpr]
procsToSExprs (Bool -> Id -> Bool
forall a b. a -> b -> a
const Bool
True) Sign f Procs
sig

qualVseSignToSExpr :: SIMPLE_ID -> LibName -> Sign f Procs -> SExpr
qualVseSignToSExpr :: Token -> LibName -> Sign f Procs -> SExpr
qualVseSignToSExpr nodeId :: Token
nodeId libId :: LibName
libId sig :: Sign f Procs
sig =
  let e :: Procs
e = Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo Sign f Procs
sig in
    [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ [Char] -> SExpr
SSymbol "signature" SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign f Procs -> SExpr
forall a e. Sign a e -> SExpr
sortSignToSExprs Sign f Procs
sig
          { sortRel :: Rel Id
sortRel = Set Id -> Rel Id -> Rel Id
forall a. Ord a => Set a -> Rel a -> Rel a
Rel.delSet
            ((Id -> Bool) -> Set Id -> Set Id
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Id -> Bool) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> LibName -> Id -> Bool
isQualNameFrom Token
nodeId LibName
libId) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f Procs
sig)
            (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f Procs
sig }
      SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: Sign f Procs -> PredMap -> [SExpr]
forall a e. Sign a e -> PredMap -> [SExpr]
predMapToSExprs Sign f Procs
sig
            ((Id -> Set PredType -> Bool) -> PredMap -> PredMap
forall a b.
Ord a =>
(a -> Set b -> Bool) -> MapSet a b -> MapSet a b
MapSet.filterWithKey (\ i :: Id
i _ -> Token -> LibName -> Id -> Bool
isQualNameFrom Token
nodeId LibName
libId Id
i)
            (PredMap -> PredMap) -> (PredMap -> PredMap) -> PredMap -> PredMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference (Sign f Procs -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f Procs
sig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Procs -> PredMap
procsToPredMap Procs
e)
      [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ Sign f Procs -> OpMap -> [SExpr]
forall a e. Sign a e -> OpMap -> [SExpr]
opMapToSExprs Sign f Procs
sig
            ((Id -> Set OpType -> Bool) -> OpMap -> OpMap
forall a b.
Ord a =>
(a -> Set b -> Bool) -> MapSet a b -> MapSet a b
MapSet.filterWithKey (\ i :: Id
i _ -> Token -> LibName -> Id -> Bool
isQualNameFrom Token
nodeId LibName
libId Id
i)
            (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpMap -> OpMap -> OpMap
diffOpMapSet (Sign f Procs -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f Procs
sig) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Procs -> OpMap
procsToOpMap Procs
e)
      [SExpr] -> [SExpr] -> [SExpr]
forall a. [a] -> [a] -> [a]
++ (Id -> Bool) -> Sign f Procs -> [SExpr]
forall f. (Id -> Bool) -> Sign f Procs -> [SExpr]
procsToSExprs (Token -> LibName -> Id -> Bool
isQualNameFrom Token
nodeId LibName
libId) Sign f Procs
sig