MixfixParser.hs revision 215b5e40dadbe65b1b225b1b80e2c529ef00bebc
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Author: Christian Maeder
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Mixfix analysis of terms
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maedermodule MixfixParser where
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport AS_Basic_CASL
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport GlobalAnnotations
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maederimport FiniteMap
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maederimport Lexer (caslChar)
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maederimport ParsecPrim
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport qualified Char as C
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederimport List(intersperse)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder-- for testing
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederimport Formula
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport PrettyPrint
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport Print_AS_Basic
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport GlobalAnnotationsFunctions
e69bfc714e534d71322f504dde433941142e1c05Christian Maederimport Anno_Parser
e69bfc714e534d71322f504dde433941142e1c05Christian Maeder-- precedence graph stuff
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaedercheckArg :: GlobalAnnos -> AssocEither -> Id -> Id -> Bool
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaedercheckArg g dir op arg =
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder then isAssoc dir (assoc_annos g) op || not (isInfix op)
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder case precRel (prec_annos g) op arg of
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder Lower -> True
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder Higher -> False
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder ExplGroup BothDirections -> False
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder ExplGroup NoDirection -> not $ isInfix arg
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaedercheckAnyArg :: GlobalAnnos -> Id -> Id -> Bool
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaedercheckAnyArg g op arg =
b26211de8c1e50efbabbb95497e7508c4d852634Christian Maeder case precRel (prec_annos g) op arg of
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian Maeder ExplGroup BothDirections -> isInfix op && op == arg
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder-- Earley Algorithm
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder-- after matching one place literally all places must match literally
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder-- and arguments must follow in parenthesis
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maederdata State = State { rule :: Id
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , posList :: [Pos] -- positions of Id tokens
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder , arglist :: [TERM] -- currently collected arguments
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder -- both in reverse order
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder , dotPos :: [Token]
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder , rulePos :: Int
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederinstance Eq State where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder State r1 _ _ t1 p1 == State r2 _ _ t2 p2 =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder r1 == r2 && t1 == t2 && p1 == p2
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maederinstance Ord State where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder State r1 _ _ t1 p1 <= State r2 _ _ t2 p2 =
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder if r1 == r2 then
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if t1 == t2 then p1 <= p2
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder else t1 <= t2
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder else r1 <= r2
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederinstance Show State where
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder showsPrec _ (State r _ _ d p) = showChar '{'
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder . showSepList (showString "") showTok first
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder . showChar '.'
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder . showSepList (showString "") showTok d
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder . shows p . showChar '}'
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder where first = take (length v - length d) v
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder v = getTokenList True r
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederinstance (Show a) => Show (Set a) where
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder showsPrec _ = shows . setToList
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercommaTok, parenTok, termTok :: Token
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedercommaTok = mkSimpleId "," -- for list elements
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedertermTok = mkSimpleId "(T)"
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)"
5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaederexpandPos :: (Token -> a) -> String -> String -> [a] -> [Pos] -> [a]
5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaederexpandPos f o c ts ps =
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder let n = length ts
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder j = length ps
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder cutOuterPos i l = let k = length l in
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder if k == i+1 then l
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder else cutOuterPos (i - 2)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder $ init (tail l)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder ps1 = if j > n && even (j - (n+1)) then cutOuterPos n ps
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder else if j > 1 then
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder head ps : replicate (n - 1) nullPos
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder else replicate (n + 1) nullPos
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder (zipWith Token (o : replicate (n - 1) "," ++ [c]) ps1)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder in head seps : concat (zipWith (\ t s -> [t,s]) ts (tail seps))
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedergetTokenList :: Bool -> Id -> [Token]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedergetTokenList asLiteral (Id ts cs ps) =
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder let (pls, toks) = span isPlace (reverse ts)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder cts = if null cs then [] else concat
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder $ expandPos (:[]) "[" "]" (map (getTokenList True) cs) ps
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder -- although positions will be replaced (by scan)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder convert = if asLiteral then reverse else
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder map (\ t -> if isPlace t then termTok else t) . reverse
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in convert toks ++ cts ++ convert pls
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaedermkState :: Int -> Id -> State
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedermkState i ide = State ide [] [] (getTokenList False ide) i
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaedermkApplState :: Int -> Id -> State
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedermkApplState i ide = State ide [] []
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (getTokenList True ide ++ [parenTok]) i
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder-- unique id (usually "[]" yields two tokens)
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederlistId = Id [mkSimpleId "[]"] [] []
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian MaederlistStates :: GlobalAnnos -> Int -> Set State
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederlistStates g i =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let listState toks = State listId [] [] toks i
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in case list_lit (literal_annos g) of
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder Nothing -> emptySet
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder Just (Id b _ _, _, _) ->
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder let (b1, rest) = break isPlace b
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder b2 = if null rest then []
6eed7cde6b75d63ec6b8f7e31caac6919558a676Christian Maeder else filter (not . isPlace) rest
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in mkSet [ listState (b1 ++ b2)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , listState (b1 ++ [termTok] ++ b2)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , listState (b1 ++ [termTok, commaTok] ++ b2)]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederinitialState :: GlobalAnnos -> Set Id -> Int -> Set State
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederinitialState g is i =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let mkTokState toks = State (Id toks [] []) [] [] toks i
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in mapSet (mkApplState i) is `union`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mapSet (mkState i) is `union`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder listStates g i `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [parenTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [termTok, colonTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [termTok, asTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [varTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [opTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [opTok, parenTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [predTok] `addToSet`
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder mkTokState [predTok, parenTok]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maedertype ParseMap = FiniteMap Int (Set State)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederlookUp :: (Ord key) => FiniteMap key (Set a) -> key -> Set a
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederlookUp m i = lookupWithDefaultFM m emptySet i
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
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder addToFM m (i+1) (mkSet $
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
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if t == commaTok then -- 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) []
70ca840c8a6cf3591d5f9aa9a3de6fae42d696e8Christian Maeder (setToList $ lookUp m i))
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
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maedercompl :: GlobalAnnos -> ParseMap -> [State] -> [State]
e69bfc714e534d71322f504dde433941142e1c05Christian Maeder concat $ map (collectArg g m)
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder $ filter (\ (State _ _ _ ts _) -> null ts) l
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedercollectArg :: GlobalAnnos -> ParseMap -> State -> [State]
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder-- pre: finished rule
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaedercollectArg g m s@(State _ _ _ _ k) =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder map (\ (State o b a ts k1) ->
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder State o b (asListAppl g s : a)
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder (tail ts) k1)
e69bfc714e534d71322f504dde433941142e1c05Christian Maeder $ filter (filterByPrec g s)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder $ setToList $ lookUp m k
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaederfilterByPrec :: GlobalAnnos -> State -> State -> Bool
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederfilterByPrec _ _ (State _ _ _ [] _) = False
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederfilterByPrec g (State argIde _ _ _ _) (State opIde _ args (hd:ts) _) =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if hd == termTok then
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder if opIde == listId || argIde == listId then True
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else if not (null ts) && head ts == commaTok then True
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder else 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
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian MaederisLeftArg, isRightArg :: Id -> Int -> Bool
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian MaederisLeftArg (Id ts _ _) n = n + 1 == (length $ takeWhile isPlace ts)
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian MaederisRightArg (Id ts _ _) n = n == (length $ filter isPlace ts) -
c8bf82bdb27dfa58f7f05045c639c14276be3333Christian Maeder (length $ takeWhile isPlace (reverse ts))
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)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder else let (newCs, ps3, ps4) = foldr (\ a (prevCs, seps, rest) ->
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
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder ps5 = tail ps4
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (ps6, ps7) = splitAt (length pls) ps5
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in (Id (front ++ f pls ps6)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (reverse newCs)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder (reverse (head ps4 : ps3)), ps7)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedersetIdePos :: Id -> [TERM] -> [Pos] -> Id
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaedersetIdePos i@(Id ts _ _) ar ps =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let nt = length $ getTokenList True 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)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederstateToAppl :: State -> TERM
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederstateToAppl (State ide rs a _ _) =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let vs = getTokenList True 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]
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
9987d35a267440c71e1e8b21c2ee6081a6390643Christian MaederasListAppl g s@(State i _ a _ _) =
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder case list_lit $ literal_annos g of
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Nothing -> stateToAppl s
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder Just (_, c, f) ->
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder if i == listId then mkList (reverse a)
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder else stateToAppl s
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder where mkList [] = asAppl c [] nullPos
9987d35a267440c71e1e8b21c2ee6081a6390643Christian Maeder mkList (hd:tl) = asAppl f [hd, mkList tl] nullPos
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedercomplRec :: GlobalAnnos -> ParseMap -> [State] -> [State]
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedercomplRec g m l = let l1 = compl g m l in
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder if null l1 then l else complRec g m l1 ++ l
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maedercomplete :: GlobalAnnos -> Int -> ParseMap -> ParseMap
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maedercomplete g i m = addToFM m i $ mkSet $ complRec g m $ setToList $ lookUp m i
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maederpredict :: GlobalAnnos -> Set Id -> Int -> ParseMap -> ParseMap
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maederpredict g is i m = if any (\ (State _ _ _ ts _) -> not (null ts)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder && head ts == termTok)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder (setToList $ lookUp m i)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder then addToFM_C union m i (initialState g is i)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maedertype Chart = (Int, [Diagnosis], ParseMap)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedernextState :: GlobalAnnos -> Set Id -> TERM -> Chart -> Chart
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedernextState g is trm (i, ds, m) =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let m1 = complete g (i+1) $
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder predict g is i m
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in if isEmptySet $ lookUp m1 (i+1)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder then (i+1, Error ("unexpected term or token: "
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ show (printText0 g trm))
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm trm) : ds, m)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else (i+1, ds, m1)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederiterateStates :: GlobalAnnos -> Set Id -> Set Id -> [TERM] -> Chart -> Chart
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederiterateStates g ops preds terms c@(i, ds, m) =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let self = iterateStates g ops preds
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder resolveTerm = resolveMixfix g ops preds False
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 ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder self (expand "[" "]" ts ps ++ tail terms) c
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_braced ts ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian 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
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (Mixfix_parenthesized tsNew ps)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder tNew = case v of Nothing -> head terms
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in self (tail terms) (nextState g ops tNew (i, ds++mds, m))
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Conditional t1 f2 t3 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let Result mds v =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do t4 <- resolveTerm t1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f5 <- resolveFormula g ops preds f2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t6 <- resolveTerm t3
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (Conditional t4 f5 t6 ps)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder tNew = case v of Nothing -> head terms
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in self (tail terms) (nextState g ops tNew (i, ds++mds, m))
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t -> self (tail terms) (nextState g ops t c)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder where expand = expandPos Mixfix_token
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
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_qual_pred _ -> nullPos
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder _ -> case get_pos_l trm of
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Nothing -> nullPos
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian 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) $
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder setToList $ lookUp m i
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederresolveMixfix :: GlobalAnnos -> Set Id -> Set Id -> Bool -> TERM -> Result TERM
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederresolveMixfix g ops preds mayBeFormula trm =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let (i, ds, m) = iterateStates g ops preds [trm]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (0, [], unitFM 0 $ initialState g
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (if mayBeFormula then ops `union` preds else ops) 0)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder ts = getAppls g i m
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder in if null ts then if null ds then
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder non_fatal_error trm ("no resolution for term: "
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ++ show (printText0 g trm))
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else Result ds (Just trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else if null $ tail ts then return $ head ts
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else non_fatal_error trm ("ambiguous mixfix term\n\t" ++
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ intersperse "\n\t"
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ map (show . printText0 g)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ take 5 ts)) (posOfTerm trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederresolveFormula :: GlobalAnnos -> Set Id -> Set Id -> FORMULA -> Result FORMULA
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaederresolveFormula g ops preds frm =
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let self = resolveFormula g ops preds
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder resolveTerm = resolveMixfix g ops preds False in
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Quantification q vs fOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fNew <- self 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 ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tNew <- resolveMixfix g ops preds 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 ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication (Pred_name ide) args ps
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
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder _ -> non_fatal_error (Mixfix_formula t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder ("unresolved formula: " ++ show (printText0 g tOld))
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm tOld)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder-- start testing
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedertestForm l r t =
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder let g = addGlobalAnnos emptyGlobalAnnos
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder $ map (parseString annotationL) l
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder resolveFormula g (mkSet $ map (parseString parseId) r)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder emptySet (parseString formula t)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian MaedermyAnnos = [ "%prec({__+__} < {__*__})%", "%prec({__*__} < {__^__})%"
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder , "%left_assoc(__+__)%"
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder , "%list([__], [], __::__)%"]
5d05fc7110bca98e897a726d60dd5f67c4100814Christian MaedermyIs = ["__^__", "__*__", "__+__", "[__]", "____p", "q____","____x____",
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder "{____}","__-__",
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder "x", "0", "1", "2", "3", "4", "5", "a", "b", "-__", "__!"]
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maederpolynom = "4*x^4+3*x^3+2*x^2+1*x^1+0*x^0=0"
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian MaedertestAppl t = testForm myAnnos myIs t
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- convert literals
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- isChar :: Token -> Bool
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- isChar t = head (tokStr t) == '\''
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederisString :: Token -> Bool
fd40e201b7277427113c89724d8a2389c18e9cbdChristian MaederisString t = head (tokStr t) == '\"'
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederisNumber :: Token -> Bool
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederisNumber t = let s = tokStr t in length s > 1 && C.isDigit (head s)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederisFloating :: Token -> Bool
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder-- precondition: isNumber
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederisFloating t = any (\c -> c == '.' || c == 'E') (tokStr t)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederparseString :: Parser a -> String -> a
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian MaederparseString p s = case parse p "" s of
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder Left _ -> error "parseString"
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maedersplit :: Parser a -> String -> (a, String)
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maedersplit p s = let ph = do hd <- p;
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder tl <- getInput;
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder return (hd, tl)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maeder in parseString ph s
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeStringTerm :: Id -> Id -> Token -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeStringTerm c f tok =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder makeStrTerm (line, colm + 1) str
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (line, colm) = tokPos tok
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder str = init (tail (tokStr tok))
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder makeStrTerm p@(lin, col) l =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if null l then asAppl c [] p
7bdf8f2044ee1bb844ec460e7d96fbdee69feda4Christian Maeder else let (hd, tl) = split caslChar l
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder real = if hd == "'" then "'\\''" else "'" ++ hd ++ "'"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder -- convert "'" to "\'" and lookup character '\''
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in asAppl f [asAppl (Id [Token real p] [] []) [] p,
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder makeStrTerm (lin, col + length hd) tl] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeNumberTerm :: Id -> Token -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeNumberTerm f t@(Token n p@(lin, col)) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeNumberTerm"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [_] -> asAppl (Id [t] [] []) [] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] p,
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder makeNumberTerm f (Token tl (lin, col+1))] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFraction :: Id -> Id -> Token -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFraction f d t@(Token s p@(lin, col)) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let (n, r) = span (\c -> c /= '.') s
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder dotcol = col + length n
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in if null r then makeNumberTerm f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else asAppl d [makeNumberTerm f (Token n p),
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder makeNumberTerm f (Token (tail r) (lin, dotcol + 1))]
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder (lin, dotcol)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeSignedNumber :: Id -> Token -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeSignedNumber f t@(Token n p@(lin, col)) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeSignedNumber"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if hd == '-' || hd == '+' then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder asAppl (Id [Token [hd] p] [] [])
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [makeNumberTerm f (Token tl (lin, col+1))] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else makeNumberTerm f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFloatTerm :: Id -> Id -> Id -> Token -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFloatTerm f d e t@(Token s p@(lin, col)) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let (m, r) = span (\c -> c /= 'E') s
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder ecol = col + length m
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in if null r then makeFraction f d t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else asAppl e [makeFraction f d (Token m p),
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder makeSignedNumber f (Token (tail r) (lin, ecol + 1))]
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
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederconvertMixfixToken:: LiteralAnnos -> Token -> Result TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederconvertMixfixToken ga t =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if isString t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case string_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "string"
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder Just (c, f) -> return $ makeStringTerm c f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian 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"
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder Just (d, e) -> return $ makeFloatTerm f d e t
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder else return $ makeNumberTerm f t
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder else return te
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder where te = Mixfix_token t
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder err s = non_fatal_error te
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder ("missing %" ++ s ++ " annotation") (tokPos t)