{-# LANGUAGE PatternGuards #-}
----------------------------------------------------------------------
-- |
-- Module      : Lookup
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/10/27 13:21:53 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.15 $
--
-- Lookup in source (concrete and resource) when compiling.
--
-- lookup in resource and concrete in compiling; for abstract, use 'Look'
-----------------------------------------------------------------------------

module GF.Grammar.Lookup (
           lookupIdent,
           lookupOrigInfo,
           allOrigInfos,
           lookupResDef, lookupResDefLoc,
           lookupResType,
           lookupOverload,
           lookupOverloadTypes,
           lookupParamValues,
           allParamValues,
           lookupAbsDef,
           lookupLincat,
           lookupFunType,
           lookupCatContext,
           allOpers, allOpersTo
          ) where

import GF.Data.Operations
import GF.Infra.Ident
import GF.Grammar.Macros
import GF.Grammar.Grammar
import GF.Grammar.Printer
import GF.Grammar.Predef
import GF.Grammar.Lockfield

import Data.List (sortBy)
--import Data.Maybe (maybe)
--import Control.Monad
import GF.Text.Pretty
import qualified Data.Map as Map

-- whether lock fields are added in reuse
lock :: Ident -> Type -> m Type
lock Ident
c = Ident -> Type -> m Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lockRecType Ident
c -- return
unlock :: Ident -> Type -> m Type
unlock Ident
c = Ident -> Type -> m Type
forall (m :: * -> *). Monad m => Ident -> Type -> m Type
unlockRecord Ident
c -- return

-- to look up a constant etc in a search tree --- why here? AR 29/5/2008
lookupIdent :: ErrorMonad m => Ident -> Map.Map Ident b -> m b
lookupIdent :: Ident -> Map Ident b -> m b
lookupIdent Ident
c Map Ident b
t =
  case Ident -> Map Ident b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
c Map Ident b
t of
    Just b
v  -> b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
v
    Maybe b
Nothing -> String -> m b
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (String
"unknown identifier" String -> String -> String
+++ Ident -> String
showIdent Ident
c)

lookupIdentInfo :: ErrorMonad m => SourceModInfo -> Ident -> m Info
lookupIdentInfo :: SourceModInfo -> Ident -> m Info
lookupIdentInfo SourceModInfo
mo Ident
i = Ident -> Map Ident Info -> m Info
forall (m :: * -> *) b. ErrorMonad m => Ident -> Map Ident b -> m b
lookupIdent Ident
i (SourceModInfo -> Map Ident Info
jments SourceModInfo
mo)

lookupQIdentInfo :: ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo :: Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c) = (SourceModInfo -> Ident -> m Info)
-> Ident -> SourceModInfo -> m Info
forall a b c. (a -> b -> c) -> b -> a -> c
flip SourceModInfo -> Ident -> m Info
forall (m :: * -> *).
ErrorMonad m =>
SourceModInfo -> Ident -> m Info
lookupIdentInfo Ident
c (SourceModInfo -> m Info) -> m SourceModInfo -> m Info
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Grammar -> ModuleName -> m SourceModInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m SourceModInfo
lookupModule Grammar
gr ModuleName
m

lookupResDef :: ErrorMonad m => Grammar -> QIdent -> m Term
lookupResDef :: Grammar -> QIdent -> m Type
lookupResDef Grammar
gr QIdent
x = (L Type -> Type) -> m (L Type) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Type -> Type
forall a. L a -> a
unLoc (Grammar -> QIdent -> m (L Type)
forall (f :: * -> *).
ErrorMonad f =>
Grammar -> QIdent -> f (L Type)
lookupResDefLoc Grammar
gr QIdent
x)

lookupResDefLoc :: Grammar -> QIdent -> f (L Type)
lookupResDefLoc Grammar
gr (ModuleName
m,Ident
c)
  | Ident -> Bool
