----------------------------------------------------------------------
-- |
-- Module      : CheckGrammar
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/11 23:24:33 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.31 $
--
-- AR 4\/12\/1999 -- 1\/4\/2000 -- 8\/9\/2001 -- 15\/5\/2002 -- 27\/11\/2002 -- 18\/6\/2003
--
-- type checking also does the following modifications:
--
--  - types of operations and local constants are inferred and put in place
--
--  - both these types and linearization types are computed
--
--  - tables are type-annotated
-----------------------------------------------------------------------------

module GF.Compile.CheckGrammar(checkModule) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint

import GF.Infra.Ident
import GF.Infra.Option

import GF.Compile.TypeCheck.Abstract
import GF.Compile.TypeCheck.Concrete(computeLType,checkLType,inferLType,ppType)
import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
import qualified GF.Compile.Compute.Concrete as CN(normalForm,resourceValues)

import GF.Grammar
import GF.Grammar.Lexer
import GF.Grammar.Lookup

import GF.Data.Operations
import GF.Infra.CheckM

import Data.List
import qualified Data.Set as Set
import qualified Data.Map as Map
import Control.Monad
import GF.Text.Pretty

-- | checking is performed in the dependency order of modules
checkModule :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
checkModule :: Options
-> FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
checkModule Options
opts FilePath
cwd SourceGrammar
sgr mo :: SourceModule
mo@(ModuleName
m,ModuleInfo
mi) = do
  FilePath -> SourceGrammar -> SourceModule -> Check ()
checkRestrictedInheritance FilePath
cwd SourceGrammar
sgr SourceModule
mo
  SourceModule
mo <- case ModuleInfo -> ModuleType
mtype ModuleInfo
mi of
          MTConcrete ModuleName
a -> do let gr :: SourceGrammar
gr = SourceGrammar -> SourceModule -> SourceGrammar
prependModule SourceGrammar
sgr SourceModule
mo
                             ModuleInfo
abs <- SourceGrammar -> ModuleName -> Check ModuleInfo
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> ModuleName -> m ModuleInfo
lookupModule SourceGrammar
gr ModuleName
a
                             Options
-> FilePath
-> SourceGrammar
-> SourceModule
-> SourceModule
-> Check SourceModule
checkCompleteGrammar Options
opts FilePath
cwd SourceGrammar
gr (ModuleName
a,ModuleInfo
abs) SourceModule
mo
          ModuleType
_            -> SourceModule -> Check SourceModule
forall (m :: * -> *) a. Monad m => a -> m a
return SourceModule
mo
  [[(Ident, Info)]]
infoss <- FilePath
-> ModuleInfo
-> Location
-> Doc
-> Check [[(Ident, Info)]]
-> Check [[(Ident, Info)]]
forall a1 a2 a3.
(Pretty a1, HasSourcePath a2) =>
FilePath -> a2 -> Location -> a1 -> Check a3 -> Check a3
checkInModule FilePath
cwd ModuleInfo
mi Location
NoLoc Doc
empty (Check [[(Ident, Info)]] -> Check [[(Ident, Info)]])
-> Check [[(Ident, Info)]] -> Check [[(Ident, Info)]]
forall a b. (a -> b) -> a -> b
$ SourceModule -> Check [[(Ident, Info)]]
forall (m :: * -> *).
ErrorMonad m =>
SourceModule -> m [[(Ident, Info)]]
topoSortJments2 SourceModule
mo
  (SourceModule -> [(Ident, Info)] -> Check SourceModule)
-> SourceModule -> [[(Ident, Info)]] -> Check SourceModule
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SourceModule -> [(Ident, Info)] -> Check SourceModule
updateCheckInfos SourceModule
mo [[(Ident, Info)]]
infoss
  where
    updateCheckInfos :: SourceModule -> [(Ident, Info)] -> Check SourceModule
updateCheckInfos SourceModule
mo = ([(Ident, Info)] -> SourceModule)
-> Check [(Ident, Info)] -> Check SourceModule
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SourceModule -> (Ident, Info) -> SourceModule)
-> SourceModule -> [(Ident, Info)] -> SourceModule
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SourceModule -> (Ident, Info) -> SourceModule
forall a. (a, ModuleInfo) -> (Ident, Info) -> (a, ModuleInfo)
update SourceModule
mo) (Check [(Ident, Info)] -> Check SourceModule)
-> ([(Ident, Info)] -> Check [(Ident, Info)])
-> [(Ident, Info)]
-> Check SourceModule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Check (Ident, Info)] -> Check [(Ident, Info)]
forall a. [Check a] -> Check [a]
parallelCheck ([Check (Ident, Info)] -> Check [(Ident, Info)])
-> ([(Ident, Info)] -> [Check (Ident, Info)])
-> [(Ident, Info)]
-> Check [(Ident, Info)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ident, Info) -> Check (Ident, Info))
-> [(Ident, Info)] -> [Check (Ident, Info)]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Info) -> Check (Ident, Info)
check
      where check :: (Ident, Info) -> Check (Ident, Info)
check (Ident
i,Info
info) = (Info -> (Ident, Info)) -> Check Info -> Check (Ident, Info)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) Ident
i) (Options
-> FilePath
-> SourceGrammar
-> SourceModule
-> Ident
-> Info
-> Check Info
checkInfo Options
opts FilePath
cwd SourceGrammar
sgr SourceModule
mo Ident
i Info
info)
    update :: (a, ModuleInfo) -> (Ident, Info) -> (a, ModuleInfo)
update mo :: (a, ModuleInfo)
mo@(a
m,ModuleInfo
mi) (Ident
i,Info
info) = (a
m,ModuleInfo
mi{jments :: Map Ident Info
jments=Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
i Info
info (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)})

