{- |
Module      :  ./CASL/StaticAna.hs
Description :  CASL static analysis for basic specifications
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

CASL static analysis for basic specifications

Follows Chaps. III:2 and III:3 of the CASL Reference Manual.

The static analysis takes an abstract syntax tree of a basic specification
and outputs a signature and a set of formulas, while checking that
- all sorts used in operation and predicate declarations have been declared
- all sorts, operation and predicate symbols used in formulas have
  been declared
- formulas type-check
The formulas are returned with fully-qualified variables, operation
and predicate symbols.

The static analysis functions are parameterized with functions for
treating CASL extensions, that is, additional basic items, signature
items and formulas.
-}

module CASL.StaticAna where

import CASL.AS_Basic_CASL
import CASL.MixfixParser
import CASL.Overload
import CASL.Quantification
import CASL.Sign
import CASL.ToDoc

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.Keywords
import Common.Lib.State
import Common.Result
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import Control.Monad

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

checkPlaces :: [SORT] -> Id -> [Diagnosis]
checkPlaces :: [SORT] -> SORT -> [Diagnosis]
checkPlaces args :: [SORT]
args i :: SORT
i = let n :: Int
n = SORT -> Int
placeCount SORT
i in
    [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "wrong number of places" SORT
i | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
args ]

checkWithVars :: String -> Map.Map SIMPLE_ID a -> Id -> [Diagnosis]
checkWithVars :: String -> Map SIMPLE_ID a -> SORT -> [Diagnosis]
checkWithVars s :: String
s m :: Map SIMPLE_ID a
m i :: SORT
i@(Id ts :: [SIMPLE_ID]
ts _ _) = if SORT -> Bool
isSimpleId SORT
i then
    case SIMPLE_ID -> Map SIMPLE_ID a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ([SIMPLE_ID] -> SIMPLE_ID
forall a. [a] -> a
head [SIMPLE_ID]
ts) Map SIMPLE_ID a
m of
    Nothing -> []
    Just _ -> String -> String -> SORT -> [Diagnosis]
alsoWarning String
s String
varS SORT
i
    else []

addOp :: Annoted a -> OpType -> Id -> State (Sign f e) ()
addOp :: Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp a :: Annoted a
a ty :: OpType
ty i :: SORT
i =
    do [SORT] -> State (Sign f e) ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts (OpType -> SORT
opRes OpType
ty SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: OpType -> [SORT]
opArgs OpType
ty)
       Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get
       let m :: OpMap
m = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
e
           l :: Set OpType
l = SORT -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
i OpMap
m
           ds :: [Diagnosis]
