{- |
Module      :  ./HasCASL/MixAna.hs
Description :  mixfix analysis for terms
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

Mixfix analysis of terms and patterns, type annotations are also analysed
-}

module HasCASL.MixAna
  ( resolve
  , anaPolyId
  , makeRules
  , getPolyIds
  , iterateCharts
  , toMixTerm
  , uTok
  ) where

import Common.AnnoParser
import Common.AnnoState
import Common.ConvertMixfixToken
import Common.DocUtils
import Common.Earley
import Common.GlobalAnnotations
import Common.Id
import Common.Lib.State
import Common.Parsec
import Common.Prec
import Common.Result

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

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.PrintAs
import HasCASL.VarDecl
import HasCASL.Le
import HasCASL.ParseTerm
import HasCASL.TypeAna

import qualified Text.ParserCombinators.Parsec as P

import Data.Maybe
import Control.Exception (assert)
import Control.Monad

addType :: Term -> Term -> Term
addType :: Term -> Term -> Term
addType (MixTypeTerm q :: TypeQual
q ty :: Type
ty ps :: Range
ps) t :: Term
t = Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
t TypeQual
q Type
ty Range
ps
addType _ _ = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error "addType"

-- | try to reparse terms as a compound list
isCompoundList :: Set.Set [Id] -> [Term] -> Bool
isCompoundList :: Set [Id] -> [Term] -> Bool
isCompoundList compIds :: Set [Id]
compIds =
    Bool -> ([Id] -> Bool) -> Maybe [Id] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ([Id] -> Set [Id] -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set [Id]
compIds) (Maybe [Id] -> Bool) -> ([Term] -> Maybe [Id]) -> [Term] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Maybe Id) -> [Term] -> Maybe [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Maybe Id
forall a. Pretty a => a -> Maybe Id
reparseAsId

isTypeList :: Env -> [Term] -> Bool
isTypeList :: Env -> [Term] -> Bool
isTypeList e :: Env
e l :: [Term]
l = case (Term -> Maybe Type) -> [Term] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Maybe Type
termToType [Term]
l of
    Nothing -> Bool
False
    Just ts :: [Type]
ts ->
        let Result ds :: [Diagnosis]
ds ml :: Maybe [((RawKind, Set Kind), Type)]
ml = (Type -> Result ((RawKind, Set Kind), Type))
-> [Type] -> Result [((RawKind, Set Kind), Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ t :: Type
t -> (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)
anaTypeM (Maybe Kind
forall a. Maybe a
Nothing, Type
t) Env
e) [Type]
ts
        in Maybe [((RawKind, Set Kind), Type)] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [((RawKind, Set Kind), Type)]
ml Bool -> Bool -> Bool
&& Bool -> Bool
not ([Diagnosis] -> Bool
hasErrors [Diagnosis]
ds)

termToType :: Term -> Maybe Type
termToType :: Term -> Maybe Type
termToType t :: Term
t = case GenParser Char (AnnoState ()) Type
-> AnnoState () -> [Char] -> [Char] -> Either ParseError Type
forall tok st a.
GenParser tok st a -> st -> [Char] -> [tok] -> Either ParseError a
P.runParser ((case Term -> [Pos]
forall a. GetRange a => a -> [Pos]
getPosList Term
t of
    [] -> () -> ParsecT [Char] (AnnoState ()) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    p :: Pos
p : _ -> SourcePos -> ParsecT [Char] (AnnoState ()) Identity ()
forall (m :: * -> *) s u. Monad m => SourcePos -> ParsecT s u m ()
P.setPosition (SourcePos -> ParsecT [Char] (AnnoState ()) Identity ())
-> SourcePos -> ParsecT [Char] (AnnoState ()) Identity ()
forall a b. (a -> b) -> a -> b
$ Pos -> SourcePos
fromPos Pos
p)
      ParsecT [Char] (AnnoState ()) Identity ()
-> GenParser Char (AnnoState ()) Type
-> GenParser Char (AnnoState ()) Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char (AnnoState ()) Type
forall st. AParser st Type
parseType GenParser Char (AnnoState ()) Type
-> ParsecT [Char] (AnnoState ()) Identity ()
-> GenParser Char (AnnoState ()) Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT [Char] (AnnoState ()) Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
P.eof) (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" ([Char] -> Either ParseError Type)
-> [Char] -> Either ParseError Type
forall a b. (a -> b) -> a -> b
$ Term -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Term
t "" of
    Right x :: Type
x -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
x
    _ -> Maybe Type
forall a. Maybe a
Nothing

anaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
anaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
anaPolyId (PolyId i :: Id
i@(Id _ cs :: [Id]
cs _) _ _) sc :: TypeScheme
sc = do
    Maybe TypeScheme
mSc <- TypeScheme -> State Env (Maybe TypeScheme)
anaTypeScheme TypeScheme
sc
    case Maybe TypeScheme
mSc of
      Nothing -> Maybe TypeScheme -> State Env (Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeScheme
forall a. Maybe a
Nothing
      Just newSc :: TypeScheme
newSc@(TypeScheme tvars :: [TypeArg]
tvars _ _) -> do
          Env
e <- State Env Env
forall s. State s s
get
          let ids :: Set Id
ids = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                [ Map Id ClassInfo -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id ClassInfo -> Set Id) -> Map Id ClassInfo -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id ClassInfo
classMap Env
e
                , Map Id TypeInfo -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id TypeInfo -> Set Id) -> Map Id TypeInfo -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeInfo
typeMap Env
e
                , Map Id (Set OpInfo) -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id (Set OpInfo) -> Set Id) -> Map Id (Set OpInfo) -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e ]
              es :: [Id]
es = (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Id -> Bool) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Set Id -> Bool) -> Set Id -> Id -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set Id
ids) [Id]
cs
          [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Id -> Diagnosis) -> [Id] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag (if [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
tvars then DiagKind
Hint else DiagKind
Warning)
            "unexpected identifier in compound list") [Id]
