ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder{- |

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederModule : $Header$

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederDescription : Mixfix analysis of terms

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederCopyright : Christian Maeder and Uni Bremen 2002-2006

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederMaintainer : Christian.Maeder@dfki.de

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederStability : experimental

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederPortability : portable

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederMixfix analysis of terms

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-}

7f0e81a8fc10c17b13569f23474a0e3fbfa79e7dChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule CASL.MixfixParser

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder ( resolveFormula, resolveMixfix, MixResolve

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , resolveMixTrm, resolveMixFrm

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , IdSets, mkIdSets, emptyIdSets, unite, single

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , makeRules, Mix(..), emptyMix

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder where

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport CASL.AS_Basic_CASL

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Common.GlobalAnnotations

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport Common.Result

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederimport Common.Id

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport qualified Data.Set as Set

7f0e81a8fc10c17b13569f23474a0e3fbfa79e7dChristian Maederimport qualified Data.Map as Map

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Common.Earley

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederimport Common.ConvertMixfixToken

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederimport Common.DocUtils

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Common.AS_Annotation

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport CASL.ShowMixfix

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport CASL.ToDoc()

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Control.Exception (assert)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederdata Mix b s f e = MixRecord

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder { getBaseIds :: b -> IdSets -- ^ ids of extra basic items

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , getSigIds :: s -> IdSets -- ^ ids of extra sig items

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , getExtIds :: e -> IdSets -- ^ ids of signature extensions

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , mixRules :: (Token -> [Rule], Rules) -- ^ rules for Earley

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , putParen :: f -> f -- ^ parenthesize extended formula

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , mixResolve :: MixResolve f -- ^ resolve extended formula

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder }

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- | an initially empty record

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederemptyMix :: Mix b s f e

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederemptyMix = MixRecord

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder { getBaseIds = const emptyIdSets

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder , getSigIds = const emptyIdSets

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , getExtIds = const emptyIdSets

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder , mixRules = error "emptyMix"

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder , putParen = id

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , mixResolve = const $ const return

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder }

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder-- precompute non-simple op and pred identifier for mixfix rules

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- | the precomputed sets of op and pred (non-simple) identifiers

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedertype IdSets = (Set.Set Id, Set.Set Id) -- ops are first component

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- | the empty 'IdSets'

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederemptyIdSets :: IdSets

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian MaederemptyIdSets = (Set.empty, Set.empty)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- | union 'IdSets'

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederunite :: [IdSets] -> IdSets

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederunite l = (Set.unions $ map fst l, Set.unions $ map snd l)

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- | get all ids of a basic spec

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_BASIC_SPEC f g (Basic_spec al) =

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder unite $ map (ids_BASIC_ITEMS f g . item) al

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder -> BASIC_ITEMS b s f -> IdSets

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_BASIC_ITEMS f g bi = case bi of

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Sig_items sis -> ids_SIG_ITEMS g sis

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Free_datatype _ al _ -> ids_anDATATYPE_DECLs al

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Ext_BASIC_ITEMS b -> f b

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder _ -> emptyIdSets

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederids_anDATATYPE_DECLs al =

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder (Set.unions $ map (ids_DATATYPE_DECL . item) al, Set.empty)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder-- | get all ids of a sig items

3c72be149cf673945cbe07a04c336fb8f4d406a3Christian Maederids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederids_SIG_ITEMS f si = case si of

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Sort_items _ _ _ -> emptyIdSets

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Op_items al _ -> (Set.unions $ map (ids_OP_ITEM . item) al, Set.empty)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Pred_items al _ -> (Set.empty, Set.unions $ map (ids_PRED_ITEM . item) al)

3c72be149cf673945cbe07a04c336fb8f4d406a3Christian Maeder Datatype_items _ al _ -> ids_anDATATYPE_DECLs al

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Ext_SIG_ITEMS s -> f s

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

3c72be149cf673945cbe07a04c336fb8f4d406a3Christian Maeder-- | get all op ids of an op item

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_OP_ITEM :: OP_ITEM f -> Set.Set Id

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_OP_ITEM o = case o of

3c72be149cf673945cbe07a04c336fb8f4d406a3Christian Maeder Op_decl ops _ _ _ -> Set.unions $ map single ops

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Op_defn i _ _ _ -> single i

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- | same as singleton

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedersingle :: Id -> Set.Set Id

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedersingle i = Set.singleton i

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- | get all pred ids of a pred item

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederids_PRED_ITEM p = case p of

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Pred_decl preds _ _ -> Set.unions $ map single preds

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Pred_defn i _ _ _ -> single i

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederids_DATATYPE_DECL :: DATATYPE_DECL -> Set.Set Id

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_DATATYPE_DECL (Datatype_decl _ al _) =

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Set.unions $ map (ids_ALTERNATIVE . item) al

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederids_ALTERNATIVE :: ALTERNATIVE -> Set.Set Id

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederids_ALTERNATIVE a = case a of

Alt_construct _ i cs _ -> Set.unions $ single i : map ids_COMPONENTS cs

Subsorts _ _ -> Set.empty

ids_COMPONENTS :: COMPONENTS -> Set.Set Id

ids_COMPONENTS c = case c of

Cons_select _ l _ _ -> Set.unions $ map single l

Sort _ -> Set.empty

-- predicates get lower precedence

mkRule :: Id -> Rule

mkRule = mixRule 1

mkSingleArgRule :: Int -> Id -> Rule

mkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])

