MixfixParser.hs revision 2eb84fc82d3ffa9116bc471fda3742bd9e5a24bb
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Author: Christian Maeder
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix analysis of terms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Missing features:
06ba4a61654b3763ad65f52283832ebf058fdf1cslive - the positions of Ids from %string, %list, %number and %floating annotations
06ba4a61654b3763ad65f52283832ebf058fdf1cslive is not changed within applications (and might be misleading)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive - using (Set State) instead of [State] avoids explosion
06ba4a61654b3763ad65f52283832ebf058fdf1cslive but detection of local ambiguities (that of subterms) is more difficult
06ba4a61654b3763ad65f52283832ebf058fdf1cslive solution: equal list states should be merged into a single state
06ba4a61654b3763ad65f52283832ebf058fdf1cslive that stores the local ambiguity
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemodule CASL.MixfixParser ( parseString, resolveFormula, resolveMixfix
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , getTokenList, expandPos )
06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport FiniteMap
06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport Common.Lib.Set hiding (filter, split)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport Common.Lexer (caslChar)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport qualified Char as C
06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport Data.List(intersperse)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveimport CASL.Formula(updFormulaPos)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowTerm :: GlobalAnnos -> TERM -> String
06ba4a61654b3763ad65f52283832ebf058fdf1csliveshowTerm g t = show $ printText0 g t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where _just_avoid_unused_import_warning = pluralS_symb_list
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- Earley Algorithm
06ba4a61654b3763ad65f52283832ebf058fdf1cslivedata State = State Id
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [Pos] -- positions of Id tokens
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [TERM] -- currently collected arguments
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- both in reverse order
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [Token] -- only tokens after the "dot" are given
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Int -- index into the ParseMap/input string
06ba4a61654b3763ad65f52283832ebf058fdf1csliveinstance Eq State where
06ba4a61654b3763ad65f52283832ebf058fdf1cslive State r1 _ _ t1 p1 == State r2 _ _ t2 p2 =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive r1 == r2 && t1 == t2 && p1 == p2
06ba4a61654b3763ad65f52283832ebf058fdf1csliveinstance Ord State where
06ba4a61654b3763ad65f52283832ebf058fdf1cslive State r1 _ _ t1 p1 <= State r2 _ _ t2 p2 =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if r1 == r2 then
5bf90772244e08b493f008381645dd3704417d40yoshiki if t1 == t2 then p1 <= p2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else t1 <= t2
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive else r1 <= r2
ff797e743eb73c1d45b08158aa6b288c2d0c46eesliveinstance Show State where
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive showsPrec _ (State r _ _ d p) = showChar '{'
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . showSepList (showString "") showTok first
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . showChar '.'
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . showSepList (showString "") showTok d
06ba4a61654b3763ad65f52283832ebf058fdf1cslive . shows p . showChar '}'
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where first = take (length v - length d) v
06ba4a61654b3763ad65f52283832ebf058fdf1cslive v = getTokenList True r
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecommaTok, parenTok, termTok :: Token
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecommaTok = mkSimpleId "," -- for list elements
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetermTok = mkSimpleId "(T)"
06ba4a61654b3763ad65f52283832ebf058fdf1csliveparenTok = mkSimpleId "(..)"
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecolonTok, asTok, varTok, opTok, predTok :: Token
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecolonTok = mkSimpleId ":"
06ba4a61654b3763ad65f52283832ebf058fdf1csliveasTok = mkSimpleId "as"
5bf90772244e08b493f008381645dd3704417d40yoshikivarTok = mkSimpleId "(v)"
5bf90772244e08b493f008381645dd3704417d40yoshikiopTok = mkSimpleId "(o)"
06ba4a61654b3763ad65f52283832ebf058fdf1cslivepredTok = mkSimpleId "(p)"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- reconstruct token list
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- expandPos f "{" "}" [a,b] [(1,1), (1,3), 1,5)] =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- [ t"{" , a , t"," , b , t"}" ] where t = f . Token (and proper positions)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveexpandPos :: (Token -> a) -> String -> String -> [a] -> [Pos] -> [a]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveexpandPos f o c ts ps =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let n = length ts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive j = length ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive cutOuterPos i l = let k = length l in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if k == i+1 then l
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else cutOuterPos (i - 2)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ init (tail l)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ps1 = if j > n && even (j - (n+1)) then cutOuterPos n ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if j > 1 then
5bf90772244e08b493f008381645dd3704417d40yoshiki head ps : replicate (n - 1) nullPos
5bf90772244e08b493f008381645dd3704417d40yoshiki ++ [last ps]
5bf90772244e08b493f008381645dd3704417d40yoshiki else replicate (n + 1) nullPos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive seps = map f
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (zipWith Token (o : replicate (n - 1) "," ++ [c]) ps1)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in head seps : if null ts then [last seps] else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive concat (zipWith (\ t s -> [t,s]) ts (tail seps))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- all tokens including "," within compound lists as sequence
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- either generate literal places or the non-terminal termTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetTokenList :: Bool -> Id -> [Token]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetTokenList asLiteral (Id ts cs ps) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (pls, toks) = span isPlace (reverse ts)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive cts = if null cs then [] else concat
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ expandPos (:[]) "[" "]" (map (getTokenList True) cs) ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- although positions will be replaced (by scan)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convert = if asLiteral then reverse else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (\ t -> if isPlace t then termTok else t) . reverse
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in convert toks ++ cts ++ convert pls
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkState :: Int -> Id -> State
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkState i ide = State ide [] [] (getTokenList False ide) i
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkApplState :: Int -> Id -> State
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemkApplState i ide = State ide [] []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (getTokenList True ide ++ [parenTok]) i
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelistId :: Id
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- unique id (usually "[]" yields two tokens)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelistId = Id [mkSimpleId "[]"] [] []
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetListBrackets :: Id -> ([Token], [Token])
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetListBrackets (Id b _ _) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (b1, rest) = break isPlace b
06ba4a61654b3763ad65f52283832ebf058fdf1cslive b2 = if null rest then []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else filter (not . isPlace) rest
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in (b1, b2)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelistStates :: GlobalAnnos -> Int -> [State]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- no empty list (can be written down directly)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelistStates g i =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let listState toks = State listId [] [] toks i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in case list_lit (literal_annos g) of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (bs, c, _) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (b1, b2) = getListBrackets bs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive el = b1++b2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ls = [ listState (b1 ++ [termTok] ++ b2)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , listState (b1 ++ [termTok, commaTok] ++ b2)]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if c == Id el [] [] then ls
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- don't put in empty list twice
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else listState el : ls
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- these are the possible matches for the nonterminal TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- the same states are used for the predictions
06ba4a61654b3763ad65f52283832ebf058fdf1csliveinitialState :: GlobalAnnos -> Set Id -> Int -> [State]
06ba4a61654b3763ad65f52283832ebf058fdf1csliveinitialState g ids i =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let mkTokState toks = State (Id toks [] []) [] [] toks i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive is = toList ids
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in mkTokState [parenTok] :
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkTokState [termTok, colonTok] :
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkTokState [termTok, asTok] :
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkTokState [varTok] :
5bf90772244e08b493f008381645dd3704417d40yoshiki mkTokState [opTok] :
5bf90772244e08b493f008381645dd3704417d40yoshiki mkTokState [opTok, parenTok] :
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkTokState [predTok] :
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkTokState [predTok, parenTok] :
06ba4a61654b3763ad65f52283832ebf058fdf1cslive listStates g i ++
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (mkState i) is ++
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (mkApplState i) is
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetype ParseMap = FiniteMap Int [State]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelookUp :: (Ord a, MonadPlus m) => FiniteMap a (m b) -> a -> (m b)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelookUp ce = lookupWithDefaultFM ce mzero
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- match (and shift) a token (or partially finished term)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivescan :: TERM -> Int -> ParseMap -> ParseMap
06ba4a61654b3763ad65f52283832ebf058fdf1cslivescan trm i m =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let t = case trm of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_token x -> x
5bf90772244e08b493f008381645dd3704417d40yoshiki Mixfix_sorted_term _ _ -> colonTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_cast _ _ -> asTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_parenthesized _ _ -> parenTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Application (Qual_op_name _ _ _) [] _ -> opTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_qual_pred _ -> predTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> varTok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive addToFM m (i+1) (
06ba4a61654b3763ad65f52283832ebf058fdf1cslive foldr (\ (State o b a ts k) l ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if null ts || head ts /= t then l
5bf90772244e08b493f008381645dd3704417d40yoshiki else let p = tokPos t : b in
5bf90772244e08b493f008381645dd3704417d40yoshiki if t == commaTok && o == listId then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- list elements separator
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (State o p a
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (termTok : commaTok : tail ts) k)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive : (State o p a (termTok : tail ts) k) : l
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if t == parenTok then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (State o b (trm : a) (tail ts) k) : l
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if t == varTok || t == opTok || t == predTok then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (State o b [trm] (tail ts) k) : l
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if t == colonTok || t == asTok then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (State o b [mkTerm $ head a] [] k) : l
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else (State o p a (tail ts) k) : l) []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (lookUp m i))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where mkTerm t1 = case trm of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_sorted_term s ps -> Sorted_term t1 s ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_cast s ps -> Cast t1 s ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- precedence graph stuff
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecheckArg :: GlobalAnnos -> AssocEither -> Id -> Id -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecheckArg g dir op arg =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if arg == op
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then isAssoc dir (assoc_annos g) op || not (isInfix op)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case precRel (prec_annos g) op arg of
5bf90772244e08b493f008381645dd3704417d40yoshiki Lower -> True
5bf90772244e08b493f008381645dd3704417d40yoshiki Higher -> False
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ExplGroup BothDirections -> False
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ExplGroup NoDirection -> not $ isInfix arg
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecheckAnyArg :: GlobalAnnos -> Id -> Id -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecheckAnyArg g op arg =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case precRel (prec_annos g) op arg of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ExplGroup BothDirections -> isInfix op && op == arg
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisLeftArg, isRightArg :: Id -> Int -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisLeftArg (Id ts _ _) n = n + 1 == (length $ takeWhile isPlace ts)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisRightArg (Id ts _ _) n = n == (length $ filter isPlace ts) -
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (length $ takeWhile isPlace (reverse ts))
06ba4a61654b3763ad65f52283832ebf058fdf1cslivefilterByPrec :: GlobalAnnos -> State -> State -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslivefilterByPrec _ _ (State _ _ _ [] _) = False
06ba4a61654b3763ad65f52283832ebf058fdf1cslivefilterByPrec g (State argIde _ _ _ _) (State opIde _ args (hd:_) _) =
5bf90772244e08b493f008381645dd3704417d40yoshiki if hd == termTok then
5bf90772244e08b493f008381645dd3704417d40yoshiki if opIde == listId || argIde == listId then True
5bf90772244e08b493f008381645dd3704417d40yoshiki else let n = length args in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if isLeftArg opIde n then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if isPostfix opIde && (isPrefix argIde
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive || isInfix argIde) then False
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive else checkArg g ALeft opIde argIde
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if isRightArg opIde n then
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive if isPrefix opIde && isInfix argIde then False
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive else checkArg g ARight opIde argIde
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive else checkAnyArg g opIde argIde
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive-- reconstructing positions
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslivesetPlainIdePos :: Id -> [Pos] -> (Id, [Pos])
06ba4a61654b3763ad65f52283832ebf058fdf1cslivesetPlainIdePos (Id ts cs _) ps =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (places, toks) = span isPlace (reverse ts)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive pls = reverse places
06ba4a61654b3763ad65f52283832ebf058fdf1cslive f = zipWith (\ a b -> up_pos (const b) a)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (ps1, ps2) = splitAt (length toks) ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive front = f (reverse toks) ps1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if null cs then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (ps3, ps4) = splitAt (length pls) ps2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in (Id (front ++ f pls ps3) [] [], ps4)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else let (newCs, ps3, ps4) = foldl (\ (prevCs, seps, rest) a ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (c1, qs) = setPlainIdePos a rest
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in (c1: prevCs, head qs : seps, tail qs))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ([], [head ps2], tail ps2) cs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (ps6, ps7) = splitAt (length pls) ps4
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in (Id (front ++ f pls ps6) (reverse newCs) (reverse ps3), ps7)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivesetIdePos :: Id -> [TERM] -> [Pos] -> Id
06ba4a61654b3763ad65f52283832ebf058fdf1cslivesetIdePos i@(Id ts _ _) ar ps =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let nt = length $ getTokenList True i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive np = length ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive na = length $ filter isPlace ts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (_, toks) = span isPlace (reverse ts)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if nt == np then -- literal places
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (newId, []) = setPlainIdePos i ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if np + na == nt && na == length ar then -- mixfix
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive let (newTps, rargs, rqs) = mergePos (reverse toks) ar ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (newId, []) = setPlainIdePos i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (newTps ++ rqs ++ map posOfTerm rargs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else error "setIdePos"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where mergePos [] args qs = ([], args, qs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mergePos (t:rs) args qs =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if isPlace t then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (tokps, rargs, rqs) = mergePos rs (tail args) qs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in (posOfTerm (head args) : tokps, rargs, rqs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else let (tokps, rargs, rqs) = mergePos rs args (tail qs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in (head qs : tokps, rargs, rqs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- constructing the parse tree from (the final) parser state(s)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivestateToAppl :: State -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslivestateToAppl (State ide rs a _ _) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let vs = getTokenList True ide
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ar = reverse a
06ba4a61654b3763ad65f52283832ebf058fdf1cslive qs = reverse rs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if vs == [termTok, colonTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive || vs == [termTok, asTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive || vs == [varTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive || vs == [opTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive || vs == [predTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive || vs == [parenTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then head ar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if vs == [opTok, parenTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then let Application q _ _ = head ar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_parenthesized ts ps = head a
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in Application q ts ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if vs == [predTok, parenTok]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then Mixfix_term [head ar, head a]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else case ar of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [Mixfix_parenthesized ts ps] ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Application (Op_name
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (setIdePos ide ts qs))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> let newIde@(Id (t:_) _ _) = setIdePos ide ar qs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive pos = if isPlace t then posOfTerm $ head ar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else tokPos t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in Application (Op_name newIde) ar [pos]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -- true mixfix
06ba4a61654b3763ad65f52283832ebf058fdf1csliveasListAppl :: GlobalAnnos -> State -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1csliveasListAppl g s@(State i bs a _ _) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if i == listId then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case list_lit $ literal_annos g of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> error "asListAppl"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (b, c, f) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (b1, b2) = getListBrackets b
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nb1 = length b1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nb2 = length b2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ra = reverse a
06ba4a61654b3763ad65f52283832ebf058fdf1cslive na = length ra
06ba4a61654b3763ad65f52283832ebf058fdf1cslive nb = length bs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkList [] ps = asAppl c [] (head ps)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkList (hd:tl) ps = asAppl f [hd, mkList tl (tail ps)] (head ps)
5bf90772244e08b493f008381645dd3704417d40yoshiki in if null a then asAppl c [] (if null bs then nullPos else last bs)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if nb + 1 == nb1 + nb2 + na then
5bf90772244e08b493f008381645dd3704417d40yoshiki let br = reverse bs
5bf90772244e08b493f008381645dd3704417d40yoshiki br1 = drop (nb1 - 1) br
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in mkList (reverse a) br1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else error "asListAppl"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else stateToAppl s
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- when a grammar rule (mixfix Id) has been fully matched
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecollectArg :: GlobalAnnos -> ParseMap -> State -> [State]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- pre: finished rule
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecollectArg g m s@(State _ _ _ _ k) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (\ (State o b a ts k1) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive State o b (asListAppl g s : a)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (tail ts) k1)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ filter (filterByPrec g s)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ lookUp m k
5bf90772244e08b493f008381645dd3704417d40yoshikicompl :: GlobalAnnos -> ParseMap -> [State] -> [State]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecompl g m l =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive concat $ map (collectArg g m)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ filter (\ (State _ _ _ ts _) -> null ts) l
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecomplRec :: GlobalAnnos -> ParseMap -> [State] -> [State]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecomplRec g m l = let l1 = compl g m l in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if null l1 then l else complRec g m l1 ++ l
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecomplete :: GlobalAnnos -> Int -> ParseMap -> ParseMap
06ba4a61654b3763ad65f52283832ebf058fdf1cslivecomplete g i m = addToFM m i $ complRec g m $ lookUp m i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- predict which rules/ids might match for (the) nonterminal(s) (termTok)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- provided the "dot" is followed by a nonterminal
5bf90772244e08b493f008381645dd3704417d40yoshikipredict :: GlobalAnnos -> Set Id -> Int -> ParseMap -> ParseMap
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslivepredict g is i m = if i /= 0 && any (\ (State _ _ _ ts _) -> not (null ts)
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive && head ts == termTok)
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive (lookUp m i)
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive then addToFM_C (++) m i (initialState g is i)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetype Chart = (Int, [Diagnosis], ParseMap)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivenextState :: GlobalAnnos -> Set Id -> TERM -> Chart -> Chart
06ba4a61654b3763ad65f52283832ebf058fdf1cslivenextState g is trm (i, ds, m) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let m1 = complete g (i+1) $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive scan trm i $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive predict g is i m
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if null (lookUp m1 (i+1)) && null ds
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then (i+1, Diag Error ("unexpected mixfix token: "
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ++ showTerm g trm)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (posOfTerm trm) : ds, m)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else (i+1, ds, m1)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveiterateStates :: GlobalAnnos -> Set Id -> Set Id -> [TERM] -> Chart -> Chart
06ba4a61654b3763ad65f52283832ebf058fdf1csliveiterateStates g ops preds terms c@(i, ds, m) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let self = iterateStates g ops preds
06ba4a61654b3763ad65f52283832ebf058fdf1cslive resolveTerm = resolveMixfix g ops preds False
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if null terms then c
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else case head terms of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_term ts -> self (ts ++ tail terms) c
5bf90772244e08b493f008381645dd3704417d40yoshiki Mixfix_bracketed ts ps ->
5bf90772244e08b493f008381645dd3704417d40yoshiki self (expand "[" "]" ts ps ++ tail terms) c
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_braced ts ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive self (expand "{" "}" ts ps ++ tail terms) c
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_parenthesized ts ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let Result mds v =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do tsNew <- mapM resolveTerm ts
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (Mixfix_parenthesized tsNew ps)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive tNew = case v of Nothing -> head terms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just x -> x
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in self (tail terms) (nextState g ops tNew (i, ds++mds, m))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Conditional t1 f2 t3 ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let Result mds v =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do t4 <- resolveTerm t1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive f5 <- resolveFormula g ops preds f2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t6 <- resolveTerm t3
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (Conditional t4 f5 t6 ps)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive tNew = case v of Nothing -> head terms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just x -> x
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in self (tail terms) (nextState g ops tNew (i, ds++mds, m))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_token t -> let (ds1, trm) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive convertMixfixToken (literal_annos g) t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in self (tail terms)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (nextState g ops trm (i, ds1++ds, m))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t -> self (tail terms) (nextState g ops t c)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where expand = expandPos Mixfix_token
06ba4a61654b3763ad65f52283832ebf058fdf1csliveposOfTerm :: TERM -> Pos
06ba4a61654b3763ad65f52283832ebf058fdf1csliveposOfTerm trm =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case trm of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_token t -> tokPos t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_term ts -> posOfTerm (head ts)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Simple_id i -> tokPos i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_qual_pred p ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Pred_name i -> posOfId i
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Qual_pred_name _ _ ps -> first (Just ps)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Application (Qual_op_name _ _ ps) [] [] -> first (Just ps)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> first $ get_pos_l trm
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where first ps = case ps of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> nullPos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just l -> if null l then nullPos else head l
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetAppls :: GlobalAnnos -> Int -> ParseMap -> [TERM]
06ba4a61654b3763ad65f52283832ebf058fdf1cslivegetAppls g i m =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (asListAppl g) $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive filter (\ (State _ _ _ ts k) -> null ts && k == 0) $
06ba4a61654b3763ad65f52283832ebf058fdf1csliveresolveMixfix :: GlobalAnnos -> Set Id -> Set Id -> Bool -> TERM -> Result TERM
06ba4a61654b3763ad65f52283832ebf058fdf1csliveresolveMixfix g ops preds mayBeFormula trm =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (i, ds, m) = iterateStates g ops preds [trm]
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive (0, [], unitFM 0 $ initialState g
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive (if mayBeFormula then ops `union` preds else ops) 0)
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive ts = getAppls g i m
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive in if null ts then if null ds then
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive plain_error trm ("no resolution for term: "
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive ++ showTerm g trm)
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive (posOfTerm trm)
4f854c24127e28f7ad72ce9a39d4448aaf910fc1slive else Result ds (Just trm)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if null $ tail ts then Result ds (Just (head ts))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else Result (Diag Error ("ambiguous mixfix term\n\t" ++
5bf90772244e08b493f008381645dd3704417d40yoshiki $ intersperse "\n\t"
5bf90772244e08b493f008381645dd3704417d40yoshiki $ map (showTerm g)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ take 5 ts)) (posOfTerm trm) : ds) (Just trm)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveresolveFormula :: GlobalAnnos -> Set Id -> Set Id -> FORMULA -> Result FORMULA
06ba4a61654b3763ad65f52283832ebf058fdf1csliveresolveFormula g ops preds frm =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let self = resolveFormula g ops preds
06ba4a61654b3763ad65f52283832ebf058fdf1cslive resolveTerm = resolveMixfix g ops preds False in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case frm of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Quantification q vs fOld ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let varIds = foldl (\ l (Var_decl va _ _) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map (\t->Id[t][][]) va ++ l) [] vs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do fNew <- resolveFormula g (fromList varIds `union` ops)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Quantification q vs fNew ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Conjunction fsOld ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do fsNew <- mapM self fsOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Conjunction fsNew ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Disjunction fsOld ps ->
5bf90772244e08b493f008381645dd3704417d40yoshiki do fsNew <- mapM self fsOld
5bf90772244e08b493f008381645dd3704417d40yoshiki return $ Disjunction fsNew ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Implication f1 f2 ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do f3 <- self f1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive f4 <- self f2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Implication f3 f4 ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Equivalence f1 f2 ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do f3 <- self f1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive f4 <- self f2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Equivalence f3 f4 ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Negation fOld ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do fNew <- self fOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Negation fNew ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Predication sym tsOld ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do tsNew <- mapM resolveTerm tsOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Predication sym tsNew ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Definedness tOld ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do tNew <- resolveTerm tOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Definedness tNew ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Existl_equation t1 t2 ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do t3 <- resolveTerm t1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t4 <- resolveTerm t2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Existl_equation t3 t4 ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Strong_equation t1 t2 ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do t3 <- resolveTerm t1
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t4 <- resolveTerm t2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Strong_equation t3 t4 ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Membership tOld s ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do tNew <- resolveTerm tOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Membership tNew s ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_formula tOld ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do tNew <- resolveMixfix g ops preds True tOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive mkPredication tNew
06ba4a61654b3763ad65f52283832ebf058fdf1cslive where mkPredication t =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_parenthesized [t0] ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive do p <- mkPredication t0
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ if null ps then p
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else updFormulaPos (head ps) (last ps) p
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Application (Op_name ide) args ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let p = Predication (Pred_name ide) args ps in
5bf90772244e08b493f008381645dd3704417d40yoshiki if ide `member` preds then return p
5bf90772244e08b493f008381645dd3704417d40yoshiki else plain_error p
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ("not a predicate: " ++ showId ide "")
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (posOfTerm t)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_qual_pred qide ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Predication qide [] []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_term [Mixfix_qual_pred qide,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_parenthesized ts ps] ->
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive return $ Predication qide ts ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_term _ -> return $ Mixfix_formula t -- still wrong
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> plain_error (Mixfix_formula t)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ("not a formula: " ++ showTerm g t)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (posOfTerm t)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive f -> return f
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- ---------------------------------------------------------------
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- convert literals
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- ---------------------------------------------------------------
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- isChar :: Token -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- isChar t = head (tokStr t) == '\''
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisString :: Token -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisString t = head (tokStr t) == '\"'
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisNumber :: Token -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisNumber t = let s = tokStr t in length s > 1 && C.isDigit (head s)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisFloating :: Token -> Bool
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- precondition: isNumber
06ba4a61654b3763ad65f52283832ebf058fdf1csliveisFloating t = any (\c -> c == '.' || c == 'E') (tokStr t)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveparseString :: Parser a -> String -> a
06ba4a61654b3763ad65f52283832ebf058fdf1csliveparseString p s = case parse p "" s of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Left _ -> error "parseString"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Right x -> x
5bf90772244e08b493f008381645dd3704417d40yoshikisplit :: Parser a -> String -> (a, String)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivesplit p s = let ph = do hd <- p;
06ba4a61654b3763ad65f52283832ebf058fdf1cslive tl <- getInput;
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return (hd, tl)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in parseString ph s
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeStringTerm :: Id -> Id -> Token -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeStringTerm c f tok =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive makeStrTerm (incSourceColumn sp 1) str
06ba4a61654b3763ad65f52283832ebf058fdf1cslive sp = tokPos tok
06ba4a61654b3763ad65f52283832ebf058fdf1cslive str = init (tail (tokStr tok))
5bf90772244e08b493f008381645dd3704417d40yoshiki makeStrTerm p l =
5bf90772244e08b493f008381645dd3704417d40yoshiki if null l then asAppl c [] p
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else let (hd, tl) = split caslChar l
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in asAppl f [asAppl (Id [Token ("'" ++ hd ++ "'") p] [] []) [] p,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive makeStrTerm (incSourceColumn p $ length hd) tl] p
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeNumberTerm :: Id -> Token -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeNumberTerm f t@(Token n p) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [] -> error "makeNumberTerm"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [_] -> asAppl (Id [t] [] []) [] p
06ba4a61654b3763ad65f52283832ebf058fdf1cslive hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] p,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive makeNumberTerm f (Token tl
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (incSourceColumn p 1))] p
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeFraction :: Id -> Id -> Token -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeFraction f d t@(Token s p) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (n, r) = span (\c -> c /= '.') s
5bf90772244e08b493f008381645dd3704417d40yoshiki dotOffset = length n
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if null r then makeNumberTerm f t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else asAppl d [makeNumberTerm f (Token n p),
06ba4a61654b3763ad65f52283832ebf058fdf1cslive makeNumberTerm f (Token (tail r)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (incSourceColumn p $ dotOffset + 1))]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ incSourceColumn p dotOffset
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeSignedNumber :: Id -> Token -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeSignedNumber f t@(Token n p) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [] -> error "makeSignedNumber"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if hd == '-' || hd == '+' then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive asAppl (Id [Token [hd] p] [] [])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive [makeNumberTerm f (Token tl $ incSourceColumn p 1)] p
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else makeNumberTerm f t
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeFloatTerm :: Id -> Id -> Id -> Token -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1cslivemakeFloatTerm f d e t@(Token s p) =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let (m, r) = span (\c -> c /= 'E') s
06ba4a61654b3763ad65f52283832ebf058fdf1cslive offset = length m
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if null r then makeFraction f d t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else asAppl e [makeFraction f d (Token m p),
06ba4a61654b3763ad65f52283832ebf058fdf1cslive makeSignedNumber f (Token (tail r)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ incSourceColumn p (offset + 1))]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ incSourceColumn p offset
06ba4a61654b3763ad65f52283832ebf058fdf1csliveasAppl :: Id -> [TERM] -> Pos -> TERM
06ba4a61654b3763ad65f52283832ebf058fdf1csliveasAppl f args p = let pos = if null args then [] else [p]
5bf90772244e08b493f008381645dd3704417d40yoshiki in Application (Op_name f) args pos
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- analyse Mixfix_token
06ba4a61654b3763ad65f52283832ebf058fdf1csliveconvertMixfixToken:: LiteralAnnos -> Token -> ([Diagnosis], TERM)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveconvertMixfixToken ga t =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if isString t then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case string_lit ga of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> err "string"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (c, f) -> ([], makeStringTerm c f t)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else if isNumber t then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case number_lit ga of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> err "number"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just f -> if isFloating t then
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case float_lit ga of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Nothing -> err "floating"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Just (d, e) -> ([], makeFloatTerm f d e t)
5bf90772244e08b493f008381645dd3704417d40yoshiki else ([], makeNumberTerm f t)
5bf90772244e08b493f008381645dd3704417d40yoshiki else ([], te)
5bf90772244e08b493f008381645dd3704417d40yoshiki where te = Mixfix_token t
06ba4a61654b3763ad65f52283832ebf058fdf1cslive err s = ([Diag Error ("missing %" ++ s ++ " annotation") (tokPos t)]