-- check if restricted inheritance modules are still coherent
-- i.e. that the defs of remaining names don't depend on omitted names
checkRestrictedInheritance :: FilePath -> SourceGrammar -> SourceModule -> Check ()
checkRestrictedInheritance :: FilePath -> SourceGrammar -> SourceModule -> Check ()
checkRestrictedInheritance FilePath
cwd SourceGrammar
sgr (ModuleName
name,ModuleInfo
mo) = FilePath -> ModuleInfo -> Location -> Doc -> Check () -> Check ()
forall a1 a2 a3.
(Pretty a1, HasSourcePath a2) =>
FilePath -> a2 -> Location -> a1 -> Check a3 -> Check a3
checkInModule FilePath
cwd ModuleInfo
mo Location
NoLoc Doc
empty (Check () -> Check ()) -> Check () -> Check ()
forall a b. (a -> b) -> a -> b
$ do
  let irs :: [(ModuleName, MInclude)]
irs = [(ModuleName, MInclude)
ii | ii :: (ModuleName, MInclude)
ii@(ModuleName
_,MInclude
mi) <- ModuleInfo -> [(ModuleName, MInclude)]
mextend ModuleInfo
mo, MInclude
mi MInclude -> MInclude -> Bool
forall a. Eq a => a -> a -> Bool
/= MInclude
MIAll]  -- names with restr. inh.
  let mrs :: [(SourceModule, MInclude)]
mrs = [((ModuleName
i,ModuleInfo
m),MInclude
mi) | (ModuleName
i,ModuleInfo
m) <- [SourceModule]
mos, Just MInclude
mi <- [ModuleName -> [(ModuleName, MInclude)] -> Maybe MInclude
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup ModuleName
i [(ModuleName, MInclude)]
irs]]
                             -- the restr. modules themself, with restr. infos
  ((SourceModule, MInclude) -> Check ())
-> [(SourceModule, MInclude)] -> Check ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SourceModule, MInclude) -> Check ()
forall a2. Pretty a2 => ((a2, ModuleInfo), MInclude) -> Check ()
checkRem [(SourceModule, MInclude)]
mrs
 where
   mos :: [SourceModule]
mos = SourceGrammar -> [SourceModule]
modules SourceGrammar
sgr
   checkRem :: ((a2, ModuleInfo), MInclude) -> Check ()
checkRem ((a2
i,ModuleInfo
m),MInclude
mi) = do
     let ([Ident]
incl,[Ident]
excl) = (Ident -> Bool) -> [Ident] -> ([Ident], [Ident])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (MInclude -> Ident -> Bool
isInherited MInclude
mi) (Map Ident Info -> [Ident]
forall k a. Map k a -> [k]
Map.keys (ModuleInfo -> Map Ident Info
jments ModuleInfo
m))
     let incld :: Ident -> Bool
incld Ident
c   = Ident -> Set Ident -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Ident
c ([Ident] -> Set Ident
forall a. Ord a => [a] -> Set a
Set.fromList [Ident]
incl)
     let illegal :: Ident -> Bool
illegal Ident
c = Ident -> Set Ident -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Ident
c ([Ident] -> Set Ident
forall a. Ord a => [a] -> Set a
Set.fromList [Ident]
excl)
     let illegals :: [(Ident, [Ident])]
illegals = [(Ident
f,[Ident]
is) |
           (Ident
f,[Ident]
cs) <- [(Ident, [Ident])]
allDeps, Ident -> Bool
incld Ident
f, let is :: [Ident]
is = (Ident -> Bool) -> [Ident] -> [Ident]
forall a. (a -> Bool) -> [a] -> [a]
filter Ident -> Bool
illegal [Ident]
cs, Bool -> Bool
not ([Ident] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ident]
is)]
     case [(Ident, [Ident])]
illegals of
       [] -> () -> Check ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [(Ident, [Ident])]
cs -> Doc -> Check ()
checkWarn (FilePath
"In inherited module" FilePath -> a2 -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> a2
i Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<> FilePath
", dependence of excluded constants:" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                         Int -> Doc -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 ([Doc] -> Doc
forall a. Pretty a => [a] -> Doc
vcat [Ident
f Ident -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> FilePath
"on" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Ident] -> Doc
forall a. Pretty a => [a] -> Doc
fsep [Ident]
is | (Ident
f,[Ident]
is) <- [(Ident, [Ident])]
cs]))
   allDeps :: [(Ident, [Ident])]
