{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./VSE/Ana.hs
Description :  static analysis of VSE parts
Copyright   :  (c) C. Maeder, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

analysis of VSE logic extension of CASL
-}

module VSE.Ana
  ( VSESign
  , uTrue
  , uFalse
  , aTrue
  , aFalse
  , uBoolean
  , constBoolType
  , boolSig
  , lookupProc
  , procsToOpMap
  , procsToPredMap
  , profileToOpType
  , profileToPredType
  , checkCases
  , basicAna
  , mapDlformula
  , minExpForm
  , simpDlformula
  , correctSign
  , correctTarget
  , inducedExt
  , VSEMorExt
  , VSEMor
  , VSEBasicSpec
  , extVSEColimit
  , vseMorExt
  ) where

import Control.Monad
import Data.Char (toLower)
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Control.Monad.Fail as Fail

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.ExtSign
import Common.Id
import Common.Result
import Common.Utils (hasMany)
import Common.Lib.State

import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign
import CASL.MixfixParser
import CASL.MapSentence as MapSen
import CASL.Morphism
import CASL.Overload
import CASL.Quantification
import CASL.StaticAna
import CASL.ShowMixfix as Paren
import CASL.SimplifySen

import VSE.As
import VSE.Fold

import Data.Graph.Inductive.Graph
import Common.Lib.Graph

type VSESign = Sign Dlformula Procs

getVariables :: Sentence -> Set.Set Token
getVariables :: Sentence -> Set Token
getVariables = Record (Ranged VSEforms) (Set Token) (Set Token)
-> Sentence -> Set Token
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record (Ranged VSEforms) (Set Token) (Set Token)
 -> Sentence -> Set Token)
-> Record (Ranged VSEforms) (Set Token) (Set Token)
-> Sentence
-> Set Token
forall a b. (a -> b) -> a -> b
$ (Ranged VSEforms -> Set Token)
-> Record (Ranged VSEforms) (Set Token) (Set Token)
forall f. (f -> Set Token) -> Record f (Set Token) (Set Token)
getVarsRec ((Ranged VSEforms -> Set Token)
 -> Record (Ranged VSEforms) (Set Token) (Set Token))
-> (Ranged VSEforms -> Set Token)
-> Record (Ranged VSEforms) (Set Token) (Set Token)
forall a b. (a -> b) -> a -> b
$ VSEforms -> Set Token
getVSEVars (VSEforms -> Set Token)
-> (Ranged VSEforms -> VSEforms) -> Ranged VSEforms -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged VSEforms -> VSEforms
forall a. Ranged a -> a
unRanged

getVarsRec :: (f -> Set.Set Token) -> Record f (Set.Set Token) (Set.Set Token)
getVarsRec :: (f -> Set Token) -> Record f (Set Token) (Set Token)
getVarsRec f :: f -> Set Token
f =
  ((f -> Set Token)
-> ([Set Token] -> Set Token)
-> Set Token
-> Record f (Set Token) (Set Token)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord f -> Set Token
f [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set Token
forall a. Set a
Set.empty)
  { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> Set Token -> Range -> Set Token
foldQuantification = \ _ _ vs :: [VAR_DECL]
vs r :: Set Token
r _ -> Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Token
r
      (Set Token -> Set Token) -> Set Token -> Set Token
forall a b. (a -> b) -> a -> b
$ [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList ([Token] -> Set Token) -> [Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ ((Token, SORT) -> Token) -> [(Token, SORT)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, SORT) -> Token
forall a b. (a, b) -> a
fst ([(Token, SORT)] -> [Token]) -> [(Token, SORT)] -> [Token]
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, SORT)]
flatVAR_DECLs [VAR_DECL]
vs
  , foldQual_var :: TERM f -> Token -> SORT -> Range -> Set Token
foldQual_var = \ _ v :: Token
v _ _ -> Token -> Set Token
forall a. a -> Set a
Set.singleton Token
v }

getVSEVars :: VSEforms -> Set.Set Token
getVSEVars :: VSEforms -> Set Token
getVSEVars vf :: VSEforms
vf = case VSEforms
vf of
  Dlformula _ p :: Program
p s :: Sentence
s -> Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Program -> Set Token
getProgVars Program
p) (Set Token -> Set Token) -> Set Token -> Set Token
forall a b. (a -> b) -> a -> b
$ Sentence -> Set Token
getVariables Sentence
s
  Defprocs l :: [Defproc]
l -> [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Token] -> Set Token) -> [Set Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ (Defproc -> Set Token) -> [Defproc] -> [Set Token]
forall a b. (a -> b) -> [a] -> [b]
map Defproc -> Set Token
getDefprogVars [Defproc]
l
  _ -> Set Token
forall a. Set a
Set.empty -- no variables in a sort generation constraint

getProgVars :: Program -> Set.Set Token
getProgVars :: Program -> Set Token
getProgVars =
  let vrec :: Record b (Set Token) (Set Token)
vrec = (b -> Set Token) -> Record b (Set Token) (Set Token)
forall f. (f -> Set Token) -> Record f (Set Token) (Set Token)
getVarsRec ((b -> Set Token) -> Record b (Set Token) (Set Token))
-> (b -> Set Token) -> Record b (Set Token) (Set Token)
forall a b. (a -> b) -> a -> b
$ Set Token -> b -> Set Token
forall a b. a -> b -> a
const Set Token
forall a. Set a
Set.empty
      getTermVars :: TERM f -> Set Token
getTermVars = Record f (Set Token) (Set Token) -> TERM f -> Set Token
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f (Set Token) (Set Token)
forall b. Record b (Set Token) (Set Token)
vrec
      getCondVars :: FORMULA f -> Set Token
getCondVars = Record f (Set Token) (Set Token) -> FORMULA f -> Set Token
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f (Set Token) (Set Token)
forall b. Record b (Set Token) (Set Token)
vrec
  in FoldRec (Set Token) -> Program -> Set Token
forall a. FoldRec a -> Program -> a
foldProg ((TERM () -> Set Token)
-> (FORMULA () -> Set Token) -> FoldRec (Set Token)
forall a.
Ord a =>
(TERM () -> Set a) -> (FORMULA () -> Set a) -> FoldRec (Set a)
progToSetRec TERM () -> Set Token
forall f. TERM f -> Set Token
getTermVars FORMULA () -> Set Token
forall f. FORMULA f -> Set Token
getCondVars)
  { foldAssign :: Program -> Token -> TERM () -> Set Token
foldAssign = \ _ v :: Token
v t :: TERM ()
t -> Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.insert Token
v (Set Token -> Set Token) -> Set Token -> Set Token
forall a b. (a -> b) -> a -> b
$ TERM () -> Set Token
forall f. TERM f -> Set Token
getTermVars TERM ()
t
  , foldBlock :: Program -> [VAR_DECL] -> Set Token -> Set Token
foldBlock = \ _ vs :: [VAR_DECL]
vs p :: Set Token
p -> Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Token
p
      (Set Token -> Set Token) -> Set Token -> Set Token
forall a b. (a -> b) -> a -> b
$ [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList ([Token] -> Set Token) -> [Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ ((Token, SORT) -> Token) -> [(Token, SORT)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, SORT) -> Token
forall a b. (a, b) -> a
fst ([(Token, SORT)] -> [Token]) -> [(Token, SORT)] -> [Token]
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, SORT)]
flatVAR_DECLs [VAR_DECL]
vs }

getDefprogVars :: Defproc -> Set.Set Token
getDefprogVars :: Defproc -> Set Token
getDefprogVars (Defproc _ _ vs :: [Token]
vs p :: Program
p _) = Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Program -> Set Token
getProgVars Program
p)
  (Set Token -> Set Token) -> Set Token -> Set Token
forall a b. (a -> b) -> a -> b
$ [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList [Token]
vs

tokenToLower :: Token -> Token
tokenToLower :: Token -> Token
tokenToLower (Token s :: String
s r :: Range
r) = String -> Range -> Token
Token ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s) Range
r

