----------------------------------------------------------------------
-- |
-- Module      : Rename
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/05/30 18:39:44 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.19 $
--
-- AR 14\/5\/2003
-- The top-level function 'renameGrammar' does several things:
--
--   - extends each module symbol table by indirections to extended module
--
--   - changes unqualified and as-qualified imports to absolutely qualified
--
--   - goes through the definitions and resolves names
--
-- Dependency analysis between modules has been performed before this pass.
-- Hence we can proceed by @fold@ing "from left to right".
-----------------------------------------------------------------------------

module GF.Compile.Rename (
     renameSourceTerm,
     renameModule
    ) where

import GF.Infra.Ident
import GF.Infra.CheckM
import GF.Grammar.Grammar
import GF.Grammar.Values
import GF.Grammar.Predef
import GF.Grammar.Lookup
import GF.Grammar.Macros
import GF.Grammar.Printer
import GF.Data.Operations

import Control.Monad
import Data.List (nub,(\\))
import qualified Data.List as L
import qualified Data.Map as Map
import Data.Maybe(mapMaybe)
import GF.Text.Pretty

-- | this gives top-level access to renaming term input in the cc command
renameSourceTerm :: Grammar -> ModuleName -> Term -> Check Term
renameSourceTerm :: Grammar -> ModuleName -> Term -> Check Term
renameSourceTerm Grammar
g ModuleName
m Term
t = do
  ModuleInfo
mi     <- Grammar -> ModuleName -> Check ModuleInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m ModuleInfo
lookupModule Grammar
g ModuleName
m
  Status
status <- FilePath -> Grammar -> Module -> Check Status
buildStatus FilePath
"" Grammar
g (ModuleName
m,ModuleInfo
mi)
  Status -> [Ident] -> Term -> Check Term
renameTerm Status
status [] Term
t

renameModule :: FilePath -> Grammar -> Module -> Check Module
renameModule :: FilePath -> Grammar -> Module -> Check Module
renameModule FilePath
cwd Grammar
gr mo :: Module
mo@(ModuleName
m,ModuleInfo
mi) = do
  Status
status <- FilePath -> Grammar -> Module -> Check Status
buildStatus FilePath
cwd Grammar
gr Module
mo
  Map Ident Info
js     <- (Ident -> Info -> Check Info)
-> Map Ident Info -> Check (Map Ident Info)
forall a b.
Ord a =>
(a -> b -> Check b) -> Map a b -> Check (Map a b)
checkMapRecover (FilePath -> Status -> Module -> Ident -> Info -> Check Info
renameInfo FilePath
cwd Status
status Module
mo) (ModuleInfo -> Map Ident Info
jments ModuleInfo
mi)
  Module -> Check Module
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName
m, ModuleInfo
mi{jments :: Map Ident Info
jments = Map Ident Info
js})

type Status = (StatusMap, [(OpenSpec, StatusMap)])

type StatusMap = Map.Map Ident StatusInfo

type StatusInfo = Ident -> Term

-- Delays errors, allowing many errors to be detected and reported
renameIdentTerm :: Status -> Term -> Check Term
renameIdentTerm Status
env = (Term -> Check Term) -> Term -> Check Term
forall a. (a -> Check a) -> a -> Check a
accumulateError (Status -> Term -> Check Term
renameIdentTerm' Status
env)

-- Fails immediately on error, makes it possible to try other possibilities
renameIdentTerm' :: Status -> Term -> Check Term
renameIdentTerm' :: Status -> Term -> Check Term
renameIdentTerm' env :: Status
env@(StatusMap
act,[(OpenSpec, StatusMap)]
imps) Term
t0 =
  case Term
t0 of
    Vr Ident
c -> (Ident -> Doc -> Check Term) -> Ident -> Check Term
ident Ident -> Doc -> Check Term
predefAbs Ident
c
    Cn Ident
c -> (Ident -> Doc -> Check Term) -> Ident -> Check Term
ident (\Ident
_ Doc
s -> Doc -> Check Term
forall a. Doc -> Check a
checkError Doc
s) Ident
c
    Q (ModuleName
m',Ident
c) | ModuleName
m' ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
cPredef {- && isInPredefined c -} -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t0
    Q (ModuleName
m',Ident
c) -> do
      StatusMap
m <- ModuleName -> [(ModuleName, StatusMap)] -> Check StatusMap
forall (m :: * -> *) a b.
(ErrorMonad m, Eq a, Show a) =>
a -> [(a, b)] -> m b
lookupErr ModuleName
m' [(ModuleName, StatusMap)]
qualifs
      StatusInfo
f <- Ident -> StatusMap -> Check StatusInfo
forall (m :: * -> *) b. ErrorMonad m => Ident -> Map Ident b -> m b
lookupIdent Ident
c StatusMap
m
      Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Check Term) -> Term -> Check Term
forall a b. (a -> b) -> a -> b
$ StatusInfo
f Ident
c
    QC (ModuleName
m',Ident
c) | ModuleName
m' ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
cPredef {- && isInPredefined c -} -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t0
    QC (ModuleName
m',Ident
c) -> do
      StatusMap
m <- ModuleName -> [(ModuleName, StatusMap)] -> Check StatusMap
forall (m :: * -> *) a b.
(ErrorMonad m, Eq a, Show a) =>
a -> [(a, b)] -> m b
lookupErr ModuleName
m' [(ModuleName, StatusMap)]
qualifs
      StatusInfo
f <- Ident -> StatusMap -> Check StatusInfo
forall (m :: * -> *) b. ErrorMonad m => Ident -> Map Ident b -> m b
lookupIdent Ident
c StatusMap
m
      Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Check Term) -> Term -> Check Term