ds = String -> String -> MapSet SORT PredType -> SORT -> [Diagnosis]
forall a. String -> String -> MapSet SORT a -> SORT -> [Diagnosis]
checkWithOtherMap String
opS String
predS (Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign f e
e) SORT
i
                [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String -> Map SIMPLE_ID SORT -> SORT -> [Diagnosis]
forall a. String -> Map SIMPLE_ID a -> SORT -> [Diagnosis]
checkWithVars String
opS (Sign f e -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign f e
e) SORT
i
           check :: State (Sign f e) ()
check = [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$
                   (if OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
ty Set OpType
l then [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "redeclared op" SORT
i]
                    else [SORT] -> SORT -> [Diagnosis]
checkPlaces (OpType -> [SORT]
opArgs OpType
ty) SORT
i [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ SORT -> [Diagnosis]
checkNamePrefix SORT
i)
                   [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
ds
           store :: State (Sign f e) ()
store = Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { opMap :: OpMap
opMap = SORT -> OpType -> OpMap -> OpMap
addOpTo SORT
i OpType
ty OpMap
m }
           pTy :: OpType
pTy = OpType -> OpType
mkPartial OpType
ty
       case OpType -> OpKind
opKind OpType
ty of
          Partial -> if OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (OpType -> OpType
mkTotal OpType
ty) Set OpType
l then
                     [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "partially redeclared" SORT
i Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds
                     else State (Sign f e) ()
store State (Sign f e) () -> State (Sign f e) () -> State (Sign f e) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> State (Sign f e) ()
forall f e. State (Sign f e) ()
check
          Total -> if OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
pTy Set OpType
l then do
                         Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { opMap :: OpMap
opMap = SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
i OpType
ty
                                   (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete SORT
i OpType
pTy OpMap
m }
                         [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "redeclared as total" SORT
i Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds
                   else State (Sign f e) ()
store State (Sign f e) () -> State (Sign f e) () -> State (Sign f e) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> State (Sign f e) ()
forall f e. State (Sign f e) ()
check
       Annoted a -> Symbol -> State (Sign f e) ()
forall a f e. Annoted a -> Symbol -> State (Sign f e) ()
addAnnoSet Annoted a
a (Symbol -> State (Sign f e) ()) -> Symbol -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ SORT -> SymbType -> Symbol
Symbol SORT
i (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> SymbType
OpAsItemType OpType
ty

addAssocOp :: OpType -> Id -> State (Sign f e) ()
addAssocOp :: OpType -> SORT -> State (Sign f e) ()
addAssocOp ty :: OpType
ty i :: SORT
i = do
       Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get
       Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { assocOps :: OpMap
assocOps = SORT -> OpType -> OpMap -> OpMap
addOpTo SORT
i OpType
ty (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
e
             , globAnnos :: GlobalAnnos
globAnnos = (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
updAssocMap (SORT -> AssocMap -> AssocMap
addAssocId SORT
i) (GlobalAnnos -> GlobalAnnos) -> GlobalAnnos -> GlobalAnnos
forall a b. (a -> b) -> a -> b
$ Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
e
             }

updateExtInfo :: (e -> Result e) -> State (Sign f e) ()
updateExtInfo :: (e -> Result e) -> State (Sign f e) ()
updateExtInfo upd :: e -> Result e
upd = do
    Sign f e
s <- State (Sign f e) (Sign f e)
forall s. State s s
get
    let re :: Result e
re = e -> Result e
upd (e -> Result e) -> e -> Result e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
s
    case Result e -> Maybe e
forall a. Result a -> Maybe a
maybeResult Result e
re of
         Nothing -> () -> State (Sign f e) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Just e :: e
e -> Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
s { extendedInfo :: e
extendedInfo = e
e }
    [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ Result e -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags Result e
re

addPred :: Annoted a -> PredType -> Id -> State (Sign f e) ()
addPred :: Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred a :: Annoted a
a ty :: PredType
ty i :: SORT
i =
    do [SORT] -> State (Sign f e) ()
forall f e. [SORT] -> State (Sign f e) ()
checkSorts ([SORT] -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ PredType -> [SORT]
predArgs PredType
ty
       Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get
       let m :: MapSet SORT PredType
m = Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign f e
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
m
           ds :: [Diagnosis]
ds = String -> String -> OpMap -> SORT -> [Diagnosis]
forall a. String -> String -> MapSet SORT a -> SORT -> [Diagnosis]
checkWithOtherMap String
predS String
opS (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
e) SORT
i
                [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String -> Map SIMPLE_ID SORT -> SORT -> [Diagnosis]
forall a. String -> Map SIMPLE_ID a -> SORT -> [Diagnosis]
checkWithVars String
predS (Sign f e -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign f e
e) SORT
i
       if PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PredType
ty Set PredType
l then
          [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "redeclared pred" SORT
i Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds
          else do
            Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { 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 PredType
ty MapSet SORT PredType
m }
            [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> [Diagnosis]
checkPlaces (PredType -> [SORT]
predArgs PredType
ty) SORT
i [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ SORT -> [Diagnosis]
checkNamePrefix SORT
i [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
ds
       Annoted a -> Symbol -> State (Sign f e) ()
forall a f e. Annoted a -> Symbol -> State (Sign f e) ()
addAnnoSet Annoted a
a (Symbol -> State (Sign f e) ()) -> Symbol -> State (Sign f e) ()
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
ty

nonConsts :: OpMap -> Set.Set Id
nonConsts :: OpMap -> Set SORT
nonConsts = OpMap -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (OpMap -> Set SORT) -> (OpMap -> OpMap) -> OpMap -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpType -> Bool) -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> MapSet a b
MapSet.filter (Bool -> Bool
not (Bool -> Bool) -> (OpType -> Bool) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([SORT] -> Bool) -> (OpType -> [SORT]) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> [SORT]
opArgs)

opMapConsts :: OpMap -> Set.Set Id
opMapConsts :: OpMap -> Set SORT
opMapConsts = OpMap -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (OpMap -> Set SORT) -> (OpMap -> OpMap) -> OpMap -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpType -> Bool) -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> MapSet a b
MapSet.filter ([SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([SORT] -> Bool) -> (OpType -> [SORT]) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> [SORT]
opArgs)

allOpIds :: Sign f e -> Set.Set Id
allOpIds :: Sign f e -> Set SORT
allOpIds = OpMap -> Set SORT
nonConsts (OpMap -> Set SORT) -> (Sign f e -> OpMap) -> Sign f e -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap

allConstIds :: Sign f e -> Set.Set Id
allConstIds :: Sign f e -> Set SORT
allConstIds = OpMap -> Set SORT
opMapConsts (OpMap -> Set SORT) -> (Sign f e -> OpMap) -> Sign f e -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap

addAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
addAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
addAssocs e :: Sign f e
e =
  (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
updAssocMap (\ m :: AssocMap
m -> (SORT -> AssocMap -> AssocMap) -> AssocMap -> Set SORT -> AssocMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold SORT -> AssocMap -> AssocMap
addAssocId AssocMap
m (Set SORT -> AssocMap) -> Set SORT -> AssocMap
forall a b. (a -> b) -> a -> b
$ OpMap -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (OpMap -> Set SORT) -> OpMap -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
e)

updAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
updAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
updAssocMap f :: AssocMap -> AssocMap
f ga :: GlobalAnnos
ga = GlobalAnnos
ga { assoc_annos :: AssocMap
assoc_annos = AssocMap -> AssocMap
f (AssocMap -> AssocMap) -> AssocMap -> AssocMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> AssocMap
assoc_annos GlobalAnnos
ga }

addAssocId :: Id -> AssocMap -> AssocMap
addAssocId :: SORT -> AssocMap -> AssocMap
addAssocId i :: SORT
i m :: AssocMap
m = case SORT -> AssocMap -> Maybe AssocEither
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SORT
i AssocMap
m of
                   Nothing -> SORT -> AssocEither -> AssocMap -> AssocMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
i AssocEither
ALeft AssocMap
m
                   _ -> AssocMap
m

formulaIds :: Sign f e -> Set.Set Id
formulaIds :: Sign f e -> Set SORT
formulaIds e :: Sign f e
e = let ops :: Set SORT
ops = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
allOpIds Sign f e
e in
    [SORT] -> Set SORT
forall a. [a] -> Set a
Set.fromDistinctAscList ((SIMPLE_ID -> SORT) -> [SIMPLE_ID] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> SORT
simpleIdToId ([SIMPLE_ID] -> [SORT]) -> [SIMPLE_ID] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Map SIMPLE_ID SORT -> [SIMPLE_ID]
forall k a. Map k a -> [k]
Map.keys (Map SIMPLE_ID SORT -> [SIMPLE_ID])
-> Map SIMPLE_ID SORT -> [SIMPLE_ID]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign f e
e)
               Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set SORT
ops

allPredIds :: Sign f e -> Set.Set Id
allPredIds :: Sign f e -> Set SORT
allPredIds = MapSet SORT PredType -> Set SORT
forall a b. MapSet a b -> Set a
MapSet.keysSet (MapSet SORT PredType -> Set SORT)
-> (Sign f e -> MapSet SORT PredType) -> Sign f e -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap

addSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
addSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ds :: [Named (FORMULA f)]
ds =
    do Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get
       Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { sentences :: [Named (FORMULA f)]
sentences = [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a]
reverse [Named (FORMULA f)]
ds [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ Sign f e -> [Named (FORMULA f)]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences Sign f e
e }

-- * traversing all data types of the abstract syntax

ana_BASIC_SPEC :: (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 -> State (Sign f e) (BASIC_SPEC b s f)
ana_BASIC_SPEC :: 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
-> State (Sign f e) (BASIC_SPEC b s f)
ana_BASIC_SPEC mef :: Min f e
mef ab :: Ana b b s f e
ab anas :: Ana s b s f e
anas mix :: Mix b s f e
mix (Basic_spec al :: [Annoted (BASIC_ITEMS b s f)]
al) = ([Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f)
-> State (Sign f e) [Annoted (BASIC_ITEMS b s f)]
-> State (Sign f e) (BASIC_SPEC b s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec (State (Sign f e) [Annoted (BASIC_ITEMS b s f)]
 -> State (Sign f e) (BASIC_SPEC b s f))
-> State (Sign f e) [Annoted (BASIC_ITEMS b s f)]
-> State (Sign f e) (BASIC_SPEC b s f)
forall a b. (a -> b) -> a -> b
$
      (BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f))
-> [Annoted (BASIC_ITEMS b s f)]
-> State (Sign f e) [Annoted (BASIC_ITEMS b s f)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> BASIC_ITEMS b s f
-> State (Sign f e) (BASIC_ITEMS b s f)
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_ITEMS b s f
-> State (Sign f e) (BASIC_ITEMS b s f)
ana_BASIC_ITEMS Min f e
mef Ana b b s f e
ab Ana s b s f e
anas Mix b s f e
mix) [Annoted (BASIC_ITEMS b s f)]
al

-- looseness of a datatype
data GenKind = Free | Generated | Loose deriving (Int -> GenKind -> ShowS
[GenKind] -> ShowS
GenKind -> String
(Int -> GenKind -> ShowS)
-> (GenKind -> String) -> ([GenKind] -> ShowS) -> Show GenKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenKind] -> ShowS
$cshowList :: [GenKind] -> ShowS
show :: GenKind -> String
$cshow :: GenKind -> String
showsPrec :: Int -> GenKind -> ShowS
$cshowsPrec :: Int -> GenKind -> ShowS
Show, GenKind -> GenKind -> Bool
(GenKind -> GenKind -> Bool)
-> (GenKind -> GenKind -> Bool) -> Eq GenKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GenKind -> GenKind -> Bool
$c/= :: GenKind -> GenKind -> Bool
== :: GenKind -> GenKind -> Bool
$c== :: GenKind -> GenKind -> Bool
Eq, Eq GenKind
Eq GenKind =>
(GenKind -> GenKind -> Ordering)
-> (GenKind -> GenKind -> Bool)
-> (GenKind -> GenKind -> Bool)
-> (GenKind -> GenKind -> Bool)
-> (GenKind -> GenKind -> Bool)
-> (GenKind -> GenKind -> GenKind)
-> (GenKind -> GenKind -> GenKind)
-> Ord GenKind
GenKind -> GenKind -> Bool
GenKind -> GenKind -> Ordering
GenKind -> GenKind -> GenKind
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GenKind -> GenKind -> GenKind
$cmin :: GenKind -> GenKind -> GenKind
max :: GenKind -> GenKind -> GenKind
$cmax :: GenKind -> GenKind -> GenKind
>= :: GenKind -> GenKind -> Bool
$c>= :: GenKind -> GenKind -> Bool
> :: GenKind -> GenKind -> Bool
$c> :: GenKind -> GenKind -> Bool
<= :: GenKind -> GenKind -> Bool
$c<= :: GenKind -> GenKind -> Bool
< :: GenKind -> GenKind -> Bool
$c< :: GenKind -> GenKind -> Bool
compare :: GenKind -> GenKind -> Ordering
$ccompare :: GenKind -> GenKind -> Ordering
$cp1Ord :: Eq GenKind
Ord)

unionGenAx :: [GenAx] -> GenAx
unionGenAx :: [GenAx] -> GenAx
unionGenAx = (GenAx -> GenAx -> GenAx) -> GenAx -> [GenAx] -> GenAx
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (s1 :: Set SORT
s1, r1 :: Rel SORT
r1, f1 :: Set Component
f1) (s2 :: Set SORT
s2, r2 :: Rel SORT
r2, f2 :: Set Component
f2) ->
                        (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set SORT
s1 Set SORT
s2,
                         Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Rel SORT
r1 Rel SORT
r2,
                         Set Component -> Set Component -> Set Component
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Component
f1 Set Component
f2)) GenAx
emptyGenAx

anaVarForms :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range
  -> State (Sign f e) [Annoted (FORMULA f)]
anaVarForms :: Min f e
-> Mix b s f e
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) [Annoted (FORMULA f)]
anaVarForms mef :: Min f e
mef mix :: Mix b s f e
mix vs :: [VAR_DECL]
vs fs :: [Annoted (FORMULA f)]
fs r :: Range
r = do
   (resFs :: [Annoted (FORMULA f)]
resFs, fufs :: [Annoted (FORMULA f)]
fufs) <- (Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
forall f e.
TermExtension f =>
(Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
anaLocalVarForms (Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm Min f e
mef Mix b s f e
mix) [VAR_DECL]
vs [Annoted (FORMULA f)]
fs Range
r
   [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (Annoted (FORMULA f) -> Named (FORMULA f))
-> [Annoted (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map Annoted (FORMULA f) -> Named (FORMULA f)
forall a. Annoted a -> Named a
makeNamedSen [Annoted (FORMULA f)]
fufs
   [Annoted (FORMULA f)] -> State (Sign f e) [Annoted (FORMULA f)]
forall (m :: * -> *) a. Monad m => a -> m a
return [Annoted (FORMULA f)]
resFs

anaLocalVarForms :: TermExtension f
  => (Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
  -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range
  -> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
anaLocalVarForms :: (Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
anaLocalVarForms anaFrm :: Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f)
anaFrm il :: [VAR_DECL]
il afs :: [Annoted (FORMULA f)]
afs ps :: Range
ps = do
           Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get -- save
           (VAR_DECL -> State (Sign f e) ())
-> [VAR_DECL] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
il
           [Diagnosis]
vds <- (Sign f e -> [Diagnosis]) -> State (Sign f e) [Diagnosis]
forall s a. (s -> a) -> State s a
gets Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags
           Sign f e
sign <- State (Sign f e) (Sign f e)
forall s. State s s
get
           Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
il) (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { envDiags :: [Diagnosis]
envDiags = [Diagnosis]
vds }
           -- restore with shadowing warnings
           let (es :: [Diagnosis]
es, resFs :: [Annoted (FORMULA f)]
resFs, anaFs :: [Annoted (FORMULA f)]
anaFs) = (Annoted (FORMULA f)
 -> ([Diagnosis], [Annoted (FORMULA f)], [Annoted (FORMULA f)])
 -> ([Diagnosis], [Annoted (FORMULA f)], [Annoted (FORMULA f)]))
-> ([Diagnosis], [Annoted (FORMULA f)], [Annoted (FORMULA f)])
-> [Annoted (FORMULA f)]
-> ([Diagnosis], [Annoted (FORMULA f)], [Annoted (FORMULA f)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: Annoted (FORMULA f)
f (dss :: [Diagnosis]
dss, ress :: [Annoted (FORMULA f)]
ress, ranas :: [Annoted (FORMULA f)]
ranas) ->
                      let Result ds :: [Diagnosis]
ds m :: Maybe (FORMULA f, FORMULA f)
m = Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f)
anaFrm Sign f e
sign (FORMULA f -> Result (FORMULA f, FORMULA f))
-> FORMULA f -> Result (FORMULA f, FORMULA f)
forall a b. (a -> b) -> a -> b
$ Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item Annoted (FORMULA f)
f
                      in case Maybe (FORMULA f, FORMULA f)
m of
                         Nothing -> ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
dss, [Annoted (FORMULA f)]
ress, [Annoted (FORMULA f)]
ranas)
                         Just (resF :: FORMULA f
resF, anaF :: FORMULA f
anaF) ->
                             ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
dss, Annoted (FORMULA f)
f {item :: FORMULA f
item = FORMULA f
resF} Annoted (FORMULA f)
-> [Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a. a -> [a] -> [a]
: [Annoted (FORMULA f)]
ress,
                                 Annoted (FORMULA f)
f {item :: FORMULA f
item = FORMULA f
anaF} Annoted (FORMULA f)
-> [Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a. a -> [a] -> [a]
: [Annoted (FORMULA f)]
ranas))
                     ([], [], []) [Annoted (FORMULA f)]
afs
               fufs :: [Annoted (FORMULA f)]
fufs = (Annoted (FORMULA f) -> Annoted (FORMULA f))
-> [Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> FORMULA f)
-> Annoted (FORMULA f) -> Annoted (FORMULA f)
forall a b. (a -> b) -> Annoted a -> Annoted b
mapAn (\ f :: FORMULA f
f -> Sign f e -> FORMULA f -> Range -> FORMULA f
forall f e.
TermExtension f =>
Sign f e -> FORMULA f -> Range -> FORMULA f
quantFreeVars Sign f e
sign
                            ([VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
il FORMULA f
f Range
ps) Range
ps))
                      [Annoted (FORMULA f)]
anaFs
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
es
           ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
-> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted (FORMULA f)]
resFs, [Annoted (FORMULA f)]
fufs)

anaDatatypeDecls :: GenKind -> SortsKind -> [Annoted DATATYPE_DECL]
  -> State (Sign f e) ()
anaDatatypeDecls :: GenKind
-> SortsKind -> [Annoted DATATYPE_DECL] -> State (Sign f e) ()
anaDatatypeDecls gk :: GenKind
gk sk :: SortsKind
sk al :: [Annoted DATATYPE_DECL]
al = do
           let ts :: [(Annoted DATATYPE_DECL, SORT)]
ts = (Annoted DATATYPE_DECL -> (Annoted DATATYPE_DECL, SORT))
-> [Annoted DATATYPE_DECL] -> [(Annoted DATATYPE_DECL, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Annoted DATATYPE_DECL
i -> case Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item Annoted DATATYPE_DECL
i of
                        Datatype_decl s :: SORT
s _ _ -> (Annoted DATATYPE_DECL
i, SORT
s)) [Annoted DATATYPE_DECL]
al
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> ([SORT] -> [Diagnosis]) -> [SORT] -> State (Sign f e) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SORT] -> Diagnosis) -> [[SORT]] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: [SORT]
l -> case [SORT]
l of
              _ : t :: SORT
t : _ -> DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag (if GenKind
gk GenKind -> GenKind -> Bool
forall a. Eq a => a -> a -> Bool
== GenKind
Loose then DiagKind
Warning else DiagKind
Error)
               "duplicate type name in mutually recursive type definition" SORT
t
              _ -> String -> Diagnosis
forall a. HasCallStack => String -> a
error "anaDatatypeDecls")
               ([[SORT]] -> [Diagnosis])
-> ([SORT] -> [[SORT]]) -> [SORT] -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SORT] -> Bool) -> [[SORT]] -> [[SORT]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (Int -> Bool) -> ([SORT] -> Int) -> [SORT] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([[SORT]] -> [[SORT]])
-> ([SORT] -> [[SORT]]) -> [SORT] -> [[SORT]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> [[SORT]]
forall a. Eq a => [a] -> [[a]]
group ([SORT] -> [[SORT]]) -> ([SORT] -> [SORT]) -> [SORT] -> [[SORT]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> [SORT]
forall a. Ord a => [a] -> [a]
sort ([SORT] -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ ((Annoted DATATYPE_DECL, SORT) -> SORT)
-> [(Annoted DATATYPE_DECL, SORT)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (Annoted DATATYPE_DECL, SORT) -> SORT
forall a b. (a, b) -> b
snd [(Annoted DATATYPE_DECL, SORT)]
ts
           ((Annoted DATATYPE_DECL, SORT) -> State (Sign f e) ())
-> [(Annoted DATATYPE_DECL, SORT)] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Annoted DATATYPE_DECL -> SORT -> State (Sign f e) ())
-> (Annoted DATATYPE_DECL, SORT) -> State (Sign f e) ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Annoted DATATYPE_DECL -> SORT -> State (Sign f e) ())
 -> (Annoted DATATYPE_DECL, SORT) -> State (Sign f e) ())
-> (Annoted DATATYPE_DECL -> SORT -> State (Sign f e) ())
-> (Annoted DATATYPE_DECL, SORT)
-> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ SortsKind -> Annoted DATATYPE_DECL -> SORT -> State (Sign f e) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
sk) [(Annoted DATATYPE_DECL, SORT)]
ts
           (DATATYPE_DECL -> State (Sign f e) [Component])
-> [Annoted DATATYPE_DECL]
-> State (Sign f e) [Annoted [Component]]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
forall f e.
GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
ana_DATATYPE_DECL GenKind
gk) [Annoted DATATYPE_DECL]
al
           State (Sign f e) ()
forall f e. State (Sign f e) ()
closeSubsortRel

ana_BASIC_ITEMS :: (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_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
ana_BASIC_ITEMS :: Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> BASIC_ITEMS b s f
-> State (Sign f e) (BASIC_ITEMS b s f)
ana_BASIC_ITEMS mef :: Min f e
mef ab :: Ana b b s f e
ab anas :: Ana s b s f e
anas mix :: Mix b s f e
mix bi :: BASIC_ITEMS b s f
bi =
    case BASIC_ITEMS b s f
bi of
    Sig_items sis :: SIG_ITEMS s f
sis -> (SIG_ITEMS s f -> BASIC_ITEMS b s f)
-> State (Sign f e) (SIG_ITEMS s f)
-> State (Sign f e) (BASIC_ITEMS b s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (State (Sign f e) (SIG_ITEMS s f)
 -> State (Sign f e) (BASIC_ITEMS b s f))
-> State (Sign f e) (SIG_ITEMS s f)
-> State (Sign f e) (BASIC_ITEMS b s f)
forall a b. (a -> b) -> a -> b
$
                     Min f e
-> Ana s b s f e
-> Mix b s f e
-> GenKind
-> SIG_ITEMS s f
-> State (Sign f e) (SIG_ITEMS s f)
forall f e s b.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana s b s f e
-> Mix b s f e
-> GenKind
-> SIG_ITEMS s f
-> State (Sign f e) (SIG_ITEMS s f)
ana_SIG_ITEMS Min f e
mef Ana s b s f e
anas Mix b s f e
mix GenKind
Loose SIG_ITEMS s f
sis
    Free_datatype sk :: SortsKind
sk al :: [Annoted DATATYPE_DECL]
al ps :: Range
ps -> do
           GenKind
-> SortsKind -> [Annoted DATATYPE_DECL] -> State (Sign f e) ()
forall f e.
GenKind
-> SortsKind -> [Annoted DATATYPE_DECL] -> State (Sign f e) ()
anaDatatypeDecls GenKind
Free SortsKind
sk [Annoted DATATYPE_DECL]
al
           Range -> Bool -> GenAx -> State (Sign f e) ()
forall f e. Range -> Bool -> GenAx -> State (Sign f e) ()
toSortGenAx Range
ps Bool
True (GenAx -> State (Sign f e) ()) -> GenAx -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig [Annoted DATATYPE_DECL]
al
           BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return BASIC_ITEMS b s f
bi
    Sort_gen al :: [Annoted (SIG_ITEMS s f)]
al ps :: Range
ps -> do
           (gs :: [GenAx]
gs, ul :: [Annoted (SIG_ITEMS s f)]
ul) <- Min f e
-> Ana s b s f e
-> Mix b s f e
-> [Annoted (SIG_ITEMS s f)]
-> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
forall f e s b.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana s b s f e
-> Mix b s f e
-> [Annoted (SIG_ITEMS s f)]
-> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
ana_Generated Min f e
mef Ana s b s f e
anas Mix b s f e
mix [Annoted (SIG_ITEMS s f)]
al
           Range -> Bool -> GenAx -> State (Sign f e) ()
forall f e. Range -> Bool -> GenAx -> State (Sign f e) ()
toSortGenAx Range
ps Bool
False (GenAx -> State (Sign f e) ()) -> GenAx -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [GenAx] -> GenAx
unionGenAx [GenAx]
gs
           BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f))
-> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall a b. (a -> b) -> a -> b
$ [Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[Annoted (SIG_ITEMS s f)] -> Range -> BASIC_ITEMS b s f
Sort_gen [Annoted (SIG_ITEMS s f)]
ul Range
ps
    Var_items il :: [VAR_DECL]
il _ -> do
           (VAR_DECL -> State (Sign f e) ())
-> [VAR_DECL] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
il
           BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return BASIC_ITEMS b s f
bi
    Local_var_axioms il :: [VAR_DECL]
il afs :: [Annoted (FORMULA f)]
afs ps :: Range
ps -> do
        [Annoted (FORMULA f)]
resFs <- Min f e
-> Mix b s f e
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) [Annoted (FORMULA f)]
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) [Annoted (FORMULA f)]
anaVarForms Min f e
mef Mix b s f e
mix [VAR_DECL]
il [Annoted (FORMULA f)]
afs Range
ps
        BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f))
-> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f.
[VAR_DECL] -> [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Local_var_axioms [VAR_DECL]
il [Annoted (FORMULA f)]
resFs Range
ps
    Axiom_items afs :: [Annoted (FORMULA f)]
afs ps :: Range
ps -> do
        [Annoted (FORMULA f)]
resFs <- Min f e
-> Mix b s f e
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) [Annoted (FORMULA f)]
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> [VAR_DECL]
-> [Annoted (FORMULA f)]
-> Range
-> State (Sign f e) [Annoted (FORMULA f)]
anaVarForms Min f e
mef Mix b s f e
mix [] [Annoted (FORMULA f)]
afs Range
ps
        BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f))
-> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
forall a b. (a -> b) -> a -> b
$ [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
forall b s f. [Annoted (FORMULA f)] -> Range -> BASIC_ITEMS b s f
Axiom_items [Annoted (FORMULA f)]
resFs Range
ps
    Ext_BASIC_ITEMS b :: b
b -> (b -> BASIC_ITEMS b s f)
-> State (Sign f e) b -> State (Sign f e) (BASIC_ITEMS b s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> BASIC_ITEMS b s f
forall b s f. b -> BASIC_ITEMS b s f
Ext_BASIC_ITEMS (State (Sign f e) b -> State (Sign f e) (BASIC_ITEMS b s f))
-> State (Sign f e) b -> State (Sign f e) (BASIC_ITEMS b s f)
forall a b. (a -> b) -> a -> b
$ Ana b b s f e
ab Mix b s f e
mix b
b

mapAn :: (a -> b) -> Annoted a -> Annoted b
mapAn :: (a -> b) -> Annoted a -> Annoted b
mapAn f :: a -> b
f an :: Annoted a
an = b -> Annoted a -> Annoted b
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted (a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ Annoted a -> a
forall a. Annoted a -> a
item Annoted a
an) Annoted a
an

type GenAx = (Set.Set SORT, Rel.Rel SORT, Set.Set Component)

emptyGenAx :: GenAx
emptyGenAx :: GenAx
emptyGenAx = (Set SORT
forall a. Set a
Set.empty, Rel SORT
forall a. Rel a
Rel.empty, Set Component
forall a. Set a
Set.empty)

toSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()
toSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()
toSortGenAx ps :: Range
ps isFree :: Bool
isFree (sorts :: Set SORT
sorts, rel :: Rel SORT
rel, ops :: Set Component
ops) = do
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
sorts
        opSyms :: [OP_SYMB]
opSyms = (Component -> OP_SYMB) -> [Component] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Component
c -> let ide :: SORT
ide = Component -> SORT
compId Component
c in SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
ide
                      (OpType -> OP_TYPE
toOP_TYPE (OpType -> OP_TYPE) -> OpType -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ Component -> OpType
compType Component
c) (Range -> OP_SYMB) -> Range -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ SORT -> Range
posOfId SORT
ide) ([Component] -> [OP_SYMB]) -> [Component] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ Set Component -> [Component]
forall a. Set a -> [a]
Set.toList Set Component
ops
        injSyms :: [OP_SYMB]
injSyms = ((SORT, SORT) -> OP_SYMB) -> [(SORT, SORT)] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, t :: SORT
t) -> let p :: Range
p = SORT -> Range
posOfId SORT
s in
                        SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (SORT -> SORT -> SORT
mkUniqueInjName SORT
s SORT
t)
                        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT
s] SORT
t Range
p) Range
p) ([(SORT, SORT)] -> [OP_SYMB]) -> [(SORT, SORT)] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList
                  (Rel SORT -> [(SORT, SORT)]) -> Rel SORT -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex Rel SORT
rel
        allSyms :: [OP_SYMB]
allSyms = [OP_SYMB]
opSyms [OP_SYMB] -> [OP_SYMB] -> [OP_SYMB]
forall a. [a] -> [a] -> [a]
++ [OP_SYMB]
injSyms
        resType :: OP_SYMB -> SORT
resType (Op_name _) = String -> SORT
forall a. HasCallStack => String -> a
error "CASL.StaticAna.resType"
        resType (Qual_op_name _ t :: OP_TYPE
t _) = OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
t
        argTypes :: OP_SYMB -> [SORT]
argTypes (Op_name _) = String -> [SORT]
forall a. HasCallStack => String -> a
error "CASL.StaticAna.argTypes"
        argTypes (Qual_op_name _ t :: OP_TYPE
t _) = OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
t
        getIndex :: [a] -> a -> Int
getIndex l :: [a]
l s :: a
s = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (-1) (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ a -> [a] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex a
s [a]
l
        addIndices :: [SORT] -> OP_SYMB -> (OP_SYMB, [Int])
addIndices l :: [SORT]
l os :: OP_SYMB
os =
            (OP_SYMB
os, (SORT -> Int) -> [SORT] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([SORT] -> SORT -> Int
forall a. Eq a => [a] -> a -> Int
getIndex [SORT]
l) ([SORT] -> [Int]) -> [SORT] -> [Int]
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [SORT]
argTypes OP_SYMB
os)
        collectOps :: SORT -> (SORT, [OP_SYMB])
collectOps s :: SORT
s = (SORT
s, (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s) (SORT -> Bool) -> (OP_SYMB -> SORT) -> OP_SYMB -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> SORT
resType) [OP_SYMB]
allSyms)
        constrs0 :: [(SORT, [OP_SYMB])]
constrs0 = (SORT -> (SORT, [OP_SYMB])) -> [SORT] -> [(SORT, [OP_SYMB])]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> (SORT, [OP_SYMB])
collectOps [SORT]
sortList
        dRel :: [Set SORT]
dRel = Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.depSort (Rel SORT -> [Set SORT])
-> (Rel SORT -> Rel SORT) -> Rel SORT -> [Set SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> [Set SORT]) -> Rel SORT -> [Set SORT]
forall a b. (a -> b) -> a -> b
$ ((SORT, [OP_SYMB]) -> Rel SORT -> Rel SORT)
-> Rel SORT -> [(SORT, [OP_SYMB])] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (s :: SORT
s, os :: [OP_SYMB]
os) r :: Rel SORT
r ->
               (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> Set SORT -> Rel SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
`Rel.insertDiffPair` SORT
s) (SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
s Rel SORT
r)
               (Set SORT -> Rel SORT) -> Set SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
               ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> Set SORT) -> [OP_SYMB] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set SORT
sorts (Set SORT -> Set SORT)
-> (OP_SYMB -> Set SORT) -> OP_SYMB -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ([SORT] -> Set SORT) -> (OP_SYMB -> [SORT]) -> OP_SYMB -> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> [SORT]
argTypes) [OP_SYMB]
os)
               Rel SORT
forall a. Rel a
Rel.empty [(SORT, [OP_SYMB])]
constrs0
        m2 :: Map SORT [OP_SYMB]
m2 = [(SORT, [OP_SYMB])] -> Map SORT [OP_SYMB]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(SORT, [OP_SYMB])]
constrs0
        mkConstr :: Set SORT -> Named (FORMULA f)
mkConstr ss :: Set SORT
ss =
            let sl :: [SORT]
sl = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
ss in
            FORMULA f -> [SORT] -> Named (FORMULA f)
forall f. FORMULA f -> [SORT] -> Named (FORMULA f)
toSortGenNamed
            ([Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax
            ((SORT -> Constraint) -> [SORT] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: SORT
s -> SORT -> [(OP_SYMB, [Int])] -> SORT -> Constraint
Constraint SORT
s
                   ((OP_SYMB -> (OP_SYMB, [Int])) -> [OP_SYMB] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map ([SORT] -> OP_SYMB -> (OP_SYMB, [Int])
addIndices [SORT]
sl)
                    ([OP_SYMB] -> [(OP_SYMB, [Int])])
-> [OP_SYMB] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> a -> b
$ [OP_SYMB] -> SORT -> Map SORT [OP_SYMB] -> [OP_SYMB]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> [OP_SYMB]
forall a. HasCallStack => String -> a
error "CASL.StaticAna.mkConstr")
                    SORT
s Map SORT [OP_SYMB]
m2) SORT
s) [SORT]
sl) Bool
isFree) [SORT]
sl
        resList :: Set SORT
resList = [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ([SORT] -> Set SORT) -> [SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> SORT) -> [OP_SYMB] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> SORT
resType [OP_SYMB]
allSyms
        noConsList :: Set SORT
noConsList = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
sorts Set SORT
resList
        voidOps :: Set SORT
voidOps = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
resList Set SORT
sorts
        sens :: [Named (FORMULA f)]
sens = (Set SORT -> Named (FORMULA f))
-> [Set SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map Set SORT -> Named (FORMULA f)
forall f. Set SORT -> Named (FORMULA f)
mkConstr [Set SORT]
dRel
    Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
sortList)
      (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error "missing generated sort" Range
ps]
    Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
noConsList)
      (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> Set SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "generated sorts without constructor"
          Set SORT
noConsList]
    Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
voidOps)
      (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> Set SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "non-generated sorts as constructor result"
                  Set SORT
voidOps]
    Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Set SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Set SORT]
dRel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1)
      (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [DiagKind -> String -> [Set SORT] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "splittable groups of generated sorts" [Set SORT]
dRel]
    [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences [Named (FORMULA f)]
forall f. [Named (FORMULA f)]
sens

ana_SIG_ITEMS :: (FormExtension f, TermExtension f)
  => Min f e -> Ana s b s f e -> Mix b s f e -> GenKind -> SIG_ITEMS s f
    -> State (Sign f e) (SIG_ITEMS s f)
ana_SIG_ITEMS :: Min f e
-> Ana s b s f e
-> Mix b s f e
-> GenKind
-> SIG_ITEMS s f
-> State (Sign f e) (SIG_ITEMS s f)
ana_SIG_ITEMS mef :: Min f e
mef anas :: Ana s b s f e
anas mix :: Mix b s f e
mix gk :: GenKind
gk si :: SIG_ITEMS s f
si =
    case SIG_ITEMS s f
si of
    Sort_items sk :: SortsKind
sk al :: [Annoted (SORT_ITEM f)]
al ps :: Range
ps ->
        do [Annoted (SORT_ITEM f)]
ul <- (Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f)))
-> [Annoted (SORT_ITEM f)]
-> State (Sign f e) [Annoted (SORT_ITEM f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min f e
-> Mix b s f e
-> SortsKind
-> Annoted (SORT_ITEM f)
-> State (Sign f e) (Annoted (SORT_ITEM f))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> SortsKind
-> Annoted (SORT_ITEM f)
-> State (Sign f e) (Annoted (SORT_ITEM f))
ana_SORT_ITEM Min f e
mef Mix b s f e
mix SortsKind
sk) [Annoted (SORT_ITEM f)]
al
           State (Sign f e) ()
forall f e. State (Sign f e) ()
closeSubsortRel
           SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f))
-> SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall a b. (a -> b) -> a -> b
$ SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
sk [Annoted (SORT_ITEM f)]
ul Range
ps
    Op_items al :: [Annoted (OP_ITEM f)]
al ps :: Range
ps ->
        do [Annoted (OP_ITEM f)]
ul <- (Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f)))
-> [Annoted (OP_ITEM f)] -> State (Sign f e) [Annoted (OP_ITEM f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min f e
-> Mix b s f e
-> Annoted (OP_ITEM f)
-> State (Sign f e) (Annoted (OP_ITEM f))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Annoted (OP_ITEM f)
-> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM Min f e
mef Mix b s f e
mix) [Annoted (OP_ITEM f)]
al
           SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f))
-> SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall a b. (a -> b) -> a -> b
$ [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (OP_ITEM f)] -> Range -> SIG_ITEMS s f
Op_items [Annoted (OP_ITEM f)]
ul Range
ps
    Pred_items al :: [Annoted (PRED_ITEM f)]
al ps :: Range
ps ->
        do [Annoted (PRED_ITEM f)]
ul <- (Annoted (PRED_ITEM f) -> State (Sign f e) (Annoted (PRED_ITEM f)))
-> [Annoted (PRED_ITEM f)]
-> State (Sign f e) [Annoted (PRED_ITEM f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min f e
-> Mix b s f e
-> Annoted (PRED_ITEM f)
-> State (Sign f e) (Annoted (PRED_ITEM f))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Annoted (PRED_ITEM f)
-> State (Sign f e) (Annoted (PRED_ITEM f))
ana_PRED_ITEM Min f e
mef Mix b s f e
mix) [Annoted (PRED_ITEM f)]
al
           SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall (m :: * -> *) a. Monad m => a -> m a
return (SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f))
-> SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall a b. (a -> b) -> a -> b
$ [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f. [Annoted (PRED_ITEM f)] -> Range -> SIG_ITEMS s f
Pred_items [Annoted (PRED_ITEM f)]
ul Range
ps
    Datatype_items sk :: SortsKind
sk al :: [Annoted DATATYPE_DECL]
al _ ->
        do GenKind
-> SortsKind -> [Annoted DATATYPE_DECL] -> State (Sign f e) ()
forall f e.
GenKind
-> SortsKind -> [Annoted DATATYPE_DECL] -> State (Sign f e) ()
anaDatatypeDecls GenKind
gk SortsKind
sk [Annoted DATATYPE_DECL]
al
           SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)
forall (m :: * -> *) a. Monad m => a -> m a
return SIG_ITEMS s f
si
    Ext_SIG_ITEMS s :: s
s -> (s -> SIG_ITEMS s f)
-> State (Sign f e) s -> State (Sign f e) (SIG_ITEMS s f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> SIG_ITEMS s f
forall s f. s -> SIG_ITEMS s f
Ext_SIG_ITEMS (State (Sign f e) s -> State (Sign f e) (SIG_ITEMS s f))
-> State (Sign f e) s -> State (Sign f e) (SIG_ITEMS s f)
forall a b. (a -> b) -> a -> b
$ Ana s b s f e
anas Mix b s f e
mix s
s

-- helper
ana_Generated :: (FormExtension f, TermExtension f)
  => Min f e -> Ana s b s f e -> Mix b s f e -> [Annoted (SIG_ITEMS s f)]
    -> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
ana_Generated :: Min f e
-> Ana s b s f e
-> Mix b s f e
-> [Annoted (SIG_ITEMS s f)]
-> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
ana_Generated mef :: Min f e
mef anas :: Ana s b s f e
anas mix :: Mix b s f e
mix al :: [Annoted (SIG_ITEMS s f)]
al = do
   [Annoted (SIG_ITEMS s f)]
ul <- (SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f))
-> [Annoted (SIG_ITEMS s f)]
-> State (Sign f e) [Annoted (SIG_ITEMS s f)]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Min f e
-> Ana s b s f e
-> Mix b s f e
-> GenKind
-> SIG_ITEMS s f
-> State (Sign f e) (SIG_ITEMS s f)
forall f e s b.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana s b s f e
-> Mix b s f e
-> GenKind
-> SIG_ITEMS s f
-> State (Sign f e) (SIG_ITEMS s f)
ana_SIG_ITEMS Min f e
mef Ana s b s f e
anas Mix b s f e
mix GenKind
Generated) [Annoted (SIG_ITEMS s f)]
al
   ([GenAx], [Annoted (SIG_ITEMS s f)])
-> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Annoted (SIG_ITEMS s f) -> GenAx)
-> [Annoted (SIG_ITEMS s f)] -> [GenAx]
forall a b. (a -> b) -> [a] -> [b]
map (SIG_ITEMS s f -> GenAx
forall s f. SIG_ITEMS s f -> GenAx
getGenSig (SIG_ITEMS s f -> GenAx)
-> (Annoted (SIG_ITEMS s f) -> SIG_ITEMS s f)
-> Annoted (SIG_ITEMS s f)
-> GenAx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SIG_ITEMS s f) -> SIG_ITEMS s f
forall a. Annoted a -> a
item) [Annoted (SIG_ITEMS s f)]
ul, [Annoted (SIG_ITEMS s f)]
ul)

getGenSig :: SIG_ITEMS s f -> GenAx
getGenSig :: SIG_ITEMS s f -> GenAx
getGenSig si :: SIG_ITEMS s f
si = case SIG_ITEMS s f
si of
      Sort_items _ al :: [Annoted (SORT_ITEM f)]
al _ -> [GenAx] -> GenAx
unionGenAx ([GenAx] -> GenAx) -> [GenAx] -> GenAx
forall a b. (a -> b) -> a -> b
$ (Annoted (SORT_ITEM f) -> GenAx)
-> [Annoted (SORT_ITEM f)] -> [GenAx]
forall a b. (a -> b) -> [a] -> [b]
map (SORT_ITEM f -> GenAx
forall f. SORT_ITEM f -> GenAx
getGenSorts (SORT_ITEM f -> GenAx)
-> (Annoted (SORT_ITEM f) -> SORT_ITEM f)
-> Annoted (SORT_ITEM f)
-> GenAx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SORT_ITEM f) -> SORT_ITEM f
forall a. Annoted a -> a
item) [Annoted (SORT_ITEM f)]
al
      Op_items al :: [Annoted (OP_ITEM f)]
al _ -> (Set SORT
forall a. Set a
Set.empty, Rel SORT
forall a. Rel a
Rel.empty,
                           [Set Component] -> Set Component
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ((Annoted (OP_ITEM f) -> Set Component)
-> [Annoted (OP_ITEM f)] -> [Set Component]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ITEM f -> Set Component
forall f. OP_ITEM f -> Set Component
getOps (OP_ITEM f -> Set Component)
-> (Annoted (OP_ITEM f) -> OP_ITEM f)
-> Annoted (OP_ITEM f)
-> Set Component
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM f) -> OP_ITEM f
forall a. Annoted a -> a
item) [Annoted (OP_ITEM f)]
al))
      Datatype_items _ dl :: [Annoted DATATYPE_DECL]
