a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett{- |

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettModule : $Header$

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettMaintainer : hets@tzi.de

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCASL static analysis for basic specifications

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

78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- todo: correct implementation of variables

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach (shadowing instead of overloading)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettmodule CASL.StaticAna where

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettimport CASL.AS_Basic_CASL

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport CASL.Sign

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettimport CASL.MixfixParser

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettimport CASL.Overload

ae930b77ed60580110b52a09456d651f9b841883Andy Gimblettimport CASL.Inject

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettimport CASL.Utils

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettimport Common.Lib.State

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.PrettyPrint

ae930b77ed60580110b52a09456d651f9b841883Andy Gimblettimport Common.Lib.Pretty

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport qualified Common.Lib.Map as Map

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.Set as Set

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Id

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederimport Common.AS_Annotation

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Common.GlobalAnnotations

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettimport Common.Result

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Data.Maybe

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport Data.List

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettimport Control.Exception (assert)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettcheckPlaces :: [SORT] -> Id -> [Diagnosis]

06dd4e7c29f33f6122a910719e3bd9062256e397Andy GimblettcheckPlaces args i =

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett if let n = placeCount i in n == 0 || n == length args then []

c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett else [mkDiag Error "wrong number of places" i]

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'ReillyaddOp :: OpType -> Id -> State (Sign f e) ()

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederaddOp ty i =

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder do checkSorts (opRes ty : opArgs ty)

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder e <- get

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder let m = opMap e

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder l = Map.findWithDefault Set.empty i m

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder check = addDiags $ checkPlaces (opArgs ty) i

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder store = do put e { opMap = addOpTo i ty m }

a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly if Set.member ty l then

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett addDiags [mkDiag Hint "redeclared op" i]

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett else case opKind ty of

7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Partial -> if Set.member ty {opKind = Total} l then

7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett addDiags [mkDiag Warning "partially redeclared" i]

7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett else store >> check

7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Total -> do store

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett if Set.member ty {opKind = Partial} l then

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett addDiags [mkDiag Hint "redeclared as total" i]

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett else check

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettaddAssocOp :: OpType -> Id -> State (Sign f e) ()

e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettaddAssocOp ty i = do

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett e <- get

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett put e { assocOps = addOpTo i ty $ assocOps e }

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettupdateExtInfo :: (e -> Result e) -> State (Sign f e) ()

e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettupdateExtInfo upd = do

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett s <- get

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let re = upd $ extendedInfo s

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett case maybeResult re of

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Nothing -> return ()

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Just e -> put s { extendedInfo = e }

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett addDiags $ diags re

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy GimblettaddOpTo :: Id -> OpType -> OpMap -> OpMap

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettaddOpTo k v m =

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let l = Map.findWithDefault Set.empty k m

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett n = Map.insert k (Set.insert v l) m

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett in case opKind v of

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Total -> let vp = v { opKind = Partial } in

fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett if Set.member vp l then

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Map.insert k (Set.insert v $ Set.delete vp l) m

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett else n

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett _ -> if Set.member v { opKind = Total } l then m

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett else n

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

820947bd01ca952c3909eaa0366c6914c87cc1cbTill MossakowskiaddPred :: PredType -> Id -> State (Sign f e) ()

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettaddPred ty i =

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett do checkSorts $ predArgs ty

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett e <- get

fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett let m = predMap e

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett l = Map.findWithDefault Set.empty i m

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett if Set.member ty l then

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett addDiags [mkDiag Hint "redeclared pred" i]

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett else do put e { predMap = Map.setInsert i ty m }

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett addDiags $ checkPlaces (predArgs ty) i

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettallOpIds :: Sign f e -> Set.Set Id

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettallOpIds = Set.fromDistinctAscList . Map.keys . opMap

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettaddAssocs :: GlobalAnnos -> Sign f e -> GlobalAnnos

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettaddAssocs ga e =

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ga { assoc_annos =

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett foldr ( \ i m -> case Map.lookup i m of

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Nothing -> Map.insert i ALeft m

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett _ -> m ) (assoc_annos ga) (Map.keys $ assocOps e) }

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettformulaIds :: Sign f e -> Set.Set Id

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettformulaIds e = let ops = allOpIds e in

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Set.fromDistinctAscList (map simpleIdToId $ Map.keys $ varMap e)

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett `Set.union` ops

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettallPredIds :: Sign f e -> Set.Set Id

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachallPredIds = Set.fromDistinctAscList . Map.keys . predMap

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett

e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettaddSentences :: [Named (FORMULA f)] -> State (Sign f e) ()

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettaddSentences ds =

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett do e <- get

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett put e { sentences = reverse ds ++ sentences e }

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- * traversing all data types of the abstract syntax

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettana_BASIC_SPEC :: Resolver f => Min f e

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> Ana b f e -> Ana s f e -> GlobalAnnos

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> BASIC_SPEC b s f -> State (Sign f e) (BASIC_SPEC b s f)

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettana_BASIC_SPEC mef ab as ga (Basic_spec al) = fmap Basic_spec $

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett mapAnM (ana_BASIC_ITEMS mef ab as ga) al

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- looseness of a datatype

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettdata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett

31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettmkForall :: [VAR_DECL] -> FORMULA f -> [Pos] -> FORMULA f

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmkForall vl f ps = if null vl then f else

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Quantification Universal vl f ps

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettana_BASIC_ITEMS :: Resolver f => Min f e

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -> Ana b f e -> Ana s f e -> GlobalAnnos

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett -> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettana_BASIC_ITEMS mef ab as ga bi =

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett case bi of

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Sig_items sis -> fmap Sig_items $

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ana_SIG_ITEMS mef as ga Loose sis

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Free_datatype al ps ->

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett mapM_ addSort sorts

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett mapAnM (ana_DATATYPE_DECL Free) al

7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett toSortGenAx ps True $ getDataGenSig al

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett closeSubsortRel

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return bi

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Sort_gen al ps ->

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do (gs,ul) <- ana_Generated mef as ga al

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett toSortGenAx ps False

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (Set.unions $ map fst gs, Set.unions $ map snd gs)

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett return $ Sort_gen ul ps

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett Var_items il _ ->

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett do mapM_ addVars il

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett return bi

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Local_var_axioms il afs ps ->

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett do e <- get -- save

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett mapM_ addVars il

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett sign <- get

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett put e -- restore

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett let preds = allPredIds sign

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett ops = formulaIds sign

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett newGa = addAssocs ga sign

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett rfs = map (anaForm mef newGa ops preds sign . item) afs

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett ds = concatMap diags rfs

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett arfs = zipWith ( \ a m -> case maybeResult m of

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett Nothing -> Nothing

7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Just f -> Just a { item = f }) afs rfs

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett ufs = catMaybes arfs

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett fufs = map ( \ a -> a { item = mkForall il

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (item a) ps } ) ufs

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett sens = map ( \ a -> NamedSen (getRLabel a) $ item a) fufs

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett addDiags ds

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett addSentences sens

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett return $ Local_var_axioms il ufs ps

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Axiom_items afs ps ->

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett do sign <- get

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett ops <- gets formulaIds

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett preds <- gets allPredIds

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett newGa <- gets $ addAssocs ga

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let rfs = map (anaForm mef newGa ops preds sign . item) afs

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett ds = concatMap diags rfs

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett arfs = zipWith ( \ a m -> case maybeResult m of

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Nothing -> Nothing

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Just f -> Just a { item = f }) afs rfs

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett ufs = catMaybes arfs

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett sens = map ( \ a -> NamedSen (getRLabel a) $ item a) ufs

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett addDiags ds

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett addSentences sens

fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett return $ Axiom_items ufs ps

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Ext_BASIC_ITEMS b -> fmap Ext_BASIC_ITEMS $ ab ga b

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimbletttoSortGenAx :: [Pos] -> Bool ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (Set.Set Id, Set.Set Component) -> State (Sign f e) ()

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimbletttoSortGenAx ps isFree (sorts, ops) = do

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let sortList = Set.toList sorts

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett opSyms = map ( \ c -> Qual_op_name (compId c)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (toOP_TYPE $ compType c) []) $ Set.toList ops

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett resType _ (Op_name _) = False

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett resType s (Qual_op_name _ t _) = res_OP_TYPE t ==s

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett getIndex s = maybe (-1) id $ findIndex (==s) sortList

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett addIndices (Op_name _) =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett error "CASL/StaticAna: Internal error in function addIndices"

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett addIndices os@(Qual_op_name _ t _) =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (os,map getIndex $ args_OP_TYPE t)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett collectOps s =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Constraint s (map addIndices $ filter (resType s) opSyms) s

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett constrs = map collectOps sortList

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett f = Sort_gen_ax constrs isFree

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett if null sortList then

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett addDiags[Diag Error "missing generated sort" (headPos ps)]

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett else return ()

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett addSentences [NamedSen ("ga_generated_" ++

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett showSepList (showString "_") showId sortList "") f]

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettana_SIG_ITEMS :: Resolver f => Min f e

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> Ana s f e -> GlobalAnnos -> GenKind

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> SIG_ITEMS s f -> State (Sign f e) (SIG_ITEMS s f)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettana_SIG_ITEMS mef as ga gk si =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case si of

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Sort_items al ps ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do ul <- mapM (ana_SORT_ITEM mef ga) al

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett closeSubsortRel

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett return $ Sort_items ul ps

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Op_items al ps ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do ul <- mapM (ana_OP_ITEM mef ga) al

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett return $ Op_items ul ps

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Pred_items al ps ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do ul <- mapM (ana_PRED_ITEM mef ga) al

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett return $ Pred_items ul ps

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Datatype_items al _ ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do let sorts = map (( \ (Datatype_decl s _ _) -> s) . item) al

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett mapM_ addSort sorts

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett mapAnM (ana_DATATYPE_DECL gk) al

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett closeSubsortRel

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett return si

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Ext_SIG_ITEMS s -> fmap Ext_SIG_ITEMS $ as ga s

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- helper

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettana_Generated :: Resolver f => Min f e

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> Ana s f e -> GlobalAnnos -> [Annoted (SIG_ITEMS s f)]

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> State (Sign f e)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ([(Set.Set Id, Set.Set Component)],[Annoted (SIG_ITEMS s f)])

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettana_Generated mef as ga al = do

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ul <- mapAnM (ana_SIG_ITEMS mef as ga Generated) al

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett return (map (getGenSig . item) ul, ul)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetGenSig :: SIG_ITEMS s f -> (Set.Set Id, Set.Set Component)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetGenSig si = case si of

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Sort_items al _ -> (Set.unions (map (getSorts . item) al), Set.empty)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Op_items al _ -> (Set.empty, Set.unions (map (getOps . item) al))

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Datatype_items dl _ -> getDataGenSig dl

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett _ -> (Set.empty, Set.empty)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetDataGenSig :: [Annoted DATATYPE_DECL] -> (Set.Set Id, Set.Set Component)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetDataGenSig dl =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let alts = map (( \ (Datatype_decl s al _) -> (s, al)) . item) dl

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sorts = map fst alts

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett mkComponent (i, ty, _) = Component i ty

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett cs = concatMap ( \ (s, al) -> concatMap (( \ a ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett map mkComponent (getConsType s a)))

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett $ map item al) alts

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett in (Set.fromList sorts, Set.fromList cs)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetSorts :: SORT_ITEM f -> Set.Set Id

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetSorts si =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case si of

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Sort_decl il _ -> Set.fromList il

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Subsort_decl il i _ -> Set.fromList (i:il)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Subsort_defn sub _ _ _ _ -> Set.single sub

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Iso_decl il _ -> Set.fromList il

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetOps :: OP_ITEM f -> Set.Set Component

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetOps oi = case oi of

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Op_decl is ty _ _ ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Set.fromList $ map ( \ i -> Component i $ toOpType ty) is

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Op_defn i par _ _ -> Set.single $ Component i $ toOpType $ headToType par

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettana_SORT_ITEM :: Resolver f => Min f e

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -> GlobalAnnos -> Annoted (SORT_ITEM f)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett -> State (Sign f e) (Annoted (SORT_ITEM f))

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettana_SORT_ITEM mef ga asi =

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case item asi of

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Sort_decl il _ ->

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett do mapM_ addSort il

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett return asi

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Subsort_decl il i _ ->

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett do mapM_ addSort (i:il)

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett mapM_ (addSubsort i) il

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return asi

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett Subsort_defn sub v super af ps ->

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett do e <- get -- save

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett put e { varMap = Map.empty }

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett addVars (Var_decl [v] super ps)

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett sign <- get

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett ops <- gets formulaIds

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett preds <- gets allPredIds

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett newGa <- gets $ addAssocs ga

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett put e -- restore

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett let Result ds mf = anaForm mef newGa ops preds sign $ item af

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett lb = getRLabel af

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett lab = if null lb then getRLabel asi else lb

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett addDiags ds

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett addSort sub

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett addSubsort super sub

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett case mf of

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett Nothing -> return asi { item = Subsort_decl [sub] super ps}

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett Just f -> do

7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett let p = [posOfId sub]

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett pv = [tokPos v]

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett addSentences[NamedSen lab $

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett mkForall [Var_decl [v] super pv]

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (Equivalence

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (Membership (Qual_var v super pv) sub p)

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett f p) p]

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett return asi { item = Subsort_defn sub v super af { item = f } ps}

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Iso_decl il _ ->

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett do mapM_ addSort il

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett mapM_ ( \ i -> mapM_ (addSubsort i) il) il

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return asi

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettana_OP_ITEM :: Resolver f => Min f e -> GlobalAnnos -> Annoted (OP_ITEM f)

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -> State (Sign f e) (Annoted (OP_ITEM f))

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblettana_OP_ITEM mef ga aoi =

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett case item aoi of

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Op_decl ops ty il ps ->

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett do let oty = toOpType ty

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett mapM_ (addOp oty) ops

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett ul <- mapM (ana_OP_ATTR mef ga oty ops) il

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett if null $ filter ( \ i -> case i of

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Assoc_op_attr -> True

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett _ -> False) il

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett then return ()

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett else mapM_ (addAssocOp oty) ops

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett return aoi {item = Op_decl ops ty (catMaybes ul) ps}

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Op_defn i ohd at ps ->

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett do let ty = headToType ohd

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett lb = getRLabel at

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett lab = if null lb then getRLabel aoi else lb

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett args = case ohd of

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Op_head _ as _ _ -> as

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett arg = concatMap ( \ (Var_decl v s qs) ->

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett map ( \ j -> Qual_var j s qs) v) vs

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett addOp (toOpType ty) i

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett e <- get -- save

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett put e { varMap = Map.empty }

fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett mapM_ addVars vs

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sign <- get

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett ops <- gets formulaIds

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett preds <- gets allPredIds

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett newGa <- gets $ addAssocs ga

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett put e -- restore

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett let Result ds mt = anaTerm mef newGa ops preds sign $

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Sorted_term (item at) (res_OP_TYPE ty) ps

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett addDiags ds

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett case mt of

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett Nothing -> return aoi { item = Op_decl [i] ty [] ps }

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Just t -> do let p = [posOfId i]

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett addSentences [NamedSen lab $

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett mkForall vs

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (Strong_equation

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (Application (Qual_op_name i ty p) arg ps)

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett t p) ps]

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett return aoi {item = Op_defn i ohd at { item = t } ps }

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettheadToType :: OP_HEAD -> OP_TYPE

9582375827616730f146b77f9d5a4fd0cc78bc47Andy GimblettheadToType (Op_head k args r ps) = Op_type k (sortsOfArgs args) r ps

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

9582375827616730f146b77f9d5a4fd0cc78bc47Andy GimblettsortsOfArgs :: [ARG_DECL] -> [SORT]

a731366827a80af216ce6bfd4aa6388260577791Andy GimblettsortsOfArgs = concatMap ( \ (Arg_decl l s _) -> map (const s) l)

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblettana_OP_ATTR :: Resolver f => Min f e -> GlobalAnnos

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett -> OpType -> [Id] -> (OP_ATTR f)

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett -> State (Sign f e) (Maybe (OP_ATTR f))

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettana_OP_ATTR mef ga ty ois oa =

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett let sty = toOP_TYPE ty

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett rty = opRes ty

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett q = [posOfId rty] in

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett case oa of

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Unit_op_attr t ->

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett do sign <- get

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett ops <- gets allOpIds

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett preds <- gets allPredIds

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett newGa <- gets $ addAssocs ga

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett let Result ds mt = anaTerm mef newGa ops preds sign

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (Sorted_term t rty q)

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett addDiags ds

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett case mt of

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Nothing -> return Nothing

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Just e -> do

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett addSentences $ map (makeUnit True e ty) ois

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett addSentences $ map (makeUnit False e ty) ois

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return $ Just $ Unit_op_attr e

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Assoc_op_attr -> do

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let ns = map mkSimpleId ["x", "y", "z"]

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett vs = map ( \ v -> Var_decl [v] rty q) ns

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett [v1, v2, v3] = map ( \ v -> Qual_var v rty q) ns

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett makeAssoc i = let p = [posOfId i]

9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett qi = Qual_op_name i sty p in

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett NamedSen ("ga_assoc_" ++ showId i "") $

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett mkForall vs

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett (Strong_equation

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett (Application qi [v1, Application qi [v2, v3] p] p)

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett (Application qi [Application qi [v1, v2] p, v3] p) p) p

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett addSentences $ map makeAssoc ois

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett return $ Just oa

adce8375991a372444ab995895442dca6faf9677Andy Gimblett Comm_op_attr -> do

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett let ns = map mkSimpleId ["x", "y"]

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett atys = opArgs ty

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett vs = zipWith ( \ v t -> Var_decl [v] t (map posOfId atys) ) ns atys

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett args = map toQualVar vs

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett makeComm i = let p = [posOfId i]

a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett qi = Qual_op_name i sty p in

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett NamedSen ("ga_comm_" ++ showId i "") $

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett mkForall vs

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett (Strong_equation

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (Application qi args p)

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (Application qi (reverse args) p) p) p

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett case atys of

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett [_,_] -> addSentences $ map makeComm ois

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett _ -> addDiags [Diag Error "expecting two arguments for commutativity"

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett $ posOfId rty]

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return $ Just oa

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Idem_op_attr -> do

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett let v = mkSimpleId "x"

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett vd = Var_decl [v] rty q

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett qv = toQualVar vd

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett makeIdem i = let p = [posOfId i] in

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett NamedSen ("ga_idem_" ++ showId i "") $

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett mkForall [vd]

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (Strong_equation

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (Application (Qual_op_name i sty p) [qv, qv] p)

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett qv p) p

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett addSentences $ map makeIdem ois

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return $ Just oa

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett

c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettmakeUnit :: Bool -> TERM f -> OpType -> Id -> Named (FORMULA f)

c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettmakeUnit b t ty i =

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett let lab = "ga_" ++ (if b then "right" else "left") ++ "_unit_"

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ++ showId i ""

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett v = mkSimpleId "x"

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett vty = opRes ty

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett q = [posOfId vty]

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett p = [posOfId i]

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett qv = Qual_var v vty q

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett args = [qv, t]

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett rargs = if b then args else reverse args

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett in NamedSen lab $ mkForall [Var_decl [v] vty q]

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (Strong_equation

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (Application (Qual_op_name i (toOP_TYPE ty) p) rargs p)

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett qv p) p

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblettana_PRED_ITEM :: Resolver f => Min f e

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett -> GlobalAnnos -> Annoted (PRED_ITEM f)

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -> State (Sign f e) (Annoted (PRED_ITEM f))

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettana_PRED_ITEM mef ga ap =

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett case item ap of

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Pred_decl preds ty _ ->

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett do mapM (addPred $ toPredType ty) preds

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return ap

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett Pred_defn i phd@(Pred_head args rs) at ps ->

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett do let lb = getRLabel at

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett lab = if null lb then getRLabel ap else lb

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett ty = Pred_type (sortsOfArgs args) rs

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett vs = map (\ (Arg_decl v s qs) -> (Var_decl v s qs)) args

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett arg = concatMap ( \ (Var_decl v s qs) ->

c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett map ( \ j -> Qual_var j s qs) v) vs

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett addPred (toPredType ty) i

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett e <- get -- save

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett put e { varMap = Map.empty }

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett mapM_ addVars vs

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett sign <- get

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett ops <- gets formulaIds

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett preds <- gets allPredIds

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett newGa <- gets $ addAssocs ga

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett put e -- restore

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett let Result ds mt = anaForm mef newGa ops preds sign $ item at

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett addDiags ds

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett case mt of

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Nothing -> return ap {item = Pred_decl [i] ty ps}

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett Just t -> do

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett let p = [posOfId i]

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett addSentences [NamedSen lab $

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett mkForall vs

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (Equivalence (Predication (Qual_pred_name i ty p)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett arg p) t p) p]

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett return ap {item = Pred_defn i phd at { item = t } ps}

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett-- full function type of a selector (result sort is component sort)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettdata Component = Component { compId :: Id, compType :: OpType }

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett deriving (Show)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance Eq Component where

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Component i1 t1 == Component i2 t2 =

c909c215242232fe78ce335e677e6f22264a0ee9Christian Maeder (i1, opArgs t1, opRes t1) == (i2, opArgs t2, opRes t2)

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance Ord Component where

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Component i1 t1 <= Component i2 t2 =

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (i1, opArgs t1, opRes t1) <= (i2, opArgs t2, opRes t2)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PrettyPrint Component where

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printText0 ga (Component i ty) =

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett printText0 ga i <+> colon <> printText0 ga ty

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettinstance PosItem Component where

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett get_pos = Just . posOfId . compId

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | return list of constructors

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettana_DATATYPE_DECL gk (Datatype_decl s al _) =

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett do ul <- mapM (ana_ALTERNATIVE s . item) al

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett let constr = catMaybes ul

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett cs = map fst constr

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett if null constr then return ()

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett else do addDiags $ checkUniqueness cs

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett let totalSels = Set.unions $ map snd constr

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett wrongConstr = filter ((totalSels /=) . snd) constr

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett addDiags $ map ( \ (c, _) -> mkDiag Error

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett ("total selectors '" ++ showSepList (showString ",")

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett showPretty (Set.toList totalSels)

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett "'\n must appear in alternative") c) wrongConstr

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett case gk of

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Free -> do

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett let allts = map item al

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett (alts, subs) = partition ( \ a -> case a of

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett Subsorts _ _ -> False

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett _ -> True) allts

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett sbs = concatMap ( \ (Subsorts ss _) -> ss) subs

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett comps = concatMap (getConsType s) alts

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ttrips = map (( \ (a, vs, t, ses) -> (a, vs, t, catSels ses))

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett . selForms1 "X" ) comps

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett sels = concatMap ( \ (_, _, _, ses) -> ses) ttrips

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett addSentences $ map makeInjective

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett $ filter ( \ (_, _, ces) -> not $ null ces)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett comps

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett addSentences $ concatMap ( \ as -> map (makeDisjToSort as) sbs)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett comps

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett addSentences $ makeDisjoint comps

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett addSentences $ catMaybes $ concatMap

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ( \ ses ->

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett map (makeUndefForm ses) ttrips) sels

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett _ -> return ()

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett return cs

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisjToSort a s =

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett let (c, v, t, _) = selForms1 "X" a

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett p = [posOfId s] in

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett NamedSen ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "") $

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett mkForall v (Negation (Membership t s p) p) p

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeInjective a =

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett let (c, v1, t1, _) = selForms1 "X" a

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (_, v2, t2, _) = selForms1 "Y" a

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett p = [posOfId c]

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett in NamedSen ("ga_injective_" ++ showId c "") $

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett mkForall (v1 ++ v2)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (Equivalence (Strong_equation t1 t2 p)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (let ces = zipWith ( \ w1 w2 -> Strong_equation

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (toQualVar w1) (toQualVar w2) p) v1 v2

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett in if isSingle ces then head ces else Conjunction ces p)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett p) p

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisjoint [] = []

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisjoint (a:as) = map (makeDisj a) as ++ makeDisjoint as

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisj :: (Id, OpType, [COMPONENTS])

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -> (Id, OpType, [COMPONENTS])

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -> Named (FORMULA f)

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeDisj a1 a2 =

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett let (c1, v1, t1, _) = selForms1 "X" a1

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (c2, v2, t2, _) = selForms1 "Y" a2

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett p = [posOfId c1, posOfId c2]

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett in NamedSen ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "") $

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett mkForall (v1 ++ v2)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (Negation (Strong_equation t1 t2 p) p) p

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettcatSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettcatSels = map ( \ (m, t) -> (fromJust m, t)) .

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett filter ( \ (m, _) -> isJust m)

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett

