MixfixParser.hs revision 18d23ee9d489a7232f15606ccb0ca3880fff59db
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Mixfix analysis of terms
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederCopyright : Christian Maeder and Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederStability : experimental
ea9ad77838dce923ced1df2ac09a7f0226363593Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiMixfix analysis of terms
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder ( resolveFormula, resolveMixfix, MixResolve
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , resolveMixTrm, resolveMixFrm
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder , IdSets, mkIdSets, emptyIdSets, unite
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder , makeRules, Mix(..), emptyMix
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederdata Mix b s f e = MixRecord
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder { getBaseIds :: b -> IdSets -- ^ ids of extra basic items
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , getSigIds :: s -> IdSets -- ^ ids of extra sig items
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , getExtIds :: e -> IdSets -- ^ ids of signature extensions
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , mixRules :: (Token -> [Rule], Rules) -- ^ rules for Earley
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , putParen :: f -> f -- ^ parenthesize extended formula
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , mixResolve :: MixResolve f -- ^ resolve extended formula
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | an initially empty record
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederemptyMix :: Mix b s f e
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederemptyMix = MixRecord
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder { getBaseIds = const emptyIdSets
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , getSigIds = const emptyIdSets
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , getExtIds = const emptyIdSets
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , mixRules = error "emptyMix"
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , putParen = id
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , mixResolve = const $ const return
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- precompute non-simple op and pred identifier for mixfix rules
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | the precomputed sets of op and pred (non-simple) identifiers
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maedertype IdSets = (Set.Set Id, Set.Set Id) -- ops are first component
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | the empty 'IdSets'
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederemptyIdSets :: IdSets
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | union 'IdSets'
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederunite :: [IdSets] -> IdSets
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederunite l = (Set.unions $ map fst l, Set.unions $ map snd l)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | get all ids of a basic spec
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_BASIC_SPEC f g (Basic_spec al) =
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder unite $ map (ids_BASIC_ITEMS f g . item) al
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder -> BASIC_ITEMS b s f -> IdSets
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_BASIC_ITEMS f g bi = case bi of
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Sig_items sis -> ids_SIG_ITEMS g sis
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder Free_datatype _ al _ -> ids_anDATATYPE_DECLs al
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder Ext_BASIC_ITEMS b -> f b
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder _ -> emptyIdSets
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_anDATATYPE_DECLs al =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder (Set.unions $ map (ids_DATATYPE_DECL . item) al, Set.empty)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | get all ids of a sig items
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_SIG_ITEMS f si = case si of
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder Sort_items _ _ _ -> emptyIdSets
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Op_items al _ -> (Set.unions $ map (ids_OP_ITEM . item) al, Set.empty)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Pred_items al _ -> (Set.empty, Set.unions $ map (ids_PRED_ITEM . item) al)
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder Datatype_items _ al _ -> ids_anDATATYPE_DECLs al
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Ext_SIG_ITEMS s -> f s
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | get all op ids of an op item
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_OP_ITEM :: OP_ITEM f -> Set.Set Id
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_OP_ITEM o = case o of
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Op_decl ops _ _ _ -> Set.unions $ map Set.singleton ops
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Op_defn i _ _ _ -> Set.singleton i
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | get all pred ids of a pred item
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_PRED_ITEM p = case p of
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Pred_decl preds _ _ -> Set.unions $ map Set.singleton preds
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Pred_defn i _ _ _ -> Set.singleton i
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_DATATYPE_DECL :: DATATYPE_DECL -> Set.Set Id
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_DATATYPE_DECL (Datatype_decl _ al _) =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Set.unions $ map (ids_ALTERNATIVE . item) al
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_ALTERNATIVE :: ALTERNATIVE -> Set.Set Id
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_ALTERNATIVE a = case a of
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Alt_construct _ i cs _ ->
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Set.unions $ Set.singleton i : map ids_COMPONENTS cs
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Subsorts _ _ -> Set.empty
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_COMPONENTS :: COMPONENTS -> Set.Set Id
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederids_COMPONENTS c = case c of
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder Cons_select _ l _ _ -> Set.unions $ map Set.singleton l
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder-- predicates get lower precedence
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian MaedermkRule :: Id -> Rule
eed6203a39f88e398d86431a66d367036a3d17baChristian MaedermkRule = mixRule 1
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedermkSingleArgRule :: Int -> Id -> Rule
62198789c7cb57cac13399055515921c0fe3483fChristian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian MaedermkArgsRule :: Int -> Id -> Rule
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian MaedermkArgsRule b ide = (protect ide, b, getPlainTokenList ide
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder ++ getTokenPlaceList tupleId)
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaedersingleArgId :: Id
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian MaedersingleArgId = mkId [exprTok, varTok]
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaedermultiArgsId :: Id
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian MaedermultiArgsId = mkId (exprTok : getPlainTokenList tupleId)
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder-- | additional scan rules
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaederaddRule :: GlobalAnnos -> [Rule] -> IdSets -> Token -> [Rule]
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederaddRule ga uRules (ops, preds) tok =
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder let addR p = Set.fold ( \ i@(Id (t : _) _ _) ->
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder [mixRule p i, mkSingleArgRule p i, mkArgsRule p i])
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder lm = foldr ( \ r@(_, _, t : _) -> Map.insertWith (++) t [r])
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder Map.empty $ listRules 1 ga
a3000204685374be86c84d76323d95d86e4735acChristian Maeder (spreds, rpreds) = Set.partition isSimpleId preds
a3000204685374be86c84d76323d95d86e4735acChristian Maeder -- do not add simple ids as preds as these may be variables
a3000204685374be86c84d76323d95d86e4735acChristian Maeder -- with higher precedence
a3000204685374be86c84d76323d95d86e4735acChristian Maeder sops = Set.union ops spreds
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder varR = mkRule varId
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder m = Map.insert placeTok uRules
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder $ Map.insert varTok [varR]
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder [varR, mkRule singleArgId, mkRule multiArgsId]
a3000204685374be86c84d76323d95d86e4735acChristian Maeder $ addR 0 (addR 1 lm sops) rpreds
a3000204685374be86c84d76323d95d86e4735acChristian Maeder tId = mkId [tok]
a3000204685374be86c84d76323d95d86e4735acChristian Maeder tPId = mkId [tok, placeTok] -- prefix identifier
a3000204685374be86c84d76323d95d86e4735acChristian Maeder in (if isSimpleToken tok && not (Set.member tId sops)
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder then mkRule tId -- add rule for new variable
18d23ee9d489a7232f15606ccb0ca3880fff59dbChristian Maeder : if Set.member tPId ops || Set.member tPId rpreds
18d23ee9d489a7232f15606ccb0ca3880fff59dbChristian Maeder || Set.member applId ops || Set.member applId rpreds
18d23ee9d489a7232f15606ccb0ca3880fff59dbChristian Maeder then [] else [mkSingleArgRule 1 tId, mkArgsRule 1 tId]
a3000204685374be86c84d76323d95d86e4735acChristian Maeder -- add also rules for undeclared op
a3000204685374be86c84d76323d95d86e4735acChristian Maeder else []) ++ Map.findWithDefault [] tok m
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder-- insert only identifiers starting with a place
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaederinitRules :: IdSets -> Rules
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaederinitRules (opS, predS) =
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder let addR p = Set.fold ((:) . mixRule p)
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder in (addR 1 (addR 0 [mkRule typeId] predS) opS, [])
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | construct rules from 'IdSets' to be put into a 'Mix' record
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaedermakeRules :: GlobalAnnos -> IdSets -> (Token -> [Rule], Rules)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaedermakeRules ga (opS, predS) = let
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder (cOps, sOps) = Set.partition begPlace opS
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder (cPreds, sPreds) = Set.partition begPlace $ Set.difference predS opS
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder addR p = Set.fold ( \ i l ->
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder mkSingleArgRule p i : mkArgsRule p i : l)
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder uRules = addR 0 (addR 1 [] cOps) cPreds
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder in (addRule ga uRules (sOps, sPreds), initRules (cOps, cPreds))
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | construct application
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiasAppl :: Id -> [TERM f] -> Range -> TERM f
4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian MaederasAppl f args ps = Application (Op_name f) args
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski $ if isNullRange ps then posOfId f else ps
9963c741a47c42d2dedc6e4589c1b197129a6239Christian Maeder-- | constructing the parse tree from (the final) parser state(s)
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaedertoAppl :: GetRange f => Id -> [TERM f] -> Range -> TERM f
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian MaedertoAppl ide ar ps =
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder if ide == singleArgId || ide == multiArgsId
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder then case ar of
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder har : tar -> case har of
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder Application q [] p ->
4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian Maeder Application q tar $ appRange ps p
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder Mixfix_qual_pred _ ->
4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian Maeder Mixfix_term [har, Mixfix_parenthesized tar ps]
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> error "stateToAppl"
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder _ -> error "stateToAppl2"
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder else asAppl ide ar ps
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederaddType :: TERM f -> TERM f -> TERM f
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian 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"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | the type for mixfix resolution
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maedertype MixResolve f = GlobalAnnos -> (Token -> [Rule], Rules) -> f -> Result f
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaederiterateCharts :: (GetRange f, Pretty f) => (f -> f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder -> MixResolve f -> GlobalAnnos -> [TERM f]
4693c24801d551cade06e8ff7b4b9f3a8abe12b4Christian Maeder -> Chart (TERM f) -> Chart (TERM f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederiterateCharts par extR g terms c =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let self = iterateCharts par extR g
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder expand = expandPos Mixfix_token
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder oneStep = nextChart addType toAppl g c
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder ruleS = rules c
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder adder = addRules c
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder resolveTerm = resolveMixTrm par extR g (adder, ruleS)
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
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_bracketed ts ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder self (expand ("[", "]") ts ps ++ tail terms) c
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_braced ts ps ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder self (expand ("{", "}") ts ps ++ tail terms) c
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_parenthesized ts ps ->
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder [h] -> let Result mds v = resolveTerm h
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder tNew = case v of
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder c2 = self (tail terms)
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder (oneStep (tNew, varTok {tokPos = ps}))
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder in mixDiags mds c2
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder _ -> self (expand ("(", ")") ts ps ++ tail terms) c
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder h@(Conditional t1 f2 t3 ps) ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder let Result mds v =
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do t4 <- resolveTerm t1
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder f5 <- resolveMixFrm par extR g (adder, ruleS) f2
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t6 <- resolveTerm t3
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return (Conditional t4 f5 t6 ps)
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder tNew = case v of
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder c2 = self (tail terms)
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder (oneStep (tNew, varTok {tokPos = ps}))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in mixDiags mds c2
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder Mixfix_token t -> let
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder (ds1, trm) = convertMixfixToken (literal_annos g) asAppl
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder Mixfix_token t
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder c2 = self (tail terms) $ oneStep $ case trm of
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder Mixfix_token tok -> (trm, tok)
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder _ -> (trm, varTok {tokPos = tokPos t})
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder in mixDiags ds1 c2
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t@(Mixfix_sorted_term _ ps) -> self (tail terms)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (oneStep (t, typeTok {tokPos = ps}))
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t@(Mixfix_cast _ ps) -> self (tail terms)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (oneStep (t, typeTok {tokPos = ps}))
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t@(Qual_var _ _ ps) -> self (tail terms)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder (oneStep (t, varTok {tokPos = ps}))
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t@(Application (Qual_op_name _ _ ps) _ _) ->
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Sorted_term t s ps ->
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder let Result mds v = resolveTerm t
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder tNew = Sorted_term (case v of
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder Just x -> x) s ps
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder c2 = self (tail terms)
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder (oneStep (tNew, varTok {tokPos = ps}))
26d3a8da6b4244d65614b5585927df4948e542a0Christian Maeder in mixDiags mds c2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> error "iterateCharts"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | construct 'IdSets' from op and pred identifiers
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaedermkIdSets :: Set.Set Id -> Set.Set Id -> IdSets
a3000204685374be86c84d76323d95d86e4735acChristian MaedermkIdSets ops preds = (ops, preds)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | top-level resolution like 'resolveMixTrm' that fails in case of diags
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaederresolveMixfix :: (GetRange f, Pretty f) => (f -> f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder -> MixResolve f -> MixResolve (TERM f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederresolveMixfix par extR g ruleS t =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let r@(Result ds _) = resolveMixTrm par extR g ruleS t
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in if null ds then r else Result ds Nothing
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | basic term resolution that supports recursion without failure
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaederresolveMixTrm :: (GetRange f, Pretty f) => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> MixResolve (TERM f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederresolveMixTrm par extR ga (adder, ruleS) trm =
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder getResolved (showTerm par ga) (getRangeSpan trm) toAppl
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder $ iterateCharts par extR ga [trm] $ initChart adder ruleS
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedershowTerm :: Pretty f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedershowTerm par ga = showGlobalDoc ga . mapTerm par
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | top-level resolution like 'resolveMixFrm' that fails in case of diags
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaederresolveFormula :: (GetRange f, Pretty f) => (f -> f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder -> MixResolve f -> MixResolve (FORMULA f)
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederresolveFormula par extR g ruleS f =
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder let r@(Result ds _) = resolveMixFrm par extR g ruleS f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in if null ds then r else Result ds Nothing
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | basic formula resolution that supports recursion without failure
ca0d4947f7b0fdcbf7eac627659e6cff6d3863baChristian MaederresolveMixFrm :: (GetRange f, Pretty f) => (f -> f)
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder -> MixResolve f -> MixResolve (FORMULA f)
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian MaederresolveMixFrm par extR g ids frm =
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder let self = resolveMixFrm par extR g ids
0af0cffad0fea46df86ff9a9b1d490247871719aChristian Maeder resolveTerm = resolveMixTrm par extR g ids in
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Quantification q vs fOld ps ->
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian Maeder do fNew <- resolveMixFrm par extR g ids fOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Quantification q vs fNew ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Conjunction fsOld ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do fsNew <- mapM self fsOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Conjunction fsNew ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Disjunction fsOld ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do fsNew <- mapM self fsOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Disjunction fsNew ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Implication f1 f2 b ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do f3 <- self f1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f4 <- self f2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Implication f3 f4 b ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Equivalence f1 f2 ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do f3 <- self f1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f4 <- self f2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Equivalence f3 f4 ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Negation fOld ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do fNew <- self fOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Negation fNew ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Predication sym tsOld ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do tsNew <- mapM resolveTerm tsOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Predication sym tsNew ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Definedness tOld ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do tNew <- resolveTerm tOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Definedness tNew ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Existl_equation t1 t2 ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do t3 <- resolveTerm t1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t4 <- resolveTerm t2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Existl_equation t3 t4 ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Strong_equation t1 t2 ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do t3 <- resolveTerm t1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t4 <- resolveTerm t2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Strong_equation t3 t4 ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Membership tOld s ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do tNew <- resolveTerm tOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Membership tNew s ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_formula tOld ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do tNew <- resolveTerm tOld
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Application (Op_name ide) args ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder return $ Predication (Pred_name ide) args ps
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_qual_pred qide ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder return $ Predication qide [] nullRange
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_term [Mixfix_qual_pred qide,
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder Mixfix_parenthesized ts ps] ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder return $ Predication qide ts ps
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder _ -> fatal_error
7d13f393d82fc9e02d741927fad70d6be96081e2Christian Maeder ("not a formula: " ++ showTerm par g tNew "")
74085f08cdbbfd79fe5f9c6a455ed0b0cadcf145Christian Maeder (getRangeSpan tNew)
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder ExtFORMULA f ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do newF <- extR g ids f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ ExtFORMULA newF
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f