MixfixParser.hs revision 42c01284bba8d7c8d995c8dfb96ace57d28ed1bc
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : Christian Maeder and Uni Bremen 2002-2003
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : maeder@tzi.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : experimental
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : portable
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMixfix analysis of terms
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder Missing features:
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder - the positions of ids from string, list, number and floating annotations
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder is not changed within applications (and might be misleading)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maedermodule CASL.MixfixParser (resolveFormula, resolveMixfix, MixResolve
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder ,resolveMixTrm, resolveMixFrm, IdSet, mkIdSet)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport qualified Common.Lib.Set as Set
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder-- > 0 means predicate
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian MaedermkRule :: Id -> Rule
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian MaedermkRule = mixRule 0
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian MaedermkSingleArgRule :: Int -> Id -> Rule
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian MaedermkSingleOpArgRule :: Int -> Id -> Rule
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian MaedermkSingleOpArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [exprTok])
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaedermkArgsRule :: Int -> Id -> Rule
473f5af6e4803fbeecc814065952396f2501039bChristian MaedermkArgsRule b ide = (protect ide, b, getPlainTokenList ide
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder ++ getTokenPlaceList tupleId)
473f5af6e4803fbeecc814065952396f2501039bChristian MaedersingleArgId, singleOpArgId, multiArgsId :: Id
473f5af6e4803fbeecc814065952396f2501039bChristian MaedersingleArgId = mkId (getPlainTokenList exprId ++ [varTok])
473f5af6e4803fbeecc814065952396f2501039bChristian MaedersingleOpArgId = mkId (getPlainTokenList exprId ++ [exprTok])
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaedermultiArgsId = mkId (getPlainTokenList exprId ++
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder getPlainTokenList tupleId)
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian MaederinitRules :: GlobalAnnos -> IdSet -> [Rule]
833d97d43e5f22c70c8abd79d344bc93a8ded319Christian MaederinitRules ga (opS, predS) =
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder in concat [ mkRule typeId :
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder mkRule exprId :
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder mkRule varId :
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder mkRule singleArgId :
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder mkRule singleOpArgId :
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder mkRule multiArgsId :
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder listRules 0 ga,
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder map (mixRule 1) preds,
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder map (mkSingleArgRule 1) preds,
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder map (mkSingleOpArgRule 1) preds,
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder map (mkArgsRule 1) preds,
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder map mkRule ops,
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder map (mkSingleArgRule 0) ops,
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder map (mkSingleOpArgRule 0) ops,
8dfcec5538467723b1cf9d1651de7c9c89fe4aabChristian Maeder map (mkArgsRule 0) ops]
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder-- | meaningful position of a term
945e82ed7877917f3ab1657f555e71991372546aChristian MaederposOfTerm :: PosItem f => TERM f -> Range
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederposOfTerm trm =
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder Mixfix_token t -> tokPos t
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Mixfix_term ts -> concatMapRange posOfTerm ts
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Mixfix_qual_pred p ->
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Pred_name i -> posOfId i
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder Qual_pred_name i _ _ -> posOfId i
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Application o _ ps -> if isNullRange ps then
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Op_name i -> posOfId i
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Qual_op_name i _ _ -> posOfId i) else ps
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder _ -> getRange trm
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- | construct application
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederasAppl :: Id -> [TERM f] -> Range -> TERM f
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederasAppl f as ps = Application (Op_name f) as
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder $ if isNullRange ps then posOfId f else ps
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder-- | constructing the parse tree from (the final) parser state(s)
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian MaedertoAppl :: PosItem f => Id -> [TERM f] -> Range -> TERM f
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian MaedertoAppl ide ar qs =
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder if ide == singleArgId || ide == multiArgsId
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder then assert (length ar > 1) $
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder let har:tar = ar
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder hp = posOfTerm har
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder ps = if isNullRange hp
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder else Range[head (rangeToList hp)] `appRange` qs
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder in case har of
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder Application q ts p -> assert (null ts) $
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder Application q tar $ (ps`appRange` p)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder Mixfix_qual_pred _ -> Mixfix_term [har,
5dd895cd3d794ecd2f0035ee3a7b6d6bf2eac5efChristian Maeder Mixfix_parenthesized tar ps]
5dd895cd3d794ecd2f0035ee3a7b6d6bf2eac5efChristian Maeder _ -> error "stateToAppl"
5dd895cd3d794ecd2f0035ee3a7b6d6bf2eac5efChristian Maeder else asAppl ide ar qs
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian MaederaddType :: TERM f -> TERM f -> TERM f
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian MaederaddType tt t =
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Mixfix_sorted_term s ps -> Sorted_term t s ps
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Mixfix_cast s ps -> Cast t s ps
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder _ -> error "addType"
5bedf8c26d27eac08962c78379bcb2e5cb529036Christian MaederfilterByPredicate :: Int -> Int -> Maybe Bool
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederfilterByPredicate bArg bOp =
e84c877ad38ce9312eab222a79f44da2015572d2Christian Maeder if bArg > 0 then Just False else
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder if bOp > 0 then Just True else Nothing
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maedertype TermChart f = Chart (TERM f)
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maedertype MixResolve f = GlobalAnnos -> IdSet -> f -> Result f
9d50556254571c0811e94b4d948463754812a5aaChristian MaederiterateCharts :: (PrettyPrint f, PosItem f) => (f -> f)
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder -> MixResolve f -> GlobalAnnos -> IdSet -> [TERM f]
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder -> TermChart f -> TermChart f
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian MaederiterateCharts par extR g ids terms c =
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder let self = iterateCharts par extR g ids
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder expand = expandPos Mixfix_token
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder oneStep = nextChart addType filterByPredicate toAppl g c
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder resolveTerm = resolveMixTrm par extR g ids
7c661ba558707feaa5d8a299365c2191e1afabb2Christian Maeder in if null terms then c
acd9ca9d8e79b7d7ba8227631afbcf839f0c4a5eChristian Maeder else case head terms of
c1bca76471ad22ac47f05b03576974762d364339Christian Maeder Mixfix_term ts -> self (ts ++ tail terms) c
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder Mixfix_bracketed ts ps ->
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder self (expand ("[", "]") ts ps ++ tail terms) c
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder Mixfix_braced ts ps ->
9d50556254571c0811e94b4d948463754812a5aaChristian Maeder self (expand ("{", "}") ts ps ++ tail terms) c
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder Mixfix_parenthesized ts ps ->
90f0ed9623257ce66c88c174acfe77fdfa7785e6Christian Maeder if isSingle ts then
5bedf8c26d27eac08962c78379bcb2e5cb529036Christian Maeder let Result mds v = resolveTerm
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder tNew = case v of Nothing -> head ts
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder in mixDiags mds c2
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder else self (expand ("(", ")") ts ps ++ tail terms) c
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Conditional t1 f2 t3 ps ->
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder let Result mds v =
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder do t4 <- resolveTerm t1
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder f5 <- resolveMixFrm par extR g ids f2
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder t6 <- resolveTerm t3
a150c2c1cf35ba98a6dda2163c96bca7c6453025Christian Maeder return (Conditional t4 f5 t6 ps)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder tNew = case v of Nothing -> head terms
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder c2 = self (tail terms)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder in mixDiags mds c2
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Mixfix_token t -> let (ds1, trm) = convertMixfixToken
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder (literal_annos g) asAppl Mixfix_token t
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder c2 = self (tail terms) $ oneStep $
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder Mixfix_token tok -> (trm, tok)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder _ -> (trm, varTok)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder in mixDiags ds1 c2
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder t@(Mixfix_sorted_term _ ps) -> self (tail terms)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder (oneStep (t, typeTok {tokPos = ps}))
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder t@(Mixfix_cast _ ps) -> self (tail terms)
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder (oneStep (t, typeTok {tokPos = ps}))
0bbc28585c7d42913167ff78a862ef25ea59e85eChristian Maeder t@(Qual_var _ _ ps) -> self (tail terms)
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder (oneStep (t, varTok {tokPos = ps}))
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder t@(Application (Qual_op_name _ _ ps) _ _) ->
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Sorted_term t s ps ->
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder let Result mds v = resolveTerm t
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder tNew = Sorted_term (case v of Nothing -> t
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Just x -> x) s ps
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder in mixDiags mds c2
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder _ -> error "iterateCharts"
526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaedermkIdSet :: Set.Set Id -> Set.Set Id -> IdSet
526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaedermkIdSet ops preds =
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder let both = Set.intersection ops preds in
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (ops, Set.difference preds both)
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaederresolveMixfix :: (PrettyPrint f, PosItem f) => (f -> f)
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder -> MixResolve f -> GlobalAnnos -> Set.Set Id -> Set.Set Id
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -> (TERM f) -> Result (TERM f)
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederresolveMixfix par extR g ops preds t =
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder let r@(Result ds _) = resolveMixTrm par extR g (mkIdSet ops preds) t
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder in if null ds then r else Result ds Nothing
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederresolveMixTrm :: (PrettyPrint f, PosItem f) => (f -> f)
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -> MixResolve f -> MixResolve (TERM f)
5896f38ba2934056542cb7cb3e6359e88a622547Christian MaederresolveMixTrm par extR ga ids trm =
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder getResolved (showTerm par ga) (posOfTerm trm) toAppl
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder $ iterateCharts par extR ga ids [trm] $
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder initChart (initRules ga ids) Set.empty
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian MaedershowTerm :: PrettyPrint f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian MaedershowTerm par ga = shows . printText0 ga . mapTerm par
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian MaederresolveFormula :: (PrettyPrint f, PosItem f) => (f -> f)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder -> MixResolve f -> GlobalAnnos -> Set.Set Id -> Set.Set Id
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder -> (FORMULA f) -> Result (FORMULA f)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian MaederresolveFormula par extR g ops preds f =
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder let r@(Result ds _) = resolveMixFrm par extR g (mkIdSet ops preds) f
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder in if null ds then r else Result ds Nothing
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian MaederresolveMixFrm :: (PrettyPrint f, PosItem f) => (f -> f)
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder -> MixResolve f -> MixResolve (FORMULA f)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian MaederresolveMixFrm par extR g ids@(ops, onlyPreds) frm =
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder let self = resolveMixFrm par extR g ids
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder resolveTerm = resolveMixTrm par extR g ids in
bd90cf050d470eb42f6e0b79327cc53bd0f80dc9Christian Maeder Quantification q vs fOld ps ->
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder let varIds = Set.fromList $ concatMap (\ (Var_decl va _ _) ->
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder map simpleIdToId va) vs
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder newIds = (Set.union ops varIds,
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder (Set.\\) onlyPreds varIds)
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder do fNew <- resolveMixFrm par extR g newIds fOld
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder return $ Quantification q vs fNew ps
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder Conjunction fsOld ps ->
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder do fsNew <- mapM self fsOld
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder return $ Conjunction fsNew ps
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder Disjunction fsOld ps ->
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder do fsNew <- mapM self fsOld
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder return $ Disjunction fsNew ps
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder Implication f1 f2 b ps ->
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder do f3 <- self f1
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder f4 <- self f2
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder return $ Implication f3 f4 b ps
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder Equivalence f1 f2 ps ->
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder do f3 <- self f1
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder f4 <- self f2
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder return $ Equivalence f3 f4 ps
3f08b178a44369b618a5e0b5f1fc2207fe043aabChristian Maeder Negation fOld ps ->
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder do fNew <- self fOld
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder return $ Negation fNew ps
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Predication sym tsOld ps ->
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder do tsNew <- mapM resolveTerm tsOld
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder return $ Predication sym tsNew ps
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Definedness tOld ps ->
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder do tNew <- resolveTerm tOld
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder return $ Definedness tNew ps
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Existl_equation t1 t2 ps ->
59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon Ulbricht do t3 <- resolveTerm t1
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder t4 <- resolveTerm t2
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder return $ Existl_equation t3 t4 ps
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder Strong_equation t1 t2 ps ->
ef1c24c8229ade3ac872febebd18c181e32fb9c4Christian Maeder do t3 <- resolveTerm t1
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder t4 <- resolveTerm t2
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder return $ Strong_equation t3 t4 ps
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder Membership tOld s ps ->
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder do tNew <- resolveTerm tOld
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder return $ Membership tNew s ps
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Mixfix_formula tOld ->
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder do tNew <- resolveTerm tOld
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder mkPredication tNew
4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder where mkPredication t =
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder Application (Op_name ide) as ps ->
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder return $ Predication (Pred_name ide) as ps
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder Mixfix_qual_pred qide ->
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder return $ Predication qide [] nullRange
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder Mixfix_term [Mixfix_qual_pred qide,
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder Mixfix_parenthesized ts ps] ->
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder return $ Predication qide ts ps
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder _ -> plain_error (Mixfix_formula t)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ("not a formula: " ++ showTerm par g t "")
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder (posOfTerm t)
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder ExtFORMULA f ->
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder do newF <- extR g ids f
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder return $ ExtFORMULA newF
f675b8f0a612e37472640da57b48d795bef4427eChristian Maeder f -> return f