94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht{- |

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtModule : ./CASL/MixfixParser.hs

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtDescription : Mixfix analysis of terms

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtCopyright : Christian Maeder and Uni Bremen 2002-2006

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtLicense : GPLv2 or higher, see LICENSE.txt

da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtMaintainer : Christian.Maeder@dfki.de

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtStability : experimental

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtPortability : portable

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon UlbrichtMixfix analysis of terms

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht-}

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtmodule CASL.MixfixParser

4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht ( resolveFormula, resolveMixfix, MixResolve

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht , resolveMixTrm, resolveMixFrm

c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , extendRules, varDeclTokens

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht , extendMixResolve

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht , IdSets, mkIdSets, emptyIdSets, unite, unite2

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht , makeRules, Mix (..), emptyMix, extendMix

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM

4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbricht , ids_DATATYPE_DECL

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht , addIdToRules

846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maeder ) where

ce07f3639c04fc3457da387c0dfd9ec01dbf05c4Christian Maeder

4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbrichtimport CASL.AS_Basic_CASL

8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbrichtimport CASL.ShowMixfix

79eb29c05606f195fe9c6fdca02bcaa458dde17dSimon Ulbrichtimport CASL.ToDoc

e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbrichtimport Common.AS_Annotation

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtimport Common.ConvertMixfixToken

4d1df661384f74cd15d2ceba8a9a3c4760e9ddfbSimon Ulbrichtimport Common.DocUtils

0223b75560eead55b7bbf11d18117a6819540983Christian Maederimport Common.Earley

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbrichtimport Common.GlobalAnnotations

1a088ae6e5ab1e717d720da7b517233286665073Christian Maederimport Common.Id

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbrichtimport Common.Result

e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht

4bf72807172000becf65e11bd225efc1dfd99713Simon Ulbrichtimport qualified Data.Map as Map

846ef0914b29a4806ca0444c116fd3cf267c4fb7Christian Maederimport qualified Data.Set as Set

e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht

e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtimport Data.Maybe

1a088ae6e5ab1e717d720da7b517233286665073Christian Maeder

e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbrichtdata Mix b s f e = MixRecord

94968509d2764786208bd34b59a93c7cbe3aa6dbSimon Ulbricht { getBaseIds :: b -> IdSets -- ^ ids of extra basic items

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht , getSigIds :: s -> IdSets -- ^ ids of extra sig items

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht , getExtIds :: e -> IdSets -- ^ ids of signature extensions

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht , mixRules :: (TokRules, Rules) -- ^ rules for Earley

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht , putParen :: f -> f -- ^ parenthesize extended formula

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht , mixResolve :: MixResolve f -- ^ resolve extended formula

59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon Ulbricht }

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht-- | an initially empty record

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon UlbrichtemptyMix :: Mix b s f e

fe6a19b07759bc4190e88dda76a211d86bf32062Simon UlbrichtemptyMix = MixRecord

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht { getBaseIds = const emptyIdSets

59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon Ulbricht , getSigIds = const emptyIdSets

59fa2ed5a4936e7e56f7164d8a274df68dd4160cSimon Ulbricht , getExtIds = const emptyIdSets

e90b8ee3fac5c932d83af2061579c6b57d528885Christian Maeder , mixRules = (const Set.empty, emptyRules)

ce07f3639c04fc3457da387c0dfd9ec01dbf05c4Christian Maeder , putParen = id

ce07f3639c04fc3457da387c0dfd9ec01dbf05c4Christian Maeder , mixResolve = const $ const return

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht }

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon UlbrichtextendMix :: Set.Set Token -> Mix b s f e -> Mix b s f e

5d75e163c4134d97bba0ced346c3095d7150685cSimon UlbrichtextendMix ts r = r

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht { mixRules = extendRules ts $ mixRules r

036b2c3b35fbb0ad74a7490d6d23de606e88a841Simon Ulbricht , mixResolve = extendMixResolve ts $ mixResolve r }

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht-- precompute non-simple op and pred identifier for mixfix rules

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht-- | the precomputed sets of constant, op, and pred identifiers

8600e22385bce13c5d1048f7b955f9394a5d94d6Simon Ulbrichttype IdSets = ((Set.Set Id, Set.Set Id), Set.Set Id) -- ops are first component

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht-- | the empty 'IdSets'

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon UlbrichtemptyIdSets :: IdSets

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtemptyIdSets = let e = Set.empty in ((e, e), e)

9b59de1ee08232aa26d9d21d3bf99f8d1f68c45dChristian Maeder

0223b75560eead55b7bbf11d18117a6819540983Christian Maederunite2 :: [(Set.Set Id, Set.Set Id)] -> (Set.Set Id, Set.Set Id)