idToLower :: Id -> Id
idToLower :: SORT -> SORT
idToLower (Id ts :: [Token]
ts cs :: [SORT]
cs r :: Range
r) = [Token] -> [SORT] -> Range -> SORT
Id ((Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Token
tokenToLower [Token]
ts) ((SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
idToLower [SORT]
cs) Range
r

getCases :: String -> Set.Set Id -> [Diagnosis]
getCases :: String -> Set SORT -> [Diagnosis]
getCases msg :: String
msg =
  (Set SORT -> Diagnosis) -> [Set SORT] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> String -> [SORT] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error ("overlapping " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ " identifiers") ([SORT] -> Diagnosis)
-> (Set SORT -> [SORT]) -> Set SORT -> Diagnosis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList)
  ([Set SORT] -> [Diagnosis])
-> (Set SORT -> [Set SORT]) -> Set SORT -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set SORT -> Bool) -> [Set SORT] -> [Set SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter Set SORT -> Bool
forall a. Set a -> Bool
hasMany ([Set SORT] -> [Set SORT])
-> (Set SORT -> [Set SORT]) -> Set SORT -> [Set SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SORT (Set SORT) -> [Set SORT]
forall k a. Map k a -> [a]
Map.elems
  (Map SORT (Set SORT) -> [Set SORT])
-> (Set SORT -> Map SORT (Set SORT)) -> Set SORT -> [Set SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> Map SORT (Set SORT) -> Map SORT (Set SORT))
-> Map SORT (Set SORT) -> Set SORT -> Map SORT (Set SORT)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ i :: SORT
i -> SORT -> SORT -> Map SORT (Set SORT) -> Map SORT (Set SORT)
forall k a.
(Ord k, Ord a) =>
k -> a -> Map k (Set a) -> Map k (Set a)
MapSet.setInsert (SORT -> SORT
idToLower SORT
i) SORT
i) Map SORT (Set SORT)
forall k a. Map k a
Map.empty

getCaseDiags :: Sign f e -> [Diagnosis]
getCaseDiags :: Sign f e -> [Diagnosis]
getCaseDiags sig :: Sign f e
sig =
  String -> Set SORT -> [Diagnosis]
getCases "sort" (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig)
  [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String -> Set SORT -> [Diagnosis]
getCases "op or function" (MapSet SORT OpType -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (MapSet SORT OpType -> Set SORT) -> MapSet SORT OpType -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f e
sig)
  [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String -> Set SORT -> [Diagnosis]
getCases "pred or proc" (MapSet SORT PredType -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (MapSet SORT PredType -> Set SORT)
-> MapSet SORT PredType -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign f e
sig)

uBoolean :: Id
uBoolean :: SORT
uBoolean = String -> SORT
stringToId "Boolean"

uTrue :: Id
uTrue :: SORT
uTrue = String -> SORT
stringToId "True"

uFalse :: Id
uFalse :: SORT
uFalse = String -> SORT
stringToId "False"

tBoolean :: OP_TYPE
tBoolean :: OP_TYPE
tBoolean = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] SORT
uBoolean Range
nullRange

constBoolType :: OpType
constBoolType :: OpType
constBoolType = OP_TYPE -> OpType
toOpType OP_TYPE
tBoolean

qBoolean :: Id -> OP_SYMB
qBoolean :: SORT -> OP_SYMB
qBoolean c :: SORT
c = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
c OP_TYPE
tBoolean Range
nullRange

qTrue :: OP_SYMB
qTrue :: OP_SYMB
qTrue = SORT -> OP_SYMB
qBoolean SORT
uTrue

qFalse :: OP_SYMB
qFalse :: OP_SYMB
qFalse = SORT -> OP_SYMB
qBoolean SORT
uFalse

mkConstAppl :: OP_SYMB -> TERM f
mkConstAppl :: OP_SYMB -> TERM f
mkConstAppl o :: OP_SYMB
o = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
o [] Range
nullRange

aTrue :: TERM f
aTrue :: TERM f
aTrue = OP_SYMB -> TERM f
forall f. OP_SYMB -> TERM f
mkConstAppl OP_SYMB
qTrue

aFalse :: TERM f
aFalse :: TERM f
aFalse = OP_SYMB -> TERM f
forall f. OP_SYMB -> TERM f
mkConstAppl OP_SYMB
qFalse

uOpMap :: OpMap
uOpMap :: MapSet SORT OpType
uOpMap = [(SORT, [OpType])] -> MapSet SORT OpType
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList ([(SORT, [OpType])] -> MapSet SORT OpType)
-> [(SORT, [OpType])] -> MapSet SORT OpType
forall a b. (a -> b) -> a -> b
$ (SORT -> (SORT, [OpType])) -> [SORT] -> [(SORT, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: SORT
c -> (SORT
c, [OpType
constBoolType]))
  [SORT
uFalse, SORT
uTrue]

boolSig :: Sign f Procs
boolSig :: Sign f Procs
boolSig = (Procs -> Sign f Procs
forall e f. e -> Sign f e
emptySign Procs
emptyProcs)
  { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
uBoolean Rel SORT
forall a. Rel a
Rel.empty
  , opMap :: MapSet SORT OpType
opMap = MapSet SORT OpType
uOpMap }

lookupProc :: Id -> Sign f Procs -> Maybe Profile
lookupProc :: SORT -> Sign f Procs -> Maybe Profile
lookupProc i :: SORT
i = SORT -> Map SORT Profile -> Maybe Profile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
i (Map SORT Profile -> Maybe Profile)
-> (Sign f Procs -> Map SORT Profile)
-> Sign f Procs
-> Maybe Profile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Procs -> Map SORT Profile
procsMap (Procs -> Map SORT Profile)
-> (Sign f Procs -> Procs) -> Sign f Procs -> Map SORT Profile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo

procsSign :: Sign f Procs -> Sign f Procs
procsSign :: Sign f Procs -> Sign f Procs
procsSign sig :: Sign f Procs
sig = (Procs -> Sign f Procs
forall e f. e -> Sign f e
emptySign Procs
emptyProcs)
 { predMap :: MapSet SORT PredType
predMap = Procs -> MapSet SORT PredType
procsToPredMap (Procs -> MapSet SORT PredType) -> Procs -> MapSet SORT PredType
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo Sign f Procs
sig }

-- | add procs as predicate
addProcs :: Sign f Procs -> Sign f Procs
addProcs :: Sign f Procs -> Sign f Procs
addProcs 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
sig (Sign f Procs -> Sign f Procs) -> Sign f Procs -> Sign f Procs
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Sign f Procs
forall f. Sign f Procs -> Sign f Procs
procsSign Sign f Procs
sig

-- | remove procs as predicate
subProcs :: Sign f Procs -> Sign f Procs
subProcs :: Sign f Procs -> Sign f Procs
subProcs 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
diffSig Procs -> Procs -> Procs
forall a b. a -> b -> a
const Sign f Procs
sig (Sign f Procs -> Sign f Procs) -> Sign f Procs -> Sign f Procs
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Sign f Procs
forall f. Sign f Procs -> Sign f Procs
procsSign Sign f Procs
sig

checkCases :: Sign f e -> [Named Sentence] -> [Diagnosis]
checkCases :: Sign f e -> [Named Sentence] -> [Diagnosis]
checkCases sig2 :: Sign f e
sig2 sens :: [Named Sentence]
sens = Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
getCaseDiags Sign f e
sig2 [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ (Named Sentence -> [Diagnosis]) -> [Named Sentence] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
    (String -> Set SORT -> [Diagnosis]
getCases "var" (Set SORT -> [Diagnosis])
-> (Named Sentence -> Set SORT) -> Named Sentence -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token -> SORT) -> Set Token -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Token -> SORT
simpleIdToId (Set Token -> Set SORT)
-> (Named Sentence -> Set Token) -> Named Sentence -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Set Token
getVariables (Sentence -> Set Token)
-> (Named Sentence -> Sentence) -> Named Sentence -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) [Named Sentence]
sens

type VSEBasicSpec = BASIC_SPEC () Procdecls Dlformula

basicAna :: (VSEBasicSpec, VSESign, GlobalAnnos)
         -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
basicAna :: (VSEBasicSpec, VSESign, GlobalAnnos)
-> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
basicAna (bs :: VSEBasicSpec
bs, sig :: VSESign
sig, ga :: GlobalAnnos
ga) = do
  let sigIn :: VSESign
sigIn = VSESign -> VSESign
forall f. Sign f Procs -> Sign f Procs
subProcs (VSESign -> VSESign) -> VSESign -> VSESign
forall a b. (a -> b) -> a -> b
$ (Procs -> Procs -> Procs) -> VSESign -> VSESign -> VSESign
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 VSESign
sig VSESign
forall f. Sign f Procs
boolSig
  (bs2 :: VSEBasicSpec
bs2, ExtSign sig2 :: VSESign
sig2 syms :: Set Symbol
syms, sens :: [Named Sentence]
sens) <-
    Min (Ranged VSEforms) Procs
-> Ana () () Procdecls (Ranged VSEforms) Procs
-> Ana Procdecls () Procdecls (Ranged VSEforms) Procs
-> Mix () Procdecls (Ranged VSEforms) Procs
-> (VSEBasicSpec, VSESign, GlobalAnnos)
-> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis Min (Ranged VSEforms) Procs
minExpForm ((() -> State VSESign ())
-> Ana () () Procdecls (Ranged VSEforms) Procs
forall a b. a -> b -> a
const () -> State VSESign ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Ana Procdecls () Procdecls (Ranged VSEforms) Procs
anaProcdecls Mix () Procdecls (Ranged VSEforms) Procs
anaMix
        (VSEBasicSpec
bs, VSESign
sigIn, GlobalAnnos
ga)
  [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ VSESign -> [Named Sentence] -> [Diagnosis]
forall f e. Sign f e -> [Named Sentence] -> [Diagnosis]
checkCases VSESign
sig2 [Named Sentence]
sens
  [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ())
-> (Procs -> [Diagnosis]) -> Procs -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> Diagnosis) -> [SORT] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map
    (DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "illegal predicate declaration for procedure")
    ([SORT] -> [Diagnosis])
-> (Procs -> [SORT]) -> Procs -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> (Procs -> Set SORT) -> Procs -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet SORT PredType -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (MapSet SORT PredType -> Set SORT)
-> (Procs -> MapSet SORT PredType) -> Procs -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet SORT PredType
-> MapSet SORT PredType -> MapSet SORT PredType
interMapSet
      (MapSet SORT PredType
-> MapSet SORT PredType -> MapSet SORT PredType
diffMapSet (VSESign -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap VSESign
sig2) (MapSet SORT PredType -> MapSet SORT PredType)
-> MapSet SORT PredType -> MapSet SORT PredType
forall a b. (a -> b) -> a -> b
$ VSESign -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap VSESign
sigIn)
    (MapSet SORT PredType -> MapSet SORT PredType)
-> (Procs -> MapSet SORT PredType) -> Procs -> MapSet SORT PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Procs -> MapSet SORT PredType
procsToPredMap (Procs -> Result ()) -> Procs -> Result ()
forall a b. (a -> b) -> a -> b
$ VSESign -> Procs
forall f e. Sign f e -> e
extendedInfo VSESign
sig2
  let sig3 :: VSESign
sig3 = (Procs -> Procs -> Procs) -> VSESign -> VSESign -> VSESign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig Procs -> Procs -> Procs
forall a b. a -> b -> a
const VSESign
sig2 VSESign
forall f. Sign f Procs
boolSig
      (rSens :: [Named Sentence]
rSens, fSens :: [Named Sentence]
fSens) = (Named Sentence -> Bool)
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Record (Ranged VSEforms) Bool Bool -> Sentence -> Bool
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Bool -> Record (Ranged VSEforms) Bool Bool
forall f. Bool -> Record f Bool Bool
checkRec Bool
True) (Sentence -> Bool)
-> (Named Sentence -> Sentence) -> Named Sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) [Named Sentence]
sens
  [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Diagnosis) -> [Named Sentence] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> String -> Sentence -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unsupported VSE formula" (Sentence -> Diagnosis)
-> (Named Sentence -> Sentence) -> Named Sentence -> Diagnosis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) [Named Sentence]
fSens
  [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ())
-> (Set SORT -> [Diagnosis]) -> Set SORT -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> Diagnosis) -> [SORT] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "illegal overloading of")
    ([SORT] -> [Diagnosis])
-> (Set SORT -> [SORT]) -> Set SORT -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT])
-> (Set SORT -> Set SORT) -> Set SORT -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (MapSet SORT OpType -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (MapSet SORT OpType -> Set SORT) -> MapSet SORT OpType -> Set SORT
forall a b. (a -> b) -> a -> b
$ VSESign -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap VSESign
sig3)
    (Set SORT -> Result ()) -> Set SORT -> Result ()
forall a b. (a -> b) -> a -> b
$ MapSet SORT OpType -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet MapSet SORT OpType
uOpMap
  (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
-> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (VSEBasicSpec
bs2, VSESign -> Set Symbol -> ExtSign VSESign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign (VSESign -> VSESign
forall f. Sign f Procs -> Sign f Procs
addProcs VSESign
sig3) Set Symbol
syms, [Named Sentence]
rSens)

anaMix :: Mix () Procdecls Dlformula Procs
anaMix :: Mix () Procdecls (Ranged VSEforms) Procs
anaMix = Mix () Procdecls Any Procs
forall b s f e. Mix b s f e
emptyMix
  { putParen :: Ranged VSEforms -> Ranged VSEforms
putParen = Ranged VSEforms -> Ranged VSEforms
parenDlFormula
  , mixResolve :: MixResolve (Ranged VSEforms)
mixResolve = MixResolve (Ranged VSEforms)
resolveDlformula }

-- | put parens around ambiguous mixfix formulas (for error messages)
parenDlFormula :: Dlformula -> Dlformula
parenDlFormula :: Ranged VSEforms -> Ranged VSEforms
parenDlFormula (Ranged f :: VSEforms
f r :: Range
r) = case VSEforms
f of
  Dlformula b :: BoxOrDiamond
b p :: Program
p s :: Sentence
s ->
    let n :: Sentence
n = (Ranged VSEforms -> Ranged VSEforms) -> Sentence -> Sentence
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula Ranged VSEforms -> Ranged VSEforms
parenDlFormula Sentence
s
    in VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
b (Program -> Program
parenProg Program
p) Sentence
n) Range
r
  Defprocs ps :: [Defproc]
