module GF.Compile.CheckGrammar(checkModule) where
import Prelude hiding ((<>))
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
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)})
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]
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]]
((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
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)
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
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
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
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
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)
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
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
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
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
[([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)
[(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]
[[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
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)
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 [
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
]