allDeps = (SourceModule -> [(Ident, [Ident])])
-> [SourceModule] -> [(Ident, [Ident])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((ModuleName -> Bool) -> Map Ident Info -> [(Ident, [Ident])]
allDependencies (Bool -> ModuleName -> Bool
forall a b. a -> b -> a
const Bool
True) (Map Ident Info -> [(Ident, [Ident])])
-> (SourceModule -> Map Ident Info)
-> SourceModule
-> [(Ident, [Ident])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> Map Ident Info
jments (ModuleInfo -> Map Ident Info)
-> (SourceModule -> ModuleInfo) -> SourceModule -> Map Ident Info
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceModule -> ModuleInfo
forall a b. (a, b) -> b
snd) [SourceModule]
mos

checkCompleteGrammar :: Options -> FilePath -> Grammar -> Module -> Module -> Check Module
checkCompleteGrammar :: Options
-> FilePath
-> SourceGrammar
-> SourceModule
-> SourceModule
-> Check SourceModule
checkCompleteGrammar Options
opts FilePath
cwd SourceGrammar
gr (ModuleName
am,ModuleInfo
abs) (ModuleName
cm,ModuleInfo
cnc) = FilePath
-> ModuleInfo
-> Location
-> Doc
-> Check SourceModule
-> Check SourceModule
forall a1 a2 a3.
(Pretty a1, HasSourcePath a2) =>
FilePath -> a2 -> Location -> a1 -> Check a3 -> Check a3
checkInModule FilePath
cwd ModuleInfo
cnc Location
NoLoc Doc
empty (Check SourceModule -> Check SourceModule)
-> Check SourceModule -> Check SourceModule
forall a b. (a -> b) -> a -> b
$ do
  let jsa :: Map Ident Info
jsa = ModuleInfo -> Map Ident Info
jments ModuleInfo
abs
  let jsc :: Map Ident Info
jsc = ModuleInfo -> Map Ident Info
jments ModuleInfo
cnc

  -- check that all concrete constants are in abstract; build types for all lin
  Map Ident Info
jsc <- (Map Ident Info -> (Ident, Info) -> Check (Map Ident Info))
-> Map Ident Info -> [(Ident, Info)] -> Check (Map Ident Info)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Ident Info -> (Ident, Info) -> Check (Map Ident Info)
checkCnc Map Ident Info
forall k a. Map k a
Map.empty (Map Ident Info -> [(Ident, Info)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Ident Info
jsc)

  -- check that all abstract constants are in concrete; build default lin and lincats
  Map Ident Info
jsc <- (Map Ident Info -> (Ident, Info) -> Check (Map Ident Info))
-> Map Ident Info -> [(Ident, Info)] -> Check (Map Ident Info)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Ident Info -> (Ident, Info) -> Check (Map Ident Info)
checkAbs Map Ident Info
jsc (Map Ident Info -> [(Ident, Info)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Ident Info
jsa)

  SourceModule -> Check SourceModule
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName
cm,ModuleInfo
cnc{jments :: Map Ident Info
jments=Map Ident Info
jsc})
  where
   checkAbs :: Map Ident Info -> (Ident, Info) -> Check (Map Ident Info)
checkAbs Map Ident Info
js i :: (Ident, Info)
i@(Ident
c,Info
info) =
     case Info
info of
       AbsFun (Just (L Location
loc Type
ty)) Maybe Int
_ Maybe [L Equation]
_ Maybe Bool
_
           -> do let mb_def :: Err Type
mb_def = do
                       let (Context
cxt,(ModuleName
_,Ident
i),[Type]
_) = Type -> (Context, (ModuleName, Ident), [Type])
typeForm Type
ty
                       Info
info <- Ident -> Map Ident Info -> Err Info
forall (m :: * -> *) b. ErrorMonad m => Ident -> Map Ident b -> m b
lookupIdent Ident
i Map Ident Info
js
                       Info
info <- case Info
info of
                                 (AnyInd Bool
_ ModuleName
m) -> do (ModuleName
m,Info
info) <- SourceGrammar -> (ModuleName, Ident) -> Err (ModuleName, Info)
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m (ModuleName, Info)
lookupOrigInfo SourceGrammar
gr (ModuleName
m,Ident
i)
                                                    Info -> Err Info
forall (m :: * -> *) a. Monad m => a -> m a
return Info
info
                                 Info
_            -> Info -> Err Info
forall (m :: * -> *) a. Monad m => a -> m a
return Info
info
                       case Info
info of
                         CncCat (Just (L Location
loc (RecType []))) Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> Type -> Err Type
forall (m :: * -> *) a. Monad m => a -> m a
return ((Hypo -> Type -> Type) -> Type -> Context -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Hypo
_ -> BindType -> Ident -> Type -> Type
Abs BindType
Explicit Ident
identW) ([Assign] -> Type
R []) Context
cxt)
                         Info
_                                          -> FilePath -> Err Type
forall a. FilePath -> Err a
Bad FilePath
"no def lin"

                 case Ident -> Map Ident Info -> Err Info
forall (m :: * -> *) b. ErrorMonad m => Ident -> Map Ident b -> m b
lookupIdent Ident
c Map Ident Info
js of
                   Ok (AnyInd Bool
_ ModuleName
_) -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js
                   Ok (CncFun Maybe (Ident, Context, Type)
ty (Just L Type
def) Maybe (L Type)
mn Maybe PMCFG
mf) ->
                                 Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c (Maybe (Ident, Context, Type)
-> Maybe (L Type) -> Maybe (L Type) -> Maybe PMCFG -> Info
CncFun Maybe (Ident, Context, Type)
ty (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just L Type
def) Maybe (L Type)
mn Maybe PMCFG
mf) Map Ident Info
js
                   Ok (CncFun Maybe (Ident, Context, Type)
ty Maybe (L Type)
Nothing    Maybe (L Type)
mn Maybe PMCFG
mf) ->
                     case Err Type
mb_def of
                       Ok Type
def -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c (Maybe (Ident, Context, Type)
-> Maybe (L Type) -> Maybe (L Type) -> Maybe PMCFG -> Info
CncFun Maybe (Ident, Context, Type)
ty (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
NoLoc Type
def)) Maybe (L Type)
mn Maybe PMCFG
mf) Map Ident Info
js
                       Bad FilePath
_  -> do Ident -> Check ()
forall a2. Pretty a2 => a2 -> Check ()
noLinOf Ident
c
                                    Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js
                   Err Info
_ -> do
                     case Err Type
mb_def of
                       Ok Type
def -> do (Context
cont,Type
val) <- SourceGrammar -> ModuleName -> Type -> Check (Context, Type)
linTypeOfType SourceGrammar
gr ModuleName
cm Type
ty
                                    let linty :: (Ident, Context, Type)
linty = ((ModuleName, Ident) -> Ident
forall a b. (a, b) -> b
snd (Type -> (ModuleName, Ident)
valCat Type
ty),Context
cont,Type
val)
                                    Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c (Maybe (Ident, Context, Type)
-> Maybe (L Type) -> Maybe (L Type) -> Maybe PMCFG -> Info
CncFun ((Ident, Context, Type) -> Maybe (Ident, Context, Type)
forall a. a -> Maybe a
Just (Ident, Context, Type)
linty) (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
NoLoc Type
def)) Maybe (L Type)
forall a. Maybe a
Nothing Maybe PMCFG
forall a. Maybe a
Nothing) Map Ident Info
js
                       Bad FilePath
_  -> do Ident -> Check ()
forall a2. Pretty a2 => a2 -> Check ()
noLinOf Ident
c
                                    Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js
         where noLinOf :: a2 -> Check ()
noLinOf a2
c = Doc -> Check ()
checkWarn (FilePath
"no linearization of" FilePath -> a2 -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> a2
c)
       AbsCat (Just L Context
_) -> case Ident -> Map Ident Info -> Err Info
forall (m :: * -> *) b. ErrorMonad m => Ident -> Map Ident b -> m b
lookupIdent Ident
c Map Ident Info
js of
         Ok (AnyInd Bool
_ ModuleName
_) -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js
         Ok (CncCat (Just L Type
_) Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_) -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js
         Ok (CncCat Maybe (L Type)
Nothing Maybe (L Type)
md Maybe (L Type)
mr Maybe (L Type)
mp Maybe PMCFG
mpmcfg) -> do
           Doc -> Check ()