es
          Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
cs Bool -> Bool -> Bool
|| [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
tvars)
            (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "is polymorphic compound identifier" Id
i]
          Maybe TypeScheme -> State Env (Maybe TypeScheme)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TypeScheme -> State Env (Maybe TypeScheme))
-> Maybe TypeScheme -> State Env (Maybe TypeScheme)
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Maybe TypeScheme
forall a. a -> Maybe a
Just TypeScheme
newSc

resolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme
resolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme
resolveQualOp i :: PolyId
i@(PolyId j :: Id
j _ _) sc :: TypeScheme
sc = do
    Maybe TypeScheme
mSc <- PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
anaPolyId PolyId
i TypeScheme
sc
    Env
e <- State Env Env
forall s. State s s
get
    case Maybe TypeScheme
mSc of
      Nothing -> TypeScheme -> State Env TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return TypeScheme
sc -- and previous
      Just nSc :: TypeScheme
nSc -> do
        Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set OpInfo -> Bool
forall a. Set a -> Bool
Set.null (Set OpInfo -> Bool) -> Set OpInfo -> Bool
forall a b. (a -> b) -> a -> b
$ (OpInfo -> Bool) -> Set OpInfo -> Set OpInfo
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((TypeScheme -> TypeScheme -> Bool
forall a. Eq a => a -> a -> Bool
== TypeScheme
nSc) (TypeScheme -> Bool) -> (OpInfo -> TypeScheme) -> OpInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpInfo -> TypeScheme
opType)
                  (Set OpInfo -> Set OpInfo) -> Set OpInfo -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> Id -> Map Id (Set OpInfo) -> Set OpInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set OpInfo
forall a. Set a
Set.empty Id
j (Map Id (Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo) -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e)
          (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Error "operation not found" Id
j]
        TypeScheme -> State Env TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return TypeScheme
nSc

iterateCharts :: GlobalAnnos -> Set.Set Id -> Set.Set [Id] -> [Term]
              -> Chart Term -> State Env (Chart Term)
iterateCharts :: GlobalAnnos
-> Set Id
-> Set [Id]
-> [Term]
-> Chart Term
-> State Env (Chart Term)
iterateCharts ga :: GlobalAnnos
ga sIds :: Set Id
sIds compIds :: Set [Id]
compIds terms :: [Term]
terms chart :: Chart Term
chart = do
    Env
e <- State Env Env
forall s. State s s
get
    let self :: [Term] -> Chart Term -> State Env (Chart Term)
self = GlobalAnnos
-> Set Id
-> Set [Id]
-> [Term]
-> Chart Term
-> State Env (Chart Term)
iterateCharts GlobalAnnos
ga Set Id
sIds Set [Id]
compIds
        oneStep :: (Term, Token) -> Chart Term
oneStep = (Term -> Term -> Term)
-> ToExpr Term
-> GlobalAnnos
-> Chart Term
-> (Term, Token)
-> Chart Term
forall a.
(a -> a -> a)
-> ToExpr a -> GlobalAnnos -> Chart a -> (a, Token) -> Chart a
nextChart Term -> Term -> Term
addType (Env -> ToExpr Term
toMixTerm Env
e) GlobalAnnos
ga Chart Term
chart
        vs :: Map Id VarDefn
vs = Env -> Map Id VarDefn
localVars Env
e
        tm :: Map Id TypeInfo
tm = Env -> Map Id TypeInfo
typeMap Env
e
    case [Term]