5b5db1d788d5240070930175f1322dab56279f99Andy GimblettmakeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)])

-> Maybe (Named (FORMULA f))

makeUndefForm (s, ty) (i, vs, t, sels) =

let p = [posOfId s] in

if any ( \ (se, ts) -> s == se && opRes ts == opRes ty ) sels

then Nothing else

Just $ NamedSen ("ga_selector_undef_" ++ showId s "_"

++ showId i "") $

mkForall vs

(Negation

(Definedness

(Application (Qual_op_name s (toOP_TYPE ty) p) [t] p)

p) p) p

getConsType :: SORT -> ALTERNATIVE -> [(Id, OpType, [COMPONENTS])]

getConsType s c =

let getConsTypeAux (part, i, il) =

(i, OpType part (concatMap

(map (opRes . snd) . getCompType s) il) s, il)

in case c of

Subsorts srts _ ->

[(injName, OpType Total [s1] s,[Sort s1]) | s1<-srts]

Alt_construct k a l _ -> [getConsTypeAux (k, a, l)]

getCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]

getCompType s (Cons_select k l cs _) =

map (\ i -> (Just i, OpType k [s] cs)) l

getCompType s (Sort cs) = [(Nothing, OpType Partial [s] cs)]

genSelVars :: String -> Int -> [(Maybe Id, OpType)] -> [VAR_DECL]

