{- |
Module      :  ./HasCASL/OpDecl.hs
Description :  analyse operation declarations
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

analyse operation declarations
-}

module HasCASL.OpDecl
  ( anaOpItem
  , anaProgEq
  , mkEnvForall
  ) where

import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import Text.ParserCombinators.Parsec (parse, eof)
import Control.Monad

import Common.Id
import Common.Lib.State as State
import Common.Result
import Common.GlobalAnnotations
import Common.AS_Annotation
import Common.Doc
import Common.Lexer (skip)
import Common.Parsec

import HasCASL.As
import HasCASL.HToken
import HasCASL.TypeAna
import HasCASL.VarDecl
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.AsUtils
import HasCASL.MixAna
import HasCASL.TypeCheck
import HasCASL.ProgEq
import HasCASL.Unify

anaAttr :: TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
anaAttr :: TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
anaAttr (TypeScheme tvs :: [TypeArg]
tvs ty :: Type
ty _) b :: OpAttr
b = case OpAttr
b of
    UnitOpAttr trm :: Term
trm ps :: Range
ps -> do
       Env
e <- State Env Env
forall s. State s s
get
       let mTy :: Maybe (Type, Type, Type)
mTy = let (fty :: Type
fty, fArgs :: [Type]
fArgs) = Type -> (Type, [Type])
getTypeAppl Type
ty in case [Type]
fArgs of
                   [arg :: Type
arg, t3 :: Type
t3] | Env -> Type -> Type -> Bool
lesserType Env
e Type
fty (Arrow -> Type
toFunType Arrow
PFunArr)
                       -> let (pty :: Type
pty, ts :: [Type]
ts) = Type -> (Type, [Type])
getTypeAppl Type
arg in case [Type]
ts of
                          [t1 :: Type
t1, t2 :: Type
t2] | Env -> Type -> Type -> Bool
lesserType Env
e Type
pty (Int -> Range -> Type
toProdType 2 Range
ps)
                                       -> (Type, Type, Type) -> Maybe (Type, Type, Type)
forall a. a -> Maybe a
Just (Type
t1, Type
t2, Type
t3)
                          _ -> Maybe (Type, Type, Type)
forall a. Maybe a
Nothing
                   _ -> Maybe (Type, Type, Type)
forall a. Maybe a
Nothing
       let tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
e
       (TypeArg -> State Env ()) -> [TypeArg] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> TypeArg -> State Env ()
addTypeVarDecl Bool
False) [TypeArg]
tvs
       case Maybe (Type, Type, Type)
mTy of
             Nothing -> do [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                                     "unexpected type of operation" Type
ty]
                           TypeMap -> State Env ()
putTypeMap TypeMap
tm
                           Maybe OpAttr -> State Env (Maybe OpAttr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe OpAttr
forall a. Maybe a
Nothing
             Just (t1 :: Type
t1, t2 :: Type
t2, t3 :: Type
t3) ->
                 do Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 Bool -> Bool -> Bool
&& Type
t2 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t3)
                      (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                                 "unexpected type components of operation" Type
ty]
                    Maybe Term
mt <- Type -> Term -> State Env (Maybe Term)
resolveTerm Type
t3 Term
trm
                    TypeMap -> State Env ()
putTypeMap TypeMap
tm
                    Maybe OpAttr -> State Env (Maybe OpAttr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe OpAttr -> State Env (Maybe OpAttr))
-> Maybe OpAttr -> State Env (Maybe OpAttr)
forall a b. (a -> b) -> a -> b
$ case Maybe Term
mt of
                               Nothing -> Maybe OpAttr
forall a. Maybe a
Nothing
                               Just t :: Term
t -> OpAttr -> Maybe OpAttr
forall a. a -> Maybe a
Just (OpAttr -> Maybe OpAttr) -> OpAttr -> Maybe OpAttr
forall a b. (a -> b) -> a -> b
$ Term -> Range -> OpAttr
UnitOpAttr Term
t Range
ps
    _ -> Maybe OpAttr -> State Env (Maybe OpAttr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe OpAttr -> State Env (Maybe OpAttr))
-> Maybe OpAttr -> State Env (Maybe OpAttr)
forall a b. (a -> b) -> a -> b
$ OpAttr -> Maybe OpAttr
forall a. a -> Maybe a
Just OpAttr
b

tuplePatternToType :: [VarDecl] -> Type
tuplePatternToType :: [VarDecl] -> Type
tuplePatternToType vds :: [VarDecl]
vds =
    [Type] -> Range -> Type
