{- |
Module      :  ./CASL/MixfixParser.hs
Description :  Mixfix analysis of terms
Copyright   :  Christian Maeder and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

Mixfix analysis of terms
-}

module CASL.MixfixParser
    ( resolveFormula, resolveMixfix, MixResolve
    , resolveMixTrm, resolveMixFrm
    , extendRules, varDeclTokens
    , extendMixResolve
    , IdSets, mkIdSets, emptyIdSets, unite, unite2
    , makeRules, Mix (..), emptyMix, extendMix
    , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM
    , ids_DATATYPE_DECL
    , addIdToRules
    ) where

import CASL.AS_Basic_CASL
import CASL.ShowMixfix
import CASL.ToDoc

import Common.AS_Annotation
import Common.ConvertMixfixToken
import Common.DocUtils
import Common.Earley
import Common.GlobalAnnotations
import Common.Id
import Common.Result

import qualified Data.Map as Map
import qualified Data.Set as Set

import Data.Maybe

data Mix b s f e = MixRecord
    { Mix b s f e -> b -> IdSets
getBaseIds :: b -> IdSets -- ^ ids of extra basic items
    , Mix b s f e -> s -> IdSets
getSigIds :: s -> IdSets  -- ^ ids of extra sig items
    , Mix b s f e -> e -> IdSets
getExtIds :: e -> IdSets  -- ^ ids of signature extensions
    , Mix b s f e -> (TokRules, Rules)
mixRules :: (TokRules, Rules) -- ^ rules for Earley
    , Mix b s f e -> f -> f
putParen :: f -> f -- ^ parenthesize extended formula
    , Mix b s f e -> MixResolve f
mixResolve :: MixResolve f -- ^ resolve extended formula
    }

-- | an initially empty record
emptyMix :: Mix b s f e
emptyMix :: Mix b s f e
emptyMix = MixRecord :: forall b s f e.
(b -> IdSets)
-> (s -> IdSets)
-> (e -> IdSets)
-> (TokRules, Rules)
-> (f -> f)
-> MixResolve f
-> Mix b s f e
MixRecord
    { getBaseIds :: b -> IdSets
getBaseIds = IdSets -> b -> IdSets
forall a b. a -> b -> a
const IdSets
emptyIdSets
    , getSigIds :: s -> IdSets
getSigIds = IdSets -> s -> IdSets
forall a b. a -> b -> a
const IdSets
emptyIdSets
    , getExtIds :: e -> IdSets
getExtIds = IdSets -> e -> IdSets
forall a b. a -> b -> a
const IdSets
emptyIdSets
    , mixRules :: (TokRules, Rules)
mixRules = (Set Rule -> TokRules
forall a b. a -> b -> a
const Set Rule
forall a. Set a
Set.empty, Rules
emptyRules)
    , putParen :: f -> f
putParen = f -> f
forall a. a -> a
id
    , mixResolve :: MixResolve f
mixResolve = ((TokRules, Rules) -> f -> Result f) -> MixResolve f
forall a b. a -> b -> a
const (((TokRules, Rules) -> f -> Result f) -> MixResolve f)
-> ((TokRules, Rules) -> f -> Result f) -> MixResolve f
forall a b. (a -> b) -> a -> b
$ (f -> Result f) -> (TokRules, Rules) -> f -> Result f
forall a b. a -> b -> a
const f -> Result f
forall (m :: * -> *) a. Monad m => a -> m a
return
    }

extendMix :: Set.Set Token -> Mix b s f e -> Mix b s f e
extendMix :: Set Token -> Mix b s f e -> Mix b s f e
extendMix ts :: Set Token
ts r :: Mix b s f e
r = Mix b s f e
r
  { mixRules :: (TokRules, Rules)
mixRules = Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules Set Token
ts ((TokRules, Rules) -> (TokRules, Rules))
-> (TokRules, Rules) -> (TokRules, Rules)
forall a b. (a -> b) -> a -> b
$ Mix b s f e -> (TokRules, Rules)
forall b s f e. Mix b s f e -> (TokRules, Rules)
mixRules Mix b s f e
r
  , mixResolve :: MixResolve f
mixResolve = Set Token -> MixResolve f -> MixResolve f
forall f. Set Token -> MixResolve f -> MixResolve f
extendMixResolve Set Token
ts (MixResolve f -> MixResolve f) -> MixResolve f -> MixResolve f
forall a b. (a -> b) -> a -> b
$ Mix b s f e -> MixResolve f
forall b s f e. Mix b s f e -> MixResolve f
mixResolve Mix b s f e
r }

-- precompute non-simple op and pred identifier for mixfix rules

-- | the precomputed sets of constant, op, and pred identifiers
type IdSets = ((Set.Set Id, Set.Set Id), Set.Set Id) -- ops are first component

-- | the empty 'IdSets'
emptyIdSets :: IdSets
emptyIdSets :: IdSets
emptyIdSets = let e :: Set a
e = Set a
forall a. Set a
Set.empty in ((Set Id
forall a. Set a
e, Set Id
forall a. Set a
e), Set Id
forall a. Set a
e)

