e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Mixfix analysis of terms
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian MaederCopyright : Christian Maeder and Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.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
3b31ee94edcb328d2aa02ddcfa8a2e227d4c98edChristian Maeder , extendRules, varDeclTokens
3b5d1e9f95905d6595b3bb01b54499a37a3d82acChristian Maeder , extendMixResolve
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , IdSets, mkIdSets, emptyIdSets, unite, unite2
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , makeRules, Mix (..), emptyMix, extendMix
75eb4b8bca5dc18a680471287ebe996d908ae5ccChristian Maeder , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM
75eb4b8bca5dc18a680471287ebe996d908ae5ccChristian Maeder , ids_DATATYPE_DECL
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , addIdToRules
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Data.Set as Set
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
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder , mixRules :: (TokRules, 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
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder , mixRules = (const Set.empty, emptyRules)
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , putParen = id
782d5365e084a40e4f717dafbe00fc41476a7cfeChristian Maeder , mixResolve = const $ const return
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederextendMix :: Set.Set Token -> Mix b s f e -> Mix b s f e
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederextendMix ts r = r
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder { mixRules = extendRules ts $ mixRules r
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , mixResolve = extendMixResolve ts $ mixResolve r }
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- precompute non-simple op and pred identifier for mixfix rules
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder-- | the precomputed sets of constant, op, and pred identifiers
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maedertype IdSets = ((Set.Set Id, Set.Set Id), Set.Set Id) -- ops are first component
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | the empty 'IdSets'
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian MaederemptyIdSets :: IdSets
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederemptyIdSets = let e = Set.empty in ((e, e), e)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederunite2 :: [(Set.Set Id, Set.Set Id)] -> (Set.Set Id, Set.Set Id)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederunite2 l = (Set.unions $ map fst l, Set.unions $ map snd l)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | union 'IdSets'
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maederunite :: [IdSets] -> IdSets
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederunite l = (unite2 $ 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 =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder (unite2 $ 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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_SIG_ITEMS f si = let e = Set.empty in case si of
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder Sort_items {} -> emptyIdSets
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Op_items al _ -> (unite2 $ map (ids_OP_ITEM . item) al, e)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Pred_items al _ -> ((e, e), 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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_OP_ITEM :: OP_ITEM f -> (Set.Set Id, Set.Set Id)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_OP_ITEM o = let e = Set.empty in case o of
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Op_decl ops (Op_type _ args _ _) _ _ ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder if null args then (s, e) else (e, s)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Op_defn i (Op_head _ args _ _) _ _ ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder if null args then (s, e) else (e, s)
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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_DATATYPE_DECL :: DATATYPE_DECL -> (Set.Set Id, Set.Set Id)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maederids_DATATYPE_DECL (Datatype_decl _ al _) =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder unite2 $ map (ids_ALTERNATIVE . item) al
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_ALTERNATIVE :: ALTERNATIVE -> (Set.Set Id, Set.Set Id)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederids_ALTERNATIVE a = let e = Set.empty in case a of
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Alt_construct _ i cs _ -> let s = Set.singleton i in
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder if null cs then (s, e) else (e, Set.unions $ s : map ids_COMPONENTS cs)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Subsorts _ _ -> (e, e)
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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedermkArgsRule b ide =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder (protect ide, b, getPlainTokenList ide ++ getTokenPlaceList tupleId)
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaedersingleArgId :: Id
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian MaedersingleArgId = mkId [exprTok, varTok]
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaedermultiArgsId :: Id
b1c32a0faa63e0c13687f36a2faae5969ec0a9d5Christian MaedermultiArgsId = mkId (exprTok : getPlainTokenList tupleId)
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian MaederaddIdToRules :: Id -> (TokRules, Rules) -> (TokRules, Rules)
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian MaederaddIdToRules i (tr, rs) =
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder (tr, let newSc = Set.union
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder (Set.fromList [mkSingleArgRule 1 i, mkArgsRule 1 i])
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder $ scanRules rs
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder in if begPlace i then
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder rs { postRules = Set.insert (mixRule 1 i) $ postRules rs
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder , scanRules = newSc }
81ae4270c8508e5e630e50923a2e790e7b1e5997Christian Maeder else rs { scanRules = Set.insert (mixRule 1 i) newSc })
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder-- | additional scan rules
9c07aad044613547d61ab235665c08adcef03a1cChristian MaederaddRule :: GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederaddRule ga uRules hasInvisible ((consts, ops), preds) tok =
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder let addP = Set.fold (\ i -> case i of
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder Id (t : _) _ _ -> Map.insertWith (++) t
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder [ mixRule (if Set.member i consts then 1 else 0) i
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder , mkSingleArgRule 0 i, mkArgsRule 0 i]
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder addO = Set.fold (\ i -> case i of
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder Id (t : _) _ _ -> Map.insertWith (++) t
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder $ [mkRule i | not (isSimpleId i)
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder ++ [mkSingleArgRule 1 i, mkArgsRule 1 i]
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder addC = Set.fold (\ i -> case i of
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder Id (t : _) _ _ -> Map.insertWith (++) t [mkRule i]
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder lm = foldr (\ r -> case r of
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder (_, _, t : _) -> Map.insertWith (++) t [r]
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder _ -> error "addRule.lm") Map.empty $ listRules 1 ga
a3000204685374be86c84d76323d95d86e4735acChristian Maeder (spreds, rpreds) = Set.partition isSimpleId preds
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder {- do not add simple ids as preds as these may be variables
35c791e6c59ef269ec639360dc94943e264d3ad1Christian Maeder with higher precedence -}
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder ops2 = Set.union ops spreds
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder sops = Set.union consts ops2
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder rConsts = Set.difference consts $ Set.union ops preds
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]
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder $ addP (addC (addO lm ops2) rConsts) $ Set.difference rpreds ops
a3000204685374be86c84d76323d95d86e4735acChristian Maeder tId = mkId [tok]
a3000204685374be86c84d76323d95d86e4735acChristian Maeder tPId = mkId [tok, placeTok] -- prefix identifier
a3000204685374be86c84d76323d95d86e4735acChristian Maeder in (if isSimpleToken tok && not (Set.member tId sops)
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder then if hasInvisible then Set.empty else
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder -- add rule for unknown constant or variable
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder $ if Set.member tPId ops || Set.member tPId rpreds
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder Set.fromList [mkSingleArgRule 1 tId, mkArgsRule 1 tId]
a3000204685374be86c84d76323d95d86e4735acChristian Maeder -- add also rules for undeclared op
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder else Set.empty) `Set.union` Set.fromList (Map.findWithDefault [] tok m)
46199904d5e648bc1a25108f60a94078ffb99b30Christian Maeder-- insert only identifiers starting with a place
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederinitRules :: (Set.Set Id, Set.Set Id) -> Rules
46199904d5e648bc1a25108f60a94078ffb99b30Christian MaederinitRules (opS, predS) =
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder let addR p = Set.fold (Set.insert . mixRule p)
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder in emptyRules
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder { postRules = addR 1 (addR 0 (Set.singleton $ mkRule typeId) predS) opS }
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | construct rules from 'IdSets' to be put into a 'Mix' record
9c07aad044613547d61ab235665c08adcef03a1cChristian MaedermakeRules :: GlobalAnnos -> IdSets -> (TokRules, Rules)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedermakeRules ga ((constS, 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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder in (addRule ga uRules (Set.member applId $ Set.union cOps cPreds)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder ((constS, 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 =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder if elem ide [singleArgId, 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
9c07aad044613547d61ab235665c08adcef03a1cChristian Maedertype MixResolve f = GlobalAnnos -> (TokRules, Rules) -> f -> Result f
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederiterateCharts :: FormExtension 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
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder ids = (addRules c, rules c)
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder resolveTerm = resolveMixTrm par extR g ids
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder in case terms of
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder hd : tl -> case hd of
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Mixfix_term ts -> self (ts ++ tl) c
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_bracketed ts ps ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder self (expand ("[", "]") ts ps ++ tl) c
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder Mixfix_braced ts ps ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder self (expand ("{", "}") ts ps ++ tl) c
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Mixfix_parenthesized ts ps -> case ts of
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Result mds v = resolveTerm h
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder c2 = self tl (oneStep (fromMaybe h v, varTok {tokPos = ps}))
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder in mixDiags mds c2
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder _ -> self (expand ("(", ")") ts ps ++ tl) c
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder h@(Conditional t1 f2 t3 ps) -> let
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Result mds v = do
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder t4 <- resolveTerm t1
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder f5 <- resolveMixFrm par extR g ids f2
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder t6 <- resolveTerm t3
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder return (Conditional t4 f5 t6 ps)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder (oneStep (fromMaybe h v, varTok {tokPos = ps}))
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian 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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder c2 = self tl $ oneStep $ case trm of
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder Mixfix_token tok -> (trm, tok)
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder _ -> (trm, varTok {tokPos = tokPos t})
d645eac2b9bf2e1a458b25982051276232670f09Christian Maeder in mixDiags ds1 c2
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder t@(Mixfix_sorted_term _ ps) ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder self tl (oneStep (t, typeTok {tokPos = ps}))
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder t@(Mixfix_cast _ ps) ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder self tl (oneStep (t, typeTok {tokPos = ps}))
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder t@(Qual_var _ _ ps) ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder self tl (oneStep (t, varTok {tokPos = ps}))
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder Application opNam ts ps -> let
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder Result mds v = mapM resolveTerm ts
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder c2 = self tl $ oneStep (Application opNam (fromMaybe ts v) ps
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder , case opNam of
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder Qual_op_name _ _ qs -> exprTok {tokPos = qs}
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder Op_name o -> varTok {tokPos = posOfId o})
545400dabab49e2009c7029a98c42d4dbaff111eChristian Maeder in mixDiags mds c2
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder self tl (oneStep (t, exprTok {tokPos = ps} ))
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Sorted_term t s ps -> let
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Result mds v = resolveTerm t
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder tNew = Sorted_term (fromMaybe t v) s ps
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder c2 = self tl (oneStep (tNew, varTok {tokPos = ps}))
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder in mixDiags mds c2
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder ExtTERM t -> let
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder Result mds v = extR g ids t
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder tNew = ExtTERM $ fromMaybe t v
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder c2 = self tl $ oneStep (tNew, varTok {tokPos = getRange t})
87ce48cde10c6835b292e39b43331a5ed94e9b6eChristian Maeder in mixDiags mds c2
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder _ -> error "iterateCharts"
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | construct 'IdSets' from op and pred identifiers
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedermkIdSets :: Set.Set Id -> Set.Set Id -> Set.Set Id -> IdSets
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedermkIdSets consts ops preds = ((consts, ops), preds)
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | top-level resolution like 'resolveMixTrm' that fails in case of diags
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederresolveMixfix :: FormExtension 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
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederresolveMixTrm :: FormExtension 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
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaedershowTerm :: FormExtension 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
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederresolveFormula :: FormExtension 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
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedervarDeclTokens :: [VAR_DECL] -> Set.Set Token
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaedervarDeclTokens = Set.unions . map (\ (Var_decl vs _ _) -> Set.fromList vs)
9c07aad044613547d61ab235665c08adcef03a1cChristian MaederextendRules :: Set.Set Token -> (TokRules, Rules)
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder -> (TokRules, Rules)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederextendRules ts (f, rs) =
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder r = mkRule $ mkId [t]
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder in if Set.member t ts then Set.insert r l else l, rs)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederextendMixResolve :: Set.Set Token -> MixResolve f -> MixResolve f
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederextendMixResolve ts f ga = f ga . extendRules ts
e849958012c0bd2bfa751f6ec264b3ecb680c00aChristian Maeder-- | basic formula resolution that supports recursion without failure
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederresolveMixFrm :: FormExtension 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 ->
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder do let ts = varDeclTokens vs
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder fNew <- resolveMixFrm par (extendMixResolve ts extR)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder g (extendRules ts ids) fOld
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ Quantification q vs fNew ps
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Junction j fsOld ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do fsNew <- mapM self fsOld
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder return $ Junction j fsNew ps
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation f1 c f2 ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do f3 <- self f1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder f4 <- self f2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder return $ Relation f3 c 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
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Equation t1 e t2 ps ->
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder do t3 <- resolveTerm t1
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder t4 <- resolveTerm t2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder return $ Equation t3 e 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
c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder _ -> return $ Mixfix_formula tNew
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder QuantOp o t fOld -> let
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder ts = if isSimpleId o then Set.singleton $ idToSimpleId o
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder in fmap (QuantOp o t)
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder $ resolveMixFrm par (extendMixResolve ts extR)
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder g (extendRules ts ids) fOld
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder QuantPred p t fOld -> let
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder ts = if isSimpleId p then Set.singleton $ idToSimpleId p
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder in fmap (QuantPred p t)
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder $ resolveMixFrm par (extendMixResolve ts extR)
bf3bf3fe0342b4253bf3ad19e00ed33e5c695a8dChristian Maeder g (extendRules ts ids) fOld
64c3ee43f3cbacbeffb633103ffe6269f2177485Christian Maeder ExtFORMULA f ->
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder do newF <- extR g ids f
a255351561838b3743d03c1629d335cfb8b83804Christian Maeder return $ ExtFORMULA newF
190828a6ce12ff8c502e3d7303dcc0d70db49b6cChristian Maeder f -> return f