MixfixParser.hs revision ca0d4947f7b0fdcbf7eac627659e6cff6d3863ba
9658657e918981d91c8647ed8c220464f10a6235Christian MaederModule : $Header$
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederDescription : Mixfix analysis of terms
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : Christian Maeder and Uni Bremen 2002-2006
d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMaintainer : Christian.Maeder@dfki.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : portable
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMixfix analysis of terms
bdeddba30d29f413af1e1ae6b6bab275c017bd98Christian Maeder ( resolveFormula, resolveMixfix, MixResolve
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , resolveMixTrm, resolveMixFrm
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder , IdSets, mkIdSets, emptyIdSets, unite, single
ae35311385999d91f812155fe99439724d54063bChristian Maeder , makeRules, Mix(..), emptyMix
46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport qualified Data.Set as Set
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified Data.Map as Map
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederdata Mix b s f e = MixRecord
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder { getBaseIds :: b -> IdSets -- ^ ids of extra basic items
46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder , getSigIds :: s -> IdSets -- ^ ids of extra sig items
46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder , getExtIds :: e -> IdSets -- ^ ids of signature extensions
46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder , mixRules :: (Token -> [Rule], Rules) -- ^ rules for Earley
48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski , putParen :: f -> f -- ^ parenthesize extended formula
c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder , mixResolve :: MixResolve f -- ^ resolve extended formula
3986813db69106b9bb1b62faa77532af42512a0cChristian Maeder-- | an initially empty record
3986813db69106b9bb1b62faa77532af42512a0cChristian MaederemptyMix :: Mix b s f e
596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian MaederemptyMix = MixRecord
596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maeder { getBaseIds = const emptyIdSets
596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maeder , getSigIds = const emptyIdSets
46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder , getExtIds = const emptyIdSets
e982190515f83fe6615436530ebe89bb320770d6Christian Maeder , mixRules = error "emptyMix"
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder , putParen = id
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich , mixResolve = const $ const return
46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder-- precompute non-simple op and pred identifier for mixfix rules
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz-- | the precomputed sets of op and pred (non-simple) identifiers
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulztype IdSets = (Set.Set Id, Set.Set Id) -- ops are first component
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder-- | the empty 'IdSets'
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian MaederemptyIdSets :: IdSets
9b6a888fced92090f2f3d60f551b8bf38bf2eecbChristian Maeder-- | union 'IdSets'
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maederunite :: [IdSets] -> IdSets
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maederunite l = (Set.unions $ map fst l, Set.unions $ map snd l)
56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder-- | get all ids of a basic spec
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Manceids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Manceids_BASIC_SPEC f g (Basic_spec al) =
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance unite $ map (ids_BASIC_ITEMS f g . item) al
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksaids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa -> BASIC_ITEMS b s f -> IdSets
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksaids_BASIC_ITEMS f g bi = case bi of
9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich Sig_items sis -> ids_SIG_ITEMS g sis
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder Free_datatype _ al _ -> ids_anDATATYPE_DECLs al
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al
2dcec0e101ddd4169f5323462911e988337c2deeChristian Maeder Ext_BASIC_ITEMS b -> f b
0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus Luettich _ -> emptyIdSets
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maederids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets
ec25781c1180ea07f66b48c34f93cf5634e9277cChristian Maederids_anDATATYPE_DECLs al =
46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder (Set.unions $ map (ids_DATATYPE_DECL . item) al, Set.empty)
938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz-- | get all ids of a sig items
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederids_SIG_ITEMS f si = case si of
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz Sort_items _ _ _ -> emptyIdSets
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz Op_items al _ -> (Set.unions $ map (ids_OP_ITEM . item) al, Set.empty)
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz Pred_items al _ -> (Set.empty, Set.unions $ map (ids_PRED_ITEM . item) al)
b83ff3749d99d03b641adee264b781039a551addChristian Maeder Datatype_items _ al _ -> ids_anDATATYPE_DECLs al
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Ext_SIG_ITEMS s -> f s
520c5bce318eff52d9315f7c4491c3381a0c4336Christian Maeder-- | get all op ids of an op item
c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maederids_OP_ITEM :: OP_ITEM f -> Set.Set Id
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulzids_OP_ITEM o = case o of
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Op_decl ops _ _ _ -> Set.unions $ map single ops
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Op_defn i _ _ _ -> single i
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz-- | same as singleton
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzsingle :: Id -> Set.Set Id
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz-- | get all pred ids of a pred item
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maederids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maederids_PRED_ITEM p = case p of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Pred_decl preds _ _ -> Set.unions $ map single preds
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder Pred_defn i _ _ _ -> single i
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maederids_DATATYPE_DECL :: DATATYPE_DECL -> Set.Set Id
63719301448519453f66383f4e583d9fd5b89ecbChristian Maederids_DATATYPE_DECL (Datatype_decl _ al _) =
a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maeder Set.unions $ map (ids_ALTERNATIVE . item) al
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulzids_ALTERNATIVE :: ALTERNATIVE -> Set.Set Id
5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulzids_ALTERNATIVE a = case a of
5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz Alt_construct _ i cs _ -> Set.unions $ single i : map ids_COMPONENTS cs
5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz Subsorts _ _ -> Set.empty
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulzids_COMPONENTS :: COMPONENTS -> Set.Set Id
5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulzids_COMPONENTS c = case c of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Cons_select _ l _ _ -> Set.unions $ map single l
48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski-- predicates get lower precedence
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaedermkRule :: Id -> Rule
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaedermkRule = mixRule 1
53e165a53dfa59f717588d1f8236c9a763826525Christian MaedermkSingleArgRule :: Int -> Id -> Rule
53e165a53dfa59f717588d1f8236c9a763826525Christian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
53e165a53dfa59f717588d1f8236c9a763826525Christian MaedermkArgsRule :: Int -> Id -> Rule
53e165a53dfa59f717588d1f8236c9a763826525Christian MaedermkArgsRule b ide = (protect ide, b, getPlainTokenList ide
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ++ getTokenPlaceList tupleId)
08d506ebb78da1e8656a73a349492e042f4c9f72Christian MaedersingleArgId :: Id
08d506ebb78da1e8656a73a349492e042f4c9f72Christian MaedersingleArgId = mkId [exprTok, varTok]
d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian MaedermultiArgsId :: Id
d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian MaedermultiArgsId = mkId (exprTok : getPlainTokenList tupleId)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder-- | additional scan rules
63719301448519453f66383f4e583d9fd5b89ecbChristian MaederaddRule :: GlobalAnnos -> [Rule] -> IdSets -> Token -> [Rule]
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaederaddRule ga uRules (ops, preds) tok =
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz let addR p = Set.fold ( \ i@(Id (t : _) _ _) ->
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz [mixRule p i, mkSingleArgRule p i, mkArgsRule p i])
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz lm = foldr ( \ r@(_, _, t : _) -> Map.insertWith (++) t [r])
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz Map.empty $ listRules 1 ga
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz (spreds, rpreds) = Set.partition isSimpleId preds
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz -- do not add simple ids as preds as these may be variables
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder -- with higher precedence
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder sops = Set.union ops spreds
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder varR = mkRule varId
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder m = Map.insert placeTok uRules
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder $ Map.insert varTok [varR]
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder [varR, mkRule singleArgId, mkRule multiArgsId]
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder $ addR 0 (addR 1 lm sops) rpreds
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder tId = mkId [tok]
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder tPId = mkId [tok, placeTok] -- prefix identifier
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder in (if isSimpleToken tok && not (Set.member tId sops)
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder then [mkRule tId] -- add rule for new variable
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder ++ if Set.member tPId ops || Set.member tPId rpreds then [] else
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder [mkSingleArgRule 1 tId, mkArgsRule 1 tId]
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder -- add also rules for undeclared op
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder else []) ++ Map.findWithDefault [] tok m
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder-- insert only identifiers starting with a place
63719301448519453f66383f4e583d9fd5b89ecbChristian MaederinitRules :: IdSets -> Rules
63719301448519453f66383f4e583d9fd5b89ecbChristian MaederinitRules (opS, predS) =
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let addR p = Set.fold ( \ i l -> mixRule p i : l)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in (addR 1 (addR 0 [mkRule typeId] predS) opS, [])
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder-- | construct rules from 'IdSets' to be put into a 'Mix' record
63719301448519453f66383f4e583d9fd5b89ecbChristian MaedermakeRules :: GlobalAnnos -> IdSets -> (Token -> [Rule], Rules)
63719301448519453f66383f4e583d9fd5b89ecbChristian MaedermakeRules ga (opS, predS) = let
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder (cOps, sOps) = Set.partition begPlace opS
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder (cPreds, sPreds) = Set.partition begPlace $ Set.difference predS opS
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder addR p = Set.fold ( \ i l ->
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder mkSingleArgRule p i : mkArgsRule p i : l)
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder uRules = addR 0 (addR 1 [] cOps) cPreds
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in (addRule ga uRules (sOps, sPreds), initRules (cOps, cPreds))
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder-- | meaningful position of a term
5382091fd2a705e6f026026e8a6adcd3607bdb9fChristian MaederposOfTerm :: GetRange f => TERM f -> Range
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian MaederposOfTerm trm =
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Qual_var v _ ps -> if isNullRange ps then tokPos v else ps
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz Mixfix_term ts -> concatMapRange posOfTerm ts
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder Mixfix_qual_pred p -> posOfId $ predSymbName p
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Application o _ ps -> if isNullRange ps then posOfId $ opSymbName o else ps
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Conditional t1 _ t2 ps ->
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder if isNullRange ps then concatMapRange posOfTerm [t1, t2] else ps
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder Mixfix_parenthesized ts ps ->
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder if isNullRange ps then concatMapRange posOfTerm ts else ps
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Mixfix_bracketed ts ps ->
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder if isNullRange ps then concatMapRange posOfTerm ts else ps
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder Mixfix_braced ts ps ->
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu if isNullRange ps then concatMapRange posOfTerm ts else ps
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu _ -> rangeOfTerm trm
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder-- | construct application
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaederasAppl :: Id -> [TERM f] -> Range -> TERM f
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaederasAppl f args ps = Application (Op_name f) args
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ if isNullRange ps then posOfId f else ps
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder-- | constructing the parse tree from (the final) parser state(s)
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai CodescutoAppl :: GetRange f => Id -> [TERM f] -> Range -> TERM f
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai CodescutoAppl ide ar qs =
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder if ide == singleArgId || ide == multiArgsId
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu then assert (length ar > 1) $
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let har : tar = ar
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder hp = posOfTerm har
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder ps = appRange hp qs
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in case har of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Application q ts p -> assert (null ts) $
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Application q tar $ appRange ps p
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder Mixfix_qual_pred _ ->
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder Mixfix_term [har, Mixfix_parenthesized tar ps]
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder _ -> error "stateToAppl"
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder else asAppl ide ar qs
706201451843aa76b8d862de800570c9838c9910Christian MaederaddType :: TERM f -> TERM f -> TERM f
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaederaddType tt t =
ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder Mixfix_sorted_term s ps -> Sorted_term t s ps
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder Mixfix_cast s ps -> Cast t s ps
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder _ -> error "addType"
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder-- | the type for mixfix resolution
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maedertype MixResolve f = GlobalAnnos -> (Token -> [Rule], Rules) -> f -> Result f
ec351e60425e2f99448cb44e933d3828f8025dddChristian MaederiterateCharts :: (GetRange f, Pretty f) => (f -> f)
ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder -> MixResolve f -> GlobalAnnos -> [TERM f]
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder -> Chart (TERM f) -> Chart (TERM f)
ec351e60425e2f99448cb44e933d3828f8025dddChristian MaederiterateCharts par extR g terms c =
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance let self = iterateCharts par extR g
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance expand = expandPos Mixfix_token
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance oneStep = nextChart addType toAppl g c
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance ruleS = rules c
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance adder = addRules c
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance resolveTerm = resolveMixTrm par extR g (adder, ruleS)
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa in if null terms then c
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa else case head terms of
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa Mixfix_term ts -> self (ts ++ tail terms) c
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa Mixfix_bracketed ts ps ->
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa self (expand ("[", "]") ts ps ++ tail terms) c
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa Mixfix_braced ts ps ->
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa self (expand ("{", "}") ts ps ++ tail terms) c
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa Mixfix_parenthesized ts ps ->
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa [h] -> let Result mds v = resolveTerm h
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder tNew = case v of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder in mixDiags mds c2
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder _ -> self (expand ("(", ")") ts ps ++ tail terms) c
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder h@(Conditional t1 f2 t3 ps) ->
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let Result mds v =
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder do t4 <- resolveTerm t1
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder f5 <- resolveMixFrm par extR g (adder, ruleS) f2
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder t6 <- resolveTerm t3
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder return (Conditional t4 f5 t6 ps)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder tNew = case v of
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder c2 = self (tail terms)
48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder in mixDiags mds c2
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder Mixfix_token t -> let (ds1, trm) = convertMixfixToken
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder (literal_annos g) asAppl Mixfix_token t
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder c2 = self (tail terms) $ oneStep $
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder Mixfix_token tok -> (trm, tok)
6c08e47c4275556c18f4f89521bf21fe94c28dd5Christian Maeder _ -> (trm, varTok)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in mixDiags ds1 c2
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder t@(Mixfix_sorted_term _ ps) -> self (tail terms)
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder (oneStep (t, typeTok {tokPos = ps}))
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder t@(Mixfix_cast _ ps) -> self (tail terms)
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder (oneStep (t, typeTok {tokPos = ps}))
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder t@(Qual_var _ _ ps) -> self (tail terms)
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder (oneStep (t, varTok {tokPos = ps}))
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder t@(Application (Qual_op_name _ _ ps) _ _) ->
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Sorted_term t s ps ->
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let Result mds v = resolveTerm t
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder tNew = Sorted_term (case v of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just x -> x) s ps
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder in mixDiags mds c2
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder _ -> error "iterateCharts"
938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz-- | construct 'IdSets' from op and pred identifiers
3143271856dbf456bd7acc1c07193173f886d986Christian MaedermkIdSets :: Set.Set Id -> Set.Set Id -> IdSets
63719301448519453f66383f4e583d9fd5b89ecbChristian MaedermkIdSets ops preds = (ops, preds)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder-- | top-level resolution like 'resolveMixTrm' that fails in case of diags
63719301448519453f66383f4e583d9fd5b89ecbChristian MaederresolveMixfix :: (GetRange f, Pretty f) => (f -> f)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> MixResolve f -> MixResolve (TERM f)
3143271856dbf456bd7acc1c07193173f886d986Christian MaederresolveMixfix par extR g ruleS t =
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder let r@(Result ds _) = resolveMixTrm par extR g ruleS t
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder in if null ds then r else Result ds Nothing
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder-- | basic term resolution that supports recursion without failure
938677803842b384a91fef21f58f86b8e3188b43Ewaryst SchulzresolveMixTrm :: (GetRange f, Pretty f) => (f -> f)
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder -> MixResolve f -> MixResolve (TERM f)
3143271856dbf456bd7acc1c07193173f886d986Christian MaederresolveMixTrm par extR ga (adder, ruleS) trm =
56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder getResolved (showTerm par ga) (posOfTerm trm) toAppl
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa $ iterateCharts par extR ga [trm] $ initChart adder ruleS
3143271856dbf456bd7acc1c07193173f886d986Christian MaedershowTerm :: Pretty f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
3143271856dbf456bd7acc1c07193173f886d986Christian MaedershowTerm par ga = showGlobalDoc ga . mapTerm par
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder-- | top-level resolution like 'resolveMixFrm' that fails in case of diags
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian MaederresolveFormula :: (GetRange f, Pretty f) => (f -> f)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> MixResolve f -> MixResolve (FORMULA f)
63719301448519453f66383f4e583d9fd5b89ecbChristian MaederresolveFormula par extR g ruleS f =
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let r@(Result ds _) = resolveMixFrm par extR g ruleS f
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder in if null ds then r else Result ds Nothing
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder-- | basic formula resolution that supports recursion without failure
1937dccb04b363364f7a7de17fdaae1d70583af9Christian MaederresolveMixFrm :: (GetRange f, Pretty f) => (f -> f)
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder -> MixResolve f -> MixResolve (FORMULA f)
3143271856dbf456bd7acc1c07193173f886d986Christian MaederresolveMixFrm par extR g ids frm =
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let self = resolveMixFrm par extR g ids
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder resolveTerm = resolveMixTrm par extR g ids in
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder Quantification q vs fOld ps ->
ef4c609cebc5260771dae6e4f3a54a8959e81ed9Christian Maeder do fNew <- resolveMixFrm par extR g ids fOld
180ab8c3df8cb0c88f0e881bca93354df6b5d560Christian Maeder return $ Quantification q vs fNew ps
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Conjunction fsOld ps ->
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder do fsNew <- mapM self fsOld
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder return $ Conjunction fsNew ps
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Disjunction fsOld ps ->
efb44558d78b59ea6ce8c16cb5eb1ac0a2604c84Christian Maeder do fsNew <- mapM self fsOld
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder return $ Disjunction fsNew ps
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder Implication f1 f2 b ps ->
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder do f3 <- self f1
ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder f4 <- self f2
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder return $ Implication f3 f4 b ps
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Equivalence f1 f2 ps ->
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder do f3 <- self f1
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder f4 <- self f2
fb37a248ebad4696bbc9d9b94ce1cfc6497a9160Christian Maeder return $ Equivalence f3 f4 ps
fb37a248ebad4696bbc9d9b94ce1cfc6497a9160Christian Maeder Negation fOld ps ->
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder do fNew <- self fOld
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder return $ Negation fNew ps
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder Predication sym tsOld ps ->
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder do tsNew <- mapM resolveTerm tsOld