2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina{- |

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaModule : $Header$

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaDescription : Mixfix analysis of terms

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaCopyright : Christian Maeder and Uni Bremen 2002-2006

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaMaintainer : Christian.Maeder@dfki.de

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaStability : experimental

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaPortability : portable

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaMixfix analysis of terms

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-}

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinamodule CASL.MixfixParser

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ( resolveFormula, resolveMixfix, MixResolve

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , resolveMixTrm, resolveMixFrm

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , IdSets, mkIdSets, emptyIdSets, unite, single

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , makeRules, Mix(..), emptyMix

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina where

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CASL.AS_Basic_CASL

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.GlobalAnnotations

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Result

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Data.Set as Set

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport qualified Data.Map as Map

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Common.Earley

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březinaimport Common.ConvertMixfixToken

d117004902c767d46430848b6ef1c11c3ad82835Pavel Březinaimport Common.DocUtils

2a25713afc6beefb11a799903a43f695c5d7a4f9Adam Tkacimport Common.AS_Annotation

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CASL.ShowMixfix

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport CASL.ToDoc()

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaimport Control.Exception (assert)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinadata Mix b s f e = MixRecord

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina { getBaseIds :: b -> IdSets -- ^ ids of extra basic items

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , getSigIds :: s -> IdSets -- ^ ids of extra sig items

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , getExtIds :: e -> IdSets -- ^ ids of signature extensions

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , mixRules :: (Token -> [Rule], Rules) -- ^ rules for Earley

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce , putParen :: f -> f -- ^ parenthesize extended formula

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , mixResolve :: MixResolve f -- ^ resolve extended formula

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina }

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | an initially empty record

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaemptyMix :: Mix b s f e

4f3a9d837a55b49448eca3c713c85a406207e523Simo SorceemptyMix = MixRecord

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce { getBaseIds = const emptyIdSets

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce , getSigIds = const emptyIdSets

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce , getExtIds = const emptyIdSets

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce , mixRules = error "emptyMix"

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , putParen = id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina , mixResolve = const $ const return

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov }

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- precompute non-simple op and pred identifier for mixfix rules

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | the precomputed sets of op and pred (non-simple) identifiers

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorcetype IdSets = (Set.Set Id, Set.Set Id) -- ops are first component

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | the empty 'IdSets'

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovemptyIdSets :: IdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaemptyIdSets = (Set.empty, Set.empty)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce-- | union 'IdSets'

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaunite :: [IdSets] -> IdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaunite l = (Set.unions $ map fst l, Set.unions $ map snd l)

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | get all ids of a basic spec

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_BASIC_SPEC f g (Basic_spec al) =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina unite $ map (ids_BASIC_ITEMS f g . item) al

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -> BASIC_ITEMS b s f -> IdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_BASIC_ITEMS f g bi = case bi of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Sig_items sis -> ids_SIG_ITEMS g sis

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Free_datatype _ al _ -> ids_anDATATYPE_DECLs al

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Ext_BASIC_ITEMS b -> f b

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina _ -> emptyIdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_anDATATYPE_DECLs al =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (Set.unions $ map (ids_DATATYPE_DECL . item) al, Set.empty)

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov-- | get all ids of a sig items

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březinaids_SIG_ITEMS f si = case si of

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Sort_items _ _ _ -> emptyIdSets

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Op_items al _ -> (Set.unions $ map (ids_OP_ITEM . item) al, Set.empty)

7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina Pred_items al _ -> (Set.empty, Set.unions $ map (ids_PRED_ITEM . item) al)

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Datatype_items _ al _ -> ids_anDATATYPE_DECLs al

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Ext_SIG_ITEMS s -> f s

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | get all op ids of an op item

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_OP_ITEM :: OP_ITEM f -> Set.Set Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_OP_ITEM o = case o of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Op_decl ops _ _ _ -> Set.unions $ map single ops

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Op_defn i _ _ _ -> single i

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | same as singleton

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinasingle :: Id -> Set.Set Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinasingle i = Set.singleton i

5ff1c3c5a12930692cb6284d14f7fda3a974af8ePavel Březina

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina-- | get all pred ids of a pred item

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březinaids_PRED_ITEM p = case p of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Pred_decl preds _ _ -> Set.unions $ map single preds

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina Pred_defn i _ _ _ -> single i

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březinaids_DATATYPE_DECL :: DATATYPE_DECL -> Set.Set Id

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březinaids_DATATYPE_DECL (Datatype_decl _ al _) =

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina Set.unions $ map (ids_ALTERNATIVE . item) al

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovids_ALTERNATIVE :: ALTERNATIVE -> Set.Set Id

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashovids_ALTERNATIVE a = case a of

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina Alt_construct _ i cs _ -> Set.unions $ single i : map ids_COMPONENTS cs

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina Subsorts _ _ -> Set.empty

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březinaids_COMPONENTS :: COMPONENTS -> Set.Set Id

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březinaids_COMPONENTS c = case c of

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina Cons_select _ l _ _ -> Set.unions $ map single l

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina Sort _ -> Set.empty

55fdd0d28e7c88f333ad78183b0ba37a1da34160Pavel Březina

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov-- predicates get lower precedence

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovmkRule :: Id -> Rule

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel BřezinamkRule = mixRule 1

c9aab1c04c399ca2d1abef74f6df22ced34983dcPavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamkSingleArgRule :: Int -> Id -> Rule

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel BřezinamkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])