ps -> VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs ([Defproc] -> VSEforms) -> [Defproc] -> VSEforms
forall a b. (a -> b) -> a -> b
$ (Defproc -> Defproc) -> [Defproc] -> [Defproc]
forall a b. (a -> b) -> [a] -> [b]
map Defproc -> Defproc
parenDefproc [Defproc]
ps) Range
r
  _ -> VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged VSEforms
f Range
r -- no mixfix formulas?

parenProg :: Program -> Program
parenProg :: Program -> Program
parenProg = FoldRec Program -> Program -> Program
forall a. FoldRec a -> Program -> a
foldProg (FoldRec Program -> Program -> Program)
-> FoldRec Program -> Program -> Program
forall a b. (a -> b) -> a -> b
$ (TERM () -> TERM ())
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
mapProg ((() -> ()) -> TERM () -> TERM ()
forall f. (f -> f) -> TERM f -> TERM f
Paren.mapTerm () -> ()
forall a. a -> a
id) ((FORMULA () -> FORMULA ()) -> FoldRec Program)
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> FORMULA () -> FORMULA ()
forall f. (f -> f) -> FORMULA f -> FORMULA f
mapFormula () -> ()
forall a. a -> a
id

parenDefproc :: Defproc -> Defproc
parenDefproc :: Defproc -> Defproc
parenDefproc (Defproc k :: ProcKind
k i :: SORT
i vs :: [Token]
vs p :: Program
p r :: Range
r) = ProcKind -> SORT -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
k SORT
i [Token]
vs (Program -> Program
parenProg Program
p) Range
r

procsToPredMap :: Procs -> PredMap
procsToPredMap :: Procs -> MapSet SORT PredType
procsToPredMap (Procs m :: Map SORT Profile
m) =
  ((SORT, Profile) -> MapSet SORT PredType -> MapSet SORT PredType)
-> MapSet SORT PredType
-> [(SORT, Profile)]
-> MapSet SORT PredType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (n :: SORT
n, pr :: Profile
pr@(Profile _ mr :: Maybe SORT
mr)) pm :: MapSet SORT PredType
pm -> case Maybe SORT
mr of
          Nothing -> SORT -> PredType -> MapSet SORT PredType -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
n (Profile -> PredType
profileToPredType Profile
pr) MapSet SORT PredType
pm
          Just _ -> MapSet SORT PredType
pm) MapSet SORT PredType
forall a b. MapSet a b
MapSet.empty ([(SORT, Profile)] -> MapSet SORT PredType)
-> [(SORT, Profile)] -> MapSet SORT PredType
forall a b. (a -> b) -> a -> b
$ Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SORT Profile
m

procsToOpMap :: Procs -> OpMap
procsToOpMap :: Procs -> MapSet SORT OpType
procsToOpMap (Procs m :: Map SORT Profile
m) =
  ((SORT, Profile) -> MapSet SORT OpType -> MapSet SORT OpType)
-> MapSet SORT OpType -> [(SORT, Profile)] -> MapSet SORT OpType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (n :: SORT
n, pr :: Profile
pr) om :: MapSet SORT OpType
om -> case Profile -> Maybe OpType
profileToOpType Profile
pr of
          Just ot :: OpType
ot -> SORT -> OpType -> MapSet SORT OpType -> MapSet SORT OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
n OpType
ot MapSet SORT OpType
om
          Nothing -> MapSet SORT OpType
om) MapSet SORT OpType
forall a b. MapSet a b
MapSet.empty ([(SORT, Profile)] -> MapSet SORT OpType)
-> [(SORT, Profile)] -> MapSet SORT OpType
forall a b. (a -> b) -> a -> b
$ Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SORT Profile
m

-- | resolve mixfix applications of terms and formulas
resolveDlformula :: MixResolve Dlformula
resolveDlformula :: MixResolve (Ranged VSEforms)
resolveDlformula ga :: GlobalAnnos
ga rules :: (TokRules, Rules)
rules (Ranged f :: VSEforms
f r :: Range
r) = case VSEforms
f of
  Dlformula b :: BoxOrDiamond
b p :: Program
p s :: Sentence
s -> do
    Program
np <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
p
    Sentence
n <- (Ranged VSEforms -> Ranged VSEforms)
-> MixResolve (Ranged VSEforms) -> MixResolve Sentence
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm Ranged VSEforms -> Ranged VSEforms
forall a. a -> a
id MixResolve (Ranged VSEforms)
resolveDlformula GlobalAnnos
ga (TokRules, Rules)
rules Sentence
s
    Ranged VSEforms -> Result (Ranged VSEforms)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ranged VSEforms -> Result (Ranged VSEforms))
-> Ranged VSEforms -> Result (Ranged VSEforms)
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
b Program
np Sentence
n) Range
r
  Defprocs ps :: [Defproc]
ps -> do
    [Defproc]
nps <- (Defproc -> Result Defproc) -> [Defproc] -> Result [Defproc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MixResolve Defproc
resolveDefproc GlobalAnnos
ga (TokRules, Rules)
rules) [Defproc]
ps
    Ranged VSEforms -> Result (Ranged VSEforms)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ranged VSEforms -> Result (Ranged VSEforms))
-> Ranged VSEforms -> Result (Ranged VSEforms)
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs [Defproc]
nps) Range
r
  _ -> Ranged VSEforms -> Result (Ranged VSEforms)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ranged VSEforms -> Result (Ranged VSEforms))
-> Ranged VSEforms -> Result (Ranged VSEforms)
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged VSEforms
f Range
r -- no mixfix?

resolveT :: MixResolve (TERM ())
resolveT :: MixResolve (TERM ())
resolveT = (() -> ()) -> MixResolve () -> MixResolve (TERM ())
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm () -> ()
forall a. a -> a
id (Mix Any Any () Any -> MixResolve ()
forall b s f e. Mix b s f e -> MixResolve f
mixResolve Mix Any Any () Any
forall b s f e. Mix b s f e
emptyMix)

resolveF :: MixResolve (FORMULA ())
resolveF :: MixResolve (FORMULA ())
resolveF = (() -> ()) -> MixResolve () -> MixResolve (FORMULA ())
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm () -> ()
forall a. a -> a
id (Mix Any Any () Any -> MixResolve ()
forall b s f e. Mix b s f e -> MixResolve f
mixResolve Mix Any Any () Any
forall b s f e. Mix b s f e
emptyMix)

resolveProg :: MixResolve Program
resolveProg :: MixResolve Program
resolveProg ga :: GlobalAnnos
ga rules :: (TokRules, Rules)
rules p :: Program
p@(Ranged prg :: PlainProgram
prg r :: Range
r) = case PlainProgram
prg of
  Abort -> Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return Program
p
  Skip -> Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return Program
p
  Assign v :: Token
v t :: TERM ()
t -> do
    TERM ()
nt <- MixResolve (TERM ())
resolveT GlobalAnnos
ga (TokRules, Rules)
rules TERM ()
t
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Token -> TERM () -> PlainProgram
Assign Token
v TERM ()
nt) Range
r
  Call f :: FORMULA ()
f -> do
    FORMULA ()
nf <- MixResolve (FORMULA ())
resolveF GlobalAnnos
ga (TokRules, Rules)
rules FORMULA ()
f
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> PlainProgram
Call FORMULA ()
nf) Range
r
  Return t :: TERM ()
t -> do
    TERM ()
nt <- MixResolve (TERM ())
resolveT GlobalAnnos
ga (TokRules, Rules)
rules TERM ()
t
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (TERM () -> PlainProgram
Return TERM ()
nt) Range
r
  Block vs :: [VAR_DECL]
vs q :: Program
q -> do
    Program
np <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
q
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block [VAR_DECL]
vs Program
np) Range
r
  Seq p1 :: Program
p1 p2 :: Program
p2 -> do
    Program
p3 <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
p1
    Program
p4 <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
p2
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p3 Program
p4) Range
r
  If f :: FORMULA ()
f p1 :: Program
p1 p2 :: Program
p2 -> do
    FORMULA ()
c <- MixResolve (FORMULA ())
resolveF GlobalAnnos
ga (TokRules, Rules)
rules FORMULA ()
f
    Program
p3 <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
p1
    Program
p4 <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
p2
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If FORMULA ()
c Program
p3 Program
p4) Range
r
  While f :: FORMULA ()
f q :: Program
q -> do
    FORMULA ()
c <- MixResolve (FORMULA ())
resolveF GlobalAnnos
ga (TokRules, Rules)
rules FORMULA ()
f
    Program
np <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
q
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> PlainProgram
While FORMULA ()
c Program
np) Range
r

resolveDefproc :: MixResolve Defproc
resolveDefproc :: MixResolve Defproc
resolveDefproc ga :: GlobalAnnos
ga rules :: (TokRules, Rules)
rules (Defproc k :: ProcKind
k i :: SORT
i vs :: [Token]
vs p :: Program
p r :: Range
r) = do
  Program
np <- MixResolve Program
resolveProg GlobalAnnos
ga (TokRules, Rules)
rules Program
p
  Defproc -> Result Defproc
forall (m :: * -> *) a. Monad m => a -> m a
return (Defproc -> Result Defproc) -> Defproc -> Result Defproc
forall a b. (a -> b) -> a -> b
$ ProcKind -> SORT -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
k SORT
i [Token]
vs Program
np Range
r

-- | resolve overloading and type check terms and formulas
minExpForm :: Min Dlformula Procs
minExpForm :: Min (Ranged VSEforms) Procs
minExpForm sign :: VSESign
sign (Ranged f :: VSEforms
f r :: Range
r) = let sig :: Sign a Procs
sig = VSESign -> Sign a Procs
forall f e a. Sign f e -> Sign a e
castSign VSESign
sign in case VSEforms
f of
  Dlformula b :: BoxOrDiamond
b p :: Program
p s :: Sentence
s -> do
    Program
np <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
forall a. Set a
Set.empty Maybe SORT
forall a. Maybe a
Nothing Sign () Procs
forall f. Sign f Procs
sig Program
p
    Sentence
n <- Min (Ranged VSEforms) Procs
-> VSESign -> Sentence -> Result Sentence
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min (Ranged VSEforms) Procs
minExpForm VSESign
sign Sentence
s
    Ranged VSEforms -> Result (Ranged VSEforms)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ranged VSEforms -> Result (Ranged VSEforms))
-> Ranged VSEforms -> Result (Ranged VSEforms)
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
b Program
np Sentence
n) Range
r
  Defprocs ps :: [Defproc]
ps -> do
    [Defproc]
nps <- (Defproc -> Result Defproc) -> [Defproc] -> Result [Defproc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign () Procs -> Defproc -> Result Defproc
minProcdecl Sign () Procs
forall f. Sign f Procs
sig) [Defproc]
ps
    Ranged VSEforms -> Result (Ranged VSEforms)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ranged VSEforms -> Result (Ranged VSEforms))
-> Ranged VSEforms -> Result (Ranged VSEforms)
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs [Defproc]
nps) Range
r
  _ -> String -> Result (Ranged VSEforms)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "nyi for restricted constraints"

