MixfixParser.hs revision 71de4b92b1ca12890a9e7bc5b0301455da3e052f
97a9a944b5887e91042b019776c41d5dd74557aferikabeleModule : $Header$
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveCopyright : Christian Maeder and Uni Bremen 2002-2003
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
fe64b2ba25510d8c9dba5560a2d537763566cf40ndMaintainer : hets@tzi.de
fe64b2ba25510d8c9dba5560a2d537763566cf40ndStability : experimental
fe64b2ba25510d8c9dba5560a2d537763566cf40ndPortability : portable
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix analysis of terms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Missing features:
fe64b2ba25510d8c9dba5560a2d537763566cf40nd - the positions of ids from string, list, number and floating annotations
fe64b2ba25510d8c9dba5560a2d537763566cf40nd is not changed within applications (and might be misleading)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndmodule CASL.MixfixParser ( resolveFormula, resolveMixfix)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport qualified Common.Lib.Set as Set
fe64b2ba25510d8c9dba5560a2d537763566cf40ndimport Control.Exception (assert)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- > 0 means predicate
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkRule :: Id -> Rule
58699879a562774640b95e9eedfd891f336e38c2ndmkRule = mixRule 0
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkSingleArgRule :: Int -> Id -> Rule
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkSingleOpArgRule :: Int -> Id -> Rule
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkSingleOpArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [exprTok])
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkArgsRule :: Int -> Id -> Rule
117c1f888a14e73cdd821dc6c23eb0411144a41cndmkArgsRule b ide = (protect ide, b, getPlainTokenList ide
117c1f888a14e73cdd821dc6c23eb0411144a41cnd ++ getTokenPlaceList tupleId)
117c1f888a14e73cdd821dc6c23eb0411144a41cndsingleArgId, singleOpArgId, multiArgsId :: Id
117c1f888a14e73cdd821dc6c23eb0411144a41cndsingleArgId = mkId (getPlainTokenList exprId ++ [varTok])
117c1f888a14e73cdd821dc6c23eb0411144a41cndsingleOpArgId = mkId (getPlainTokenList exprId ++ [exprTok])
117c1f888a14e73cdd821dc6c23eb0411144a41cndmultiArgsId = mkId (getPlainTokenList exprId ++
117c1f888a14e73cdd821dc6c23eb0411144a41cnd getPlainTokenList tupleId)
117c1f888a14e73cdd821dc6c23eb0411144a41cndinitRules :: GlobalAnnos -> IdSet -> Int -> [Rule]
117c1f888a14e73cdd821dc6c23eb0411144a41cndinitRules ga (opS, predS, _) maybeFormula =
117c1f888a14e73cdd821dc6c23eb0411144a41cnd let ops = Set.toList opS
117c1f888a14e73cdd821dc6c23eb0411144a41cnd preds = if maybeFormula > 0 then
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Set.toList predS else []
117c1f888a14e73cdd821dc6c23eb0411144a41cnd in concat [ mkRule typeId :
117c1f888a14e73cdd821dc6c23eb0411144a41cnd mkRule exprId :
117c1f888a14e73cdd821dc6c23eb0411144a41cnd mkRule varId :
117c1f888a14e73cdd821dc6c23eb0411144a41cnd mkRule singleArgId :
117c1f888a14e73cdd821dc6c23eb0411144a41cnd mkRule singleOpArgId :
117c1f888a14e73cdd821dc6c23eb0411144a41cnd mkRule multiArgsId :
117c1f888a14e73cdd821dc6c23eb0411144a41cnd listRules 0 ga,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mixRule 1) preds,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mkSingleArgRule 1) preds,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mkSingleOpArgRule 1) preds,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mkArgsRule 1) preds,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map mkRule ops,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mkSingleArgRule 0) ops,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mkSingleOpArgRule 0) ops,
117c1f888a14e73cdd821dc6c23eb0411144a41cnd map (mkArgsRule 0) ops]
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- | meaningful position of a term
117c1f888a14e73cdd821dc6c23eb0411144a41cndposOfTerm :: TERM f -> Pos
117c1f888a14e73cdd821dc6c23eb0411144a41cndposOfTerm trm =
117c1f888a14e73cdd821dc6c23eb0411144a41cnd case trm of
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Mixfix_token t -> tokPos t
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Mixfix_term ts -> headPos $ map posOfTerm ts
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Simple_id i -> tokPos i
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Mixfix_qual_pred p ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Pred_name i -> posOfId i
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Qual_pred_name i _ _ -> posOfId i
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Application o _ _ ->
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Op_name i -> posOfId i
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Qual_op_name i _ _ -> posOfId i
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Qual_var v _ _ -> tokPos v
117c1f888a14e73cdd821dc6c23eb0411144a41cnd Sorted_term t _ _ -> posOfTerm t
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Cast t _ _ -> posOfTerm t
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Conditional t _ _ _ -> posOfTerm t
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Unparsed_term _ ps -> headPos ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix_sorted_term _ ps -> headPos ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix_cast _ ps -> headPos ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix_parenthesized _ ps -> headPos ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix_bracketed _ ps -> headPos ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix_braced _ ps -> headPos ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | construct application
fe64b2ba25510d8c9dba5560a2d537763566cf40ndasAppl :: Id -> [TERM f] -> [Pos] -> TERM f
fe64b2ba25510d8c9dba5560a2d537763566cf40ndasAppl f as ps = Application (Op_name f) as ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | constructing the parse tree from (the final) parser state(s)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndtoAppl :: Id -> [TERM f] -> [Pos] -> TERM f
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetoAppl ide ar qs =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if ide == singleArgId || ide == multiArgsId
06ba4a61654b3763ad65f52283832ebf058fdf1cslive then assert (length ar > 1) $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let har:tar = ar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ps = posOfTerm har : qs
fb77c505254b6e9c925e23e734463e87574f8f40kess in case har of
fb77c505254b6e9c925e23e734463e87574f8f40kess Application q ts _ -> assert (null ts) $
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Application q tar ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_qual_pred _ -> Mixfix_term [har,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_parenthesized tar ps]
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error "stateToAppl"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive else asAppl ide ar qs
06ba4a61654b3763ad65f52283832ebf058fdf1csliveaddType :: TERM f -> TERM f -> TERM f
06ba4a61654b3763ad65f52283832ebf058fdf1csliveaddType tt t =
fb77c505254b6e9c925e23e734463e87574f8f40kess Mixfix_sorted_term s ps -> Sorted_term t s ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_cast s ps -> Cast t s ps
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error "addType"
06ba4a61654b3763ad65f52283832ebf058fdf1cslivefilterByPredicate :: Int -> Int -> Maybe Bool
fb77c505254b6e9c925e23e734463e87574f8f40kessfilterByPredicate bArg bOp =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if bArg > 0 then Just False else
06ba4a61654b3763ad65f52283832ebf058fdf1cslive if bOp > 0 then Just True else Nothing
fb77c505254b6e9c925e23e734463e87574f8f40kesstype TermChart f = Chart (TERM f)
06ba4a61654b3763ad65f52283832ebf058fdf1csliveiterateCharts :: GlobalAnnos -> IdSet -> Int -> [TERM f] -> TermChart f
fb77c505254b6e9c925e23e734463e87574f8f40kess -> TermChart f
fb77c505254b6e9c925e23e734463e87574f8f40kessiterateCharts g ids maybeFormula terms c =
fb77c505254b6e9c925e23e734463e87574f8f40kess let self = iterateCharts g ids maybeFormula
06ba4a61654b3763ad65f52283832ebf058fdf1cslive expand = expandPos Mixfix_token
06ba4a61654b3763ad65f52283832ebf058fdf1cslive oneStep = nextChart addType filterByPredicate toAppl g c
06ba4a61654b3763ad65f52283832ebf058fdf1cslive resolveTerm = resolveMixTrm g ids 0
06ba4a61654b3763ad65f52283832ebf058fdf1cslive in if null terms then c
fb77c505254b6e9c925e23e734463e87574f8f40kess else case head terms of
fb77c505254b6e9c925e23e734463e87574f8f40kess Mixfix_term ts -> self (ts ++ tail terms) c
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Mixfix_bracketed ts ps ->
fb77c505254b6e9c925e23e734463e87574f8f40kess self (expand ("[", "]") ts ps ++ tail terms) c
fb77c505254b6e9c925e23e734463e87574f8f40kess Mixfix_braced ts ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive self (expand ("{", "}") ts ps ++ tail terms) c
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Mixfix_parenthesized ts ps ->
130d299c4b2b15be45532a176604c71fdc7bea5bnd if isSingle ts then
130d299c4b2b15be45532a176604c71fdc7bea5bnd let Result mds v = resolveMixTrm g ids maybeFormula
130d299c4b2b15be45532a176604c71fdc7bea5bnd tNew = case v of Nothing -> head ts
130d299c4b2b15be45532a176604c71fdc7bea5bnd Just x -> x
130d299c4b2b15be45532a176604c71fdc7bea5bnd c2 = self (tail terms) (oneStep (tNew, varTok))
130d299c4b2b15be45532a176604c71fdc7bea5bnd in mixDiags mds c2
130d299c4b2b15be45532a176604c71fdc7bea5bnd else self (expand ("(", ")") ts ps ++ tail terms) c
130d299c4b2b15be45532a176604c71fdc7bea5bnd Conditional t1 f2 t3 ps ->
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd let Result mds v =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd do t4 <- resolveTerm t1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd f5 <- resolveMixFrm g ids f2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd t6 <- resolveTerm t3
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return (Conditional t4 f5 t6 ps)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd tNew = case v of Nothing -> head terms
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just x -> x
fe64b2ba25510d8c9dba5560a2d537763566cf40nd c2 = self (tail terms)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in mixDiags mds c2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Mixfix_token t -> let (ds1, trm) = convertMixfixToken
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (literal_annos g) asAppl Mixfix_token t
fe64b2ba25510d8c9dba5560a2d537763566cf40nd c2 = self (tail terms) $ oneStep $
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess case trm of
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive Mixfix_token tok -> (trm, tok)
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive _ -> (trm, varTok
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive {tokPos = tokPos t})
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive in mixDiags ds1 c2
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t@(Mixfix_sorted_term _ (p:_)) -> self (tail terms)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (oneStep (t, typeTok {tokPos = p}))
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd t@(Mixfix_cast _ (p:_)) -> self (tail terms)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd (oneStep (t, typeTok {tokPos = p}))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t@(Qual_var _ _ (p:_)) -> self (tail terms)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (oneStep (t, varTok {tokPos = p}))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t@(Application (Qual_op_name _ _ (p:_)) _ _) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive t@(Mixfix_qual_pred (Qual_pred_name _ _ (p:_))) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
06ba4a61654b3763ad65f52283832ebf058fdf1cslive _ -> error "iterateCharts"
130d299c4b2b15be45532a176604c71fdc7bea5bndmkIdSet ops preds =
130d299c4b2b15be45532a176604c71fdc7bea5bnd let both = Set.intersection ops preds in
130d299c4b2b15be45532a176604c71fdc7bea5bnd (ops, Set.difference preds both, preds)
130d299c4b2b15be45532a176604c71fdc7bea5bndresolveMixfix :: GlobalAnnos -> Set.Set Id -> Set.Set Id -> Bool -> TERM f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> Result (TERM f)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveMixfix g ops preds maybeFormula t =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let r@(Result ds _) = resolveMixTrm g (mkIdSet ops preds)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd (if maybeFormula then 1 else 0) t
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in if null ds then r else Result ds Nothing
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveMixTrm :: GlobalAnnos -> IdSet -> Int -> TERM f -> Result (TERM f)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveMixTrm ga ids maybeFormula trm =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd getResolved showTerm (posOfTerm trm) toAppl
fe64b2ba25510d8c9dba5560a2d537763566cf40nd $ iterateCharts ga ids maybeFormula [trm] $
fe64b2ba25510d8c9dba5560a2d537763566cf40nd initChart (initRules ga ids maybeFormula) Set.empty
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveFormula :: GlobalAnnos -> Set.Set Id -> Set.Set Id -> (FORMULA f)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -> Result (FORMULA f)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveFormula g ops preds f =
fe64b2ba25510d8c9dba5560a2d537763566cf40nd let r@(Result ds _) = resolveMixFrm g (mkIdSet ops preds) f
fe64b2ba25510d8c9dba5560a2d537763566cf40nd in if null ds then r else Result ds Nothing
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveMixFrm :: GlobalAnnos -> IdSet-> FORMULA f -> Result (FORMULA f)
fe64b2ba25510d8c9dba5560a2d537763566cf40ndresolveMixFrm g ids@(ops, onlyPreds, preds) frm =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let self = resolveMixFrm g ids
06ba4a61654b3763ad65f52283832ebf058fdf1cslive resolveTerm = resolveMixTrm g ids 0 in
06ba4a61654b3763ad65f52283832ebf058fdf1cslive case frm of
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Quantification q vs fOld ps ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive let varIds = Set.fromList $ concatMap (\ (Var_decl va _ _) ->
06ba4a61654b3763ad65f52283832ebf058fdf1cslive map simpleIdToId va) vs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive newIds = (Set.union ops varIds,
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (Set.\\) onlyPreds varIds, preds)
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd do fNew <- resolveMixFrm g newIds fOld
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ Quantification q vs fNew ps
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd Conjunction fsOld ps ->
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd do fsNew <- mapM self fsOld
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd return $ Conjunction fsNew ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Disjunction fsOld ps ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd do fsNew <- mapM self fsOld
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ Disjunction fsNew ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Implication f1 f2 b ps ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd do f3 <- self f1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd f4 <- self f2
fb77c505254b6e9c925e23e734463e87574f8f40kess return $ Implication f3 f4 b ps
fb77c505254b6e9c925e23e734463e87574f8f40kess Equivalence f1 f2 ps ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd do f3 <- self f1
fe64b2ba25510d8c9dba5560a2d537763566cf40nd f4 <- self f2
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ Equivalence f3 f4 ps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Negation fOld ps ->
fe64b2ba25510d8c9dba5560a2d537763566cf40nd do fNew <- self fOld
fe64b2ba25510d8c9dba5560a2d537763566cf40nd return $ Negation fNew ps
58699879a562774640b95e9eedfd891f336e38c2nd Predication sym tsOld ps ->
58699879a562774640b95e9eedfd891f336e38c2nd do tsNew <- mapM resolveTerm tsOld
58699879a562774640b95e9eedfd891f336e38c2nd return $ Predication sym tsNew ps
fb77c505254b6e9c925e23e734463e87574f8f40kess Definedness tOld ps ->
fb77c505254b6e9c925e23e734463e87574f8f40kess do tNew <- resolveTerm tOld
fb77c505254b6e9c925e23e734463e87574f8f40kess return $ Definedness tNew ps
fb77c505254b6e9c925e23e734463e87574f8f40kess Existl_equation t1 t2 ps ->
fb77c505254b6e9c925e23e734463e87574f8f40kess do t3 <- resolveTerm t1
58699879a562774640b95e9eedfd891f336e38c2nd t4 <- resolveTerm t2
58699879a562774640b95e9eedfd891f336e38c2nd return $ Existl_equation t3 t4 ps
58699879a562774640b95e9eedfd891f336e38c2nd Strong_equation t1 t2 ps ->
58699879a562774640b95e9eedfd891f336e38c2nd do t3 <- resolveTerm t1
58699879a562774640b95e9eedfd891f336e38c2nd t4 <- resolveTerm t2
58699879a562774640b95e9eedfd891f336e38c2nd return $ Strong_equation t3 t4 ps
58699879a562774640b95e9eedfd891f336e38c2nd Membership tOld s ps ->
58699879a562774640b95e9eedfd891f336e38c2nd do tNew <- resolveTerm tOld
58699879a562774640b95e9eedfd891f336e38c2nd return $ Membership tNew s ps
58699879a562774640b95e9eedfd891f336e38c2nd Mixfix_formula tOld ->
58699879a562774640b95e9eedfd891f336e38c2nd do tNew <- resolveMixTrm g ids 1 tOld
fb77c505254b6e9c925e23e734463e87574f8f40kess mkPredication tNew
fb77c505254b6e9c925e23e734463e87574f8f40kess where mkPredication t =
58699879a562774640b95e9eedfd891f336e38c2nd Application (Op_name ide) as ps ->
58699879a562774640b95e9eedfd891f336e38c2nd let p = Predication (Pred_name ide) as ps in
58699879a562774640b95e9eedfd891f336e38c2nd if ide `Set.member` preds
58699879a562774640b95e9eedfd891f336e38c2nd then return p else
58699879a562774640b95e9eedfd891f336e38c2nd plain_error p
58699879a562774640b95e9eedfd891f336e38c2nd ("not a predicate: " ++ showId ide "")
58699879a562774640b95e9eedfd891f336e38c2nd (posOfId ide)
58699879a562774640b95e9eedfd891f336e38c2nd Mixfix_qual_pred qide ->
58699879a562774640b95e9eedfd891f336e38c2nd return $ Predication qide [] []
58699879a562774640b95e9eedfd891f336e38c2nd Mixfix_term [Mixfix_qual_pred qide,
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess Mixfix_parenthesized ts ps] ->
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd return $ Predication qide ts ps
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd _ -> plain_error (Mixfix_formula t)
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd ("not a formula: " ++ showTerm t "")
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd (posOfTerm t)
4a7affccb2f1f5b94cab395e1bf3825aed715ebcnd f -> return f