dl _ -> [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig [Annoted DATATYPE_DECL]
dl
      _ -> GenAx
emptyGenAx

isConsAlt :: ALTERNATIVE -> Bool
isConsAlt :: ALTERNATIVE -> Bool
isConsAlt a :: ALTERNATIVE
a = case ALTERNATIVE
a of
  Subsorts _ _ -> Bool
False
  _ -> Bool
True

getDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig dl :: [Annoted DATATYPE_DECL]
dl =
    let alts :: [(SORT, ALTERNATIVE)]
alts = (Annoted DATATYPE_DECL -> [(SORT, ALTERNATIVE)])
-> [Annoted DATATYPE_DECL] -> [(SORT, ALTERNATIVE)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((\ (Datatype_decl s :: SORT
s al :: [Annoted ALTERNATIVE]
al _) ->
                          (Annoted ALTERNATIVE -> (SORT, ALTERNATIVE))
-> [Annoted ALTERNATIVE] -> [(SORT, ALTERNATIVE)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: Annoted ALTERNATIVE
a -> (SORT
s, Annoted ALTERNATIVE -> ALTERNATIVE
forall a. Annoted a -> a
item Annoted ALTERNATIVE
a)) [Annoted ALTERNATIVE]
al) (DATATYPE_DECL -> [(SORT, ALTERNATIVE)])
-> (Annoted DATATYPE_DECL -> DATATYPE_DECL)
-> Annoted DATATYPE_DECL
-> [(SORT, ALTERNATIVE)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted DATATYPE_DECL]
dl
        sorts :: [SORT]
sorts = ((SORT, ALTERNATIVE) -> SORT) -> [(SORT, ALTERNATIVE)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, ALTERNATIVE) -> SORT
forall a b. (a, b) -> a
fst [(SORT, ALTERNATIVE)]
alts
        (realAlts :: [(SORT, ALTERNATIVE)]
realAlts, subs :: [(SORT, ALTERNATIVE)]
subs) = ((SORT, ALTERNATIVE) -> Bool)
-> [(SORT, ALTERNATIVE)]
-> ([(SORT, ALTERNATIVE)], [(SORT, ALTERNATIVE)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (ALTERNATIVE -> Bool
isConsAlt (ALTERNATIVE -> Bool)
-> ((SORT, ALTERNATIVE) -> ALTERNATIVE)
-> (SORT, ALTERNATIVE)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, ALTERNATIVE) -> ALTERNATIVE
forall a b. (a, b) -> b
snd) [(SORT, ALTERNATIVE)]
alts
        cs :: [Component]
cs = ((SORT, ALTERNATIVE) -> Component)
-> [(SORT, ALTERNATIVE)] -> [Component]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, a :: ALTERNATIVE
a) ->
               let (i :: SORT
i, ty :: OpType
ty, _) = SORT -> ALTERNATIVE -> (SORT, OpType, [COMPONENTS])
getConsType SORT
s ALTERNATIVE
a
               in SORT -> OpType -> Component
Component SORT
i OpType
ty) [(SORT, ALTERNATIVE)]
realAlts
        rel :: Rel SORT
rel = ((SORT, ALTERNATIVE) -> Rel SORT -> Rel SORT)
-> Rel SORT -> [(SORT, ALTERNATIVE)] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (t :: SORT
t, a :: ALTERNATIVE
a) r :: Rel SORT
r ->
                  (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> [SORT] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
`Rel.insertDiffPair` SORT
t)
                  Rel SORT
r ([SORT] -> Rel SORT) -> [SORT] -> Rel SORT
forall a b. (a -> b) -> a -> b
$ ALTERNATIVE -> [SORT]
getAltSubsorts ALTERNATIVE
a)
               Rel SORT
forall a. Rel a
Rel.empty [(SORT, ALTERNATIVE)]
subs
        in ([SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [SORT]
sorts, Rel SORT
rel, [Component] -> Set Component
forall a. Ord a => [a] -> Set a
Set.fromList [Component]
cs)

getGenSorts :: SORT_ITEM f -> GenAx
getGenSorts :: SORT_ITEM f -> GenAx
getGenSorts si :: SORT_ITEM f
si = let
  (sorts :: Set SORT
sorts, rel :: Rel SORT
rel) = case SORT_ITEM f
si of
    Sort_decl il :: [SORT]
il _ -> ([SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [SORT]
il, Rel SORT
forall a. Rel a
Rel.empty)
    Subsort_decl il :: [SORT]
il i :: SORT
i _ ->
      ([SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList (SORT
i SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
il), (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> [SORT] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
`Rel.insertDiffPair` SORT
i) Rel SORT
forall a. Rel a
Rel.empty [SORT]
il)
    Subsort_defn sub :: SORT
sub _ super :: SORT
super _ _ ->
      (SORT -> Set SORT
forall a. a -> Set a
Set.singleton SORT
sub, SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertDiffPair SORT
sub SORT
super Rel SORT
forall a. Rel a
Rel.empty)
    Iso_decl il :: [SORT]
il _ -> ([SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [SORT]
il,
      (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> [SORT] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ s :: SORT
s r :: Rel SORT
r -> (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> [SORT] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertDiffPair SORT
s) Rel SORT
r [SORT]
il) Rel SORT
forall a. Rel a
Rel.empty [SORT]
il)
    in (Set SORT
sorts, Rel SORT
rel, Set Component
forall a. Set a
Set.empty)

getOps :: OP_ITEM f -> Set.Set Component
getOps :: OP_ITEM f -> Set Component
getOps oi :: OP_ITEM f
oi = case OP_ITEM f
oi of
    Op_decl is :: [SORT]
is ty :: OP_TYPE
ty _ _ ->
        [Component] -> Set Component
forall a. Ord a => [a] -> Set a
Set.fromList ([Component] -> Set Component) -> [Component] -> Set Component
forall a b. (a -> b) -> a -> b
$ (SORT -> Component) -> [SORT] -> [Component]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT -> OpType -> Component) -> OpType -> SORT -> Component
forall a b c. (a -> b -> c) -> b -> a -> c
flip SORT -> OpType -> Component
Component (OpType -> SORT -> Component) -> OpType -> SORT -> Component
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
ty) [SORT]
is
    Op_defn i :: SORT
i par :: OP_HEAD
par _ _ -> Set Component
-> (OP_TYPE -> Set Component) -> Maybe OP_TYPE -> Set Component
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Component
forall a. Set a
Set.empty
        (Component -> Set Component
forall a. a -> Set a
Set.singleton (Component -> Set Component)
-> (OP_TYPE -> Component) -> OP_TYPE -> Set Component
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> OpType -> Component
Component SORT
i (OpType -> Component)
-> (OP_TYPE -> OpType) -> OP_TYPE -> Component
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_TYPE -> OpType
toOpType) (Maybe OP_TYPE -> Set Component) -> Maybe OP_TYPE -> Set Component
forall a b. (a -> b) -> a -> b
$ OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
par

ana_SORT_ITEM :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> SortsKind -> Annoted (SORT_ITEM f)
    -> State (Sign f e) (Annoted (SORT_ITEM f))
ana_SORT_ITEM :: Min f e
-> Mix b s f e
-> SortsKind
-> Annoted (SORT_ITEM f)
-> State (Sign f e) (Annoted (SORT_ITEM f))
ana_SORT_ITEM mef :: Min f e
mef mix :: Mix b s f e
mix sk :: SortsKind
sk asi :: Annoted (SORT_ITEM f)
asi =
    case Annoted (SORT_ITEM f) -> SORT_ITEM f
forall a. Annoted a -> a
item Annoted (SORT_ITEM f)
asi of
    Sort_decl il :: [SORT]
il _ ->
        do (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SortsKind -> Annoted (SORT_ITEM f) -> SORT -> State (Sign f e) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
sk Annoted (SORT_ITEM f)
asi) [SORT]
il
           Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (SORT_ITEM f)
asi
    Subsort_decl il :: [SORT]
il i :: SORT
i _ ->
        do (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SortsKind -> Annoted (SORT_ITEM f) -> SORT -> State (Sign f e) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
sk Annoted (SORT_ITEM f)
asi) (SORT
i SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT]
il)
           (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SORT -> SORT -> State (Sign f e) ()
forall f e. SORT -> SORT -> State (Sign f e) ()
addSubsort SORT
i) [SORT]
il
           Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (SORT_ITEM f)
asi
    Subsort_defn sub :: SORT
sub v :: SIMPLE_ID
v super :: SORT
super af :: Annoted (FORMULA f)
af ps :: Range
ps ->
        do Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get -- save
           Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { varMap :: Map SIMPLE_ID SORT
varMap = Map SIMPLE_ID SORT
forall k a. Map k a
Map.empty }
           VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars ([SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] SORT
super Range
ps)
           Sign f e
sign <- State (Sign f e) (Sign f e)
forall s. State s s
get
           Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e -- restore
           let Result ds :: [Diagnosis]
ds mf :: Maybe (FORMULA f, FORMULA f)
mf = Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm Min f e
mef Mix b s f e
mix Sign f e
sign (FORMULA f -> Result (FORMULA f, FORMULA f))
-> FORMULA f -> Result (FORMULA f, FORMULA f)
forall a b. (a -> b) -> a -> b
$ Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item Annoted (FORMULA f)
af
               lb :: String
lb = Annoted (FORMULA f) -> String
forall a. Annoted a -> String
getRLabel Annoted (FORMULA f)
af
               lab :: String
lab = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lb then Annoted (SORT_ITEM f) -> String
forall a. Annoted a -> String
getRLabel Annoted (SORT_ITEM f)
asi else String
lb
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
           SortsKind -> Annoted (SORT_ITEM f) -> SORT -> State (Sign f e) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
sk Annoted (SORT_ITEM f)
asi SORT
sub
           SORT -> SORT -> State (Sign f e) ()
forall f e. SORT -> SORT -> State (Sign f e) ()
addSubsort SORT
super SORT
sub
           case Maybe (FORMULA f, FORMULA f)
mf of
             Nothing -> Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (SORT_ITEM f)
asi { item :: SORT_ITEM f
item = [SORT] -> SORT -> Range -> SORT_ITEM f
forall f. [SORT] -> SORT -> Range -> SORT_ITEM f
Subsort_decl [SORT
sub] SORT
super Range
ps}
             Just (resF :: FORMULA f
resF, anaF :: FORMULA f
anaF) -> do
               let p :: Range
p = SORT -> Range
posOfId SORT
sub
                   pv :: Range
pv = SIMPLE_ID -> Range
tokPos SIMPLE_ID
v
               [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences [(String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
lab (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$
                              [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [[SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] SORT
super Range
pv]
                              (FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation
                               (TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership (SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
v SORT
super Range
pv) SORT
sub Range
p)
                               Relation
Equivalence FORMULA f
anaF Range
p) Range
p) {
                              isAxiom :: Bool
isAxiom = Annoted (FORMULA f) -> Bool
forall a. Annoted a -> Bool
notImplied Annoted (FORMULA f)
af }]
               Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (SORT_ITEM f)
asi { item :: SORT_ITEM f
item = SORT
-> SIMPLE_ID -> SORT -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
forall f.
SORT
-> SIMPLE_ID -> SORT -> Annoted (FORMULA f) -> Range -> SORT_ITEM f
Subsort_defn SORT
sub SIMPLE_ID
v SORT
super
                                   Annoted (FORMULA f)
af { item :: FORMULA f
item = FORMULA f
resF } Range
ps}
    Iso_decl il :: [SORT]
il _ ->
        do (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SortsKind -> Annoted (SORT_ITEM f) -> SORT -> State (Sign f e) ()
forall a f e. SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
addSort SortsKind
sk Annoted (SORT_ITEM f)
asi) [SORT]
il
           case [SORT]
il of
               [] -> () -> State (Sign f e) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
               _ : tl :: [SORT]
tl -> ((SORT, SORT) -> State (Sign f e) ())
-> [(SORT, SORT)] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((SORT -> SORT -> State (Sign f e) ())
-> (SORT, SORT) -> State (Sign f e) ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((SORT -> SORT -> State (Sign f e) ())
 -> (SORT, SORT) -> State (Sign f e) ())
-> (SORT -> SORT -> State (Sign f e) ())
-> (SORT, SORT)
-> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ Bool -> SORT -> SORT -> State (Sign f e) ()
forall f e. Bool -> SORT -> SORT -> State (Sign f e) ()
addSubsortOrIso Bool
False)
                         ([(SORT, SORT)] -> State (Sign f e) ())
-> [(SORT, SORT)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [SORT] -> [SORT] -> [(SORT, SORT)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SORT]
tl [SORT]
il
           Annoted (SORT_ITEM f) -> State (Sign f e) (Annoted (SORT_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (SORT_ITEM f)
asi

putVarsInEmptyMap :: [VAR_DECL] -> State (Sign f e) (Sign f e)
putVarsInEmptyMap :: [VAR_DECL] -> State (Sign f e) (Sign f e)
putVarsInEmptyMap vs :: [VAR_DECL]
vs = do
           Sign f e
e <- State (Sign f e) (Sign f e)
forall s. State s s
get -- save
           Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e { varMap :: Map SIMPLE_ID SORT
varMap = Map SIMPLE_ID SORT
forall k a. Map k a
Map.empty }
           (VAR_DECL -> State (Sign f e) ())
-> [VAR_DECL] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs
           Sign f e
sign <- State (Sign f e) (Sign f e)
forall s. State s s
get
           Sign f e -> State (Sign f e) ()
forall s. s -> State s ()
put Sign f e
e -- restore
           Sign f e -> State (Sign f e) (Sign f e)
forall (m :: * -> *) a. Monad m => a -> m a
return Sign f e
sign

ana_OP_ITEM :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Annoted (OP_ITEM f)
    -> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM :: Min f e
-> Mix b s f e
-> Annoted (OP_ITEM f)
-> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM mef :: Min f e
mef mix :: Mix b s f e
mix aoi :: Annoted (OP_ITEM f)
aoi =
    case Annoted (OP_ITEM f) -> OP_ITEM f
forall a. Annoted a -> a
item Annoted (OP_ITEM f)
aoi of
    Op_decl ops :: [SORT]
ops ty :: OP_TYPE
ty il :: [OP_ATTR f]
il ps :: Range
ps ->
        do let oty :: OpType
oty = OP_TYPE -> OpType
toOpType OP_TYPE
ty
               ni :: Bool
ni = Annoted (OP_ITEM f) -> Bool
forall a. Annoted a -> Bool
notImplied Annoted (OP_ITEM f)
aoi
           (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Annoted (OP_ITEM f) -> OpType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp Annoted (OP_ITEM f)
aoi OpType
oty) [SORT]
ops
           [Maybe (OP_ATTR f)]
ul <- (OP_ATTR f -> State (Sign f e) (Maybe (OP_ATTR f)))
-> [OP_ATTR f] -> State (Sign f e) [Maybe (OP_ATTR f)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Min f e
-> Mix b s f e
-> OpType
-> Bool
-> [SORT]
-> OP_ATTR f
-> State (Sign f e) (Maybe (OP_ATTR f))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> OpType
-> Bool
-> [SORT]
-> OP_ATTR f
-> State (Sign f e) (Maybe (OP_ATTR f))
ana_OP_ATTR Min f e
mef Mix b s f e
mix OpType
oty Bool
ni [SORT]
ops) [OP_ATTR f]
il
           Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((OP_ATTR f -> Bool) -> [OP_ATTR f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a :: OP_ATTR f
a -> case OP_ATTR f
a of
                  Assoc_op_attr -> Bool
True
                  _ -> Bool
False) [OP_ATTR f]
il) (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ do
              (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (OpType -> SORT -> State (Sign f e) ()
forall f e. OpType -> SORT -> State (Sign f e) ()
addAssocOp OpType
oty) [SORT]
ops
              Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((OP_ATTR f -> Bool) -> [OP_ATTR f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a :: OP_ATTR f
a -> case OP_ATTR f
a of
                  Comm_op_attr -> Bool
True
                  _ -> Bool
False) [OP_ATTR f]
il)
                   (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (OpType -> Bool -> SORT -> Named (FORMULA f)
forall f. OpType -> Bool -> SORT -> Named (FORMULA f)
addLeftComm OpType
oty Bool
ni) [SORT]
ops
           Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (OP_ITEM f)
aoi {item :: OP_ITEM f
item = [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
forall f. [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [SORT]
ops OP_TYPE
ty ([Maybe (OP_ATTR f)] -> [OP_ATTR f]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (OP_ATTR f)]
ul) Range
ps}
    Op_defn i :: SORT
i ohd :: OP_HEAD
ohd@(Op_head k :: OpKind
k vs :: [VAR_DECL]
vs _ _) at :: Annoted (TERM f)
at ps :: Range
ps ->
        do let mty :: Maybe OP_TYPE
mty = OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
ohd
               lb :: String
lb = Annoted (TERM f) -> String
forall a. Annoted a -> String
getRLabel Annoted (TERM f)
at
               lab :: String
lab = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lb then Annoted (OP_ITEM f) -> String
forall a. Annoted a -> String
getRLabel Annoted (OP_ITEM f)
aoi else String
lb
               arg :: [TERM f]
arg = (VAR_DECL -> [TERM f]) -> [VAR_DECL] -> [TERM f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl v :: [SIMPLE_ID]
v s :: SORT
s qs :: Range
qs) ->
                                 (SIMPLE_ID -> TERM f) -> [SIMPLE_ID] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\ j :: SIMPLE_ID
j -> SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
j SORT
s Range
qs) [SIMPLE_ID]
v) [VAR_DECL]
vs
           State (Sign f e) ()
-> (OP_TYPE -> State (Sign f e) ())
-> Maybe OP_TYPE
-> State (Sign f e) ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> State (Sign f e) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (\ ty :: OP_TYPE
ty -> Annoted (OP_ITEM f) -> OpType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp Annoted (OP_ITEM f)
aoi (OP_TYPE -> OpType
toOpType OP_TYPE
ty) SORT
i) Maybe OP_TYPE
mty
           Sign f e
sign <- [VAR_DECL] -> State (Sign f e) (Sign f e)
forall f e. [VAR_DECL] -> State (Sign f e) (Sign f e)
putVarsInEmptyMap [VAR_DECL]
vs
           let Result ds :: [Diagnosis]
ds mt :: Maybe (TERM f, TERM f)
mt = Min f e
-> Mix b s f e
-> Sign f e
-> Maybe SORT
-> Range
-> TERM f
-> Result (TERM f, TERM f)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> Maybe SORT
-> Range
-> TERM f
-> Result (TERM f, TERM f)
anaTerm Min f e
mef Mix b s f e
mix Sign f e
sign
                 ((OP_TYPE -> SORT) -> Maybe OP_TYPE -> Maybe SORT
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OP_TYPE -> SORT
res_OP_TYPE Maybe OP_TYPE
mty) Range
ps (TERM f -> Result (TERM f, TERM f))
-> TERM f -> Result (TERM f, TERM f)
forall a b. (a -> b) -> a -> b
$ Annoted (TERM f) -> TERM f
forall a. Annoted a -> a
item Annoted (TERM f)
at
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
           case Maybe (TERM f, TERM f)
mt of
             Nothing -> Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f)))
-> Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))
forall a b. (a -> b) -> a -> b
$ Annoted (OP_ITEM f)
-> (OP_TYPE -> Annoted (OP_ITEM f))
-> Maybe OP_TYPE
-> Annoted (OP_ITEM f)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Annoted (OP_ITEM f)
aoi
               (\ ty :: OP_TYPE
ty -> Annoted (OP_ITEM f)
aoi { item :: OP_ITEM f
item = [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
forall f. [SORT] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [SORT
i] OP_TYPE
ty [] Range
ps }) Maybe OP_TYPE
mty
             Just (resT :: TERM f
resT, anaT :: TERM f
anaT) -> do
                 let p :: Range
p = SORT -> Range
posOfId SORT
i
                     tvs :: VarSet
tvs = Sign f e -> TERM f -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign f e
sign TERM f
anaT
                     ty :: OP_TYPE
ty = OP_TYPE -> (OP_TYPE -> OP_TYPE) -> OP_HEAD -> OP_TYPE
forall a. a -> (OP_TYPE -> a) -> OP_HEAD -> a
headToTypeM (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
k ([VAR_DECL] -> [SORT]
sortsOfArgs [VAR_DECL]
vs)
                                       (TERM f -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM f
anaT) Range
ps) OP_TYPE -> OP_TYPE
forall a. a -> a
id OP_HEAD
ohd
                 State (Sign f e) ()
-> (OP_TYPE -> State (Sign f e) ())
-> Maybe OP_TYPE
-> State (Sign f e) ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Annoted (OP_ITEM f) -> OpType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp Annoted (OP_ITEM f)
aoi (OP_TYPE -> OpType
toOpType OP_TYPE
ty) SORT
i) (State (Sign f e) () -> OP_TYPE -> State (Sign f e) ()
forall a b. a -> b -> a
const (State (Sign f e) () -> OP_TYPE -> State (Sign f e) ())
-> State (Sign f e) () -> OP_TYPE -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ () -> State (Sign f e) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) Maybe OP_TYPE
mty
                 [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ String -> Sign f e -> VarSet -> [Diagnosis]
forall f e. String -> Sign f e -> VarSet -> [Diagnosis]
warnUnusedVars " local " Sign f e
sign VarSet
tvs
                 [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences [(String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
lab (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
                     (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                      (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i OP_TYPE
ty Range
p) [TERM f]
forall f. [TERM f]
arg Range
ps)
                      Equality
Strong TERM f
anaT Range
p) Range
ps) {
                       isAxiom :: Bool
isAxiom = Annoted (TERM f) -> Bool
forall a. Annoted a -> Bool
notImplied Annoted (TERM f)
at, isDef :: Bool
isDef = Bool
True }]
                 Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (OP_ITEM f)
aoi {item :: OP_ITEM f
item = SORT -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
forall f. SORT -> OP_HEAD -> Annoted (TERM f) -> Range -> OP_ITEM f
Op_defn SORT
i OP_HEAD
ohd Annoted (TERM f)
at { item :: TERM f
item = TERM f
resT } Range
ps }

headToTypeM :: a -> (OP_TYPE -> a) -> OP_HEAD -> a
headToTypeM :: a -> (OP_TYPE -> a) -> OP_HEAD -> a
headToTypeM def :: a
def f :: OP_TYPE -> a
f (Op_head k :: OpKind
k args :: [VAR_DECL]
args mr :: Maybe SORT
mr ps :: Range
ps) = a -> (SORT -> a) -> Maybe SORT -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
def
  (\ r :: SORT
r -> OP_TYPE -> a
f (OP_TYPE -> a) -> OP_TYPE -> a
forall a b. (a -> b) -> a -> b
$ OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
k ([VAR_DECL] -> [SORT]
sortsOfArgs [VAR_DECL]
args) SORT
r Range
ps) Maybe SORT
mr

headToType :: OP_HEAD -> Maybe OP_TYPE
headToType :: OP_HEAD -> Maybe OP_TYPE
headToType = Maybe OP_TYPE
-> (OP_TYPE -> Maybe OP_TYPE) -> OP_HEAD -> Maybe OP_TYPE
forall a. a -> (OP_TYPE -> a) -> OP_HEAD -> a
headToTypeM Maybe OP_TYPE
forall a. Maybe a
Nothing OP_TYPE -> Maybe OP_TYPE
forall a. a -> Maybe a
Just

sortsOfArgs :: [VAR_DECL] -> [SORT]
sortsOfArgs :: [VAR_DECL] -> [SORT]
sortsOfArgs = (VAR_DECL -> [SORT]) -> [VAR_DECL] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl l :: [SIMPLE_ID]
l s :: SORT
s _) -> (SIMPLE_ID -> SORT) -> [SIMPLE_ID] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> SIMPLE_ID -> SORT
forall a b. a -> b -> a
const SORT
s) [SIMPLE_ID]
l)

threeVars :: SORT -> ([VAR_DECL], [TERM f])
threeVars :: SORT -> ([VAR_DECL], [TERM f])
threeVars rty :: SORT
rty =
      let q :: Range
q = SORT -> Range
posOfId SORT
rty
          ns :: [SIMPLE_ID]
ns = (String -> SIMPLE_ID) -> [String] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map String -> SIMPLE_ID
mkSimpleId ["x", "y", "z"]
          vs :: [VAR_DECL]
vs = (SIMPLE_ID -> VAR_DECL) -> [SIMPLE_ID] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: SIMPLE_ID
v -> [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] SORT
rty Range
q) [SIMPLE_ID]
ns
      in ([VAR_DECL]
vs, (VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs)

-- see Isabelle/doc/ref.pdf 10.6 Permutative rewrite rules (p. 137)
addLeftComm :: OpType -> Bool -> Id -> Named (FORMULA f)
addLeftComm :: OpType -> Bool -> SORT -> Named (FORMULA f)
addLeftComm ty :: OpType
ty ni :: Bool
ni i :: SORT
i =
  let sty :: OP_TYPE
sty = OpType -> OP_TYPE
toOP_TYPE OpType
ty
      rty :: SORT
rty = OpType -> SORT
opRes OpType
ty
      (vs :: [VAR_DECL]
vs, [v1 :: TERM f
v1, v2 :: TERM f
v2, v3 :: TERM f
v3]) = SORT -> ([VAR_DECL], [TERM f])
forall f. SORT -> ([VAR_DECL], [TERM f])
threeVars SORT
rty
      p :: Range
p = SORT -> Range
posOfId SORT
i
      qi :: OP_SYMB
qi = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i OP_TYPE
sty Range
p
  in (String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_left_comm_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
i "") (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$
             [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
             (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
              (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v1, OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v2, TERM f
forall f. TERM f
v3] Range
p] Range
p) Equality
Strong
              (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v2, OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v1, TERM f
forall f. TERM f
v3] Range
p] Range
p) Range
p) Range
p)
            { isAxiom :: Bool
isAxiom = Bool
ni }

ana_OP_ATTR :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> OpType -> Bool -> [Id] -> OP_ATTR f
    -> State (Sign f e) (Maybe (OP_ATTR f))
ana_OP_ATTR :: Min f e
-> Mix b s f e
-> OpType
-> Bool
-> [SORT]
-> OP_ATTR f
-> State (Sign f e) (Maybe (OP_ATTR f))
ana_OP_ATTR mef :: Min f e
mef mix :: Mix b s f e
mix ty :: OpType
ty ni :: Bool
ni ois :: [SORT]
ois oa :: OP_ATTR f
oa = do
  let sty :: OP_TYPE
sty = OpType -> OP_TYPE
toOP_TYPE OpType
ty
      rty :: SORT
rty = OpType -> SORT
opRes OpType
ty
      atys :: [SORT]
atys = OpType -> [SORT]
opArgs OpType
ty
      q :: Range
q = SORT -> Range
posOfId SORT
rty
      tds :: [Diagnosis]
tds = case [SORT]
atys of
         [t1 :: SORT
t1, t2 :: SORT
t2] | SORT
t1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
t2 -> case OP_ATTR f
oa of
              Comm_op_attr -> []
              _ -> [ DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error "result sort must be equal to argument sorts" Range
q
                   | SORT
t1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
/= SORT
rty ]
         _ -> [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error "expecting two arguments of equal sort" Range
q]
  [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
tds
  case OP_ATTR f
oa of
    Unit_op_attr t :: TERM f
t -> do
           Sign f e
sign <- State (Sign f e) (Sign f e)
forall s. State s s
get
           let Result ds :: [Diagnosis]
ds mt :: Maybe (TERM f, TERM f)
mt = Min f e
-> Mix b s f e
-> Sign f e
-> Maybe SORT
-> Range
-> TERM f
-> Result (TERM f, TERM f)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> Maybe SORT
-> Range
-> TERM f
-> Result (TERM f, TERM f)
anaTerm Min f e
mef Mix b s f e
mix
                              Sign f e
sign { varMap :: Map SIMPLE_ID SORT
varMap = Map SIMPLE_ID SORT
forall k a. Map k a
Map.empty } (SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
rty) Range
q TERM f
t
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
           case Maybe (TERM f, TERM f)
mt of
             Nothing -> Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (OP_ATTR f)
forall a. Maybe a
Nothing
             Just (resT :: TERM f
resT, anaT :: TERM f
anaT) -> do
               Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
tds) (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ do
                 [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> TERM f -> OpType -> Bool -> SORT -> Named (FORMULA f)
forall f.
Bool -> TERM f -> OpType -> Bool -> SORT -> Named (FORMULA f)
makeUnit Bool
True TERM f
anaT OpType
ty Bool
ni) [SORT]
ois
                 [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> TERM f -> OpType -> Bool -> SORT -> Named (FORMULA f)
forall f.
Bool -> TERM f -> OpType -> Bool -> SORT -> Named (FORMULA f)
makeUnit Bool
False TERM f
anaT OpType
ty Bool
ni) [SORT]
ois
               Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f)))
-> Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall a b. (a -> b) -> a -> b
$ OP_ATTR f -> Maybe (OP_ATTR f)
forall a. a -> Maybe a
Just (OP_ATTR f -> Maybe (OP_ATTR f)) -> OP_ATTR f -> Maybe (OP_ATTR f)
forall a b. (a -> b) -> a -> b
$ TERM f -> OP_ATTR f
forall f. TERM f -> OP_ATTR f
Unit_op_attr TERM f
resT
    Assoc_op_attr -> do
      let (vs :: [VAR_DECL]
vs, [v1 :: TERM f
v1, v2 :: TERM f
v2, v3 :: TERM f
v3]) = SORT -> ([VAR_DECL], [TERM f])
forall f. SORT -> ([VAR_DECL], [TERM f])
threeVars SORT
rty
          makeAssoc :: SORT -> SenAttr (FORMULA f) String
makeAssoc i :: SORT
i = let p :: Range
p = SORT -> Range
posOfId SORT
i
                            qi :: OP_SYMB
qi = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i OP_TYPE
sty Range
p in
            (String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_assoc_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
i "") (FORMULA f -> SenAttr (FORMULA f) String)
-> FORMULA f -> SenAttr (FORMULA f) String
forall a b. (a -> b) -> a -> b
$
             [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
             (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
              (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v1, TERM f
forall f. TERM f
v2] Range
p, TERM f
forall f. TERM f
v3] Range
p) Equality
Strong
              (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v1, OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f
forall f. TERM f
v2, TERM f
forall f. TERM f
v3] Range
p] Range
p) Range
p) Range
p)
            { isAxiom :: Bool
isAxiom = Bool
ni }
      Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
tds) (State (Sign f e) () -> State (Sign f e) ())
-> ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)]
-> State (Sign f e) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Named (FORMULA f)
forall f. SORT -> SenAttr (FORMULA f) String
makeAssoc [SORT]
ois
      Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f)))
-> Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall a b. (a -> b) -> a -> b
$ OP_ATTR f -> Maybe (OP_ATTR f)
forall a. a -> Maybe a
Just OP_ATTR f
oa
    Comm_op_attr -> do
      let ns :: [SIMPLE_ID]
ns = (String -> SIMPLE_ID) -> [String] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map String -> SIMPLE_ID
mkSimpleId ["x", "y"]
          vs :: [VAR_DECL]
vs = (SIMPLE_ID -> SORT -> VAR_DECL)
-> [SIMPLE_ID] -> [SORT] -> [VAR_DECL]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ v :: SIMPLE_ID
v t :: SORT
t -> [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] SORT
t
                         (Range -> VAR_DECL) -> Range -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ (SORT -> Range) -> [SORT] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange SORT -> Range
posOfId [SORT]
atys) [SIMPLE_ID]
ns [SORT]
atys
          args :: [TERM f]
args = (VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs
          makeComm :: SORT -> SenAttr (FORMULA f) String
makeComm i :: SORT
i = let p :: Range
p = SORT -> Range
posOfId SORT
i
                           qi :: OP_SYMB
qi = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i OP_TYPE
sty Range
p in
            (String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_comm_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
i "") (FORMULA f -> SenAttr (FORMULA f) String)
-> FORMULA f -> SenAttr (FORMULA f) String
forall a b. (a -> b) -> a -> b
$
             [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
             (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi [TERM f]
forall f. [TERM f]
args Range
p) Equality
Strong
              (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
qi ([TERM f] -> [TERM f]
forall a. [a] -> [a]
reverse [TERM f]
forall f. [TERM f]
args) Range
p) Range
p) Range
p) {
             isAxiom :: Bool
isAxiom = Bool
ni }
      Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
tds) (State (Sign f e) () -> State (Sign f e) ())
-> ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)]
-> State (Sign f e) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Named (FORMULA f)
forall f. SORT -> SenAttr (FORMULA f) String
makeComm [SORT]
ois
      Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f)))
-> Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall a b. (a -> b) -> a -> b
$ OP_ATTR f -> Maybe (OP_ATTR f)
forall a. a -> Maybe a
Just OP_ATTR f
oa
    Idem_op_attr -> do
      let v :: SIMPLE_ID
v = String -> SIMPLE_ID
mkSimpleId "x"
          vd :: VAR_DECL
vd = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] SORT
rty Range
q
          qv :: TERM f
qv = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vd
          makeIdem :: SORT -> SenAttr (FORMULA f) String
makeIdem i :: SORT
i = let p :: Range
p = SORT -> Range
posOfId SORT
i in
           (String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_idem_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
i "") (FORMULA f -> SenAttr (FORMULA f) String)
-> FORMULA f -> SenAttr (FORMULA f) String
forall a b. (a -> b) -> a -> b
$
            [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
vd]
            (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
             (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i OP_TYPE
sty Range
p) [TERM f
forall f. TERM f
qv, TERM f
forall f. TERM f
qv] Range
p)
             Equality
Strong TERM f
forall f. TERM f
qv Range
p) Range
p) { isAxiom :: Bool
isAxiom = Bool
ni }
      Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
tds) (State (Sign f e) () -> State (Sign f e) ())
-> ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)]
-> State (Sign f e) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Named (FORMULA f)
forall f. SORT -> SenAttr (FORMULA f) String
makeIdem [SORT]
ois
      Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f)))
-> Maybe (OP_ATTR f) -> State (Sign f e) (Maybe (OP_ATTR f))
forall a b. (a -> b) -> a -> b
$ OP_ATTR f -> Maybe (OP_ATTR f)
forall a. a -> Maybe a
Just OP_ATTR f
oa

-- first bool for left and right, second one for no implied annotation
makeUnit :: Bool -> TERM f -> OpType -> Bool -> Id -> Named (FORMULA f)
makeUnit :: Bool -> TERM f -> OpType -> Bool -> SORT -> Named (FORMULA f)
makeUnit b :: Bool
b t :: TERM f
t ty :: OpType
ty ni :: Bool
ni i :: SORT
i =
    let lab :: String
lab = "ga_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "right" else "left") String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_unit_"
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
i ""
        v :: SIMPLE_ID
v = String -> SIMPLE_ID
mkSimpleId "x"
        vty :: SORT
vty = OpType -> SORT
opRes OpType
ty
        q :: Range
q = SORT -> Range
posOfId SORT
vty
        p :: Range
p = SORT -> Range
posOfId SORT
i
        qv :: TERM f