0223b75560eead55b7bbf11d18117a6819540983Christian Maederunite2 l = (Set.unions $ map fst l, Set.unions $ map snd l)

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbricht-- | union 'IdSets'

9b59de1ee08232aa26d9d21d3bf99f8d1f68c45dChristian Maederunite :: [IdSets] -> IdSets

857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maederunite l = (unite2 $ map fst l, Set.unions $ map snd l)

3413b54d5439b4a66d6423cc134e1b9abb5bbe2fChristian Maeder

9b59de1ee08232aa26d9d21d3bf99f8d1f68c45dChristian Maeder-- | get all ids of a basic spec

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbrichtids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets

a9ad67574dd71144680f8dedc285f6c4498a79f8Christian Maederids_BASIC_SPEC f g (Basic_spec al) =

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

a9ad67574dd71144680f8dedc285f6c4498a79f8Christian Maeder

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon Ulbrichtids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -> BASIC_ITEMS b s f -> IdSets

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbrichtids_BASIC_ITEMS f g bi = case bi of

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Sig_items sis -> ids_SIG_ITEMS g sis

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Free_datatype _ al _ -> ids_anDATATYPE_DECLs al

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al

2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbricht Ext_BASIC_ITEMS b -> f b

627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht _ -> emptyIdSets

5d75e163c4134d97bba0ced346c3095d7150685cSimon Ulbricht

5d75e163c4134d97bba0ced346c3095d7150685cSimon Ulbrichtids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbrichtids_anDATATYPE_DECLs al =

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht (unite2 $ map (ids_DATATYPE_DECL . item) al, Set.empty)

fcc4b0f2dadf063ebb8022737cb6e40fb9c4baa8Simon Ulbricht

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht-- | get all ids of a sig items

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbrichtids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbrichtids_SIG_ITEMS f si = let e = Set.empty in case si of

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht Sort_items {} -> emptyIdSets

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht Op_items al _ -> (unite2 $ map (ids_OP_ITEM . item) al, e)

a2cf22f16e226fcc85aa0801f001923ab2db49ddSimon Ulbricht Pred_items al _ -> ((e, e), Set.unions $ map (ids_PRED_ITEM . item) al)

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder Datatype_items _ al _ -> ids_anDATATYPE_DECLs al

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder Ext_SIG_ITEMS s -> f s

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder-- | get all op ids of an op item

0223b75560eead55b7bbf11d18117a6819540983Christian Maederids_OP_ITEM :: OP_ITEM f -> (Set.Set Id, Set.Set Id)

0223b75560eead55b7bbf11d18117a6819540983Christian Maederids_OP_ITEM o = let e = Set.empty in case o of

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder Op_decl ops (Op_type _ args _ _) _ _ ->

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder let s = Set.fromList ops in

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder if null args then (s, e) else (e, s)

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder Op_defn i (Op_head _ args _ _) _ _ ->

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder let s = Set.singleton i in

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder if null args then (s, e) else (e, s)

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht

08913787eb7dc05172d505d02b11545ffc7e1256Simon Ulbricht-- | get all pred ids of a pred item

fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id

fe6a19b07759bc4190e88dda76a211d86bf32062Simon Ulbrichtids_PRED_ITEM p = case p of

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Pred_decl preds _ _ -> Set.unions $ map Set.singleton preds

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht Pred_defn i _ _ _ -> Set.singleton i

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbrichtids_DATATYPE_DECL :: DATATYPE_DECL -> (Set.Set Id, Set.Set Id)

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbrichtids_DATATYPE_DECL (Datatype_decl _ al _) =

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht unite2 $ map (ids_ALTERNATIVE . item) al

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbrichtids_ALTERNATIVE :: ALTERNATIVE -> (Set.Set Id, Set.Set Id)

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbrichtids_ALTERNATIVE a = let e = Set.empty in case a of

e4d1479434761dc3eb8d17b6c75de4eb24866f0bSimon Ulbricht Alt_construct _ i cs _ -> let s = Set.singleton i in

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht if null cs then (s, e) else (e, Set.unions $ s : map ids_COMPONENTS cs)

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht Subsorts _ _ -> (e, e)

2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbricht

2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbrichtids_COMPONENTS :: COMPONENTS -> Set.Set Id

2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbrichtids_COMPONENTS c = case c of

2fa75b8879de8c878475f16ab43161e0580f5430Simon Ulbricht Cons_select _ l _ _ -> Set.unions $ map Set.singleton l

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht Sort _ -> Set.empty

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht-- predicates get lower precedence

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon UlbrichtmkRule :: Id -> Rule

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon UlbrichtmkRule = mixRule 1

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon Ulbricht

