Description : CASL static analysis for basic specifications
Copyright : (c) Christian Maeder and Uni Bremen 2002-2005
Maintainer : Christian.Maeder@dfki.de
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
The formulas are returned with fully-qualified variables, operation
The static analysis functions are parameterized with functions for
treating CASL extensions, that is, additional basic items, signature
checkPlaces :: [SORT] -> Id -> [Diagnosis]
checkPlaces args i = let n = placeCount i in
[mkDiag Error "wrong number of places" i | n > 0 && n /= length args ]
checkWithVars :: String ->
Map.Map SIMPLE_ID a -> Id -> [Diagnosis]
checkWithVars s m i@(Id ts _ _) = if isSimpleId i then
Just _ -> alsoWarning s varS i
addOp :: Annoted a -> OpType -> Id -> State (Sign f e) ()
do checkSorts (opRes ty : opArgs ty)
ds = checkWithOtherMap opS predS (predMap e) i
++ checkWithVars opS (varMap e) i
(if
Set.member ty l then [mkDiag Hint "redeclared op" i]
else checkPlaces (opArgs ty) i ++ checkNamePrefix i)
store = put e { opMap = addOpTo i ty m }
Partial -> if
Set.member ty {opKind = Total} l then
addDiags $ mkDiag Warning "partially redeclared" i : ds
Total -> if
Set.member ty {opKind = Partial} l then do
addDiags $ mkDiag Hint "redeclared as total" i : ds
addAnnoSet a $ Symbol i $ OpAsItemType ty
addAssocOp :: OpType -> Id -> State (Sign f e) ()
put e { assocOps = addOpTo i ty $ assocOps e
, globAnnos = updAssocMap (addAssocId i) $ globAnnos e
updateExtInfo :: (e -> Result e) -> State (Sign f e) ()
let re = upd $ extendedInfo s
Just e -> put s { extendedInfo = e }
addPred :: Annoted a -> PredType -> Id -> State (Sign f e) ()
do checkSorts $ predArgs ty
ds = checkWithOtherMap predS opS (opMap e) i
++ checkWithVars predS (varMap e) i
addDiags $ mkDiag Hint "redeclared pred" i : ds
addDiags $ checkPlaces (predArgs ty) i ++ checkNamePrefix i ++ ds
addAnnoSet a $ Symbol i $ PredAsItemType ty
allOpIds = nonConsts . opMap
allConstIds :: Sign f e ->
Set.Set Id
allConstIds = opMapConsts . opMap
addAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
addAssocs e = updAssocMap (\ m -> foldr addAssocId m $
Map.keys $ assocOps e)
updAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
updAssocMap f ga = ga { assoc_annos = f $ assoc_annos ga }
addAssocId :: Id -> AssocMap -> AssocMap
formulaIds :: Sign f e ->
Set.Set Id
formulaIds e = let ops = allOpIds e in
allPredIds :: Sign f e ->
Set.Set Id
addSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
put e { sentences = reverse ds ++ sentences e }
-- * traversing all data types of the abstract syntax
ana_BASIC_SPEC :: (GetRange f, Pretty f, FreeVars 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 mef ab anas mix (Basic_spec al) = fmap Basic_spec $
mapAnM (ana_BASIC_ITEMS mef ab anas mix) al
-- looseness of a datatype
data GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)
unionGenAx :: [GenAx] -> GenAx
unionGenAx = foldr (\ (s1, r1, f1) (s2, r2, f2) ->
ana_BASIC_ITEMS :: (GetRange f, Pretty f, FreeVars f) => Min 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 ab anas mix bi =
Sig_items sis -> fmap Sig_items $
ana_SIG_ITEMS mef anas mix Loose sis
Free_datatype sk al ps ->
do mapM_ (\ i -> case item i of
Datatype_decl s _ _ -> addSort sk i s) al
mapAnM (ana_DATATYPE_DECL Free) al
toSortGenAx ps True $ getDataGenSig al
do (gs, ul) <- ana_Generated mef anas mix al
toSortGenAx ps False $ unionGenAx gs
Local_var_axioms il afs ps ->
put e { envDiags = vds } -- restore with shadowing warnings
let (es, resFs, anaFs) = foldr (\ f (dss, ress, ranas) ->
let Result ds m = anaForm mef mix sign $ item f
Nothing -> (ds ++ dss, ress, ranas)
(ds ++ dss, f {item = resF} : ress,
f {item = anaF} : ranas))
fufs = map (mapAn (\ f -> let
vs = map (\ (v, s) -> Var_decl [v] s ps)
in stripQuant sign $ mkForall vs qf ps))
sens = map makeNamedSen fufs
return $ Local_var_axioms il resFs ps
let (es, resFs, anaFs) = foldr (\ f (dss, ress, ranas) ->
let Result ds m = anaForm mef mix
Nothing -> (ds ++ dss, ress, ranas)
(ds ++ dss, f {item = resF} : ress,
f {item = anaF} : ranas))
fufs = map (mapAn (\ f -> let
vs = map (\ (v, s) -> Var_decl [v] s ps)
in stripQuant sign $ mkForall vs f ps)) anaFs
sens = map makeNamedSen fufs
return $ Axiom_items resFs ps
Ext_BASIC_ITEMS b -> fmap Ext_BASIC_ITEMS $ ab mix b
mapAn :: (a -> b) -> Annoted a -> Annoted b
mapAn f an = replaceAnnoted (f $ item an) an
toSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()
toSortGenAx ps isFree (sorts, rel, ops) = do
opSyms = map (\ c -> let ide = compId c in Qual_op_name ide
(toOP_TYPE $ compType c) $ posOfId ide) $
Set.toList ops
injSyms = map (\ (s, t) -> let p = posOfId s in
Qual_op_name (mkUniqueInjName s t)
allSyms = opSyms ++ injSyms
resType _ (Op_name _) = False
resType s (Qual_op_name _ t _) = res_OP_TYPE t == s
getIndex s = fromMaybe (-1) $ findIndex (== s) sortList
addIndices os@(Qual_op_name _ t _) =
(os, map getIndex $ args_OP_TYPE t)
Constraint s (map addIndices $ filter (resType s) allSyms) s
constrs = map collectOps sortList
resList =
Set.fromList $ map (\ (Qual_op_name _ t _) -> res_OP_TYPE t)
f = Sort_gen_ax constrs isFree
$ addDiags [Diag Error "missing generated sort" ps]
$ addDiags [mkDiag Warning "generated sorts without constructor"
$ addDiags [mkDiag Warning "non-generated sorts as constructor result"
addSentences [toSortGenNamed f sortList]
ana_SIG_ITEMS :: (GetRange f, Pretty 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 mef anas mix gk si =
do ul <- mapM (ana_SORT_ITEM mef mix sk) al
return $ Sort_items sk ul ps
do ul <- mapM (ana_OP_ITEM mef mix) al
do ul <- mapM (ana_PRED_ITEM mef mix) al
return $ Pred_items ul ps
Datatype_items sk al _ ->
do mapM_ (\ i -> case item i of
Datatype_decl s _ _ -> addSort sk i s) al
mapAnM (ana_DATATYPE_DECL gk) al
Ext_SIG_ITEMS s -> fmap Ext_SIG_ITEMS $ anas mix s
ana_Generated :: (GetRange f, Pretty 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 mef anas mix al = do
ul <- mapAnM (ana_SIG_ITEMS mef anas mix Generated) al
return (map (getGenSig . item) ul, ul)
getGenSig :: SIG_ITEMS s f -> GenAx
getGenSig si = case si of
Sort_items _ al _ -> unionGenAx $ map (getGenSorts . item) al
Datatype_items _ dl _ -> getDataGenSig dl
isPartAlt :: ALTERNATIVE -> Bool
Alt_construct p _ _ _ -> p == Partial
isConsAlt :: ALTERNATIVE -> Bool
getDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx
let alts = concatMap ((\ (Datatype_decl s al _) ->
map (\ a -> (s, item a)) al) . item) dl
(realAlts, subs) = partition (isConsAlt . snd) alts
let (i, ty, _) = getConsType s a
in Component i ty) realAlts
rel = foldr (\ (t, a) r ->
getGenSorts :: SORT_ITEM f -> GenAx
let (sorts, rel) = case si of
getOps :: OP_ITEM f ->
Set.Set Component
ana_SORT_ITEM :: (GetRange f, Pretty 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 mef mix sk asi =
do mapM_ (addSort sk asi) il
do mapM_ (addSort sk asi) (i : il)
Subsort_defn sub v super af ps ->
addVars (Var_decl [v] super ps)
let Result ds mf = anaForm mef mix sign $ item af
lab = if null lb then getRLabel asi else lb
Nothing -> return asi { item = Subsort_decl [sub] super ps}
addSentences [(makeNamed lab $
mkForall [Var_decl [v] super pv]
(Membership (Qual_var v super pv) sub p)
isAxiom = notImplied af }]
return asi { item = Subsort_defn sub v super
do mapM_ (addSort sk asi) il
_ : tl -> mapM_ (uncurry $ addSubsortOrIso False)
ana_OP_ITEM :: (GetRange f, Pretty f) => Min f e -> Mix b s f e
-> Annoted (OP_ITEM f) -> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM mef mix aoi =
mapM_ (addOp aoi oty) ops
ul <- mapM (ana_OP_ATTR mef mix oty ni ops) il
when (any (\ a -> case a of
mapM_ (addAssocOp oty) ops
when (any (\ a -> case a of
$ addSentences $ map (addLeftComm oty ni) ops
return aoi {item = Op_decl ops ty (catMaybes ul) ps}
do let ty = headToType ohd
lab = if null lb then getRLabel aoi else lb
vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args
arg = concatMap (\ (Var_decl v s qs) ->
map (\ j -> Qual_var j s qs) v) vs
addOp aoi (toOpType ty) i
let Result ds mt = anaTerm mef mix sign
(res_OP_TYPE ty) ps $ item at
Nothing -> return aoi { item = Op_decl [i] ty [] ps }
addSentences [(makeNamed lab $ mkForall vs
(Application (Qual_op_name i ty p) arg ps)
isAxiom = notImplied at, isDef = True }]
return aoi {item = Op_defn i ohd at { item = resT } ps }
headToType :: OP_HEAD -> OP_TYPE
headToType (Op_head k args r ps) = Op_type k (sortsOfArgs args) r ps
sortsOfArgs :: [ARG_DECL] -> [SORT]
sortsOfArgs = concatMap (\ (Arg_decl l s _) -> map (const s) l)
addLeftComm :: OpType -> Bool -> Id -> Named (FORMULA f)
ns = map mkSimpleId ["x", "y", "z"]
vs = map (\ v -> Var_decl [v] rty q) ns
[v1, v2, v3] = map (\ v -> Qual_var v rty q) ns
qi = Qual_op_name i sty p
in (makeNamed ("ga_left_comm_" ++ showId i "") $
(Application qi [v1, Application qi [v2, v3] p] p)
(Application qi [v2, Application qi [v1, v3] p] p) p) p)
ana_OP_ATTR :: (GetRange f, Pretty 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 mef mix ty ni ois oa = do
[t1, t2] | t1 == t2 -> case oa of
Comm_op_attr -> return ()
_ -> unless (t1 == rty) $ addDiags [Diag Error
"result sort must be equal to argument sorts" q]
_ -> addDiags [Diag Error
"expecting two arguments of equal sort" q]
let Result ds mt = anaTerm mef mix
Nothing -> return Nothing
addSentences $ map (makeUnit True anaT ty ni) ois
addSentences $ map (makeUnit False anaT ty ni) ois
return $ Just $ Unit_op_attr resT
let ns = map mkSimpleId ["x", "y", "z"]
vs = map (\ v -> Var_decl [v] rty q) ns
[v1, v2, v3] = map (\ v -> Qual_var v rty q) ns
makeAssoc i = let p = posOfId i
qi = Qual_op_name i sty p in
(makeNamed ("ga_assoc_" ++ showId i "") $
(Application qi [Application qi [v1, v2] p, v3] p)
(Application qi [v1, Application qi [v2, v3] p] p) p) p)
addSentences $ map makeAssoc ois
let ns = map mkSimpleId ["x", "y"]
vs = zipWith (\ v t -> Var_decl [v] t
$ concatMapRange posOfId atys) ns atys
makeComm i = let p = posOfId i
qi = Qual_op_name i sty p in
(makeNamed ("ga_comm_" ++ showId i "") $
(Application qi (reverse args) p) p) p) {
addSentences $ map makeComm ois
makeIdem i = let p = posOfId i in
(makeNamed ("ga_idem_" ++ showId i "") $
(Application (Qual_op_name i sty p) [qv, qv] p)
qv p) p) { isAxiom = ni }
addSentences $ map makeIdem ois
-- first bool for left and right, second one for no implied annotation
makeUnit :: Bool -> TERM f -> OpType -> Bool -> Id -> Named (FORMULA f)
let lab = "ga_" ++ (if b then "right" else "left") ++ "_unit_"
rargs = if b then args else reverse args
in (makeNamed lab $ mkForall [Var_decl [v] vty q]
(Application (Qual_op_name i (toOP_TYPE ty) p) rargs p)
ana_PRED_ITEM :: (GetRange f, Pretty f) => Min f e -> Mix b s f e
-> State (Sign f e) (Annoted (PRED_ITEM f))
ana_PRED_ITEM mef mix apr = case item apr of
Pred_decl preds ty _ -> do
mapM_ (addPred apr $ toPredType ty) preds
Pred_defn i phd@(Pred_head args rs) at ps -> do
lab = if null lb then getRLabel apr else lb
ty = Pred_type (sortsOfArgs args) rs
vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args
arg = concatMap (\ (Var_decl v s qs) ->
map (\ j -> Qual_var j s qs) v) vs
addPred apr (toPredType ty) i
let Result ds mt = anaForm mef mix sign $ item at
Nothing -> return apr {item = Pred_decl [i] ty ps}
addSentences [(makeNamed lab $
(Equivalence (Predication (Qual_pred_name i ty p)
return apr {item = Pred_defn i phd at { item = resF } ps}
-- full function type of a selector (result sort is component sort)
data Component = Component { compId :: Id, compType :: OpType } deriving Show
instance Eq Component where
Component i1 t1 == Component i2 t2 =
(i1, opArgs t1, opRes t1) == (i2, opArgs t2, opRes t2)
instance Ord Component where
Component i1 t1 <= Component i2 t2 =
(i1, opArgs t1, opRes t1) <= (i2, opArgs t2, opRes t2)
instance Pretty Component where
pretty (Component i ty) =
pretty i <+> colon <> pretty ty
instance GetRange Component where
getRange = getRange . compId
-- | return list of constructors
ana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
ana_DATATYPE_DECL gk (Datatype_decl s al _) =
do ul <- mapM (ana_ALTERNATIVE s) al
let constr = catMaybes ul
unless (null constr) $ do
addDiags $ checkUniqueness cs
wrongConstr = filter ((totalSels /=) . snd) constr
addDiags $ map (\ (c, _) -> mkDiag Warning
("total selectors '" ++ showSepList (showString ", ")
"'\n should be in alternative") c) wrongConstr
pfs = filter isPartAlt allts
(alts, subs) = partition isConsAlt allts
sbs = concatMap getAltSubsorts subs
comps = map (getConsType s) alts
ttrips = map ((\ (a, vs, t, ses) -> (a, vs, t, catSels ses))
sels = concatMap (\ (_, _, _, ses) -> ses) ttrips
addDiags $ map (\ (Alt_construct _ i _ _) -> mkDiag Error
"illegal free partial constructor" i) pfs
addSentences $ map makeInjective
$ filter (\ (_, _, ces) -> not $ null ces)
addSentences $ makeDisjSubsorts s sbs
addSentences $ concatMap (\ c -> map (makeDisjToSort c) sbs)
addSentences $ makeDisjoint comps
addSentences $ catMaybes $ concatMap
map (makeUndefForm ses) ttrips) sels
makeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts d subs = case subs of
s : rs -> map (makeDisjSubsort s) rs ++ makeDisjSubsorts d rs
makeDisjSubsort :: SORT -> SORT -> Named (FORMULA f)
makeDisjSubsort s1 s2 = let
p = pd `appRange` p1 `appRange` p2
in makeNamed ("ga_disjoint_sorts_" ++ showId s1 "_" ++ showId s2 "")
$ mkForall [v] (Negation (Conjunction [
Membership qv s1 p1, Membership qv s2 p2] p) p) p
makeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
let (c, v, t, _) = selForms1 "X" a
in makeNamed ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "")
$ mkForall v (Negation (Membership t s p) p) p
makeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)
let (c, v1, t1, _) = selForms1 "X" a
(_, v2, t2, _) = selForms1 "Y" a
in makeNamed ("ga_injective_" ++ showId c "")
(Equivalence (Strong_equation t1 t2 p)
(let ces = zipWith (\ w1 w2 -> Strong_equation
(toQualVar w1) (toQualVar w2) p) v1 v2
in if isSingle ces then head ces else Conjunction ces p)
makeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint l = case l of
c : cs -> map (makeDisj c) cs ++ makeDisjoint cs
makeDisj :: (Id, OpType, [COMPONENTS]) -> (Id, OpType, [COMPONENTS])
let (c1, v1, t1, _) = selForms1 "X" a1
(c2, v2, t2, _) = selForms1 "Y" a2
p = posOfId c1 `appRange` posOfId c2
in makeNamed ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "")
$ mkForall (v1 ++ v2) (Negation (Strong_equation t1 t2 p) p) p
catSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]
catSels = map (\ (m, t) -> (fromJust m, t)) .
filter (\ (m, _) -> isJust m)
makeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)])
-> Maybe (Named (FORMULA f))
makeUndefForm (s, ty) (i, vs, t, sels) =
if any (\ (se, ts) -> s == se && opRes ts == opRes ty ) sels
Just $ makeNamed ("ga_selector_undef_" ++ showId s "_" ++ showId i "")
(Application (Qual_op_name s (toOP_TYPE ty) p) [t] p)
getAltSubsorts :: ALTERNATIVE -> [SORT]
getAltSubsorts c = case c of
getConsType :: SORT -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])
let getConsTypeAux (part, i, il) =
(i, OpType part (concatMap
(map (opRes . snd) . getCompType s) il) s, il)
Subsorts _ _ -> error "getConsType"
Alt_construct k a l _ -> getConsTypeAux (k, a, l)
getCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]
getCompType s c = case c of
Cons_select k l cs _ -> map (\ i -> (Just i, OpType k [s] cs)) l
Sort cs -> [(Nothing, OpType Partial [s] cs)]
genSelVars :: String -> Int -> [OpType] -> [VAR_DECL]
genSelVars str n tys = case tys of
ty : rs -> Var_decl [mkNumVar str n] (opRes ty) nullRange
: genSelVars str (n + 1) rs
makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
makeSelForms n (i, vs, t, tys) = case tys of
Just j -> let p = posOfId j
[makeNamed ("ga_selector_" ++ showId j "")
(Application (Qual_op_name j (toOP_TYPE ty) p) [t] p)
(Qual_var (mkNumVar "X" n) rty q) p) p]
) ++ makeSelForms (n + 1) (i, vs, t, rs)
selForms1 :: String -> (Id, OpType, [COMPONENTS])
-> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
selForms1 str (i, ty, il) =
let cs = concatMap (getCompType (opRes ty)) il
vs = genSelVars str 1 $ map snd cs
in (i, vs, Application (Qual_op_name i (toOP_TYPE ty) nullRange)
(map toQualVar vs) nullRange, cs)
selForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
selForms = makeSelForms 1 . 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 s c = case item c of
let cons@(i, ty, il) = getConsType s ic
ul <- mapM (ana_COMPONENTS s) il
let ts = concatMap fst ul
addDiags $ checkUniqueness (ts ++ concatMap snd ul)
addSentences $ selForms cons
-- | return total and partial selectors
ana_COMPONENTS :: SORT -> COMPONENTS
-> State (Sign f e) ([Component], [Component])
sels <- mapM (\ (mi, ty) ->
Nothing -> return Nothing
addOp (emptyAnno ()) ty i
return $ Just $ Component i ty) cs
return $ partition ((== Total) . opKind . compType) $ catMaybes sels
resultToState :: (a -> Result a) -> a -> State (Sign f e) a
-- 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 :: (GetRange f, Pretty f) => Min f e -> Mix b s f e -> Sign f e
-> FORMULA f -> Result (FORMULA f, FORMULA f)
anaForm mef mixIn sign f = do
resF <- resolveFormula (putParen mix) (mixResolve mix)
(globAnnos sign) (mixRules mix) f
anaF <- minExpFORMULA mef sign resF
anaTerm :: (GetRange f, Pretty f) => Min f e -> Mix b s f e -> Sign f e
-> SORT -> Range -> TERM f -> Result (TERM f, TERM f)
anaTerm mef mixIn sign srt pos t = do
resT <- resolveMixfix (putParen mix) (mixResolve mix)
(globAnnos sign) (mixRules mix) t
anaT <- oneExpTerm mef sign $ Sorted_term resT srt pos
basicAnalysis :: (GetRange f, Pretty f, FreeVars 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 mef anab anas mix (bs, inSig, ga) =
let allIds = unite $ ids_BASIC_SPEC (getBaseIds mix) (getSigIds mix) bs
: getExtIds mix (extendedInfo inSig) :
[mkIdSets (allConstIds inSig) (allOpIds inSig)
(newBs, accSig) = runState (ana_BASIC_SPEC mef anab anas
mix { mixRules = makeRules ga allIds }
bs) inSig { globAnnos = addAssocs inSig ga }
ds = reverse $ envDiags accSig
sents = reverse $ sentences accSig
cleanSig = (emptySign $ extendedInfo accSig)
{ sortSet = sortSet accSig
, emptySortSet = emptySortSet accSig
, assocOps = assocOps accSig
, predMap = predMap accSig
in Result (ds ++ warnUnused accSig sents) $
Just (newBs, ExtSign cleanSig $ declaredSymbols accSig, sents)
basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos)
-> Result (BASIC_SPEC () () (),
ExtSign (Sign () ()) Symbol,
basicAnalysis (const return) (const return) (const return) emptyMix