qv = SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
v SORT
vty Range
q
        args :: [TERM f]
args = [TERM f
forall f. TERM f
qv, TERM f
t]
        rargs :: [TERM f]
rargs = if Bool
b then [TERM f]
args else [TERM f] -> [TERM f]
forall a. [a] -> [a]
reverse [TERM f]
args
    in (String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
lab (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [[SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] SORT
vty Range
q]
                     (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                      (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
i (OpType -> OP_TYPE
toOP_TYPE OpType
ty) Range
p) [TERM f]
rargs Range
p)
                      Equality
Strong TERM f
forall f. TERM f
qv Range
p) Range
p) {isAxiom :: Bool
isAxiom = Bool
ni }

ana_PRED_ITEM :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Annoted (PRED_ITEM f)
    -> State (Sign f e) (Annoted (PRED_ITEM f))
ana_PRED_ITEM :: Min f e
-> Mix b s f e
-> Annoted (PRED_ITEM f)
-> State (Sign f e) (Annoted (PRED_ITEM f))
ana_PRED_ITEM mef :: Min f e
mef mix :: Mix b s f e
mix apr :: Annoted (PRED_ITEM f)
apr = case Annoted (PRED_ITEM f) -> PRED_ITEM f
forall a. Annoted a -> a
item Annoted (PRED_ITEM f)
apr of
    Pred_decl preds :: [SORT]
preds ty :: PRED_TYPE
ty _ -> do
      (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Annoted (PRED_ITEM f) -> PredType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred Annoted (PRED_ITEM f)
apr (PredType -> SORT -> State (Sign f e) ())
-> PredType -> SORT -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> PredType
toPredType PRED_TYPE
ty) [SORT]
preds
      Annoted (PRED_ITEM f) -> State (Sign f e) (Annoted (PRED_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (PRED_ITEM f)
apr
    Pred_defn i :: SORT
i phd :: PRED_HEAD
phd@(Pred_head vs :: [VAR_DECL]
vs rs :: Range
rs) at :: Annoted (FORMULA f)
at ps :: Range
ps -> do
           let lb :: String
lb = Annoted (FORMULA f) -> String
forall a. Annoted a -> String
getRLabel Annoted (FORMULA f)
at
               lab :: String
lab = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lb then Annoted (PRED_ITEM f) -> String
forall a. Annoted a -> String
getRLabel Annoted (PRED_ITEM f)
apr else String
lb
               ty :: PRED_TYPE
ty = [SORT] -> Range -> PRED_TYPE
Pred_type ([VAR_DECL] -> [SORT]
sortsOfArgs [VAR_DECL]
vs) Range
rs
               arg :: [TERM f]
arg = (VAR_DECL -> [TERM f]) -> [VAR_DECL] -> [TERM f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl v :: [SIMPLE_ID]
v s :: SORT
s qs :: Range
qs) ->
                                 (SIMPLE_ID -> TERM f) -> [SIMPLE_ID] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (\ j :: SIMPLE_ID
j -> SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
j SORT
s Range
qs) [SIMPLE_ID]
v) [VAR_DECL]
vs
           Annoted (PRED_ITEM f) -> PredType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred Annoted (PRED_ITEM f)
apr (PRED_TYPE -> PredType
toPredType PRED_TYPE
ty) SORT
i
           Sign f e
sign <- [VAR_DECL] -> State (Sign f e) (Sign f e)
forall f e. [VAR_DECL] -> State (Sign f e) (Sign f e)
putVarsInEmptyMap [VAR_DECL]
vs
           let Result ds :: [Diagnosis]
ds mt :: Maybe (FORMULA f, FORMULA f)
mt = Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm Min f e
mef Mix b s f e
mix Sign f e
sign (FORMULA f -> Result (FORMULA f, FORMULA f))
-> FORMULA f -> Result (FORMULA f, FORMULA f)
forall a b. (a -> b) -> a -> b
$ Annoted (FORMULA f) -> FORMULA f
forall a. Annoted a -> a
item Annoted (FORMULA f)
at
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
           case Maybe (FORMULA f, FORMULA f)
mt of
             Nothing -> Annoted (PRED_ITEM f) -> State (Sign f e) (Annoted (PRED_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (PRED_ITEM f)
apr {item :: PRED_ITEM f
item = [SORT] -> PRED_TYPE -> Range -> PRED_ITEM f
forall f. [SORT] -> PRED_TYPE -> Range -> PRED_ITEM f
Pred_decl [SORT
i] PRED_TYPE
ty Range
ps}
             Just (resF :: FORMULA f
resF, anaF :: FORMULA f
anaF) -> do
               let p :: Range
p = SORT -> Range
posOfId SORT
i
               [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences [(String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
lab (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$
                              [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
                              (FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
i PRED_TYPE
ty Range
p)
                                            [TERM f]
forall f. [TERM f]
arg Range
p) Relation
Equivalence FORMULA f
anaF Range
p) Range
p) {
                              isDef :: Bool
isDef = Bool
True }]
               Annoted (PRED_ITEM f) -> State (Sign f e) (Annoted (PRED_ITEM f))
forall (m :: * -> *) a. Monad m => a -> m a
return Annoted (PRED_ITEM f)
apr {item :: PRED_ITEM f
item = SORT -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
forall f.
SORT -> PRED_HEAD -> Annoted (FORMULA f) -> Range -> PRED_ITEM f
Pred_defn SORT
i PRED_HEAD
phd Annoted (FORMULA f)
at { item :: FORMULA f
item = FORMULA f
resF } Range
ps}

-- full function type of a selector (result sort is component sort)
data Component = Component { Component -> SORT
compId :: Id, Component -> OpType
compType :: OpType } deriving Int -> Component -> ShowS
[Component] -> ShowS
Component -> String
(Int -> Component -> ShowS)
-> (Component -> String)
-> ([Component] -> ShowS)
-> Show Component
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Component] -> ShowS
$cshowList :: [Component] -> ShowS
show :: Component -> String
$cshow :: Component -> String
showsPrec :: Int -> Component -> ShowS
$cshowsPrec :: Int -> Component -> ShowS
Show

instance Eq Component where
    Component i1 :: SORT
i1 t1 :: OpType
t1 == :: Component -> Component -> Bool
== Component i2 :: SORT
i2 t2 :: OpType
t2 =
        (SORT
i1, OpType -> [SORT]
opArgs OpType
t1, OpType -> SORT
opRes OpType
t1) (SORT, [SORT], SORT) -> (SORT, [SORT], SORT) -> Bool
forall a. Eq a => a -> a -> Bool
== (SORT
i2, OpType -> [SORT]
opArgs OpType
t2, OpType -> SORT
opRes OpType
t2)

instance Ord Component where
    Component i1 :: SORT
i1 t1 :: OpType
t1 <= :: Component -> Component -> Bool
<= Component i2 :: SORT
i2 t2 :: OpType
t2 =
        (SORT
i1, OpType -> [SORT]
opArgs OpType
t1, OpType -> SORT
opRes OpType
t1) (SORT, [SORT], SORT) -> (SORT, [SORT], SORT) -> Bool
forall a. Ord a => a -> a -> Bool
<= (SORT
i2, OpType -> [SORT]
opArgs OpType
t2, OpType -> SORT
opRes OpType
t2)

instance Pretty Component where
    pretty :: Component -> Doc
pretty (Component i :: SORT
i ty :: OpType
ty) =
        SORT -> Doc
forall a. Pretty a => a -> Doc
pretty SORT
i Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OpType -> Doc
forall a. Pretty a => a -> Doc
pretty OpType
ty

instance GetRange Component where
    getRange :: Component -> Range
getRange = SORT -> Range
forall a. GetRange a => a -> Range
getRange (SORT -> Range) -> (Component -> SORT) -> Component -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Component -> SORT
compId

-- | return list of constructors
ana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
ana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
ana_DATATYPE_DECL gk :: GenKind
gk (Datatype_decl s :: SORT
s al :: [Annoted ALTERNATIVE]
al _) =
    do [Maybe (Component, Set Component)]
ul <- (Annoted ALTERNATIVE
 -> State (Sign f e) (Maybe (Component, Set Component)))
-> [Annoted ALTERNATIVE]
-> State (Sign f e) [Maybe (Component, Set Component)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SORT
-> Annoted ALTERNATIVE
-> State (Sign f e) (Maybe (Component, Set Component))
forall f e.
SORT
-> Annoted ALTERNATIVE
-> State (Sign f e) (Maybe (Component, Set Component))
ana_ALTERNATIVE SORT
s) [Annoted ALTERNATIVE]
al
       let constr :: [(Component, Set Component)]
constr = [Maybe (Component, Set Component)] -> [(Component, Set Component)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Component, Set Component)]
ul
           cs :: [Component]
cs = ((Component, Set Component) -> Component)
-> [(Component, Set Component)] -> [Component]
forall a b. (a -> b) -> [a] -> [b]
map (Component, Set Component) -> Component
forall a b. (a, b) -> a
fst [(Component, Set Component)]
constr
       Bool -> State (Sign f e) () -> State (Sign f e) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Component, Set Component)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Component, Set Component)]
constr) (State (Sign f e) () -> State (Sign f e) ())
-> State (Sign f e) () -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ do
                  [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Component] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness [Component]
cs
                  let totalSels :: Set Component
totalSels = [Set Component] -> Set Component
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Component] -> Set Component)
-> [Set Component] -> Set Component
forall a b. (a -> b) -> a -> b
$ ((Component, Set Component) -> Set Component)
-> [(Component, Set Component)] -> [Set Component]
forall a b. (a -> b) -> [a] -> [b]
map (Component, Set Component) -> Set Component
forall a b. (a, b) -> b
snd [(Component, Set Component)]
constr
                      wrongConstr :: [(Component, Set Component)]
wrongConstr = ((Component, Set Component) -> Bool)
-> [(Component, Set Component)] -> [(Component, Set Component)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Set Component
totalSels Set Component -> Set Component -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Set Component -> Bool)
-> ((Component, Set Component) -> Set Component)
-> (Component, Set Component)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Component, Set Component) -> Set Component
forall a b. (a, b) -> b
snd) [(Component, Set Component)]
constr
                  [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ ((Component, Set Component) -> Diagnosis)
-> [(Component, Set Component)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c :: Component
c, _) -> DiagKind -> String -> Component -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                      ("total selectors '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS -> (Component -> ShowS) -> [Component] -> ShowS
forall a. ShowS -> (a -> ShowS) -> [a] -> ShowS
showSepList (String -> ShowS
showString ", ")
                       Component -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (Set Component -> [Component]
forall a. Set a -> [a]
Set.toList Set Component
totalSels)
                       "'\n  should be in alternative") Component
c) [(Component, Set Component)]
wrongConstr
       case GenKind
gk of
         Free -> do
           let allts :: [ALTERNATIVE]
allts = (Annoted ALTERNATIVE -> ALTERNATIVE)
-> [Annoted ALTERNATIVE] -> [ALTERNATIVE]
forall a b. (a -> b) -> [a] -> [b]
map Annoted ALTERNATIVE -> ALTERNATIVE
forall a. Annoted a -> a
item [Annoted ALTERNATIVE]
al
               (alts :: [ALTERNATIVE]
alts, subs :: [ALTERNATIVE]
subs) = (ALTERNATIVE -> Bool)
-> [ALTERNATIVE] -> ([ALTERNATIVE], [ALTERNATIVE])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ALTERNATIVE -> Bool
isConsAlt [ALTERNATIVE]
allts
               sbs :: [SORT]
sbs = (ALTERNATIVE -> [SORT]) -> [ALTERNATIVE] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ALTERNATIVE -> [SORT]
getAltSubsorts [ALTERNATIVE]
subs
               comps :: [(SORT, OpType, [COMPONENTS])]
comps = (ALTERNATIVE -> (SORT, OpType, [COMPONENTS]))
-> [ALTERNATIVE] -> [(SORT, OpType, [COMPONENTS])]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> ALTERNATIVE -> (SORT, OpType, [COMPONENTS])
getConsType SORT
s) [ALTERNATIVE]
alts
               ttrips :: [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
ttrips = ((SORT, OpType, [COMPONENTS])
 -> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)]))
-> [(SORT, OpType, [COMPONENTS])]
-> [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
forall a b. (a -> b) -> [a] -> [b]
map ((\ (a :: SORT
a, vs :: [VAR_DECL]
vs, t :: TERM f
t, ses :: [(Maybe SORT, OpType)]
ses) -> (SORT
a, [VAR_DECL]
vs, TERM f
t, [(Maybe SORT, OpType)] -> [(SORT, OpType)]
catSels [(Maybe SORT, OpType)]
ses))
                               ((SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
 -> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)]))
-> ((SORT, OpType, [COMPONENTS])
    -> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)]))
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "X" ) [(SORT, OpType, [COMPONENTS])]
comps
               sels :: [(SORT, OpType)]
sels = ((SORT, [VAR_DECL], TERM Any, [(SORT, OpType)])
 -> [(SORT, OpType)])
-> [(SORT, [VAR_DECL], TERM Any, [(SORT, OpType)])]
-> [(SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (_, _, _, ses :: [(SORT, OpType)]
ses) -> [(SORT, OpType)]
ses) [(SORT, [VAR_DECL], TERM Any, [(SORT, OpType)])]
forall f. [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
ttrips
           [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (ALTERNATIVE -> [Diagnosis] -> [Diagnosis])
-> [Diagnosis] -> [ALTERNATIVE] -> [Diagnosis]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a :: ALTERNATIVE
a ds :: [Diagnosis]
ds -> case ALTERNATIVE
a of
             Alt_construct p :: OpKind
p i :: SORT
i _ _ | OpKind
p OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Partial ->
               DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
               "illegal free partial constructor" SORT
i Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds
             _ -> [Diagnosis]
ds) [] [ALTERNATIVE]
allts
           [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType, [COMPONENTS]) -> Named (FORMULA f))
-> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
forall f. (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeInjective
                            ([(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)])
-> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType, [COMPONENTS]) -> Bool)
-> [(SORT, OpType, [COMPONENTS])] -> [(SORT, OpType, [COMPONENTS])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, ces :: [COMPONENTS]
ces) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [COMPONENTS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [COMPONENTS]
ces)
                              [(SORT, OpType, [COMPONENTS])]
comps
           [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT] -> [Named (FORMULA f)]
forall f. SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts SORT
s [SORT]
sbs
           [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType, [COMPONENTS]) -> [Named (FORMULA f)])
-> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: (SORT, OpType, [COMPONENTS])
c -> (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
forall f. (SORT, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
makeDisjToSort (SORT, OpType, [COMPONENTS])
c) [SORT]
sbs)
                        [(SORT, OpType, [COMPONENTS])]
comps
           [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall f. [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint [(SORT, OpType, [COMPONENTS])]
comps
           [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Maybe (Named (FORMULA f))] -> [Named (FORMULA f)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Named (FORMULA f))] -> [Named (FORMULA f)])
-> [Maybe (Named (FORMULA f))] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> [Maybe (Named (FORMULA f))])
-> [(SORT, OpType)] -> [Maybe (Named (FORMULA f))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                             (\ ses :: (SORT, OpType)
ses ->
                               ((SORT, [VAR_DECL], TERM f, [(SORT, OpType)])
 -> Maybe (Named (FORMULA f)))
-> [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
-> [Maybe (Named (FORMULA f))]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, OpType)
-> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)])
-> Maybe (Named (FORMULA f))
forall f.
(SORT, OpType)
-> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)])
-> Maybe (Named (FORMULA f))
makeUndefForm (SORT, OpType)
ses) [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
forall f. [(SORT, [VAR_DECL], TERM f, [(SORT, OpType)])]
ttrips) [(SORT, OpType)]
sels
         _ -> () -> State (Sign f e) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [Component] -> State (Sign f e) [Component]
forall (m :: * -> *) a. Monad m => a -> m a
return [Component]
cs

makeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts d :: SORT
d subs :: [SORT]
subs = case [SORT]
subs of
    [] -> []
    s :: SORT