checkWarn (FilePath
"no linearization type for" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<> FilePath
", inserting default {s : Str}")
           Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c (Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe PMCFG
-> Info
CncCat (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
NoLoc Type
defLinType)) Maybe (L Type)
md Maybe (L Type)
mr Maybe (L Type)
mp Maybe PMCFG
mpmcfg) Map Ident Info
js
         Err Info
_ -> do
           Doc -> Check ()
checkWarn (FilePath
"no linearization type for" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<> FilePath
", inserting default {s : Str}")
           Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c (Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe PMCFG
-> Info
CncCat (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
NoLoc Type
defLinType)) Maybe (L Type)
forall a. Maybe a
Nothing Maybe (L Type)
forall a. Maybe a
Nothing Maybe (L Type)
forall a. Maybe a
Nothing Maybe PMCFG
forall a. Maybe a
Nothing) Map Ident Info
js
       Info
_ -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js

   checkCnc :: Map Ident Info -> (Ident, Info) -> Check (Map Ident Info)
checkCnc Map Ident Info
js (Ident
c,Info
info) =
     case Info
info of
       CncFun Maybe (Ident, Context, Type)
_ Maybe (L Type)
d Maybe (L Type)
mn Maybe PMCFG
mf -> case SourceGrammar -> (ModuleName, Ident) -> Err (ModuleName, Info)
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m (ModuleName, Info)
lookupOrigInfo SourceGrammar
gr (ModuleName
am,Ident
c) of
                             Ok (ModuleName
_,AbsFun (Just (L Location
_ Type
ty)) Maybe Int
_ Maybe [L Equation]
_ Maybe Bool
_) ->
                                        do (Context
cont,Type
val) <- SourceGrammar -> ModuleName -> Type -> Check (Context, Type)
linTypeOfType SourceGrammar
gr ModuleName
cm Type
ty
                                           let linty :: (Ident, Context, Type)
linty = ((ModuleName, Ident) -> Ident
forall a b. (a, b) -> b
snd (Type -> (ModuleName, Ident)
valCat Type
ty),Context
cont,Type
val)
                                           Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c (Maybe (Ident, Context, Type)
-> Maybe (L Type) -> Maybe (L Type) -> Maybe PMCFG -> Info
CncFun ((Ident, Context, Type) -> Maybe (Ident, Context, Type)
forall a. a -> Maybe a
Just (Ident, Context, Type)
linty) Maybe (L Type)
d Maybe (L Type)
mn Maybe PMCFG
mf) Map Ident Info
js
                             Err (ModuleName, Info)
_       -> do Doc -> Check ()
checkWarn (FilePath
"function" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> FilePath
"is not in abstract")
                                           Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js
       CncCat {} ->
         case SourceGrammar -> (ModuleName, Ident) -> Err (ModuleName, Info)
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m (ModuleName, Info)
lookupOrigInfo SourceGrammar
gr (ModuleName
am,Ident
c) of
           Ok (ModuleName
_,AbsCat Maybe (L Context)
_) -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c Info
info Map Ident Info
js
           {- -- This might be too pedantic:
           Ok (_,AbsFun {}) ->
                   checkError ("lincat:"<+>c<+>"is a fun, not a cat")
           -}
           Err (ModuleName, Info)
_ -> do Doc -> Check ()
checkWarn (FilePath
"category" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> FilePath
"is not in abstract")
                   Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Ident Info
js

       Info
_ -> Map Ident Info -> Check (Map Ident Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Ident Info -> Check (Map Ident Info))
-> Map Ident Info -> Check (Map Ident Info)
forall a b. (a -> b) -> a -> b
$ Ident -> Info -> Map Ident Info -> Map Ident Info
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
c Info
info Map Ident Info
js


-- | General Principle: only Just-values are checked.
-- A May-value has always been checked in its origin module.
checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
checkInfo :: Options
-> FilePath
-> SourceGrammar
-> SourceModule
-> Ident
-> Info
-> Check Info
checkInfo Options
opts FilePath
cwd SourceGrammar
sgr (ModuleName
m,ModuleInfo
mo) Ident
c Info
info = FilePath
-> ModuleInfo -> Location -> Doc -> Check Info -> Check Info
forall a1 a2 a3.
(Pretty a1, HasSourcePath a2) =>
FilePath -> a2 -> Location -> a1 -> Check a3 -> Check a3
checkInModule FilePath
cwd ModuleInfo
mo Location
NoLoc Doc
empty (Check Info -> Check Info) -> Check Info -> Check Info
forall a b. (a -> b) -> a -> b
$ do
  Ident -> Check ()
checkReservedId Ident
c
  case Info
info of
    AbsCat (Just (L Location
loc Context
cont)) ->
      Location -> FilePath -> [Doc] -> Check Info
forall a2 a.
(Pretty a2, Pretty a) =>
Location -> a2 -> [a] -> Check Info
mkCheck Location
loc FilePath
"the category" ([Doc] -> Check Info) -> [Doc] -> Check Info
forall a b. (a -> b) -> a -> b
$
        SourceGrammar -> Context -> [Doc]
checkContext SourceGrammar
gr Context
cont

    AbsFun (Just (L Location
loc Type
typ0)) Maybe Int
ma Maybe [L Equation]
md Maybe Bool
moper -> do
      Type
typ <- [(Ident, Type)] -> Type -> Check Type
compAbsTyp [] Type
typ0   -- to calculate let definitions
      Location -> FilePath -> [Doc] -> Check Info
forall a2 a.
(Pretty a2, Pretty a) =>
Location -> a2 -> [a] -> Check Info
mkCheck Location
loc FilePath
"the type of function" ([Doc] -> Check Info) -> [Doc] -> Check Info
forall a b. (a -> b) -> a -> b
$
        SourceGrammar -> Type -> [Doc]
