MixfixParser.hs revision 75a6279dbae159d018ef812185416cf6df386c10
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederModule : $Header$
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederCopyright : Christian Maeder and Uni Bremen 2002-2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederMaintainer : hets@tzi.de
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederStability : experimental
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederPortability : portable
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder Mixfix analysis of terms
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder Missing features:
ea9ad77838dce923ced1df2ac09a7f0226363593Christian Maeder - the positions of ids from string, list, number and floating annotations
bc67ede91ef5309852f1ba3a5a0d6b429f405e9dChristian Maeder is not changed within applications (and might be misleading)
3ec187613707411408c677058155bc618f16dabbChristian Maedermodule CASL.MixfixParser ( resolveFormula, resolveMixfix)
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maederimport qualified Common.Lib.Set as Set
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- import Control.Exception (assert)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederassert :: Bool -> a -> a
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maederassert b a = if b then a else error ("assert")
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maedertype Rule = (Id, Bool, [Token]) -- True means predicate
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkRule :: Id -> Rule
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkRule = mixRule False
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkSingleArgRule :: Bool -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkSingleOpArgRule :: Bool -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkSingleOpArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [exprTok])
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkArgsRule :: Bool -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkArgsRule b ide = (protect ide, b, getPlainTokenList ide
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder ++ getTokenPlaceList tupleId)
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian MaedersingleArgId, singleOpArgId, multiArgsId :: Id
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian MaedersingleArgId = mkId (getPlainTokenList exprId ++ [varTok])
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian MaedersingleOpArgId = mkId (getPlainTokenList exprId ++ [exprTok])
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian MaedermultiArgsId = mkId (getPlainTokenList exprId ++
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder getPlainTokenList tupleId)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederinitRules :: GlobalAnnos -> IdSet -> Bool -> [Rule]
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederinitRules ga (opS, predS, _) maybeFormula =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder preds = if maybeFormula then
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder in concat [ mkRule typeId :
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder mkRule exprId :
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder mkRule varId :
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder mkRule singleArgId :
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder mkRule singleOpArgId :
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder mkRule multiArgsId :
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder listRules False ga,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mixRule True) preds,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mkSingleArgRule True) preds,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mkSingleOpArgRule True) preds,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mkArgsRule True) preds,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map mkRule ops,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mkSingleArgRule False) ops,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mkSingleOpArgRule False) ops,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map (mkArgsRule False) ops]
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | meaningful position of a term
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederposOfTerm :: TERM -> Pos
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederposOfTerm trm =
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Mixfix_token t -> tokPos t
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Mixfix_term ts -> posOfTerm (head ts)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Simple_id i -> tokPos i
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Mixfix_qual_pred p ->
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Pred_name i -> posOfId i
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Qual_pred_name _ _ ps -> first (Just ps)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Application o [] [] ->
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Op_name i -> posOfId i
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder Qual_op_name _ _ ps -> first (Just ps)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder _ -> first $ get_pos_l trm
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder where first ps = case ps of
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Nothing -> nullPos
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Just l -> if null l then nullPos else head l
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | construct application
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederasAppl :: Id -> [TERM] -> [Pos] -> TERM
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederasAppl f as ps = Application (Op_name f) as ps
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | constructing the parse tree from (the final) parser state(s)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedertoAppl :: Id -> Bool -> [TERM] -> [Pos] -> TERM
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedertoAppl ide _ ar qs =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder if ide == singleArgId || ide == multiArgsId
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder then assert (length ar > 1) $
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder let har:tar = ar
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder ps = posOfTerm har : qs
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder in case har of
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder Application q ts _ -> assert (null ts) $
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder Application q tar ps
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder Mixfix_qual_pred _ -> Mixfix_term [har,
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder Mixfix_parenthesized tar ps]
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder _ -> error "stateToAppl"
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder else asAppl ide ar qs
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maedertype IdSet = (Set.Set Id, Set.Set Id, Set.Set Id)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederaddType :: TERM -> TERM -> TERM
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederaddType tt t =
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Mixfix_sorted_term s ps -> Sorted_term t s ps
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Mixfix_cast s ps -> Cast t s ps
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder _ -> error "addType"
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian MaederfilterByPredicate :: Bool -> Bool -> Maybe Bool
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian MaederfilterByPredicate bArg bOp =
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder if bArg then Just False else
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder if bOp then Just True else Nothing
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maedertype TermChart = Chart TERM Bool
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederiterateCharts :: GlobalAnnos -> IdSet -> Bool -> [TERM] -> TermChart
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederiterateCharts g ids maybeFormula terms c =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder let self = iterateCharts g ids maybeFormula
f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder expand = expandPos Mixfix_token
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder oneStep = nextChart addType filterByPredicate toAppl g c
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder resolveTerm = resolveMixTrm g ids 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 ->
469af98c69977faf5666e689eae863c1606ce269Christian Maeder self (expand ("[", "]") ts ps ++ tail terms) c
ab7a0615fceecfe401c3229ce7147d2bafc80287Christian Maeder Mixfix_braced ts ps ->
469af98c69977faf5666e689eae863c1606ce269Christian Maeder self (expand ("{", "}") ts ps ++ tail terms) c
5d05fc7110bca98e897a726d60dd5f67c4100814Christian Maeder Mixfix_parenthesized ts ps ->
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder if isSingle ts then
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder let Result mds v = resolveMixTrm g ids maybeFormula
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder tNew = case v of Nothing -> head ts
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder in mixDiags mds c2
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder else self (expand ("(", ")") ts ps ++ tail terms) c
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Conditional t1 f2 t3 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let Result mds v =
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder do t4 <- resolveTerm t1
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder f5 <- resolveMixFrm g ids f2
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder t6 <- resolveTerm t3
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return (Conditional t4 f5 t6 ps)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder tNew = case v of Nothing -> head terms
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder c2 = self (tail terms)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder in mixDiags mds c2
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder Mixfix_token t -> let (ds1, trm) =
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder convertMixfixToken (literal_annos g) t
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder c2 = self (tail terms) $ oneStep $
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Mixfix_token tok -> (trm, tok)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder _ -> (trm, varTok
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder {tokPos = tokPos t})
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder in mixDiags ds1 c2
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder t@(Mixfix_sorted_term _ (p:_)) -> self (tail terms)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (oneStep (t, typeTok {tokPos = p}))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder t@(Mixfix_cast _ (p:_)) -> self (tail terms)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (oneStep (t, typeTok {tokPos = p}))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder t@(Qual_var _ _ (p:_)) -> self (tail terms)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (oneStep (t, varTok {tokPos = p}))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder t@(Application (Qual_op_name _ _ (p:_)) _ _) ->
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ (p:_))) ->
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder t -> error ("iterate mixfix states: " ++ show t)
dd836737068504898d4f7843ebd8a3df05f3067dChristian MaedermkIdSet :: Set.Set Id -> Set.Set Id -> IdSet
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkIdSet ops preds =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let both = Set.intersection ops preds in
e1997b6204d2de9f4f496c2db72b5e754c66a3cbChristian Maeder (ops, Set.difference preds both, preds)
dd836737068504898d4f7843ebd8a3df05f3067dChristian MaederresolveMixfix :: GlobalAnnos -> Set.Set Id -> Set.Set Id -> Bool -> TERM
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder -> Result TERM
8dddde4041af20b71009e6092440fc393f91666aChristian MaederresolveMixfix g ops preds maybeFormula t =
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder let r@(Result ds _) = resolveMixTrm g (mkIdSet ops preds) maybeFormula t
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder in if null ds then r else Result ds Nothing
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederresolveMixTrm :: GlobalAnnos -> IdSet -> Bool
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder -> TERM -> Result TERM
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederresolveMixTrm ga ids maybeFormula trm =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder getResolved showTerm (posOfTerm trm) toAppl
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder $ iterateCharts ga ids maybeFormula [trm] $
aeb1d2a7487f480dbab690ec77f51b5a57cb04dfChristian Maeder initChart (initRules ga ids maybeFormula) Set.empty
dd836737068504898d4f7843ebd8a3df05f3067dChristian MaederresolveFormula :: GlobalAnnos -> Set.Set Id -> Set.Set Id -> FORMULA
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maeder -> Result FORMULA
8dddde4041af20b71009e6092440fc393f91666aChristian MaederresolveFormula g ops preds f =
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder let r@(Result ds _) = resolveMixFrm g (mkIdSet ops preds) f
8dddde4041af20b71009e6092440fc393f91666aChristian Maeder in if null ds then r else Result ds Nothing
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaederresolveMixFrm :: GlobalAnnos -> IdSet-> FORMULA -> Result FORMULA
e1997b6204d2de9f4f496c2db72b5e754c66a3cbChristian MaederresolveMixFrm g ids@(ops, onlyPreds, preds) frm =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let self = resolveMixFrm g ids
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder resolveTerm = resolveMixTrm g ids False in
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Quantification q vs fOld ps ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let varIds = Set.fromList $ concatMap (\ (Var_decl va _ _) ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder map simpleIdToId va) vs
e1997b6204d2de9f4f496c2db72b5e754c66a3cbChristian Maeder newIds = (Set.union ops varIds,
e1997b6204d2de9f4f496c2db72b5e754c66a3cbChristian Maeder (Set.\\) onlyPreds varIds, preds)
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder do fNew <- resolveMixFrm g newIds fOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Quantification q vs fNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Conjunction fsOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fsNew <- mapM self fsOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Conjunction fsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Disjunction fsOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fsNew <- mapM self fsOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Disjunction fsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Implication f1 f2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do f3 <- self f1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f4 <- self f2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Implication f3 f4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Equivalence f1 f2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do f3 <- self f1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f4 <- self f2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Equivalence f3 f4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Negation fOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do fNew <- self fOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Negation fNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Predication sym tsOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tsNew <- mapM resolveTerm tsOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Predication sym tsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Definedness tOld ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tNew <- resolveTerm tOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Definedness tNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Existl_equation t1 t2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do t3 <- resolveTerm t1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t4 <- resolveTerm t2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Existl_equation t3 t4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Strong_equation t1 t2 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do t3 <- resolveTerm t1
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder t4 <- resolveTerm t2
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Strong_equation t3 t4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Membership tOld s ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder do tNew <- resolveTerm tOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder return $ Membership tNew s ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_formula tOld ->
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder do tNew <- resolveMixTrm g ids True tOld
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder mkPredication tNew
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder where mkPredication t =
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder Application (Op_name ide) as ps ->
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder let p = Predication (Pred_name ide) as ps in
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder then return p else
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder plain_error p
14327755c1e6236e5a23594980a4b82bdce4d0a0Christian Maeder ("not a predicate: " ++ showId ide "")
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (posOfId ide)
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
959680c14d514a07eebf7a0c9f786f86a4fcf1ebChristian Maeder _ -> plain_error (Mixfix_formula t)
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder ("not a formula: " ++ showTerm t "")
1eb602487b8b0dff5fad820439fc27264eb8889cChristian Maeder (posOfTerm t)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- convert literals
93fa7e4374de6e37328e752991a698bf03032c75Christian Maeder-- ---------------------------------------------------------------
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 =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder if null l then asAppl c [] [p]
6e6ba3ab90205840b9c0ea408befaed7d1d7b80bChristian Maeder else let (hd, tl) = splitString caslChar l
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder in asAppl f [asAppl (Id [Token ("'" ++ hd ++ "'") p] [] []) [] [p],
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder makeStrTerm (incSourceColumn p $ length hd) tl] [p]
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian MaedermakeNumberTerm :: Id -> Token -> TERM
2f98027959ced502c0332e557618b42e41a2504aChristian MaedermakeNumberTerm f t@(Token n p) =
e31c7e91ecb4b23aac070f64fa1b099c05aadd0dChristian Maeder [] -> error "makeNumberTerm"
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder [_] -> asAppl (Id [t] [] []) [] [p]
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] [p],
2f98027959ced502c0332e557618b42e41a2504aChristian Maeder makeNumberTerm f (Token tl
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian 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))]
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian 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] [] [])
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian 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))]
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder [incSourceColumn p offset]
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)]