isPredefCat Ident
c = (Type -> L Type) -> f Type -> f (L Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> L Type
forall a. a -> L a
noLoc (Ident -> Type -> f Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lock Ident
c Type
defLinType)
  | Bool
otherwise     = ModuleName -> Ident -> f (L Type)
forall (m :: * -> *).
ErrorMonad m =>
ModuleName -> Ident -> m (L Type)
look ModuleName
m Ident
c
  where
    look :: ModuleName -> Ident -> m (L Type)
look ModuleName
m Ident
c = do
      Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
      case Info
info of
        ResOper Maybe (L Type)
_ (Just L Type
lt) -> L Type -> m (L Type)
forall (m :: * -> *) a. Monad m => a -> m a
return L Type
lt
        ResOper Maybe (L Type)
_ Maybe (L Type)
Nothing  -> L Type -> m (L Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> L Type
forall a. a -> L a
noLoc (QIdent -> Type
Q (ModuleName
m,Ident
c)))
        CncCat (Just (L Location
l Type
ty)) Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> (Type -> L Type) -> m Type -> m (L Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
l) (Ident -> Type -> m Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lock Ident
c Type
ty)
        CncCat Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_         -> (Type -> L Type) -> m Type -> m (L Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> L Type
forall a. a -> L a
noLoc (Ident -> Type -> m Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lock Ident
c Type
defLinType)

        CncFun (Just (Ident
cat,Context
_,Type
_)) (Just (L Location
l Type
tr)) Maybe (L Type)
_ Maybe PMCFG
_ -> (Type -> L Type) -> m Type -> m (L Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
l) (Ident -> Type -> m Type
forall (m :: * -> *). Monad m => Ident -> Type -> m Type
unlock Ident
cat Type
tr)
        CncFun Maybe (Ident, Context, Type)
_                (Just L Type
ltr) Maybe (L Type)
_ Maybe PMCFG
_ -> L Type -> m (L Type)
forall (m :: * -> *) a. Monad m => a -> m a
return L Type
ltr

        AnyInd Bool
_ ModuleName
n        -> ModuleName -> Ident -> m (L Type)
look ModuleName
n Ident
c
        ResParam Maybe (L [Param])
_ Maybe [Type]
_      -> L Type -> m (L Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> L Type
forall a. a -> L a
noLoc (QIdent -> Type
QC (ModuleName
m,Ident
c)))
        ResValue L Type
_        -> L Type -> m (L Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> L Type
forall a. a -> L a
noLoc (QIdent -> Type
QC (ModuleName
m,Ident
c)))
        Info
_   -> String -> m (L Type)
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (String -> m (L Type)) -> String -> m (L Type)
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (Ident
c Ident -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"is not defined in resource" Doc -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
m)

lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type
lookupResType :: Grammar -> QIdent -> m Type
lookupResType Grammar
gr (ModuleName
m,Ident
c) = do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    ResOper (Just (L Location
_ Type
t)) Maybe (L Type)
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t

    -- used in reused concrete
    CncCat Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typeType
    CncFun (Just (Ident
cat,Context
cont,Type
val)) Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> do
          Type
val' <- Ident -> Type -> m Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lock Ident
cat Type
val
          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
$ Context -> Type -> [Type] -> Type
mkProd Context
cont Type
val' []
    AnyInd Bool
_ ModuleName
n        -> Grammar -> QIdent -> m Type
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Type
lookupResType Grammar
gr (ModuleName
n,Ident
c)
    ResParam Maybe (L [Param])
_ Maybe [Type]
_      -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typePType
    ResValue (L Location
_ Type
t)  -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    Info
_   -> String -> m Type
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (Ident
c Ident -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"has no type defined in resource" Doc -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
m)

lookupOverloadTypes :: ErrorMonad m => Grammar -> QIdent -> m [(Term,Type)]
lookupOverloadTypes :: Grammar -> QIdent -> m [(Type, Type)]
lookupOverloadTypes Grammar
gr id :: QIdent
id@(ModuleName
m,Ident
c) = do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    ResOper (Just (L Location
_ Type
ty)) Maybe (L Type)
_ -> Type -> m [(Type, Type)]
forall (m :: * -> *) b. Monad m => b -> m [(Type, b)]
ret Type
ty

    -- used in reused concrete
    CncCat Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> Type -> m [(Type, Type)]
forall (m :: * -> *) b. Monad m => b -> m [(Type, b)]
ret Type
typeType
    CncFun (Just (Ident
cat,Context
cont,Type
val)) Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> do
          Type
val' <- Ident -> Type -> m Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lock Ident
cat Type
val
          Type -> m [(Type, Type)]
forall (m :: * -> *) b. Monad m => b -> m [(Type, b)]
ret (Type -> m [(Type, Type)]) -> Type -> m [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ Context -> Type -> [Type] -> Type
mkProd Context
cont Type
val' []
    ResParam Maybe (L [Param])
_ Maybe [Type]
_      -> Type -> m [(Type, Type)]
forall (m :: * -> *) b. Monad m => b -> m [(Type, b)]
ret Type
typePType
    ResValue (L Location
_ Type
t)  -> Type -> m [(Type, Type)]
forall (m :: * -> *) b. Monad m => b -> m [(Type, b)]
ret Type
t
    ResOverload [ModuleName]
os [(L Type, L Type)]
tysts -> do
            [[(Type, Type)]]
tss <- (ModuleName -> m [(Type, Type)])
-> [ModuleName] -> m [[(Type, Type)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ModuleName
x -> Grammar -> QIdent -> m [(Type, Type)]
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m [(Type, Type)]
lookupOverloadTypes Grammar
gr (ModuleName
x,Ident
c)) [ModuleName]
os
            [(Type, Type)] -> m [(Type, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Type, Type)] -> m [(Type, Type)])
-> [(Type, Type)] -> m [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ [(Type
tr,Type
ty) | (L Location
_ Type
ty,L Location
_ Type
tr) <- [(L Type, L Type)]
tysts] [(Type, Type)] -> [(Type, Type)] -> [(Type, Type)]
forall a. [a] -> [a] -> [a]
++
                     [[(Type, Type)]] -> [(Type, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Type)]]
tss
    AnyInd Bool
_ ModuleName
n   -> Grammar -> QIdent -> m [(Type, Type)]
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m [(Type, Type)]
lookupOverloadTypes Grammar
gr (ModuleName
n,Ident
c)
    Info
_            -> String -> m [(Type, Type)]
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (String -> m [(Type, Type)]) -> String -> m [(Type, Type)]
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (Ident
c Ident -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"has no types defined in resource" Doc -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
m)
  where
    ret :: b -> m [(Type, b)]
ret b
ty = [(Type, b)] -> m [(Type, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(QIdent -> Type
Q QIdent
id,b
ty)]

lookupOverload :: ErrorMonad m => Grammar -> QIdent -> m [([Type],(Type,Term))]
lookupOverload :: Grammar -> QIdent -> m [([Type], (Type, Type))]
lookupOverload Grammar
gr (ModuleName
m,Ident
c) = do
    Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
    case Info
info of
      ResOverload [ModuleName]
os [(L Type, L Type)]
tysts -> do
            [[([Type], (Type, Type))]]
tss <- (ModuleName -> m [([Type], (Type, Type))])
-> [ModuleName] -> m [[([Type], (Type, Type))]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ModuleName
x -> Grammar -> QIdent -> m [([Type], (Type, Type))]
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m [([Type], (Type, Type))]
lookupOverload Grammar
gr (ModuleName
x,Ident
c)) [ModuleName]
os
            [([Type], (Type, Type))] -> m [([Type], (Type, Type))]
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Type], (Type, Type))] -> m [([Type], (Type, Type))])
-> [([Type], (Type, Type))] -> m [([Type], (Type, Type))]
forall a b. (a -> b) -> a -> b
$ [let (Context
args,Type
val) = Type -> (Context, Type)
typeFormCnc Type
ty in (((BindType, Ident, Type) -> Type) -> Context -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(BindType
b,Ident
x,Type
t) -> Type
t) Context
args,(Type
val,Type
tr)) |
                      (L Location
_ Type
ty,L Location
_ Type
tr) <- [(L Type, L Type)]
tysts] [([Type], (Type, Type))]
-> [([Type], (Type, Type))] -> [([Type], (Type, Type))]
forall a. [a] -> [a] -> [a]
++
                     [[([Type], (Type, Type))]] -> [([Type], (Type, Type))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[([Type], (Type, Type))]]