mkArgsRule :: Int -> Id -> Rule

mkArgsRule b ide = (protect ide, b, getPlainTokenList ide

++ getTokenPlaceList tupleId)

singleArgId :: Id

singleArgId = mkId [exprTok, varTok]

multiArgsId :: Id

multiArgsId = mkId (exprTok : getPlainTokenList tupleId)

-- | additional scan rules

addRule :: GlobalAnnos -> [Rule] -> IdSets -> Token -> [Rule]

addRule ga uRules (ops, preds) tok =

let addR p = Set.fold ( \ i@(Id (t : _) _ _) ->

Map.insertWith (++) t

[mixRule p i, mkSingleArgRule p i, mkArgsRule p i])

lm = foldr ( \ r@(_, _, t : _) -> Map.insertWith (++) t [r])

Map.empty $ listRules 1 ga

(spreds, rpreds) = Set.partition isSimpleId preds

-- do not add simple ids as preds as these may be variables

-- with higher precedence

sops = Set.union ops spreds

varR = mkRule varId

m = Map.insert placeTok uRules

$ Map.insert varTok [varR]

$ Map.insert exprTok

[varR, mkRule singleArgId, mkRule multiArgsId]

$ addR 0 (addR 1 lm sops) rpreds

tId = mkId [tok]

tPId = mkId [tok, placeTok] -- prefix identifier

in (if isSimpleToken tok && not (Set.member tId sops)

then [mkRule tId] -- add rule for new variable

++ if Set.member tPId ops || Set.member tPId rpreds then [] else

[mkSingleArgRule 1 tId, mkArgsRule 1 tId]

-- add also rules for undeclared op

else []) ++ Map.findWithDefault [] tok m

-- insert only identifiers starting with a place

initRules :: IdSets -> Rules

initRules (opS, predS) =

let addR p = Set.fold ( \ i l -> mixRule p i : l)

in (addR 1 (addR 0 [mkRule typeId] predS) opS, [])

-- | construct rules from 'IdSets' to be put into a 'Mix' record

makeRules :: GlobalAnnos -> IdSets -> (Token -> [Rule], Rules)

makeRules ga (opS, predS) = let

(cOps, sOps) = Set.partition begPlace opS

(cPreds, sPreds) = Set.partition begPlace $ Set.difference predS opS

addR p = Set.fold ( \ i l ->

mkSingleArgRule p i : mkArgsRule p i : l)

uRules = addR 0 (addR 1 [] cOps) cPreds

in (addRule ga uRules (sOps, sPreds), initRules (cOps, cPreds))

-- | meaningful position of a term

posOfTerm :: TERM f -> Range

posOfTerm trm =

case trm of