oneExpT :: Sign () Procs -> TERM () -> Result (TERM ())
oneExpT :: Sign () Procs -> TERM () -> Result (TERM ())
oneExpT = Min () Procs -> Sign () Procs -> TERM () -> Result (TERM ())
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm ((() -> Result ()) -> Min () Procs
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return)

minExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())
minExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())
minExpF = Min () Procs -> Sign () Procs -> FORMULA () -> Result (FORMULA ())
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA ((() -> Result ()) -> Min () Procs
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return)

checkRec :: Bool -> Record f Bool Bool
checkRec :: Bool -> Record f Bool Bool
checkRec b :: Bool
b = ((f -> Bool) -> ([Bool] -> Bool) -> Bool -> Record f Bool Bool
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord (Bool -> f -> Bool
forall a b. a -> b -> a
const Bool
False) [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and Bool
True)
  { foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> Bool -> Range -> Bool
foldQuantification = \ _ _ _ _ _ -> Bool
b
  , foldDefinedness :: FORMULA f -> Bool -> Range -> Bool
foldDefinedness = \ _ _ _ -> Bool
False
  , foldEquation :: FORMULA f -> Bool -> Equality -> Bool -> Range -> Bool
foldEquation = \ _ _ e :: Equality
e _ _ -> Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Strong
  , foldMembership :: FORMULA f -> Bool -> SORT -> Range -> Bool
foldMembership = \ _ _ _ _ -> Bool
False
  , foldCast :: TERM f -> Bool -> SORT -> Range -> Bool
foldCast = \ _ _ _ _ -> Bool
False
  , foldConditional :: TERM f -> Bool -> Bool -> Bool -> Range -> Bool
foldConditional = \ _ _ _ _ _ -> Bool
False
  , foldExtFORMULA :: FORMULA f -> f -> Bool
foldExtFORMULA = \ _ _ -> Bool
b }

minExpProg :: Set.Set VAR -> Maybe SORT -> Sign () Procs
           -> Program -> Result Program
minExpProg :: Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg invars :: Set Token
invars res :: Maybe SORT
res sig :: Sign () Procs
sig p :: Program
p@(Ranged prg :: PlainProgram
prg r :: Range
r) = let
  checkCond :: FORMULA f -> Result (FORMULA f)
checkCond f :: FORMULA f
f = if Record f Bool Bool -> FORMULA f -> Bool
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Bool -> Record f Bool Bool
forall f. Bool -> Record f Bool Bool
checkRec Bool
False) FORMULA f
f then FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f else
                    String -> FORMULA f -> Result (FORMULA f)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "illegal formula" FORMULA f
f
  checkTerm :: TERM f -> Result (TERM f)
checkTerm t :: TERM f
t = if Record f Bool Bool -> TERM f -> Bool
forall f a b. Record f a b -> TERM f -> b
foldTerm (Bool -> Record f Bool Bool
forall f. Bool -> Record f Bool Bool
checkRec Bool
False) TERM f
t then TERM f -> Result (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return TERM f
t else
                    String -> TERM f -> Result (TERM f)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "illegal term" TERM f
t
  in case PlainProgram
prg of
  Abort -> Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return Program
p
  Skip -> Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return Program
p
  Assign v :: Token
v t :: TERM ()
t -> case Token -> Map Token SORT -> Maybe SORT
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
v (Map Token SORT -> Maybe SORT) -> Map Token SORT -> Maybe SORT
forall a b. (a -> b) -> a -> b
$ Sign () Procs -> Map Token SORT
forall f e. Sign f e -> Map Token SORT
varMap Sign () Procs
sig of
    Nothing -> [Diagnosis] -> Maybe Program -> Result Program
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Token -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "undeclared program variable" Token
v] Maybe Program
forall a. Maybe a
Nothing
    Just s :: SORT
s -> do
      TERM ()
nt <- Sign () Procs -> TERM () -> Result (TERM ())
oneExpT Sign () Procs
sig (TERM () -> Result (TERM ())) -> TERM () -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
t SORT
s Range
r
      TERM () -> Result (TERM ())
forall f. FormExtension f => TERM f -> Result (TERM f)
checkTerm TERM ()
nt
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
v Set Token
invars)
        (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Token -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "assignment to input variable" Token
v]
      Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Token -> TERM () -> PlainProgram
Assign Token
v TERM ()
nt) Range
r
  Call f :: FORMULA ()
f -> case FORMULA ()
f of
    Predication ps :: PRED_SYMB
ps ts :: [TERM ()]
ts _ -> let i :: SORT
i = PRED_SYMB -> SORT
predSymbName PRED_SYMB
ps in
      case SORT -> Sign () Procs -> Maybe Profile
forall f. SORT -> Sign f Procs -> Maybe Profile
lookupProc SORT
i Sign () Procs
sig of
        Nothing -> [Diagnosis] -> Maybe Program -> Result Program
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown procedure" SORT
i] Maybe Program
forall a. Maybe a
Nothing
        Just pr :: Profile
pr@(Profile l :: [Procparam]
l re :: Maybe SORT
re) -> let
          nl :: [Procparam]
nl = case Maybe SORT
re of
             Nothing -> [Procparam]
l
             Just s :: SORT
s -> [Procparam]
l [Procparam] -> [Procparam] -> [Procparam]
forall a. [a] -> [a] -> [a]
++ [Paramkind -> SORT -> Procparam
Procparam Paramkind
Out SORT
s]
          in if [Procparam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Procparam]
nl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [TERM ()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM ()]
ts then
          [Diagnosis] -> Maybe Program -> Result Program
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "non-matching number of parameters for" SORT
i]
          Maybe Program
forall a. Maybe a
Nothing
             else do
          Sign () Procs
sign <- if [Procparam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Procparam]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Procparam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Procparam]
nl then
            [Diagnosis] -> Maybe (Sign () Procs) -> Result (Sign () Procs)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "function used as procedure" SORT
i] (Maybe (Sign () Procs) -> Result (Sign () Procs))
-> Maybe (Sign () Procs) -> Result (Sign () Procs)
forall a b. (a -> b) -> a -> b
$ Sign () Procs -> Maybe (Sign () Procs)
forall a. a -> Maybe a
Just
              Sign () Procs
sig { predMap :: MapSet SORT PredType
predMap = SORT -> PredType -> MapSet SORT PredType -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
i (Profile -> PredType
funProfileToPredType Profile
pr)
                    (MapSet SORT PredType -> MapSet SORT PredType)
-> MapSet SORT PredType -> MapSet SORT PredType
forall a b. (a -> b) -> a -> b
$ Sign () Procs -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign () Procs
sig }
            else Sign () Procs -> Result (Sign () Procs)
forall (m :: * -> *) a. Monad m => a -> m a
return Sign () Procs
sig { predMap :: MapSet SORT PredType
predMap = SORT -> PredType -> MapSet SORT PredType -> MapSet SORT PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
i (Profile -> PredType
profileToPredType Profile
pr)
                    (MapSet SORT PredType -> MapSet SORT PredType)
-> MapSet SORT PredType -> MapSet SORT PredType
forall a b. (a -> b) -> a -> b
$ Sign () Procs -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign () Procs
sig }
          FORMULA ()
nf <- Sign () Procs -> FORMULA () -> Result (FORMULA ())
minExpF Sign () Procs
sign FORMULA ()
f
          FORMULA () -> Result (FORMULA ())
forall f. FormExtension f => FORMULA f -> Result (FORMULA f)
checkCond FORMULA ()
nf
          Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> PlainProgram
Call FORMULA ()
nf) Range
r
    _ -> [Diagnosis] -> Maybe Program -> Result Program
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> FORMULA () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "no procedure call" FORMULA ()
f] Maybe Program
forall a. Maybe a
Nothing
  Return t :: TERM ()
t -> case Maybe SORT
res of
    Nothing -> [Diagnosis] -> Maybe Program -> Result Program
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> TERM () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unexpected return statement" TERM ()
t] Maybe Program
forall a. Maybe a
Nothing
    Just s :: SORT
s -> do
      TERM ()
nt <- Sign () Procs -> TERM () -> Result (TERM ())
oneExpT Sign () Procs
sig (TERM () -> Result (TERM ())) -> TERM () -> Result (TERM ())
forall a b. (a -> b) -> a -> b
$ TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
t SORT
s Range
r
      TERM () -> Result (TERM ())
forall f. FormExtension f => TERM f -> Result (TERM f)
checkTerm TERM ()
nt
      Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (TERM () -> PlainProgram
Return TERM ()
nt) Range
r
  Block vs :: [VAR_DECL]
vs q :: Program
q -> do
    let sign' :: Sign () Procs
sign' = State (Sign () Procs) () -> Sign () Procs -> Sign () Procs
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State (Sign () Procs) ())
-> [VAR_DECL] -> State (Sign () Procs) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign () Procs) ()
forall f. VAR_DECL -> State (Sign f Procs) ()
addVSEVars [VAR_DECL]
vs) Sign () Procs
sig { envDiags :: [Diagnosis]
envDiags = [] }
    [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ Sign () Procs -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags Sign () Procs
sign'
    Program
np <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
res Sign () Procs
sign' Program
q
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block [VAR_DECL]
vs Program
np) Range
r
  Seq p1 :: Program
p1 p2 :: Program
p2 -> do
    Program
p3 <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
res Sign () Procs
sig Program
p1
    Program
p4 <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
res Sign () Procs
sig Program
p2
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p3 Program
p4) Range
r
  If f :: FORMULA ()
f p1 :: Program
p1 p2 :: Program
p2 -> do
    FORMULA ()
c <- Sign () Procs -> FORMULA () -> Result (FORMULA ())
minExpF Sign () Procs
sig FORMULA ()
f
    FORMULA () -> Result (FORMULA ())
forall f. FormExtension f => FORMULA f -> Result (FORMULA f)
checkCond FORMULA ()
c
    Program
p3 <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
res Sign () Procs
sig Program
p1
    Program
p4 <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
res Sign () Procs
sig Program
p2
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If FORMULA ()
c Program
p3 Program
p4) Range
r
  While f :: FORMULA ()
f q :: Program
q -> do
    FORMULA ()
c <- Sign () Procs -> FORMULA () -> Result (FORMULA ())
minExpF Sign () Procs
sig FORMULA ()
f
    FORMULA () -> Result (FORMULA ())
forall f. FormExtension f => FORMULA f -> Result (FORMULA f)
checkCond FORMULA ()
c
    Program
np <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
res Sign () Procs
sig Program
q
    Program -> Result Program
forall (m :: * -> *) a. Monad m => a -> m a
return (Program -> Result Program) -> Program -> Result Program
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> PlainProgram
While FORMULA ()
c Program
np) Range
r

addVSEVars :: VAR_DECL -> State (Sign f Procs) ()
addVSEVars :: VAR_DECL -> State (Sign f Procs) ()
addVSEVars vd :: VAR_DECL
vd@(Var_decl vs :: [Token]
vs _ _) = do
    VAR_DECL -> State (Sign f Procs) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars VAR_DECL
vd
    Map SORT Profile
p <- (Sign f Procs -> Map SORT Profile)
-> State (Sign f Procs) (Map SORT Profile)
forall s a. (s -> a) -> State s a
gets ((Sign f Procs -> Map SORT Profile)
 -> State (Sign f Procs) (Map SORT Profile))