tss

      AnyInd Bool
_ ModuleName
n  -> Grammar -> QIdent -> m [([Type], (Type, Type))]
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m [([Type], (Type, Type))]
lookupOverload Grammar
gr (ModuleName
n,Ident
c)
      Info
_   -> String -> m [([Type], (Type, Type))]
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (String -> m [([Type], (Type, Type))])
-> String -> m [([Type], (Type, Type))]
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (Ident
c Ident -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"is not an overloaded operation")

-- | returns the original 'Info' and the module where it was found
lookupOrigInfo :: ErrorMonad m => Grammar -> QIdent -> m (ModuleName,Info)
lookupOrigInfo :: Grammar -> QIdent -> m (ModuleName, Info)
lookupOrigInfo Grammar
gr (ModuleName
m,Ident
c) = do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    AnyInd Bool
_ ModuleName
n  -> Grammar -> QIdent -> m (ModuleName, Info)
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m (ModuleName, Info)
lookupOrigInfo Grammar
gr (ModuleName
n,Ident
c)
    Info
i           -> (ModuleName, Info) -> m (ModuleName, Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName
m,Info
i)

allOrigInfos :: Grammar -> ModuleName -> [(QIdent,Info)]
allOrigInfos :: Grammar -> ModuleName -> [(QIdent, Info)]
allOrigInfos Grammar
gr ModuleName
m = [(QIdent, Info)] -> Err [(QIdent, Info)] -> [(QIdent, Info)]
forall a. a -> Err a -> a
fromErr [] (Err [(QIdent, Info)] -> [(QIdent, Info)])
-> Err [(QIdent, Info)] -> [(QIdent, Info)]
forall a b. (a -> b) -> a -> b
$ do
  SourceModInfo
