StaticAna.hs revision 94e112d16f89130a688db8b03ad3224903f5e97e
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 BungiuMaintainer : Christian.Maeder@dfki.de
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuStability : provisional
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuPortability : portable
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuCASL static analysis for basic specifications
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuFollows Chaps. III:2 and III:3 of the CASL Reference Manual.
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- formulas type-check
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuThe formulas are returned with fully-qualified variables, operation
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuand predicate symbols.
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 Bungiuimport qualified Common.Lib.MapSet as MapSet
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Common.Lib.Rel as Rel
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Map as Map
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Set as Set
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 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 Just _ -> alsoWarning s varS i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddOp :: Annoted a -> OpType -> Id -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu do checkSorts (opRes ty : opArgs ty)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let m = opMap e
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 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 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 BungiuaddAssocOp :: OpType -> Id -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocOp ty i = do
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu put e { assocOps = addOpTo i ty $ assocOps e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , globAnnos = updAssocMap (addAssocId i) $ globAnnos e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdateExtInfo :: (e -> Result e) -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdateExtInfo upd = do
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 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 let m = predMap e
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ds = checkWithOtherMap predS opS (opMap e) i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ++ checkWithVars predS (varMap e) i
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu addDiags $ mkDiag Hint "redeclared pred" i : ds
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 BungiunonConsts :: OpMap -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiunonConsts = MapSet.keysSet . MapSet.filter (not . null . opArgs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuopMapConsts :: OpMap -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuopMapConsts = MapSet.keysSet . MapSet.filter (null . opArgs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallOpIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallOpIds = nonConsts . opMap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallConstIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallConstIds = opMapConsts . opMap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu updAssocMap (\ m -> Set.fold addAssocId m $ MapSet.keysSet $ assocOps e)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuupdAssocMap f ga = ga { assoc_annos = f $ assoc_annos ga }
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 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 BungiuallPredIds :: Sign f e -> Set.Set Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuallPredIds = MapSet.keysSet . predMap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuaddSentences ds =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu put e { sentences = reverse ds ++ sentences e }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- * traversing all data types of the abstract syntax
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-- looseness of a datatype
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiudata GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel ManceunionGenAx :: [GenAx] -> GenAx
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuunionGenAx = foldr (\ (s1, r1, f1) (s2, r2, f2) ->
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance Set.union f1 f2)) emptyGenAx
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 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 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 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 return (resFs, fufs)
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 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
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
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 MaedermapAn :: (a -> b) -> Annoted a -> Annoted b
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel MancemapAn f an = replaceAnnoted (f $ item an) an
2713ec15465bd1e643f6310d7048b5a30ad55c83Christian Maedertype GenAx = (Set.Set SORT, Rel.Rel SORT, Set.Set Component)
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel ManceemptyGenAx :: GenAx
86f318f607745d1f40cbf87048a13ac1c65100e6Felix Gabriel ManceemptyGenAx = (Set.empty, Rel.empty, Set.empty)
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
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 _) =
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 noConsList = Set.difference sorts resList
9a160cb31a4d2b1a193f3229c79b38efc517152cFrancisc Nicolae Bungiu voidOps = Set.difference resList sorts
unless (Set.null noConsList)
unless (Set.null voidOps)
Set.unions (map (getOps . item) al))
foldr (`Rel.insertDiffPair` t)
Rel.empty subs
Iso_decl il _ -> (Set.fromList il,
in (sorts, rel, Set.empty)
getOps :: OP_ITEM f -> Set.Set Component
Set.fromList $ map (flip Component $ toOpType ty) is
Op_defn i par _ _ -> maybe Set.empty
(Set.singleton . Component i . toOpType) $ headToType par
put e { varMap = Map.empty }
put e { varMap = Map.empty }
-- see Isabelle/doc/ref.pdf 10.6 Permutative rewrite rules (p. 137)
sign { varMap = Map.empty } (Just rty) q t
let totalSels = Set.unions $ map snd constr
showDoc (Set.toList totalSels)
-> State (Sign f e) (Maybe (Component, Set.Set Component))
return $ Just (Component i ty, Set.fromList ts)
let mix = extendMix (Map.keysSet $ varMap sign) mixIn
let mix = extendMix (Map.keysSet $ varMap sign) mixIn