terms of
      [] -> Chart Term -> State Env (Chart Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Chart Term
chart
      t :: Term
t : tt :: [Term]
tt -> let recurse :: Term -> State Env (Chart Term)
recurse trm :: Term
trm = [Term] -> Chart Term -> State Env (Chart Term)
self [Term]
tt (Chart Term -> State Env (Chart Term))
-> Chart Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ (Term, Token) -> Chart Term
oneStep
                      (Term
trm, Token
exprTok {tokPos :: Range
tokPos = Term -> Range
forall a. GetRange a => a -> Range
getRange Term
trm}) in case Term
t of
        MixfixTerm ts :: [Term]
ts -> [Term] -> Chart Term -> State Env (Chart Term)
self ([Term]
ts [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
tt) Chart Term
chart
        MixTypeTerm q :: TypeQual
q typ :: Type
typ ps :: Range
ps -> do
          Maybe Type
mTyp <- Type -> State Env (Maybe Type)
anaStarType Type
typ
          case Maybe Type
mTyp of
            Nothing -> Term -> State Env (Chart Term)
recurse Term
t
            Just nTyp :: Type
nTyp -> [Term] -> Chart Term -> State Env (Chart Term)
self [Term]
tt (Chart Term -> State Env (Chart Term))
-> Chart Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ (Term, Token) -> Chart Term
oneStep
                (TypeQual -> Type -> Range -> Term
MixTypeTerm TypeQual
q (Type -> Type
monoType Type
nTyp) Range
ps, Token
typeTok {tokPos :: Range
tokPos = Range
ps})
        BracketTerm b :: BracketKind
b ts :: [Term]
ts ps :: Range
ps ->
          let bres :: State Env (Chart Term)
bres = [Term] -> Chart Term -> State Env (Chart Term)
self ((Token -> Term) -> ([Char], [Char]) -> [Term] -> Range -> [Term]
forall a. (Token -> a) -> ([Char], [Char]) -> [a] -> Range -> [a]
expandPos Token -> Term
TermToken
                (BracketKind -> ([Char], [Char])
getBrackets BracketKind
b) [Term]
ts Range
ps [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
tt) Chart Term
chart in case (BracketKind
b, [Term]
ts, [Term]
tt) of
          (Squares, _ : _, _)
            | Set [Id] -> [Term] -> Bool
isCompoundList Set [Id]
compIds [Term]
ts -> do
              [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "is compound list" Term
t]
              State Env (Chart Term)
bres
            | Env -> [Term] -> Bool
isTypeList Env
e [Term]
ts -> do
              let testChart :: Chart Term
testChart = (Term, Token) -> Chart Term
oneStep (Term
t, Token
typeInstTok {tokPos :: Range
tokPos = Range
ps})
              if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Diagnosis] -> Bool) -> [Diagnosis] -> Bool
forall a b. (a -> b) -> a -> b
$ Chart Term -> [Diagnosis]
forall a. Chart a -> [Diagnosis]
solveDiags Chart Term
testChart then do
                [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "is type list" Term
t]
                [Term] -> Chart Term -> State Env (Chart Term)
self [Term]
tt Chart Term
testChart
                else State Env (Chart Term)
bres
          (Parens, [QualOp b2 :: OpBrand
b2 v :: PolyId
v sc :: TypeScheme
sc [] _ ps2 :: Range
ps2], hd :: Term
hd@(BracketTerm Squares
                   ts2 :: [Term]
ts2@(_ : _) ps3 :: Range
ps3) : rtt :: [Term]
rtt)
            | Env -> [Term] -> Bool
isTypeList Env
e [Term]
ts2 -> do
                   [Diagnosis] -> State Env ()
addDiags [DiagKind -> [Char] -> [Term] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Hint "is type list" [Term]
ts2]
                   TypeScheme
nSc <- PolyId -> TypeScheme -> State Env TypeScheme
resolveQualOp PolyId
v TypeScheme
sc
                   [Term] -> Chart Term -> State Env (Chart Term)
self [Term]
rtt (Chart Term -> State Env (Chart Term))
-> Chart Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ (Term, Token) -> Chart Term
oneStep
                     ( OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
b2 PolyId
v TypeScheme
nSc (Env -> Term -> [Type]
bracketTermToTypes Env
e Term
hd) InstKind
UserGiven Range
ps2
                     , Token
exprTok {tokPos :: Range
tokPos = Range -> Range -> Range
appRange Range
ps Range
ps3})
          _ -> State Env (Chart Term)
bres
        QualVar (VarDecl v :: Id
v typ :: Type
typ ok :: SeparatorKind
ok ps :: Range
ps) -> do
          Maybe Type
mTyp <- Type -> State Env (Maybe Type)
anaStarType Type
typ
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ Term -> (Type -> Term) -> Maybe Type -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
t ( \ nType :: Type
nType -> VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
v (Type -> Type
monoType Type
nType)
            SeparatorKind
ok Range
ps) Maybe Type
mTyp
        QualOp b :: OpBrand
b v :: PolyId
v sc :: TypeScheme
sc [] k :: InstKind
k ps :: Range
ps -> do
          TypeScheme
nSc <- PolyId -> TypeScheme -> State Env TypeScheme
resolveQualOp PolyId
v TypeScheme
sc
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
b PolyId
v TypeScheme
nSc [] InstKind
k Range
ps
        QuantifiedTerm quant :: Quantifier
quant decls :: [GenVarDecl]
decls hd :: Term
hd ps :: Range
ps -> do
          [Maybe GenVarDecl]
newDs <- (GenVarDecl -> State Env (Maybe GenVarDecl))
-> [GenVarDecl] -> State Env [Maybe GenVarDecl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
anaddGenVarDecl Bool
False) [GenVarDecl]
decls
          Maybe Term
mt <- Term -> State Env (Maybe Term)
resolve Term
hd
          Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
          Map Id TypeInfo -> State Env ()
putTypeMap Map Id TypeInfo
tm
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
quant ([Maybe GenVarDecl] -> [GenVarDecl]
forall a. [Maybe a] -> [a]
catMaybes [Maybe GenVarDecl]
newDs) (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
hd Maybe Term
mt) Range
ps
        LambdaTerm decls :: [Term]
decls part :: Partiality
part hd :: Term
hd ps :: Range
ps -> do
          [Maybe Term]
mDecls <- (Term -> State Env (Maybe Term))
-> [Term] -> State Env [Maybe Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> State Env (Maybe Term)
resolve [Term]
decls
          let anaDecls :: [Term]
anaDecls = [Maybe Term] -> [Term]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Term]
mDecls
              bs :: [VarDecl]
bs = (Term -> [VarDecl]) -> [Term] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarDecl]
extractVars [Term]
anaDecls
          [VarDecl] -> State Env ()