mkProductTypeWithRange ((VarDecl -> Type) -> [VarDecl] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (VarDecl _ t :: Type
t _ _) -> Type
t) [VarDecl]
vds) (Range -> Type) -> Range -> Type
forall a b. (a -> b) -> a -> b
$ [VarDecl] -> Range
forall a. GetRange a => a -> Range
getRange [VarDecl]
vds

anaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool
anaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool
anaOpId br :: OpBrand
br sc :: TypeScheme
sc attrs :: [OpAttr]
attrs i :: PolyId
i@(PolyId j :: Id
j _ _) =
    do Maybe TypeScheme
mSc <- PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
anaPolyId PolyId
i TypeScheme
sc
       case Maybe TypeScheme
mSc of
           Nothing -> Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
           Just newSc :: TypeScheme
newSc -> do
               [Maybe OpAttr]
mAttrs <- (OpAttr -> State Env (Maybe OpAttr))
-> [OpAttr] -> State Env [Maybe OpAttr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
anaAttr TypeScheme
newSc) [OpAttr]
attrs
               Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
j TypeScheme
newSc ([OpAttr] -> Set OpAttr
forall a. Ord a => [a] -> Set a
Set.fromList ([OpAttr] -> Set OpAttr) -> [OpAttr] -> Set OpAttr
forall a b. (a -> b) -> a -> b
$ [Maybe OpAttr] -> [OpAttr]
forall a. [Maybe a] -> [a]
catMaybes [Maybe OpAttr]
mAttrs) (OpDefn -> State Env Bool) -> OpDefn -> State Env Bool
forall a b. (a -> b) -> a -> b
$ OpBrand -> OpDefn
NoOpDefn OpBrand
br

-- | analyse an op-item
anaOpItem :: OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))
anaOpItem :: OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))
anaOpItem br :: OpBrand
br oi :: Annoted OpItem
oi = do
  let Result ds :: [Diagnosis]
ds (Just bs :: [Id]
bs) = [Annotation] -> Result [Id]
extractBinders ([Annotation] -> Result [Id]) -> [Annotation] -> Result [Id]
forall a b. (a -> b) -> a -> b
$ Annoted OpItem -> [Annotation]
forall a. Annoted a -> [Annotation]
l_annos Annoted OpItem
oi [Annotation] -> [Annotation] -> [Annotation]
forall a. [a] -> [a] -> [a]
++ Annoted OpItem -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos Annoted OpItem
oi
  [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
  case Annoted OpItem -> OpItem
forall a. Annoted a -> a
item Annoted OpItem
oi of
    OpDecl is :: [PolyId]
is sc :: TypeScheme
sc attr :: [OpAttr]
attr ps :: Range
ps -> do
        case [PolyId]
is of
          [PolyId i :: Id
i _ _] -> (Id -> State Env ()) -> [Id] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Id -> Id -> State Env ()
addBinder Id
i) [Id]
bs
          _ -> 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]
bs) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags
            [DiagKind -> String -> [Id] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "ignoring binder syntax" [Id]
bs]
        [Bool]
ois <- (PolyId -> State Env Bool) -> [PolyId] -> State Env [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool
anaOpId OpBrand
br TypeScheme
sc [OpAttr]
attr) [PolyId]
is
        let us :: [PolyId]
us = ((PolyId, Bool) -> PolyId) -> [(PolyId, Bool)] -> [PolyId]
forall a b. (a -> b) -> [a] -> [b]
map (PolyId, Bool) -> PolyId
forall a b. (a, b) -> a
fst ([(PolyId, Bool)] -> [PolyId]) -> [(PolyId, Bool)] -> [PolyId]
forall a b. (a -> b) -> a -> b
$ ((PolyId, Bool) -> Bool) -> [(PolyId, Bool)] -> [(PolyId, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (PolyId, Bool) -> Bool
forall a b. (a, b) -> b
snd ([(PolyId, Bool)] -> [(PolyId, Bool)])
-> [(PolyId, Bool)] -> [(PolyId, Bool)]
forall a b. (a -> b) -> a -> b
$ [PolyId] -> [Bool] -> [(PolyId, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PolyId]
is [Bool]
ois
        Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem)))
-> Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall a b. (a -> b) -> a -> b
$ Maybe OpItem -> Annoted OpItem -> Annoted (Maybe OpItem)
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted (if [PolyId] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PolyId]
us then Maybe OpItem
forall a. Maybe a
Nothing else
            OpItem -> Maybe OpItem
