StaticAna.hs revision 94e112d16f89130a688db8b03ad3224903f5e97e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu{- |
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuModule : $Header$
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuDescription : CASL static analysis for basic specifications
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuLicense : GPLv2 or higher, see LICENSE.txt
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuMaintainer : Christian.Maeder@dfki.de
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuStability : provisional
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuPortability : portable
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuCASL static analysis for basic specifications
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuFollows Chaps. III:2 and III:3 of the CASL Reference Manual.
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuThe static analysis takes an abstract syntax tree of a basic specification
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuand outputs a signature and a set of formulas, while checking that
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu- all sorts used in operation and predicate declarations have been declared
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu- all sorts, operation and predicate symbols used in formulas have
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu been declared
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu- formulas type-check
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuThe formulas are returned with fully-qualified variables, operation
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuand predicate symbols.
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuThe static analysis functions are parameterized with functions for
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiutreating CASL extensions, that is, additional basic items, signature
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuitems and formulas.
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-}
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiumodule CASL.StaticAna where
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Manceimport CASL.AS_Basic_CASL
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport CASL.MixfixParser
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Manceimport CASL.Overload
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport CASL.Quantification
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport CASL.Sign
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport CASL.ToDoc
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.AS_Annotation
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.Doc
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.DocUtils
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maederimport Common.ExtSign
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.GlobalAnnotations
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.Keywords
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.Lib.State
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Common.Result
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Common.Lib.MapSet as MapSet
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Common.Lib.Rel as Rel
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Control.Monad
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Map as Map
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Set as Set
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Data.Maybe
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport Data.List
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiucheckPlaces :: [SORT] -> Id -> [Diagnosis]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiucheckPlaces args i = let n = placeCount i in
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu [mkDiag Error "wrong number of places" i | n > 0 && n /= length args ]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiucheckWithVars :: String -> Map.Map SIMPLE_ID a -> Id -> [Diagnosis]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiucheckWithVars s m i@(Id ts _ _) = if isSimpleId i then
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu case Map.lookup (head ts) m of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Nothing -> []
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Just _ -> alsoWarning s varS i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu else []
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddOp :: Annoted a -> OpType -> Id -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddOp a ty i =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu do checkSorts (opRes ty : opArgs ty)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu e <- get
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let m = opMap e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu l = MapSet.lookup i m
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ds = checkWithOtherMap opS predS (predMap e) i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ++ checkWithVars opS (varMap e) i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu check = addDiags $
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (if Set.member ty l then [mkDiag Hint "redeclared op" i]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu else checkPlaces (opArgs ty) i ++ checkNamePrefix i)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ++ ds
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu store = put e { opMap = addOpTo i ty m }
9475501a6acf48434052d9e6f4a05ed6681eaaabFrancisc Nicolae Bungiu pTy = mkPartial ty
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu case opKind ty of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Partial -> if Set.member (mkTotal ty) l then
9475501a6acf48434052d9e6f4a05ed6681eaaabFrancisc Nicolae Bungiu addDiags $ mkDiag Warning "partially redeclared" i : ds
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu else store >> check
9475501a6acf48434052d9e6f4a05ed6681eaaabFrancisc Nicolae Bungiu Total -> if Set.member pTy l then do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu put e { opMap = MapSet.insert i ty
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu $ MapSet.delete i pTy m }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addDiags $ mkDiag Hint "redeclared as total" i : ds
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu else store >> check
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addAnnoSet a $ Symbol i $ OpAsItemType ty
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocOp :: OpType -> Id -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocOp ty i = do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu e <- get
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu put e { assocOps = addOpTo i ty $ assocOps e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , globAnnos = updAssocMap (addAssocId i) $ globAnnos e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdateExtInfo :: (e -> Result e) -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdateExtInfo upd = do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu s <- get
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let re = upd $ extendedInfo s
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu case maybeResult re of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Nothing -> return ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Just e -> put s { extendedInfo = e }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addDiags $ diags re
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddPred :: Annoted a -> PredType -> Id -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddPred a ty i =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu do checkSorts $ predArgs ty
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu e <- get
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let m = predMap e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu l = MapSet.lookup i m
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ds = checkWithOtherMap predS opS (opMap e) i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ++ checkWithVars predS (varMap e) i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu if Set.member ty l then
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addDiags $ mkDiag Hint "redeclared pred" i : ds
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu else do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu put e { predMap = MapSet.insert i ty m }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addDiags $ checkPlaces (predArgs ty) i ++ checkNamePrefix i ++ ds
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addAnnoSet a $ Symbol i $ PredAsItemType ty
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiunonConsts :: OpMap -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiunonConsts = MapSet.keysSet . MapSet.filter (not . null . opArgs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuopMapConsts :: OpMap -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuopMapConsts = MapSet.keysSet . MapSet.filter (null . opArgs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallOpIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallOpIds = nonConsts . opMap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallConstIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallConstIds = opMapConsts . opMap
06acd8a23b2f06e7b2373d53f738cf56c7f03223Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocs e =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu updAssocMap (\ m -> Set.fold addAssocId m $ MapSet.keysSet $ assocOps e)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdAssocMap f ga = ga { assoc_annos = f $ assoc_annos ga }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocId :: Id -> AssocMap -> AssocMap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocId i m = case Map.lookup i m of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Nothing -> Map.insert i ALeft m
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu _ -> m
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuformulaIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuformulaIds e = let ops = allOpIds e in
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Set.fromDistinctAscList (map simpleIdToId $ Map.keys $ varMap e)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu `Set.union` ops
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallPredIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallPredIds = MapSet.keysSet . predMap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddSentences ds =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu do e <- get
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu put e { sentences = reverse ds ++ sentences e }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- * traversing all data types of the abstract syntax
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuana_BASIC_SPEC :: (FormExtension f, TermExtension f) => Min f e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -> Ana b b s f e -> Ana s b s f e -> Mix b s f e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -> BASIC_SPEC b s f -> State (Sign f e) (BASIC_SPEC b s f)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuana_BASIC_SPEC mef ab anas mix (Basic_spec al) = fmap Basic_spec $
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu mapAnM (ana_BASIC_ITEMS mef ab anas mix) al
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- looseness of a datatype
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiudata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel ManceunionGenAx :: [GenAx] -> GenAx
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuunionGenAx = foldr (\ (s1, r1, f1) (s2, r2, f2) ->
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (Set.union s1 s2,
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance Rel.union r1 r2,
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance Set.union f1 f2)) emptyGenAx
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuanaVarForms :: (FormExtension f, TermExtension f)
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance => Min f e -> Mix b s f e -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -> State (Sign f e) [Annoted (FORMULA f)]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuanaVarForms mef mix vs fs r = do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (resFs, fufs) <- anaLocalVarForms (anaForm mef mix) vs fs r
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addSentences $ map makeNamedSen fufs
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu return resFs
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuanaLocalVarForms :: TermExtension f
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu => (Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuanaLocalVarForms anaFrm il afs ps = do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu e <- get -- save
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu mapM_ addVars il
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu vds <- gets envDiags
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu sign <- get
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu unless (null il) $ put e { envDiags = vds }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -- restore with shadowing warnings
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let (es, resFs, anaFs) = foldr (\ f (dss, ress, ranas) ->
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let Result ds m = anaFrm sign $ item f
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu in case m of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Nothing -> (ds ++ dss, ress, ranas)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Just (resF, anaF) ->
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (ds ++ dss, f {item = resF} : ress,
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu f {item = anaF} : ranas))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ([], [], []) afs
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu fufs = map (mapAn (\ f -> let
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu qf = mkForallRange il f ps
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu vs = map (\ (v, s) -> Var_decl [v] s ps)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu $ Set.toList $ freeVars sign qf
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu in stripQuant sign $ mkForallRange vs qf ps))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu anaFs
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addDiags es
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu return (resFs, fufs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuana_BASIC_ITEMS :: (FormExtension f, TermExtension f)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu => Min f e -> Ana b b s f e -> Ana s b s f e -> Mix b s f e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuana_BASIC_ITEMS mef ab anas mix bi =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu case bi of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Sig_items sis -> fmap Sig_items $
a6526952d69bccd048c954eb920493a6a83e78faFelix Gabriel Mance ana_SIG_ITEMS mef anas mix Loose sis
a6526952d69bccd048c954eb920493a6a83e78faFelix Gabriel Mance Free_datatype sk al ps -> do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu mapM_ (\ i -> case item i of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Datatype_decl s _ _ -> addSort sk i s) al
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu mapAnM (ana_DATATYPE_DECL Free) al
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu toSortGenAx ps True $ getDataGenSig al
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance closeSubsortRel
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance return bi
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder Sort_gen al ps -> do
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance (gs, ul) <- ana_Generated mef anas mix al
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder toSortGenAx ps False $ unionGenAx gs
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance return $ Sort_gen ul ps
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance Var_items il _ -> do
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder mapM_ addVars il
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance return bi
f20c085644aa49702488405bc2d4245cf0e5a713Felix Gabriel Mance Local_var_axioms il afs ps -> do
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance resFs <- anaVarForms mef mix il afs ps
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance return $ Local_var_axioms il resFs ps
f20c085644aa49702488405bc2d4245cf0e5a713Felix Gabriel Mance Axiom_items afs ps -> do
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance resFs <- anaVarForms mef mix [] afs ps
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance return $ Axiom_items resFs ps
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance Ext_BASIC_ITEMS b -> fmap Ext_BASIC_ITEMS $ ab mix b
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian MaedermapAn :: (a -> b) -> Annoted a -> Annoted b
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel MancemapAn f an = replaceAnnoted (f $ item an) an
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maedertype GenAx = (Set.Set SORT, Rel.Rel SORT, Set.Set Component)
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel ManceemptyGenAx :: GenAx
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel ManceemptyGenAx = (Set.empty, Rel.empty, Set.empty)
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian MaedertoSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel MancetoSortGenAx ps isFree (sorts, rel, ops) = do
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance let sortList = Set.toList sorts
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance opSyms = map (\ c -> let ide = compId c in Qual_op_name ide
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance (toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance injSyms = map (\ (s, t) -> let p = posOfId s in
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder Qual_op_name (mkUniqueInjName s t)
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance (Op_type Total [s] t p) p) $ Rel.toList
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder $ Rel.irreflex rel
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance allSyms = opSyms ++ injSyms
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance resType _ (Op_name _) = False
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance resType s (Qual_op_name _ t _) = res_OP_TYPE t == s
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance getIndex s = fromMaybe (-1) $ elemIndex s sortList
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance addIndices (Op_name _) =
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance error "CASL.StaticAna.addIndices"
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maeder addIndices os@(Qual_op_name _ t _) =
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance (os, map getIndex $ args_OP_TYPE t)
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance collectOps s =
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance Constraint s (map addIndices $ filter (resType s) allSyms) s
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel Mance constrs = map collectOps sortList
f20c085644aa49702488405bc2d4245cf0e5a713Felix Gabriel Mance resList = Set.fromList $ map (\ o -> case o of
f20c085644aa49702488405bc2d4245cf0e5a713Felix Gabriel Mance Qual_op_name _ t _ -> res_OP_TYPE t
f20c085644aa49702488405bc2d4245cf0e5a713Felix Gabriel Mance Op_name _ -> error "CASL.StaticAna.resList")
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance allSyms
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance noConsList = Set.difference sorts resList
9a160cb31a4d2b1a193f3229c79b38efc517152cFrancisc Nicolae Bungiu voidOps = Set.difference resList sorts
f = Sort_gen_ax constrs isFree
when (null sortList)
$ addDiags [Diag Error "missing generated sort" ps]
unless (Set.null noConsList)
$ addDiags [mkDiag Warning "generated sorts without constructor"
noConsList]
unless (Set.null voidOps)
$ addDiags [mkDiag Warning "non-generated sorts as constructor result"
voidOps]
addSentences [toSortGenNamed f sortList]
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 mef anas mix gk si =
case si of
Sort_items sk al ps ->
do ul <- mapM (ana_SORT_ITEM mef mix sk) al
closeSubsortRel
return $ Sort_items sk ul ps
Op_items al ps ->
do ul <- mapM (ana_OP_ITEM mef mix) al
return $ Op_items ul ps
Pred_items al ps ->
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
closeSubsortRel
return si
Ext_SIG_ITEMS s -> fmap Ext_SIG_ITEMS $ anas mix 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 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
Op_items al _ -> (Set.empty, Rel.empty,
Set.unions (map (getOps . item) al))
Datatype_items _ dl _ -> getDataGenSig dl
_ -> emptyGenAx
isConsAlt :: ALTERNATIVE -> Bool
isConsAlt a = case a of
Subsorts _ _ -> False
_ -> True
getDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig dl =
let alts = concatMap ((\ (Datatype_decl s al _) ->
map (\ a -> (s, item a)) al) . item) dl
sorts = map fst alts
(realAlts, subs) = partition (isConsAlt . snd) alts
cs = map (\ (s, a) ->
let (i, ty, _) = getConsType s a
in Component i ty) realAlts
rel = foldr (\ (t, a) r ->
foldr (`Rel.insertDiffPair` t)
r $ getAltSubsorts a)
Rel.empty subs
in (Set.fromList sorts, rel, Set.fromList cs)
getGenSorts :: SORT_ITEM f -> GenAx
getGenSorts si = let
(sorts, rel) = case si of
Sort_decl il _ -> (Set.fromList il, Rel.empty)
Subsort_decl il i _ ->
(Set.fromList (i : il), foldr (`Rel.insertDiffPair` i) Rel.empty il)
Subsort_defn sub _ super _ _ ->
(Set.singleton sub, Rel.insertDiffPair sub super Rel.empty)
Iso_decl il _ -> (Set.fromList il,
foldr (\ s r -> foldr (Rel.insertDiffPair s) r il) Rel.empty il)
in (sorts, rel, Set.empty)
getOps :: OP_ITEM f -> Set.Set Component
getOps oi = case oi of
Op_decl is ty _ _ ->
Set.fromList $ map (flip Component $ toOpType ty) is
Op_defn i par _ _ -> maybe Set.empty
(Set.singleton . Component i . toOpType) $ headToType 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 mef mix sk asi =
case item asi of
Sort_decl il _ ->
do mapM_ (addSort sk asi) il
return asi
Subsort_decl il i _ ->
do mapM_ (addSort sk asi) (i : il)
mapM_ (addSubsort i) il
return asi
Subsort_defn sub v super af ps ->
do e <- get -- save
put e { varMap = Map.empty }
addVars (Var_decl [v] super ps)
sign <- get
put e -- restore
let Result ds mf = anaForm mef mix sign $ item af
lb = getRLabel af
lab = if null lb then getRLabel asi else lb
addDiags ds
addSort sk asi sub
addSubsort super sub
case mf of
Nothing -> return asi { item = Subsort_decl [sub] super ps}
Just (resF, anaF) -> do
let p = posOfId sub
pv = tokPos v
addSentences [(makeNamed lab $
mkForallRange [Var_decl [v] super pv]
(Relation
(Membership (Qual_var v super pv) sub p)
Equivalence anaF p) p) {
isAxiom = notImplied af }]
return asi { item = Subsort_defn sub v super
af { item = resF } ps}
Iso_decl il _ ->
do mapM_ (addSort sk asi) il
case il of
[] -> return ()
_ : tl -> mapM_ (uncurry $ addSubsortOrIso False)
$ zip tl il
return asi
putVarsInEmptyMap :: [VAR_DECL] -> State (Sign f e) (Sign f e)
putVarsInEmptyMap vs = do
e <- get -- save
put e { varMap = Map.empty }
mapM_ addVars vs
sign <- get
put e -- restore
return 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 mef mix aoi =
case item aoi of
Op_decl ops ty il ps ->
do let oty = toOpType ty
ni = notImplied aoi
mapM_ (addOp aoi oty) ops
ul <- mapM (ana_OP_ATTR mef mix oty ni ops) il
when (any (\ a -> case a of
Assoc_op_attr -> True
_ -> False) il) $ do
mapM_ (addAssocOp oty) ops
when (any (\ a -> case a of
Comm_op_attr -> True
_ -> False) il)
$ addSentences $ map (addLeftComm oty ni) ops
return aoi {item = Op_decl ops ty (catMaybes ul) ps}
Op_defn i ohd@(Op_head k vs _ _) at ps ->
do let mty = headToType ohd
lb = getRLabel at
lab = if null lb then getRLabel aoi else lb
arg = concatMap (\ (Var_decl v s qs) ->
map (\ j -> Qual_var j s qs) v) vs
maybe (return ()) (\ ty -> addOp aoi (toOpType ty) i) mty
sign <- putVarsInEmptyMap vs
let Result ds mt = anaTerm mef mix sign
(fmap res_OP_TYPE mty) ps $ item at
addDiags ds
case mt of
Nothing -> return $ maybe aoi
(\ ty -> aoi { item = Op_decl [i] ty [] ps }) mty
Just (resT, anaT) -> do
let p = posOfId i
tvs = freeTermVars sign anaT
ty = headToTypeM (Op_type k (sortsOfArgs vs)
(sortOfTerm anaT) ps) id ohd
maybe (addOp aoi (toOpType ty) i) (const $ return ()) mty
addDiags $ warnUnusedVars " local " sign tvs
addSentences [(makeNamed lab $ mkForallRange vs
(Equation
(Application (Qual_op_name i ty p) arg ps)
Strong anaT p) ps) {
isAxiom = notImplied at, isDef = True }]
return aoi {item = Op_defn i ohd at { item = resT } ps }
headToTypeM :: a -> (OP_TYPE -> a) -> OP_HEAD -> a
headToTypeM def f (Op_head k args mr ps) = maybe def
(\ r -> f $ Op_type k (sortsOfArgs args) r ps) mr
headToType :: OP_HEAD -> Maybe OP_TYPE
headToType = headToTypeM Nothing Just
sortsOfArgs :: [VAR_DECL] -> [SORT]
sortsOfArgs = concatMap (\ (Var_decl l s _) -> map (const s) l)
threeVars :: SORT -> ([VAR_DECL], [TERM f])
threeVars rty =
let q = posOfId rty
ns = map mkSimpleId ["x", "y", "z"]
vs = map (\ v -> Var_decl [v] rty q) ns
in (vs, map toQualVar vs)
-- see Isabelle/doc/ref.pdf 10.6 Permutative rewrite rules (p. 137)
addLeftComm :: OpType -> Bool -> Id -> Named (FORMULA f)
addLeftComm ty ni i =
let sty = toOP_TYPE ty
rty = opRes ty
(vs, [v1, v2, v3]) = threeVars rty
p = posOfId i
qi = Qual_op_name i sty p
in (makeNamed ("ga_left_comm_" ++ showId i "") $
mkForallRange vs
(Equation
(Application qi [v1, Application qi [v2, v3] p] p) Strong
(Application qi [v2, Application qi [v1, v3] p] p) p) p)
{ isAxiom = 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 mef mix ty ni ois oa = do
let sty = toOP_TYPE ty
rty = opRes ty
atys = opArgs ty
q = posOfId rty
case atys of
[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]
case oa of
Unit_op_attr t -> do
sign <- get
let Result ds mt = anaTerm mef mix
sign { varMap = Map.empty } (Just rty) q t
addDiags ds
case mt of
Nothing -> return Nothing
Just (resT, anaT) -> do
addSentences $ map (makeUnit True anaT ty ni) ois
addSentences $ map (makeUnit False anaT ty ni) ois
return $ Just $ Unit_op_attr resT
Assoc_op_attr -> do
let (vs, [v1, v2, v3]) = threeVars rty
makeAssoc i = let p = posOfId i
qi = Qual_op_name i sty p in
(makeNamed ("ga_assoc_" ++ showId i "") $
mkForallRange vs
(Equation
(Application qi [Application qi [v1, v2] p, v3] p) Strong
(Application qi [v1, Application qi [v2, v3] p] p) p) p)
{ isAxiom = ni }
addSentences $ map makeAssoc ois
return $ Just oa
Comm_op_attr -> do
let ns = map mkSimpleId ["x", "y"]
vs = zipWith (\ v t -> Var_decl [v] t
$ concatMapRange posOfId atys) ns atys
args = map toQualVar vs
makeComm i = let p = posOfId i
qi = Qual_op_name i sty p in
(makeNamed ("ga_comm_" ++ showId i "") $
mkForallRange vs
(Equation (Application qi args p) Strong
(Application qi (reverse args) p) p) p) {
isAxiom = ni }
addSentences $ map makeComm ois
return $ Just oa
Idem_op_attr -> do
let v = mkSimpleId "x"
vd = Var_decl [v] rty q
qv = toQualVar vd
makeIdem i = let p = posOfId i in
(makeNamed ("ga_idem_" ++ showId i "") $
mkForallRange [vd]
(Equation
(Application (Qual_op_name i sty p) [qv, qv] p)
Strong qv p) p) { isAxiom = ni }
addSentences $ map makeIdem ois
return $ Just oa
-- first bool for left and right, second one for no implied annotation
makeUnit :: Bool -> TERM f -> OpType -> Bool -> Id -> Named (FORMULA f)
makeUnit b t ty ni i =
let lab = "ga_" ++ (if b then "right" else "left") ++ "_unit_"
++ showId i ""
v = mkSimpleId "x"
vty = opRes ty
q = posOfId vty
p = posOfId i
qv = Qual_var v vty q
args = [qv, t]
rargs = if b then args else reverse args
in (makeNamed lab $ mkForallRange [Var_decl [v] vty q]
(Equation
(Application (Qual_op_name i (toOP_TYPE ty) p) rargs p)
Strong qv p) p) {isAxiom = 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 mef mix apr = case item apr of
Pred_decl preds ty _ -> do
mapM_ (addPred apr $ toPredType ty) preds
return apr
Pred_defn i phd@(Pred_head vs rs) at ps -> do
let lb = getRLabel at
lab = if null lb then getRLabel apr else lb
ty = Pred_type (sortsOfArgs vs) rs
arg = concatMap (\ (Var_decl v s qs) ->
map (\ j -> Qual_var j s qs) v) vs
addPred apr (toPredType ty) i
sign <- putVarsInEmptyMap vs
let Result ds mt = anaForm mef mix sign $ item at
addDiags ds
case mt of
Nothing -> return apr {item = Pred_decl [i] ty ps}
Just (resF, anaF) -> do
let p = posOfId i
addSentences [(makeNamed lab $
mkForallRange vs
(Relation (Predication (Qual_pred_name i ty p)
arg p) Equivalence anaF p) p) {
isDef = True }]
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
cs = map fst constr
unless (null constr) $ do
addDiags $ checkUniqueness cs
let totalSels = Set.unions $ map snd constr
wrongConstr = filter ((totalSels /=) . snd) constr
addDiags $ map (\ (c, _) -> mkDiag Warning
("total selectors '" ++ showSepList (showString ", ")
showDoc (Set.toList totalSels)
"'\n should be in alternative") c) wrongConstr
case gk of
Free -> do
let allts = map item al
(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))
. selForms1 "X" ) comps
sels = concatMap (\ (_, _, _, ses) -> ses) ttrips
addDiags $ foldr (\ a ds -> case a of
Alt_construct p i _ _ | p == Partial ->
mkDiag Error
"illegal free partial constructor" i : ds
_ -> ds) [] allts
addSentences $ map makeInjective
$ filter (\ (_, _, ces) -> not $ null ces)
comps
addSentences $ makeDisjSubsorts s sbs
addSentences $ concatMap (\ c -> map (makeDisjToSort c) sbs)
comps
addSentences $ makeDisjoint comps
addSentences $ catMaybes $ concatMap
(\ ses ->
map (makeUndefForm ses) ttrips) sels
_ -> return ()
return cs
makeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts d subs = case subs of
[] -> []
s : rs -> map (makeDisjSubsort s) rs ++ makeDisjSubsorts d rs
where
makeDisjSubsort :: SORT -> SORT -> Named (FORMULA f)
makeDisjSubsort s1 s2 = let
n = mkSimpleId "x"
pd = posOfId d
p1 = posOfId s1
p2 = posOfId s2
p = pd `appRange` p1 `appRange` p2
v = Var_decl [n] d pd
qv = toQualVar v
in makeNamed ("ga_disjoint_sorts_" ++ showId s1 "_" ++ showId s2 "")
$ mkForallRange [v] (Negation (Junction Con [
Membership qv s1 p1, Membership qv s2 p2] p) p) p
makeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
makeDisjToSort a s =
let (c, v, t, _) = selForms1 "X" a
p = posOfId s
in makeNamed ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "")
$ mkForallRange v (Negation (Membership t s p) p) p
makeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeInjective a =
let (c, v1, t1, _) = selForms1 "X" a
(_, v2, t2, _) = selForms1 "Y" a
p = posOfId c
in makeNamed ("ga_injective_" ++ showId c "")
$ mkForallRange (v1 ++ v2)
(Relation (Equation t1 Strong t2 p) Equivalence
(let ces = zipWith (\ w1 w2 -> Equation
(toQualVar w1) Strong (toQualVar w2) p) v1 v2
in conjunctRange ces p)
p) p
makeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint l = case l of
[] -> []
c : cs -> map (makeDisj c) cs ++ makeDisjoint cs
where
makeDisj :: (Id, OpType, [COMPONENTS]) -> (Id, OpType, [COMPONENTS])
-> Named (FORMULA f)
makeDisj a1 a2 =
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 "")
$ mkForallRange (v1 ++ v2) (Negation (Equation t1 Strong 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) =
let p = posOfId s in
if any (\ (se, ts) -> s == se && opRes ts == opRes ty ) sels
then Nothing else
Just $ makeNamed ("ga_selector_undef_" ++ showId s "_" ++ showId i "")
$ mkForallRange vs
(Negation
(Definedness
(Application (Qual_op_name s (toOP_TYPE ty) p) [t] p)
p) p) p
getAltSubsorts :: ALTERNATIVE -> [SORT]
getAltSubsorts c = case c of
Subsorts cs _ -> cs
_ -> []
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 _ _ -> 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 -> mkVarDecl (mkNumVar str n) (opRes ty)
: genSelVars str (n + 1) rs
makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
-> [Named (FORMULA f)]
makeSelForms n (i, vs, t, tys) = case tys of
[] -> []
(mi, ty) : rs ->
(case mi of
Nothing -> []
Just j -> let p = posOfId j
rty = opRes ty
q = posOfId rty in
[makeNamed ("ga_selector_" ++ showId j "")
$ mkForallRange vs
(Equation
(Application (Qual_op_name j (toOP_TYPE ty) p) [t] p)
Strong (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, mkAppl (mkQualOp i $ toOP_TYPE ty)
(map toQualVar vs), 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
Subsorts ss _ -> do
mapM_ (addSubsort s) ss
return Nothing
ic -> do
let cons@(i, ty, il) = getConsType s ic
addOp c 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 (emptyAnno ()) ty i
return $ Just $ Component i ty) cs
return $ partition (isTotal . 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 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 mef mixIn sign f = do
let mix = extendMix (Map.keysSet $ varMap sign) mixIn
resF <- resolveFormula (putParen mix) (mixResolve mix)
(globAnnos sign) (mixRules mix) f
anaF <- minExpFORMULA mef sign resF
return (resF, 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 mef mixIn sign msrt pos t = do
let mix = extendMix (Map.keysSet $ varMap sign) mixIn
resT <- resolveMixfix (putParen mix) (mixResolve mix)
(globAnnos sign) (mixRules mix) t
anaT <- oneExpTerm mef sign $ maybe resT
(\ srt -> Sorted_term resT srt pos) msrt
return (resT, 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 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)
$ allPredIds 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)
{ emptySortSet = emptySortSet accSig
, sortRel = sortRel accSig
, opMap = opMap accSig
, assocOps = assocOps accSig
, predMap = predMap accSig
, annoMap = annoMap accSig
, globAnnos = ga }
in Result (ds ++ warnUnused accSig sents) $
Just (newBs, ExtSign cleanSig $ declaredSymbols accSig, sents)
basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos)
-> Result (BASIC_SPEC () () (),
ExtSign (Sign () ()) Symbol,
[Named (FORMULA ())])
basicCASLAnalysis =
basicAnalysis (const return) (const return) (const return) emptyMix