MixfixParser.hs revision 8dddde4041af20b71009e6092440fc393f91666a
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Author: Christian Maeder
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Mixfix analysis of terms
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder Missing features:
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder - the positions of Ids from %string, %list, %number and %floating annotations
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder is not changed within applications (and might be misleading)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder - using (Set State) instead of [State] avoids explosion
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder but detection of local ambiguities (that of subterms) is more difficult
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder solution: equal list states should be merged into a single state
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder that stores the local ambiguity
3ec187613707411408c677058155bc618f16dabbChristian Maedermodule CASL.MixfixParser ( resolveFormula, resolveMixfix)
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maederimport Common.Lib.Map as Map hiding (filter, split, map)
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maederimport Common.Lib.Set as Set hiding (filter, split, single, insert)
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport qualified Char as C
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maederimport Data.List(intersperse)
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maederimport CASL.Formula(updFormulaPos)
4f6bf9805777b4c9b263f647a3fa97c8daeb54b2Christian Maederimport qualified CASL.ShowMixfix as ShowMixfix (showTerm)
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian MaedershowTerm :: GlobalAnnos -> TERM -> String
0ca0057165c510ada537b23f6797c770a51990e3Christian MaedershowTerm _ t = ShowMixfix.showTerm t ""
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder-- Earley Algorithm
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederdata IdKind = IsPred | IsOp | IsBoth deriving (Eq, Ord)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederdata State = State (Id, IdKind) -- True means predicate
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder [Pos] -- positions of Id tokens
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder [TERM] -- currently collected arguments
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder -- both in reverse order
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder [Token] -- only tokens after the "dot" are given
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Int -- index into the ParseMap/input string
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederinstance Eq State where
97061dace53e199664c3ec5da6434b8cd46b58dfChristian Maeder State r1 _ _ t1 p1 == State r2 _ _ t2 p2 = (r1, t1, p1) == (r2, t2, p2)
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederinstance Ord State where
97061dace53e199664c3ec5da6434b8cd46b58dfChristian Maeder State r1 _ _ t1 p1 <= State r2 _ _ t2 p2 = (r1, t1, p1) <= (r2, t2, p2)
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian MaedertermStr :: String
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian MaedertermStr = "(T)"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercommaTok, parenTok, termTok :: Token
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercommaTok = mkSimpleId "," -- for list elements
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian MaedertermTok = mkSimpleId termStr
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederparenTok = mkSimpleId "(..)"
9256f871e7dd915ccfb5969e2117f054306cd366Christian MaedercolonTok, asTok, varTok, opTok, predTok :: Token
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedercolonTok = mkSimpleId ":"
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederasTok = mkSimpleId "as"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedervarTok = mkSimpleId "(v)"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederopTok = mkSimpleId "(o)"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederpredTok = mkSimpleId "(p)"
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkState :: Int -> IdKind -> Id -> State
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkState i b ide = State (ide, b) [] [] (getTokenList termStr ide) i
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkApplState :: Int -> IdKind -> Id -> State
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkApplState i b ide = State (ide, b) [] []
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maeder (getTokenList place ide ++ [parenTok]) i
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederlistToken :: Token
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederlistToken = mkSimpleId "[]"
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederlistId :: Id -> Id
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder-- unique id (usually "[]" yields two tokens)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederlistId i = Id [listToken] [i] []
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian MaederisListId :: Id -> Bool
0cc809b79c4276013d0325bedbc33c4244d32705Christian MaederisListId (Id ts cs _) = not (null ts) && head ts == listToken && length cs == 1
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederlistStates :: GlobalAnnos -> Int -> [State]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederlistStates g i =
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder let lists = list_lit $ literal_annos g
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder listState co toks = State (listId co, IsOp) [] [] toks i
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder in concatMap ( \ (bs, n, c) ->
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder let (b1, b2, cs) = getListBrackets bs
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder e = Id (b1 ++ b2) cs [] in
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder (if e == n then [] -- add b1 ++ b2 if its not yet included by n
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder else [listState c $ getTokenList place e]) ++
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder [listState c (b1 ++ [termTok] ++ b2)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder , listState c (b1 ++ [termTok, commaTok] ++ b2)]
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- these are the possible matches for the nonterminal TERM
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- the same states are used for the predictions
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederinitialState :: GlobalAnnos -> ([Id], [Id], [Id]) -> Int -> [State]
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederinitialState g (ops, preds, both) i =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let mkPredState b toks = State (Id toks [] [], b) [] [] toks i
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder mkTokState = mkPredState IsOp
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder in concat [mkTokState [parenTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [termTok, colonTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [termTok, asTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [varTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [opTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [opTok, parenTok] :
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder mkPredState IsPred [predTok] :
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder mkPredState IsPred [predTok, parenTok] :
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder listStates g i,
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder map (mkState i IsBoth) both,
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder map (mkApplState i IsBoth) both,
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder map (mkState i IsPred) preds,
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder map (mkApplState i IsPred) preds,
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder map (mkState i IsOp) ops,
7bbd71619608c6b19535818ebf628ba04fe55f91Christian Maeder map (mkApplState i IsOp) ops]
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian Maedertype ParseMap = Map Int [State]
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian MaederlookUp :: (Ord a, MonadPlus m) => Map a (m b) -> a -> (m b)
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian MaederlookUp ce k = findWithDefault mzero k ce
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- match (and shift) a token (or partially finished term)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederscan :: TERM -> Int -> ParseMap -> ParseMap
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederscan trm i m =
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder let t = case trm of
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_token x -> x
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_sorted_term _ _ -> colonTok
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_cast _ _ -> asTok
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_parenthesized _ _ -> parenTok
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Application (Qual_op_name _ _ _) [] _ -> opTok
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder Mixfix_qual_pred _ -> predTok
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder foldr (\ (State o b a ts k) l ->
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if null ts || head ts /= t then l
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else let p = tokPos t : b in
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if t == commaTok && isListId (fst o) then
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder -- list elements separator
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (termTok : commaTok : tail ts) k)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder : (State o p a (termTok : tail ts) k) : l
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder else if t == parenTok then
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (State o b (trm : a) (tail ts) k) : l
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder else if t == varTok || t == opTok || t == predTok then
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder (State o b [trm] (tail ts) k) : l
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder else if t == colonTok || t == asTok then
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (State o b [mkTerm $ head a] [] k) : l
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else (State o p a (tail ts) k) : l) []
d21f1db14625cb0a536fc06b46fcc115d48a25bbChristian Maeder (lookUp m i)) m
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder where mkTerm t1 = case trm of
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_sorted_term s ps -> Sorted_term t1 s ps
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_cast s ps -> Cast t1 s ps
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- precedence graph stuff
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedercheckArg :: GlobalAnnos -> AssocEither -> Id -> Id -> Bool
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedercheckArg g dir op arg =
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder then isAssoc dir (assoc_annos g) op || not (isInfix op)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case precRel (prec_annos g) op arg of
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Lower -> True
dd38bafd384f5a5bc9634aad395505a0fd74395aChristian Maeder NoDirection -> not $ isInfix arg
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedercheckAnyArg :: GlobalAnnos -> Id -> Id -> Bool
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedercheckAnyArg g op arg =
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case precRel (prec_annos g) op arg of
dd38bafd384f5a5bc9634aad395505a0fd74395aChristian Maeder BothDirections -> isInfix op && op == arg
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederisLeftArg, isRightArg :: Id -> Int -> Bool
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederisLeftArg (Id ts _ _) n = n + 1 == (length $ takeWhile isPlace ts)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederisRightArg (Id ts _ _) n = n == (length $ filter isPlace ts) -
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (length $ takeWhile isPlace (reverse ts))
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederfilterByPrec :: GlobalAnnos -> State -> State -> Bool
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederfilterByPrec _ _ (State _ _ _ [] _) = False
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederfilterByPrec g (State (argIde, predArg) _ _ _ _)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder (State (opIde, predOp) _ args (hd:_) _) =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if hd == termTok then
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if predArg == IsPred
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder else if isListId opIde || isListId argIde || predOp == IsPred
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder then True else
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let n = length args in
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder if isLeftArg opIde n then
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder if isPostfix opIde && (isPrefix argIde
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder || isInfix argIde) then False
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder else checkArg g ALeft opIde argIde
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder else if isRightArg opIde n then
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder if isPrefix opIde && isInfix argIde then False
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder else checkArg g ARight opIde argIde
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder else checkAnyArg g opIde argIde
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- reconstructing positions
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedersetPlainIdePos :: Id -> [Pos] -> (Id, [Pos])
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedersetPlainIdePos (Id ts cs _) ps =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let (places, toks) = span isPlace (reverse ts)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder pls = reverse places
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder f = zipWith (\ a b -> up_pos (const b) a)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (ps1, ps2) = splitAt (length toks) ps
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder front = f (reverse toks) ps1
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in if null cs then
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let (ps3, ps4) = splitAt (length pls) ps2
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in (Id (front ++ f pls ps3) [] [], ps4)
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder else let (newCs, ps3, ps4) = foldl (\ (prevCs, seps, rest) a ->
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let (c1, qs) = setPlainIdePos a rest
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in (c1: prevCs, head qs : seps, tail qs))
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ([], [head ps2], tail ps2) cs
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder (ps6, ps7) = splitAt (length pls) ps4
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder in (Id (front ++ f pls ps6) (reverse newCs) (reverse ps3), ps7)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedersetIdePos :: Id -> [TERM] -> [Pos] -> Id
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedersetIdePos i@(Id ts _ _) ar ps =
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maeder let nt = length $ getTokenList place i
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder np = length ps
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder na = length $ filter isPlace ts
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (_, toks) = span isPlace (reverse ts)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in if nt == np then -- literal places
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let (newId, []) = setPlainIdePos i ps
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else if np + na == nt && na == length ar then -- mixfix
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let (newTps, rargs, rqs) = mergePos (reverse toks) ar ps
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (newId, []) = setPlainIdePos i
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (newTps ++ rqs ++ map posOfTerm rargs)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else error "setIdePos"
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder where mergePos [] args qs = ([], args, qs)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mergePos (t:rs) args qs =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if isPlace t then
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let (tokps, rargs, rqs) = mergePos rs (tail args) qs
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in (posOfTerm (head args) : tokps, rargs, rqs)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else let (tokps, rargs, rqs) = mergePos rs args (tail qs)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in (head qs : tokps, rargs, rqs)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- constructing the parse tree from (the final) parser state(s)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederstateToAppl :: State -> TERM
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederstateToAppl (State (ide, _) rs a _ _) =
f161da699d7e8eddbb9294618dbc7a54966d7f7fChristian Maeder let vs = getTokenList place ide
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder ar = reverse a
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder qs = reverse rs
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in if vs == [termTok, colonTok]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder || vs == [termTok, asTok]
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder || vs == [varTok]
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder || vs == [opTok]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder || vs == [predTok]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder || vs == [parenTok]
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder then case head ar of
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder Mixfix_parenthesized ts _ -> if length ts == 1 then head ts
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else if vs == [opTok, parenTok]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder then let Application q _ _ = head ar
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_parenthesized ts ps = head a
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in Application q ts ps
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else if vs == [predTok, parenTok]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder then Mixfix_term [head ar, head a]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else case ar of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder [Mixfix_parenthesized ts ps] ->
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder Application (Op_name
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (setIdePos ide ts qs))
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder _ -> let newIde@(Id (t:_) _ _) = setIdePos ide ar qs
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder pos = if isPlace t then posOfTerm $ head ar
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder else tokPos t
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder in Application (Op_name newIde) ar [pos]
215b5e40dadbe65b1b225b1b80e2c529ef00bebcChristian Maeder -- true mixfix
9987d35a267440c71e1e8b21c2ee6081a6390643Christian MaederasListAppl :: GlobalAnnos -> State -> TERM
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederasListAppl g s@(State (i,_) bs a _ _) =
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder if isListId i then
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder let Id _ [f] _ = i
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder ListCons b c = getLiteralType g f
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder (b1, _, _) = getListBrackets b
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder cl = length $ getTokenList place b
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder nb1 = length b1
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ra = reverse a
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder na = length ra
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder nb = length bs
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder mkList [] ps = asAppl c [] (head ps)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder mkList (hd:tl) ps = asAppl f [hd, mkList tl (tail ps)] (head ps)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder in if null a then asAppl c [] (if null bs then nullPos else last bs)
950766f1e2b0a1f7e502982c7dacfbf96ec3cb3aChristian Maeder else if nb + 2 == cl + na then
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let br = reverse bs
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder br1 = drop (nb1 - 1) br
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder in mkList (reverse a) br1
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else error "asListAppl"
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else stateToAppl s
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- when a grammar rule (mixfix Id) has been fully matched
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedercollectArg :: GlobalAnnos -> ParseMap -> State -> [State]
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- pre: finished rule
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedercollectArg g m s@(State _ _ _ _ k) =
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder map (\ (State o b a ts k1) ->
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder State o b (asListAppl g s : a)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (tail ts) k1)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder $ filter (filterByPrec g s)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maedercompl :: GlobalAnnos -> ParseMap -> [State] -> [State]
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder concat $ map (collectArg g m)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder $ filter (\ (State _ _ _ ts _) -> null ts) l
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedercomplRec :: GlobalAnnos -> ParseMap -> [State] -> [State]
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedercomplRec g m l =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let l1 = compl g m l in
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if null l1 then l else complRec g m l1 ++ l
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maedercomplete :: GlobalAnnos -> Int -> ParseMap -> ParseMap
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maedercomplete g i m =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder Map.insert i (complRec g m $ lookUp m i) m
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- predict which rules/ids might match for (the) nonterminal(s) (termTok)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- provided the "dot" is followed by a nonterminal
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederpredict :: GlobalAnnos -> [Id] -> Int -> ParseMap -> ParseMap
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maederpredict g ops i m =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if i /= 0 && any (\ (State _ _ _ ts _) -> not (null ts)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder && head ts == termTok) (lookUp m i)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder then insertWith (++) i (initialState g (ops, [], []) i) m
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maedertype Chart = (Int, [Diagnosis], ParseMap)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedernextState :: GlobalAnnos -> [Id] -> TERM
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -> Chart -> Chart
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedernextState g ops trm (i, ds, m) =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let m1 = complete g (i+1) $
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder predict g ops i m
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder in if null (lookUp m1 (i+1)) && null ds
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder then (i+1, Diag Error ("unexpected mixfix token: "
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder ++ showTerm g trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm trm) : ds, m)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else (i+1, ds, m1)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maedertype IdSet = (Set Id, Set Id, Set Id)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederiterateStates :: GlobalAnnos -> IdSet -> Bool -> [TERM] -> Chart -> Chart
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederiterateStates g ids@(ops,_,both) maybeFormula terms c@(i, ds, m) =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let self = iterateStates g ids maybeFormula
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder expand = expandPos Mixfix_token
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder oneStep = nextState g (Set.toList $ Set.union ops both)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder resolvePred = resolveMixTrm g ids
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder resolveTerm = resolvePred maybeFormula
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in if null terms then c
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder else case head terms of
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_term ts -> self (ts ++ tail terms) c
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_bracketed ts ps ->
469af98c69977faf5666e689eae863c1606ce269Christian Maeder self (expand ("[", "]") ts ps ++ tail terms) c
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_braced ts ps ->
469af98c69977faf5666e689eae863c1606ce269Christian Maeder self (expand ("{", "}") ts ps ++ tail terms) c
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder Mixfix_parenthesized ts ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let Result mds v =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tsNew <- mapM resolveTerm ts
accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder return $ Mixfix_parenthesized tsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder tNew = case v of Nothing -> head terms
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder in self (tail terms) (oneStep tNew (i, ds++mds, m))
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Conditional t1 f2 t3 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let Result mds v =
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder do t4 <- resolvePred False t1
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder f5 <- resolveMixFrm g ids f2
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder t6 <- resolvePred False t3
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (Conditional t4 f5 t6 ps)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder tNew = case v of Nothing -> head terms
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder in self (tail terms) (oneStep tNew (i, ds++mds, m))
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Mixfix_token t -> let (ds1, trm) =
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder convertMixfixToken (literal_annos g) t
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder in self (tail terms)
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder (oneStep trm (i, ds1++ds, m))
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder t -> self (tail terms) (oneStep t c)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaederposOfTerm :: TERM -> Pos
5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaederposOfTerm trm =
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_token t -> tokPos t
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_term ts -> posOfTerm (head ts)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Simple_id i -> tokPos i
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Mixfix_qual_pred p ->
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Pred_name i -> posOfId i
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Qual_pred_name _ _ ps -> first (Just ps)
05b5fdc3a64b84276a9792c1df60b2c48c1738bdChristian Maeder Application (Qual_op_name _ _ ps) [] [] -> first (Just ps)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder _ -> first $ get_pos_l trm
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder where first ps = case ps of
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Nothing -> nullPos
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Just l -> if null l then nullPos else head l
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedergetAppls :: GlobalAnnos -> Int -> ParseMap -> [TERM]
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedergetAppls g i m =
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder map (asListAppl g) $
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder filter (\ (State _ _ _ ts k) -> null ts && k == 0) $
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkIdSet :: Set Id -> Set Id -> IdSet
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkIdSet ops preds =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let both = Set.intersection ops preds in
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder (Set.difference ops both, Set.difference preds both, both)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederresolveMixfix :: GlobalAnnos -> Set Id -> Set Id -> Bool -> TERM -> Result TERM
8dddde4041af20b71009e6092440fc393f91666aChristian MaederresolveMixfix g ops preds maybeFormula t =
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder let r@(Result ds _) = resolveMixTrm g (mkIdSet ops preds) maybeFormula t
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder in if null ds then r else Result ds Nothing
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederresolveMixTrm :: GlobalAnnos -> IdSet -> Bool
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -> TERM -> Result TERM
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederresolveMixTrm g ids@(ops, preds, both) mayBeFormula trm =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let (i, ds, m) = iterateStates g ids mayBeFormula [trm]
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder (0, [], Map.single 0 $ initialState g
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder (if mayBeFormula then (Set.toList ops,
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder else (Set.toList $ Set.union ops both, [], [])) 0)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder ts = getAppls g i m
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in if null ts then if null ds then
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder plain_error trm ("no resolution for term: "
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder ++ showTerm g trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else Result ds (Just trm)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else if null $ tail ts then Result ds (Just (head ts))
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder else Result (Diag Error ("ambiguous mixfix term\n\t" ++
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ intersperse "\n\t"
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder $ map (showTerm g)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder $ take 5 ts)) (posOfTerm trm) : ds) (Just trm)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederresolveFormula :: GlobalAnnos -> Set Id -> Set Id -> FORMULA -> Result FORMULA
8dddde4041af20b71009e6092440fc393f91666aChristian MaederresolveFormula g ops preds f =
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder let r@(Result ds _) = resolveMixFrm g (mkIdSet ops preds) f
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder in if null ds then r else Result ds Nothing
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederresolveMixFrm :: GlobalAnnos -> IdSet-> FORMULA -> Result FORMULA
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederresolveMixFrm g ids@(ops, preds, both) frm =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let self = resolveMixFrm g ids
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder resolveTerm = resolveMixTrm g ids False in
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Quantification q vs fOld ps ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let varIds = Set.fromList $ concatMap (\ (Var_decl va _ _) ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder map simpleIdToId va) vs
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder vps = Set.intersection varIds preds
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder newBoth = Set.union both vps
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder newIds = ((Set.\\) (Set.union ops varIds) newBoth,
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder (Set.\\) preds vps, newBoth)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder do fNew <- resolveMixFrm g newIds fOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Quantification q vs fNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Conjunction fsOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fsNew <- mapM self fsOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Conjunction fsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Disjunction fsOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fsNew <- mapM self fsOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Disjunction fsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Implication f1 f2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do f3 <- self f1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f4 <- self f2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Implication f3 f4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Equivalence f1 f2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do f3 <- self f1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f4 <- self f2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Equivalence f3 f4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Negation fOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fNew <- self fOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Negation fNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Predication sym tsOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tsNew <- mapM resolveTerm tsOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication sym tsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Definedness tOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tNew <- resolveTerm tOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Definedness tNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Existl_equation t1 t2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do t3 <- resolveTerm t1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t4 <- resolveTerm t2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Existl_equation t3 t4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Strong_equation t1 t2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do t3 <- resolveTerm t1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t4 <- resolveTerm t2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Strong_equation t3 t4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Membership tOld s ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tNew <- resolveTerm tOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Membership tNew s ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_formula tOld ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder do tNew <- resolveMixTrm g ids True tOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder mkPredication tNew
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder where mkPredication t =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_parenthesized [t0] ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do p <- mkPredication t0
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ if null ps then p
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else updFormulaPos (head ps) (last ps) p
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Application (Op_name ide) args ps ->
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let p = Predication (Pred_name ide) args ps in
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder if ide `Set.member` preds || ide `Set.member` both
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder then return p else
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder plain_error p
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ("not a predicate: " ++ showId ide "")
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (posOfTerm t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_qual_pred qide ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication qide [] []
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_term [Mixfix_qual_pred qide,
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_parenthesized ts ps] ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication qide ts ps
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Mixfix_term _ -> return $ Mixfix_formula t -- still wrong
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder _ -> plain_error (Mixfix_formula t)
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder ("not a formula: " ++ showTerm g t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (posOfTerm t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- convert literals
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeStringTerm :: Id -> Id -> Token -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeStringTerm c f tok =
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeStrTerm (incSourceColumn sp 1) str
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder sp = tokPos tok
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder str = init (tail (tokStr tok))
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeStrTerm p l =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if null l then asAppl c [] p
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder else let (hd, tl) = splitString caslChar l
a5023d78ecc3452c0de580912e7bd018640ddeaaChristian Maeder in asAppl f [asAppl (Id [Token ("'" ++ hd ++ "'") p] [] []) [] p,
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeStrTerm (incSourceColumn p $ length hd) tl] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeNumberTerm :: Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeNumberTerm f t@(Token n p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeNumberTerm"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [_] -> asAppl (Id [t] [] []) [] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] p,
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeNumberTerm f (Token tl
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder (incSourceColumn p 1))] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFraction :: Id -> Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeFraction f d t@(Token s p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let (n, r) = span (\c -> c /= '.') s
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder dotOffset = length n
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in if null r then makeNumberTerm f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else asAppl d [makeNumberTerm f (Token n p),
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeNumberTerm f (Token (tail r)
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder (incSourceColumn p $ dotOffset + 1))]
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder $ incSourceColumn p dotOffset
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeSignedNumber :: Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeSignedNumber f t@(Token n p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeSignedNumber"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if hd == '-' || hd == '+' then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder asAppl (Id [Token [hd] p] [] [])
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder [makeNumberTerm f (Token tl $ incSourceColumn p 1)] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else makeNumberTerm f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFloatTerm :: Id -> Id -> Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeFloatTerm f d e t@(Token s p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let (m, r) = span (\c -> c /= 'E') s
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder offset = length m
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in if null r then makeFraction f d t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else asAppl e [makeFraction f d (Token m p),
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeSignedNumber f (Token (tail r)
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder $ incSourceColumn p (offset + 1))]
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder $ incSourceColumn p offset
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederasAppl :: Id -> [TERM] -> Pos -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederasAppl f args p = let pos = if null args then [] else [p]
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in Application (Op_name f) args pos
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder-- analyse Mixfix_token
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaederconvertMixfixToken:: LiteralAnnos -> Token -> ([Diagnosis], TERM)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederconvertMixfixToken ga t =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if isString t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case string_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "string"
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just (c, f) -> ([], makeStringTerm c f t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else if isNumber t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case number_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "number"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Just f -> if isFloating t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case float_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "floating"
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just (d, e) -> ([], makeFloatTerm f d e t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else ([], makeNumberTerm f t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else ([], te)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder where te = Mixfix_token t
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder err s = ([Diag Error ("missing %" ++ s ++ " annotation") (tokPos t)]