Qual_var v _ ps -> if isNullRange ps then tokPos v else ps

Mixfix_term ts -> concatMapRange posOfTerm ts

Mixfix_qual_pred p -> posOfId $ predSymbName p

Application o _ ps -> if isNullRange ps then posOfId $ opSymbName o else ps

Conditional t1 _ t2 ps ->

if isNullRange ps then concatMapRange posOfTerm [t1, t2] else ps

Mixfix_parenthesized ts ps ->

if isNullRange ps then concatMapRange posOfTerm ts else ps

Mixfix_bracketed ts ps ->

if isNullRange ps then concatMapRange posOfTerm ts else ps

Mixfix_braced ts ps ->

if isNullRange ps then concatMapRange posOfTerm ts else ps

_ -> rangeOfTerm trm

-- | construct application

asAppl :: Id -> [TERM f] -> Range -> TERM f

asAppl f args ps = Application (Op_name f) args

$ if isNullRange ps then posOfId f else ps

-- | constructing the parse tree from (the final) parser state(s)

toAppl :: Id -> [TERM f] -> Range -> TERM f

toAppl ide ar qs =

if ide == singleArgId || ide == multiArgsId

then assert (length ar > 1) $

let har : tar = ar

hp = posOfTerm har

ps = appRange hp qs

in case har of

Application q ts p -> assert (null ts) $

Application q tar $ appRange ps p

Mixfix_qual_pred _ ->

Mixfix_term [har, Mixfix_parenthesized tar ps]

_ -> error "stateToAppl"

else asAppl ide ar qs

addType :: TERM f -> TERM f -> TERM f

addType tt t =

case tt of

Mixfix_sorted_term s ps -> Sorted_term t s ps

Mixfix_cast s ps -> Cast t s ps

_ -> error "addType"

-- | the type for mixfix resolution

type MixResolve f = GlobalAnnos -> (Token -> [Rule], Rules) -> f -> Result f

iterateCharts :: Pretty f => (f -> f)

-> MixResolve f -> GlobalAnnos -> [TERM f]

-> Chart (TERM f) -> Chart (TERM f)

iterateCharts par extR g terms c =

let self = iterateCharts par extR g

expand = expandPos Mixfix_token

oneStep = nextChart addType toAppl g c

ruleS = rules c

adder = addRules c

resolveTerm = resolveMixTrm par extR g (adder, ruleS)

in if null terms then c

else case head terms of

Mixfix_term ts -> self (ts ++ tail terms) c

Mixfix_bracketed ts ps ->

self (expand ("[", "]") ts ps ++ tail terms) c

Mixfix_braced ts ps ->

self (expand ("{", "}") ts ps ++ tail terms) c

Mixfix_parenthesized ts ps ->

case ts of

[h] -> let Result mds v = resolveTerm h

tNew = case v of

Nothing -> h

Just x -> x

c2 = self (tail terms) (oneStep (tNew, varTok))

in mixDiags mds c2

_ -> self (expand ("(", ")") ts ps ++ tail terms) c

h@(Conditional t1 f2 t3 ps) ->

let Result mds v =

do t4 <- resolveTerm t1

f5 <- resolveMixFrm par extR g (adder, ruleS) f2

t6 <- resolveTerm t3

return (Conditional t4 f5 t6 ps)

tNew = case v of

Nothing -> h

Just x -> x

c2 = self (tail terms)

(oneStep (tNew, varTok {tokPos = posOfTerm tNew}))

in mixDiags mds c2

Mixfix_token t -> let (ds1, trm) = convertMixfixToken

(literal_annos g) asAppl Mixfix_token t

c2 = self (tail terms) $ oneStep $

case trm of

Mixfix_token tok -> (trm, tok)

_ -> (trm, varTok)

in mixDiags ds1 c2

t@(Mixfix_sorted_term _ ps) -> self (tail terms)

(oneStep (t, typeTok {tokPos = ps}))

t@(Mixfix_cast _ ps) -> self (tail terms)

(oneStep (t, typeTok {tokPos = ps}))

t@(Qual_var _ _ ps) -> self (tail terms)