checkUniqueVars [VarDecl]
bs
          (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
False) [VarDecl]
bs
          Maybe Term
mt <- Term -> State Env (Maybe Term)
resolve Term
hd
          Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm [Term]
anaDecls Partiality
part (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
hd Maybe Term
mt) Range
ps
        CaseTerm hd :: Term
hd eqs :: [ProgEq]
eqs ps :: Range
ps -> do
          Maybe Term
mt <- Term -> State Env (Maybe Term)
resolve Term
hd
          [ProgEq]
newEs <- [ProgEq] -> State Env [ProgEq]
resolveCaseEqs [ProgEq]
eqs
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ Term -> [ProgEq] -> Range -> Term
CaseTerm (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
hd Maybe Term
mt) [ProgEq]
newEs Range
ps
        LetTerm b :: LetBrand
b eqs :: [ProgEq]
eqs hd :: Term
hd ps :: Range
ps -> do
          [ProgEq]
newEs <- [ProgEq] -> State Env [ProgEq]
resolveLetEqs [ProgEq]
eqs
          Maybe Term
mt <- Term -> State Env (Maybe Term)
resolve Term
hd
          Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
b [ProgEq]
newEs (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
hd Maybe Term
mt) Range
ps
        TermToken tok :: Token
tok -> do
          let (ds1 :: [Diagnosis]
ds1, trm :: Term
trm) = LiteralAnnos
-> ToExpr Term -> (Token -> Term) -> Token -> ([Diagnosis], Term)
forall a.
LiteralAnnos
-> AsAppl a -> (Token -> a) -> Token -> ([Diagnosis], a)
convertMixfixToken (GlobalAnnos -> LiteralAnnos
literal_annos GlobalAnnos
ga)
                ((Id -> [Type] -> [Term] -> Range -> Term) -> [Type] -> ToExpr Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm []) Token -> Term