unite2 :: [(Set.Set Id, Set.Set Id)] -> (Set.Set Id, Set.Set Id)
unite2 :: [(Set Id, Set Id)] -> (Set Id, Set Id)
unite2 l :: [(Set Id, Set Id)]
l = ([Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ ((Set Id, Set Id) -> Set Id) -> [(Set Id, Set Id)] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map (Set Id, Set Id) -> Set Id
forall a b. (a, b) -> a
fst [(Set Id, Set Id)]
l, [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ ((Set Id, Set Id) -> Set Id) -> [(Set Id, Set Id)] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map (Set Id, Set Id) -> Set Id
forall a b. (a, b) -> b
snd [(Set Id, Set Id)]
l)

-- | union 'IdSets'
unite :: [IdSets] -> IdSets
unite :: [IdSets] -> IdSets
unite l :: [IdSets]
l = ([(Set Id, Set Id)] -> (Set Id, Set Id)
unite2 ([(Set Id, Set Id)] -> (Set Id, Set Id))
-> [(Set Id, Set Id)] -> (Set Id, Set Id)
forall a b. (a -> b) -> a -> b
$ (IdSets -> (Set Id, Set Id)) -> [IdSets] -> [(Set Id, Set Id)]
forall a b. (a -> b) -> [a] -> [b]
map IdSets -> (Set Id, Set Id)
forall a b. (a, b) -> a
fst [IdSets]
l, [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (IdSets -> Set Id) -> [IdSets] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map IdSets -> Set Id
forall a b. (a, b) -> b
snd [IdSets]
l)

-- | get all ids of a basic spec
ids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
ids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
ids_BASIC_SPEC f :: b -> IdSets
f g :: s -> IdSets
g (Basic_spec al :: [Annoted (BASIC_ITEMS b s f)]
al) =
    [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$ (Annoted (BASIC_ITEMS b s f) -> IdSets)
-> [Annoted (BASIC_ITEMS b s f)] -> [IdSets]
forall a b. (a -> b) -> [a] -> [b]
map ((b -> IdSets) -> (s -> IdSets) -> BASIC_ITEMS b s f -> IdSets
forall b s f.
(b -> IdSets) -> (s -> IdSets) -> BASIC_ITEMS b s f -> IdSets
ids_BASIC_ITEMS b -> IdSets
f s -> IdSets
g (BASIC_ITEMS b s f -> IdSets)
-> (Annoted (BASIC_ITEMS b s f) -> BASIC_ITEMS b s f)
-> Annoted (BASIC_ITEMS b s f)
-> IdSets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (BASIC_ITEMS b s f) -> BASIC_ITEMS b s f
forall a. Annoted a -> a
item) [Annoted (BASIC_ITEMS b s f)]
al

ids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)
                -> BASIC_ITEMS b s f -> IdSets
ids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets) -> BASIC_ITEMS b s f -> IdSets
ids_BASIC_ITEMS f :: b -> IdSets
f g :: s -> IdSets
g bi :: BASIC_ITEMS b s f
bi = case BASIC_ITEMS b s f
bi of
    Sig_items sis :: SIG_ITEMS s f
sis -> (s -> IdSets) -> SIG_ITEMS s f -> IdSets
forall s f. (s -> IdSets) -> SIG_ITEMS s f -> IdSets
ids_SIG_ITEMS s -> IdSets
g SIG_ITEMS s f
sis
    Free_datatype _ al :: [Annoted DATATYPE_DECL]
al _ -> [Annoted DATATYPE_DECL] -> IdSets
ids_anDATATYPE_DECLs [Annoted DATATYPE_DECL]
al
    Sort_gen al :: [Annoted (SIG_ITEMS s f)]
al _ -> [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$ (Annoted (SIG_ITEMS s f) -> IdSets)
-> [Annoted (SIG_ITEMS s f)] -> [IdSets]
forall a b. (a -> b) -> [a] -> [b]
map ((s -> IdSets) -> SIG_ITEMS s f -> IdSets
forall s f. (s -> IdSets) -> SIG_ITEMS s f -> IdSets
ids_SIG_ITEMS s -> IdSets
g (SIG_ITEMS s f -> IdSets)
-> (Annoted (SIG_ITEMS s f) -> SIG_ITEMS s f)
-> Annoted (SIG_ITEMS s f)
-> IdSets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SIG_ITEMS s f) -> SIG_ITEMS s f
forall a. Annoted a -> a
item) [Annoted (SIG_ITEMS s f)]
al
    Ext_BASIC_ITEMS b :: b
b -> b -> IdSets
f b
b
    _ -> IdSets
emptyIdSets

ids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets
ids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets
ids_anDATATYPE_DECLs al :: [Annoted DATATYPE_DECL]
al =
    ([(Set Id, Set Id)] -> (Set Id, Set Id)
unite2 ([(Set Id, Set Id)] -> (Set Id, Set Id))
-> [(Set Id, Set Id)] -> (Set Id, Set Id)
forall a b. (a -> b) -> a -> b
$ (Annoted DATATYPE_DECL -> (Set Id, Set Id))
-> [Annoted DATATYPE_DECL] -> [(Set Id, Set Id)]
forall a b. (a -> b) -> [a] -> [b]
map (DATATYPE_DECL -> (Set Id, Set Id)
ids_DATATYPE_DECL (DATATYPE_DECL -> (Set Id, Set Id))
-> (Annoted DATATYPE_DECL -> DATATYPE_DECL)
-> Annoted DATATYPE_DECL
-> (Set Id, Set Id)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted DATATYPE_DECL -> DATATYPE_DECL
forall a. Annoted a -> a
item) [Annoted DATATYPE_DECL]
al, Set Id
forall a. Set a
Set.empty)

-- | get all ids of a sig items
ids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets
ids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets
ids_SIG_ITEMS f :: s -> IdSets
f si :: SIG_ITEMS s f
si = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case SIG_ITEMS s f
si of
    Sort_items {} -> IdSets
emptyIdSets
    Op_items al :: [Annoted (OP_ITEM f)]
al _ -> ([(Set Id, Set Id)] -> (Set Id, Set Id)
unite2 ([(Set Id, Set Id)] -> (Set Id, Set Id))
-> [(Set Id, Set Id)] -> (Set Id, Set Id)
forall a b. (a -> b) -> a -> b
$ (Annoted (OP_ITEM f) -> (Set Id, Set Id))
-> [Annoted (OP_ITEM f)] -> [(Set Id, Set Id)]
forall a b. (a -> b) -> [a] -> [b]
map (OP_ITEM f -> (Set Id, Set Id)
forall f. OP_ITEM f -> (Set Id, Set Id)
ids_OP_ITEM (OP_ITEM f -> (Set Id, Set Id))
-> (Annoted (OP_ITEM f) -> OP_ITEM f)
-> Annoted (OP_ITEM f)
-> (Set Id, Set Id)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM f) -> OP_ITEM f
forall a. Annoted a -> a
item) [Annoted (OP_ITEM f)]
al, Set Id
forall a. Set a
e)
    Pred_items al :: [Annoted (PRED_ITEM f)]
al _ -> ((Set Id
forall a. Set a
e, Set Id
forall a. Set a
e), [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Annoted (PRED_ITEM f) -> Set Id)
-> [Annoted (PRED_ITEM f)] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map (PRED_ITEM f -> Set Id
forall f. PRED_ITEM f -> Set Id
ids_PRED_ITEM (PRED_ITEM f -> Set Id)
-> (Annoted (PRED_ITEM f) -> PRED_ITEM f)
-> Annoted (PRED_ITEM f)
-> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (PRED_ITEM f) -> PRED_ITEM f
forall a. Annoted a -> a
item) [Annoted (PRED_ITEM f)]
al)
    Datatype_items _ al :: [Annoted DATATYPE_DECL]
al _ -> [Annoted DATATYPE_DECL] -> IdSets
ids_anDATATYPE_DECLs [Annoted DATATYPE_DECL]
al
    Ext_SIG_ITEMS s :: s
s -> s -> IdSets
f s
s

-- | get all op ids of an op item
ids_OP_ITEM :: OP_ITEM f -> (Set.Set Id, Set.Set Id)
ids_OP_ITEM :: OP_ITEM f -> (Set Id, Set Id)
ids_OP_ITEM o :: OP_ITEM f
o = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case OP_ITEM f
o of
    Op_decl ops :: [Id]
ops (Op_type _ args :: [Id]
args _ _) _ _ ->
      let s :: Set Id
s = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id]
ops in
      if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
args then (Set Id
s, Set Id
forall a. Set a
e) else (Set Id
forall a. Set a
e, Set Id
s)
    Op_defn i :: Id
i (Op_head _ args :: [VAR_DECL]
args _ _) _ _ ->
      let s :: Set Id
s = Id -> Set Id
forall a. a -> Set a
Set.singleton Id
i in
      if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
args then (Set Id
s, Set Id
forall a. Set a
e) else (Set Id
forall a. Set a
e, Set Id
s)