forall a b. (a -> b) -> a -> b
$ StatusInfo
f Ident
c
    Term
_ -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t0
  where
    opens :: [StatusMap]
opens   = [StatusMap
st  | (OSimple ModuleName
_,StatusMap
st) <- [(OpenSpec, StatusMap)]
imps]
    qualifs :: [(ModuleName, StatusMap)]
qualifs = [(ModuleName
m, StatusMap
st) | (OQualif ModuleName
m ModuleName
_, StatusMap
st) <- [(OpenSpec, StatusMap)]
imps] [(ModuleName, StatusMap)]
-> [(ModuleName, StatusMap)] -> [(ModuleName, StatusMap)]
forall a. [a] -> [a] -> [a]
++
              [(ModuleName
m, StatusMap
st) | (OQualif ModuleName
_ ModuleName
m, StatusMap
st) <- [(OpenSpec, StatusMap)]
imps] [(ModuleName, StatusMap)]
-> [(ModuleName, StatusMap)] -> [(ModuleName, StatusMap)]
forall a. [a] -> [a] -> [a]
++
              [(ModuleName
m, StatusMap
st) | (OSimple ModuleName
m, StatusMap
st) <- [(OpenSpec, StatusMap)]
imps] -- qualif is always possible

    -- this facility is mainly for BWC with GF1: you need not import PredefAbs
    predefAbs :: Ident -> Doc -> Check Term
predefAbs Ident
c Doc
s
      | Ident -> Bool
isPredefCat Ident
c = Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return ((ModuleName, Ident) -> Term
Q (ModuleName
cPredefAbs,Ident
c))
      | Bool
otherwise     = Doc -> Check Term
forall a. Doc -> Check a
checkError Doc
s

    ident :: (Ident -> Doc -> Check Term) -> Ident -> Check Term
ident Ident -> Doc -> Check Term
alt Ident
c =
      case Ident -> StatusMap -> Maybe StatusInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
c StatusMap
act of
        Just StatusInfo
f -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (StatusInfo
f Ident
c)
        Maybe StatusInfo
_      -> case (StatusMap -> Maybe StatusInfo) -> [StatusMap] -> [StatusInfo]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Ident -> StatusMap -> Maybe StatusInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
c) [StatusMap]
opens of
                    [StatusInfo
f]  -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (StatusInfo
f Ident
c)
                    []   -> Ident -> Doc -> Check Term
alt Ident
c (FilePath
"constant not found:" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
c Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                                   FilePath
"given" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
fsep (Char -> [ModuleName] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' (((ModuleName, StatusMap) -> ModuleName)
-> [(ModuleName, StatusMap)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, StatusMap) -> ModuleName
forall a b. (a, b) -> a
fst [(ModuleName, StatusMap)]
qualifs)))
                    [StatusInfo]
fs   -> case [Term] -> [Term]
forall a. Eq a => [a] -> [a]
nub [StatusInfo
f Ident
c | StatusInfo
f <- [StatusInfo]
fs]  of
                              [Term
tr]     -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tr
                              ts :: [Term]
ts@(Term
t:[Term]
_) -> do Doc -> Check ()
checkWarn (FilePath
"atomic term" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Term
t0 Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                                                        FilePath
"conflict" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hsep (Char -> [Doc] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Qualified Integer
0) [Term]
ts)) Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$
                                                        FilePath
"given" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
fsep (Char -> [ModuleName] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' (((ModuleName, StatusMap) -> ModuleName)
-> [(ModuleName, StatusMap)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, StatusMap) -> ModuleName
forall a b. (a, b) -> a
fst [(ModuleName, StatusMap)]
qualifs)))
                                             Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> Term
bestTerm [Term]
ts) -- Heuristic for resource grammar. Returns t for all others.
       where
        -- Hotfix for https://github.com/GrammaticalFramework/gf-core/issues/56
        -- Real bug is probably somewhere deeper in recognising excluded functions. /IL 2020-06-06
        notFromCommonModule :: Term -> Bool
        notFromCommonModule :: Term -> Bool
notFromCommonModule Term
term =
          let t :: FilePath