TermToken Token
tok
          [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds1
          [Term] -> Chart Term -> State Env (Chart Term)
self [Term]
tt (Chart Term -> State Env (Chart Term))
-> Chart Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ (Term, Token) -> Chart Term
oneStep ((Term, Token) -> Chart Term) -> (Term, Token) -> Chart Term
forall a b. (a -> b) -> a -> b
$ case Term
trm of
            TermToken _ -> (Term
trm, Token
tok)
            _ -> (Term
trm, Token
exprTok {tokPos :: Range
tokPos = Token -> Range
tokPos Token
tok})
        AsPattern vd :: VarDecl
vd p :: Term
p ps :: Range
ps -> do
          Maybe Term
mp <- Term -> State Env (Maybe Term)
resolve Term
p
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term -> Range -> Term
AsPattern VarDecl
vd (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
p Maybe Term
mp) Range
ps
        TypedTerm trm :: Term
trm k :: TypeQual
k ty :: Type
ty ps :: Range
ps -> do
          -- assume that type is analysed
          Maybe Term
mt <- Term -> State Env (Maybe Term)
resolve Term
trm
          Term -> State Env (Chart Term)
recurse (Term -> State Env (Chart Term)) -> Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ Term -> TypeQual -> Type -> Range -> Term
TypedTerm (Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
trm Maybe Term
mt) TypeQual
k Type
ty Range
ps
        _ -> [Char] -> State Env (Chart Term)
forall a. HasCallStack => [Char] -> a
error ("iterCharts: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Show a => a -> [Char]
show Term
t)

-- * equation stuff
resolveCaseEq :: ProgEq -> State Env (Maybe ProgEq)
resolveCaseEq :: ProgEq -> State Env (Maybe ProgEq)
resolveCaseEq (ProgEq p :: Term
p t :: Term
t ps :: Range
ps) = do
    Maybe Term
mp <- Term -> State Env (Maybe Term)
resolve Term
p
    case Maybe Term
mp of
      Nothing -> Maybe ProgEq -> State Env (Maybe ProgEq)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProgEq
forall a. Maybe a
Nothing
      Just newP :: Term
newP -> do
        let bs :: [VarDecl]
bs = Term -> [VarDecl]
extractVars Term
newP
        [VarDecl] -> State Env ()
checkUniqueVars [VarDecl]
bs
        Map Id VarDefn
vs <- (Env -> Map Id VarDefn) -> State Env (Map Id VarDefn)
forall s a. (s -> a) -> State s a
gets Env -> Map Id VarDefn
localVars
        (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
False) [VarDecl]
bs
        Maybe Term
mtt <- Term -> State Env (Maybe Term)
resolve Term
t
        Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
        Maybe ProgEq -> State Env (Maybe ProgEq)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ProgEq -> State Env (Maybe ProgEq))
-> Maybe ProgEq -> State Env (Maybe ProgEq)
forall a b. (a -> b) -> a -> b
$ case Maybe Term
mtt of
          Nothing -> Maybe ProgEq
forall a. Maybe a
Nothing
          Just newT :: Term
newT -> ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just (ProgEq -> Maybe ProgEq) -> ProgEq -> Maybe ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
newP Term
newT Range
ps

resolveCaseEqs :: [ProgEq] -> State Env [ProgEq]
resolveCaseEqs :: [ProgEq] -> State Env [ProgEq]
resolveCaseEqs eqs :: [ProgEq]
eqs = case [ProgEq]
eqs of
    [] -> [ProgEq] -> State Env [ProgEq]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    eq :: ProgEq
eq : rt :: [ProgEq]
rt -> do
      Maybe ProgEq
mEq <- ProgEq -> State Env (Maybe ProgEq)
resolveCaseEq ProgEq
eq
      [ProgEq]
reqs <- [ProgEq] -> State Env [ProgEq]
resolveCaseEqs [ProgEq]
rt
      [ProgEq] -> State Env [ProgEq]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgEq] -> State Env [ProgEq]) -> [ProgEq] -> State Env [ProgEq]
forall a b. (a -> b) -> a -> b
$ case Maybe ProgEq
mEq of
        Nothing -> [ProgEq]
reqs
        Just newEq :: ProgEq
newEq -> ProgEq
newEq ProgEq -> [ProgEq] -> [ProgEq]
forall a. a -> [a] -> [a]
: [ProgEq]
reqs

resolveLetEqs :: [ProgEq] -> State Env [ProgEq]
resolveLetEqs :: [ProgEq] -> State Env [ProgEq]
resolveLetEqs eqs :: [ProgEq]
eqs = case [ProgEq]
eqs of
    [] -> [ProgEq] -> State Env [ProgEq]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    ProgEq pat :: Term
pat trm :: Term
trm ps :: Range
ps : rt :: [ProgEq]
rt -> do
      Maybe Term
mPat <- Term -> State Env (Maybe Term)
resolve Term
pat
      case Maybe Term
mPat of
        Nothing -> do
          Term -> State Env (Maybe Term)
resolve Term
trm
          [ProgEq] -> State Env [ProgEq]
resolveLetEqs [ProgEq]
rt
        Just newPat :: Term
newPat -> do
          let bs :: [VarDecl]
bs = Term -> [VarDecl]
extractVars Term
newPat
          [VarDecl] -> State Env ()
checkUniqueVars [VarDecl]
bs
          (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
False) [VarDecl]
bs
          Maybe Term
mTrm <- Term -> State Env (Maybe Term)
resolve Term
trm
          case Maybe Term
mTrm of
            Nothing -> [ProgEq] -> State Env [ProgEq]
resolveLetEqs [ProgEq]
rt
            Just newTrm :: Term
newTrm -> do
              [ProgEq]
reqs <- [ProgEq] -> State Env [ProgEq]
resolveLetEqs [ProgEq]
rt
              [ProgEq] -> State Env [ProgEq]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProgEq] -> State Env [ProgEq]) -> [ProgEq] -> State Env [ProgEq]
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
newPat Term
newTrm Range
ps ProgEq -> [ProgEq] -> [ProgEq]
forall a. a -> [a] -> [a]
: [ProgEq]
reqs