-> (Sign f Procs -> Map SORT Profile)
-> State (Sign f Procs) (Map SORT Profile)
forall a b. (a -> b) -> a -> b
$ Procs -> Map SORT Profile
procsMap (Procs -> Map SORT Profile)
-> (Sign f Procs -> Procs) -> Sign f Procs -> Map SORT Profile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo
    (Token -> State (Sign f Procs) ())
-> [Token] -> State (Sign f Procs) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Diagnosis] -> State (Sign f Procs) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f Procs) ())
-> (Token -> [Diagnosis]) -> Token -> State (Sign f Procs) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Map SORT Profile -> SORT -> [Diagnosis]
forall a. String -> String -> Map SORT a -> SORT -> [Diagnosis]
checkWithMap "var" "procedure" Map SORT Profile
p (SORT -> [Diagnosis]) -> (Token -> SORT) -> Token -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> SORT
simpleIdToId) [Token]
vs

minProcdecl :: Sign () Procs -> Defproc -> Result Defproc
minProcdecl :: Sign () Procs -> Defproc -> Result Defproc
minProcdecl sig :: Sign () Procs
sig (Defproc k :: ProcKind
k i :: SORT
i vs :: [Token]
vs p :: Program
p r :: Range
r) = case SORT -> Sign () Procs -> Maybe Profile
forall f. SORT -> Sign f Procs -> Maybe Profile
lookupProc SORT
i Sign () Procs
sig of
    Nothing -> [Diagnosis] -> Maybe Defproc -> Result Defproc
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown procedure" SORT
i] Maybe Defproc
forall a. Maybe a
Nothing
    Just (Profile l :: [Procparam]
l re :: Maybe SORT
re) -> if [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Procparam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Procparam]
l then
      [Diagnosis] -> Maybe Defproc -> Result Defproc
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown procedure" SORT
i] Maybe Defproc
forall a. Maybe a
Nothing
      else do
        let invars :: Set Token
invars = [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList ([Token] -> Set Token) -> [Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ ((Token, Procparam) -> Token) -> [(Token, Procparam)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Procparam) -> Token
forall a b. (a, b) -> a
fst ([(Token, Procparam)] -> [Token])
-> [(Token, Procparam)] -> [Token]
forall a b. (a -> b) -> a -> b
$
              ((Token, Procparam) -> Bool)
-> [(Token, Procparam)] -> [(Token, Procparam)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, Procparam j :: Paramkind
j _) -> Paramkind
j Paramkind -> Paramkind -> Bool
forall a. Eq a => a -> a -> Bool
== Paramkind
In) ([(Token, Procparam)] -> [(Token, Procparam)])
-> [(Token, Procparam)] -> [(Token, Procparam)]
forall a b. (a -> b) -> a -> b
$ [Token] -> [Procparam] -> [(Token, Procparam)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Token]
vs [Procparam]
l
        Program
np <- Set Token
-> Maybe SORT -> Sign () Procs -> Program -> Result Program
minExpProg Set Token
invars Maybe SORT
re Sign () Procs
sig { varMap :: Map Token SORT
varMap = [(Token, SORT)] -> Map Token SORT
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Token, SORT)] -> Map Token SORT)
-> [(Token, SORT)] -> Map Token SORT
forall a b. (a -> b) -> a -> b
$ (Token -> Procparam -> (Token, SORT))
-> [Token] -> [Procparam] -> [(Token, SORT)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
                (\ v :: Token
v (Procparam _ s :: SORT
s) -> (Token
v, SORT
s)) [Token]
vs [Procparam]
l } Program
p
        Defproc -> Result Defproc
forall (m :: * -> *) a. Monad m => a -> m a
return (Defproc -> Result Defproc) -> Defproc -> Result Defproc
forall a b. (a -> b) -> a -> b
$ ProcKind -> SORT -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
k SORT
i [Token]
vs Program
np Range
r

-- | analyse and add procedure declarations
anaProcdecls :: Ana Procdecls () Procdecls Dlformula Procs
anaProcdecls :: Ana Procdecls () Procdecls (Ranged VSEforms) Procs
anaProcdecls _ ds :: Procdecls
ds@(Procdecls ps :: [Annoted Sigentry]
ps _) = do
  (Annoted Sigentry -> State VSESign ())
-> [Annoted Sigentry] -> State VSESign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Sigentry -> State VSESign ()
anaProcdecl (Sigentry -> State VSESign ())
-> (Annoted Sigentry -> Sigentry)
-> Annoted Sigentry
-> State VSESign ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted Sigentry -> Sigentry
forall a. Annoted a -> a
item) [Annoted Sigentry]
ps
  Procdecls -> State VSESign Procdecls
forall (m :: * -> *) a. Monad m => a -> m a
return Procdecls
ds

anaProcdecl :: Sigentry -> State (Sign Dlformula Procs) ()
anaProcdecl :: Sigentry -> State VSESign ()
anaProcdecl (Procedure i :: SORT
i p :: Profile
p@(Profile ps :: [Procparam]
ps mr :: Maybe SORT
mr) q :: Range
q) = do
     VSESign
e <- State VSESign VSESign
forall s. State s s
get
     let prM :: MapSet SORT PredType
prM = VSESign -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap VSESign
e
         l :: Set PredType
l = SORT -> MapSet SORT PredType -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
i MapSet SORT PredType
prM
         ea :: Annoted ()
ea = () -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()
         isPred :: Bool
isPred = case Maybe SORT
mr of
           Nothing -> PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Profile -> PredType
profileToPredType Profile
p) Set PredType
l
           _ -> Bool
False
     (Procs -> Result Procs) -> State VSESign ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo (\ pm :: Procs
pm@(Procs m :: Map SORT Profile
m) ->
       let n :: Procs
n = Map SORT Profile -> Procs
Procs (Map SORT Profile -> Procs) -> Map SORT Profile -> Procs
forall a b. (a -> b) -> a -> b
$ SORT -> Profile -> Map SORT Profile -> Map SORT Profile
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
i Profile
p Map SORT Profile
m in case SORT -> Map SORT Profile -> Maybe Profile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
i Map SORT Profile
m of
         Just o :: Profile
o -> if Profile
p Profile -> Profile -> Bool
forall a. Eq a => a -> a -> Bool
== Profile
o then
           Procs -> String -> Range -> Result Procs
forall a. a -> String -> Range -> Result a
hint Procs
n ("repeated procedure " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
showId SORT
i "") Range
q
           else Procs -> String -> Range -> Result Procs
forall a. a -> String -> Range -> Result a
plain_error Procs
pm
             ("cannot change profile of procedure " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
showId SORT
i "") Range
q
         Nothing -> if Bool
isPred then Procs -> String -> Range -> Result Procs
forall a. a -> String -> Range -> Result a
plain_error Procs
pm
           ("cannot change predicate to procedure " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
showId SORT
i "") Range
q
           else Procs -> Result Procs
forall (m :: * -> *) a. Monad m => a -> m a
return Procs
n)
     case Profile -> Maybe OpType
profileToOpType Profile
p of
       Just t :: OpType
t -> do
         Bool -> State VSESign () -> State VSESign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Procparam -> Bool) -> [Procparam] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (Procparam j :: Paramkind
j _) -> Paramkind
j Paramkind -> Paramkind -> Bool
forall a. Eq a => a -> a -> Bool
== Paramkind
In) [Procparam]
ps)
           (State VSESign () -> State VSESign ())
-> State VSESign () -> State VSESign ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State VSESign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "function must have IN params only" SORT
i]
         Annoted () -> OpType -> SORT -> State VSESign ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp Annoted ()
ea OpType
t SORT
i
       _ -> Bool -> State VSESign () -> State VSESign ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
isPred
         (State VSESign () -> State VSESign ())
-> State VSESign () -> State VSESign ()
forall a b. (a -> b) -> a -> b
$ Annoted () -> Symbol -> State VSESign ()
forall a f e. Annoted a -> Symbol -> State (Sign f e) ()
addAnnoSet Annoted ()
ea (Symbol -> State VSESign ()) -> Symbol -> State VSESign ()
forall a b. (a -> b) -> a -> b
$ SORT -> SymbType -> Symbol
Symbol SORT
i (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> SymbType
PredAsItemType (PredType -> SymbType) -> PredType -> SymbType
forall a b. (a -> b) -> a -> b
$ Profile -> PredType
profileToPredType Profile
p

paramsToArgs :: [Procparam] -> [SORT]
paramsToArgs :: [Procparam] -> [SORT]
paramsToArgs = (Procparam -> SORT) -> [Procparam] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Procparam _ s :: SORT
s) -> SORT
s)