0e62ba92d48fb6b8251a0707d0c7e8358ac00a02Simon UlbrichtmkSingleArgRule :: Int -> Id -> Rule

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtmkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht

9575d8e9e9211ccd22dbc9b86fa3e8941ee1d021Simon UlbrichtmkArgsRule :: Int -> Id -> Rule

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtmkArgsRule b ide =

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (protect ide, b, getPlainTokenList ide ++ getTokenPlaceList tupleId)

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder

9575d8e9e9211ccd22dbc9b86fa3e8941ee1d021Simon UlbrichtsingleArgId :: Id

08913787eb7dc05172d505d02b11545ffc7e1256Simon UlbrichtsingleArgId = mkId [exprTok, varTok]

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder

0223b75560eead55b7bbf11d18117a6819540983Christian MaedermultiArgsId :: Id

0223b75560eead55b7bbf11d18117a6819540983Christian MaedermultiArgsId = mkId (exprTok : getPlainTokenList tupleId)

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder

0223b75560eead55b7bbf11d18117a6819540983Christian MaederaddIdToRules :: Id -> (TokRules, Rules) -> (TokRules, Rules)

0223b75560eead55b7bbf11d18117a6819540983Christian MaederaddIdToRules i (tr, rs) =

0223b75560eead55b7bbf11d18117a6819540983Christian Maeder (tr, let newSc = Set.union

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht (Set.fromList [mkSingleArgRule 1 i, mkArgsRule 1 i])

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht $ scanRules rs

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht in if begPlace i then

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht rs { postRules = Set.insert (mixRule 1 i) $ postRules rs

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht , scanRules = newSc }

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht else rs { scanRules = Set.insert (mixRule 1 i) newSc })

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht-- | additional scan rules

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtaddRule :: GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules

776dc405f11bb5a86787cd05c1e539203e88759bSimon UlbrichtaddRule ga uRules hasInvisible ((consts, ops), preds) tok =

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht let addP = Set.fold (\ i -> case i of

c044cefcba5a9db7f8948b3778266971742b3dc6Simon Ulbricht Id (t : _) _ _ -> Map.insertWith (++) t

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht [ mixRule (if Set.member i consts then 1 else 0) i

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht , mkSingleArgRule 0 i, mkArgsRule 0 i]

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht _ -> error "addRule.addP")

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht addO = Set.fold (\ i -> case i of

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht Id (t : _) _ _ -> Map.insertWith (++) t

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht $ [mkRule i | not (isSimpleId i)

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht || Set.member i (Set.union consts preds) ]

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht ++ [mkSingleArgRule 1 i, mkArgsRule 1 i]

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht _ -> error "addRule.addO")

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht addC = Set.fold (\ i -> case i of

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Id (t : _) _ _ -> Map.insertWith (++) t [mkRule i]

f665662391cc4b8fdc03e8bd082936cfedbce1a2Simon Ulbricht _ -> error "addRule.addC")

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht lm = foldr (\ r -> case r of

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht (_, _, t : _) -> Map.insertWith (++) t [r]

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht _ -> error "addRule.lm") Map.empty $ listRules 1 ga

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht (spreds, rpreds) = Set.partition isSimpleId preds

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht {- do not add simple ids as preds as these may be variables

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht with higher precedence -}

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht ops2 = Set.union ops spreds

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht sops = Set.union consts ops2

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht rConsts = Set.difference consts $ Set.union ops preds

a9ad67574dd71144680f8dedc285f6c4498a79f8Christian Maeder varR = mkRule varId

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht m = Map.insert placeTok uRules

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht $ Map.insert varTok [varR]

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht $ Map.insert exprTok

776dc405f11bb5a86787cd05c1e539203e88759bSimon Ulbricht [varR, mkRule singleArgId, mkRule multiArgsId]

08913787eb7dc05172d505d02b11545ffc7e1256Simon Ulbricht $ addP (addC (addO lm ops2) rConsts) $ Set.difference rpreds ops

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht tId = mkId [tok]

7dc84ca1f3a253bcf947bd870f0303fffd37d3afSimon Ulbricht tPId = mkId [tok, placeTok] -- prefix identifier

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

627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht then if hasInvisible then Set.empty else

627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht Set.insert (mkRule tId)

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht -- add rule for unknown constant or variable

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht $ if Set.member tPId ops || Set.member tPId rpreds

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht then Set.empty else

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht Set.fromList [mkSingleArgRule 1 tId, mkArgsRule 1 tId]

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht -- add also rules for undeclared op

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht else Set.empty) `Set.union` Set.fromList (Map.findWithDefault [] tok m)

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht-- insert only identifiers starting with a place

