MixfixParser.hs revision 03b2c932671a04fdba42cf5b9052b087402072e5
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Author: Christian Maeder
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Mixfix analysis of terms
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maedermodule MixfixParser (parseString, resolveFormula, resolveMixfix)
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 Maederimport PrettyPrint
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport Print_AS_Basic
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport GlobalAnnotationsFunctions
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Formula(updFormulaPos)
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maeder-- Earley Algorithm
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederdata State = State Id
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
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
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)"
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- reconstruct token list
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- expandPos f "{" "}" [a,b] [(1,1), (1,3), 1,5)] =
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- [ t"{" , a , t"," , b , t"}" ] where t = f . Token (and proper positions)
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)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder in head seps : if null ts then [last seps] else
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder concat (zipWith (\ t s -> [t,s]) ts (tail seps))
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- all tokens including "," within compound lists as sequence
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- either generate literal places or the non-terminal termTok
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 "[]"] [] []
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedergetListBrackets :: Id -> ([Token], [Token])
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedergetListBrackets (Id b _ _) =
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let (b1, rest) = break isPlace b
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder b2 = if null rest then []
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else filter (not . isPlace) rest
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederlistStates :: GlobalAnnos -> Int -> [State]
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder-- no empty list (can be written down directly)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederlistStates g i =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let listState toks = State listId [] [] toks i
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder in case list_lit (literal_annos g) of
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder Nothing -> []
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just (bs, c, _) ->
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let (b1, b2) = getListBrackets bs
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder ls = [ listState (b1 ++ [termTok] ++ b2)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder , listState (b1 ++ [termTok, commaTok] ++ b2)]
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder in if c == Id el [] [] then ls
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder -- don't put in empty list twice
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder else listState el : ls
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- these are the possible matches for the nonterminal TERM
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- the same states are used for the predictions
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederinitialState :: GlobalAnnos -> [Id] -> Int -> [State]
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian MaederinitialState g is i =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let mkTokState toks = State (Id toks [] []) [] [] toks i
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder in 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] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [predTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkTokState [predTok, parenTok] :
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder listStates g i ++
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder map (mkState i) is ++
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder map (mkApplState i) is
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maedertype ParseMap = FiniteMap Int [State]
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederlookUp :: (Ord key) => FiniteMap key [a] -> key -> [a]
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederlookUp m i = lookupWithDefaultFM m [] i
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
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder addToFM m (i+1) (
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
1919917c90a1bf84a25ca866ac632605ad0548e6Christian Maeder if t == commaTok && o == listId 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) []
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder (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
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
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Higher -> False
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ExplGroup BothDirections -> False
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ExplGroup 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
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ExplGroup 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))
b26211de8c1e50efbabbb95497e7508c4d852634Christian MaederfilterByPrec :: GlobalAnnos -> State -> State -> Bool
6fb319833285f714693d58e9620d67ab21ddebe4Christian MaederfilterByPrec _ _ (State _ _ _ [] _) = False
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederfilterByPrec g (State argIde _ _ _ _) (State opIde _ args (hd:_) _) =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder if hd == termTok then
6fb319833285f714693d58e9620d67ab21ddebe4Christian Maeder if opIde == listId || argIde == listId then True
03b2c932671a04fdba42cf5b9052b087402072e5Christian 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
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 =
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)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- constructing the parse tree from (the final) parser state(s)
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
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederasListAppl g s@(State i bs a _ _) =
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder if i == listId then
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder case list_lit $ literal_annos g of
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Nothing -> error "asListAppl"
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder Just (b, c, f) ->
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let (b1, b2) = getListBrackets b
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder nb1 = length b1
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder nb2 = length b2
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)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else if nb + 1 == nb1 + nb2 + 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
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaedercollectArg :: GlobalAnnos -> ParseMap -> State -> [State]
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- pre: finished rule
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian 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)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder $ filter (filterByPrec g s)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maedercompl :: GlobalAnnos -> ParseMap -> [State] -> [State]
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder concat $ map (collectArg g m)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder $ filter (\ (State _ _ _ ts _) -> null ts) l
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
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maedercomplete g i m = addToFM m i $ complRec g m $ lookUp m i
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- predict which rules/ids might match for (the) nonterminal(s) (termTok)
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder-- provided the "dot" is followed by a nonterminal
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maederpredict :: GlobalAnnos -> [Id] -> Int -> ParseMap -> ParseMap
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maederpredict g is i m = if i /= 0 && any (\ (State _ _ _ ts _) -> not (null ts)
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder && head ts == termTok)
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder then addToFM_C (++) m i (initialState g is i)
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maedertype Chart = (Int, [Diagnosis], ParseMap)
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaedernextState :: GlobalAnnos -> [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
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder in if null (lookUp m1 (i+1)) && null ds
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)
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederiterateStates :: GlobalAnnos -> [Id] -> [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))
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Mixfix_token t -> let (ds1, trm) =
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder convertMixfixToken (literal_annos g) t
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder in self (tail terms)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (nextState g ops trm (i, ds1++ds, m))
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder t -> self (tail terms) (nextState g ops t c)
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder where expand = expandPos Mixfix_token
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederposOfId :: Id -> Pos
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian MaederposOfId (Id ts _ _) = let l = dropWhile isPlace ts
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder in if null l then
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let h = head ts
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder (lin, col) = tokPos h
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder in (lin, col + length (tokStr h))
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else tokPos $ head l
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) $
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederresolveMixfix :: GlobalAnnos -> [Id] -> [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
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder (if mayBeFormula then setToList $
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder mkSet (ops ++ 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)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else if null $ tail ts then Result ds (Just (head ts))
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else Result (Error ("ambiguous mixfix term\n\t" ++
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ intersperse "\n\t"
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ map (show . printText0 g)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder $ take 5 ts)) (posOfTerm trm) : ds) (Just trm)
03b2c932671a04fdba42cf5b9052b087402072e5Christian MaederresolveFormula :: GlobalAnnos -> [Id] -> [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 ->
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder let p = Predication (Pred_name ide) args ps in
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder if ide `elem` preds then return p
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder else non_fatal_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
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder _ -> non_fatal_error (Mixfix_formula t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder ("not a formula: " ++ show (printText0 g t))
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (posOfTerm t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f
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
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else let (real, len, rest) = if head l == '\''
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder then ("'\\''", 1, tail l)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else let (hd, tl) = split caslChar l
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder in ("'" ++ hd ++ "'", length hd, tl)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder -- convert "'" to "\'" and lookup character '\''
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in asAppl f [asAppl (Id [Token real p] [] []) [] p,
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder makeStrTerm (lin, col + len) rest] 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
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
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder err s = ([Error ("missing %" ++ s ++ " annotation") (tokPos t)], te)