mkPatAppl :: Term -> Term -> Range -> Term
mkPatAppl :: Term -> Term -> Range -> Term
mkPatAppl op :: Term
op arg :: Term
arg qs :: Range
qs = case Term
op of
    QualVar (VarDecl i :: Id
i (MixfixType []) _ _) -> Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
i [] [Term
arg] Range
qs
    _ -> Term -> Term -> Range -> Term
ApplTerm Term
op Term
arg Range
qs

bracketTermToTypes :: Env -> Term -> [Type]
bracketTermToTypes :: Env -> Term -> [Type]
bracketTermToTypes e :: Env
e t :: Term
t = case Term
t of
    BracketTerm Squares tys :: [Term]
tys _ ->
      (((RawKind, Set Kind), Type) -> Type)
-> [((RawKind, Set Kind), Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
monoType (Type -> Type)
-> (((RawKind, Set Kind), Type) -> Type)
-> ((RawKind, Set Kind), Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((RawKind, Set Kind), Type) -> Type
forall a b. (a, b) -> b
snd) ([((RawKind, Set Kind), Type)] -> [Type])
-> [((RawKind, Set Kind), Type)] -> [Type]
forall a b. (a -> b) -> a -> b
$ [((RawKind, Set Kind), Type)]
-> Maybe [((RawKind, Set Kind), Type)]
-> [((RawKind, Set Kind), Type)]
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> [((RawKind, Set Kind), Type)]
forall a. HasCallStack => [Char] -> a
error "bracketTermToTypes")
      (Maybe [((RawKind, Set Kind), Type)]
 -> [((RawKind, Set Kind), Type)])
-> Maybe [((RawKind, Set Kind), Type)]
-> [((RawKind, Set Kind), Type)]
forall a b. (a -> b) -> a -> b
$ Result [((RawKind, Set Kind), Type)]
-> Maybe [((RawKind, Set Kind), Type)]
forall a. Result a -> Maybe a
maybeResult (Result [((RawKind, Set Kind), Type)]
 -> Maybe [((RawKind, Set Kind), Type)])
-> Result [((RawKind, Set Kind), Type)]
-> Maybe [((RawKind, Set Kind), Type)]
forall a b. (a -> b) -> a -> b
$ (Type -> Result ((RawKind, Set Kind), Type))
-> [Type] -> Result [((RawKind, Set Kind), Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ( \ ty :: Type
ty -> (Maybe Kind, Type) -> Env -> Result ((RawKind, Set Kind), Type)
anaTypeM (Maybe Kind
forall a. Maybe a
Nothing, Type
ty) Env
e)
      ([Type] -> Result [((RawKind, Set Kind), Type)])
-> [Type] -> Result [((RawKind, Set Kind), Type)]
forall a b. (a -> b) -> a -> b
$ [Type] -> Maybe [Type] -> [Type]
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> [Type]
forall a. HasCallStack => [Char] -> a
error "bracketTermToTypes1") (Maybe [Type] -> [Type]) -> Maybe [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Term -> Maybe Type) -> [Term] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Maybe Type
termToType [Term]
tys
    _ -> [Char] -> [Type]
forall a. HasCallStack => [Char] -> a
error "bracketTermToTypes2"

toMixTerm :: Env -> Id -> [Term] -> Range -> Term
toMixTerm :: Env -> ToExpr Term
toMixTerm e :: Env
e i :: Id
i ar :: [Term]
ar qs :: Range
qs
  | Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
applId = Bool -> Term -> Term
forall a. HasCallStack => Bool -> a -> a
assert ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ar Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
           let [op :: Term
op, arg :: Term
arg] = [Term]
ar in Term -> Term -> Range -> Term
mkPatAppl Term
op Term
arg Range
qs
  | Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i [Id
tupleId, Id
unitId] = [Term] -> Range -> Term
mkTupleTerm [Term]
ar Range
qs
  | Bool
otherwise = case Id -> Maybe Id
unPolyId Id
i of
      Just j :: Id
j@(Id ts :: [Token]
ts _ _) -> if Id -> Bool
isMixfix Id
j Bool -> Bool -> Bool
&& [Term] -> Bool
forall a. [a] -> Bool
isSingle [Term]
ar then
          Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
j (Env -> Term -> [Type]
bracketTermToTypes Env
e (Term -> [Type]) -> Term -> [Type]
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
forall a. [a] -> a
head [Term]
ar) [] Range
qs
        else Bool -> Term -> Term
forall a. HasCallStack => Bool -> a -> a
assert ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ar Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Id -> Int
placeCount Id
j) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
        let (far :: [Term]
far, tar :: Term
tar : sar :: [Term]
sar) =
                Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt (Id -> Int
placeCount (Id -> Int) -> Id -> Int
forall a b. (a -> b) -> a -> b
$ [Token] -> Id
mkId ([Token] -> Id) -> [Token] -> Id
forall a b. (a -> b) -> a -> b
$ ([Token], [Token]) -> [Token]
forall a b. (a, b) -> a
fst (([Token], [Token]) -> [Token]) -> ([Token], [Token]) -> [Token]
forall a b. (a -> b) -> a -> b
$ [Token] -> ([Token], [Token])
splitMixToken [Token]
ts) [Term]
ar
        in Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
j (Env -> Term -> [Type]
bracketTermToTypes Env
e Term
tar) ([Term]
far [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
sar) Range
qs
      _ -> Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
i [] [Term]
ar Range
qs

getKnowns :: Id -> Set.Set Token
getKnowns :: Id -> Set Token
getKnowns (Id ts :: [Token]
ts cs :: [Id]
cs _) =
    Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([Token] -> Set Token
forall a. Ord a => [a] -> Set a
Set.fromList [Token]
ts) (Set Token -> Set Token) -> Set Token -> Set Token
forall a b. (a -> b) -> a -> b
$ [Set Token] -> Set Token
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Token] -> Set Token) -> [Set Token] -> Set Token
forall a b. (a -> b) -> a -> b
$ (Id -> Set Token) -> [Id] -> [Set Token]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Set Token
getKnowns [Id]
cs

