e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye{- HetCATS/CASL/MixfixParser.hs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye $Id$

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Author: Christian Maeder

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Year: 2002

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix analysis of terms

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Missing features:

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye - the positions of Ids from %string, %list, %number and %floating annotations

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye is not changed within applications (and might be misleading)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye - using (Set State) instead of [State] avoids explosion

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye but detection of local ambiguities (that of subterms) is more difficult

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye solution: equal list states should be merged into a single state

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye that stores the local ambiguity

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-}

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yemodule CASL.MixfixParser ( resolveFormula, resolveMixfix)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye where

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport CASL.AS_Basic_CASL

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.AS_Annotation

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothierimport Common.GlobalAnnotations

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.Result

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.Id

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.Lib.Map as Map hiding (filter, split, map)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.Lib.Set as Set hiding (filter, split, single, insert)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.Lexer

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Control.Monad

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.Lib.Parsec

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport qualified Char as C

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothierimport Data.List(intersperse)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport Common.GlobalAnnotationsFunctions

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport CASL.Formula(updFormulaPos)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeimport qualified CASL.ShowMixfix as ShowMixfix (showTerm)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeshowTerm :: GlobalAnnos -> TERM -> String

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeshowTerm _ t = ShowMixfix.showTerm t ""

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- Earley Algorithm

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yedata State = State Id

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye [Pos] -- positions of Id tokens

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye [TERM] -- currently collected arguments

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye -- both in reverse order

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye [Token] -- only tokens after the "dot" are given

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Int -- index into the ParseMap/input string

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeinstance Eq State where

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye State r1 _ _ t1 p1 == State r2 _ _ t2 p2 = (r1, t1, p1) == (r2, t2, p2)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yeinstance Ord State where

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye State r1 _ _ t1 p1 <= State r2 _ _ t2 p2 = (r1, t1, p1) <= (r2, t2, p2)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YetermStr :: String

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YetermStr = "(T)"

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercommaTok, parenTok, termTok :: Token

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercommaTok = mkSimpleId "," -- for list elements

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YetermTok = mkSimpleId termStr

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeparenTok = mkSimpleId "(..)"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YecolonTok, asTok, varTok, opTok, predTok :: Token

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YecolonTok = mkSimpleId ":"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeasTok = mkSimpleId "as"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YevarTok = mkSimpleId "(v)"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeopTok = mkSimpleId "(o)"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YepredTok = mkSimpleId "(p)"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YemkState :: Int -> Id -> State

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YemkState i ide = State ide [] [] (getTokenList termStr ide) i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YemkApplState :: Int -> Id -> State

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YemkApplState i ide = State ide [] []

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (getTokenList place ide ++ [parenTok]) i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelistToken :: Token

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelistToken = mkSimpleId "[]"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelistId :: Id -> Id

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- unique id (usually "[]" yields two tokens)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelistId i = Id [listToken] [i] []

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeisListId :: Id -> Bool

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeisListId (Id ts cs _) = not (null ts) && head ts == listToken && length cs == 1

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelistStates :: GlobalAnnos -> Int -> [State]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelistStates g i =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let lists = list_lit $ literal_annos g

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye listState co toks = State (listId co) [] [] toks i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in concatMap ( \ (bs, n, c) ->

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (b1, b2, cs) = getListBrackets bs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye e = Id (b1 ++ b2) cs [] in

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (if e == n then [] -- add b1 ++ b2 if its not yet included by n

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else [listState c $ getTokenList place e]) ++

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye [listState c (b1 ++ [termTok] ++ b2)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye , listState c (b1 ++ [termTok, commaTok] ++ b2)]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye ) $ Set.toList lists

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- these are the possible matches for the nonterminal TERM

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- the same states are used for the predictions

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeinitialState :: GlobalAnnos -> Set Id -> Int -> [State]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeinitialState g ids i =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let mkTokState toks = State (Id toks [] []) [] [] toks i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye is = Set.toList ids

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in mkTokState [parenTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [termTok, colonTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [termTok, asTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [varTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [opTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [opTok, parenTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [predTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkTokState [predTok, parenTok] :

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye listStates g i ++

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye map (mkState i) is ++

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye map (mkApplState i) is

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yetype ParseMap = Map Int [State]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelookUp :: (Ord a, MonadPlus m) => Map a (m b) -> a -> (m b)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YelookUp ce k = findWithDefault mzero k ce

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- match (and shift) a token (or partially finished term)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yescan :: TERM -> Int -> ParseMap -> ParseMap

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Yescan trm i m =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let t = case trm of

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_token x -> x

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_sorted_term _ _ -> colonTok

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_cast _ _ -> asTok

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_parenthesized _ _ -> parenTok

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Application (Qual_op_name _ _ _) [] _ -> opTok

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_qual_pred _ -> predTok

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye _ -> varTok

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Map.insert (i+1) (

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye foldr (\ (State o b a ts k) l ->

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if null ts || head ts /= t then l

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else let p = tokPos t : b in

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if t == commaTok && isListId o then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye -- list elements separator

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (State o p a

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (termTok : commaTok : tail ts) k)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye : (State o p a (termTok : tail ts) k) : l

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if t == parenTok then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (State o b (trm : a) (tail ts) k) : l

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if t == varTok || t == opTok || t == predTok then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (State o b [trm] (tail ts) k) : l

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if t == colonTok || t == asTok then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (State o b [mkTerm $ head a] [] k) : l

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else (State o p a (tail ts) k) : l) []

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier (lookUp m i)) m

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier where mkTerm t1 = case trm of

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier Mixfix_sorted_term s ps -> Sorted_term t1 s ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_cast s ps -> Cast t1 s ps

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier _ -> t1

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier-- precedence graph stuff

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercheckArg :: GlobalAnnos -> AssocEither -> Id -> Id -> Bool

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercheckArg g dir op arg =

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier if arg == op

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier then isAssoc dir (assoc_annos g) op || not (isInfix op)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier else

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier case precRel (prec_annos g) op arg of

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier Lower -> True

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier NoDirection -> not $ isInfix arg

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier _ -> False

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercheckAnyArg :: GlobalAnnos -> Id -> Id -> Bool

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercheckAnyArg g op arg =

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier case precRel (prec_annos g) op arg of

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier BothDirections -> isInfix op && op == arg

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier _ -> True

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothierisLeftArg, isRightArg :: Id -> Int -> Bool

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothierisLeftArg (Id ts _ _) n = n + 1 == (length $ takeWhile isPlace ts)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeisRightArg (Id ts _ _) n = n == (length $ filter isPlace ts) -

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (length $ takeWhile isPlace (reverse ts))

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YefilterByPrec :: GlobalAnnos -> Set Id -> Bool -> State -> State -> Bool

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YefilterByPrec _ _ _ _ (State _ _ _ [] _) = False

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YefilterByPrec g preds maybeFormula

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (State argIde _ _ _ _) (State opIde _ args (hd:_) _) =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if hd == termTok then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if isListId opIde || isListId argIde ||

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (Set.member opIde preds && maybeFormula)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier then True

8031591d3cc3c82e97f4b60ea22d671525077b15Srihari Venkatesan else let n = length args in

8031591d3cc3c82e97f4b60ea22d671525077b15Srihari Venkatesan if isLeftArg opIde n then

8031591d3cc3c82e97f4b60ea22d671525077b15Srihari Venkatesan if isPostfix opIde && (isPrefix argIde

8031591d3cc3c82e97f4b60ea22d671525077b15Srihari Venkatesan || isInfix argIde) then False

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else checkArg g ALeft opIde argIde

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if isRightArg opIde n then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if isPrefix opIde && isInfix argIde then False

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else checkArg g ARight opIde argIde

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier else checkAnyArg g opIde argIde

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier else False

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- reconstructing positions

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YesetPlainIdePos :: Id -> [Pos] -> (Id, [Pos])

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YesetPlainIdePos (Id ts cs _) ps =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (places, toks) = span isPlace (reverse ts)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye pls = reverse places

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye f = zipWith (\ a b -> up_pos (const b) a)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (ps1, ps2) = splitAt (length toks) ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye front = f (reverse toks) ps1

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in if null cs then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (ps3, ps4) = splitAt (length pls) ps2

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in (Id (front ++ f pls ps3) [] [], ps4)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else let (newCs, ps3, ps4) = foldl (\ (prevCs, seps, rest) a ->

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (c1, qs) = setPlainIdePos a rest

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in (c1: prevCs, head qs : seps, tail qs))

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye ([], [head ps2], tail ps2) cs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (ps6, ps7) = splitAt (length pls) ps4

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in (Id (front ++ f pls ps6) (reverse newCs) (reverse ps3), ps7)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YesetIdePos :: Id -> [TERM] -> [Pos] -> Id

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YesetIdePos i@(Id ts _ _) ar ps =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let nt = length $ getTokenList place i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye np = length ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye na = length $ filter isPlace ts

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (_, toks) = span isPlace (reverse ts)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in if nt == np then -- literal places

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (newId, []) = setPlainIdePos i ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in newId

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if np + na == nt && na == length ar then -- mixfix

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (newTps, rargs, rqs) = mergePos (reverse toks) ar ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (newId, []) = setPlainIdePos i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (newTps ++ rqs ++ map posOfTerm rargs)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in newId

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else error "setIdePos"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye where mergePos [] args qs = ([], args, qs)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mergePos (t:rs) args qs =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if isPlace t then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let (tokps, rargs, rqs) = mergePos rs (tail args) qs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in (posOfTerm (head args) : tokps, rargs, rqs)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else let (tokps, rargs, rqs) = mergePos rs args (tail qs)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in (head qs : tokps, rargs, rqs)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye-- constructing the parse tree from (the final) parser state(s)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YestateToAppl :: State -> TERM

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YestateToAppl (State ide rs a _ _) =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let vs = getTokenList place ide

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye ar = reverse a

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye qs = reverse rs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in if vs == [termTok, colonTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye || vs == [termTok, asTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye || vs == [varTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye || vs == [opTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye || vs == [predTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye || vs == [parenTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye then case head ar of

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_parenthesized ts _ -> if length ts == 1 then head ts

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else head ar

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye har -> har

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if vs == [opTok, parenTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye then let Application q _ _ = head ar

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Mixfix_parenthesized ts ps = head a

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in Application q ts ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if vs == [predTok, parenTok]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye then Mixfix_term [head ar, head a]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else case ar of

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye [Mixfix_parenthesized ts ps] ->

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye Application (Op_name

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (setIdePos ide ts qs))

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye ts ps

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye _ -> let newIde@(Id (t:_) _ _) = setIdePos ide ar qs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye pos = if isPlace t then posOfTerm $ head ar

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else tokPos t

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in Application (Op_name newIde) ar [pos]

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye -- true mixfix

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeasListAppl :: GlobalAnnos -> State -> TERM

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean YeasListAppl g s@(State i bs a _ _) =

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye if isListId i then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let Id _ [f] _ = i

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye ListCons b c = getLiteralType g f

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye (b1, _, _) = getListBrackets b

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye cl = length $ getTokenList place b

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye nb1 = length b1

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye ra = reverse a

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye na = length ra

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye nb = length bs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkList [] ps = asAppl c [] (head ps)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye mkList (hd:tl) ps = asAppl f [hd, mkList tl (tail ps)] (head ps)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in if null a then asAppl c [] (if null bs then nullPos else last bs)

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else if nb + 2 == cl + na then

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye let br = reverse bs

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye br1 = drop (nb1 - 1) br

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye in mkList (reverse a) br1

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else error "asListAppl"

e4b86885570d77af552e9cf94f142f4d744fb8c8Cheng Sean Ye else stateToAppl s

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier-- final complete/reduction phase

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier-- when a grammar rule (mixfix Id) has been fully matched

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercollectArg :: GlobalAnnos -> Set Id -> Bool -> ParseMap -> State -> [State]

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier-- pre: finished rule

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercollectArg g preds maybeFormula m s@(State _ _ _ _ k) =

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier map (\ (State o b a ts k1) ->

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier State o b (asListAppl g s : a)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier (tail ts) k1)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier $ filter (filterByPrec g preds maybeFormula s)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier $ lookUp m k

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothiercompl :: GlobalAnnos -> Set Id -> Bool -> ParseMap -> [State] -> [State]

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothiercompl g preds maybeFormula m l =

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier concat $ map (collectArg g preds maybeFormula m)

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier $ filter (\ (State _ _ _ ts _) -> null ts) l

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercomplRec :: GlobalAnnos -> Set Id -> Bool -> ParseMap -> [State] -> [State]

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom PothiercomplRec g preds maybeFormula m l =

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier let l1 = compl g preds maybeFormula m l in

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier if null l1 then l else complRec g preds maybeFormula m l1 ++ l

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothiercomplete :: GlobalAnnos -> Set Id -> Bool -> Int -> ParseMap -> ParseMap

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothiercomplete g preds maybeFormula i m =

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier Map.insert i (complRec g preds maybeFormula m $ lookUp m i) m

074bb90d80fdbeb2d04a8450a55ecbc96de28785Tom Pothier

-- predict which rules/ids might match for (the) nonterminal(s) (termTok)

-- provided the "dot" is followed by a nonterminal

predict :: GlobalAnnos -> Set Id -> Int -> ParseMap -> ParseMap

predict g is i m = if i /= 0 && any (\ (State _ _ _ ts _) -> not (null ts)

&& head ts == termTok)

(lookUp m i)

then insertWith (++) i (initialState g is i) m

else m

type Chart = (Int, [Diagnosis], ParseMap)

nextState :: GlobalAnnos -> Set Id -> Set Id -> Bool -> TERM -> Chart -> Chart

nextState g is preds maybeFormula trm (i, ds, m) =

let m1 = complete g preds maybeFormula (i+1) $

scan trm i $

predict g is i m

in if null (lookUp m1 (i+1)) && null ds

then (i+1, Diag Error ("unexpected mixfix token: "

++ showTerm g trm)

(posOfTerm trm) : ds, m)

else (i+1, ds, m1)

iterateStates :: GlobalAnnos -> Set Id -> Set Id -> Bool -> [TERM]

-> Chart -> Chart

iterateStates g ops preds maybeFormula terms c@(i, ds, m) =

let self = iterateStates g ops preds maybeFormula

expand = expandPos Mixfix_token

oneStep = nextState g ops preds maybeFormula

resolvePred = resolveMixfix g ops preds

resolveTerm = resolvePred maybeFormula

in if null terms then c

else case head terms of

Mixfix_term ts -> self (ts ++ tail terms) c

Mixfix_bracketed ts ps ->

self (expand ("[", "]") ts ps ++ tail terms) c

Mixfix_braced ts ps ->

self (expand ("{", "}") ts ps ++ tail terms) c

Mixfix_parenthesized ts ps ->

let Result mds v =

do tsNew <- mapM resolveTerm ts

return $ Mixfix_parenthesized tsNew ps

tNew = case v of Nothing -> head terms

Just x -> x

in self (tail terms) (oneStep tNew (i, ds++mds, m))

Conditional t1 f2 t3 ps ->

let Result mds v =

do t4 <- resolvePred False t1

f5 <- resolveFormula g ops preds f2

t6 <- resolvePred False t3

return (Conditional t4 f5 t6 ps)

tNew = case v of Nothing -> head terms

Just x -> x

in self (tail terms) (oneStep tNew (i, ds++mds, m))

Mixfix_token t -> let (ds1, trm) =

convertMixfixToken (literal_annos g) t

in self (tail terms)

(oneStep trm (i, ds1++ds, m))

t -> self (tail terms) (oneStep t c)

posOfTerm :: TERM -> Pos

posOfTerm trm =

case trm of

Mixfix_token t -> tokPos t

Mixfix_term ts -> posOfTerm (head ts)

Simple_id i -> tokPos i

Mixfix_qual_pred p ->

case p of

Pred_name i -> posOfId i

Qual_pred_name _ _ ps -> first (Just ps)

Application (Qual_op_name _ _ ps) [] [] -> first (Just ps)

_ -> first $ get_pos_l trm

where first ps = case ps of

Nothing -> nullPos

Just l -> if null l then nullPos else head l

getAppls :: GlobalAnnos -> Int -> ParseMap -> [TERM]

getAppls g i m =

map (asListAppl g) $

filter (\ (State _ _ _ ts k) -> null ts && k == 0) $

lookUp m i

resolveMixfix :: GlobalAnnos -> Set Id -> Set Id -> Bool -> TERM -> Result TERM

resolveMixfix g ops preds mayBeFormula trm =

let (i, ds, m) = iterateStates g ops preds mayBeFormula [trm]

(0, [], Map.single 0 $ initialState g

(if mayBeFormula then ops `Set.union` preds else ops) 0)

ts = getAppls g i m

in if null ts then if null ds then

plain_error trm ("no resolution for term: "

++ showTerm g trm)

(posOfTerm trm)

else Result ds (Just trm)

else if null $ tail ts then Result ds (Just (head ts))

else Result (Diag Error ("ambiguous mixfix term\n\t" ++

(concat

$ intersperse "\n\t"

$ map (showTerm g)

$ take 5 ts)) (posOfTerm trm) : ds) (Just trm)

resolveFormula :: GlobalAnnos -> Set Id -> Set Id -> FORMULA -> Result FORMULA

resolveFormula g ops preds frm =

let self = resolveFormula g ops preds

resolveTerm = resolveMixfix g ops preds False in

case frm of

Quantification q vs fOld ps ->

let varIds = foldl (\ l (Var_decl va _ _) ->

map (\t->Id[t][][]) va ++ l) [] vs

in

do fNew <- resolveFormula g (Set.fromList varIds `Set.union` ops)

preds fOld

return $ Quantification q vs fNew ps

Conjunction fsOld ps ->

do fsNew <- mapM self fsOld

return $ Conjunction fsNew ps

Disjunction fsOld ps ->

do fsNew <- mapM self fsOld

return $ Disjunction fsNew ps

Implication f1 f2 ps ->

do f3 <- self f1

f4 <- self f2

return $ Implication f3 f4 ps

Equivalence f1 f2 ps ->

do f3 <- self f1

f4 <- self f2

return $ Equivalence f3 f4 ps

Negation fOld ps ->

do fNew <- self fOld

return $ Negation fNew ps

Predication sym tsOld ps ->

do tsNew <- mapM resolveTerm tsOld

return $ Predication sym tsNew ps

Definedness tOld ps ->

do tNew <- resolveTerm tOld

return $ Definedness tNew ps

Existl_equation t1 t2 ps ->

do t3 <- resolveTerm t1

t4 <- resolveTerm t2

return $ Existl_equation t3 t4 ps

Strong_equation t1 t2 ps ->

do t3 <- resolveTerm t1

t4 <- resolveTerm t2

return $ Strong_equation t3 t4 ps

Membership tOld s ps ->

do tNew <- resolveTerm tOld

return $ Membership tNew s ps

Mixfix_formula tOld ->

do tNew <- resolveMixfix g ops preds True tOld

mkPredication tNew

where mkPredication t =

case t of

Mixfix_parenthesized [t0] ps ->

do p <- mkPredication t0

return $ if null ps then p

else updFormulaPos (head ps) (last ps) p

Application (Op_name ide) args ps ->

let p = Predication (Pred_name ide) args ps in

if ide `Set.member` preds then return p

else plain_error p

("not a predicate: " ++ showId ide "")

(posOfTerm t)

Mixfix_qual_pred qide ->

return $ Predication qide [] []

Mixfix_term [Mixfix_qual_pred qide,

Mixfix_parenthesized ts ps] ->

return $ Predication qide ts ps

Mixfix_term _ -> return $ Mixfix_formula t -- still wrong

_ -> plain_error (Mixfix_formula t)

("not a formula: " ++ showTerm g t)

(posOfTerm t)

f -> return f

-- ---------------------------------------------------------------

-- convert literals

-- ---------------------------------------------------------------

makeStringTerm :: Id -> Id -> Token -> TERM

makeStringTerm c f tok =

makeStrTerm (incSourceColumn sp 1) str

where

sp = tokPos tok

str = init (tail (tokStr tok))

makeStrTerm p l =

if null l then asAppl c [] p

else let (hd, tl) = splitString caslChar l

in asAppl f [asAppl (Id [Token ("'" ++ hd ++ "'") p] [] []) [] p,

makeStrTerm (incSourceColumn p $ length hd) tl] p

makeNumberTerm :: Id -> Token -> TERM

makeNumberTerm f t@(Token n p) =

case n of

[] -> error "makeNumberTerm"

[_] -> asAppl (Id [t] [] []) [] p

hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] p,

makeNumberTerm f (Token tl

(incSourceColumn p 1))] p

makeFraction :: Id -> Id -> Token -> TERM

makeFraction f d t@(Token s p) =

let (n, r) = span (\c -> c /= '.') s

dotOffset = length n

in if null r then makeNumberTerm f t

else asAppl d [makeNumberTerm f (Token n p),

makeNumberTerm f (Token (tail r)

(incSourceColumn p $ dotOffset + 1))]

$ incSourceColumn p dotOffset

makeSignedNumber :: Id -> Token -> TERM

makeSignedNumber f t@(Token n p) =

case n of

[] -> error "makeSignedNumber"

hd:tl ->

if hd == '-' || hd == '+' then

asAppl (Id [Token [hd] p] [] [])

[makeNumberTerm f (Token tl $ incSourceColumn p 1)] p

else makeNumberTerm f t

makeFloatTerm :: Id -> Id -> Id -> Token -> TERM

makeFloatTerm f d e t@(Token s p) =

let (m, r) = span (\c -> c /= 'E') s

offset = length m

in if null r then makeFraction f d t

else asAppl e [makeFraction f d (Token m p),

makeSignedNumber f (Token (tail r)

$ incSourceColumn p (offset + 1))]

$ incSourceColumn p offset

asAppl :: Id -> [TERM] -> Pos -> TERM

asAppl f args p = let pos = if null args then [] else [p]

in Application (Op_name f) args pos

-- analyse Mixfix_token

convertMixfixToken:: LiteralAnnos -> Token -> ([Diagnosis], TERM)

convertMixfixToken ga t =

if isString t then

case string_lit ga of

Nothing -> err "string"

Just (c, f) -> ([], makeStringTerm c f t)

else if isNumber t then

case number_lit ga of

Nothing -> err "number"

Just f -> if isFloating t then

case float_lit ga of

Nothing -> err "floating"

Just (d, e) -> ([], makeFloatTerm f d e t)

else ([], makeNumberTerm f t)

else ([], te)

where te = Mixfix_token t

err s = ([Diag Error ("missing %" ++ s ++ " annotation") (tokPos t)]

, te)