forall a. a -> Maybe a
Just (OpItem -> Maybe OpItem) -> OpItem -> Maybe OpItem
forall a b. (a -> b) -> a -> b
$ [PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId]
us TypeScheme
sc [OpAttr]
attr Range
ps) Annoted OpItem
oi
    OpDefn p :: PolyId
p@(PolyId i :: Id
i _ _) oldPats :: [[VarDecl]]
oldPats rsc :: TypeScheme
rsc@(TypeScheme tArgs :: [TypeArg]
tArgs scTy :: Type
scTy qs :: Range
qs) trm :: Term
trm ps :: Range
ps
        -> do
       (Id -> State Env ()) -> [Id] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Id -> Id -> State Env ()
addBinder Id
i) [Id]
bs
       [VarDecl] -> State Env ()
checkUniqueVars ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ [[VarDecl]] -> [VarDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[VarDecl]]
oldPats
       LocalTypeVars
tvs <- (Env -> LocalTypeVars) -> State Env LocalTypeVars
forall s a. (s -> a) -> State s a
gets Env -> LocalTypeVars
localTypeVars
       [Maybe TypeArg]
mArgs <- (TypeArg -> State Env (Maybe TypeArg))
-> [TypeArg] -> State Env [Maybe TypeArg]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TypeArg -> State Env (Maybe TypeArg)
anaddTypeVarDecl [TypeArg]
tArgs
       [[Maybe VarDecl]]