mo <- Grammar -> ModuleName -> Err SourceModInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m SourceModInfo
lookupModule Grammar
gr ModuleName
m
  [(QIdent, Info)] -> Err [(QIdent, Info)]
forall (m :: * -> *) a. Monad m => a -> m a
return [((ModuleName
m,Ident
c),Info
i) | (Ident
c,Info
_) <- Map Ident Info -> [(Ident, Info)]
forall k a. Map k a -> [(k, a)]
Map.toList (SourceModInfo -> Map Ident Info
jments SourceModInfo
mo), Ok (ModuleName
m,Info
i) <- [Grammar -> QIdent -> Err (ModuleName, Info)
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m (ModuleName, Info)
lookupOrigInfo Grammar
gr (ModuleName
m,Ident
c)]]

lookupParamValues :: ErrorMonad m => Grammar -> QIdent -> m [Term]
lookupParamValues :: Grammar -> QIdent -> m [Type]
lookupParamValues Grammar
gr QIdent
c = do
  (ModuleName
_,Info
info) <- Grammar -> QIdent -> m (ModuleName, Info)
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> QIdent -> m (ModuleName, Info)
lookupOrigInfo Grammar
gr QIdent
c
  case Info
info of
    ResParam Maybe (L [Param])
_ (Just [Type]
pvs) -> [Type] -> m [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type]
pvs
    Info
_                     -> String -> m [Type]
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (String -> m [Type]) -> String -> m [Type]
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (TermPrintQual -> QIdent -> Doc
ppQIdent TermPrintQual
Qualified QIdent
c Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"has no parameter values defined")

allParamValues :: ErrorMonad m => Grammar -> Type -> m [Term]
allParamValues :: Grammar -> Type -> m [Type]
allParamValues Grammar
cnc Type
ptyp =
  case Type
ptyp of
    Type
_ | Just Int
n <- Type -> Maybe Int
isTypeInts Type
ptyp -> [Type] -> m [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int -> Type
EInt Int
i | Int
i <- [Int
0..Int
n]]
    QC QIdent
c -> Grammar -> QIdent -> m [Type]
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m [Type]
lookupParamValues Grammar
cnc QIdent
c
    Q  QIdent
c -> Grammar -> QIdent -> m Type
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Type
lookupResDef Grammar
cnc QIdent
c m Type -> (Type -> m [Type]) -> m [Type]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Grammar -> Type -> m [Type]
forall (m :: * -> *). ErrorMonad m => Grammar -> Type -> m [Type]
allParamValues Grammar
cnc
    RecType [Labelling]
r -> do
       let ([Label]
ls,[Type]
tys) = [Labelling] -> ([Label], [Type])
forall a b. [(a, b)] -> ([a], [b])
unzip ([Labelling] -> ([Label], [Type]))
-> [Labelling] -> ([Label], [Type])
forall a b. (a -> b) -> a -> b
$ [Labelling] -> [Labelling]
forall b. [(Label, b)] -> [(Label, b)]
sortByFst [Labelling]
r
       [[Type]]
tss <- (Type -> m [Type]) -> [Type] -> m [[Type]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Grammar -> Type -> m [Type]
forall (m :: * -> *). ErrorMonad m => Grammar -> Type -> m [Type]
allParamValues Grammar
cnc) [Type]
tys
       [Type] -> m [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [[Assign] -> Type
R ([Label] -> [Type] -> [Assign]
zipAssign [Label]
ls [Type]
ts) | [Type]
ts <- [[Type]] -> [[Type]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Type]]
tss]
    Table Type
pt Type
vt -> do
       [Type]
pvs <- Grammar -> Type -> m [Type]
forall (m :: * -> *). ErrorMonad m => Grammar -> Type -> m [Type]
allParamValues Grammar
cnc Type
pt
       [Type]
