MixfixParser.hs revision 9c07aad044613547d61ab235665c08adcef03a1c
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederDescription : Mixfix analysis of terms
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : Christian Maeder and Uni Bremen 2002-2006
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer : Christian.Maeder@dfki.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : experimental
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederPortability : portable
679d3f541f7a9ede4079e045f7758873bb901872Till MossakowskiMixfix analysis of terms
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder ( resolveFormula, resolveMixfix, MixResolve
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , resolveMixTrm, resolveMixFrm
d21dd452cd68abade683103a5c0cfe6d02c5f17bTill Mossakowski , extendRules, varDeclTokens
d21dd452cd68abade683103a5c0cfe6d02c5f17bTill Mossakowski , IdSets, mkIdSets, emptyIdSets, unite, unite2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , makeRules, Mix (..), emptyMix, extendMix
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder , ids_DATATYPE_DECL
c83546084a1344bb2ef752b83d0e082823508db2Christian Maederimport qualified Data.Map as Map
9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettichimport qualified Data.Set as Set
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederdata Mix b s f e = MixRecord
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder { getBaseIds :: b -> IdSets -- ^ ids of extra basic items
c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder , getSigIds :: s -> IdSets -- ^ ids of extra sig items
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski , getExtIds :: e -> IdSets -- ^ ids of signature extensions
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder , mixRules :: (TokRules, Rules) -- ^ rules for Earley
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder , putParen :: f -> f -- ^ parenthesize extended formula
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder , mixResolve :: MixResolve f -- ^ resolve extended formula
b0294d73dcefc502ddaa13e18b46103a5916971fTill Mossakowski-- | an initially empty record
c83546084a1344bb2ef752b83d0e082823508db2Christian MaederemptyMix :: Mix b s f e
c83546084a1344bb2ef752b83d0e082823508db2Christian MaederemptyMix = MixRecord
c83546084a1344bb2ef752b83d0e082823508db2Christian Maeder { getBaseIds = const emptyIdSets
c83546084a1344bb2ef752b83d0e082823508db2Christian Maeder , getSigIds = const emptyIdSets
c83546084a1344bb2ef752b83d0e082823508db2Christian Maeder , getExtIds = const emptyIdSets
c83546084a1344bb2ef752b83d0e082823508db2Christian Maeder , mixRules = (const Set.empty, emptyRules)
c83546084a1344bb2ef752b83d0e082823508db2Christian Maeder , putParen = id
c83546084a1344bb2ef752b83d0e082823508db2Christian Maeder , mixResolve = const $ const return
ed4fa6119209d695816e056a7e13c337b09adfa1Christian MaederextendMix :: Set.Set Token -> Mix b s f e -> Mix b s f e
ed4fa6119209d695816e056a7e13c337b09adfa1Christian MaederextendMix ts r = r
cc88b37a3fcafdb1d6bba895ee22e8322f42c1ccChristian Maeder { mixRules = extendRules ts $ mixRules r
9f08800df9da91d444560875167fbf7acb8396edChristian Maeder , mixResolve = extendMixResolve ts $ mixResolve r }
ed4fa6119209d695816e056a7e13c337b09adfa1Christian Maeder-- precompute non-simple op and pred identifier for mixfix rules
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | the precomputed sets of constant, op, and pred identifiers
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskitype IdSets = ((Set.Set Id, Set.Set Id), Set.Set Id) -- ops are first component
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder-- | the empty 'IdSets'
74885352ea11b26253d453af28dc904dadc4d530Christian MaederemptyIdSets :: IdSets
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaederemptyIdSets = let e = Set.empty in ((e, e), e)
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowskiunite2 :: [(Set.Set Id, Set.Set Id)] -> (Set.Set Id, Set.Set Id)
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maederunite2 l = (Set.unions $ map fst l, Set.unions $ map snd l)
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maeder-- | union 'IdSets'
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maederunite :: [IdSets] -> IdSets
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maederunite l = (unite2 $ map fst l, Set.unions $ map snd l)
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maeder-- | get all ids of a basic spec
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maederids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maederids_BASIC_SPEC f g (Basic_spec al) =
f0e85ee7e4accfc01f46aa0363acc59fcd248e8aTill Mossakowski unite $ map (ids_BASIC_ITEMS f g . item) al
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)
f0e85ee7e4accfc01f46aa0363acc59fcd248e8aTill Mossakowski -> BASIC_ITEMS b s f -> IdSets
dc8100ead1e97ea34c9ff3fe4af14d37510bf8aeChristian Maederids_BASIC_ITEMS f g bi = case bi of
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maeder Sig_items sis -> ids_SIG_ITEMS g sis
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder Free_datatype _ al _ -> ids_anDATATYPE_DECLs al
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder Ext_BASIC_ITEMS b -> f b
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder _ -> emptyIdSets
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maederids_anDATATYPE_DECLs al =
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder (unite2 $ map (ids_DATATYPE_DECL . item) al, Set.empty)
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder-- | get all ids of a sig items
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maederids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederids_SIG_ITEMS f si = let e = Set.empty in case si of
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maeder Sort_items _ _ _ -> emptyIdSets
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder Op_items al _ -> (unite2 $ map (ids_OP_ITEM . item) al, e)
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder Pred_items al _ -> ((e, e), Set.unions $ map (ids_PRED_ITEM . item) al)
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder Datatype_items _ al _ -> ids_anDATATYPE_DECLs al
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder Ext_SIG_ITEMS s -> f s
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maeder-- | get all op ids of an op item
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederids_OP_ITEM :: OP_ITEM f -> (Set.Set Id, Set.Set Id)
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maederids_OP_ITEM o = let e = Set.empty in case o of
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder Op_decl ops (Op_type _ args _ _) _ _ ->
ed4fa6119209d695816e056a7e13c337b09adfa1Christian Maeder if null args then (s, e) else (e, s)
15bceb77af626f79747d46d35979640f229a4c71Christian Maeder Op_defn i (Op_head _ args _ _) _ _ ->
15bceb77af626f79747d46d35979640f229a4c71Christian Maeder if null args then (s, e) else (e, s)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder-- | get all pred ids of a pred item
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maederids_PRED_ITEM p = case p of
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski Pred_decl preds _ _ -> Set.unions $ map Set.singleton preds
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski Pred_defn i _ _ _ -> Set.singleton i
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maederids_DATATYPE_DECL :: DATATYPE_DECL -> (Set.Set Id, Set.Set Id)
42972ddff400840d46eb54422b60083228b2996cChristian Maederids_DATATYPE_DECL (Datatype_decl _ al _) =
42972ddff400840d46eb54422b60083228b2996cChristian Maeder unite2 $ map (ids_ALTERNATIVE . item) al
42972ddff400840d46eb54422b60083228b2996cChristian Maederids_ALTERNATIVE :: ALTERNATIVE -> (Set.Set Id, Set.Set Id)
42972ddff400840d46eb54422b60083228b2996cChristian Maederids_ALTERNATIVE a = let e = Set.empty in case a of
42972ddff400840d46eb54422b60083228b2996cChristian Maeder Alt_construct _ i cs _ -> let s = Set.singleton i in
42972ddff400840d46eb54422b60083228b2996cChristian Maeder if null cs then (s, e) else (e, Set.unions $ s : map ids_COMPONENTS cs)
42972ddff400840d46eb54422b60083228b2996cChristian Maeder Subsorts _ _ -> (e, e)
42972ddff400840d46eb54422b60083228b2996cChristian Maederids_COMPONENTS :: COMPONENTS -> Set.Set Id
42972ddff400840d46eb54422b60083228b2996cChristian Maederids_COMPONENTS c = case c of
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder Cons_select _ l _ _ -> Set.unions $ map Set.singleton l
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder-- predicates get lower precedence
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermkRule :: Id -> Rule
0ea2cddb8715a770e646895e16b7b8085f49167cChristian MaedermkRule = mixRule 1
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermkSingleArgRule :: Int -> Id -> Rule
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermkArgsRule :: Int -> Id -> Rule
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermkArgsRule b ide =
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder (protect ide, b, getPlainTokenList ide ++ getTokenPlaceList tupleId)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedersingleArgId :: Id
42972ddff400840d46eb54422b60083228b2996cChristian MaedersingleArgId = mkId [exprTok, varTok]
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaedermultiArgsId :: Id
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermultiArgsId = mkId (exprTok : getPlainTokenList tupleId)
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder-- | additional scan rules
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederaddRule :: GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederaddRule ga uRules hasInvisible ((consts, ops), preds) tok =
ba94e132a4f88a5eb1ff0977e041b824c99d6a7fChristian Maeder let addP = Set.fold (\ i -> case i of
74885352ea11b26253d453af28dc904dadc4d530Christian Maeder Id (t : _) _ _ -> Map.insertWith (++) t
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder [ mixRule (if Set.member i consts then 1 else 0) i
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder , mkSingleArgRule 0 i, mkArgsRule 0 i]
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder addO = Set.fold (\ i -> case i of
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder Id (t : _) _ _ -> Map.insertWith (++) t
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder $ [mkRule i | not (isSimpleId i)
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder ++ [mkSingleArgRule 1 i, mkArgsRule 1 i]
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder addC = Set.fold (\ i -> case i of
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder Id (t : _) _ _ -> Map.insertWith (++) t [mkRule i]
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder lm = foldr (\ r -> case r of
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder (_, _, t : _) -> Map.insertWith (++) t [r]
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder _ -> error "addRule.lm") Map.empty $ listRules 1 ga
74885352ea11b26253d453af28dc904dadc4d530Christian Maeder (spreds, rpreds) = Set.partition isSimpleId preds
26ed2a19326560786ff94dfc462309d6d5d862a8Heng Jiang {- do not add simple ids as preds as these may be variables
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski with higher precedence -}
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski ops2 = Set.union ops spreds
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski sops = Set.union consts ops2
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski rConsts = Set.difference consts $ Set.union ops preds
15bceb77af626f79747d46d35979640f229a4c71Christian Maeder varR = mkRule varId
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski m = Map.insert placeTok uRules
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski $ Map.insert varTok [varR]
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski [varR, mkRule singleArgId, mkRule multiArgsId]
503e836b34d3abed34520eb4a0a345b5e13f248dTill Mossakowski $ addP (addC (addO lm ops2) rConsts) $ Set.difference rpreds ops
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder tId = mkId [tok]
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder tPId = mkId [tok, placeTok] -- prefix identifier
503e836b34d3abed34520eb4a0a345b5e13f248dTill Mossakowski in (if isSimpleToken tok && not (Set.member tId sops)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski then if hasInvisible then Set.empty else
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -- add rule for unknown constant or variable
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder $ if Set.member tPId ops || Set.member tPId rpreds
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Set.fromList [mkSingleArgRule 1 tId, mkArgsRule 1 tId]
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder -- add also rules for undeclared op
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski else Set.empty) `Set.union` Set.fromList (Map.findWithDefault [] tok m)
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- insert only identifiers starting with a place
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederinitRules (opS, predS) =
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder let addR p = Set.fold (Set.insert . mixRule p)
8db14bfdbfec2f153de435718d748fe5e22fd634Heng Jiang in emptyRules
ff49754b0e0b7ca133a66ce6c0b240c55128cde1Heng Jiang { postRules = addR 1 (addR 0 (Set.singleton $ mkRule typeId) predS) opS }
26ed2a19326560786ff94dfc462309d6d5d862a8Heng Jiang-- | construct rules from 'IdSets' to be put into a 'Mix' record
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedermakeRules :: GlobalAnnos -> IdSets -> (TokRules, Rules)
26ed2a19326560786ff94dfc462309d6d5d862a8Heng JiangmakeRules ga ((constS, opS), predS) = let
26ed2a19326560786ff94dfc462309d6d5d862a8Heng Jiang (cOps, sOps) = Set.partition begPlace opS
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder (cPreds, sPreds) = Set.partition begPlace $ Set.difference predS opS
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder addR p = Set.fold ( \ i l ->
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder mkSingleArgRule p i : mkArgsRule p i : l)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder uRules = addR 0 (addR 1 [] cOps) cPreds
26ed2a19326560786ff94dfc462309d6d5d862a8Heng Jiang in (addRule ga uRules (Set.member applId $ Set.union cOps cPreds)
26ed2a19326560786ff94dfc462309d6d5d862a8Heng Jiang ((constS, sOps), sPreds), initRules (cOps, cPreds))
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder-- | construct application
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaederasAppl :: Id -> [TERM f] -> Range -> TERM f
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaederasAppl f args ps = Application (Op_name f) args
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder $ if isNullRange ps then posOfId f else ps
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder-- | constructing the parse tree from (the final) parser state(s)
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian MaedertoAppl :: GetRange f => Id -> [TERM f] -> Range -> TERM f
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian MaedertoAppl ide ar ps =
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder if elem ide [singleArgId, multiArgsId]
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder then case ar of
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski har : tar -> case har of
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder Application q [] p ->
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder Application q tar $ appRange ps p
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder Mixfix_qual_pred _ ->
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder Mixfix_term [har, Mixfix_parenthesized tar ps]
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder _ -> error "stateToAppl"
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder _ -> error "stateToAppl2"
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski else asAppl ide ar ps
21dae7237ac384abdb94a81e00b3f099873ec623Till MossakowskiaddType :: TERM f -> TERM f -> TERM f
21dae7237ac384abdb94a81e00b3f099873ec623Till MossakowskiaddType tt t =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Mixfix_sorted_term s ps -> Sorted_term t s ps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Mixfix_cast s ps -> Cast t s ps
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder _ -> error "addType"
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder-- | the type for mixfix resolution
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maedertype MixResolve f = GlobalAnnos -> (TokRules, Rules) -> f -> Result f
f1d04fe5072b827d9cc490ebdbca78108241a392Christian MaederiterateCharts :: (GetRange f, Pretty f) => (f -> f)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder -> MixResolve f -> GlobalAnnos -> [TERM f]
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder -> Chart (TERM f) -> Chart (TERM f)
db7143998eee23e3d781f1f1e97e953bb831df1fTill MossakowskiiterateCharts par extR g terms c =
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski let self = iterateCharts par extR g
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder expand = expandPos Mixfix_token
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski oneStep = nextChart addType toAppl g c
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder ids = (addRules c, rules c)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder resolveTerm = resolveMixTrm par extR g ids
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in case terms of
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder hd : tl -> case hd of
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder Mixfix_term ts -> self (ts ++ tl) c
f1d04fe5072b827d9cc490ebdbca78108241a392Christian Maeder Mixfix_bracketed ts ps ->
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski self (expand ("[", "]") ts ps ++ tl) c
21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski Mixfix_braced ts ps ->
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski self (expand ("{", "}") ts ps ++ tl) c
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder Mixfix_parenthesized ts ps -> case ts of
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Result mds v = resolveTerm h
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski c2 = self tl (oneStep (fromMaybe h v, varTok {tokPos = ps}))
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski in mixDiags mds c2
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder _ -> self (expand ("(", ")") ts ps ++ tl) c
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder h@(Conditional t1 f2 t3 ps) -> let
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder Result mds v = do
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder t4 <- resolveTerm t1
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder f5 <- resolveMixFrm par extR g ids f2
320198216ed3bde106b509c4024b857ce4345880Maciek Makowski t6 <- resolveTerm t3
320198216ed3bde106b509c4024b857ce4345880Maciek Makowski return (Conditional t4 f5 t6 ps)
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski (oneStep (fromMaybe h v, varTok {tokPos = ps}))
320198216ed3bde106b509c4024b857ce4345880Maciek Makowski in mixDiags mds c2
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder Mixfix_token t -> let
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (ds1, trm) = convertMixfixToken (literal_annos g) asAppl
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski Mixfix_token t
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder c2 = self tl $ oneStep $ case trm of
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder Mixfix_token tok -> (trm, tok)
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder _ -> (trm, varTok {tokPos = tokPos t})
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder in mixDiags ds1 c2
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder t@(Mixfix_sorted_term _ ps) ->
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder self tl (oneStep (t, typeTok {tokPos = ps}))
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder t@(Mixfix_cast _ ps) ->
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski self tl (oneStep (t, typeTok {tokPos = ps}))
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski t@(Qual_var _ _ ps) ->
503e836b34d3abed34520eb4a0a345b5e13f248dTill Mossakowski self tl (oneStep (t, varTok {tokPos = ps}))
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder t@(Application (Qual_op_name _ _ ps) _ _) ->
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder self tl (oneStep (t, exprTok {tokPos = ps} ))
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder t@(Application (Op_name o) [] _) ->
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski self tl (oneStep (t, varTok {tokPos = posOfId o} ))
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski self tl (oneStep (t, exprTok {tokPos = ps} ))
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski Sorted_term t s ps -> let
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder Result mds v = resolveTerm t
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder tNew = Sorted_term (fromMaybe t v) s ps
e182d0ec56025d97d74829cac75ee31eec12b093Maciek Makowski c2 = self tl (oneStep (tNew, varTok {tokPos = ps}))
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder in mixDiags mds c2
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder ExtTERM t -> let
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder Result mds v = extR g ids t
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder tNew = ExtTERM $ fromMaybe t v
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder c2 = self tl $ oneStep (tNew, varTok {tokPos = getRange t})
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder in mixDiags mds c2
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski _ -> error "iterateCharts"
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maeder-- | construct 'IdSets' from op and pred identifiers
a3bcb365497d592616a4e527b426ec210dcd385cChristian MaedermkIdSets :: Set.Set Id -> Set.Set Id -> Set.Set Id -> IdSets
948f37fdb71c544ff4c907bc5863702648cf36e4Christian MaedermkIdSets consts ops preds = ((consts, ops), preds)
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski-- | top-level resolution like 'resolveMixTrm' that fails in case of diags
b4b6cffb6746d672e2bb558b72f616f97ac98316Till MossakowskiresolveMixfix :: (GetRange f, Pretty f) => (f -> f)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder -> MixResolve f -> MixResolve (TERM f)
b4b6cffb6746d672e2bb558b72f616f97ac98316Till MossakowskiresolveMixfix par extR g ruleS t =
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski let r@(Result ds _) = resolveMixTrm par extR g ruleS t
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski in if null ds then r else Result ds Nothing
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski-- | basic term resolution that supports recursion without failure
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederresolveMixTrm :: (GetRange f, Pretty f) => (f -> f)
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski -> MixResolve f -> MixResolve (TERM f)
b4b6cffb6746d672e2bb558b72f616f97ac98316Till MossakowskiresolveMixTrm par extR ga (adder, ruleS) trm =
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski getResolved (showTerm par ga) (getRangeSpan trm) toAppl
b4b6cffb6746d672e2bb558b72f616f97ac98316Till Mossakowski $ iterateCharts par extR ga [trm] $ initChart adder ruleS
b4b6cffb6746d672e2bb558b72f616f97ac98316Till MossakowskishowTerm :: Pretty f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
b4b6cffb6746d672e2bb558b72f616f97ac98316Till MossakowskishowTerm par ga = showGlobalDoc ga . mapTerm par
0e4b70274950d17f45c85d124bc600921e70fd87Christian Maeder-- | top-level resolution like 'resolveMixFrm' that fails in case of diags
0e4b70274950d17f45c85d124bc600921e70fd87Christian MaederresolveFormula :: (GetRange f, Pretty f) => (f -> f)
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder -> MixResolve f -> MixResolve (FORMULA f)
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian MaederresolveFormula par extR g ruleS f =
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski let r@(Result ds _) = resolveMixFrm par extR g ruleS f
a3bcb365497d592616a4e527b426ec210dcd385cChristian Maeder in if null ds then r else Result ds Nothing
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaedervarDeclTokens :: [VAR_DECL] -> Set.Set Token
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedervarDeclTokens = Set.unions . map (\ (Var_decl vs _ _) -> Set.fromList vs)
948f37fdb71c544ff4c907bc5863702648cf36e4Christian MaederextendRules :: Set.Set Token -> (TokRules, Rules)
948f37fdb71c544ff4c907bc5863702648cf36e4Christian Maeder -> (TokRules, Rules)
948f37fdb71c544ff4c907bc5863702648cf36e4Christian MaederextendRules ts (f, rs) =
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder r = mkRule $ mkId [t]
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder in if Set.member t ts then Set.insert r l else l, rs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextendMixResolve :: Set.Set Token -> MixResolve f -> MixResolve f
948f37fdb71c544ff4c907bc5863702648cf36e4Christian MaederextendMixResolve ts f ga = f ga . extendRules ts
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski-- | basic formula resolution that supports recursion without failure
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill MossakowskiresolveMixFrm :: (GetRange f, Pretty f) => (f -> f)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder -> MixResolve f -> MixResolve (FORMULA f)
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian MaederresolveMixFrm par extR g ids frm =
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski let self = resolveMixFrm par extR g ids
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder resolveTerm = resolveMixTrm par extR g ids in
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Quantification q vs fOld ps ->
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder do let ts = varDeclTokens vs
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder fNew <- resolveMixFrm par (extendMixResolve ts extR)
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski g (extendRules ts ids) fOld
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder return $ Quantification q vs fNew ps
db7143998eee23e3d781f1f1e97e953bb831df1fTill Mossakowski Conjunction fsOld ps ->
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski do fsNew <- mapM self fsOld
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski return $ Conjunction fsNew ps
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Disjunction fsOld ps ->
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski do fsNew <- mapM self fsOld
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian Maeder return $ Disjunction fsNew ps
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Implication f1 f2 b ps ->
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder do f3 <- self f1
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder f4 <- self f2
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder return $ Implication f3 f4 b ps
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski Equivalence f1 f2 ps ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do f3 <- self f1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski f4 <- self f2
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder return $ Equivalence f3 f4 ps
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder Negation fOld ps ->
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder do fNew <- self fOld
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski return $ Negation fNew ps
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Predication sym tsOld ps ->
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder do tsNew <- mapM resolveTerm tsOld
4ea99e115bbade1632815267d5e0dcb9931aac1eChristian Maeder return $ Predication sym tsNew ps
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Definedness tOld ps ->
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder do tNew <- resolveTerm tOld
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder return $ Definedness tNew ps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Existl_equation t1 t2 ps ->
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder do t3 <- resolveTerm t1
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder t4 <- resolveTerm t2
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski return $ Existl_equation t3 t4 ps
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Strong_equation t1 t2 ps ->
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski do t3 <- resolveTerm t1
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski t4 <- resolveTerm t2
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski return $ Strong_equation t3 t4 ps
1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Membership tOld s ps ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder do tNew <- resolveTerm tOld
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return $ Membership tNew s ps
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder Mixfix_formula tOld ->
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder do tNew <- resolveTerm tOld
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Application (Op_name ide) args ps ->
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maeder return $ Predication (Pred_name ide) args ps
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Mixfix_qual_pred qide ->
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return $ Predication qide [] nullRange
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder Mixfix_term [Mixfix_qual_pred qide,
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder Mixfix_parenthesized ts ps] ->
2d2826f9db2c17275f91b0104940a60a2f9fd44dChristian Maeder return $ Predication qide ts ps
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder _ -> fatal_error
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ("not a formula: " ++ showTerm par g tNew "")
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski (getRangeSpan tNew)
74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder ExtFORMULA f ->
c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder do newF <- extR g ids f
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return $ ExtFORMULA newF
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder f -> return f