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
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
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)
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 -> 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 -> 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]
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)
where
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"]
bestTerm :: [Term] -> Term
bestTerm :: [Term] -> Term
bestTerm [] = FilePath -> Term
forall a. HasCallStack => FilePath -> a
error FilePath
"constant not found"
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
(Term
u:[Term]
_) -> Term
u
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)
else (ModuleName -> ModuleInfo -> StatusMap
self2status ModuleName
m ModuleInfo
mi,[(OpenSpec, StatusMap)] -> [(OpenSpec, StatusMap)]
forall a. [a] -> [a]
reverse [(OpenSpec, StatusMap)]
sts))
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
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
| 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
| 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))
, 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)
, 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
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