profileToPredType :: Profile -> PredType
profileToPredType :: Profile -> PredType
profileToPredType (Profile a :: [Procparam]
a _) = [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ [Procparam] -> [SORT]
paramsToArgs [Procparam]
a

funProfileToPredType :: Profile -> PredType
funProfileToPredType :: Profile -> PredType
funProfileToPredType (Profile a :: [Procparam]
a r :: Maybe SORT
r) = case Maybe SORT
r of
  Nothing -> String -> PredType
forall a. HasCallStack => String -> a
error "funProfileToPredType"
  Just s :: SORT
s -> [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ [Procparam] -> [SORT]
paramsToArgs [Procparam]
a [SORT] -> [SORT] -> [SORT]
forall a. [a] -> [a] -> [a]
++ [SORT
s]

profileToOpType :: Profile -> Maybe OpType
profileToOpType :: Profile -> Maybe OpType
profileToOpType (Profile a :: [Procparam]
a r :: Maybe SORT
r) = case Maybe SORT
r of
  Nothing -> Maybe OpType
forall a. Maybe a
Nothing
  Just s :: SORT
s -> OpType -> Maybe OpType
forall a. a -> Maybe a
Just (OpType -> Maybe OpType) -> OpType -> Maybe OpType
forall a b. (a -> b) -> a -> b
$ OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Partial ([Procparam] -> [SORT]
paramsToArgs [Procparam]
a) SORT
s

castSign :: Sign f e -> Sign a e
castSign :: Sign f e -> Sign a e
castSign s :: Sign f e
s = Sign f e
s { sentences :: [Named (FORMULA a)]
sentences = [] }

castMor :: Morphism f e b -> Morphism a e b
castMor :: Morphism f e b -> Morphism a e b
castMor m :: Morphism f e b
m = Morphism f e b
m
  { msource :: Sign a e
msource = Sign f e -> Sign a e
forall f e a. Sign f e -> Sign a e
castSign (Sign f e -> Sign a e) -> Sign f e -> Sign a e
forall a b. (a -> b) -> a -> b
$ Morphism f e b -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e b
m
  , mtarget :: Sign a e
mtarget = Sign f e -> Sign a e
forall f e a. Sign f e -> Sign a e
castSign (Sign f e -> Sign a e) -> Sign f e -> Sign a e
forall a b. (a -> b) -> a -> b
$ Morphism f e b -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e b
m }

type VSEMorExt = DefMorExt Procs
type VSEMor = Morphism Dlformula Procs VSEMorExt

-- | apply a morphism
mapMorProg :: Morphism f Procs VSEMorExt -> Program -> Program
mapMorProg :: Morphism f Procs VSEMorExt -> Program -> Program
mapMorProg mor :: Morphism f Procs VSEMorExt
mor = let m :: Morphism a Procs VSEMorExt
m = Morphism f Procs VSEMorExt -> Morphism a Procs VSEMorExt
forall f e b a. Morphism f e b -> Morphism a e b
castMor Morphism f Procs VSEMorExt
mor in
  FoldRec Program -> Program -> Program
forall a. FoldRec a -> Program -> a
foldProg ((TERM () -> TERM ())
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
mapProg (MapSen () Procs VSEMorExt
-> Morphism () Procs VSEMorExt -> TERM () -> TERM ()
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
MapSen.mapTerm ((() -> ()) -> MapSen () Procs VSEMorExt
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) Morphism () Procs VSEMorExt
forall a. Morphism a Procs VSEMorExt
m)
    ((FORMULA () -> FORMULA ()) -> FoldRec Program)
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
forall a b. (a -> b) -> a -> b
$ MapSen () Procs VSEMorExt
-> Morphism () Procs VSEMorExt -> FORMULA () -> FORMULA ()
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen ((() -> ()) -> MapSen () Procs VSEMorExt
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) Morphism () Procs VSEMorExt
forall a. Morphism a Procs VSEMorExt
m)
    { foldBlock :: Program -> [VAR_DECL] -> Program -> Program
foldBlock = \ (Ranged _ r :: Range
r) vs :: [VAR_DECL]
vs p :: Program
p ->
        PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block ((VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism Any Procs VSEMorExt -> VAR_DECL -> VAR_DECL
forall f e m. Morphism f e m -> VAR_DECL -> VAR_DECL
mapVars Morphism Any Procs VSEMorExt
forall a. Morphism a Procs VSEMorExt
m) [VAR_DECL]
vs) Program
p) Range
r
    , foldCall :: Program -> FORMULA () -> Program
foldCall = \ (Ranged _ r :: Range
r) f :: FORMULA ()
f -> case FORMULA ()
f of
     Predication (Qual_pred_name i :: SORT
i (Pred_type args :: [SORT]
args r1 :: Range
r1) r2 :: Range
r2) ts :: [TERM ()]
ts r3 :: Range
r3 ->
      case SORT -> Sign f Procs -> Maybe Profile
forall f. SORT -> Sign f Procs -> Maybe Profile
lookupProc SORT
i (Sign f Procs -> Maybe Profile) -> Sign f Procs -> Maybe Profile
forall a b. (a -> b) -> a -> b
$ Morphism f Procs VSEMorExt -> Sign f Procs
forall f e m. Morphism f e m -> Sign f e
msource Morphism f Procs VSEMorExt
mor of
        Nothing -> String -> Program
forall a. HasCallStack => String -> a
error "mapMorProg"
        Just pr :: Profile
pr -> let
          j :: SORT
j = Morphism f Procs VSEMorExt -> SORT -> Profile -> SORT
forall f. Morphism f Procs VSEMorExt -> SORT -> Profile -> SORT
mapProcIdProfile Morphism f Procs VSEMorExt
mor SORT
i Profile
pr
          nargs :: [SORT]
nargs = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism f Procs VSEMorExt -> SORT -> SORT
forall f e m. Morphism f e m -> SORT -> SORT
mapSrt Morphism f Procs VSEMorExt
mor) [SORT]
args
          nts :: [TERM ()]
nts = (TERM () -> TERM ()) -> [TERM ()] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (MapSen () Procs VSEMorExt
-> Morphism () Procs VSEMorExt -> TERM () -> TERM ()
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
MapSen.mapTerm ((() -> ()) -> MapSen () Procs VSEMorExt
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) Morphism () Procs VSEMorExt
forall a. Morphism a Procs VSEMorExt
m) [TERM ()]
ts
          in 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
                (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
j ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
nargs Range
r1) Range
r2) [TERM ()]
nts Range
r3) Range
r
     _ -> String -> Program
forall a. HasCallStack => String -> a
error (String -> Program) -> String -> Program
forall a b. (a -> b) -> a -> b
$ "mapMorProg " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FORMULA () -> String
forall a. Show a => a -> String
show FORMULA ()
f }

mapProcId :: Morphism f Procs VSEMorExt -> Id -> Id
mapProcId :: Morphism f Procs VSEMorExt -> SORT -> SORT
mapProcId m :: Morphism f Procs VSEMorExt
m i :: SORT
i = case SORT -> Sign f Procs -> Maybe Profile
forall f. SORT -> Sign f Procs -> Maybe Profile
lookupProc SORT
i (Sign f Procs -> Maybe Profile) -> Sign f Procs -> Maybe Profile
forall a b. (a -> b) -> a -> b
$ Morphism f Procs VSEMorExt -> Sign f Procs
forall f e m. Morphism f e m -> Sign f e
msource Morphism f Procs VSEMorExt
m of
  Just p :: Profile
p -> Morphism f Procs VSEMorExt -> SORT -> Profile -> SORT
forall f. Morphism f Procs VSEMorExt -> SORT -> Profile -> SORT
mapProcIdProfile Morphism f Procs VSEMorExt
m SORT
i Profile
p
  Nothing -> String -> SORT
forall a. HasCallStack => String -> a
error (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ "VSE.mapProcId unknown " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
i

mapProcIdProfile :: Morphism f Procs VSEMorExt -> Id -> Profile -> Id
mapProcIdProfile :: Morphism f Procs VSEMorExt -> SORT -> Profile -> SORT
mapProcIdProfile m :: Morphism f Procs VSEMorExt
m = Sort_map -> Op_map -> Pred_map -> SORT -> Profile -> SORT
mapProcIdProfileExt (Morphism f Procs VSEMorExt -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f Procs VSEMorExt
m) (Morphism f Procs VSEMorExt -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f Procs VSEMorExt
m) (Morphism f Procs VSEMorExt -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f Procs VSEMorExt
m)

mapProcIdProfileExt :: Sort_map -> Op_map -> Pred_map -> Id -> Profile -> Id
mapProcIdProfileExt :: Sort_map -> Op_map -> Pred_map -> SORT -> Profile -> SORT
mapProcIdProfileExt sm :: Sort_map
sm om :: Op_map
om pm :: Pred_map
pm i :: SORT
i p :: Profile
p = case Profile -> Maybe OpType
profileToOpType Profile
p of
  Just t :: OpType
t -> (SORT, OpType) -> SORT
forall a b. (a, b) -> a
fst ((SORT, OpType) -> SORT) -> (SORT, OpType) -> SORT
forall a b. (a -> b) -> a -> b
$ Sort_map -> Op_map -> (SORT, OpType) -> (SORT, OpType)
mapOpSym Sort_map
sm Op_map
om (SORT
i, OpType
t)
  Nothing -> (SORT, PredType) -> SORT
forall a b. (a, b) -> a
fst ((SORT, PredType) -> SORT) -> (SORT, PredType) -> SORT
forall a b. (a -> b) -> a -> b
$ Sort_map -> Pred_map -> (SORT, PredType) -> (SORT, PredType)
mapPredSym Sort_map
sm Pred_map
pm (SORT
i, Profile -> PredType
profileToPredType Profile
p)

mapMorDefproc :: Morphism f Procs VSEMorExt -> Defproc -> Defproc
mapMorDefproc :: Morphism f Procs VSEMorExt -> Defproc -> Defproc
mapMorDefproc m :: Morphism f Procs VSEMorExt
m (Defproc k :: ProcKind
k i :: SORT
i vs :: [Token]
vs p :: Program
p r :: Range
r) =
  ProcKind -> SORT -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
k (Morphism f Procs VSEMorExt -> SORT -> SORT
forall f. Morphism f Procs VSEMorExt -> SORT -> SORT
mapProcId Morphism f Procs VSEMorExt
m SORT
i) [Token]
vs (Morphism f Procs VSEMorExt -> Program -> Program
forall f. Morphism f Procs VSEMorExt -> Program -> Program
mapMorProg Morphism f Procs VSEMorExt
m Program
p) Range
r

mapDlformula :: MapSen Dlformula Procs VSEMorExt
mapDlformula :: MapSen (Ranged VSEforms) Procs VSEMorExt
mapDlformula m :: Morphism (Ranged VSEforms) Procs VSEMorExt
m (Ranged f :: VSEforms
f r :: Range
r) = case VSEforms
f of
  Dlformula b :: BoxOrDiamond
b p :: Program
p s :: Sentence
s ->
    let n :: Sentence
n = MapSen (Ranged VSEforms) Procs VSEMorExt
-> Morphism (Ranged VSEforms) Procs VSEMorExt
-> Sentence
-> Sentence
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen (Ranged VSEforms) Procs VSEMorExt
mapDlformula Morphism (Ranged VSEforms) Procs VSEMorExt
m Sentence
s
    in VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
b (Morphism (Ranged VSEforms) Procs VSEMorExt -> Program -> Program
forall f. Morphism f Procs VSEMorExt -> Program -> Program
mapMorProg Morphism (Ranged VSEforms) Procs VSEMorExt
m Program
p) Sentence
n) Range
r
  Defprocs ps :: [Defproc]
ps -> VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs ([Defproc] -> VSEforms) -> [Defproc] -> VSEforms
forall a b. (a -> b) -> a -> b
$ (Defproc -> Defproc) -> [Defproc] -> [Defproc]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism (Ranged VSEforms) Procs VSEMorExt -> Defproc -> Defproc
forall f. Morphism f Procs VSEMorExt -> Defproc -> Defproc
mapMorDefproc Morphism (Ranged VSEforms) Procs VSEMorExt
m) [Defproc]
ps) Range
r
  RestrictedConstraint constr :: [Constraint]
constr restr :: Sort_map
restr flag :: Bool
flag ->
   VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
    ([Constraint] -> Sort_map -> Bool -> VSEforms
RestrictedConstraint
       ((Constraint -> Constraint) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism (Ranged VSEforms) Procs VSEMorExt
-> Constraint -> Constraint
forall f e m. Morphism f e m -> Constraint -> Constraint
MapSen.mapConstr Morphism (Ranged VSEforms) Procs VSEMorExt
m) [Constraint]
constr)
       ([(SORT, SORT)] -> Sort_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        ([(SORT, SORT)] -> Sort_map) -> [(SORT, SORT)] -> Sort_map
forall a b. (a -> b) -> a -> b
$ ((SORT, SORT) -> (SORT, SORT)) -> [(SORT, SORT)] -> [(SORT, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, i :: SORT
i) -> (Sort_map -> SORT -> SORT
mapSort (Morphism (Ranged VSEforms) Procs VSEMorExt -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism (Ranged VSEforms) Procs VSEMorExt
m) SORT
s, Morphism (Ranged VSEforms) Procs VSEMorExt -> SORT -> SORT
forall f. Morphism f Procs VSEMorExt -> SORT -> SORT
mapProcId Morphism (Ranged VSEforms) Procs VSEMorExt
m SORT
i))
        ([(SORT, SORT)] -> [(SORT, SORT)])
-> [(SORT, SORT)] -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ Sort_map -> [(SORT, SORT)]
forall k a. Map k a -> [(k, a)]
Map.toList Sort_map
restr)
    Bool
flag) Range
r

