MixfixParser.hs revision 409578f7f6dbee1e10dd1c969328bb92dabd087d
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Author: Christian Maeder
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Mixfix analysis of terms
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder Missing features:
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder - the positions of Ids from %string, %list, %number and %floating annotations
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder is not changed within applications (and might be misleading)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder - using (Set State) instead of [State] avoids explosion
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder but detection of local ambiguities (that of subterms) is more difficult
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder solution: equal list states should be merged into a single state
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder that stores the local ambiguity
28b44554f1c23185d6586c03cccea682a36027a2Christian Maedermodule MixfixParser ( parseString, resolveFormula, resolveMixfix
28b44554f1c23185d6586c03cccea682a36027a2Christian Maeder , getTokenList, expandPos )
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport AS_Basic_CASL
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport GlobalAnnotations
e4eed2389ec1b1bfa03c662c71e8165e93df43c4Christian Maederimport FiniteMap
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maederimport Common.Lib.Set hiding (filter, split)
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maederimport Lexer (caslChar)
d697755cce49a436e1170e8e158c19f79b0389b8Christian Maederimport qualified Char as C
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maederimport Data.List(intersperse)
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport PrettyPrint
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport Print_AS_Basic
3f0cd3e73a8aa47bb586b69fe5f7fa450000ecfdChristian Maederimport GlobalAnnotationsFunctions
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maederimport Formula(updFormulaPos)
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian MaedershowTerm :: GlobalAnnos -> TERM -> String
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian MaedershowTerm g t = show $ printText0 g t
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder where _just_avoid_unused_import_warning = pluralS_symb_list
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
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederinitialState :: GlobalAnnos -> Set Id -> Int -> [State]
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederinitialState g ids i =
3004ea619754fb657d87ecad1d9a8b6b8ed0f9d1Christian Maeder let mkTokState toks = State (Id toks [] []) [] [] toks i
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maeder is = toList ids
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]
a5023d78ecc3452c0de580912e7bd018640ddeaaChristian MaederlookUp :: (Ord a, MonadPlus m) => FiniteMap a (m b) -> a -> (m b)
a5023d78ecc3452c0de580912e7bd018640ddeaaChristian MaederlookUp ce = lookupWithDefaultFM ce mzero
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
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maederpredict :: GlobalAnnos -> Set 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)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian 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
03b2c932671a04fdba42cf5b9052b087402072e5Christian Maeder in if null (lookUp m1 (i+1)) && null ds
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder then (i+1, Diag Error ("unexpected mixfix token: "
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder ++ showTerm g trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm trm) : ds, m)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else (i+1, ds, m1)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian 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))
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
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) $
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian 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
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian 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
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder plain_error trm ("no resolution for term: "
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder ++ showTerm g trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder (posOfTerm trm)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder else Result ds (Just trm)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else if null $ tail ts then Result ds (Just (head ts))
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder else Result (Diag Error ("ambiguous mixfix term\n\t" ++
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder $ intersperse "\n\t"
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder $ map (showTerm g)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder $ take 5 ts)) (posOfTerm trm) : ds) (Just trm)
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian MaederresolveFormula :: GlobalAnnos -> Set Id -> Set Id -> FORMULA -> Result FORMULA
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 ->
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder let varIds = foldl (\ l (Var_decl va _ _) ->
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder map (\t->Id[t][][]) va ++ l) [] vs
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maeder do fNew <- resolveFormula g (fromList varIds `union` ops)
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
409578f7f6dbee1e10dd1c969328bb92dabd087dChristian Maeder if ide `member` preds then return p
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder else plain_error p
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ("not a predicate: " ++ showId ide "")
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (posOfTerm t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_qual_pred qide ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication qide [] []
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_term [Mixfix_qual_pred qide,
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_parenthesized ts ps] ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication qide ts ps
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Mixfix_term _ -> return $ Mixfix_formula t -- still wrong
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder _ -> plain_error (Mixfix_formula t)
36b1d2b1423e96d38a7f5e9b7a18c4c323eedd0aChristian Maeder ("not a formula: " ++ showTerm g t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (posOfTerm t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- convert literals
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian 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 =
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeStrTerm (incSourceColumn sp 1) str
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder sp = tokPos tok
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder str = init (tail (tokStr tok))
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeStrTerm p l =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if null l then asAppl c [] p
a5023d78ecc3452c0de580912e7bd018640ddeaaChristian Maeder else let (hd, tl) = split caslChar l
a5023d78ecc3452c0de580912e7bd018640ddeaaChristian Maeder in asAppl f [asAppl (Id [Token ("'" ++ hd ++ "'") p] [] []) [] p,
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeStrTerm (incSourceColumn p $ length hd) tl] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeNumberTerm :: Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeNumberTerm f t@(Token n p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeNumberTerm"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [_] -> asAppl (Id [t] [] []) [] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] p,
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeNumberTerm f (Token tl
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder (incSourceColumn p 1))] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFraction :: Id -> Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeFraction f d t@(Token s p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let (n, r) = span (\c -> c /= '.') s
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder dotOffset = length n
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in if null r then makeNumberTerm f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else asAppl d [makeNumberTerm f (Token n p),
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeNumberTerm f (Token (tail r)
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder (incSourceColumn p $ dotOffset + 1))]
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder $ incSourceColumn p dotOffset
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeSignedNumber :: Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeSignedNumber f t@(Token n p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeSignedNumber"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if hd == '-' || hd == '+' then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder asAppl (Id [Token [hd] p] [] [])
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder [makeNumberTerm f (Token tl $ incSourceColumn p 1)] p
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else makeNumberTerm f t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeFloatTerm :: Id -> Id -> Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeFloatTerm f d e t@(Token s p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder let (m, r) = span (\c -> c /= 'E') s
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder offset = length m
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in if null r then makeFraction f d t
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder else asAppl e [makeFraction f d (Token m p),
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeSignedNumber f (Token (tail r)
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder $ incSourceColumn p (offset + 1))]
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder $ incSourceColumn p offset
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederasAppl :: Id -> [TERM] -> Pos -> TERM
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederasAppl f args p = let pos = if null args then [] else [p]
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder in Application (Op_name f) args pos
fd40e201b7277427113c89724d8a2389c18e9cbdChristian Maeder-- analyse Mixfix_token
1eb602487b8b0dff5fad820439fc27264eb8889cChristian MaederconvertMixfixToken:: LiteralAnnos -> Token -> ([Diagnosis], TERM)
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaederconvertMixfixToken ga t =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder if isString t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case string_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "string"
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just (c, f) -> ([], makeStringTerm c f t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else if isNumber t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case number_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "number"
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Just f -> if isFloating t then
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder case float_lit ga of
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder Nothing -> err "floating"
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Just (d, e) -> ([], makeFloatTerm f d e t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else ([], makeNumberTerm f t)
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder else ([], te)
9256f871e7dd915ccfb5969e2117f054306cd366Christian Maeder where te = Mixfix_token t
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder err s = ([Diag Error ("missing %" ++ s ++ " annotation") (tokPos t)]