checkTyp SourceGrammar
gr Type
typ
      case Maybe [L Equation]
md of
        Just [L Equation]
eqs -> (L Equation -> Check Info) -> [L Equation] -> Check ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(L Location
loc Equation
eq) -> Location -> FilePath -> [Doc] -> Check Info
forall a2 a.
(Pretty a2, Pretty a) =>
Location -> a2 -> [a] -> Check Info
mkCheck Location
loc FilePath
"the definition of function" ([Doc] -> Check Info) -> [Doc] -> Check Info
forall a b. (a -> b) -> a -> b
$
                                          SourceGrammar -> (ModuleName, Ident) -> Type -> Equation -> [Doc]
checkDef SourceGrammar
gr (ModuleName
m,Ident
c) Type
typ Equation
eq) [L Equation]
eqs
        Maybe [L Equation]
Nothing  -> () -> Check ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (L Type)
-> Maybe Int -> Maybe [L Equation] -> Maybe Bool -> Info
AbsFun (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
typ)) Maybe Int
ma Maybe [L Equation]
md Maybe Bool
moper)

    CncCat Maybe (L Type)
mty Maybe (L Type)
mdef Maybe (L Type)
mref Maybe (L Type)
mpr Maybe PMCFG
mpmcfg -> do
      Maybe (L Type)
mty  <- case Maybe (L Type)
mty of
                Just (L Location
loc Type
typ) -> Location
-> FilePath -> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"linearization type of" (Check (Maybe (L Type)) -> Check (Maybe (L Type)))
-> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a b. (a -> b) -> a -> b
$
                                     (if Bool
False --flag optNewComp opts
                                        then do (Type
typ,Type
_) <- GlobalEnv -> Type -> Type -> Check (Type, Type)
CN.checkLType (Options -> SourceGrammar -> GlobalEnv
CN.resourceValues Options
opts SourceGrammar
gr) Type
typ Type
typeType
                                                Type
typ  <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr [] Type
typ
                                                Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
typ))
                                        else do (Type
typ,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
typ Type
typeType
                                                Type
typ  <- SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr [] Type
typ
                                                Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
typ)))
                Maybe (L Type)
Nothing          -> Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
forall a. Maybe a
Nothing
      Maybe (L Type)
mdef <- case (Maybe (L Type)
mty,Maybe (L Type)
mdef) of
                (Just (L Location
_ Type
typ),Just (L Location
loc Type
def)) ->
                    Location
-> FilePath -> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"default linearization of" (Check (Maybe (L Type)) -> Check (Maybe (L Type)))
-> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a b. (a -> b) -> a -> b
$ do
                       (Type
def,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
def ([Type] -> Type -> Type
mkFunType [Type
typeStr] Type
typ)
                       Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
def))
                (Maybe (L Type), Maybe (L Type))
_ -> Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
forall a. Maybe a
Nothing
      Maybe (L Type)
mref <- case (Maybe (L Type)
mty,Maybe (L Type)
mref) of
                (Just (L Location
_ Type
typ),Just (L Location
loc Type
ref)) ->
                    Location
-> FilePath -> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"reference linearization of" (Check (Maybe (L Type)) -> Check (Maybe (L Type)))
-> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a b. (a -> b) -> a -> b
$ do
                       (Type
ref,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
ref ([Type] -> Type -> Type
mkFunType [Type
typ] Type
typeStr)
                       Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
ref))
                (Maybe (L Type), Maybe (L Type))
_ -> Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
forall a. Maybe a
Nothing
      Maybe (L Type)
mpr  <- case Maybe (L Type)
mpr of
                (Just (L Location
loc Type
t)) ->
                    Location
-> FilePath -> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"print name of" (Check (Maybe (L Type)) -> Check (Maybe (L Type)))
-> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a b. (a -> b) -> a -> b
$ do
                       (Type
t,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
t Type
typeStr
                       Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
t))
                Maybe (L Type)
_ -> Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
forall a. Maybe a
Nothing
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe (L Type)
-> Maybe PMCFG
-> Info
CncCat Maybe (L Type)
mty Maybe (L Type)
mdef Maybe (L Type)
mref Maybe (L Type)
mpr Maybe PMCFG
mpmcfg)

    CncFun Maybe (Ident, Context, Type)
mty Maybe (L Type)
mt Maybe (L Type)
mpr Maybe PMCFG
mpmcfg -> do
      Maybe (L Type)
mt <- case (Maybe (Ident, Context, Type)
mty,Maybe (L Type)
mt) of
              (Just (Ident
cat,Context
cont,Type
val),Just (L Location
loc Type
trm)) ->
                  Location
-> FilePath -> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"linearization of" (Check (Maybe (L Type)) -> Check (Maybe (L Type)))
-> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a b. (a -> b) -> a -> b
$ do
                     (Type
trm,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
trm ([Type] -> Type -> Type
mkFunType ((Hypo -> Type) -> Context -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(BindType
_,Ident
_,Type
ty) -> Type
ty) Context
cont) Type
val)  -- erases arg vars
                     Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
trm))
              (Maybe (Ident, Context, Type), Maybe (L Type))
_ -> Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
mt
      Maybe (L Type)
mpr  <- case Maybe (L Type)
mpr of
                (Just (L Location
loc Type
t)) ->
                    Location
-> FilePath -> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"print name of" (Check (Maybe (L Type)) -> Check (Maybe (L Type)))
-> Check (Maybe (L Type)) -> Check (Maybe (L Type))
forall a b. (a -> b) -> a -> b
$ do
                       (Type
t,Type
_) <- SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
t Type
typeStr
                       Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc Type
t))
                Maybe (L Type)
_ -> Maybe (L Type) -> Check (Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (L Type)
forall a. Maybe a
Nothing
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Ident, Context, Type)
-> Maybe (L Type) -> Maybe (L Type) -> Maybe PMCFG -> Info
CncFun Maybe (Ident, Context, Type)
mty Maybe (L Type)
mt Maybe (L Type)
mpr Maybe PMCFG
mpmcfg)

    ResOper Maybe (L Type)