mPats <- ([VarDecl] -> State Env [Maybe VarDecl])
-> [[VarDecl]] -> State Env [[Maybe VarDecl]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((VarDecl -> State Env (Maybe VarDecl))
-> [VarDecl] -> State Env [Maybe VarDecl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VarDecl -> State Env (Maybe VarDecl)
anaVarDecl) [[VarDecl]]
oldPats
       let newPats :: [[VarDecl]]
newPats = ([Maybe VarDecl] -> [VarDecl]) -> [[Maybe VarDecl]] -> [[VarDecl]]
forall a b. (a -> b) -> [a] -> [b]
map [Maybe VarDecl] -> [VarDecl]
forall a. [Maybe a] -> [a]
catMaybes [[Maybe VarDecl]]
mPats
           monoPats :: [[VarDecl]]
monoPats = ([VarDecl] -> [VarDecl]) -> [[VarDecl]] -> [[VarDecl]]
forall a b. (a -> b) -> [a] -> [b]
map ((VarDecl -> VarDecl) -> [VarDecl] -> [VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> VarDecl
makeMonomorph) [[VarDecl]]
newPats
           pats :: [Term]
pats = ([VarDecl] -> Term) -> [[VarDecl]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: [VarDecl]
l -> [Term] -> Range -> Term
mkTupleTerm ((VarDecl -> Term) -> [VarDecl] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Term
QualVar [VarDecl]
l) Range
nullRange) [[VarDecl]]
monoPats
       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_ ((VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((VarDecl -> State Env ()) -> [VarDecl] -> State Env ())
-> (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Bool -> VarDecl -> State Env ()
addLocalVar Bool
True) [[VarDecl]]
monoPats
       let newArgs :: [TypeArg]
newArgs = [Maybe TypeArg] -> [TypeArg]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TypeArg]
mArgs
       Maybe Type
mty <- Type -> State Env (Maybe Type)
anaStarType Type
scTy
       Maybe Term
mtrm <- Term -> State Env (Maybe Term)
resolve Term
trm
       case (Maybe Type
mty, Maybe Term
mtrm) of
           (Just rty :: Type
rty, Just rTrm :: Term
rTrm) -> do
               let (partial :: Partiality
partial, ty :: Type
ty) = case Type -> (Type, [Type])
getTypeAppl Type
rty of
                     (TypeName j :: Id
j _ _ , [lt :: Type
lt]) | Id
j Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId -> (Partiality
Partial, Type
lt)
                     _ -> (Partiality
Total, Type
rty)
                   monoty :: Type
monoty = Type -> Type
monoType Type
ty
               Maybe Term
mt <- Type -> Term -> State Env (Maybe Term)
typeCheck Type
monoty (Term -> State Env (Maybe Term)) -> Term -> State Env (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
rTrm TypeQual
AsType Type
monoty Range
ps
               Env
e <- State Env Env
forall s. State s s
get
               TypeScheme
newSc <- TypeScheme -> State Env TypeScheme
generalizeS (TypeScheme -> State Env TypeScheme)
-> TypeScheme -> State Env TypeScheme
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
newArgs
                      (Type -> Partiality -> [Type] -> Type
getFunType Type
ty Partiality
partial
                       ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ ([VarDecl] -> Type) -> [[VarDecl]] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map [VarDecl] -> Type
tuplePatternToType [[VarDecl]]
newPats) Range
qs
               Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
               LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
               case Maybe Term
mt of
                   Just lastTrm0 :: Term
lastTrm0 -> do
                       let lastTrm :: Term
lastTrm = case Term
lastTrm0 of
                             TypedTerm lTrm :: Term
lTrm AsType rTy :: Type
rTy rs :: Range
rs ->
                               case Term -> Maybe Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
lTrm of
                                 Just oTy :: Type
oTy | Env -> Type -> Type -> Bool
lesserType Env
e Type
oTy Type
rTy ->
                                   if Type
oTy Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
rTy then Term
lTrm else
                                      Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
lTrm TypeQual
Inferred Type
rTy Range
rs
                                 _ -> Term
lastTrm0
                             _ -> Term
lastTrm0
                           lamTrm :: Term
lamTrm = case ([Term]
pats, Partiality
partial) of
                             ([], Total) -> Term
lastTrm
                             _ -> [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm [Term]
pats Partiality
partial Term
lastTrm Range
ps
                           ot :: Term
ot = OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
br PolyId
p TypeScheme
newSc [] InstKind
Infer
                             Range
nullRange
                           lhs :: Term
lhs = Term -> [Term] -> Term
mkApplTerm Term
ot [Term]
pats
                           ef :: Term
ef = if OpBrand -> Bool
isPred OpBrand
br then
                                    Id -> Range -> Term -> Term -> Term
mkLogTerm Id
eqvId Range
ps Term
lhs Term
lastTrm
                                else Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm Id
eqId Type
monoty Range
ps Term
lhs Term
lastTrm
                           f :: Term
f = Env -> Term -> Range -> Term
mkEnvForall Env
e Term
ef Range
ps
                       Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
i TypeScheme
newSc Set OpAttr
forall a. Set a
Set.empty (OpDefn -> State Env Bool) -> OpDefn -> State Env Bool
forall a b. (a -> b) -> a -> b
$ OpBrand -> Term -> OpDefn
Definition OpBrand
br Term
lamTrm
                       [Named Sentence] -> State Env ()
appendSentences
                           [(String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed (Annoted OpItem -> String
forall a. Annoted a -> String
getRLabel Annoted OpItem
oi) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
Formula Term
f)
                            { isDef :: Bool
isDef = Bool
True }]
                       Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem)))
-> Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall a b. (a -> b) -> a -> b
$ Maybe OpItem -> Annoted OpItem -> Annoted (Maybe OpItem)
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted
                         (OpItem -> Maybe OpItem
forall a. a -> Maybe a
Just (OpItem -> Maybe OpItem) -> OpItem -> Maybe OpItem
forall a b. (a -> b) -> a -> b
$ PolyId -> [[VarDecl]] -> TypeScheme -> Term -> Range -> OpItem
OpDefn PolyId
p [[VarDecl]]
oldPats TypeScheme
rsc Term
rTrm Range
ps) Annoted OpItem
oi
                   Nothing -> do
                       Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
i TypeScheme
newSc Set OpAttr
forall a. Set a
Set.empty (OpDefn -> State Env Bool) -> OpDefn -> State Env Bool
forall a b. (a -> b) -> a -> b
$ OpBrand -> OpDefn
NoOpDefn OpBrand
br
                       Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem)))
-> Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall a b. (a -> b) -> a -> b
$ Maybe OpItem -> Annoted OpItem -> Annoted (Maybe OpItem)
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted
                         (OpItem -> Maybe OpItem
forall a. a -> Maybe a
Just (OpItem -> Maybe OpItem) -> OpItem -> Maybe OpItem
forall a b. (a -> b) -> a -> b
$ [PolyId] -> TypeScheme -> [OpAttr] -> Range -> OpItem
OpDecl [PolyId
p] TypeScheme
newSc [] Range
ps) Annoted OpItem
oi
           _ -> do
               Map Id VarDefn -> State Env ()
putLocalVars Map Id VarDefn
vs
               LocalTypeVars -> State Env ()
putLocalTypeVars LocalTypeVars
tvs
               Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem)))