vvs <- Grammar -> Type -> m [Type]
forall (m :: * -> *). ErrorMonad m => Grammar -> Type -> m [Type]
allParamValues Grammar
cnc Type
vt
       [Type] -> m [Type]
forall (m :: * -> *) a. Monad m => a -> m a
return [Type -> [Type] -> Type
V Type
pt [Type]
ts | [Type]
ts <- [[Type]] -> [[Type]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Int -> [Type] -> [[Type]]
forall a. Int -> a -> [a]
replicate ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
pvs) [Type]
vvs)]
    Type
_ -> String -> m [Type]
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"cannot find parameter values for" String -> Type -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Type
ptyp))
  where
    -- to normalize records and record types
    sortByFst :: [(Label, b)] -> [(Label, b)]
sortByFst = ((Label, b) -> (Label, b) -> Ordering)
-> [(Label, b)] -> [(Label, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\ (Label, b)
x (Label, b)
y -> Label -> Label -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((Label, b) -> Label
forall a b. (a, b) -> a
fst (Label, b)
x) ((Label, b) -> Label
forall a b. (a, b) -> a
fst (Label, b)
y))

lookupAbsDef :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m (Maybe Int,Maybe [Equation])
lookupAbsDef :: Grammar -> ModuleName -> Ident -> m (Maybe Int, Maybe [Equation])
lookupAbsDef Grammar
gr ModuleName
m Ident
c = String
-> m (Maybe Int, Maybe [Equation])
-> m (Maybe Int, Maybe [Equation])
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (Doc -> String
forall a. Pretty a => a -> String
render (String
"looking up absdef of" String -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c)) (m (Maybe Int, Maybe [Equation])
 -> m (Maybe Int, Maybe [Equation]))
-> m (Maybe Int, Maybe [Equation])
-> m (Maybe Int, Maybe [Equation])
forall a b. (a -> b) -> a -> b
$ do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    AbsFun Maybe (L Type)
_ Maybe Int
a Maybe [L Equation]
d Maybe Bool
_ -> (Maybe Int, Maybe [Equation]) -> m (Maybe Int, Maybe [Equation])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int
a,([L Equation] -> [Equation])
-> Maybe [L Equation] -> Maybe [Equation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((L Equation -> Equation) -> [L Equation] -> [Equation]
forall a b. (a -> b) -> [a] -> [b]
map L Equation -> Equation
forall a. L a -> a
unLoc) Maybe [L Equation]
d)
    AnyInd Bool
_ ModuleName
n     -> Grammar -> ModuleName -> Ident -> m (Maybe Int, Maybe [Equation])
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> Ident -> m (Maybe Int, Maybe [Equation])
lookupAbsDef Grammar
gr ModuleName
n Ident
c
    Info
_              -> (Maybe Int, Maybe [Equation]) -> m (Maybe Int, Maybe [Equation])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int
forall a. Maybe a
Nothing,Maybe [Equation]
forall a. Maybe a
Nothing)

lookupLincat :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type
lookupLincat :: Grammar -> ModuleName -> Ident -> m Type
lookupLincat Grammar
gr ModuleName
m Ident
c | Ident -> Bool
isPredefCat Ident
c = Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
defLinType --- ad hoc; not needed?
lookupLincat Grammar
gr ModuleName
m Ident
c = do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    CncCat (Just (L Location
_ Type
t)) Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    AnyInd Bool
_ ModuleName
n                    -> Grammar -> ModuleName -> Ident -> m Type
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> Ident -> m Type
lookupLincat Grammar
gr ModuleName
n Ident
c
    Info
_                             -> String -> m Type
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (Ident
c Ident -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"has no linearization type in" Doc -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
m))

-- | this is needed at compile time
lookupFunType :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type
lookupFunType :: Grammar -> ModuleName -> Ident -> m Type
lookupFunType Grammar
gr ModuleName
m Ident
c = do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    AbsFun (Just (L Location
_ Type
t)) Maybe Int
_ Maybe [L Equation]
_ Maybe Bool
_ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    AnyInd Bool
_ ModuleName
n                  -> Grammar -> ModuleName -> Ident -> m Type
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> Ident -> m Type
lookupFunType Grammar
gr ModuleName
n Ident
c
    Info
_                           -> String -> m Type
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"cannot find type of" String -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c))

-- | this is needed at compile time
lookupCatContext :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Context
lookupCatContext :: Grammar -> ModuleName -> Ident -> m Context
lookupCatContext Grammar
gr ModuleName
m Ident
c = do
  Info