s : rs :: [SORT]
rs -> (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> SORT -> Named (FORMULA f)
forall f. SORT -> SORT -> Named (FORMULA f)
makeDisjSubsort SORT
s) [SORT]
rs [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ SORT -> [SORT] -> [Named (FORMULA f)]
forall f. SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts SORT
d [SORT]
rs
  where
  makeDisjSubsort :: SORT -> SORT -> Named (FORMULA f)
  makeDisjSubsort :: SORT -> SORT -> Named (FORMULA f)
makeDisjSubsort s1 :: SORT
s1 s2 :: SORT
s2 = let
     n :: SIMPLE_ID
n = String -> SIMPLE_ID
mkSimpleId "x"
     pd :: Range
pd = SORT -> Range
posOfId SORT
d
     p1 :: Range
p1 = SORT -> Range
posOfId SORT
s1
     p2 :: Range
p2 = SORT -> Range
posOfId SORT
s2
     p :: Range
p = Range
pd Range -> Range -> Range
`appRange` Range
p1 Range -> Range -> Range
`appRange` Range
p2
     v :: VAR_DECL
v = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
n] SORT
d Range
pd
     qv :: TERM f
qv = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v
     in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_disjoint_sorts_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
s1 "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
s2 "")
         (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
v] (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [
              TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
forall f. TERM f
qv SORT
s1 Range
p1, TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
forall f. TERM f
qv SORT
s2 Range
p2] Range
p) Range
p) Range
p

makeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
makeDisjToSort :: (SORT, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
makeDisjToSort a :: (SORT, OpType, [COMPONENTS])
a s :: SORT
s =
    let (c :: SORT
c, v :: [VAR_DECL]
v, t :: TERM f
t, _) = String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "X" (SORT, OpType, [COMPONENTS])
a
        p :: Range
p = SORT -> Range
posOfId SORT
s
    in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_disjoint_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
c "_sort_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
s "")
         (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
v (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership TERM f
forall f. TERM f
t SORT
s Range
p) Range
p) Range
p

makeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeInjective :: (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeInjective a :: (SORT, OpType, [COMPONENTS])
a =
    let (c :: SORT
c, v1 :: [VAR_DECL]
v1, t1 :: TERM f
t1, _) = String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "X" (SORT, OpType, [COMPONENTS])
a
        (_, v2 :: [VAR_DECL]
v2, t2 :: TERM f
t2, _) = String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "Y" (SORT, OpType, [COMPONENTS])
a
        p :: Range
p = SORT -> Range
posOfId SORT
c
    in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_injective_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
c "")
        (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange ([VAR_DECL]
v1 [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL]
v2)
        (FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
forall f. TERM f
t1 Equality
Strong TERM f
forall f. TERM f
t2 Range
p) Relation
Equivalence
         (let ces :: [FORMULA f]
ces = (VAR_DECL -> VAR_DECL -> FORMULA f)
-> [VAR_DECL] -> [VAR_DECL] -> [FORMULA f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ w1 :: VAR_DECL
w1 w2 :: VAR_DECL
w2 -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                              (VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
w1) Equality
Strong (VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
w2) Range
p) [VAR_DECL]
v1 [VAR_DECL]
v2
          in [FORMULA f] -> Range -> FORMULA f
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange [FORMULA f]
forall f. [FORMULA f]
ces Range
p)
         Range
p) Range
p

makeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint :: [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint l :: [(SORT, OpType, [COMPONENTS])]
l = case [(SORT, OpType, [COMPONENTS])]
l of
    [] -> []
    c :: (SORT, OpType, [COMPONENTS])
c : cs :: [(SORT, OpType, [COMPONENTS])]
cs -> ((SORT, OpType, [COMPONENTS]) -> Named (FORMULA f))
-> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, OpType, [COMPONENTS])
-> (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
forall f.
(SORT, OpType, [COMPONENTS])
-> (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeDisj (SORT, OpType, [COMPONENTS])
c) [(SORT, OpType, [COMPONENTS])]
cs [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall f. [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint [(SORT, OpType, [COMPONENTS])]
cs
  where
  makeDisj :: (Id, OpType, [COMPONENTS]) -> (Id, OpType, [COMPONENTS])
           -> Named (FORMULA f)
  makeDisj :: (SORT, OpType, [COMPONENTS])
-> (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeDisj a1 :: (SORT, OpType, [COMPONENTS])
a1 a2 :: (SORT, OpType, [COMPONENTS])
a2 =
    let (c1 :: SORT
c1, v1 :: [VAR_DECL]
v1, t1 :: TERM f
t1, _) = String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "X" (SORT, OpType, [COMPONENTS])
a1
        (c2 :: SORT
c2, v2 :: [VAR_DECL]
v2, t2 :: TERM f
t2, _) = String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "Y" (SORT, OpType, [COMPONENTS])
a2
        p :: Range
p = SORT -> Range
posOfId SORT
c1 Range -> Range -> Range
`appRange` SORT -> Range
posOfId SORT
c2
    in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_disjoint_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
c1 "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
c2 "")
        (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange ([VAR_DECL]
v1 [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL]
v2) (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
forall f. TERM f
t1 Equality
Strong TERM f
forall f. TERM f
t2 Range
p) Range
p) Range
p

catSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]
catSels :: [(Maybe SORT, OpType)] -> [(SORT, OpType)]
catSels = ((Maybe SORT, OpType) -> (SORT, OpType))
-> [(Maybe SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (m :: Maybe SORT
m, t :: OpType
t) -> (Maybe SORT -> SORT
forall a. HasCallStack => Maybe a -> a
fromJust Maybe SORT
m, OpType
t)) ([(Maybe SORT, OpType)] -> [(SORT, OpType)])
-> ([(Maybe SORT, OpType)] -> [(Maybe SORT, OpType)])
-> [(Maybe SORT, OpType)]
-> [(SORT, OpType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                 ((Maybe SORT, OpType) -> Bool)
-> [(Maybe SORT, OpType)] -> [(Maybe SORT, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (m :: Maybe SORT
m, _) -> Maybe SORT -> Bool
forall a. Maybe a -> Bool
isJust Maybe SORT
m)

makeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)])
              -> Maybe (Named (FORMULA f))
makeUndefForm :: (SORT, OpType)
-> (SORT, [VAR_DECL], TERM f, [(SORT, OpType)])
-> Maybe (Named (FORMULA f))
makeUndefForm (s :: SORT
s, ty :: OpType
ty) (i :: SORT
i, vs :: [VAR_DECL]
vs, t :: TERM f
t, sels :: [(SORT, OpType)]
sels) =
    let p :: Range
p = SORT -> Range
posOfId SORT
s in
    if ((SORT, OpType) -> Bool) -> [(SORT, OpType)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (se :: SORT
se, ts :: OpType
ts) -> SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
se Bool -> Bool -> Bool
&& OpType -> SORT
opRes OpType
ts SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== OpType -> SORT
opRes OpType
ty ) [(SORT, OpType)]
sels
    then Maybe (Named (FORMULA f))
forall a. Maybe a
Nothing else
       Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall a. a -> Maybe a
Just (Named (FORMULA f) -> Maybe (Named (FORMULA f)))
-> Named (FORMULA f) -> Maybe (Named (FORMULA f))
forall a b. (a -> b) -> a -> b
$ String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_selector_undef_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
s "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
i "")
              (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
               (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation
                (TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness
                 (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
s (OpType -> OP_TYPE
toOP_TYPE OpType
ty) Range
p) [TERM f
t] Range
p)
                 Range
p) Range
p) Range
p

getAltSubsorts :: ALTERNATIVE -> [SORT]
getAltSubsorts :: ALTERNATIVE -> [SORT]
getAltSubsorts c :: ALTERNATIVE
c = case ALTERNATIVE
c of
    Subsorts cs :: [SORT]
cs _ -> [SORT]
cs
    _ -> []

getConsType :: SORT -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])
getConsType :: SORT -> ALTERNATIVE -> (SORT, OpType, [COMPONENTS])
getConsType s :: SORT
s c :: ALTERNATIVE
c =
    let getConsTypeAux :: (OpKind, a, t COMPONENTS) -> (a, OpType, t COMPONENTS)
getConsTypeAux (part :: OpKind
part, i :: a
i, il :: t COMPONENTS
il) =
          (a
i, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
part ((COMPONENTS -> [SORT]) -> t COMPONENTS -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                            (((Maybe SORT, OpType) -> SORT) -> [(Maybe SORT, OpType)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (OpType -> SORT
opRes (OpType -> SORT)
-> ((Maybe SORT, OpType) -> OpType) -> (Maybe SORT, OpType) -> SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe SORT, OpType) -> OpType
forall a b. (a, b) -> b
snd) ([(Maybe SORT, OpType)] -> [SORT])
-> (COMPONENTS -> [(Maybe SORT, OpType)]) -> COMPONENTS -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> COMPONENTS -> [(Maybe SORT, OpType)]
getCompType SORT
s) t COMPONENTS
il) SORT
s, t COMPONENTS
il)
     in case ALTERNATIVE
c of
        Subsorts _ _ -> String -> (SORT, OpType, [COMPONENTS])
forall a. HasCallStack => String -> a
error "getConsType"
        Alt_construct k :: OpKind
k a :: SORT
a l :: [COMPONENTS]
l _ -> (OpKind, SORT, [COMPONENTS]) -> (SORT, OpType, [COMPONENTS])
forall (t :: * -> *) a.
Foldable t =>
(OpKind, a, t COMPONENTS) -> (a, OpType, t COMPONENTS)
getConsTypeAux (OpKind
k, SORT
a, [COMPONENTS]
l)

getCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]
getCompType :: SORT -> COMPONENTS -> [(Maybe SORT, OpType)]
getCompType s :: SORT
s c :: COMPONENTS
c = case COMPONENTS
c of
  Cons_select k :: OpKind
k l :: [SORT]
l cs :: SORT
cs _ -> (SORT -> (Maybe SORT, OpType)) -> [SORT] -> [(Maybe SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: SORT
i -> (SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
i, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
k [SORT
s] SORT
cs)) [SORT]
l
  Sort cs :: SORT
cs -> [(Maybe SORT
forall a. Maybe a
Nothing, OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Partial [SORT
s] SORT
cs)]

genSelVars :: String -> Int -> [OpType] -> [VAR_DECL]
genSelVars :: String -> Int -> [OpType] -> [VAR_DECL]
genSelVars str :: String
str n :: Int
n tys :: [OpType]
tys = case [OpType]
tys of
  [] -> []
  ty :: OpType
ty : rs :: [OpType]
rs -> SIMPLE_ID -> SORT -> VAR_DECL
mkVarDecl (String -> Int -> SIMPLE_ID
mkNumVar String
str Int
n) (OpType -> SORT
opRes OpType
ty)
    VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: String -> Int -> [OpType] -> [VAR_DECL]
genSelVars String
str (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [OpType]
rs

makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
             -> [Named (FORMULA f)]
makeSelForms :: Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
makeSelForms n :: Int
n (i :: SORT
i, vs :: [VAR_DECL]
vs, t :: TERM f
t, tys :: [(Maybe SORT, OpType)]
tys) = case [(Maybe SORT, OpType)]
tys of
  [] -> []
  (mi :: Maybe SORT
mi, ty :: OpType
ty) : rs :: [(Maybe SORT, OpType)]
rs ->
    (case Maybe SORT
mi of
            Nothing -> []
            Just j :: SORT
j -> let p :: Range
p = SORT -> Range
posOfId SORT
j
                          rty :: SORT
rty = OpType -> SORT
opRes OpType
ty
                          q :: Range
q = SORT -> Range
posOfId SORT
rty in
              [String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_selector_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> ShowS
showId SORT
j "")
                     (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL]
vs
                      (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                       (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
j (OpType -> OP_TYPE
toOP_TYPE OpType
ty) Range
p) [TERM f
t] Range
p)
                       Equality
Strong (SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var (String -> Int -> SIMPLE_ID
mkNumVar "X" Int
n) SORT
rty Range
q) Range
p) Range
p]
    ) [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
forall f.
Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
makeSelForms (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (SORT
i, [VAR_DECL]
vs, TERM f
t, [(Maybe SORT, OpType)]
rs)

selForms1 :: String -> (Id, OpType, [COMPONENTS])
          -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
selForms1 :: String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 str :: String
str (i :: SORT
i, ty :: OpType
ty, il :: [COMPONENTS]
il) =
    let cs :: [(Maybe SORT, OpType)]
cs = (COMPONENTS -> [(Maybe SORT, OpType)])
-> [COMPONENTS] -> [(Maybe SORT, OpType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SORT -> COMPONENTS -> [(Maybe SORT, OpType)]
getCompType (OpType -> SORT
opRes OpType
ty)) [COMPONENTS]
il
        vs :: [VAR_DECL]
vs = String -> Int -> [OpType] -> [VAR_DECL]
genSelVars String
str 1 ([OpType] -> [VAR_DECL]) -> [OpType] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ ((Maybe SORT, OpType) -> OpType)
-> [(Maybe SORT, OpType)] -> [OpType]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe SORT, OpType) -> OpType
forall a b. (a, b) -> b
snd [(Maybe SORT, OpType)]
cs
    in (SORT
i, [VAR_DECL]
vs, OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
i (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
ty)
            ((VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
vs), [(Maybe SORT, OpType)]
cs)

selForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
selForms :: (SORT, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
selForms = Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
forall f.
Int
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
-> [Named (FORMULA f)]
makeSelForms 1 ((SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
 -> [Named (FORMULA f)])
-> ((SORT, OpType, [COMPONENTS])
    -> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)]))
-> (SORT, OpType, [COMPONENTS])
-> [Named (FORMULA f)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
forall f.
String
-> (SORT, OpType, [COMPONENTS])
-> (SORT, [VAR_DECL], TERM f, [(Maybe SORT, OpType)])
selForms1 "X"

-- | return the constructor and the set of total selectors
ana_ALTERNATIVE :: SORT -> Annoted ALTERNATIVE
                -> State (Sign f e) (Maybe (Component, Set.Set Component))
ana_ALTERNATIVE :: SORT
-> Annoted ALTERNATIVE
-> State (Sign f e) (Maybe (Component, Set Component))
ana_ALTERNATIVE s :: SORT
s c :: Annoted ALTERNATIVE
c = case Annoted ALTERNATIVE -> ALTERNATIVE
forall a. Annoted a -> a
item Annoted ALTERNATIVE
c of
    Subsorts ss :: [SORT]
ss _ -> do
        (SORT -> State (Sign f e) ()) -> [SORT] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SORT -> SORT -> State (Sign f e) ()
forall f e. SORT -> SORT -> State (Sign f e) ()
addSubsort SORT
s) [SORT]
ss
        Maybe (Component, Set Component)
-> State (Sign f e) (Maybe (Component, Set Component))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Component, Set Component)
forall a. Maybe a
Nothing
    ic :: ALTERNATIVE
ic -> do
        let cons :: (SORT, OpType, [COMPONENTS])
cons@(i :: SORT
i, ty :: OpType
ty, il :: [COMPONENTS]
il) = SORT -> ALTERNATIVE -> (SORT, OpType, [COMPONENTS])
getConsType SORT
s ALTERNATIVE
ic
        Annoted ALTERNATIVE -> OpType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp Annoted ALTERNATIVE
c OpType
ty SORT
i
        [([Component], [Component])]
ul <- (COMPONENTS -> State (Sign f e) ([Component], [Component]))
-> [COMPONENTS] -> State (Sign f e) [([Component], [Component])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SORT -> COMPONENTS -> State (Sign f e) ([Component], [Component])
forall f e.
SORT -> COMPONENTS -> State (Sign f e) ([Component], [Component])
ana_COMPONENTS SORT
s) [COMPONENTS]
il
        let ts :: [Component]
ts = (([Component], [Component]) -> [Component])
-> [([Component], [Component])] -> [Component]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Component], [Component]) -> [Component]
forall a b. (a, b) -> a
fst [([Component], [Component])]
ul
        [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ [Component] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Component]
ts [Component] -> [Component] -> [Component]
forall a. [a] -> [a] -> [a]
++ (([Component], [Component]) -> [Component])
-> [([Component], [Component])] -> [Component]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Component], [Component]) -> [Component]
forall a b. (a, b) -> b
snd [([Component], [Component])]
ul)
        [Named (FORMULA f)] -> State (Sign f e) ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ([Named (FORMULA f)] -> State (Sign f e) ())
-> [Named (FORMULA f)] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ (SORT, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
forall f. (SORT, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
selForms (SORT, OpType, [COMPONENTS])
cons
        Maybe (Component, Set Component)
-> State (Sign f e) (Maybe (Component, Set Component))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Component, Set Component)
 -> State (Sign f e) (Maybe (Component, Set Component)))