resolve :: Term -> State Env (Maybe Term)
resolve :: Term -> State Env (Maybe Term)
resolve trm :: Term
trm = do
    Env
e <- State Env Env
forall s. State s s
get
    let ass :: Map Id (Set OpInfo)
ass = Env -> Map Id (Set OpInfo)
assumps Env
e
        ga :: GlobalAnnos
ga = Env -> GlobalAnnos
globAnnos Env
e
        (addRule :: TokRules
addRule, ruleS :: Rules
ruleS, sIds :: Set Id
sIds) = GlobalAnnos
-> (PrecMap, Set Id)
-> Set Id
-> Set Id
-> (TokRules, Rules, Set Id)
makeRules GlobalAnnos
ga (Env -> (PrecMap, Set Id)
preIds Env
e) (Map Id (Set OpInfo) -> Set Id
getPolyIds Map Id (Set OpInfo)
ass)
                 (Set Id -> (TokRules, Rules, Set Id))
-> Set Id -> (TokRules, Rules, 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 (Map Id Id -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id Id -> Set Id) -> Map Id Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id Id
binders Env
e)
                 (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 (Map Id (Set OpInfo) -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Map Id (Set OpInfo)
ass)
                 (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Map Id VarDefn -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id VarDefn -> Set Id) -> Map Id VarDefn -> Set Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id VarDefn
localVars Env
e
    Chart Term
chart <- GlobalAnnos
-> Set Id
-> Set [Id]
-> [Term]
-> Chart Term
-> State Env (Chart Term)
iterateCharts GlobalAnnos
ga Set Id
sIds (Env -> Set [Id]
getCompoundLists Env
e) [Term
trm]
      (Chart Term -> State Env (Chart Term))
-> Chart Term -> State Env (Chart Term)
forall a b. (a -> b) -> a -> b
$ TokRules -> Rules -> Chart Term
forall a. TokRules -> Rules -> Chart a
initChart TokRules
addRule Rules
ruleS
    let Result ds :: [Diagnosis]
ds mr :: Maybe Term
mr = (Term -> ShowS)
-> Range -> ToExpr Term -> Chart Term -> Result Term
forall a. (a -> ShowS) -> Range -> ToExpr a -> Chart a -> Result a
getResolved (Term -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (Term -> ShowS) -> (Term -> Term) -> Term -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
parenTerm) (Term -> Range
forall a. GetRange a => a -> Range
getRange Term
trm)
          (Env -> ToExpr Term
toMixTerm Env
e) Chart Term
chart
    [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
    Maybe Term -> State Env (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
mr

getPolyIds :: Assumps -> Set.Set Id
getPolyIds :: Map Id (Set OpInfo) -> Set Id
getPolyIds = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id)
-> (Map Id (Set OpInfo) -> [Set Id])
-> Map Id (Set OpInfo)
-> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Id, Set OpInfo) -> Set Id) -> [(Id, Set OpInfo)] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, s :: Set OpInfo
s) ->
     (OpInfo -> Set Id -> Set Id) -> Set Id -> Set OpInfo -> Set Id
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ oi :: OpInfo
oi -> case OpInfo -> TypeScheme
opType OpInfo
oi of
       TypeScheme (_ : _) _ _ -> Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
i
       _ -> Set Id -> Set Id