(oneStep (t, varTok {tokPos = ps}))

t@(Application (Qual_op_name _ _ ps) _ _) ->

self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))

t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->

self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))

Sorted_term t s ps ->

let Result mds v = resolveTerm t

tNew = Sorted_term (case v of

Nothing -> t

Just x -> x) s ps

c2 = self (tail terms) (oneStep (tNew, varTok))

in mixDiags mds c2

_ -> error "iterateCharts"

-- | construct 'IdSets' from op and pred identifiers

mkIdSets :: Set.Set Id -> Set.Set Id -> IdSets

mkIdSets ops preds = (ops, preds)

-- | top-level resolution like 'resolveMixTrm' that fails in case of diags

resolveMixfix :: Pretty f => (f -> f)

-> MixResolve f -> MixResolve (TERM f)

resolveMixfix par extR g ruleS t =

let r@(Result ds _) = resolveMixTrm par extR g ruleS t

in if null ds then r else Result ds Nothing

-- | basic term resolution that supports recursion without failure

resolveMixTrm :: Pretty f => (f -> f)

-> MixResolve f -> MixResolve (TERM f)

resolveMixTrm par extR ga (adder, ruleS) trm =

getResolved (showTerm par ga) (posOfTerm trm) toAppl

$ iterateCharts par extR ga [trm] $ initChart adder ruleS

showTerm :: Pretty f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS

showTerm par ga = showGlobalDoc ga . mapTerm par

-- | top-level resolution like 'resolveMixFrm' that fails in case of diags

resolveFormula :: Pretty f => (f -> f)

-> MixResolve f -> MixResolve (FORMULA f)

resolveFormula par extR g ruleS f =

let r@(Result ds _) = resolveMixFrm par extR g ruleS f

in if null ds then r else Result ds Nothing

-- | basic formula resolution that supports recursion without failure

resolveMixFrm :: Pretty f => (f -> f)

-> MixResolve f -> MixResolve (FORMULA f)

resolveMixFrm par extR g ids frm =

let self = resolveMixFrm par extR g ids

resolveTerm = resolveMixTrm par extR g ids in

case frm of

Quantification q vs fOld ps ->

do fNew <- resolveMixFrm par extR g ids fOld

return $ Quantification q vs fNew ps

Conjunction fsOld ps ->

do fsNew <- mapM self fsOld

return $ Conjunction fsNew ps

Disjunction fsOld ps ->

do fsNew <- mapM self fsOld

return $ Disjunction fsNew ps

Implication f1 f2 b ps ->

do f3 <- self f1

f4 <- self f2

return $ Implication f3 f4 b ps

Equivalence f1 f2 ps ->

do f3 <- self f1

f4 <- self f2

return $ Equivalence f3 f4 ps

Negation fOld ps ->

do fNew <- self fOld

return $ Negation fNew ps

Predication sym tsOld ps ->

do tsNew <- mapM resolveTerm tsOld

return $ Predication sym tsNew ps

Definedness tOld ps ->

do tNew <- resolveTerm tOld

return $ Definedness tNew ps

Existl_equation t1 t2 ps ->

do t3 <- resolveTerm t1

t4 <- resolveTerm t2

return $ Existl_equation t3 t4 ps

Strong_equation t1 t2 ps ->

do t3 <- resolveTerm t1

t4 <- resolveTerm t2

return $ Strong_equation t3 t4 ps

Membership tOld s ps ->

do tNew <- resolveTerm tOld

return $ Membership tNew s ps

Mixfix_formula tOld ->

do tNew <- resolveTerm tOld

case tNew of

Application (Op_name ide) args ps ->

return $ Predication (Pred_name ide) args ps

Mixfix_qual_pred qide ->

return $ Predication qide [] nullRange

Mixfix_term [Mixfix_qual_pred qide,

Mixfix_parenthesized ts ps] ->

return $ Predication qide ts ps

_ -> fatal_error

("not a formula: " ++ showTerm par g tNew "")

(posOfTerm tNew)

ExtFORMULA f ->

do newF <- extR g ids f

return $ ExtFORMULA newF

f -> return f