-> Annoted (Maybe OpItem) -> State Env (Annoted (Maybe OpItem))
forall a b. (a -> b) -> a -> b
$ Maybe OpItem -> Annoted OpItem -> Annoted (Maybe OpItem)
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted Maybe OpItem
forall a. Maybe a
Nothing Annoted OpItem
oi

-- | analyse a program equation
anaProgEq :: Annoted ProgEq -> State Env (Maybe ProgEq)
anaProgEq :: Annoted ProgEq -> State Env (Maybe ProgEq)
anaProgEq ape :: Annoted ProgEq
ape = do
       let pe :: ProgEq
pe@(ProgEq _ _ q :: Range
q) = Annoted ProgEq -> ProgEq
forall a. Annoted a -> a
item Annoted ProgEq
ape
       Maybe Term
rp <- Term -> State Env (Maybe Term)
resolve (LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
Program [ProgEq
pe] (BracketKind -> [Term] -> Range -> Term
BracketTerm BracketKind
Parens [] Range
q) Range
q)
       case Maybe Term
rp of
         Just t :: Term
t@(LetTerm _ (rpe :: ProgEq
rpe@(ProgEq {}) : _) _ _) -> do
           Maybe Term
mp <- Type -> Term -> State Env (Maybe Term)
typeCheck Type
unitType Term
t
           GlobalAnnos
ga <- (Env -> GlobalAnnos) -> State Env GlobalAnnos
forall s a. (s -> a) -> State s a
State.gets Env -> GlobalAnnos
globAnnos
           case Maybe Term
mp of
             Just (LetTerm _ (newPrg :: ProgEq
newPrg@(ProgEq newPat :: Term
newPat _ _) : _) _ _) ->
               case Term -> Maybe (Id, TypeScheme, [Term])
getAppl Term
newPat of
               Just (i :: Id
i, sc :: TypeScheme
sc, _) -> do
                           Id -> TypeScheme -> Set OpAttr -> OpDefn -> State Env Bool
addOpId Id
i TypeScheme
sc Set OpAttr
forall a. Set a
Set.empty (OpDefn -> State Env Bool) -> OpDefn -> State Env Bool
forall a b. (a -> b) -> a -> b
$ OpBrand -> OpDefn
NoOpDefn OpBrand
Op
                           [Named Sentence] -> State Env ()
appendSentences [(String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("pe_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
i "")
                                            (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> ProgEq -> Sentence
ProgEqSen Id
i TypeScheme
sc ProgEq
newPrg)
                                            { isDef :: Bool
isDef = Bool
True }]
                           Env
e <- State Env Env
forall s. State s s
get
                           Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Env -> Term -> Bool
isLHS Env
e Term
newPat)
                             (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> String -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> String -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Warning
                                         "illegal lhs pattern" Term
newPat]
                           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
$ ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just ProgEq
rpe
               Nothing -> do [Diagnosis] -> State Env ()
addDiags [GlobalAnnos -> DiagKind -> String -> Term -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
GlobalAnnos -> DiagKind -> String -> a -> Diagnosis
mkNiceDiag GlobalAnnos
ga DiagKind
Error
                                       "illegal toplevel pattern" Term
newPat]
                             Maybe ProgEq -> State Env (Maybe ProgEq)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProgEq
forall a. Maybe a
Nothing
             _ -> Maybe ProgEq -> State Env (Maybe ProgEq)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProgEq
forall a. Maybe a
Nothing
         _ -> Maybe ProgEq -> State Env (Maybe ProgEq)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProgEq
forall a. Maybe a
Nothing
extractBinderId :: Annotation -> Result Id
extractBinderId :: Annotation -> Result Id
extractBinderId a :: Annotation
a = case Annotation
a of
  Unparsed_anno (Annote_word f :: String
f@String
"binder") s :: Annote_text
s r :: Range
r ->
    case Parsec String () Id -> String -> String -> Either ParseError Id
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (CharParser () ()
forall st. CharParser st ()
skip CharParser () () -> Parsec String () Id -> Parsec String () Id
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parsec String () Id
forall st. GenParser Char st Id
opId Parsec String () Id -> CharParser () () -> Parsec String () Id
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser () ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) String
f (String -> Either ParseError Id) -> String -> Either ParseError Id
forall a b. (a -> b) -> a -> b
$ Annote_text -> String
annoArg Annote_text
s of
      Right i :: Id
i -> Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
i
      Left err :: ParseError
err -> String -> Range -> Result Id
forall a. String -> Range -> Result a
fatal_error (ParseError -> String
showErr ParseError
err String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nin " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Annotation -> Doc
annoDoc Annotation
a)) Range
r
  _ -> [Diagnosis] -> Maybe Id -> Result Id
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe Id
forall a. Maybe a
Nothing