19988126590a72905215aef1d7a67c646d99bdadSimon UlbrichtinitRules :: (Set.Set Id, Set.Set Id) -> Rules

8221f726d2e0ca6f0df32ef8f88063b7a85b1cfeSimon UlbrichtinitRules (opS, predS) =

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht let addR p = Set.fold (Set.insert . mixRule p)

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht in emptyRules

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht { postRules = addR 1 (addR 0 (Set.singleton $ mkRule typeId) predS) opS }

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht

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

5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian MaedermakeRules :: GlobalAnnos -> IdSets -> (TokRules, Rules)

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtmakeRules ga ((constS, opS), predS) = let

5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder (cOps, sOps) = Set.partition begPlace opS

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

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

19988126590a72905215aef1d7a67c646d99bdadSimon Ulbricht mkSingleArgRule p i : mkArgsRule p i : l)

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht uRules = addR 0 (addR 1 [] cOps) cPreds

01bf5a978a5dd7aecf7dea0ee2e1046922c64fd2Simon Ulbricht in (addRule ga uRules (Set.member applId $ Set.union cOps cPreds)

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht ((constS, sOps), sPreds), initRules (cOps, cPreds))

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht

95f75d053c19b9be988c73b7c866d9db57825efeSimon Ulbricht-- | construct application

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtasAppl :: Id -> [TERM f] -> Range -> TERM f

454e349ad409df6c5fa9ba2b485243b8222dec41Simon UlbrichtasAppl f args ps = Application (Op_name f) args

d3d09eed06d615a26a9c930966f29cf2c149b876Simon Ulbricht $ if isNullRange ps then posOfId f else ps

d3d09eed06d615a26a9c930966f29cf2c149b876Simon Ulbricht

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

454e349ad409df6c5fa9ba2b485243b8222dec41Simon UlbrichttoAppl :: GetRange f => Id -> [TERM f] -> Range -> TERM f

1a088ae6e5ab1e717d720da7b517233286665073Christian MaedertoAppl ide ar ps =

1a088ae6e5ab1e717d720da7b517233286665073Christian Maeder if elem ide [singleArgId, multiArgsId]

1a088ae6e5ab1e717d720da7b517233286665073Christian Maeder then case ar of

454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht har : tar -> case har of

454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht Application q [] p ->

454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht Application q tar $ appRange ps p

454e349ad409df6c5fa9ba2b485243b8222dec41Simon Ulbricht Mixfix_qual_pred _ ->

01bf5a978a5dd7aecf7dea0ee2e1046922c64fd2Simon Ulbricht Mixfix_term [har, Mixfix_parenthesized tar ps]

857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder _ -> error "stateToAppl"

857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder _ -> error "stateToAppl2"

857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian Maeder else asAppl ide ar ps

627e304eb081ce411768e08d3554d8efd52d4187Simon Ulbricht

627e304eb081ce411768e08d3554d8efd52d4187Simon UlbrichtaddType :: TERM f -> TERM f -> TERM f

857ab542e0b0bdf90e5a484ffe8df5a9c9c3e38fChristian MaederaddType tt t =

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht case tt of

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Mixfix_sorted_term s ps -> Sorted_term t s ps

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht Mixfix_cast s ps -> Cast t s ps

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht _ -> error "addType"

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht-- | the type for mixfix resolution

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbrichttype MixResolve f = GlobalAnnos -> (TokRules, Rules) -> f -> Result f

9deba6a2981f6b73fc57f27d525cabbb4f8bf484Simon Ulbricht

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon UlbrichtiterateCharts :: FormExtension f => (f -> f)

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -> MixResolve f -> GlobalAnnos -> [TERM f]

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht -> Chart (TERM f) -> Chart (TERM f)

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon UlbrichtiterateCharts par extR g terms c =

042cf1b6c164c2b06bccafc8db6bf44134f3f0b8Simon Ulbricht let self = iterateCharts par extR g

9deba6a2981f6b73fc57f27d525cabbb4f8bf484Simon Ulbricht expand = expandPos Mixfix_token

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht oneStep = nextChart addType toAppl g c

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht ids = (addRules c, rules c)

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht resolveTerm = resolveMixTrm par extR g ids

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht in case terms of

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht [] -> c

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht hd : tl -> case hd of

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Mixfix_term ts -> self (ts ++ tl) c

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Mixfix_bracketed ts ps ->

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht self (expand ("[", "]") ts ps ++ tl) c

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Mixfix_braced ts ps ->

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht self (expand ("{", "}") ts ps ++ tl) c

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Mixfix_parenthesized ts ps -> case ts of

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht [h] -> let

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Result mds v = resolveTerm h

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht c2 = self tl (oneStep (fromMaybe h v, varTok {tokPos = ps}))

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht in mixDiags mds c2

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht _ -> self (expand ("(", ")") ts ps ++ tl) c

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht h@(Conditional t1 f2 t3 ps) -> let

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht Result mds v = do

