- the positions of ids from string, list, number and floating annotations
is not changed within applications (and might be misleading)
- using (Set State) instead of [State] avoids explosion
but detection of local ambiguities (that of subterms) is more difficult,
solution: equal list states should be merged into a single state
that stores the local ambiguity
import qualified Char as C
showTerm :: GlobalAnnos -> TERM -> String
data State = State (Id, Bool) -- True means predicate
[Pos] -- positions of Id tokens
[TERM] -- currently collected arguments
[Token] -- only tokens after the "dot" are given
State r1 _ _ t1 p1 == State r2 _ _ t2 p2 = (r1, t1, p1) == (r2, t2, p2)
State r1 _ _ t1 p1 <= State r2 _ _ t2 p2 = (r1, t1, p1) <= (r2, t2, p2)
commaTok, parenTok, termTok :: Token
commaTok = mkSimpleId "," -- for list elements
termTok = mkSimpleId termStr
parenTok = mkSimpleId "(..)"
colonTok, asTok, varTok, opTok, predTok :: Token
colonTok = mkSimpleId ":"
varTok = mkSimpleId "(v)"
predTok = mkSimpleId "(p)"
mkState :: Int -> Bool -> Id -> State
mkState i b ide = State (ide, b) [] [] (getTokenList termStr ide) i
mkApplState :: Int -> Bool -> Id -> State
mkApplState i b ide = State (ide, b) [] []
(getPlainTokenList ide ++ [parenTok]) i
listToken = mkSimpleId "[]"
-- unique id (usually "[]" yields two tokens)
listId i = Id [listToken] [i] []
isListId (Id ts cs _) = not (null ts) && head ts == listToken && isSingle cs
listStates :: GlobalAnnos -> Int -> [State]
let lists = list_lit $ literal_annos g
listState co toks = State (listId co, False) [] [] toks i
in concatMap ( \ (bs, n, c) ->
let (b1, b2, cs) = getListBrackets bs
e = Id (b1 ++ b2) cs [] in
(if e == n then [] -- add b1 ++ b2 if its not yet included by n
else [listState c $ getPlainTokenList e]) ++
[listState c (b1 ++ [termTok] ++ b2)
, listState c (b1 ++ [termTok, commaTok] ++ b2)]
-- these are the possible matches for the nonterminal TERM
-- the same states are used for the predictions
initialState :: GlobalAnnos -> ([Id], [Id]) -> Int -> [State]
initialState g (ops, preds) i =
let mkPredState b toks = State (Id toks [] [], b) [] [] toks i
mkTokState = mkPredState False
in concat [mkTokState [parenTok] :
mkTokState [termTok, colonTok] :
mkTokState [termTok, asTok] :
mkTokState [opTok, parenTok] :
mkPredState True [predTok] :
mkPredState True [predTok, parenTok] :
map (mkState i True) preds,
map (mkApplState i True) preds,
map (mkState i False) ops,
map (mkApplState i False) ops]
type ParseMap = Map Int [State]
lookUp :: (Ord a, MonadPlus m) => Map a (m b) -> a -> (m b)
lookUp ce k = findWithDefault mzero k ce
-- match (and shift) a token (or partially finished term)
scan :: TERM -> Int -> ParseMap -> ParseMap
Mixfix_sorted_term _ _ -> colonTok
Mixfix_parenthesized _ _ -> parenTok
Application (Qual_op_name _ _ _) [] _ -> opTok
Mixfix_qual_pred _ -> predTok
foldr (\ (State o b a ts k) l ->
if null ts || head ts /= t then l
else let p = tokPos t : b in
if t == commaTok && isListId (fst o) then
-- list elements separator
(termTok : commaTok : tail ts) k)
: (State o p a (termTok : tail ts) k) : l
else if t == parenTok then
(State o b (trm : a) (tail ts) k) : l
else if t == varTok || t == opTok || t == predTok then
(State o b [trm] (tail ts) k) : l
else if t == colonTok || t == asTok then
(State o b [mkTerm $ head a] [] k) : l
else (State o p a (tail ts) k) : l) []
where mkTerm t1 = case trm of
Mixfix_sorted_term s ps -> Sorted_term t1 s ps
Mixfix_cast s ps -> Cast t1 s ps
-- precedence graph stuff
checkArg :: GlobalAnnos -> AssocEither -> Id -> Id -> Bool
then isAssoc dir (assoc_annos g) op || not (isInfix op)
case precRel (prec_annos g) op arg of
NoDirection -> not $ isInfix arg
checkAnyArg :: GlobalAnnos -> Id -> Id -> Bool
case precRel (prec_annos g) op arg of
BothDirections -> isInfix op && op == arg
isLeftArg, isRightArg :: Id -> Int -> Bool
isLeftArg (Id ts _ _) n = n + 1 == (length $ takeWhile isPlace ts)
isRightArg (Id ts _ _) n = n == (length $ filter isPlace ts) -
(length $ takeWhile isPlace (reverse ts))
filterByPrec :: GlobalAnnos -> State -> State -> Bool
filterByPrec _ _ (State _ _ _ [] _) = False
filterByPrec g (State (argIde, predArg) _ _ _ _)
(State (opIde, predOp) _ args (hd:_) _) =
else if isListId opIde || isListId argIde || predOp
if isLeftArg opIde n then
if isPostfix opIde && (isPrefix argIde
|| isInfix argIde) then False
else checkArg g ALeft opIde argIde
else if isRightArg opIde n then
if isPrefix opIde && isInfix argIde then False
else checkArg g ARight opIde argIde
else checkAnyArg g opIde argIde
-- constructing the parse tree from (the final) parser state(s)
stateToAppl :: State -> TERM
stateToAppl (State (ide, _) rs a _ _) =
let vs = getPlainTokenList ide
in if vs == [termTok, colonTok]
|| vs == [termTok, asTok]
Mixfix_parenthesized ts _ -> if isSingle ts then head ts
else if vs == [opTok, parenTok]
then let Application q _ _ = head ar
Mixfix_parenthesized ts ps = head a
else if vs == [predTok, parenTok]
then Mixfix_term [head ar, head a]
[Mixfix_parenthesized ts ps] ->
_ -> let newIde@(Id (t:_) _ _) = setIdePos ide ar qs
pos = if isPlace t then posOfTerm $ head ar
in Application (Op_name newIde) ar [pos]
asListAppl :: GlobalAnnos -> State -> TERM
asListAppl g s@(State (i,_) bs a _ _) =
ListCons b c = getLiteralType g f
(b1, _, _) = getListBrackets b
cl = length $ getPlainTokenList b
mkList [] ps = asAppl c [] (head ps)
mkList (hd:tl) ps = asAppl f [hd, mkList tl (tail ps)] (head ps)
in if null a then asAppl c [] (if null bs then nullPos else last bs)
else if nb + 2 == cl + na then
in mkList (reverse a) br1
-- when a grammar rule (mixfix Id) has been fully matched
collectArg :: GlobalAnnos -> ParseMap -> State -> [State]
collectArg g m s@(State _ _ _ _ k) =
map (\ (State o b a ts k1) ->
State o b (asListAppl g s : a)
$ filter (filterByPrec g s)
compl :: GlobalAnnos -> ParseMap -> [State] -> [State]
concat $ map (collectArg g m)
$ filter (\ (State _ _ _ ts _) -> null ts) l
complRec :: GlobalAnnos -> ParseMap -> [State] -> [State]
if null l1 then l else complRec g m l1 ++ l
complete :: GlobalAnnos -> Int -> ParseMap -> ParseMap
-- predict which
rules/ids might match for (the) nonterminal(s) (termTok)
-- provided the "dot" is followed by a nonterminal
predict :: GlobalAnnos -> [Id] -> Int -> ParseMap -> ParseMap
if i /= 0 && any (\ (State _ _ _ ts _) -> not (null ts)
&& head ts == termTok) (lookUp m i)
then insertWith (++) i (initialState g (ops, []) i) m
type Chart = (Int, [Diagnosis], ParseMap)
nextState :: GlobalAnnos -> [Id] -> TERM
nextState g ops trm (i, ds, m) =
let m1 = complete g (i+1) $
in if null (lookUp m1 (i+1)) && null ds
then (i+1, Diag Error ("unexpected mixfix token: "
type IdSet = (Set Id, Set Id, Set Id)
iterateStates :: GlobalAnnos -> IdSet -> Bool -> [TERM] -> Chart -> Chart
iterateStates g ids@(ops, _, _) maybeFormula terms c@(i, ds, m) =
let self = iterateStates g ids maybeFormula
expand = expandPos Mixfix_token
resolvePred = resolveMixTrm g ids
resolveTerm = resolvePred maybeFormula
Mixfix_term ts -> self (ts ++ tail terms) c
Mixfix_bracketed ts ps ->
self (expand ("[", "]") ts ps ++ tail terms) c
self (expand ("{", "}") ts ps ++ tail terms) c
Mixfix_parenthesized ts ps ->
do tsNew <- mapM resolveTerm ts
return $ Mixfix_parenthesized tsNew ps
tNew = case v of Nothing -> head terms
in self (tail terms) (oneStep tNew (i, ds++mds, m))
Conditional t1 f2 t3 ps ->
do t4 <- resolvePred False t1
f5 <- resolveMixFrm g ids f2
t6 <- resolvePred False t3
return (Conditional t4 f5 t6 ps)
tNew = case v of Nothing -> head terms
in self (tail terms) (oneStep tNew (i, ds++mds, m))
Mixfix_token t -> let (ds1, trm) =
convertMixfixToken (literal_annos g) t
(oneStep trm (i, ds1++ds, m))
t -> self (tail terms) (oneStep t c)
Mixfix_token t -> tokPos t
Mixfix_term ts -> posOfTerm (head ts)
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
Just l -> if null l then nullPos else head l
getAppls :: GlobalAnnos -> Int -> ParseMap -> [TERM]
filter (\ (State _ _ _ ts k) -> null ts && k == 0) $
mkIdSet :: Set Id -> Set Id -> IdSet
resolveMixfix :: GlobalAnnos -> Set Id -> Set Id -> Bool -> TERM -> Result TERM
resolveMixfix g ops preds maybeFormula t =
let r@(Result ds _) = resolveMixTrm g (mkIdSet ops preds) maybeFormula t
in if null ds then r else Result ds Nothing
resolveMixTrm :: GlobalAnnos -> IdSet -> Bool
resolveMixTrm g ids@(ops, preds, _) mayBeFormula trm =
let (i, ds, m) = iterateStates g ids mayBeFormula [trm]
in if null ts then if null ds then
plain_error trm ("no resolution for term: "
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" ++
$ take 5 ts)) (posOfTerm trm) : ds) (Just trm)
resolveFormula :: GlobalAnnos -> Set Id -> Set Id -> FORMULA -> Result FORMULA
resolveFormula g ops preds f =
let r@(Result ds _) = resolveMixFrm g (mkIdSet ops preds) f
in if null ds then r else Result ds Nothing
resolveMixFrm :: GlobalAnnos -> IdSet-> FORMULA -> Result FORMULA
resolveMixFrm g ids@(ops, onlyPreds, preds) frm =
let self = resolveMixFrm g ids
resolveTerm = resolveMixTrm g ids False in
Quantification q vs fOld ps ->
let varIds =
Set.fromList $ concatMap (\ (Var_decl va _ _) ->
(Set.\\) onlyPreds varIds, preds)
do fNew <- resolveMixFrm g newIds fOld
return $ Quantification q vs fNew ps
do fsNew <- mapM self fsOld
return $ Conjunction fsNew ps
do fsNew <- mapM self fsOld
return $ Disjunction fsNew ps
return $ Implication f3 f4 ps
return $ Equivalence f3 f4 ps
return $ Negation fNew ps
Predication sym tsOld ps ->
do tsNew <- mapM resolveTerm tsOld
return $ Predication sym tsNew ps
do tNew <- resolveTerm tOld
return $ Definedness tNew ps
Existl_equation t1 t2 ps ->
return $ Existl_equation t3 t4 ps
Strong_equation t1 t2 ps ->
return $ Strong_equation t3 t4 ps
do tNew <- resolveTerm tOld
return $ Membership tNew s ps
do tNew <- resolveMixTrm g ids True tOld
Mixfix_parenthesized [t0] ps ->
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
("not a predicate: " ++ showId ide "")
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)
-- ---------------------------------------------------------------
-- ---------------------------------------------------------------
makeStringTerm :: Id -> Id -> Token -> TERM
makeStrTerm (incSourceColumn sp 1) str
str = init (tail (tokStr tok))
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) =
[] -> 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
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) =
[] -> error "makeSignedNumber"
if hd == '-' || hd == '+' then
asAppl (Id [Token [hd] p] [] [])
[makeNumberTerm f (Token tl $ incSourceColumn p 1)] p
makeFloatTerm :: Id -> Id -> Id -> Token -> TERM
makeFloatTerm f d e t@(Token s p) =
let (m, r) = span (\c -> c /= 'E') s
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
convertMixfixToken:: LiteralAnnos -> Token -> ([Diagnosis], TERM)
convertMixfixToken ga t =
Just (c, f) -> ([], makeStringTerm c f t)
Just f -> if isFloating t then
Nothing -> err "floating"
Just (d, e) -> ([], makeFloatTerm f d e t)
else ([], makeNumberTerm f t)
where te = Mixfix_token t
err s = ([Diag Error ("missing %" ++ s ++ " annotation") (tokPos t)]