7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina

710472d946f6c337a095699dfd79134fa8b9eab9Pavel BřezinamkArgsRule :: Int -> Id -> Rule

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamkArgsRule b ide = (protect ide, b, getPlainTokenList ide

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ++ getTokenPlaceList tupleId)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinasingleArgId :: Id

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel BřezinasingleArgId = mkId [exprTok, varTok]

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamultiArgsId :: Id

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamultiArgsId = mkId (exprTok : getPlainTokenList tupleId)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | additional scan rules

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaaddRule :: GlobalAnnos -> [Rule] -> IdSets -> Token -> [Rule]

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinaaddRule ga uRules (ops, preds) tok =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina let addR p = Set.fold ( \ i@(Id (t : _) _ _) ->

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Map.insertWith (++) t

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina [mixRule p i, mkSingleArgRule p i, mkArgsRule p i])

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

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Map.empty $ listRules 1 ga

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (spreds, rpreds) = Set.partition isSimpleId preds

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -- do not add simple ids as preds as these may be variables

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -- with higher precedence

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina sops = Set.union ops spreds

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina varR = mkRule varId

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina m = Map.insert placeTok uRules

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina $ Map.insert varTok [varR]

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina $ Map.insert exprTok

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina [varR, mkRule singleArgId, mkRule multiArgsId]

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina $ addR 0 (addR 1 lm sops) rpreds

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina tId = mkId [tok]

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

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina in (if isSimpleToken tok && not (Set.member tId sops)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina then [mkRule tId] -- add rule for new variable

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ++ if Set.member tPId ops || Set.member tPId rpreds then [] else

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina [mkSingleArgRule 1 tId, mkArgsRule 1 tId]

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina -- add also rules for undeclared op

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina else []) ++ Map.findWithDefault [] tok m

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina-- insert only identifiers starting with a place

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel BřezinainitRules :: IdSets -> Rules

76db25eab9010a33657f35e5afc8477c996df7a3Pavel BřezinainitRules (opS, predS) =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina let addR p = Set.fold ( \ i l -> mixRule p i : l)

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina in (addR 1 (addR 0 [mkRule typeId] predS) opS, [])

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | construct rules from 'IdSets' to be put into a 'Mix' record

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamakeRules :: GlobalAnnos -> IdSets -> (Token -> [Rule], Rules)

4f3a9d837a55b49448eca3c713c85a406207e523Simo SorcemakeRules ga (opS, predS) = let

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce (cOps, sOps) = Set.partition begPlace opS

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (cPreds, sPreds) = Set.partition begPlace $ Set.difference predS opS

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina addR p = Set.fold ( \ i l ->

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina mkSingleArgRule p i : mkArgsRule p i : l)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina uRules = addR 0 (addR 1 [] cOps) cPreds

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina in (addRule ga uRules (sOps, sPreds), initRules (cOps, cPreds))

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel Březina

1509d1723d39124f840c214327e698aff3b3f683Pavel Březina-- | meaningful position of a term

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovposOfTerm :: TERM f -> Range

1509d1723d39124f840c214327e698aff3b3f683Pavel BřezinaposOfTerm trm =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina case trm of

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina Qual_var v _ ps -> if isNullRange ps then tokPos v else ps

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Mixfix_term ts -> concatMapRange posOfTerm ts

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Mixfix_qual_pred p -> posOfId $ predSymbName p

41ef946f3f74a46b9e26118116e4811e259b30efPavel Březina Application o _ ps -> if isNullRange ps then posOfId $ opSymbName o else ps

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina Conditional t1 _ t2 ps ->

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

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina Mixfix_parenthesized ts ps ->

41ef946f3f74a46b9e26118116e4811e259b30efPavel Březina if isNullRange ps then concatMapRange posOfTerm ts else ps

41ef946f3f74a46b9e26118116e4811e259b30efPavel Březina Mixfix_bracketed ts ps ->

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce if isNullRange ps then concatMapRange posOfTerm ts else ps

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce Mixfix_braced ts ps ->

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce if isNullRange ps then concatMapRange posOfTerm ts else ps

04b3ab7658985af749460010123bbe37eccf50edPavel Březina _ -> rangeOfTerm trm

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina-- | construct application

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovasAppl :: Id -> [TERM f] -> Range -> TERM f

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovasAppl f args ps = Application (Op_name f) args

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina $ if isNullRange ps then posOfId f else ps

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina-- | constructing the parse tree from (the final) parser state(s)