-- | simplify fully qualified terms and formulas for pretty printing sentences
simpProg :: Sign () e -> Program -> Program
simpProg :: Sign () e -> Program -> Program
simpProg sig :: Sign () e
sig =
  FoldRec Program -> Program -> Program
forall a. FoldRec a -> Program -> a
foldProg ((TERM () -> TERM ())
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
mapProg (Sign () e -> TERM () -> TERM ()
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> TERM f -> TERM f
simplifyCASLTerm Sign () e
sig)
  ((FORMULA () -> FORMULA ()) -> FoldRec Program)
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
forall a b. (a -> b) -> a -> b
$ Sign () e -> FORMULA () -> FORMULA ()
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen Sign () e
sig)
    { foldBlock :: Program -> [VAR_DECL] -> Program -> Program
foldBlock = \ (Ranged b :: PlainProgram
b r :: Range
r) _ _ -> case PlainProgram
b of
                  Block vs :: [VAR_DECL]
vs p :: Program
p -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block [VAR_DECL]
vs (Program -> PlainProgram) -> Program -> PlainProgram
forall a b. (a -> b) -> a -> b
$ Sign () e -> Program -> Program
forall e. Sign () e -> Program -> Program
simpProg
                           (State (Sign () e) () -> Sign () e -> Sign () e
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State (Sign () e) ())
-> [VAR_DECL] -> State (Sign () e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign () e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs) Sign () e
sig) Program
p) Range
r
                  _ -> String -> Program
forall a. HasCallStack => String -> a
error "VSE.Ana.simpProg" }

simpDefproc :: Sign () Procs -> Defproc -> Defproc
simpDefproc :: Sign () Procs -> Defproc -> Defproc
simpDefproc sign :: Sign () Procs
sign (Defproc k :: ProcKind
k i :: SORT
i vs :: [Token]
vs p :: Program
p r :: Range
r) =
  let sig :: Sign () Procs
sig = case SORT -> Sign () Procs -> Maybe Profile
forall f. SORT -> Sign f Procs -> Maybe Profile
lookupProc SORT
i Sign () Procs
sign of
              Nothing -> Sign () Procs
sign
              Just (Profile l :: [Procparam]
l _) -> if [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Procparam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Procparam]
l then Sign () Procs
sign
                else Sign () Procs
sign { varMap :: Map Token SORT
varMap = [(Token, SORT)] -> Map Token SORT
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Token, SORT)] -> Map Token SORT)
-> [(Token, SORT)] -> Map Token SORT
forall a b. (a -> b) -> a -> b
$ (Token -> Procparam -> (Token, SORT))
-> [Token] -> [Procparam] -> [(Token, SORT)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
                            (\ v :: Token
v (Procparam _ s :: SORT
s) -> (Token
v, SORT
s)) [Token]
vs [Procparam]
l }
  in ProcKind -> SORT -> [Token] -> Program -> Range -> Defproc
Defproc ProcKind
k SORT
i [Token]
vs (Sign () Procs -> Program -> Program
forall e. Sign () e -> Program -> Program
simpProg Sign () Procs
sig Program
p) Range
r

simpDlformula :: Sign Dlformula Procs -> Dlformula -> Dlformula
simpDlformula :: VSESign -> Ranged VSEforms -> Ranged VSEforms
simpDlformula sign :: VSESign
sign (Ranged f :: VSEforms
f r :: Range
r) = let sig :: Sign a Procs
sig = VSESign -> Sign a Procs
forall f e a. Sign f e -> Sign a e
castSign VSESign
sign in case VSEforms
f of
  Dlformula b :: BoxOrDiamond
b p :: Program
p s :: Sentence
s -> let
    q :: Program
q = Sign () Procs -> Program -> Program
forall e. Sign () e -> Program -> Program
simpProg Sign () Procs
forall f. Sign f Procs
sig Program
p
    n :: Sentence
n = Min (Ranged VSEforms) Procs
-> (VSESign -> Ranged VSEforms -> Ranged VSEforms)
-> VSESign
-> Sentence
-> Sentence
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min (Ranged VSEforms) Procs
minExpForm VSESign -> Ranged VSEforms -> Ranged VSEforms
simpDlformula VSESign
sign Sentence
s
    in VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged (BoxOrDiamond -> Program -> Sentence -> VSEforms
Dlformula BoxOrDiamond
b Program
q Sentence
n) Range
r
  Defprocs ps :: [Defproc]
ps -> VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged ([Defproc] -> VSEforms
Defprocs ([Defproc] -> VSEforms) -> [Defproc] -> VSEforms
forall a b. (a -> b) -> a -> b
$ (Defproc -> Defproc) -> [Defproc] -> [Defproc]
forall a b. (a -> b) -> [a] -> [b]
map (Sign () Procs -> Defproc -> Defproc
simpDefproc Sign () Procs
forall f. Sign f Procs
sig) [Defproc]
ps) Range
r
  RestrictedConstraint {} -> VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged VSEforms
f Range
r
    -- how should this be for restricted constraints?

-- | free variables to be universally bound on the top level
freeProgVars :: Sign () e -> Program -> VarSet
freeProgVars :: Sign () e -> Program -> VarSet
freeProgVars sig :: Sign () e
sig = let ft :: TERM () -> VarSet
ft = Sign () e -> TERM () -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign () e
sig in
  FoldRec VarSet -> Program -> VarSet
forall a. FoldRec a -> Program -> a
foldProg ((TERM () -> VarSet) -> (FORMULA () -> VarSet) -> FoldRec VarSet
forall a.
Ord a =>
(TERM () -> Set a) -> (FORMULA () -> Set a) -> FoldRec (Set a)
progToSetRec TERM () -> VarSet
ft (Sign () e -> FORMULA () -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign () e
sig))
  { foldAssign :: Program -> Token -> TERM () -> VarSet
foldAssign = \ _ v :: Token
v t :: TERM ()
t -> (case Token -> Map Token SORT -> Maybe SORT
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
v (Map Token SORT -> Maybe SORT) -> Map Token SORT -> Maybe SORT
forall a b. (a -> b) -> a -> b
$ Sign () e -> Map Token SORT
forall f e. Sign f e -> Map Token SORT
varMap Sign () e
sig of
      Just s :: SORT
s -> (Token, SORT) -> VarSet -> VarSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Token
v, SORT
s)
      Nothing -> (Token, SORT) -> VarSet -> VarSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Token
v, TERM () -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM ()
t)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ TERM () -> VarSet
ft TERM ()
t
  , foldBlock :: Program -> [VAR_DECL] -> VarSet -> VarSet
foldBlock = \ (Ranged b :: PlainProgram
b _) _ _ -> case PlainProgram
b of
      Block vs :: [VAR_DECL]
vs p :: Program
p ->
        VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign () e -> Program -> VarSet
forall e. Sign () e -> Program -> VarSet
freeProgVars (State (Sign () e) () -> Sign () e -> Sign () e
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State (Sign () e) ())
-> [VAR_DECL] -> State (Sign () e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign () e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs) Sign () e
sig) Program
p)
          (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ [(Token, SORT)] -> VarSet
forall a. Ord a => [a] -> Set a
Set.fromList ([(Token, SORT)] -> VarSet) -> [(Token, SORT)] -> VarSet
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, SORT)]
flatVAR_DECLs [VAR_DECL]
vs
      _ -> String -> VarSet
forall a. HasCallStack => String -> a
error "VSE.Ana.freeProgVars" }

freeDlVars :: Sign Dlformula e -> Dlformula -> VarSet
freeDlVars :: Sign (Ranged VSEforms) e -> Ranged VSEforms -> VarSet
freeDlVars sig :: Sign (Ranged VSEforms) e
sig (Ranged f :: VSEforms
f _) = case VSEforms
f of
  Dlformula _ p :: Program
p s :: Sentence
s -> VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign () e -> Program -> VarSet
forall e. Sign () e -> Program -> VarSet
freeProgVars (Sign (Ranged VSEforms) e -> Sign () e
forall f e a. Sign f e -> Sign a e
castSign Sign (Ranged VSEforms) e
sig) Program
p) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
          Sign (Ranged VSEforms) e -> Sentence -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign (Ranged VSEforms) e
sig Sentence
s
  Defprocs _ -> VarSet
forall a. Set a
Set.empty
  RestrictedConstraint {} -> VarSet
forall a. Set a
Set.empty

instance TermExtension Dlformula where
  freeVarsOfExt :: Sign (Ranged VSEforms) e -> Ranged VSEforms -> VarSet
freeVarsOfExt = Sign (Ranged VSEforms) e -> Ranged VSEforms -> VarSet
forall e. Sign (Ranged VSEforms) e -> Ranged VSEforms -> VarSet
freeDlVars

-- | adjust procs map in morphism target signature
correctTarget :: Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget :: Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget m :: Morphism f Procs VSEMorExt
m = Morphism f Procs VSEMorExt
m
  { mtarget :: Sign f Procs
mtarget = Sign f Procs -> Sign f Procs
forall f. Sign f Procs -> Sign f Procs
correctSign (Sign f Procs -> Sign f Procs) -> Sign f Procs -> Sign f Procs
forall a b. (a -> b) -> a -> b
$ Morphism f Procs VSEMorExt -> Sign f Procs
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f Procs VSEMorExt
m
  , msource :: Sign f Procs
msource = Sign f Procs -> Sign f Procs
forall f. Sign f Procs -> Sign f Procs
correctSign (Sign f Procs -> Sign f Procs) -> Sign f Procs -> Sign f Procs
forall a b. (a -> b) -> a -> b
$ Morphism f Procs VSEMorExt -> Sign f Procs
forall f e m. Morphism f e m -> Sign f e
msource Morphism f Procs VSEMorExt
m }

inducedExt :: InducedSign f Procs VSEMorExt Procs
inducedExt :: InducedSign f Procs VSEMorExt Procs
inducedExt sm :: Sort_map
sm om :: Op_map
om pm :: Pred_map
pm _ = Map SORT Profile -> Procs
Procs (Map SORT Profile -> Procs)
-> (Sign f Procs -> Map SORT Profile) -> Sign f Procs -> Procs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SORT, Profile)] -> Map SORT Profile
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    ([(SORT, Profile)] -> Map SORT Profile)
-> (Sign f Procs -> [(SORT, Profile)])
-> Sign f Procs
-> Map SORT Profile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SORT, Profile) -> (SORT, Profile))
-> [(SORT, Profile)] -> [(SORT, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: SORT
i, p :: Profile
p) -> (Sort_map -> Op_map -> Pred_map -> SORT -> Profile -> SORT
mapProcIdProfileExt Sort_map
sm Op_map
om Pred_map
pm SORT
i Profile
p, Sort_map -> Profile -> Profile
mapProfile Sort_map
sm Profile
p))
    ([(SORT, Profile)] -> [(SORT, Profile)])