forall a. a -> a
id) Set Id
forall a. Set a
Set.empty Set OpInfo
s) ([(Id, Set OpInfo)] -> [Set Id])
-> (Map Id (Set OpInfo) -> [(Id, Set OpInfo)])
-> Map Id (Set OpInfo)
-> [Set Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id (Set OpInfo) -> [(Id, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList

uTok :: Token
uTok :: Token
uTok = [Char] -> Token
mkSimpleId "_"

builtinIds :: [Id]
builtinIds :: [Id]
builtinIds = [Id
unitId, Id
parenId, Id
tupleId, Id
exprId, Id
typeId, Id
applId]

makeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
          -> Set.Set Id -> (TokRules, Rules, Set.Set Id)
makeRules :: GlobalAnnos
-> (PrecMap, Set Id)
-> Set Id
-> Set Id
-> (TokRules, Rules, Set Id)
makeRules ga :: GlobalAnnos
ga ps :: (PrecMap, Set Id)
ps@(p :: PrecMap
p, _) polyIds :: Set Id
polyIds aIds :: Set Id
aIds =
    let (sIds :: Set Id
sIds, ids :: Set Id
ids) = (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
aIds
        ks :: Set Token
ks = (Id -> Set Token -> Set Token) -> Set Token -> Set Id -> Set Token
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set Token -> Set Token -> Set Token)
-> (Id -> Set Token) -> Id -> Set Token -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Set Token
getKnowns) Set Token
forall a. Set a
Set.empty Set Id
ids
        rIds :: Set Id
rIds = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
ids (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.intersection Set Id
sIds (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ (Token -> Id) -> Set Token -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Token -> Id
simpleIdToId Set Token
ks
        m2 :: Int
m2 = PrecMap -> Int
maxWeight PrecMap
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 2
    in ( \ tok :: Token
tok -> if Token -> Bool
isSimpleToken Token
tok Bool -> Bool -> Bool
&& Bool -> Bool
not (Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
tok Set Token
ks)
                  Bool -> Bool -> Bool
|| Token
tok Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
uTok
         then (Id, Int, [Token]) -> Set (Id, Int, [Token])
forall a. a -> Set a
Set.singleton (Token -> Id
simpleIdToId Token
tok, Int
m2, [Token
tok])
         else Set (Id, Int, [Token])
forall a. Set a
Set.empty
       , [(Id, Int, [Token])] -> Rules
partitionRules ([(Id, Int, [Token])] -> Rules) -> [(Id, Int, [Token])] -> Rules
forall a b. (a -> b) -> a -> b
$ Int -> GlobalAnnos -> [(Id, Int, [Token])]
listRules Int
m2 GlobalAnnos
ga [(Id, Int, [Token])]
-> [(Id, Int, [Token])] -> [(Id, Int, [Token])]
forall a. [a] -> [a] -> [a]
++
             (PrecMap, Set Id) -> [Id] -> [Id] -> [Id] -> [(Id, Int, [Token])]
initRules (PrecMap, Set Id)
ps (Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
polyIds) [Id]
builtinIds (Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
rIds)
       , Set Id
sIds)

initRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]
initRules :: (PrecMap, Set Id) -> [Id] -> [Id] -> [Id] -> [(Id, Int, [Token])]
initRules (p :: PrecMap
p, ps :: Set Id
ps) polyIds :: [Id]
polyIds bs :: [Id]
bs is :: [Id]
is =
    (Id -> (Id, Int, [Token])) -> [Id] -> [(Id, Int, [Token])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> Int -> Id -> (Id, Int, [Token])
mixRule (PrecMap -> Set Id -> Id -> Int
getIdPrec PrecMap
p Set Id
ps Id
i) Id
i)
            ([Id]
bs [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id]
is) [(Id, Int, [Token])]
-> [(Id, Int, [Token])] -> [(Id, Int, [Token])]
forall a. [a] -> [a] -> [a]
++
    (Id -> (Id, Int, [Token])) -> [Id] -> [(Id, Int, [Token])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> (Id -> Id
protect Id
i, PrecMap -> Int
maxWeight PrecMap
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 3, Id -> [Token]
getPlainTokenList Id
i))
            ((Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter Id -> Bool
isMixfix [Id]
is) [(Id, Int, [Token])]
-> [(Id, Int, [Token])] -> [(Id, Int, [Token])]
forall a. [a] -> [a] -> [a]
++
-- identifiers with a positive number of type arguments
    (Id -> (Id, Int, [Token])) -> [Id] -> [(Id, Int, [Token])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> ( Id -> Id
polyId Id
i, PrecMap -> Set Id -> Id -> Int
getIdPrec PrecMap
p Set Id
ps Id
i
                 , Id -> [Token]
getPolyTokenList Id
i)) [Id]
polyIds [(Id, Int, [Token])]
-> [(Id, Int, [Token])] -> [(Id, Int, [Token])]
forall a. [a] -> [a] -> [a]
++
    (Id -> (Id, Int, [Token])) -> [Id] -> [(Id, Int, [Token])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> ( Id -> Id
protect (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$ Id -> Id
polyId Id
i, PrecMap -> Int
maxWeight PrecMap
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 3
                 , Id -> [Token]
getPlainPolyTokenList Id
i)) ((Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter Id -> Bool
isMixfix [Id]
polyIds)