b510d909cbe8d8216b60ee070730dd5c41294303Pavel BřezinatoAppl :: Id -> [TERM f] -> Range -> TERM f

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovtoAppl ide ar qs =

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov if ide == singleArgId || ide == multiArgsId

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina then assert (length ar > 1) $

b510d909cbe8d8216b60ee070730dd5c41294303Pavel Březina let har : tar = ar

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov hp = posOfTerm har

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ps = appRange hp qs

04b3ab7658985af749460010123bbe37eccf50edPavel Březina in case har of

04b3ab7658985af749460010123bbe37eccf50edPavel Březina Application q ts p -> assert (null ts) $

04b3ab7658985af749460010123bbe37eccf50edPavel Březina Application q tar $ appRange ps p

04b3ab7658985af749460010123bbe37eccf50edPavel Březina Mixfix_qual_pred _ ->

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina Mixfix_term [har, Mixfix_parenthesized tar ps]

4f3a9d837a55b49448eca3c713c85a406207e523Simo Sorce _ -> error "stateToAppl"

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina else asAppl ide ar qs

a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel BřezinaaddType :: TERM f -> TERM f -> TERM f

b0abb3bfdfd95951a23c9fc223c735805ffd2969Pavel BřezinaaddType tt t =

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina case tt of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Mixfix_sorted_term s ps -> Sorted_term t s ps

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina Mixfix_cast s ps -> Cast t s ps

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina _ -> error "addType"

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina-- | the type for mixfix resolution

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březinatype MixResolve f = GlobalAnnos -> (Token -> [Rule], Rules) -> f -> Result f

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel BřezinaiterateCharts :: Pretty f => (f -> f)

15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina -> MixResolve f -> GlobalAnnos -> [TERM f]

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina -> Chart (TERM f) -> Chart (TERM f)

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel BřezinaiterateCharts par extR g terms c =

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina let self = iterateCharts par extR g

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina expand = expandPos Mixfix_token

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina oneStep = nextChart addType toAppl g c

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina ruleS = rules c

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina adder = addRules c

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina resolveTerm = resolveMixTrm par extR g (adder, ruleS)

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina in if null terms then c

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina else case head terms of

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina Mixfix_term ts -> self (ts ++ tail terms) c

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina Mixfix_bracketed ts ps ->

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina self (expand ("[", "]") ts ps ++ tail terms) c

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina Mixfix_braced ts ps ->

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina self (expand ("{", "}") ts ps ++ tail terms) c

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina Mixfix_parenthesized ts ps ->

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina case ts of

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina [h] -> let Result mds v = resolveTerm h

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina tNew = case v of

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina Nothing -> h

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina Just x -> x

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina c2 = self (tail terms) (oneStep (tNew, varTok))

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina in mixDiags mds c2

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina _ -> self (expand ("(", ")") ts ps ++ tail terms) c

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina h@(Conditional t1 f2 t3 ps) ->

d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina let Result mds v =

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina do t4 <- resolveTerm t1

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina f5 <- resolveMixFrm par extR g (adder, ruleS) f2

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina t6 <- resolveTerm t3

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina return (Conditional t4 f5 t6 ps)

46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina tNew = case v of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Nothing -> h

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Just x -> x

b3ca35780617b2e5a7637f9888b089e8e26a4e8cPavel Březina c2 = self (tail terms)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina in mixDiags mds c2

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina Mixfix_token t -> let (ds1, trm) = convertMixfixToken

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina (literal_annos g) asAppl Mixfix_token t

76db25eab9010a33657f35e5afc8477c996df7a3Pavel Březina c2 = self (tail terms) $ oneStep $

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina case trm of

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina Mixfix_token tok -> (trm, tok)

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina _ -> (trm, varTok)

710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina in mixDiags ds1 c2

76db25eab9010a33657f35e5afc8477c996df7a3Pavel Březina t@(Mixfix_sorted_term _ ps) -> self (tail terms)

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina (oneStep (t, typeTok {tokPos = ps}))

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina t@(Mixfix_cast _ ps) -> self (tail terms)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (oneStep (t, typeTok {tokPos = ps}))

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina t@(Qual_var _ _ ps) -> self (tail terms)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (oneStep (t, varTok {tokPos = ps}))

04b3ab7658985af749460010123bbe37eccf50edPavel Březina t@(Application (Qual_op_name _ _ ps) _ _) ->

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina self (tail terms) (oneStep (t, exprTok{tokPos = ps} ))

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Sorted_term t s ps ->

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina let Result mds v = resolveTerm t

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina tNew = Sorted_term (case v of

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Nothing -> t

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina Just x -> x) s ps

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina c2 = self (tail terms) (oneStep (tNew, varTok))

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina in mixDiags mds c2

c47e9d522f0d87259e5074ea643daaa3dfcb8d92Pavel Březina _ -> error "iterateCharts"

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina-- | construct 'IdSets' from op and pred identifiers

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamkIdSets :: Set.Set Id -> Set.Set Id -> IdSets

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel BřezinamkIdSets ops preds = (ops, preds)

2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina

-- | 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