MixfixParser.hs revision 26d3a8da6b4244d65614b5585927df4948e542a0
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)
a255351561838b3743d03c1629d335cfb8b83804Christian Maedermodule CASL.MixfixParser (resolveFormula, resolveMixfix, MixResolve
deb8b0dec8533bc6260d47ded15a3e216819fa39Christian Maeder ,resolveMixTrm, resolveMixFrm, mkIdSet)
dd836737068504898d4f7843ebd8a3df05f3067dChristian Maederimport qualified Common.Lib.Set as Set
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder-- > 0 means predicate
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkRule :: Id -> Rule
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedermkRule = mixRule 0
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedermkSingleArgRule :: Int -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedermkSingleOpArgRule :: Int -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkSingleOpArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [exprTok])
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedermkArgsRule :: Int -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkArgsRule b ide = (protect ide, b, getPlainTokenList ide
a255351561838b3743d03c1629d335cfb8b83804Christian 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 ++
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder getPlainTokenList tupleId)
b502963581a463467939d578b211cb7a173c5428Christian MaederinitRules :: GlobalAnnos -> IdSet -> [Rule]
906f0b21e2dc78ee4f37f879518be018a0204cd9Christian MaederinitRules ga (opS, predS) =
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 :
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder listRules 0 ga,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mixRule 1) preds,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mkSingleArgRule 1) preds,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mkSingleOpArgRule 1) preds,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mkArgsRule 1) preds,
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder map mkRule ops,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mkSingleArgRule 0) ops,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mkSingleOpArgRule 0) ops,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder map (mkArgsRule 0) ops]
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | meaningful position of a term
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederposOfTerm :: TERM f -> Pos
9963c741a47c42d2dedc6e4589c1b197129a6239Christian MaederposOfTerm trm =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_token t -> tokPos t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_term ts -> headPos $ map posOfTerm ts
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Simple_id i -> tokPos i
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_qual_pred p ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Pred_name i -> posOfId i
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Qual_pred_name i _ _ -> posOfId i
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Application o _ _ ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Op_name i -> posOfId i
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Qual_op_name i _ _ -> posOfId i
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Qual_var v _ _ -> tokPos v
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Sorted_term t _ _ -> posOfTerm t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Cast t _ _ -> posOfTerm t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Conditional t _ _ _ -> posOfTerm t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Unparsed_term _ ps -> headPos ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_sorted_term _ ps -> headPos ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_cast _ ps -> headPos ps
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Mixfix_parenthesized _ ps -> headPos ps
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Mixfix_bracketed _ ps -> headPos ps
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Mixfix_braced _ ps -> headPos ps
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | construct application
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederasAppl :: Id -> [TERM f] -> [Pos] -> TERM f
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaederasAppl f as ps = Application (Op_name f) as ps
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | constructing the parse tree from (the final) parser state(s)
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedertoAppl :: Id -> [TERM f] -> [Pos] -> TERM f
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedertoAppl ide ar qs =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder if ide == singleArgId || ide == multiArgsId
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder then assert (length ar > 1) $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let har:tar = ar
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ps = posOfTerm har : qs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in case har of
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Application q ts _ -> assert (null ts) $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Application q tar ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_qual_pred _ -> Mixfix_term [har,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_parenthesized tar ps]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> error "stateToAppl"
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder else asAppl ide ar qs
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederaddType :: TERM f -> TERM f -> TERM f
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"
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaederfilterByPredicate :: Int -> Int -> Maybe Bool
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian MaederfilterByPredicate bArg bOp =
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder if bArg > 0 then Just False else
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder if bOp > 0 then Just True else Nothing
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maedertype TermChart f = Chart (TERM f)
a255351561838b3743d03c1629d335cfb8b83804Christian Maedertype MixResolve f = GlobalAnnos -> IdSet -> f -> Result f
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederiterateCharts :: PrettyPrint f => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> GlobalAnnos -> IdSet -> [TERM f]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> TermChart f -> TermChart f
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederiterateCharts par extR g ids terms c =
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let self = iterateCharts par extR g ids
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder expand = expandPos Mixfix_token
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder oneStep = nextChart addType filterByPredicate toAppl g c
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder resolveTerm = resolveMixTrm par extR g ids
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 ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder self (expand ("[", "]") ts ps ++ tail terms) c
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_braced ts ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder self (expand ("{", "}") ts ps ++ tail terms) c
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_parenthesized ts ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder if isSingle ts then
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let Result mds v = resolveTerm
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder tNew = case v of Nothing -> head ts
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in mixDiags mds c2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder else self (expand ("(", ")") ts ps ++ tail terms) c
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Conditional t1 f2 t3 ps ->
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder let Result mds v =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do t4 <- resolveTerm t1
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder f5 <- resolveMixFrm par extR g ids f2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t6 <- resolveTerm t3
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return (Conditional t4 f5 t6 ps)
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder tNew = case v of Nothing -> head terms
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder c2 = self (tail terms)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in mixDiags mds c2
95936ba3a6577d40aae065aafac4147f5a308782Christian Maeder Mixfix_token t -> let (ds1, trm) = convertMixfixToken
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (literal_annos g) asAppl Mixfix_token t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder c2 = self (tail terms) $ oneStep $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_token tok -> (trm, tok)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> (trm, varTok
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder {tokPos = tokPos t})
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in mixDiags ds1 c2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t@(Mixfix_sorted_term _ (p:_)) -> self (tail terms)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (oneStep (t, typeTok {tokPos = p}))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t@(Mixfix_cast _ (p:_)) -> self (tail terms)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (oneStep (t, typeTok {tokPos = p}))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t@(Qual_var _ _ (p:_)) -> self (tail terms)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (oneStep (t, varTok {tokPos = p}))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t@(Application (Qual_op_name _ _ (p:_)) _ _) ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ (p:_))) ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder Sorted_term t s ps ->
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder let Result mds v = resolveTerm t
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder tNew = Sorted_term (case v of Nothing -> t
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder Just x -> x) s ps
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder in mixDiags mds c2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> error "iterateCharts"
dd836737068504898d4f7843ebd8a3df05f3067dChristian MaedermkIdSet :: Set.Set Id -> Set.Set Id -> IdSet
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian MaedermkIdSet ops preds =
690f3a0b5f77633547e0a797c96b005a5f6ae56cChristian Maeder let both = Set.intersection ops preds in
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (ops, Set.difference preds both)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveMixfix :: PrettyPrint f => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> GlobalAnnos -> Set.Set Id -> Set.Set Id
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> (TERM f) -> Result (TERM f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveMixfix par extR g ops preds t =
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let r@(Result ds _) = resolveMixTrm par extR g (mkIdSet ops preds) t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in if null ds then r else Result ds Nothing
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveMixTrm :: PrettyPrint f => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> MixResolve (TERM f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveMixTrm par extR ga ids trm =
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder getResolved (showTerm par ga) (posOfTerm trm) toAppl
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder $ iterateCharts par extR ga ids [trm] $
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder initChart (initRules ga ids) Set.empty
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaedershowTerm :: PrettyPrint f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaedershowTerm par ga = shows . printText0 ga . mapTerm par
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveFormula :: PrettyPrint f => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> GlobalAnnos -> Set.Set Id -> Set.Set Id
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder -> (FORMULA f) -> Result (FORMULA f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveFormula par extR g ops preds f =
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let r@(Result ds _) = resolveMixFrm par extR g (mkIdSet ops preds) f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in if null ds then r else Result ds Nothing
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveMixFrm :: PrettyPrint f => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> MixResolve (FORMULA f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian MaederresolveMixFrm par extR g ids@(ops, onlyPreds) frm =
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder let self = resolveMixFrm par extR g ids
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder resolveTerm = resolveMixTrm par extR g ids in
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Quantification q vs fOld ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder let varIds = Set.fromList $ concatMap (\ (Var_decl va _ _) ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder map simpleIdToId va) vs
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder newIds = (Set.union ops varIds,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (Set.\\) onlyPreds varIds)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder do fNew <- resolveMixFrm par extR g newIds fOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Quantification q vs fNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Conjunction fsOld ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do fsNew <- mapM self fsOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Conjunction fsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Disjunction fsOld ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do fsNew <- mapM self fsOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Disjunction fsNew ps
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Implication f1 f2 b ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do f3 <- self f1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f4 <- self f2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Implication f3 f4 b ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Equivalence f1 f2 ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do f3 <- self f1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f4 <- self f2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Equivalence f3 f4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Negation fOld ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do fNew <- self fOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Negation fNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Predication sym tsOld ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do tsNew <- mapM resolveTerm tsOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Predication sym tsNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Definedness tOld ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do tNew <- resolveTerm tOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Definedness tNew ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Existl_equation t1 t2 ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do t3 <- resolveTerm t1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t4 <- resolveTerm t2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Existl_equation t3 t4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Strong_equation t1 t2 ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do t3 <- resolveTerm t1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t4 <- resolveTerm t2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Strong_equation t3 t4 ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Membership tOld s ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do tNew <- resolveTerm tOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Membership tNew s ps
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder Mixfix_formula tOld ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do tNew <- resolveTerm tOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder mkPredication tNew
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder where mkPredication t =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Application (Op_name ide) as ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Predication (Pred_name ide) as ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_qual_pred qide ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Predication qide [] []
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_term [Mixfix_qual_pred qide,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_parenthesized ts ps] ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Predication qide ts ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> plain_error (Mixfix_formula t)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder ("not a formula: " ++ showTerm par g t "")
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder (posOfTerm t)
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ExtFORMULA f ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do newF <- extR g ids f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ ExtFORMULA newF
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f