pty Maybe (L Type)
pde -> do
      (Maybe (L Type)
pty', Maybe (L Type)
pde') <- case (Maybe (L Type)
pty,Maybe (L Type)
pde) of
         (Just (L Location
loct Type
ty), Just (L Location
locd Type
de)) -> do
           Type
ty'     <- Location -> FilePath -> Check Type -> Check Type
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loct FilePath
"operation" (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$
                         (if Bool
False --flag optNewComp opts
                            then GlobalEnv -> Type -> Type -> Check (Type, Type)
CN.checkLType (Options -> SourceGrammar -> GlobalEnv
CN.resourceValues Options
opts SourceGrammar
gr) Type
ty Type
typeType Check (Type, Type) -> ((Type, Type) -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type)
-> ((Type, Type) -> Type) -> (Type, Type) -> Check Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalEnv -> L Ident -> Type -> Type
CN.normalForm (Options -> SourceGrammar -> GlobalEnv
CN.resourceValues Options
opts SourceGrammar
gr) (Location -> Ident -> L Ident
forall a. Location -> a -> L a
L Location
loct Ident
c) (Type -> Type) -> ((Type, Type) -> Type) -> (Type, Type) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> a
fst -- !!
                            else SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
ty Type
typeType Check (Type, Type) -> ((Type, Type) -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
gr [] (Type -> Check Type)
-> ((Type, Type) -> Type) -> (Type, Type) -> Check Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Type) -> Type
forall a b. (a, b) -> a
fst)
           (Type
de',Type
_) <- Location -> FilePath -> Check (Type, Type) -> Check (Type, Type)
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
locd FilePath
"operation" (Check (Type, Type) -> Check (Type, Type))
-> Check (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$
                         (if Bool
False -- flag optNewComp opts
                            then GlobalEnv -> Type -> Type -> Check (Type, Type)
CN.checkLType (Options -> SourceGrammar -> GlobalEnv
CN.resourceValues Options
opts SourceGrammar
gr) Type
de Type
ty'
                            else SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
de Type
ty')
           (Maybe (L Type), Maybe (L Type))
-> Check (Maybe (L Type), Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loct Type
ty'), L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
locd Type
de'))
         (Maybe (L Type)
Nothing         , Just (L Location
locd Type
de)) -> do
           (Type
de',Type
ty') <- Location -> FilePath -> Check (Type, Type) -> Check (Type, Type)
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
locd FilePath
"operation" (Check (Type, Type) -> Check (Type, Type))
-> Check (Type, Type) -> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$
                          (if Bool
False -- flag optNewComp opts
                            then GlobalEnv -> Type -> Check (Type, Type)
CN.inferLType (Options -> SourceGrammar -> GlobalEnv
CN.resourceValues Options
opts SourceGrammar
gr) Type
de
                            else SourceGrammar -> Context -> Type -> Check (Type, Type)
inferLType SourceGrammar
gr [] Type
de)
           (Maybe (L Type), Maybe (L Type))
-> Check (Maybe (L Type), Maybe (L Type))
forall (m :: * -> *) a. Monad m => a -> m a
return (L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
locd Type
ty'), L Type -> Maybe (L Type)
forall a. a -> Maybe a
Just (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
locd Type
de'))
         (Just (L Location
loct Type
ty), Maybe (L Type)
Nothing) -> do
           Location
-> FilePath
-> Check (Maybe (L Type), Maybe (L Type))
-> Check (Maybe (L Type), Maybe (L Type))
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loct FilePath
"operation" (Check (Maybe (L Type), Maybe (L Type))
 -> Check (Maybe (L Type), Maybe (L Type)))
-> Check (Maybe (L Type), Maybe (L Type))
-> Check (Maybe (L Type), Maybe (L Type))
forall a b. (a -> b) -> a -> b
$
             Doc -> Check (Maybe (L Type), Maybe (L Type))
forall a. Doc -> Check a
checkError (FilePath -> Doc
forall a. Pretty a => a -> Doc
pp FilePath
"No definition given to the operation")
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (L Type) -> Maybe (L Type) -> Info
ResOper Maybe (L Type)
pty' Maybe (L Type)
pde')

    ResOverload [ModuleName]
os [(L Type, L Type)]
tysts -> Location -> FilePath -> Check Info -> Check Info
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
NoLoc FilePath
"overloading" (Check Info -> Check Info) -> Check Info -> Check Info
forall a b. (a -> b) -> a -> b
$ do
      [(L Type, L Type)]
tysts' <- ((L Type, L Type) -> Check (L Type, L Type))
-> [(L Type, L Type)] -> Check [(L Type, L Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((L Type -> L Type -> Check (L Type, L Type))
-> (L Type, L Type) -> Check (L Type, L Type)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((L Type -> L Type -> Check (L Type, L Type))
 -> (L Type, L Type) -> Check (L Type, L Type))
-> (L Type -> L Type -> Check (L Type, L Type))
-> (L Type, L Type)
-> Check (L Type, L Type)
forall a b. (a -> b) -> a -> b
$ (L Type -> L Type -> Check (L Type, L Type))
-> L Type -> L Type -> Check (L Type, L Type)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (\(L Location
loc1 Type
t) (L Location
loc2 Type
ty) -> SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr [] Type
t Type
ty Check (Type, Type)
-> ((Type, Type) -> Check (L Type, L Type))
-> Check (L Type, L Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Type
t,Type
ty) -> (L Type, L Type) -> Check (L Type, L Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc1 Type
t, Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
loc2 Type
ty))) [(L Type, L Type)]
tysts  -- return explicit ones
      [([Type], (Type, Type))]
tysts0 <- SourceGrammar
-> (ModuleName, Ident) -> Check [([Type], (Type, Type))]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> (ModuleName, Ident) -> m [([Type], (Type, Type))]
lookupOverload SourceGrammar
gr (ModuleName
m,Ident
c)  -- check against inherited ones too
      [(Type, Type)]
tysts1 <- ((Type, Type) -> Check (Type, Type))
-> [(Type, Type)] -> Check [(Type, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Type -> Type -> Check (Type, Type))
-> (Type, Type) -> Check (Type, Type)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Type -> Type -> Check (Type, Type))
 -> (Type, Type) -> Check (Type, Type))
-> (Type -> Type -> Check (Type, Type))
-> (Type, Type)
-> Check (Type, Type)
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Check (Type, Type))
-> Type -> Type -> Check (Type, Type)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (SourceGrammar -> Context -> Type -> Type -> Check (Type, Type)
checkLType SourceGrammar
gr []))
                  [([Type] -> Type -> Type
mkFunType [Type]
args Type
val,Type
tr) | ([Type]
args,(Type
val,Type
tr)) <- [([Type], (Type, Type))]
tysts0]
      --- this can only be a partial guarantee, since matching
      --- with value type is only possible if expected type is given
      [[Type]] -> Check ()
checkUniq ([[Type]] -> Check ()) -> [[Type]] -> Check ()
forall a b. (a -> b) -> a -> b
$
        [[Type]] -> [[Type]]
forall a. Ord a => [a] -> [a]
sort [let (Context
xs,Type
t) = Type -> (Context, Type)
typeFormCnc Type
x in Type
t Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: (Hypo -> Type) -> Context -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(BindType
b,Ident
x,Type
t) -> Type
t) Context
xs | (Type
_,Type
x) <- [(Type, Type)]
tysts1]
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return ([ModuleName] -> [(L Type, L Type)] -> Info
ResOverload [ModuleName]
os [(L Type
y,L Type
x) | (L Type
x,L Type
y) <- [(L Type, L Type)]
tysts'])

    ResParam (Just (L Location
loc [Param]
pcs)) Maybe [Type]
_ -> do
      [Type]
ts <- Location -> FilePath -> Check [Type] -> Check [Type]
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc FilePath
"parameter type" (Check [Type] -> Check [Type]) -> Check [Type] -> Check [Type]
forall a b. (a -> b) -> a -> b
$
              ([[Type]] -> [Type]) -> Check [[Type]] -> Check [Type]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Check [[Type]] -> Check [Type]) -> Check [[Type]] -> Check [Type]
forall a b. (a -> b) -> a -> b
$ (Param -> Check [Type]) -> [Param] -> Check [[Type]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Param -> Check [Type]
forall (m :: * -> *) a b.
ErrorMonad m =>
(Ident, [(a, b, Type)]) -> m [Type]
mkPar [Param]
pcs
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (L [Param]) -> Maybe [Type] -> Info
ResParam (L [Param] -> Maybe (L [Param])
forall a. a -> Maybe a
Just (Location -> [Param] -> L [Param]
forall a. Location -> a -> L a
L Location
loc [Param]
pcs)) ([Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
ts))

    Info
_ ->  Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return Info
info
 where
   gr :: SourceGrammar
gr = SourceGrammar -> SourceModule -> SourceGrammar
prependModule SourceGrammar
sgr (ModuleName
m,ModuleInfo
mo)
   chIn :: Location -> a2 -> Check a3 -> Check a3
chIn Location
loc a2
cat = FilePath -> ModuleInfo -> Location -> Doc -> Check a3 -> Check a3
forall a1 a2 a3.
(Pretty a1, HasSourcePath a2) =>
FilePath -> a2 -> Location -> a1 -> Check a3 -> Check a3
checkInModule FilePath
cwd ModuleInfo
mo Location
loc (FilePath
"Happened in" FilePath -> a2 -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> a2
cat Doc -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c)

   mkPar :: (Ident, [(a, b, Type)]) -> m [Type]
mkPar (Ident
f,[(a, b, Type)]
co) = do
       [[Type]]
vs <- ([[Type]] -> [[Type]]) -> m [[Type]] -> m [[Type]]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[Type]] -> [[Type]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (m [[Type]] -> m [[Type]]) -> m [[Type]] -> m [[Type]]
forall a b. (a -> b) -> a -> b
$ ((a, b, Type) -> m [Type]) -> [(a, b, Type)] -> m [[Type]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(a
_,b
_,Type
ty) -> SourceGrammar -> Type -> m [Type]
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> Type -> m [Type]
allParamValues SourceGrammar
gr Type
ty) [(a, b, Type)]
co
       [Type] -> m [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> m [Type]) -> [Type] -> m [Type]
forall a b. (a -> b) -> a -> b
$ ([Type] -> Type) -> [[Type]] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> [Type] -> Type
mkApp ((ModuleName, Ident) -> Type
QC (ModuleName
m,Ident
f))) [[Type]]
vs

   checkUniq :: [[Type]] -> Check ()
checkUniq [[Type]]
xss = case [[Type]]
xss of
     [Type]
x:[Type]
y:[[Type]]
xs
      | [Type]
x [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type]
y    -> Doc -> Check ()
forall a. Doc -> Check a
checkError (Doc -> Check ()) -> Doc -> Check ()
forall a b. (a -> b) -> a -> b
$ FilePath
"ambiguous for type" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>
                                  Type -> Doc
ppType ([Type] -> Type -> Type
mkFunType ([Type] -> [Type]
forall a. [a] -> [a]
tail [Type]
x) ([Type] -> Type
forall a. [a] -> a
head [Type]
x))
      | Bool
otherwise -> [[Type]] -> Check ()
checkUniq ([[Type]] -> Check ()) -> [[Type]] -> Check ()
forall a b. (a -> b) -> a -> b
$ [Type]
y[Type] -> [[Type]] -> [[Type]]
forall a. a -> [a] -> [a]
:[[Type]]
xs
     [[Type]]
_ -> () -> Check ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

   mkCheck :: Location -> a2 -> [a] -> Check Info
mkCheck Location
loc a2
cat [a]
ss = case [a]
ss of
     [] -> Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return Info
info
     [a]
_ -> Location -> a2 -> Check Info -> Check Info
forall a2 a3. Pretty a2 => Location -> a2 -> Check a3 -> Check a3
chIn Location
loc a2
cat (Check Info -> Check Info) -> Check Info -> Check Info
forall a b. (a -> b) -> a -> b
$ Doc -> Check Info
forall a. Doc -> Check a
checkError ([a] -> Doc
forall a. Pretty a => [a] -> Doc
vcat [a]
ss)

   compAbsTyp :: [(Ident, Type)] -> Type -> Check Type
compAbsTyp [(Ident, Type)]
g Type
t = case Type
t of
     Vr Ident
x -> Check Type -> (Type -> Check Type) -> Maybe Type -> Check Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc -> Check Type
forall a. Doc -> Check a
checkError (FilePath
"no value given to variable" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
x)) Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> Check Type) -> Maybe Type -> Check Type
forall a b. (a -> b) -> a -> b
$ Ident -> [(Ident, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
x [(Ident, Type)]
g
     Let (Ident
x,(Maybe Type
_,Type
a)) Type
b -> do
       Type
a' <- [(Ident, Type)] -> Type -> Check Type
compAbsTyp [(Ident, Type)]
g Type
a
       [(Ident, Type)] -> Type -> Check Type
compAbsTyp ((Ident
x, Type
a')(Ident, Type) -> [(Ident, Type)] -> [(Ident, Type)]
forall a. a -> [a] -> [a]
:[(Ident, Type)]
g) Type
b
     Prod BindType
b Ident
x Type
a Type
t -> do
       Type
a' <- [(Ident, Type)] -> Type -> Check Type
compAbsTyp [(Ident, Type)]
g Type
a
       Type
t' <- [(Ident, Type)] -> Type -> Check Type
compAbsTyp ((Ident
x,Ident -> Type
Vr Ident
x)(Ident, Type) -> [(Ident, Type)] -> [(Ident, Type)]
forall a. a -> [a] -> [a]
:[(Ident, Type)]
g) Type
t
       Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Check Type) -> Type -> Check Type
forall a b. (a -> b) -> a -> b
$ BindType -> Ident -> Type -> Type -> Type
Prod BindType
b Ident
x Type
a' Type
t'
     Abs BindType
_ Ident
_ Type
_ -> Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
     Type
_ -> (Type -> Check Type) -> Type -> Check Type
forall (m :: * -> *). Monad m => (Type -> m Type) -> Type -> m Type
composOp ([(Ident, Type)] -> Type -> Check Type
compAbsTyp [(Ident, Type)]
g) Type
t


-- | for grammars obtained otherwise than by parsing ---- update!!
checkReservedId :: Ident -> Check ()
checkReservedId :: Ident -> Check ()
checkReservedId Ident
x =
  Bool -> Check () -> Check ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident -> Bool
isReservedWord Ident
x) (Check () -> Check ()) -> Check () -> Check ()
forall a b. (a -> b) -> a -> b
$
       Doc -> Check ()
checkWarn (FilePath
"reserved word used as identifier:" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
x)

-- auxiliaries

-- | linearization types and defaults
linTypeOfType :: Grammar -> ModuleName -> Type -> Check (Context,Type)
linTypeOfType :: SourceGrammar -> ModuleName -> Type -> Check (Context, Type)
linTypeOfType SourceGrammar
cnc ModuleName
m Type
typ = do
  let ([(Int, (ModuleName, Ident))]
cont,(ModuleName, Ident)
cat) = Type -> ([(Int, (ModuleName, Ident))], (ModuleName, Ident))
typeSkeleton Type
typ
  Type
val  <- (ModuleName, Ident) -> Check Type
forall a. (a, Ident) -> Check Type
lookLin (ModuleName, Ident)
cat
  Context
args <- ((Int, (Int, (ModuleName, Ident))) -> Check Hypo)
-> [(Int, (Int, (ModuleName, Ident)))] -> Check Context
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Int, (Int, (ModuleName, Ident))) -> Check Hypo
forall a. (Int, (Int, (a, Ident))) -> Check Hypo
mkLinArg ([Int]
-> [(Int, (ModuleName, Ident))]
-> [(Int, (Int, (ModuleName, Ident)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(Int, (ModuleName, Ident))]
cont)
  (Context, Type) -> Check (Context, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Context
args, Type
val)
 where
   mkLinArg :: (Int, (Int, (a, Ident))) -> Check Hypo
mkLinArg (Int
i,(Int
n,mc :: (a, Ident)
mc@(a
m,Ident
cat))) = do
     Type
val  <- (a, Ident) -> Check Type
forall a. (a, Ident) -> Check Type
lookLin (a, Ident)
mc
     let vars :: Type
vars = (Int -> Label) -> [Type] -> Type
mkRecType Int -> Label
varLabel ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> [Type]
forall a. Int -> a -> [a]
replicate Int
n Type
typeStr
         symb :: Ident
symb = Int -> Ident -> Int -> Ident
argIdent Int
n Ident
cat Int
i
     Type
rec <- if Int
nInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 then Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
val else
                       FilePath -> Check Type -> Check Type
forall (m :: * -> *) a. ErrorMonad m => FilePath -> m a -> m a
errIn (Doc -> FilePath
forall a. Pretty a => a -> FilePath
render (FilePath
"extending" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                                      Int -> Type -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 Type
vars Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                                      FilePath
"with" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                                      Int -> Type -> Doc
forall a. Pretty a => Int -> a -> Doc
nest Int
2 Type
val)) (Check Type -> Check Type) -> Check Type -> Check Type
forall a b. (a -> b) -> a -> b
$
                             Type -> Type -> Check Type
forall (m :: * -> *). ErrorMonad m => Type -> Type -> m Type
plusRecType Type
vars Type
val
     Hypo -> Check Hypo
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType
Explicit,Ident
symb,Type
rec)
   lookLin :: (a, Ident) -> Check Type
lookLin (a
_,Ident
c) = [Check Type] -> Check Type
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [ --- rather: update with defLinType ?
      SourceGrammar -> ModuleName -> Ident -> Check Type
forall (m :: * -> *).
ErrorMonad m =>
SourceGrammar -> ModuleName -> Ident -> m Type
lookupLincat SourceGrammar
cnc ModuleName
m Ident
c Check Type -> (Type -> Check Type) -> Check Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SourceGrammar -> Context -> Type -> Check Type
computeLType SourceGrammar
cnc []
     ,Type -> Check Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
defLinType
     ]