-> (Sign f Procs -> [(SORT, Profile)])
-> Sign f Procs
-> [(SORT, Profile)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map SORT Profile -> [(SORT, Profile)])
-> (Sign f Procs -> Map SORT Profile)
-> Sign f Procs
-> [(SORT, Profile)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Procs -> Map SORT Profile
procsMap (Procs -> Map SORT Profile)
-> (Sign f Procs -> Procs) -> Sign f Procs -> Map SORT Profile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo

correctSign :: Sign f Procs -> Sign f Procs
correctSign :: Sign f Procs -> Sign f Procs
correctSign sig :: Sign f Procs
sig = Sign f Procs
sig
  { extendedInfo :: Procs
extendedInfo = Map SORT Profile -> Procs
Procs (Map SORT Profile -> Procs) -> Map SORT Profile -> Procs
forall a b. (a -> b) -> a -> b
$ (SORT -> Profile -> Bool) -> Map SORT Profile -> Map SORT Profile
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ i :: SORT
i p :: Profile
p -> case Profile -> Maybe OpType
profileToOpType Profile
p of
         Just t :: OpType
t -> let s :: Set OpType
s = SORT -> MapSet SORT OpType -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
i (MapSet SORT OpType -> Set OpType)
-> MapSet SORT OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f Procs
sig in
           OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
t Set OpType
s Bool -> Bool -> Bool
|| OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (OpType -> OpType
mkTotal OpType
t) Set OpType
s
         Nothing ->
           PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Profile -> PredType
profileToPredType Profile
p) (Set PredType -> Bool)
-> (MapSet SORT PredType -> Set PredType)
-> MapSet SORT PredType
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> MapSet SORT PredType -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
i (MapSet SORT PredType -> Bool) -> MapSet SORT PredType -> Bool
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign f Procs
sig
         ) (Map SORT Profile -> Map SORT Profile)
-> Map SORT Profile -> Map SORT Profile
forall a b. (a -> b) -> a -> b
$ Procs -> Map SORT Profile
procsMap (Procs -> Map SORT Profile) -> Procs -> Map SORT Profile
forall a b. (a -> b) -> a -> b
$ Sign f Procs -> Procs
forall f e. Sign f e -> e
extendedInfo Sign f Procs
sig }

mapProfile :: Sort_map -> Profile -> Profile
mapProfile :: Sort_map -> Profile -> Profile
mapProfile m :: Sort_map
m (Profile l :: [Procparam]
l r :: Maybe SORT
r) = [Procparam] -> Maybe SORT -> Profile
Profile
  ((Procparam -> Procparam) -> [Procparam] -> [Procparam]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Procparam k :: Paramkind
k s :: SORT
s) -> Paramkind -> SORT -> Procparam
Procparam Paramkind
k (SORT -> Procparam) -> SORT -> Procparam
forall a b. (a -> b) -> a -> b
$ Sort_map -> SORT -> SORT
mapSort Sort_map
m SORT
s) [Procparam]
l)
  (Maybe SORT -> Profile) -> Maybe SORT -> Profile
forall a b. (a -> b) -> a -> b
$ (SORT -> SORT) -> Maybe SORT -> Maybe SORT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sort_map -> SORT -> SORT
mapSort Sort_map
m) Maybe SORT
r

extVSEColimit :: Gr Procs (Int, VSEMorExt) ->
                  Map.Map Int VSEMor ->
                  (Procs, Map.Map Int VSEMorExt)
extVSEColimit :: Gr Procs (Int, VSEMorExt)
-> Map Int (Morphism (Ranged VSEforms) Procs VSEMorExt)
-> (Procs, Map Int VSEMorExt)
extVSEColimit graph :: Gr Procs (Int, VSEMorExt)
graph morMap :: Map Int (Morphism (Ranged VSEforms) Procs VSEMorExt)
morMap = let
  procs :: Map SORT Profile
procs = [(SORT, Profile)] -> Map SORT Profile
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SORT, Profile)] -> Map SORT Profile)
-> [(SORT, Profile)] -> Map SORT Profile
forall a b. (a -> b) -> a -> b
$ [(SORT, Profile)] -> [(SORT, Profile)]
forall a. Eq a => [a] -> [a]
nub ([(SORT, Profile)] -> [(SORT, Profile)])
-> [(SORT, Profile)] -> [(SORT, Profile)]
forall a b. (a -> b) -> a -> b
$
          ((Int, Procs) -> [(SORT, Profile)])
-> [(Int, Procs)] -> [(SORT, Profile)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (n :: Int
n, Procs p :: Map SORT Profile
p) -> let
            phi :: Morphism (Ranged VSEforms) Procs VSEMorExt
phi = Morphism (Ranged VSEforms) Procs VSEMorExt
-> Int
-> Map Int (Morphism (Ranged VSEforms) Procs VSEMorExt)
-> Morphism (Ranged VSEforms) Procs VSEMorExt
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Morphism (Ranged VSEforms) Procs VSEMorExt
forall a. HasCallStack => String -> a
error "extVSEColimit") Int
n Map Int (Morphism (Ranged VSEforms) Procs VSEMorExt)
morMap
           in ((SORT, Profile) -> (SORT, Profile))
-> [(SORT, Profile)] -> [(SORT, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (idN :: SORT
idN, profile :: Profile
profile) ->
                    (Morphism (Ranged VSEforms) Procs VSEMorExt -> SORT -> SORT
forall f. Morphism f Procs VSEMorExt -> SORT -> SORT
mapProcId Morphism (Ranged VSEforms) Procs VSEMorExt
phi SORT
idN, Sort_map -> Profile -> Profile
mapProfile (Morphism (Ranged VSEforms) Procs VSEMorExt -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism (Ranged VSEforms) Procs VSEMorExt
phi) Profile
profile)) ([(SORT, Profile)] -> [(SORT, Profile)])
-> [(SORT, Profile)] -> [(SORT, Profile)]
forall a b. (a -> b) -> a -> b
$
              Map SORT Profile -> [(SORT, Profile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map SORT Profile
p) ([(Int, Procs)] -> [(SORT, Profile)])
-> [(Int, Procs)] -> [(SORT, Profile)]
forall a b. (a -> b) -> a -> b
$
          Gr Procs (Int, VSEMorExt) -> [(Int, Procs)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr Procs (Int, VSEMorExt)
graph
 in (Map SORT Profile -> Procs
Procs Map SORT Profile
procs, [(Int, VSEMorExt)] -> Map Int VSEMorExt
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, VSEMorExt)] -> Map Int VSEMorExt)
-> [(Int, VSEMorExt)] -> Map Int VSEMorExt
forall a b. (a -> b) -> a -> b
$ (Int -> (Int, VSEMorExt)) -> [Int] -> [(Int, VSEMorExt)]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Int
n -> (Int
n, VSEMorExt
forall e. DefMorExt e
emptyMorExt)) ([Int] -> [(Int, VSEMorExt)]) -> [Int] -> [(Int, VSEMorExt)]
forall a b. (a -> b) -> a -> b
$
                  Gr Procs (Int, VSEMorExt) -> [Int]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Int]
nodes Gr Procs (Int, VSEMorExt)
graph)

vseMorExt :: CASLMor -> (Op_map, Pred_map)
vseMorExt :: CASLMor -> (Op_map, Pred_map)
vseMorExt m :: CASLMor
m = let
  sm :: [(SORT, SORT)]
sm = Sort_map -> [(SORT, SORT)]
forall k a. Map k a -> [(k, a)]
Map.toList (Sort_map -> [(SORT, SORT)]) -> Sort_map -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ CASLMor -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map CASLMor
m
  om :: Op_map
om = CASLMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map CASLMor
m
  pm :: Pred_map
pm = CASLMor -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map CASLMor
m
  eqOps :: Op_map
eqOps = [((SORT, OpType), (SORT, OpKind))] -> Op_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((SORT, OpType), (SORT, OpKind))] -> Op_map)
-> [((SORT, OpType), (SORT, OpKind))] -> Op_map
forall a b. (a -> b) -> a -> b
$ ((SORT, SORT) -> ((SORT, OpType), (SORT, OpKind)))
-> [(SORT, SORT)] -> [((SORT, OpType), (SORT, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, t :: SORT
t) ->
    ((SORT -> SORT
gnEqName SORT
s, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Partial [SORT
s, SORT
s] SORT
uBoolean)
    , (SORT -> SORT
gnEqName SORT
t, OpKind
Partial))) [(SORT, SORT)]
sm
  restrPreds :: Pred_map
restrPreds = [((SORT, PredType), SORT)] -> Pred_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((SORT, PredType), SORT)] -> Pred_map)
-> [((SORT, PredType), SORT)] -> Pred_map
forall a b. (a -> b) -> a -> b
$ ((SORT, SORT) -> ((SORT, PredType), SORT))
-> [(SORT, SORT)] -> [((SORT, PredType), SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, t :: SORT
t) ->
    ((SORT -> SORT
gnRestrName SORT
s, [SORT] -> PredType
PredType [SORT
s]), SORT -> SORT
gnRestrName SORT
t)) [(SORT, SORT)]
sm
  opsProcs :: Op_map
opsProcs = [((SORT, OpType), (SORT, OpKind))] -> Op_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((SORT, OpType), (SORT, OpKind))] -> Op_map)
-> [((SORT, OpType), (SORT, OpKind))] -> Op_map
forall a b. (a -> b) -> a -> b
$ (((SORT, OpType), (SORT, OpKind))
 -> ((SORT, OpType), (SORT, OpKind)))
-> [((SORT, OpType), (SORT, OpKind))]
-> [((SORT, OpType), (SORT, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((idN :: SORT
idN, OpType _ w :: [SORT]
w s :: SORT
s), (idN' :: SORT
idN', _)) ->
    ((SORT -> SORT
mkGenName SORT
idN, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Partial [SORT]
w SORT
s)
    , (SORT -> SORT
mkGenName SORT
idN', OpKind
Partial))) ([((SORT, OpType), (SORT, OpKind))]
 -> [((SORT, OpType), (SORT, OpKind))])
-> [((SORT, OpType), (SORT, OpKind))]
-> [((SORT, OpType), (SORT, OpKind))]
forall a b. (a -> b) -> a -> b
$ Op_map -> [((SORT, OpType), (SORT, OpKind))]
forall k a. Map k a -> [(k, a)]
Map.toList Op_map
om
  predProcs :: Pred_map
predProcs = [((SORT, PredType), SORT)] -> Pred_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((SORT, PredType), SORT)] -> Pred_map)
-> [((SORT, PredType), SORT)] -> Pred_map
forall a b. (a -> b) -> a -> b
$ (((SORT, PredType), SORT) -> ((SORT, PredType), SORT))
-> [((SORT, PredType), SORT)] -> [((SORT, PredType), SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((idN :: SORT
idN, PredType w :: [SORT]
w), idN' :: SORT
idN') ->
    ((SORT -> SORT
mkGenName SORT
idN, [SORT] -> PredType
PredType [SORT]
w), SORT -> SORT
mkGenName SORT
idN')) ([((SORT, PredType), SORT)] -> [((SORT, PredType), SORT)])
-> [((SORT, PredType), SORT)] -> [((SORT, PredType), SORT)]
forall a b. (a -> b) -> a -> b
$ Pred_map -> [((SORT, PredType), SORT)]
forall k a. Map k a -> [(k, a)]
Map.toList Pred_map
pm
  in (Op_map -> Op_map -> Op_map
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Op_map
eqOps Op_map
opsProcs, Pred_map -> Pred_map -> Pred_map
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Pred_map
restrPreds Pred_map
predProcs)