info <- Grammar -> QIdent -> m Info
forall (m :: * -> *). ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo Grammar
gr (ModuleName
m,Ident
c)
  case Info
info of
    AbsCat (Just (L Location
_ Context
co)) -> Context -> m Context
forall (m :: * -> *) a. Monad m => a -> m a
return Context
co
    AnyInd Bool
_ ModuleName
n             -> Grammar -> ModuleName -> Ident -> m Context
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> Ident -> m Context
lookupCatContext Grammar
gr ModuleName
n Ident
c
    Info
_                      -> String -> m Context
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"unknown category" String -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c))


-- this gives all opers and param constructors, also overloaded opers and funs, and the types, and locations
-- notice that it only gives the modules that are reachable and the opers that are included

allOpers :: Grammar -> [(QIdent,Type,Location)]
allOpers :: Grammar -> [(QIdent, Type, Location)]
allOpers Grammar
gr =
  [((ModuleName
m,Ident
op),Type
typ,Location
loc) |
      (ModuleName
m,SourceModInfo
mi)  <- [(ModuleName, SourceModInfo)]
-> (ModuleName -> [(ModuleName, SourceModInfo)])
-> Maybe ModuleName
-> [(ModuleName, SourceModInfo)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Grammar -> ModuleName -> [(ModuleName, SourceModInfo)]
allExtends Grammar
gr) (Grammar -> Maybe ModuleName
greatestResource Grammar
gr),
      (Ident
op,Info
info)  <- Map Ident Info -> [(Ident, Info)]
forall k a. Map k a -> [(k, a)]
Map.toList (SourceModInfo -> Map Ident Info
jments SourceModInfo
mi),
      L Location
loc Type
typ  <- Info -> [L Type]
typesIn Info
info
  ]
  where
    typesIn :: Info -> [L Type]
typesIn Info
info = case Info
info of
      AbsFun  (Just L Type
ltyp) Maybe Int
_ Maybe [L Equation]
_ Maybe Bool
_ -> [L Type
ltyp]
      ResOper (Just L Type
ltyp) Maybe (L Type)
_     -> [L Type
ltyp]
      ResValue L Type
ltyp             -> [L Type
ltyp]
      ResOverload [ModuleName]
_ [(L Type, L Type)]
tytrs       -> [L Type
ltyp | (L Type
ltyp,L Type
_) <- [(L Type, L Type)]
tytrs]
      CncFun  (Just (Ident
i,Context
ctx,Type
typ)) Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ ->
                                   [Location -> Type -> L Type
forall a. Location -> a -> L a
L Location
NoLoc (Context -> Type -> Type
mkProdSimple Context
ctx (Ident -> Type -> Type
lock' Ident
i Type
typ))]
      Info
_                         -> []

    lock' :: Ident -> Type -> Type
lock' Ident
i Type
typ = case Ident -> Type -> Err Type
forall (m :: * -> *). ErrorMonad m => Ident -> Type -> m Type
lock Ident
i Type
typ of
                    Ok Type
t -> Type
t
                    Err Type
_ -> Type
typ

--- not for dependent types
allOpersTo :: Grammar -> Type -> [(QIdent,Type,Location)]
allOpersTo :: Grammar -> Type -> [(QIdent, Type, Location)]
allOpersTo Grammar
gr Type
ty = [(QIdent, Type, Location)
op | op :: (QIdent, Type, Location)
op@(QIdent
_,Type
typ,Location
_) <- Grammar -> [(QIdent, Type, Location)]
allOpers Grammar
gr, Type -> Type -> Bool
isProdTo Type
ty Type
typ] where
  isProdTo :: Type -> Type -> Bool
isProdTo Type
t Type
typ = Type -> Type -> Bool
eqProd Type
typ Type
t Bool -> Bool -> Bool
|| case Type
typ of
    Prod BindType
_ Ident
_ Type
a Type
b -> Type -> Type -> Bool
isProdTo Type
t Type
b
    Type
_ -> Bool
False
  eqProd :: Type -> Type -> Bool
eqProd Type
f Type
g = case (Type
f,Type
g) of
    (Prod BindType
_ Ident
_ Type
a1 Type
b1, Prod BindType
_ Ident
_ Type
a2 Type
b2) -> Type -> Type -> Bool
eqProd Type
a1 Type
a2 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqProd Type
b1 Type
b2
    (Type, Type)
_ -> Type
f Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
g