5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder t4 <- resolveTerm t1

5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder f5 <- resolveMixFrm par extR g ids f2

5f662be3a5a327b763dbc53e28836a04cfc3bd3aChristian Maeder t6 <- resolveTerm t3

bcce4250f8aa524ddc0af7021a238e9fc2b8034aSimon Ulbricht return (Conditional t4 f5 t6 ps)

c2 = self tl

(oneStep (fromMaybe h v, varTok {tokPos = ps}))

in mixDiags mds c2

Mixfix_token t -> let

(ds1, trm) = convertMixfixToken (literal_annos g) asAppl

Mixfix_token t

c2 = self tl $ oneStep $ case trm of

Mixfix_token tok -> (trm, tok)

_ -> (trm, varTok {tokPos = tokPos t})

in mixDiags ds1 c2

t@(Mixfix_sorted_term _ ps) ->

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

t@(Mixfix_cast _ ps) ->

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

t@(Qual_var _ _ ps) ->

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

Application opNam ts ps -> let

Result mds v = mapM resolveTerm ts

c2 = self tl $ oneStep (Application opNam (fromMaybe ts v) ps

, case opNam of

Qual_op_name _ _ qs -> exprTok {tokPos = qs}

Op_name o -> varTok {tokPos = posOfId o})

in mixDiags mds c2

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

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

Sorted_term t s ps -> let

Result mds v = resolveTerm t

tNew = Sorted_term (fromMaybe t v) s ps

c2 = self tl (oneStep (tNew, varTok {tokPos = ps}))

in mixDiags mds c2

ExtTERM t -> let

Result mds v = extR g ids t

tNew = ExtTERM $ fromMaybe t v

c2 = self tl $ oneStep (tNew, varTok {tokPos = getRange t})

in mixDiags mds c2

_ -> error "iterateCharts"

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

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

mkIdSets consts ops preds = ((consts, ops), preds)

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

resolveMixfix :: FormExtension 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 :: FormExtension f => (f -> f)

-> MixResolve f -> MixResolve (TERM f)

resolveMixTrm par extR ga (adder, ruleS) trm =

getResolved (showTerm par ga) (getRangeSpan trm) toAppl

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

showTerm :: FormExtension 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 :: FormExtension 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

varDeclTokens :: [VAR_DECL] -> Set.Set Token

varDeclTokens = Set.unions . map (\ (Var_decl vs _ _) -> Set.fromList vs)

extendRules :: Set.Set Token -> (TokRules, Rules)

-> (TokRules, Rules)

extendRules ts (f, rs) =

(\ t -> let

l = f t

r = mkRule $ mkId [t]

in if Set.member t ts then Set.insert r l else l, rs)

extendMixResolve :: Set.Set Token -> MixResolve f -> MixResolve f

extendMixResolve ts f ga = f ga . extendRules ts

-- | basic formula resolution that supports recursion without failure

resolveMixFrm :: FormExtension 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 let ts = varDeclTokens vs

fNew <- resolveMixFrm par (extendMixResolve ts extR)

g (extendRules ts ids) fOld

return $ Quantification q vs fNew ps

Junction j fsOld ps ->

do fsNew <- mapM self fsOld

return $ Junction j fsNew ps

Relation f1 c f2 ps ->

do f3 <- self f1

f4 <- self f2

return $ Relation f3 c 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

Equation t1 e t2 ps ->

do t3 <- resolveTerm t1

t4 <- resolveTerm t2

return $ Equation t3 e 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

_ -> return $ Mixfix_formula tNew

QuantOp o t fOld -> let

ts = if isSimpleId o then Set.singleton $ idToSimpleId o

else Set.empty

in fmap (QuantOp o t)

$ resolveMixFrm par (extendMixResolve ts extR)

g (extendRules ts ids) fOld

QuantPred p t fOld -> let

ts = if isSimpleId p then Set.singleton $ idToSimpleId p

else Set.empty

in fmap (QuantPred p t)

$ resolveMixFrm par (extendMixResolve ts extR)

g (extendRules ts ids) fOld

ExtFORMULA f ->

do newF <- extR g ids f

return $ ExtFORMULA newF

f -> return f