-- | get all pred ids of a pred item
ids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id
ids_PRED_ITEM :: PRED_ITEM f -> Set Id
ids_PRED_ITEM p :: PRED_ITEM f
p = case PRED_ITEM f
p of
    Pred_decl preds :: [Id]
preds _ _ -> [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Id -> Set Id) -> [Id] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Set Id
forall a. a -> Set a
Set.singleton [Id]
preds
    Pred_defn i :: Id
i _ _ _ -> Id -> Set Id
forall a. a -> Set a
Set.singleton Id
i

ids_DATATYPE_DECL :: DATATYPE_DECL -> (Set.Set Id, Set.Set Id)
ids_DATATYPE_DECL :: DATATYPE_DECL -> (Set Id, Set Id)
ids_DATATYPE_DECL (Datatype_decl _ al :: [Annoted ALTERNATIVE]
al _) =
    [(Set Id, Set Id)] -> (Set Id, Set Id)
unite2 ([(Set Id, Set Id)] -> (Set Id, Set Id))
-> [(Set Id, Set Id)] -> (Set Id, Set Id)
forall a b. (a -> b) -> a -> b
$ (Annoted ALTERNATIVE -> (Set Id, Set Id))
-> [Annoted ALTERNATIVE] -> [(Set Id, Set Id)]
forall a b. (a -> b) -> [a] -> [b]
map (ALTERNATIVE -> (Set Id, Set Id)
ids_ALTERNATIVE (ALTERNATIVE -> (Set Id, Set Id))
-> (Annoted ALTERNATIVE -> ALTERNATIVE)
-> Annoted ALTERNATIVE
-> (Set Id, Set Id)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ALTERNATIVE -> ALTERNATIVE
forall a. Annoted a -> a
item) [Annoted ALTERNATIVE]
al

ids_ALTERNATIVE :: ALTERNATIVE -> (Set.Set Id, Set.Set Id)
ids_ALTERNATIVE :: ALTERNATIVE -> (Set Id, Set Id)
ids_ALTERNATIVE a :: ALTERNATIVE
a = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case ALTERNATIVE
a of
    Alt_construct _ i :: Id