-> Maybe (Component, Set Component)
-> State (Sign f e) (Maybe (Component, Set Component))
forall a b. (a -> b) -> a -> b
$ (Component, Set Component) -> Maybe (Component, Set Component)
forall a. a -> Maybe a
Just (SORT -> OpType -> Component
Component SORT
i OpType
ty, [Component] -> Set Component
forall a. Ord a => [a] -> Set a
Set.fromList [Component]
ts)

-- | return total and partial selectors
ana_COMPONENTS :: SORT -> COMPONENTS
               -> State (Sign f e) ([Component], [Component])
ana_COMPONENTS :: SORT -> COMPONENTS -> State (Sign f e) ([Component], [Component])
ana_COMPONENTS s :: SORT
s c :: COMPONENTS
c = do
    let cs :: [(Maybe SORT, OpType)]
cs = SORT -> COMPONENTS -> [(Maybe SORT, OpType)]
getCompType SORT
s COMPONENTS
c
    [Maybe Component]
sels <- ((Maybe SORT, OpType) -> State (Sign f e) (Maybe Component))
-> [(Maybe SORT, OpType)] -> State (Sign f e) [Maybe Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (mi :: Maybe SORT
mi, ty :: OpType
ty) ->
            case Maybe SORT
mi of
            Nothing -> Maybe Component -> State (Sign f e) (Maybe Component)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Component
forall a. Maybe a
Nothing
            Just i :: SORT
i -> do
              Annoted () -> OpType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) OpType
ty SORT
i
              Maybe Component -> State (Sign f e) (Maybe Component)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Component -> State (Sign f e) (Maybe Component))
-> Maybe Component -> State (Sign f e) (Maybe Component)
forall a b. (a -> b) -> a -> b
$ Component -> Maybe Component
forall a. a -> Maybe a
Just (Component -> Maybe Component) -> Component -> Maybe Component
forall a b. (a -> b) -> a -> b
$ SORT -> OpType -> Component
Component SORT
i OpType
ty) [(Maybe SORT, OpType)]
cs
    ([Component], [Component])
-> State (Sign f e) ([Component], [Component])
forall (m :: * -> *) a. Monad m => a -> m a
return (([Component], [Component])
 -> State (Sign f e) ([Component], [Component]))
-> ([Component], [Component])
-> State (Sign f e) ([Component], [Component])
forall a b. (a -> b) -> a -> b
$ (Component -> Bool) -> [Component] -> ([Component], [Component])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (OpType -> Bool
isTotal (OpType -> Bool) -> (Component -> OpType) -> Component -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Component -> OpType
compType) ([Component] -> ([Component], [Component]))
-> [Component] -> ([Component], [Component])
forall a b. (a -> b) -> a -> b
$ [Maybe Component] -> [Component]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Component]
sels

-- | utility
resultToState :: (a -> Result a) -> a -> State (Sign f e) a
resultToState :: (a -> Result a) -> a -> State (Sign f e) a
resultToState f :: a -> Result a
f a :: a
a = do
    let r :: Result a
r = a -> Result a
f a
a
    [Diagnosis] -> State (Sign f e) ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags ([Diagnosis] -> State (Sign f e) ())
-> [Diagnosis] -> State (Sign f e) ()
forall a b. (a -> b) -> a -> b
$ Result a -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags Result a
r
    case Result a -> Maybe a
forall a. Result a -> Maybe a
maybeResult Result a
r of
        Nothing -> a -> State (Sign f e) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
        Just b :: a
b -> a -> State (Sign f e) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
b

-- wrap it all up for a logic

type Ana a b s f e = Mix b s f e -> a -> State (Sign f e) a

anaForm :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Sign f e -> FORMULA f
    -> Result (FORMULA f, FORMULA f)
anaForm :: Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm mef :: Min f e
mef mixIn :: Mix b s f e
mixIn sign :: Sign f e
sign f :: FORMULA f
f = do
    let mix :: Mix b s f e
mix = Set SIMPLE_ID -> Mix b s f e -> Mix b s f e
forall b s f e. Set SIMPLE_ID -> Mix b s f e -> Mix b s f e
extendMix (Map SIMPLE_ID SORT -> Set SIMPLE_ID
forall k a. Map k a -> Set k
Map.keysSet (Map SIMPLE_ID SORT -> Set SIMPLE_ID)
-> Map SIMPLE_ID SORT -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ Sign f e -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign f e
sign) Mix b s f e
mixIn
    FORMULA f
resF <- (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveFormula (Mix b s f e -> f -> f
forall b s f e. Mix b s f e -> f -> f
putParen Mix b s f e
mix) (Mix b s f e -> MixResolve f
forall b s f e. Mix b s f e -> MixResolve f
mixResolve Mix b s f e
mix)
            (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign) (Mix b s f e -> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix b s f e
mix) FORMULA f
f
    FORMULA f
anaF <- Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
mef Sign f e
sign FORMULA f
resF
    (FORMULA f, FORMULA f) -> Result (FORMULA f, FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f
resF, FORMULA f
anaF)

anaTerm :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Sign f e -> Maybe SORT -> Range -> TERM f
    -> Result (TERM f, TERM f)
anaTerm :: Min f e
-> Mix b s f e
-> Sign f e
-> Maybe SORT
-> Range
-> TERM f
-> Result (TERM f, TERM f)
anaTerm mef :: Min f e
mef mixIn :: Mix b s f e
mixIn sign :: Sign f e
sign msrt :: Maybe SORT
msrt pos :: Range
pos t :: TERM f
t = do
    let mix :: Mix b s f e
mix = Set SIMPLE_ID -> Mix b s f e -> Mix b s f e
forall b s f e. Set SIMPLE_ID -> Mix b s f e -> Mix b s f e
extendMix (Map SIMPLE_ID SORT -> Set SIMPLE_ID
forall k a. Map k a -> Set k
Map.keysSet (Map SIMPLE_ID SORT -> Set SIMPLE_ID)
-> Map SIMPLE_ID SORT -> Set SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ Sign f e -> Map SIMPLE_ID SORT
forall f e. Sign f e -> Map SIMPLE_ID SORT
varMap Sign f e
sign) Mix b s f e
mixIn
    TERM f
resT <- (f -> f) -> MixResolve f -> MixResolve (TERM f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixfix (Mix b s f e -> f -> f
forall b s f e. Mix b s f e -> f -> f
putParen Mix b s f e
mix) (Mix b s f e -> MixResolve f
forall b s f e. Mix b s f e -> MixResolve f
mixResolve Mix b s f e
mix)
            (Sign f e -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign f e
sign) (Mix b s f e -> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix b s f e
mix) TERM f
t
    TERM f
anaT <- Min f e -> Sign f e -> TERM f -> Result (TERM f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min f e
mef Sign f e
sign (TERM f -> Result (TERM f)) -> TERM f -> Result (TERM f)
forall a b. (a -> b) -> a -> b
$ TERM f -> (SORT -> TERM f) -> Maybe SORT -> TERM f
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TERM f
resT
      (\ srt :: SORT
srt -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
resT SORT
srt Range
pos) Maybe SORT
msrt
    (TERM f, TERM f) -> Result (TERM f, TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f
resT, TERM f
anaT)

basicAnalysis :: (FormExtension f, TermExtension f)
              => Min f e -- ^ type analysis of f
              -> Ana b b s f e  -- ^ static analysis of basic item b
              -> Ana s b s f e  -- ^ static analysis of signature item s
              -> Mix b s f e -- ^ for mixfix analysis
              -> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
  -> Result (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
            {- ^ (BS with analysed mixfix formulas for pretty printing,
            differences to input Sig,accumulated Sig,analysed Sentences) -}
basicAnalysis :: 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 mef :: Min f e
mef anab :: Ana b b s f e
anab anas :: Ana s b s f e
anas mix :: Mix b s f e
mix (bs :: BASIC_SPEC b s f
bs, inSig :: Sign f e
inSig, ga :: GlobalAnnos
ga) =
    let allIds :: IdSets
allIds = [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$ (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
forall b s f.
(b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
ids_BASIC_SPEC (Mix b s f e -> b -> IdSets
forall b s f e. Mix b s f e -> b -> IdSets
getBaseIds Mix b s f e
mix) (Mix b s f e -> s -> IdSets
forall b s f e. Mix b s f e -> s -> IdSets
getSigIds Mix b s f e
mix) BASIC_SPEC b s f
bs
                 IdSets -> [IdSets] -> [IdSets]
forall a. a -> [a] -> [a]
: Mix b s f e -> e -> IdSets
forall b s f e. Mix b s f e -> e -> IdSets
getExtIds Mix b s f e
mix (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
inSig) IdSets -> [IdSets] -> [IdSets]
forall a. a -> [a] -> [a]
:
                  [Set SORT -> Set SORT -> Set SORT -> IdSets
mkIdSets (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
allConstIds Sign f e
inSig) (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
allOpIds Sign f e
inSig)
                  (Set SORT -> IdSets) -> Set SORT -> IdSets
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
allPredIds Sign f e
inSig]
        (newBs :: BASIC_SPEC b s f
newBs, accSig :: Sign f e
accSig) = State (Sign f e) (BASIC_SPEC b s f)
-> Sign f e -> (BASIC_SPEC b s f, Sign f e)
forall s a. State s a -> s -> (a, s)
runState (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
-> State (Sign f e) (BASIC_SPEC b s f)
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
-> State (Sign f e) (BASIC_SPEC b s f)
ana_BASIC_SPEC Min f e
mef Ana b b s f e
anab Ana s b s f e
anas
               Mix b s f e
mix { mixRules :: (TokRules, Rules)
mixRules = GlobalAnnos -> IdSets -> (TokRules, Rules)
makeRules GlobalAnnos
ga IdSets
allIds }
               BASIC_SPEC b s f
bs) Sign f e
inSig { globAnnos :: GlobalAnnos
globAnnos = Sign f e -> GlobalAnnos -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos -> GlobalAnnos
addAssocs Sign f e
inSig GlobalAnnos
ga }
        ds :: [Diagnosis]
ds = [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a]
reverse ([Diagnosis] -> [Diagnosis]) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Sign f e -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
envDiags Sign f e
accSig
        sents :: [Named (FORMULA f)]
sents = [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a]
reverse ([Named (FORMULA f)] -> [Named (FORMULA f)])
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> [Named (FORMULA f)]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences Sign f e
accSig
        cleanSig :: Sign f e
cleanSig = (e -> Sign f e
forall e f. e -> Sign f e
emptySign (e -> Sign f e) -> e -> Sign f e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
accSig)
                   { emptySortSet :: Set SORT
emptySortSet = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
accSig
                   , sortRel :: Rel SORT
sortRel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
accSig
                   , opMap :: OpMap
opMap = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
accSig
                   , assocOps :: OpMap
assocOps = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
assocOps Sign f e
accSig
                   , predMap :: MapSet SORT PredType
predMap = Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign f e
accSig
                   , annoMap :: AnnoMap
annoMap = Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
accSig
                   , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
ga }
    in [Diagnosis]
-> Maybe
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ Sign f e -> [Named (FORMULA f)] -> [Diagnosis]
forall f e. Sign f e -> [Named (FORMULA f)] -> [Diagnosis]
warnUnused Sign f e
accSig [Named (FORMULA f)]
sents) (Maybe
   (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
 -> Result
      (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)]))
-> Maybe
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
forall a b. (a -> b) -> a -> b
$
       (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
-> Maybe
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
forall a. a -> Maybe a
Just (BASIC_SPEC b s f
newBs, Sign f e -> Set Symbol -> ExtSign (Sign f e) Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign f e
forall f. Sign f e
cleanSig (Set Symbol -> ExtSign (Sign f e) Symbol)
-> Set Symbol -> ExtSign (Sign f e) Symbol
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Symbol
forall f e. Sign f e -> Set Symbol
declaredSymbols Sign f e
accSig, [Named (FORMULA f)]
sents)

basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos)
  -> Result (BASIC_SPEC () () (),
             ExtSign (Sign () ()) Symbol,
             [Named (FORMULA ())])
basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos)
-> Result
     (BASIC_SPEC () () (), ExtSign (Sign () ()) Symbol,
      [Named (FORMULA ())])
basicCASLAnalysis = Min () ()
-> Ana () () () () ()
-> Ana () () () () ()
-> Mix () () () ()
-> (BASIC_SPEC () () (), Sign () (), GlobalAnnos)
-> Result
     (BASIC_SPEC () () (), ExtSign (Sign () ()) Symbol,
      [Named (FORMULA ())])
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 ((() -> Result ()) -> Min () ()
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return) ((() -> State (Sign () ()) ()) -> Ana () () () () ()
forall a b. a -> b -> a
const () -> State (Sign () ()) ()
forall (m :: * -> *) a. Monad m => a -> m a
return)
                                  ((() -> State (Sign () ()) ()) -> Ana () () () () ()
forall a b. a -> b -> a
const () -> State (Sign () ()) ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix () () () ()
forall b s f e. Mix b s f e
emptyMix

-- | extra
cASLsen_analysis ::
        (BASIC_SPEC () () (), Sign () (), FORMULA ()) -> Result (FORMULA ())
cASLsen_analysis :: (BASIC_SPEC () () (), Sign () (), FORMULA ())
-> Result (FORMULA ())
cASLsen_analysis (bs :: BASIC_SPEC () () ()
bs, s :: Sign () ()
s, f :: FORMULA ()
f) = let
                         mix :: Mix b s f e
mix = Mix b s f e
forall b s f e. Mix b s f e
emptyMix
                         allIds :: IdSets
allIds = [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$
                                (() -> IdSets) -> (() -> IdSets) -> BASIC_SPEC () () () -> IdSets
forall b s f.
(b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
ids_BASIC_SPEC (Mix () Any Any Any -> () -> IdSets
forall b s f e. Mix b s f e -> b -> IdSets
getBaseIds Mix () Any Any Any
forall b s f e. Mix b s f e
mix)
                                               (Mix Any () Any Any -> () -> IdSets
forall b s f e. Mix b s f e -> s -> IdSets
getSigIds Mix Any () Any Any
forall b s f e. Mix b s f e
mix) BASIC_SPEC () () ()
bs
                                IdSets -> [IdSets] -> [IdSets]
forall a. a -> [a] -> [a]
: Mix Any Any Any () -> () -> IdSets
forall b s f e. Mix b s f e -> e -> IdSets
getExtIds Mix Any Any Any ()
forall b s f e. Mix b s f e
mix (Sign () () -> ()
forall f e. Sign f e -> e
extendedInfo Sign () ()
s) IdSets -> [IdSets] -> [IdSets]
forall a. a -> [a] -> [a]
:
                                [Set SORT -> Set SORT -> Set SORT -> IdSets
mkIdSets (Sign () () -> Set SORT
forall f e. Sign f e -> Set SORT
allConstIds Sign () ()
s) (Sign () () -> Set SORT
forall f e. Sign f e -> Set SORT
allOpIds Sign () ()
s)
                                (Set SORT -> IdSets) -> Set SORT -> IdSets
forall a b. (a -> b) -> a -> b
$ Sign () () -> Set SORT
forall f e. Sign f e -> Set SORT
allPredIds Sign () ()
s]
                         mix' :: Mix b s f e
mix' = Mix b s f e
forall b s f e. Mix b s f e
mix { mixRules :: (TokRules, Rules)
mixRules = GlobalAnnos -> IdSets -> (TokRules, Rules)
makeRules GlobalAnnos
emptyGlobalAnnos
                                                           IdSets
allIds }
                         in ((FORMULA (), FORMULA ()) -> FORMULA ())
-> Result (FORMULA (), FORMULA ()) -> Result (FORMULA ())
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (FORMULA (), FORMULA ()) -> FORMULA ()
forall a b. (a, b) -> a
fst (Result (FORMULA (), FORMULA ()) -> Result (FORMULA ()))
-> Result (FORMULA (), FORMULA ()) -> Result (FORMULA ())
forall a b. (a -> b) -> a -> b
$ Min () ()
-> Mix Any Any () ()
-> Sign () ()
-> FORMULA ()
-> Result (FORMULA (), FORMULA ())
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> FORMULA f
-> Result (FORMULA f, FORMULA f)
anaForm ((() -> Result ()) -> Min () ()
forall a b. a -> b -> a
const () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix Any Any () ()
forall b s f e. Mix b s f e
mix' Sign () ()
s FORMULA ()
f