t = Doc -> FilePath
forall a. Pretty a => a -> FilePath
render (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Term
term :: String
           in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\FilePath
moduleName -> FilePath
moduleName FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` FilePath
t)
                        [FilePath
"CommonX", FilePath
"ConstructX", FilePath
"ExtendFunctor"
                        ,FilePath
"MarkHTMLX", FilePath
"ParamX", FilePath
"TenseX", FilePath
"TextX"]

        -- If one of the terms comes from the common modules,
        -- we choose the other one, because that's defined in the grammar.
        bestTerm :: [Term] -> Term
        bestTerm :: [Term] -> Term
bestTerm [] = FilePath -> Term
forall a. HasCallStack => FilePath -> a
error FilePath
"constant not found" -- not reached: bestTerm is only called for case ts@(t:_)
        bestTerm ts :: [Term]
ts@(Term
t:[Term]
_) =
          let notCommon :: [Term]
notCommon = [Term
t | Term
t <- [Term]
ts, Term -> Bool
notFromCommonModule Term
t]
           in case [Term]
notCommon of
                []    -> Term
t -- All terms are from common modules, return first of original list
                (Term
u:[Term]
_) -> Term
u -- ≥1 terms are not from common modules, return first of those

info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
info2status Maybe ModuleName
mq Ident
c Info
i = case Info
i of
  AbsFun Maybe (L Term)
_ Maybe Int
_ Maybe [L Equation]
Nothing Maybe Bool
_ -> StatusInfo
-> (ModuleName -> StatusInfo) -> Maybe ModuleName -> StatusInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StatusInfo
Con (((ModuleName, Ident) -> Term) -> ModuleName -> StatusInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ModuleName, Ident) -> Term
QC) Maybe ModuleName
mq
  ResValue L Term
_  -> StatusInfo
-> (ModuleName -> StatusInfo) -> Maybe ModuleName -> StatusInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StatusInfo
Con (((ModuleName, Ident) -> Term) -> ModuleName -> StatusInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ModuleName, Ident) -> Term
QC) Maybe ModuleName
mq
  ResParam Maybe (L [Param])
_ Maybe [Term]
_  -> StatusInfo
-> (ModuleName -> StatusInfo) -> Maybe ModuleName -> StatusInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StatusInfo
Con (((ModuleName, Ident) -> Term) -> ModuleName -> StatusInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ModuleName, Ident) -> Term
QC) Maybe ModuleName
mq
  AnyInd Bool
True ModuleName
m -> StatusInfo
-> (ModuleName -> StatusInfo) -> Maybe ModuleName -> StatusInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StatusInfo
Con (StatusInfo -> ModuleName -> StatusInfo
forall a b. a -> b -> a
const (((ModuleName, Ident) -> Term) -> ModuleName -> StatusInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ModuleName, Ident) -> Term
QC ModuleName
m)) Maybe ModuleName
mq
  AnyInd Bool
False ModuleName
m -> StatusInfo
-> (ModuleName -> StatusInfo) -> Maybe ModuleName -> StatusInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StatusInfo
Cn (StatusInfo -> ModuleName -> StatusInfo
forall a b. a -> b -> a
const (((ModuleName, Ident) -> Term) -> ModuleName -> StatusInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ModuleName, Ident) -> Term
Q ModuleName
m)) Maybe ModuleName
mq
  Info
_           -> StatusInfo
-> (ModuleName -> StatusInfo) -> Maybe ModuleName -> StatusInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe StatusInfo
Cn (((ModuleName, Ident) -> Term) -> ModuleName -> StatusInfo
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (ModuleName, Ident) -> Term
Q) Maybe ModuleName
mq

tree2status :: OpenSpec -> Map.Map Ident Info -> StatusMap
tree2status :: OpenSpec -> Map Ident Info -> StatusMap
tree2status OpenSpec
o = case OpenSpec
o of
  OSimple ModuleName
i   -> (Ident -> Info -> StatusInfo) -> Map Ident Info -> StatusMap
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (Maybe ModuleName -> Ident -> Info -> StatusInfo
info2status (ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just ModuleName
i))
  OQualif ModuleName
i ModuleName
j -> (Ident -> Info -> StatusInfo) -> Map Ident Info -> StatusMap
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (Maybe ModuleName -> Ident -> Info -> StatusInfo
info2status (ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just ModuleName
j))

buildStatus :: FilePath -> Grammar -> Module -> Check Status
buildStatus :: FilePath -> Grammar -> Module -> Check Status
buildStatus FilePath
cwd Grammar
gr mo :: Module
mo@(ModuleName
m,ModuleInfo
mi) = FilePath
-> ModuleInfo -> Location -> Doc -> Check Status -> Check Status
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 Status -> Check Status) -> Check Status -> Check Status
forall a b. (a -> b) -> a -> b
$ do
  let gr1 :: Grammar
gr1  = Grammar -> Module -> Grammar
prependModule Grammar
gr Module
mo
      exts :: [(OpenSpec, ModuleInfo)]
exts = [(ModuleName -> OpenSpec
OSimple ModuleName
m,ModuleInfo
mi) | (ModuleName
m,ModuleInfo
mi) <- Grammar -> ModuleName -> [Module]
allExtends Grammar
gr1 ModuleName
m]
  [(OpenSpec, ModuleInfo)]
ops <- (OpenSpec -> Check (OpenSpec, ModuleInfo))
-> [OpenSpec] -> Check [(OpenSpec, ModuleInfo)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\OpenSpec
o -> Grammar -> ModuleName -> Check ModuleInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m ModuleInfo
lookupModule Grammar
gr1 (OpenSpec -> ModuleName
openedModule OpenSpec
o) Check ModuleInfo
-> (ModuleInfo -> Check (OpenSpec, ModuleInfo))
-> Check (OpenSpec, ModuleInfo)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ModuleInfo
mi -> (OpenSpec, ModuleInfo) -> Check (OpenSpec, ModuleInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (OpenSpec
o,ModuleInfo
mi)) (ModuleInfo -> [OpenSpec]
mopens ModuleInfo
mi)
  let sts :: [(OpenSpec, StatusMap)]
sts = ((OpenSpec, ModuleInfo) -> (OpenSpec, StatusMap))
-> [(OpenSpec, ModuleInfo)] -> [(OpenSpec, StatusMap)]
forall a b. (a -> b) -> [a] -> [b]
map (OpenSpec, ModuleInfo) -> (OpenSpec, StatusMap)
modInfo2status ([(OpenSpec, ModuleInfo)]
exts[(OpenSpec, ModuleInfo)]
-> [(OpenSpec, ModuleInfo)] -> [(OpenSpec, ModuleInfo)]
forall a. [a] -> [a] -> [a]
++[(OpenSpec, ModuleInfo)]
ops)
  Status -> Check Status
forall (m :: * -> *) a. Monad m => a -> m a
return (if ModuleInfo -> Bool
isModCnc ModuleInfo
mi
            then (StatusMap
forall k a. Map k a
Map.empty,       [(OpenSpec, StatusMap)] -> [(OpenSpec, StatusMap)]
forall a. [a] -> [a]
reverse [(OpenSpec, StatusMap)]
sts)  -- the module itself does not define any names
            else (ModuleName -> ModuleInfo -> StatusMap
self2status ModuleName
m ModuleInfo
mi,[(OpenSpec, StatusMap)] -> [(OpenSpec, StatusMap)]
forall a. [a] -> [a]
reverse [(OpenSpec, StatusMap)]
sts)) -- so the empty ident is not needed

modInfo2status :: (OpenSpec,ModuleInfo) -> (OpenSpec, StatusMap)
modInfo2status :: (OpenSpec, ModuleInfo) -> (OpenSpec, StatusMap)
modInfo2status (OpenSpec
o,ModuleInfo
mo) = (OpenSpec
o,OpenSpec -> Map Ident Info -> StatusMap
tree2status OpenSpec
o (ModuleInfo -> Map Ident Info
jments ModuleInfo
mo))

self2status :: ModuleName -> ModuleInfo -> StatusMap
self2status :: ModuleName -> ModuleInfo -> StatusMap
self2status ModuleName
c ModuleInfo
m = (Ident -> Info -> StatusInfo) -> Map Ident Info -> StatusMap
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (Maybe ModuleName -> Ident -> Info -> StatusInfo
info2status (ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just ModuleName
c)) (ModuleInfo -> Map Ident Info
jments ModuleInfo
m)


renameInfo :: FilePath -> Status -> Module -> Ident -> Info -> Check Info
renameInfo :: FilePath -> Status -> Module -> Ident -> Info -> Check Info
renameInfo FilePath
cwd Status
status (ModuleName
m,ModuleInfo
mi) Ident
i Info
info =
  case Info
info of
    AbsCat Maybe (L Context)
pco -> (Maybe (L Context) -> Info)
-> Check (Maybe (L Context)) -> Check Info
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Maybe (L Context) -> Info
AbsCat ((Context -> Check Context)
-> Maybe (L Context) -> Check (Maybe (L Context))
forall t a. (t -> Check a) -> Maybe (L t) -> Check (Maybe (L a))
renPerh (Status -> Context -> Check Context
renameContext Status
status) Maybe (L Context)
pco)
    AbsFun  Maybe (L Term)
pty Maybe Int
pa Maybe [L Equation]
ptr Maybe Bool
poper -> (Maybe (L Term)
 -> Maybe Int -> Maybe [L Equation] -> Maybe Bool -> Info)
-> Check (Maybe (L Term))
-> Check (Maybe Int)
-> Check (Maybe [L Equation])
-> Check (Maybe Bool)
-> Check Info
forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 Maybe (L Term)
-> Maybe Int -> Maybe [L Equation] -> Maybe Bool -> Info
AbsFun (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
pty) (Maybe Int -> Check (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
pa) (([L Equation] -> Check [L Equation])
-> Maybe [L Equation] -> Check (Maybe [L Equation])
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> Maybe t -> m (Maybe a)
renMaybe ((L Equation -> Check (L Equation))
-> [L Equation] -> Check [L Equation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Equation -> Check Equation) -> L Equation -> Check (L Equation)
forall t a. (t -> Check a) -> L t -> Check (L a)
renLoc (Status -> Equation -> Check Equation
renEquation Status
status))) Maybe [L Equation]
ptr) (Maybe Bool -> Check (Maybe Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
poper)
    ResOper Maybe (L Term)
pty Maybe (L Term)
ptr -> (Maybe (L Term) -> Maybe (L Term) -> Info)
-> Check (Maybe (L Term)) -> Check (Maybe (L Term)) -> Check Info
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe (L Term) -> Maybe (L Term) -> Info
ResOper (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
pty) (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
ptr)
    ResOverload [ModuleName]
os [(L Term, L Term)]
tysts -> ([(L Term, L Term)] -> Info)
-> Check [(L Term, L Term)] -> Check Info
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ([ModuleName] -> [(L Term, L Term)] -> Info
ResOverload [ModuleName]
os) (((L Term, L Term) -> Check (L Term, L Term))
-> [(L Term, L Term)] -> Check [(L Term, L Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Term -> Check Term) -> (L Term, L Term) -> Check (L Term, L Term)
forall t a. (t -> Check a) -> (L t, L t) -> Check (L a, L a)
renPair (Status -> [Ident] -> Term -> Check Term
renameTerm Status
status [])) [(L Term, L Term)]
tysts)
    ResParam (Just L [Param]
pp) Maybe [Term]
m -> do
      L [Param]
pp' <- ([Param] -> Check [Param]) -> L [Param] -> Check (L [Param])
forall t a. (t -> Check a) -> L t -> Check (L a)
renLoc ((Param -> Check Param) -> [Param] -> Check [Param]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Status -> Param -> Check Param
renParam Status
status)) L [Param]
pp
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (L [Param]) -> Maybe [Term] -> Info
ResParam (L [Param] -> Maybe (L [Param])
forall a. a -> Maybe a
Just L [Param]
pp') Maybe [Term]
m)
    ResValue L Term
t -> do
      L Term
t <- (Term -> Check Term) -> L Term -> Check (L Term)
forall t a. (t -> Check a) -> L t -> Check (L a)
renLoc (Status -> [Ident] -> Term -> Check Term
renameTerm Status
status []) L Term
t
      Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return (L Term -> Info
ResValue L Term
t)
    CncCat Maybe (L Term)
mcat Maybe (L Term)
mdef Maybe (L Term)
mref Maybe (L Term)
mpr Maybe PMCFG
mpmcfg -> (Maybe (L Term)
 -> Maybe (L Term)
 -> Maybe (L Term)
 -> Maybe (L Term)
 -> Maybe PMCFG
 -> Info)
-> Check (Maybe (L Term))
-> Check (Maybe (L Term))
-> Check (Maybe (L Term))
-> Check (Maybe (L Term))
-> Check (Maybe PMCFG)
-> Check Info
forall (m :: * -> *) a1 a2 a3 a4 a5 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> a5 -> r)
-> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
liftM5 Maybe (L Term)
-> Maybe (L Term)
-> Maybe (L Term)
-> Maybe (L Term)
-> Maybe PMCFG
-> Info
CncCat (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
mcat) (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
mdef) (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
mref) (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
mpr) (Maybe PMCFG -> Check (Maybe PMCFG)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PMCFG
mpmcfg)
    CncFun Maybe (Ident, Context, Term)
mty Maybe (L Term)
mtr Maybe (L Term)
mpr Maybe PMCFG
mpmcfg -> (Maybe (L Term) -> Maybe (L Term) -> Maybe PMCFG -> Info)
-> Check (Maybe (L Term))
-> Check (Maybe (L Term))
-> Check (Maybe PMCFG)
-> Check Info
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (Maybe (Ident, Context, Term)
-> Maybe (L Term) -> Maybe (L Term) -> Maybe PMCFG -> Info
CncFun Maybe (Ident, Context, Term)
mty)         (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
mtr) (Maybe (L Term) -> Check (Maybe (L Term))
renTerm Maybe (L Term)
mpr) (Maybe PMCFG -> Check (Maybe PMCFG)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PMCFG
mpmcfg)
    Info
_ -> Info -> Check Info
forall (m :: * -> *) a. Monad m => a -> m a
return Info
info
  where
    renTerm :: Maybe (L Term) -> Check (Maybe (L Term))
renTerm = (Term -> Check Term) -> Maybe (L Term) -> Check (Maybe (L Term))
forall t a. (t -> Check a) -> Maybe (L t) -> Check (Maybe (L a))
renPerh (Status -> [Ident] -> Term -> Check Term
renameTerm Status
status [])

    renPerh :: (t -> Check a) -> Maybe (L t) -> Check (Maybe (L a))
renPerh t -> Check a
ren = (L t -> Check (L a)) -> Maybe (L t) -> Check (Maybe (L a))
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> Maybe t -> m (Maybe a)
renMaybe ((t -> Check a) -> L t -> Check (L a)
forall t a. (t -> Check a) -> L t -> Check (L a)
renLoc t -> Check a
ren)

    renMaybe :: (t -> m a) -> Maybe t -> m (Maybe a)
renMaybe t -> m a
ren (Just t
x) = t -> m a
ren t
x m a -> (a -> m (Maybe a)) -> m (Maybe a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
    renMaybe t -> m a
ren Maybe t
Nothing  = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing

    renLoc :: (t -> Check a) -> L t -> Check (L a)
renLoc t -> Check a
ren (L Location
loc t
x) =
      FilePath
-> ModuleInfo -> Location -> Doc -> Check (L a) -> Check (L a)
forall a1 a2 a3.
(Pretty a1, HasSourcePath a2) =>
FilePath -> a2 -> Location -> a1 -> Check a3 -> Check a3
checkInModule FilePath
cwd ModuleInfo
mi Location
loc (FilePath
"Happened in the renaming of" FilePath -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
i) (Check (L a) -> Check (L a)) -> Check (L a) -> Check (L a)
forall a b. (a -> b) -> a -> b
$ do
        a
x <- t -> Check a
ren t
x
        L a -> Check (L a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Location -> a -> L a
forall a. Location -> a -> L a
L Location
loc a
x)

    renPair :: (t -> Check a) -> (L t, L t) -> Check (L a, L a)
renPair t -> Check a
ren (L t
x, L t
y) = do L a
x <- (t -> Check a) -> L t -> Check (L a)
forall t a. (t -> Check a) -> L t -> Check (L a)
renLoc t -> Check a
ren L t
x
                            L a
y <- (t -> Check a) -> L t -> Check (L a)
forall t a. (t -> Check a) -> L t -> Check (L a)
renLoc t -> Check a
ren L t
y
                            (L a, L a) -> Check (L a, L a)
forall (m :: * -> *) a. Monad m => a -> m a
return (L a
x, L a
y)

    renEquation :: Status -> Equation -> Check Equation
    renEquation :: Status -> Equation -> Check Equation
renEquation Status
b ([Patt]
ps,Term
t) = do
        ([Patt]
ps',[[Ident]]
vs) <- ([(Patt, [Ident])] -> ([Patt], [[Ident]]))
-> Check [(Patt, [Ident])] -> Check ([Patt], [[Ident]])
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Patt, [Ident])] -> ([Patt], [[Ident]])
forall a b. [(a, b)] -> ([a], [b])
unzip (Check [(Patt, [Ident])] -> Check ([Patt], [[Ident]]))
-> Check [(Patt, [Ident])] -> Check ([Patt], [[Ident]])
forall a b. (a -> b) -> a -> b
$ (Patt -> Check (Patt, [Ident]))
-> [Patt] -> Check [(Patt, [Ident])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Status -> Patt -> Check (Patt, [Ident])
renamePattern Status
b) [Patt]
ps
        Term
t'       <- Status -> [Ident] -> Term -> Check Term
renameTerm Status
b ([[Ident]] -> [Ident]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ident]]
vs) Term
t
        Equation -> Check Equation
forall (m :: * -> *) a. Monad m => a -> m a
return ([Patt]
ps',Term
t')

    renParam :: Status -> Param -> Check Param
    renParam :: Status -> Param -> Check Param
renParam Status
env (Ident
c,Context
co) = do
      Context
co' <- Status -> Context -> Check Context
renameContext Status
env Context
co
      Param -> Check Param
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident
c,Context
co')

renameTerm :: Status -> [Ident] -> Term -> Check Term
renameTerm :: Status -> [Ident] -> Term -> Check Term
renameTerm Status
env [Ident]
vars = [Ident] -> Term -> Check Term
ren [Ident]
vars where
  ren :: [Ident] -> Term -> Check Term
ren [Ident]
vs Term
trm = case Term
trm of
    Abs BindType
b Ident
x Term
t    -> (Term -> Term) -> Check Term -> Check Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM  (BindType -> Ident -> Term -> Term
Abs BindType
b Ident
x) ([Ident] -> Term -> Check Term
ren (Ident
xIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:[Ident]
vs) Term
t)
    Prod BindType
bt Ident
x Term
a Term
b -> (Term -> Term -> Term) -> Check Term -> Check Term -> Check Term
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (BindType -> Ident -> Term -> Term -> Term
Prod BindType
bt Ident
x) ([Ident] -> Term -> Check Term
ren [Ident]
vs Term
a) ([Ident] -> Term -> Check Term
ren (Ident
xIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:[Ident]
vs) Term
b)
    Typed Term
a Term
b  -> (Term -> Term -> Term) -> Check Term -> Check Term -> Check Term
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Term -> Term -> Term
Typed ([Ident] -> Term -> Check Term
ren [Ident]
vs Term
a) ([Ident] -> Term -> Check Term
ren [Ident]
vs Term
b)
    Vr Ident
x
      | Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Ident
x [Ident]
vs -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
trm
      | Bool
otherwise -> Term -> Check Term
renid Term
trm
    Cn Ident
_   -> Term -> Check Term
renid Term
trm
    Con Ident
_  -> Term -> Check Term
renid Term
trm
    Q (ModuleName, Ident)
_    -> Term -> Check Term
renid Term
trm
    QC (ModuleName, Ident)
_   -> Term -> Check Term
renid Term
trm
    T TInfo
i [Case]
cs -> do
      TInfo
i' <- case TInfo
i of
        TTyped Term
ty -> (Term -> TInfo) -> Check Term -> Check TInfo
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Term -> TInfo
TTyped (Check Term -> Check TInfo) -> Check Term -> Check TInfo
forall a b. (a -> b) -> a -> b
$ [Ident] -> Term -> Check Term
ren [Ident]
vs Term
ty -- the only annotation in source
        TInfo
_ -> TInfo -> Check TInfo
forall (m :: * -> *) a. Monad m => a -> m a
return TInfo
i
      ([Case] -> Term) -> Check [Case] -> Check Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (TInfo -> [Case] -> Term
T TInfo
i') (Check [Case] -> Check Term) -> Check [Case] -> Check Term
forall a b. (a -> b) -> a -> b
$ (Case -> Check Case) -> [Case] -> Check [Case]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Ident] -> Case -> Check Case
renCase [Ident]
vs) [Case]
cs

    Let (Ident
x,(Maybe Term
m,Term
a)) Term
b -> do
      Maybe Term
m' <- case Maybe Term
m of
        Just Term
ty -> (Term -> Maybe Term) -> Check Term -> Check (Maybe Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Term -> Maybe Term
forall a. a -> Maybe a
Just (Check Term -> Check (Maybe Term))
-> Check Term -> Check (Maybe Term)
forall a b. (a -> b) -> a -> b
$ [Ident] -> Term -> Check Term
ren [Ident]
vs Term
ty
        Maybe Term
_ -> Maybe Term -> Check (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
m
      Term
a' <- [Ident] -> Term -> Check Term
ren [Ident]
vs Term
a
      Term
b' <- [Ident] -> Term -> Check Term
ren (Ident
xIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:[Ident]
vs) Term
b
      Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Check Term) -> Term -> Check Term
forall a b. (a -> b) -> a -> b
$ (Ident, (Maybe Term, Term)) -> Term -> Term
Let (Ident
x,(Maybe Term
m',Term
a')) Term
b'

    P t :: Term
t@(Vr Ident
r) Label
l                                               -- Here we have $r.l$ and this is ambiguous it could be either
                                                               -- record projection from variable or constant $r$ or qualified expression with module $r$
      | Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Ident
r [Ident]
vs -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
trm                                -- try var proj first ..
      | Bool
otherwise -> [Check Term] -> Check Term
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [ Term -> Check Term
renid' ((ModuleName, Ident) -> Term
Q (Ident -> ModuleName
MN Ident
r,Label -> Ident
label2ident Label
l))      -- .. and qualified expression second.
                            , Term -> Check Term
renid' Term
t Check Term -> (Term -> Check Term) -> Check Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Term
t -> Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Label -> Term
P Term
t Label
l) -- try as a constant at the end
                            , Doc -> Check Term
forall a. Doc -> Check a
checkError (FilePath
"unknown qualified constant" FilePath -> Term -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Term
trm)
                            ]

    EPatt Patt
p -> do
      (Patt
p',[Ident]
_) <- Patt -> Check (Patt, [Ident])
renpatt Patt
p
      Term -> Check Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Check Term) -> Term -> Check Term
forall a b. (a -> b) -> a -> b
$ Patt -> Term
EPatt Patt
p'

    Term
_ -> (Term -> Check Term) -> Term -> Check Term
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
composOp ([Ident] -> Term -> Check Term
ren [Ident]
vs) Term
trm

  renid :: Term -> Check Term
renid = Status -> Term -> Check Term
renameIdentTerm Status
env
  renid' :: Term -> Check Term
renid' = Status -> Term -> Check Term
renameIdentTerm' Status
env
  renCase :: [Ident] -> Case -> Check Case
renCase [Ident]
vs (Patt
p,Term
t) = do
    (Patt
p',[Ident]
vs') <- Patt -> Check (Patt, [Ident])
renpatt Patt
p
    Term
t' <- [Ident] -> Term -> Check Term
ren ([Ident]
vs' [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ [Ident]
vs) Term
t
    Case -> Check Case
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt
p',Term
t')
  renpatt :: Patt -> Check (Patt, [Ident])
renpatt = Status -> Patt -> Check (Patt, [Ident])
renamePattern Status
env

-- | vars not needed in env, since patterns always overshadow old vars
renamePattern :: Status -> Patt -> Check (Patt,[Ident])
renamePattern :: Status -> Patt -> Check (Patt, [Ident])
renamePattern Status
env Patt
patt =
    do r :: (Patt, [Ident])
r@(Patt
p',[Ident]
vs) <- Patt -> Check (Patt, [Ident])
renp Patt
patt
       let dupl :: [Ident]
dupl = [Ident]
vs [Ident] -> [Ident] -> [Ident]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub [Ident]
vs
       Bool -> Check () -> Check ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Ident] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ident]
dupl) (Check () -> Check ()) -> Check () -> Check ()
forall a b. (a -> b) -> a -> b
$ Doc -> Check ()
forall a. Doc -> Check a
checkError (FilePath -> Int -> Patt -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang (FilePath
"[C.4.13] Pattern is not linear. All variable names on the left-hand side must be distinct.") Int
4
                                             Patt
patt)
       (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt, [Ident])
r
  where
    renp :: Patt -> Check (Patt, [Ident])
renp Patt
patt = case Patt
patt of
      PMacro Ident
c -> do
        Term
c' <- Term -> Check Term
renid (Term -> Check Term) -> Term -> Check Term
forall a b. (a -> b) -> a -> b
$ StatusInfo
Vr Ident
c
        case Term
c' of
          Q (ModuleName, Ident)
d -> Patt -> Check (Patt, [Ident])
renp (Patt -> Check (Patt, [Ident])) -> Patt -> Check (Patt, [Ident])
forall a b. (a -> b) -> a -> b
$ (ModuleName, Ident) -> Patt
PM (ModuleName, Ident)
d
          Term
_ -> Doc -> Check (Patt, [Ident])
forall a. Doc -> Check a
checkError (FilePath
"unresolved pattern" FilePath -> Patt -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Patt
patt)

      PC Ident
c [Patt]
ps -> do
        Term
c' <- Term -> Check Term
renid (Term -> Check Term) -> Term -> Check Term
forall a b. (a -> b) -> a -> b
$ StatusInfo
Cn Ident
c
        case Term
c' of
          QC (ModuleName, Ident)
c -> do [(Patt, [Ident])]
psvss <- (Patt -> Check (Patt, [Ident]))
-> [Patt] -> Check [(Patt, [Ident])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Patt -> Check (Patt, [Ident])
renp [Patt]
ps
                     let ([Patt]
ps,[[Ident]]
vs) = [(Patt, [Ident])] -> ([Patt], [[Ident]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Patt, [Ident])]
psvss
                     (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return ((ModuleName, Ident) -> [Patt] -> Patt
PP (ModuleName, Ident)
c [Patt]
ps, [[Ident]] -> [Ident]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ident]]
vs)
          Q  (ModuleName, Ident)
_ -> Doc -> Check (Patt, [Ident])
forall a. Doc -> Check a
checkError (FilePath
"data constructor expected but" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Term
c' Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> FilePath
"is found instead")
          Term
_    -> Doc -> Check (Patt, [Ident])
forall a. Doc -> Check a
checkError (FilePath
"unresolved data constructor" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Term
c')

      PP (ModuleName, Ident)
c [Patt]
ps -> do
        (QC (ModuleName, Ident)
c') <- Term -> Check Term
renid ((ModuleName, Ident) -> Term
QC (ModuleName, Ident)
c)
        [(Patt, [Ident])]
psvss <- (Patt -> Check (Patt, [Ident]))
-> [Patt] -> Check [(Patt, [Ident])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Patt -> Check (Patt, [Ident])
renp [Patt]
ps
        let ([Patt]
ps',[[Ident]]
vs) = [(Patt, [Ident])] -> ([Patt], [[Ident]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Patt, [Ident])]
psvss
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return ((ModuleName, Ident) -> [Patt] -> Patt
PP (ModuleName, Ident)
c' [Patt]
ps', [[Ident]] -> [Ident]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ident]]
vs)

      PM (ModuleName, Ident)
c -> do
        Term
x <- Term -> Check Term
renid ((ModuleName, Ident) -> Term
Q (ModuleName, Ident)
c)
        (ModuleName, Ident)
c' <- case Term
x of
                (Q (ModuleName, Ident)
c') -> (ModuleName, Ident) -> Check (ModuleName, Ident)
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName, Ident)
c'
                Term
_      -> Doc -> Check (ModuleName, Ident)
forall a. Doc -> Check a
checkError (FilePath
"not a pattern macro" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Qualified Integer
0 Patt
patt)
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return ((ModuleName, Ident) -> Patt
PM (ModuleName, Ident)
c', [])

      PV Ident
x -> [Check (Patt, [Ident])] -> Check (Patt, [Ident])
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [ Term -> Check Term
renid' (StatusInfo
Vr Ident
x) Check Term
-> (Term -> Check (Patt, [Ident])) -> Check (Patt, [Ident])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Term
t' -> case Term
t' of
                                                 QC (ModuleName, Ident)
c -> (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return ((ModuleName, Ident) -> [Patt] -> Patt
PP (ModuleName, Ident)
c [],[])
                                                 Term
_    -> Doc -> Check (Patt, [Ident])
forall a. Doc -> Check a
checkError (FilePath -> Doc
forall a. Pretty a => a -> Doc
pp FilePath
"not a constructor")
                     , (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt
patt, [Ident
x])
                     ]

      PR [(Label, Patt)]
r -> do
        let ([Label]
ls,[Patt]
ps) = [(Label, Patt)] -> ([Label], [Patt])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Label, Patt)]
r
        [(Patt, [Ident])]
psvss <- (Patt -> Check (Patt, [Ident]))
-> [Patt] -> Check [(Patt, [Ident])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Patt -> Check (Patt, [Ident])
renp [Patt]
ps
        let ([Patt]
ps',[[Ident]]
vs') = [(Patt, [Ident])] -> ([Patt], [[Ident]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Patt, [Ident])]
psvss
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Label, Patt)] -> Patt
PR ([Label] -> [Patt] -> [(Label, Patt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Label]
ls [Patt]
ps'), [[Ident]] -> [Ident]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ident]]
vs')

      PAlt Patt
p Patt
q -> do
        (Patt
p',[Ident]
vs) <- Patt -> Check (Patt, [Ident])
renp Patt
p
        (Patt
q',[Ident]
ws) <- Patt -> Check (Patt, [Ident])
renp Patt
q
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt -> Patt
PAlt Patt
p' Patt
q', [Ident]
vs [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ [Ident]
ws)

      PSeq Patt
p Patt
q -> do
        (Patt
p',[Ident]
vs) <- Patt -> Check (Patt, [Ident])
renp Patt
p
        (Patt
q',[Ident]
ws) <- Patt -> Check (Patt, [Ident])
renp Patt
q
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt -> Patt
PSeq Patt
p' Patt
q', [Ident]
vs [Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++ [Ident]
ws)

      PRep Patt
p -> do
        (Patt
p',[Ident]
vs) <- Patt -> Check (Patt, [Ident])
renp Patt
p
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt
PRep Patt
p', [Ident]
vs)

      PNeg Patt
p -> do
        (Patt
p',[Ident]
vs) <- Patt -> Check (Patt, [Ident])
renp Patt
p
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt -> Patt
PNeg Patt
p', [Ident]
vs)

      PAs Ident
x Patt
p -> do
        (Patt
p',[Ident]
vs) <- Patt -> Check (Patt, [Ident])
renp Patt
p
        (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> Patt -> Patt
PAs Ident
x Patt
p', Ident
xIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:[Ident]
vs)

      Patt
_ -> (Patt, [Ident]) -> Check (Patt, [Ident])
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt
patt,[])

    renid :: Term -> Check Term
renid = Status -> Term -> Check Term
renameIdentTerm Status
env
    renid' :: Term -> Check Term
renid' = Status -> Term -> Check Term
renameIdentTerm' Status
env

renameContext :: Status -> Context -> Check Context
renameContext :: Status -> Context -> Check Context
renameContext Status
b = [Ident] -> Context -> Check Context
forall a. [Ident] -> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
renc [] where
  renc :: [Ident] -> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
renc [Ident]
vs [(a, Ident, Term)]
cont = case [(a, Ident, Term)]
cont of
    (a
bt,Ident
x,Term
t) : [(a, Ident, Term)]
xts
      | Ident -> Bool
isWildIdent Ident
x -> do
          Term
t'   <- [Ident] -> Term -> Check Term
ren [Ident]
vs Term
t
          [(a, Ident, Term)]
xts' <- [Ident] -> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
renc [Ident]
vs [(a, Ident, Term)]
xts
          [(a, Ident, Term)] -> Check [(a, Ident, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, Ident, Term)] -> Check [(a, Ident, Term)])
-> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
forall a b. (a -> b) -> a -> b
$ (a
bt,Ident
x,Term
t') (a, Ident, Term) -> [(a, Ident, Term)] -> [(a, Ident, Term)]
forall a. a -> [a] -> [a]
: [(a, Ident, Term)]
xts'
      | Bool
otherwise -> do
          Term
t'   <- [Ident] -> Term -> Check Term
ren [Ident]
vs Term
t
          let vs' :: [Ident]
vs' = Ident
xIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:[Ident]
vs
          [(a, Ident, Term)]
xts' <- [Ident] -> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
renc [Ident]
vs' [(a, Ident, Term)]
xts
          [(a, Ident, Term)] -> Check [(a, Ident, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, Ident, Term)] -> Check [(a, Ident, Term)])
-> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
forall a b. (a -> b) -> a -> b
$ (a
bt,Ident
x,Term
t') (a, Ident, Term) -> [(a, Ident, Term)] -> [(a, Ident, Term)]
forall a. a -> [a] -> [a]
: [(a, Ident, Term)]
xts'
    [(a, Ident, Term)]
_ -> [(a, Ident, Term)] -> Check [(a, Ident, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a, Ident, Term)]
cont
  ren :: [Ident] -> Term -> Check Term
ren = Status -> [Ident] -> Term -> Check Term
renameTerm Status
b