i cs :: [COMPONENTS]
cs _ -> let s :: Set Id
s = Id -> Set Id
forall a. a -> Set a
Set.singleton Id
i in
      if [COMPONENTS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [COMPONENTS]
cs then (Set Id
s, Set Id
forall a. Set a
e) else (Set Id
forall a. Set a
e, [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ Set Id
s Set Id -> [Set Id] -> [Set Id]
forall a. a -> [a] -> [a]
: (COMPONENTS -> Set Id) -> [COMPONENTS] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map COMPONENTS -> Set Id
ids_COMPONENTS [COMPONENTS]
cs)
    Subsorts _ _ -> (Set Id
forall a. Set a
e, Set Id
forall a. Set a
e)

ids_COMPONENTS :: COMPONENTS -> Set.Set Id
ids_COMPONENTS :: COMPONENTS -> Set Id
ids_COMPONENTS c :: COMPONENTS
c = case COMPONENTS
c of
    Cons_select _ l :: [Id]
l _ _ -> [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> [Set Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (Id -> Set Id) -> [Id] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Set Id
forall a. a -> Set a
Set.singleton [Id]
l
    Sort _ -> Set Id
forall a. Set a
Set.empty

-- predicates get lower precedence
mkRule :: Id -> Rule
mkRule :: Id -> Rule
mkRule = Int -> Id -> Rule
mixRule 1

mkSingleArgRule :: Int -> Id -> Rule
mkSingleArgRule :: Int -> Id -> Rule
mkSingleArgRule b :: Int
b ide :: Id
ide = (Id -> Id
protect Id
ide, Int
b, Id -> [Token]
getPlainTokenList Id
ide [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
varTok])

mkArgsRule :: Int -> Id -> Rule
mkArgsRule :: Int -> Id -> Rule
mkArgsRule b :: Int
b ide :: Id
ide =
  (Id -> Id
protect Id
ide, Int
b, Id -> [Token]
getPlainTokenList Id
ide [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ Id -> [Token]
getTokenPlaceList Id
tupleId)

singleArgId :: Id
singleArgId :: Id
singleArgId = [Token] -> Id
mkId [Token
exprTok, Token
varTok]

multiArgsId :: Id
multiArgsId :: Id
multiArgsId = [Token] -> Id
mkId (Token
exprTok Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: Id -> [Token]
getPlainTokenList Id
tupleId)

addIdToRules :: Id -> (TokRules, Rules) -> (TokRules, Rules)
addIdToRules :: Id -> (TokRules, Rules) -> (TokRules, Rules)
addIdToRules i :: Id
i (tr :: TokRules
tr, rs :: Rules
rs) =
   (TokRules
tr, let newSc :: Set Rule
newSc = Set Rule -> Set Rule -> Set Rule
forall a. Ord a => Set a -> Set a -> Set a
Set.union
              ([Rule] -> Set Rule
forall a. Ord a => [a] -> Set a
Set.fromList [Int -> Id -> Rule
mkSingleArgRule 1 Id
i, Int -> Id -> Rule
mkArgsRule 1 Id
i])
              (Set Rule -> Set Rule) -> Set Rule -> Set Rule
forall a b. (a -> b) -> a -> b
$ Rules -> Set Rule
scanRules Rules
rs
        in if Id -> Bool
begPlace Id
i then
            Rules
rs { postRules :: Set Rule
postRules = Rule -> Set Rule -> Set Rule
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int -> Id -> Rule
mixRule 1 Id
i) (Set Rule -> Set Rule) -> Set Rule -> Set Rule
forall a b. (a -> b) -> a -> b
$ Rules -> Set Rule
postRules Rules
rs
               , scanRules :: Set Rule
scanRules = Set Rule
newSc }
        else Rules
rs { scanRules :: Set Rule
scanRules = Rule -> Set Rule -> Set Rule
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int -> Id -> Rule
mixRule 1 Id
i) Set Rule
newSc })

-- | additional scan rules
addRule :: GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules
addRule :: GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules
addRule ga :: GlobalAnnos
ga uRules :: [Rule]
uRules hasInvisible :: Bool
hasInvisible ((consts :: Set Id
consts, ops :: Set Id
ops), preds :: Set Id
preds) tok :: Token
tok =
    let addP :: Map Token [Rule] -> Set Id -> Map Token [Rule]
addP = (Id -> Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> Set Id -> Map Token [Rule]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ i :: Id
i -> case Id
i of
                 Id (t :: Token
t : _) _ _ -> ([Rule] -> [Rule] -> [Rule])
-> Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
(++) Token
t
                   [ Int -> Id -> Rule
mixRule (if Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i Set Id
consts then 1 else 0) Id
i
                   , Int -> Id -> Rule
mkSingleArgRule 0 Id
i, Int -> Id -> Rule
mkArgsRule 0 Id
i]
                 _ -> [Char] -> Map Token [Rule] -> Map Token [Rule]
forall a. HasCallStack => [Char] -> a
error "addRule.addP")
        addO :: Map Token [Rule] -> Set Id -> Map Token [Rule]
addO = (Id -> Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> Set Id -> Map Token [Rule]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ i :: Id
i -> case Id
i of
                 Id (t :: Token
t : _) _ _ -> ([Rule] -> [Rule] -> [Rule])
-> Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
(++) Token
t
                   ([Rule] -> Map Token [Rule] -> Map Token [Rule])
-> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall a b. (a -> b) -> a -> b
$ [Id -> Rule
mkRule Id
i | Bool -> Bool
not (Id -> Bool
isSimpleId Id
i)
                      Bool -> Bool -> Bool
|| Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i (Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
consts Set Id
preds) ]
                   [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ [Int -> Id -> Rule
mkSingleArgRule 1 Id
i, Int -> Id -> Rule
mkArgsRule 1 Id
i]
                 _ -> [Char] -> Map Token [Rule] -> Map Token [Rule]
forall a. HasCallStack => [Char] -> a
error "addRule.addO")
        addC :: Map Token [Rule] -> Set Id -> Map Token [Rule]
addC = (Id -> Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> Set Id -> Map Token [Rule]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ i :: Id
i -> case Id
i of
                 Id (t :: Token
t : _) _ _ -> ([Rule] -> [Rule] -> [Rule])
-> Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
(++) Token
t [Id -> Rule
mkRule Id
i]
                 _ -> [Char] -> Map Token [Rule] -> Map Token [Rule]
forall a. HasCallStack => [Char] -> a
error "addRule.addC")
        lm :: Map Token [Rule]
lm = (Rule -> Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> [Rule] -> Map Token [Rule]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ r :: Rule
r -> case Rule
r of
               (_, _, t :: Token
t : _) -> ([Rule] -> [Rule] -> [Rule])
-> Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
(++) Token
t [Rule
r]
               _ -> [Char] -> Map Token [Rule] -> Map Token [Rule]
forall a. HasCallStack => [Char] -> a
error "addRule.lm") Map Token [Rule]
forall k a. Map k a
Map.empty ([Rule] -> Map Token [Rule]) -> [Rule] -> Map Token [Rule]
forall a b. (a -> b) -> a -> b
$ Int -> GlobalAnnos -> [Rule]
listRules 1 GlobalAnnos
ga
        (spreds :: Set Id
spreds, rpreds :: Set Id
rpreds) = (Id -> Bool) -> Set Id -> (Set Id, Set Id)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition Id -> Bool
isSimpleId Set Id
preds
        {- do not add simple ids as preds as these may be variables
        with higher precedence -}
        ops2 :: Set Id
ops2 = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
ops Set Id
spreds
        sops :: Set Id
sops = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
consts Set Id
ops2
        rConsts :: Set Id
rConsts = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Id
consts (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
ops Set Id
preds
        varR :: Rule
varR = Id -> Rule
mkRule Id
varId
        m :: Map Token [Rule]
m = Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
placeTok [Rule]
uRules
            (Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> Map Token [Rule]
forall a b. (a -> b) -> a -> b
$ Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
varTok [Rule
varR]
            (Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> Map Token [Rule]
forall a b. (a -> b) -> a -> b
$ Token -> [Rule] -> Map Token [Rule] -> Map Token [Rule]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
exprTok
                  [Rule
varR, Id -> Rule
mkRule Id
singleArgId, Id -> Rule
mkRule Id
multiArgsId]
            (Map Token [Rule] -> Map Token [Rule])
-> Map Token [Rule] -> Map Token [Rule]
forall a b. (a -> b) -> a -> b
$ Map Token [Rule] -> Set Id -> Map Token [Rule]
addP (Map Token [Rule] -> Set Id -> Map Token [Rule]
addC (Map Token [Rule] -> Set Id -> Map Token [Rule]
addO Map Token [Rule]
lm Set Id
ops2) Set Id
rConsts) (Set Id -> Map Token [Rule]) -> Set Id -> Map Token [Rule]
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Id
rpreds Set Id
ops
        tId :: Id
tId = [Token] -> Id
mkId [Token
tok]
        tPId :: Id
tPId = [Token] -> Id
mkId [Token
tok, Token
placeTok] -- prefix identifier
    in (if Token -> Bool
isSimpleToken Token
tok Bool -> Bool -> Bool
&& Bool -> Bool
not (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
tId Set Id
sops)
        then if Bool
hasInvisible then Set Rule
forall a. Set a
Set.empty else
             Rule -> Set Rule -> Set Rule
forall a. Ord a => a -> Set a -> Set a
Set.insert (Id -> Rule
mkRule Id
tId)
             -- add rule for unknown constant or variable
             (Set Rule -> Set Rule) -> Set Rule -> Set Rule
forall a b. (a -> b) -> a -> b
$ if Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
tPId Set Id
ops Bool -> Bool -> Bool
|| Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
tPId Set Id
rpreds
               then Set Rule
forall a. Set a
Set.empty else
                 [Rule] -> Set Rule
forall a. Ord a => [a] -> Set a
Set.fromList [Int -> Id -> Rule
mkSingleArgRule 1 Id
tId, Int -> Id -> Rule
mkArgsRule 1 Id
tId]
              -- add also rules for undeclared op
        else Set Rule
forall a. Set a
Set.empty) Set Rule -> Set Rule -> Set Rule
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [Rule] -> Set Rule
forall a. Ord a => [a] -> Set a
Set.fromList ([Rule] -> Token -> Map Token [Rule] -> [Rule]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Token
tok Map Token [Rule]
m)

-- insert only identifiers starting with a place
initRules :: (Set.Set Id, Set.Set Id) -> Rules
initRules :: (Set Id, Set Id) -> Rules
initRules (opS :: Set Id
opS, predS :: Set Id
predS) =
  let addR :: Int -> Set Rule -> Set Id -> Set Rule
addR p :: Int
p = (Id -> Set Rule -> Set Rule) -> Set Rule -> Set Id -> Set Rule
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Rule -> Set Rule -> Set Rule
forall a. Ord a => a -> Set a -> Set a
Set.insert (Rule -> Set Rule -> Set Rule)
-> (Id -> Rule) -> Id -> Set Rule -> Set Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Id -> Rule
mixRule Int
p)
  in Rules
emptyRules
  { postRules :: Set Rule
postRules = Int -> Set Rule -> Set Id -> Set Rule
addR 1 (Int -> Set Rule -> Set Id -> Set Rule
addR 0 (Rule -> Set Rule
forall a. a -> Set a
Set.singleton (Rule -> Set Rule) -> Rule -> Set Rule
forall a b. (a -> b) -> a -> b
$ Id -> Rule
mkRule Id
typeId) Set Id
predS) Set Id
opS }

-- | construct rules from 'IdSets' to be put into a 'Mix' record
makeRules :: GlobalAnnos -> IdSets -> (TokRules, Rules)
makeRules :: GlobalAnnos -> IdSets -> (TokRules, Rules)
makeRules ga :: GlobalAnnos
ga ((constS :: Set Id
constS, opS :: Set Id
opS), predS :: Set Id
predS) = let
    (cOps :: Set Id
cOps, sOps :: Set Id
sOps) = (Id -> Bool) -> Set Id -> (Set Id, Set Id)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition Id -> Bool
begPlace Set Id
opS
    (cPreds :: Set Id
cPreds, sPreds :: Set Id
sPreds) = (Id -> Bool) -> Set Id -> (Set Id, Set Id)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition Id -> Bool
begPlace (Set Id -> (Set Id, Set Id)) -> Set Id -> (Set Id, Set Id)
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Id
predS Set Id
opS
    addR :: Int -> [Rule] -> Set Id -> [Rule]
addR p :: Int
p = (Id -> [Rule] -> [Rule]) -> [Rule] -> Set Id -> [Rule]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ i :: Id
i l :: [Rule]
l ->
           Int -> Id -> Rule
mkSingleArgRule Int
p Id
i Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
: Int -> Id -> Rule
mkArgsRule Int
p Id
i Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
: [Rule]
l)
    uRules :: [Rule]
uRules = Int -> [Rule] -> Set Id -> [Rule]
addR 0 (Int -> [Rule] -> Set Id -> [Rule]
addR 1 [] Set Id
cOps) Set Id
cPreds
    in (GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules
addRule GlobalAnnos
ga [Rule]
uRules (Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
applId (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
cOps Set Id
cPreds)
        ((Set Id
constS, Set Id
sOps), Set Id
sPreds), (Set Id, Set Id) -> Rules
initRules (Set Id
cOps, Set Id
cPreds))

-- | construct application
asAppl :: Id -> [TERM f] -> Range -> TERM f
asAppl :: Id -> [TERM f] -> Range -> TERM f
asAppl f :: Id
f args :: [TERM f]
args ps :: Range
ps = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_SYMB
Op_name Id
f) [TERM f]
args
                 (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ if Range -> Bool
isNullRange Range
ps then Id -> Range
posOfId Id
f else Range
ps

-- | constructing the parse tree from (the final) parser state(s)
toAppl :: GetRange f => Id -> [TERM f] -> Range -> TERM f
toAppl :: Id -> [TERM f] -> Range -> TERM f
toAppl ide :: Id
ide ar :: [TERM f]
ar ps :: Range
ps =
       if Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
ide [Id
singleArgId, Id
multiArgsId]
            then case [TERM f]
ar of
              har :: TERM f
har : tar :: [TERM f]
tar -> case TERM f
har of
                 Application q :: OP_SYMB
q [] p :: Range
p ->
                     OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
q [TERM f]
tar (Range -> TERM f) -> Range -> TERM f
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
ps Range
p
                 Mixfix_qual_pred _ ->
                     [TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term [TERM f
har, [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM f]
tar Range
ps]
                 _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error "stateToAppl"
              _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error "stateToAppl2"
            else Id -> [TERM f] -> Range -> TERM f
forall f. Id -> [TERM f] -> Range -> TERM f
asAppl Id
ide [TERM f]
ar Range
ps

addType :: TERM f -> TERM f -> TERM f
addType :: TERM f -> TERM f -> TERM f
addType tt :: TERM f
tt t :: TERM f
t =
    case TERM f
tt of
    Mixfix_sorted_term s :: Id
s ps :: Range
ps -> TERM f -> Id -> Range -> TERM f
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM f
t Id
s Range
ps
    Mixfix_cast s :: Id
s ps :: Range
ps -> TERM f -> Id -> Range -> TERM f
forall f. TERM f -> Id -> Range -> TERM f
Cast TERM f
t Id
s Range
ps
    _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error "addType"

-- | the type for mixfix resolution
type MixResolve f = GlobalAnnos -> (TokRules, Rules) -> f -> Result f

iterateCharts :: FormExtension f => (f -> f)
              -> MixResolve f -> GlobalAnnos -> [TERM f]
              -> Chart (TERM f) -> Chart (TERM f)
iterateCharts :: (f -> f)
-> MixResolve f
-> GlobalAnnos
-> [TERM f]
-> Chart (TERM f)
-> Chart (TERM f)
iterateCharts par :: f -> f
par extR :: MixResolve f
extR g :: GlobalAnnos
g terms :: [TERM f]
terms c :: Chart (TERM f)
c =
    let self :: [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self = (f -> f)
-> MixResolve f
-> GlobalAnnos
-> [TERM f]
-> Chart (TERM f)
-> Chart (TERM f)
forall f.
FormExtension f =>
(f -> f)
-> MixResolve f
-> GlobalAnnos
-> [TERM f]
-> Chart (TERM f)
-> Chart (TERM f)
iterateCharts f -> f
par MixResolve f
extR GlobalAnnos
g
        expand :: ([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
expand = (Token -> TERM f)
-> ([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
forall a. (Token -> a) -> ([Char], [Char]) -> [a] -> Range -> [a]
expandPos Token -> TERM f
forall f. Token -> TERM f
Mixfix_token
        oneStep :: (TERM f, Token) -> Chart (TERM f)
oneStep = (TERM f -> TERM f -> TERM f)
-> ToExpr (TERM f)
-> GlobalAnnos
-> Chart (TERM f)
-> (TERM f, Token)
-> Chart (TERM f)
forall a.
(a -> a -> a)
-> ToExpr a -> GlobalAnnos -> Chart a -> (a, Token) -> Chart a
nextChart TERM f -> TERM f -> TERM f
forall f. TERM f -> TERM f -> TERM f
addType ToExpr (TERM f)
forall f. GetRange f => Id -> [TERM f] -> Range -> TERM f
toAppl GlobalAnnos
g Chart (TERM f)
c
        ids :: (TokRules, Rules)
ids = (Chart (TERM f) -> TokRules
forall a. Chart a -> TokRules
addRules Chart (TERM f)
c, Chart (TERM f) -> Rules
forall a. Chart a -> Rules
rules Chart (TERM f)
c)
        resolveTerm :: TERM f -> Result (TERM f)
resolveTerm = (f -> f) -> MixResolve f -> MixResolve (TERM f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm f -> f
par MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ids
    in case [TERM f]
terms of
    [] -> Chart (TERM f)
c
    hd :: TERM f
hd : tl :: [TERM f]
tl -> case TERM f
hd of
            Mixfix_term ts :: [TERM f]
ts -> [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self ([TERM f]
ts [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
tl) Chart (TERM f)
c
            Mixfix_bracketed ts :: [TERM f]
ts ps :: Range
ps ->
                [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self (([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
forall f. ([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
expand ("[", "]") [TERM f]
ts Range
ps [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
tl) Chart (TERM f)
c
            Mixfix_braced ts :: [TERM f]
ts ps :: Range
ps ->
                [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self (([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
forall f. ([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
expand ("{", "}") [TERM f]
ts Range
ps [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
tl) Chart (TERM f)
c
            Mixfix_parenthesized ts :: [TERM f]
ts ps :: Range
ps -> case [TERM f]
ts of
              [h :: TERM f
h] -> let
                Result mds :: [Diagnosis]
mds v :: Maybe (TERM f)
v = TERM f -> Result (TERM f)
resolveTerm TERM f
h
                c2 :: Chart (TERM f)
c2 = [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f -> Maybe (TERM f) -> TERM f
forall a. a -> Maybe a -> a
fromMaybe TERM f
h Maybe (TERM f)
v, Token
varTok {tokPos :: Range
tokPos = Range
ps}))
                in [Diagnosis] -> Chart (TERM f) -> Chart (TERM f)
forall a. [Diagnosis] -> Chart a -> Chart a
mixDiags [Diagnosis]
mds Chart (TERM f)
c2
              _ -> [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self (([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
forall f. ([Char], [Char]) -> [TERM f] -> Range -> [TERM f]
expand ("(", ")") [TERM f]
ts Range
ps [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
tl) Chart (TERM f)
c
            h :: TERM f
h@(Conditional t1 :: TERM f
t1 f2 :: FORMULA f
f2 t3 :: TERM f
t3 ps :: Range
ps) -> let
              Result mds :: [Diagnosis]
mds v :: Maybe (TERM f)
v = do
                TERM f
t4 <- TERM f -> Result (TERM f)
resolveTerm TERM f
t1
                FORMULA f
f5 <- (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm f -> f
par MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ids FORMULA f
f2
                TERM f
t6 <- TERM f -> Result (TERM f)
resolveTerm TERM f
t3
                TERM f -> Result (TERM f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
t4 FORMULA f
f5 TERM f
t6 Range
ps)
              c2 :: Chart (TERM f)
c2 = [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl
                   ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f -> Maybe (TERM f) -> TERM f
forall a. a -> Maybe a -> a
fromMaybe TERM f
h Maybe (TERM f)
v, Token
varTok {tokPos :: Range
tokPos = Range
ps}))
              in [Diagnosis] -> Chart (TERM f) -> Chart (TERM f)
forall a. [Diagnosis] -> Chart a -> Chart a
mixDiags [Diagnosis]
mds Chart (TERM f)
c2
            Mixfix_token t :: Token
t -> let
              (ds1 :: [Diagnosis]
ds1, trm :: TERM f
trm) = LiteralAnnos
-> AsAppl (TERM f)
-> (Token -> TERM f)
-> Token
-> ([Diagnosis], TERM f)
forall a.
LiteralAnnos
-> AsAppl a -> (Token -> a) -> Token -> ([Diagnosis], a)
convertMixfixToken (GlobalAnnos -> LiteralAnnos
literal_annos GlobalAnnos
g) AsAppl (TERM f)
forall f. Id -> [TERM f] -> Range -> TERM f
asAppl
                Token -> TERM f
forall f. Token -> TERM f
Mixfix_token Token
t
              c2 :: Chart (TERM f)
c2 = [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl (Chart (TERM f) -> Chart (TERM f))
-> Chart (TERM f) -> Chart (TERM f)
forall a b. (a -> b) -> a -> b
$ (TERM f, Token) -> Chart (TERM f)
oneStep ((TERM f, Token) -> Chart (TERM f))
-> (TERM f, Token) -> Chart (TERM f)
forall a b. (a -> b) -> a -> b
$ case TERM Any
forall f. TERM f
trm of
                Mixfix_token tok :: Token
tok -> (TERM f
forall f. TERM f
trm, Token
tok)
                _ -> (TERM f
forall f. TERM f
trm, Token
varTok {tokPos :: Range
tokPos = Token -> Range
tokPos Token
t})
              in [Diagnosis] -> Chart (TERM f) -> Chart (TERM f)
forall a. [Diagnosis] -> Chart a -> Chart a
mixDiags [Diagnosis]
ds1 Chart (TERM f)
c2
            t :: TERM f
t@(Mixfix_sorted_term _ ps :: Range
ps) ->
              [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f
t, Token
typeTok {tokPos :: Range
tokPos = Range
ps}))
            t :: TERM f
t@(Mixfix_cast _ ps :: Range
ps) ->
              [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f
t, Token
typeTok {tokPos :: Range
tokPos = Range
ps}))
            t :: TERM f
t@(Qual_var _ _ ps :: Range
ps) ->
              [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f
t, Token
varTok {tokPos :: Range
tokPos = Range
ps}))
            Application opNam :: OP_SYMB
opNam ts :: [TERM f]
ts ps :: Range
ps -> let
              Result mds :: [Diagnosis]
mds v :: Maybe [TERM f]
v = (TERM f -> Result (TERM f)) -> [TERM f] -> Result [TERM f]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TERM f -> Result (TERM f)
resolveTerm [TERM f]
ts
              c2 :: Chart (TERM f)
c2 = [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl (Chart (TERM f) -> Chart (TERM f))
-> Chart (TERM f) -> Chart (TERM f)
forall a b. (a -> b) -> a -> b
$ (TERM f, Token) -> Chart (TERM f)
oneStep (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
opNam ([TERM f] -> Maybe [TERM f] -> [TERM f]
forall a. a -> Maybe a -> a
fromMaybe [TERM f]
ts Maybe [TERM f]
v) Range
ps
                                     , case OP_SYMB
opNam of
                     Qual_op_name _ _ qs :: Range
qs -> Token
exprTok {tokPos :: Range
tokPos = Range
qs}
                     Op_name o :: Id
o -> Token
varTok {tokPos :: Range
tokPos = Id -> Range
posOfId Id
o})
              in [Diagnosis] -> Chart (TERM f) -> Chart (TERM f)
forall a. [Diagnosis] -> Chart a -> Chart a
mixDiags [Diagnosis]
mds Chart (TERM f)
c2
            t :: TERM f
t@(Mixfix_qual_pred (Qual_pred_name _ _ ps :: Range
ps)) ->
                [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f
t, Token
exprTok {tokPos :: Range
tokPos = Range
ps} ))
            Sorted_term t :: TERM f
t s :: Id
s ps :: Range
ps -> let
              Result mds :: [Diagnosis]
mds v :: Maybe (TERM f)
v = TERM f -> Result (TERM f)
resolveTerm TERM f
t
              tNew :: TERM f
tNew = TERM f -> Id -> Range -> TERM f
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term (TERM f -> Maybe (TERM f) -> TERM f
forall a. a -> Maybe a -> a
fromMaybe TERM f
t Maybe (TERM f)
v) Id
s Range
ps
              c2 :: Chart (TERM f)
c2 = [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl ((TERM f, Token) -> Chart (TERM f)
oneStep (TERM f
tNew, Token
varTok {tokPos :: Range
tokPos = Range
ps}))
              in [Diagnosis] -> Chart (TERM f) -> Chart (TERM f)
forall a. [Diagnosis] -> Chart a -> Chart a
mixDiags [Diagnosis]
mds Chart (TERM f)
c2
            ExtTERM t :: f
t -> let
              Result mds :: [Diagnosis]
mds v :: Maybe f
v = MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ids f
t
              tNew :: TERM f
tNew = f -> TERM f
forall f. f -> TERM f
ExtTERM (f -> TERM f) -> f -> TERM f
forall a b. (a -> b) -> a -> b
$ f -> Maybe f -> f
forall a. a -> Maybe a -> a
fromMaybe f
t Maybe f
v
              c2 :: Chart (TERM f)
c2 = [TERM f] -> Chart (TERM f) -> Chart (TERM f)
self [TERM f]
tl (Chart (TERM f) -> Chart (TERM f))
-> Chart (TERM f) -> Chart (TERM f)
forall a b. (a -> b) -> a -> b
$ (TERM f, Token) -> Chart (TERM f)
oneStep (TERM f
tNew, Token
varTok {tokPos :: Range
tokPos = f -> Range
forall a. GetRange a => a -> Range
getRange f
t})
              in [Diagnosis] -> Chart (TERM f) -> Chart (TERM f)
forall a. [Diagnosis] -> Chart a -> Chart a
mixDiags [Diagnosis]
mds Chart (TERM f)
c2
            _ -> [Char] -> Chart (TERM f)
forall a. HasCallStack => [Char] -> a
error "iterateCharts"

-- | construct 'IdSets' from op and pred identifiers
mkIdSets :: Set.Set Id -> Set.Set Id -> Set.Set Id -> IdSets
mkIdSets :: Set Id -> Set Id -> Set Id -> IdSets
mkIdSets consts :: Set Id
consts ops :: Set Id
ops preds :: Set Id
preds = ((Set Id
consts, Set Id
ops), Set Id
preds)

-- | top-level resolution like 'resolveMixTrm' that fails in case of diags
resolveMixfix :: FormExtension f => (f -> f)
              -> MixResolve f -> MixResolve (TERM f)
resolveMixfix :: (f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixfix par :: f -> f
par extR :: MixResolve f
extR g :: GlobalAnnos
g ruleS :: (TokRules, Rules)
ruleS t :: TERM f
t =
    let r :: Result (TERM f)
r@(Result ds :: [Diagnosis]
ds _) = (f -> f) -> MixResolve f -> MixResolve (TERM f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm f -> f
par MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ruleS TERM f
t
        in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then Result (TERM f)
r else [Diagnosis] -> Maybe (TERM f) -> Result (TERM f)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (TERM f)
forall a. Maybe a
Nothing

-- | basic term resolution that supports recursion without failure
resolveMixTrm :: FormExtension f => (f -> f)
              -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm :: (f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm par :: f -> f
par extR :: MixResolve f
extR ga :: GlobalAnnos
ga (adder :: TokRules
adder, ruleS :: Rules
ruleS) trm :: TERM f
trm =
    (TERM f -> ShowS)
-> Range -> ToExpr (TERM f) -> Chart (TERM f) -> Result (TERM f)
forall a. (a -> ShowS) -> Range -> ToExpr a -> Chart a -> Result a
getResolved ((f -> f) -> GlobalAnnos -> TERM f -> ShowS
forall f.
FormExtension f =>
(f -> f) -> GlobalAnnos -> TERM f -> ShowS
showTerm f -> f
par GlobalAnnos
ga) (TERM f -> Range
forall a. GetRange a => a -> Range
getRangeSpan TERM f
trm) ToExpr (TERM f)
forall f. GetRange f => Id -> [TERM f] -> Range -> TERM f
toAppl
           (Chart (TERM f) -> Result (TERM f))
-> Chart (TERM f) -> Result (TERM f)
forall a b. (a -> b) -> a -> b
$ (f -> f)
-> MixResolve f
-> GlobalAnnos
-> [TERM f]
-> Chart (TERM f)
-> Chart (TERM f)
forall f.
FormExtension f =>
(f -> f)
-> MixResolve f
-> GlobalAnnos
-> [TERM f]
-> Chart (TERM f)
-> Chart (TERM f)
iterateCharts f -> f
par MixResolve f
extR GlobalAnnos
ga [TERM f
trm] (Chart (TERM f) -> Chart (TERM f))
-> Chart (TERM f) -> Chart (TERM f)
forall a b. (a -> b) -> a -> b
$ TokRules -> Rules -> Chart (TERM f)
forall a. TokRules -> Rules -> Chart a
initChart TokRules
adder Rules
ruleS

showTerm :: FormExtension f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
showTerm :: (f -> f) -> GlobalAnnos -> TERM f -> ShowS
showTerm par :: f -> f
par ga :: GlobalAnnos
ga = GlobalAnnos -> TERM f -> ShowS
forall a. Pretty a => GlobalAnnos -> a -> ShowS
showGlobalDoc GlobalAnnos
ga (TERM f -> ShowS) -> (TERM f -> TERM f) -> TERM f -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> TERM f -> TERM f
forall f. (f -> f) -> TERM f -> TERM f
mapTerm f -> f
par

-- | top-level resolution like 'resolveMixFrm' that fails in case of diags
resolveFormula :: FormExtension f => (f -> f)
               -> MixResolve f -> MixResolve (FORMULA f)
resolveFormula :: (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveFormula par :: f -> f
par extR :: MixResolve f
extR g :: GlobalAnnos
g ruleS :: (TokRules, Rules)
ruleS f :: FORMULA f
f =
    let r :: Result (FORMULA f)
r@(Result ds :: [Diagnosis]
ds _) = (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm f -> f
par MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ruleS FORMULA f
f
        in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then Result (FORMULA f)
r else [Diagnosis] -> Maybe (FORMULA f) -> Result (FORMULA f)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (FORMULA f)
forall a. Maybe a
Nothing

varDeclTokens :: [VAR_DECL] -> Set.Set Token
varDeclTokens :: [VAR_DECL] -> Set Token
varDeclTokens = [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Token] -> Set Token)
-> ([VAR_DECL] -> [Set Token]) -> [VAR_DECL] -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR_DECL -> Set Token) -> [VAR_DECL] -> [Set Token]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Var_decl vs :: [Token]
vs _ _) -> [Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList [Token]
vs)

extendRules :: Set.Set Token -> (TokRules, Rules)
  -> (TokRules, Rules)
extendRules :: Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules ts :: Set Token
ts (f :: TokRules
f, rs :: Rules
rs) =
  (\ t :: Token
t -> let
     l :: Set Rule
l = TokRules
f Token
t
     r :: Rule
r = Id -> Rule
mkRule (Id -> Rule) -> Id -> Rule
forall a b. (a -> b) -> a -> b
$ [Token] -> Id
mkId [Token
t]
     in if Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
t Set Token
ts then Rule -> Set Rule -> Set Rule
forall a. Ord a => a -> Set a -> Set a
Set.insert Rule
r Set Rule
l else Set Rule
l, Rules
rs)

extendMixResolve :: Set.Set Token -> MixResolve f -> MixResolve f
extendMixResolve :: Set Token -> MixResolve f -> MixResolve f
extendMixResolve ts :: Set Token
ts f :: MixResolve f
f ga :: GlobalAnnos
ga = MixResolve f
f GlobalAnnos
ga ((TokRules, Rules) -> f -> Result f)
-> ((TokRules, Rules) -> (TokRules, Rules))
-> (TokRules, Rules)
-> f
-> Result f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules Set Token
ts

-- | basic formula resolution that supports recursion without failure
resolveMixFrm :: FormExtension f => (f -> f)
              -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm :: (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm par :: f -> f
par extR :: MixResolve f
extR g :: GlobalAnnos
g ids :: (TokRules, Rules)
ids frm :: FORMULA f
frm =
    let self :: FORMULA f -> Result (FORMULA f)
self = (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm f -> f
par MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ids
        resolveTerm :: TERM f -> Result (TERM f)
resolveTerm = (f -> f) -> MixResolve f -> MixResolve (TERM f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm f -> f
par MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ids in
    case FORMULA f
frm of
       Quantification q :: QUANTIFIER
q vs :: [VAR_DECL]
vs fOld :: FORMULA f
fOld ps :: Range
ps ->
           do let ts :: Set Token
ts = [VAR_DECL] -> Set Token
varDeclTokens [VAR_DECL]
vs
              FORMULA f
fNew <- (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm f -> f
par (Set Token -> MixResolve f -> MixResolve f
forall f. Set Token -> MixResolve f -> MixResolve f
extendMixResolve Set Token
ts MixResolve f
extR)
                GlobalAnnos
g (Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules Set Token
ts (TokRules, Rules)
ids) FORMULA f
fOld
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs FORMULA f
fNew Range
ps
       Junction j :: Junctor
j fsOld :: [FORMULA f]
fsOld ps :: Range
ps ->
           do [FORMULA f]
fsNew <- (FORMULA f -> Result (FORMULA f))
-> [FORMULA f] -> Result [FORMULA f]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FORMULA f -> Result (FORMULA f)
self [FORMULA f]
fsOld
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j [FORMULA f]
fsNew Range
ps
       Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 ps :: Range
ps ->
           do FORMULA f
f3 <- FORMULA f -> Result (FORMULA f)
self FORMULA f
f1
              FORMULA f
f4 <- FORMULA f -> Result (FORMULA f)
self FORMULA f
f2
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
f3 Relation
c FORMULA f
f4 Range
ps
       Negation fOld :: FORMULA f
fOld ps :: Range
ps ->
           do FORMULA f
fNew <- FORMULA f -> Result (FORMULA f)
self FORMULA f
fOld
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation FORMULA f
fNew Range
ps
       Predication sym :: PRED_SYMB
sym tsOld :: [TERM f]
tsOld ps :: Range
ps ->
           do [TERM f]
tsNew <- (TERM f -> Result (TERM f)) -> [TERM f] -> Result [TERM f]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TERM f -> Result (TERM f)
resolveTerm [TERM f]
tsOld
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
sym [TERM f]
tsNew Range
ps
       Definedness tOld :: TERM f
tOld ps :: Range
ps ->
           do TERM f
tNew <- TERM f -> Result (TERM f)
resolveTerm TERM f
tOld
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
tNew Range
ps
       Equation t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 ps :: Range
ps ->
           do TERM f
t3 <- TERM f -> Result (TERM f)
resolveTerm TERM f
t1
              TERM f
t4 <- TERM f -> Result (TERM f)
resolveTerm TERM f
t2
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
t3 Equality
e TERM f
t4 Range
ps
       Membership tOld :: TERM f
tOld s :: Id
s ps :: Range
ps ->
           do TERM f
tNew <- TERM f -> Result (TERM f)
resolveTerm TERM f
tOld
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> Id -> Range -> FORMULA f
forall f. TERM f -> Id -> Range -> FORMULA f
Membership TERM f
tNew Id
s Range
ps
       Mixfix_formula tOld :: TERM f
tOld ->
           do TERM f
tNew <- TERM f -> Result (TERM f)
resolveTerm TERM f
tOld
              case TERM f
tNew of
                 Application (Op_name ide :: Id
ide) args :: [TERM f]
args ps :: Range
ps ->
                     FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_SYMB
Pred_name Id
ide) [TERM f]
args Range
ps
                 Mixfix_qual_pred qide :: PRED_SYMB
qide ->
                     FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qide [] Range
nullRange
                 Mixfix_term [Mixfix_qual_pred qide :: PRED_SYMB
qide,
                              Mixfix_parenthesized ts :: [TERM f]
ts ps :: Range
ps] ->
                     FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qide [TERM f]
ts Range
ps
                 _ -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ TERM f -> FORMULA f
forall f. TERM f -> FORMULA f
Mixfix_formula TERM f
tNew
       QuantOp o :: Id
o t :: OP_TYPE
t fOld :: FORMULA f
fOld -> let
         ts :: Set Token
ts = if Id -> Bool
isSimpleId Id
o then Token -> Set Token
forall a. a -> Set a
Set.singleton (Token -> Set Token) -> Token -> Set Token
forall a b. (a -> b) -> a -> b
$ Id -> Token
idToSimpleId Id
o
              else Set Token
forall a. Set a
Set.empty
         in (FORMULA f -> FORMULA f)
-> Result (FORMULA f) -> Result (FORMULA f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Id -> OP_TYPE -> FORMULA f -> FORMULA f
forall f. Id -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp Id
o OP_TYPE
t)
            (Result (FORMULA f) -> Result (FORMULA f))
-> Result (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm f -> f
par (Set Token -> MixResolve f -> MixResolve f
forall f. Set Token -> MixResolve f -> MixResolve f
extendMixResolve Set Token
ts MixResolve f
extR)
              GlobalAnnos
g (Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules Set Token
ts (TokRules, Rules)
ids) FORMULA f
fOld
       QuantPred p :: Id
p t :: PRED_TYPE
t fOld :: FORMULA f
fOld -> let
         ts :: Set Token
ts = if Id -> Bool
isSimpleId Id
p then Token -> Set Token
forall a. a -> Set a
Set.singleton (Token -> Set Token) -> Token -> Set Token
forall a b. (a -> b) -> a -> b
$ Id -> Token
idToSimpleId Id
p
              else Set Token
forall a. Set a
Set.empty
         in (FORMULA f -> FORMULA f)
-> Result (FORMULA f) -> Result (FORMULA f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Id -> PRED_TYPE -> FORMULA f -> FORMULA f
forall f. Id -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred Id
p PRED_TYPE
t)
            (Result (FORMULA f) -> Result (FORMULA f))
-> Result (FORMULA f) -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ (f -> f) -> MixResolve f -> MixResolve (FORMULA f)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm f -> f
par (Set Token -> MixResolve f -> MixResolve f
forall f. Set Token -> MixResolve f -> MixResolve f
extendMixResolve Set Token
ts MixResolve f
extR)
              GlobalAnnos
g (Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules Set Token
ts (TokRules, Rules)
ids) FORMULA f
fOld
       ExtFORMULA f :: f
f ->
           do f
newF <- MixResolve f
extR GlobalAnnos
g (TokRules, Rules)
ids f
f
              FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA f -> Result (FORMULA f))
-> FORMULA f -> Result (FORMULA f)
forall a b. (a -> b) -> a -> b
$ f -> FORMULA f
forall f. f -> FORMULA f
ExtFORMULA f
newF
       f :: FORMULA f
f -> FORMULA f -> Result (FORMULA f)
forall (m :: * -> *) a. Monad m => a -> m a
return FORMULA f
f