genSelVars _ _ [] = []

genSelVars str n ((_, ty):rs) =

Var_decl [mkSelVar str n] (opRes ty) [] : genSelVars str (n+1) rs

mkSelVar :: String -> Int -> Token

mkSelVar str n = mkSimpleId (str ++ show n)

makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])

-> [Named (FORMULA f)]

makeSelForms _ (_, _, _, []) = []

makeSelForms n (i, vs, t, (mi, ty):rs) =

(case mi of

Nothing -> []

Just j -> let p = [posOfId j]

rty = opRes ty

q = [posOfId rty] in

[NamedSen ("ga_selector_" ++ showId j "")

$ mkForall vs

(Strong_equation

(Application (Qual_op_name j (toOP_TYPE ty) p) [t] p)

(Qual_var (mkSelVar "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 cs

in (i, vs, Application (Qual_op_name i (toOP_TYPE ty) [])

(map toQualVar vs) [], cs)

toQualVar :: VAR_DECL -> TERM f

toQualVar (Var_decl v s ps) =

if isSingle v then Qual_var (head v) s ps else error "toQualVar"

selForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]

selForms = makeSelForms 1 . selForms1 "X"

-- | return the constructor and the set of total selectors

ana_ALTERNATIVE :: SORT -> ALTERNATIVE

-> State (Sign f e) (Maybe (Component, Set.Set Component))

ana_ALTERNATIVE s c =

case c of

Subsorts ss _ ->

do mapM_ (addSubsort s) ss

return Nothing

_ -> do let [cons@(i, ty, il)] = getConsType s c

addOp ty i

ul <- mapM (ana_COMPONENTS s) il

let ts = concatMap fst ul

addDiags $ checkUniqueness (ts ++ concatMap snd ul)

addSentences $ selForms cons

return $ Just (Component i ty, Set.fromList ts)

-- | return total and partial selectors

ana_COMPONENTS :: SORT -> COMPONENTS

-> State (Sign f e) ([Component], [Component])

ana_COMPONENTS s c = do

let cs = getCompType s c

sels <- mapM ( \ (mi, ty) ->

case mi of

Nothing -> return Nothing

Just i -> do addOp ty i

return $ Just $ Component i ty) cs

return $ partition ((==Total) . opKind . compType) $ catMaybes sels

-- | utility

resultToState :: (a -> Result a) -> a -> State (Sign f e) a

resultToState f a = do

let r = f a

addDiags $ diags r

case maybeResult r of

Nothing -> return a

Just b -> return b

-- wrap it all up for a logic

type Ana b f e = GlobalAnnos -> b -> State (Sign f e) b

class PrettyPrint f => Resolver f where

putParen :: f -> f -- ^ put parenthesis around mixfix terms

mixResolve :: MixResolve f -- ^ resolve mixfix terms

checkMix :: (f -> Bool) -- ^ check if a formula extension has been

-- analysed completely by mixfix resolution

putInj :: f -> f -- ^ insert injections

anaForm :: Resolver f => Min f e -> GlobalAnnos -> Set.Set Id -> Set.Set Id

-> Sign f e -> (FORMULA f) -> Result (FORMULA f)

anaForm mef ga ops preds sign f = do

f' <- resolveFormula putParen mixResolve ga ops preds f

fmap (injFormula putInj) . minExpFORMULA mef ga sign

$ assert (noMixfixF checkMix f') f'

anaTerm :: Resolver f => Min f e -> GlobalAnnos -> Set.Set Id -> Set.Set Id

-> Sign f e -> (TERM f) -> Result (TERM f)

anaTerm mef ga ops preds sign t = do

t' <- resolveMixfix putParen mixResolve ga ops preds t

fmap (injTerm putInj) . oneExpTerm mef ga sign

$ assert (noMixfixT checkMix t') t'

basicAnalysis :: Resolver f

=> Min f e -- ^ type analysis of f

-> Ana b f e -- ^ static analysis of basic item b

-> Ana s f e -- ^ static analysis of signature item s

-> (e -> e -> e) -- ^ difference of signature extension e

-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)

-> Result (BASIC_SPEC b s f, Sign f e, Sign f e, [Named (FORMULA f)])

basicAnalysis mef anab anas dif (bs, inSig, ga) =

let (newBs, accSig) = runState (ana_BASIC_SPEC mef anab anas ga bs)

inSig

ds = reverse $ envDiags accSig

sents = reverse $ sentences accSig

cleanSig = accSig { envDiags = [], sentences = [], varMap = Map.empty }

diff = diffSig cleanSig inSig

{ extendedInfo = dif (extendedInfo accSig) $ extendedInfo inSig }

in Result ds $ Just (newBs, diff, cleanSig, sents)

basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos)

-> Result (BASIC_SPEC () () (), Sign () (),

Sign () (), [Named (FORMULA ())])

basicCASLAnalysis =

basicAnalysis (const $ const return) (const return) (const return) const

instance Resolver () where

putParen = id

mixResolve = const $ const return

checkMix = const True

putInj = id