extractBinders :: [Annotation] -> Result [Id]
extractBinders :: [Annotation] -> Result [Id]
extractBinders as :: [Annotation]
as =
    let rs :: [Result Id]
rs = (Annotation -> Result Id) -> [Annotation] -> [Result Id]
forall a b. (a -> b) -> [a] -> [b]
map Annotation -> Result Id
extractBinderId [Annotation]
as
        ds :: [Diagnosis]
ds = (Result Id -> [Diagnosis]) -> [Result Id] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Result Id -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags [Result Id]
rs
    in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then [Id] -> Result [Id]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Result [Id]) -> [Id] -> Result [Id]
forall a b. (a -> b) -> a -> b
$ (Result Id -> Maybe Id) -> [Result Id] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Result Id -> Maybe Id
forall a. Result a -> Maybe a
maybeResult [Result Id]
rs
       else [Diagnosis] -> Maybe [Id] -> Result [Id]
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds (Maybe [Id] -> Result [Id]) -> Maybe [Id] -> Result [Id]
forall a b. (a -> b) -> a -> b
$ [Id] -> Maybe [Id]
forall a. a -> Maybe a
Just []

addBinding :: Id -> Id -> State.State Env ()
addBinding :: Id -> Id -> State Env ()
addBinding o :: Id
o b :: Id
b = do
  [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> Id -> [Diagnosis]
getBinderDiags Id
o Id
b
  (Env -> Env) -> State Env ()
forall s. (s -> s) -> State s ()
State.modify ((Env -> Env) -> State Env ()) -> (Env -> Env) -> State Env ()
forall a b. (a -> b) -> a -> b
$ \ e :: Env
e -> Env
e { binders :: Map Id Id
binders = Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
b Id
o (Map Id Id -> Map Id Id) -> Map Id Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ Env -> Map Id Id
binders Env
e }
  Env
e <- State Env Env
forall s. State s s
State.get
  let ga :: GlobalAnnos
ga = Env -> GlobalAnnos
globAnnos Env
e
      aa :: AssocMap
aa = GlobalAnnos -> AssocMap
assoc_annos GlobalAnnos
ga
  Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Bool
isInfix Id
b Bool -> Bool -> Bool
&& Bool -> Bool
not (Id -> AssocMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
b AssocMap
aa)) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$
      Env -> State Env ()
forall s. s -> State s ()
State.put Env
e { globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
ga { assoc_annos :: AssocMap
assoc_annos = Id -> AssocEither -> AssocMap -> AssocMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
b AssocEither
ARight AssocMap
aa }}

getBinderDiags :: Id -> Id -> [Diagnosis]
getBinderDiags :: Id -> Id -> [Diagnosis]
getBinderDiags o :: Id
o b :: Id
b =
    let c :: Int
c = Id -> Int
placeCount Id
b
        d :: Int
d = Id -> Int
placeCount Id
o Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
        str :: String
str = "expected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max 2 Int
d) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " places in binder"
    in if Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error String
str Id
b]
    else if Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
c then
       if Id -> Bool
isMixfix Id
o then [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning String
str Id
b]
       else [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint ("non-mixfix-id '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' for binder") Id
b]
    else []

addBinder :: Id -> Id -> State.State Env ()
addBinder :: Id -> Id -> State Env ()
addBinder o :: Id
o b :: Id
b = do
  Map Id Id
bs <- (Env -> Map Id Id) -> State Env (Map Id Id)
forall s a. (s -> a) -> State s a
State.gets Env -> Map Id Id
binders
  Assumps
as <- (Env -> Assumps) -> State Env Assumps
forall s a. (s -> a) -> State s a
State.gets Env -> Assumps
assumps
  Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Id -> Assumps -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
b Assumps
as) (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> State Env ()
addDiags
    [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "binder shadows shadows global name(s)" Id
b]
  case Id -> Map Id Id -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
b Map Id Id
bs of
    Just o2 :: Id
o2 -> if Id
o Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
o2 then do
        [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning
                  ("binder conflict for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> Id -> String
forall a. Pretty a => a -> a -> String
expected Id
o2 Id
o)
                  (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
b]
        Id -> Id -> State Env ()
addBinding Id
o Id
b
      else [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "repeated binder syntax" Id
b]
    Nothing -> Id -> Id -> State Env ()
addBinding Id
o Id
b