{- |
module: $Header$
description: OpenTheory interpretations
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.OpenTheory.Interpret
where

import Control.Monad (guard)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (mapMaybe)
import Text.Parsec ((<|>))
import qualified Text.Parsec as Parsec
import Text.Parsec.Text.Lazy ()
import Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as PP

import HOL.Name
import HOL.Parse
import HOL.Print

-------------------------------------------------------------------------------
-- Symbols
-------------------------------------------------------------------------------

data Symbol =
    TypeOpSymbol Name
  | ConstSymbol Name
  deriving (Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq,Eq Symbol
Eq Symbol
-> (Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Symbol)
-> (Symbol -> Symbol -> Symbol)
-> Ord Symbol
Symbol -> Symbol -> Bool
Symbol -> Symbol -> Ordering
Symbol -> Symbol -> Symbol
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Symbol -> Symbol -> Symbol
$cmin :: Symbol -> Symbol -> Symbol
max :: Symbol -> Symbol -> Symbol
$cmax :: Symbol -> Symbol -> Symbol
>= :: Symbol -> Symbol -> Bool
$c>= :: Symbol -> Symbol -> Bool
> :: Symbol -> Symbol -> Bool
$c> :: Symbol -> Symbol -> Bool
<= :: Symbol -> Symbol -> Bool
$c<= :: Symbol -> Symbol -> Bool
< :: Symbol -> Symbol -> Bool
$c< :: Symbol -> Symbol -> Bool
compare :: Symbol -> Symbol -> Ordering
$ccompare :: Symbol -> Symbol -> Ordering
$cp1Ord :: Eq Symbol
Ord,Int -> Symbol -> ShowS
[Symbol] -> ShowS
Symbol -> String
(Int -> Symbol -> ShowS)
-> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Symbol] -> ShowS
$cshowList :: [Symbol] -> ShowS
show :: Symbol -> String
$cshow :: Symbol -> String
showsPrec :: Int -> Symbol -> ShowS
$cshowsPrec :: Int -> Symbol -> ShowS
Show)

symbolName :: Symbol -> Name
symbolName :: Symbol -> Name
symbolName (TypeOpSymbol Name
n) = Name
n
symbolName (ConstSymbol Name
n) = Name
n

renameSymbol :: Symbol -> Name -> Symbol
renameSymbol :: Symbol -> Name -> Symbol
renameSymbol (TypeOpSymbol Name
_) Name
n = Name -> Symbol
TypeOpSymbol Name
n
renameSymbol (ConstSymbol Name
_) Name
n = Name -> Symbol
ConstSymbol Name
n

instance Printable Symbol where
  toDoc :: Symbol -> Doc
toDoc (TypeOpSymbol Name
n) = String -> Doc
PP.text String
"type" Doc -> Doc -> Doc
<+> Name -> Doc
quoteName Name
n
  toDoc (ConstSymbol Name
n) = String -> Doc
PP.text String
"const" Doc -> Doc -> Doc
<+> Name -> Doc
quoteName Name
n

instance Parsable Symbol where
  parser :: Parsec Text st Symbol
parser = do
      Name -> Symbol
k <- ParsecT Text st Identity (Name -> Symbol)
forall u. ParsecT Text u Identity (Name -> Symbol)
kind
      ParsecT Text st Identity ()
forall u. ParsecT Text u Identity ()
space
      Name
n <- Parsec Text st Name
forall a st. Parsable a => Parsec Text st a
parser
      Symbol -> Parsec Text st Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> Parsec Text st Symbol)
-> Symbol -> Parsec Text st Symbol
forall a b. (a -> b) -> a -> b
$ Name -> Symbol
k Name
n
    where
      kind :: ParsecT Text u Identity (Name -> Symbol)
kind = (String -> ParsecT Text u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
Parsec.string String
"type" ParsecT Text u Identity String
-> ParsecT Text u Identity (Name -> Symbol)
-> ParsecT Text u Identity (Name -> Symbol)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Name -> Symbol) -> ParsecT Text u Identity (Name -> Symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return Name -> Symbol
TypeOpSymbol)
             ParsecT Text u Identity (Name -> Symbol)
-> ParsecT Text u Identity (Name -> Symbol)
-> ParsecT Text u Identity (Name -> Symbol)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> ParsecT Text u Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
Parsec.string String
"const" ParsecT Text u Identity String
-> ParsecT Text u Identity (Name -> Symbol)
-> ParsecT Text u Identity (Name -> Symbol)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Name -> Symbol) -> ParsecT Text u Identity (Name -> Symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return Name -> Symbol
ConstSymbol)

      space :: ParsecT Text u Identity ()
space = ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany1 ParsecT Text u Identity ()
forall u. ParsecT Text u Identity ()
spaceParser

-------------------------------------------------------------------------------
-- Renaming a symbol
-------------------------------------------------------------------------------

data Rename = Rename Symbol Name
  deriving (Rename -> Rename -> Bool
(Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool) -> Eq Rename
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rename -> Rename -> Bool
$c/= :: Rename -> Rename -> Bool
== :: Rename -> Rename -> Bool
$c== :: Rename -> Rename -> Bool
Eq,Eq Rename
Eq Rename
-> (Rename -> Rename -> Ordering)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Bool)
-> (Rename -> Rename -> Rename)
-> (Rename -> Rename -> Rename)
-> Ord Rename
Rename -> Rename -> Bool
Rename -> Rename -> Ordering
Rename -> Rename -> Rename
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Rename -> Rename -> Rename
$cmin :: Rename -> Rename -> Rename
max :: Rename -> Rename -> Rename
$cmax :: Rename -> Rename -> Rename
>= :: Rename -> Rename -> Bool
$c>= :: Rename -> Rename -> Bool
> :: Rename -> Rename -> Bool
$c> :: Rename -> Rename -> Bool
<= :: Rename -> Rename -> Bool
$c<= :: Rename -> Rename -> Bool
< :: Rename -> Rename -> Bool
$c< :: Rename -> Rename -> Bool
compare :: Rename -> Rename -> Ordering
$ccompare :: Rename -> Rename -> Ordering
$cp1Ord :: Eq Rename
Ord,Int -> Rename -> ShowS
[Rename] -> ShowS
Rename -> String
(Int -> Rename -> ShowS)
-> (Rename -> String) -> ([Rename] -> ShowS) -> Show Rename
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rename] -> ShowS
$cshowList :: [Rename] -> ShowS
show :: Rename -> String
$cshow :: Rename -> String
showsPrec :: Int -> Rename -> ShowS
$cshowsPrec :: Int -> Rename -> ShowS
Show)

destRename :: Rename -> (Symbol,Name)
destRename :: Rename -> (Symbol, Name)
destRename (Rename Symbol
s Name
n) = (Symbol
s,Name
n)

instance Printable Rename where
  toDoc :: Rename -> Doc
toDoc (Rename Symbol
s Name
n) = Symbol -> Doc
forall a. Printable a => a -> Doc
toDoc Symbol
s Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
"as" Doc -> Doc -> Doc
<+> Name -> Doc
quoteName Name
n

instance Parsable Rename where
  parser :: Parsec Text st Rename
parser = do
      Symbol
s <- Parsec Text st Symbol
forall a st. Parsable a => Parsec Text st a
parser
      ParsecT Text st Identity ()
forall u. ParsecT Text u Identity ()
space
      String
_ <- String -> ParsecT Text st Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
Parsec.string String
"as"
      ParsecT Text st Identity ()
forall u. ParsecT Text u Identity ()
space
      Name
n2 <- Parsec Text st Name
forall a st. Parsable a => Parsec Text st a
parser
      Rename -> Parsec Text st Rename
forall (m :: * -> *) a. Monad m => a -> m a
return (Rename -> Parsec Text st Rename)
-> Rename -> Parsec Text st Rename
forall a b. (a -> b) -> a -> b
$ Symbol -> Name -> Rename
Rename Symbol
s Name
n2
    where
      space :: ParsecT Text u Identity ()
space = ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany1 ParsecT Text u Identity ()
forall u. ParsecT Text u Identity ()
spaceParser

-------------------------------------------------------------------------------
-- A collection of symbol renamings
-------------------------------------------------------------------------------

newtype Renames = Renames {Renames -> [Rename]
destRenames :: [Rename]}
  deriving (Renames -> Renames -> Bool
(Renames -> Renames -> Bool)
-> (Renames -> Renames -> Bool) -> Eq Renames
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Renames -> Renames -> Bool
$c/= :: Renames -> Renames -> Bool
== :: Renames -> Renames -> Bool
$c== :: Renames -> Renames -> Bool
Eq,Eq Renames
Eq Renames
-> (Renames -> Renames -> Ordering)
-> (Renames -> Renames -> Bool)
-> (Renames -> Renames -> Bool)
-> (Renames -> Renames -> Bool)
-> (Renames -> Renames -> Bool)
-> (Renames -> Renames -> Renames)
-> (Renames -> Renames -> Renames)
-> Ord Renames
Renames -> Renames -> Bool
Renames -> Renames -> Ordering
Renames -> Renames -> Renames
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Renames -> Renames -> Renames
$cmin :: Renames -> Renames -> Renames
max :: Renames -> Renames -> Renames
$cmax :: Renames -> Renames -> Renames
>= :: Renames -> Renames -> Bool
$c>= :: Renames -> Renames -> Bool
> :: Renames -> Renames -> Bool
$c> :: Renames -> Renames -> Bool
<= :: Renames -> Renames -> Bool
$c<= :: Renames -> Renames -> Bool
< :: Renames -> Renames -> Bool
$c< :: Renames -> Renames -> Bool
compare :: Renames -> Renames -> Ordering
$ccompare :: Renames -> Renames -> Ordering
$cp1Ord :: Eq Renames
Ord,Int -> Renames -> ShowS
[Renames] -> ShowS
Renames -> String
(Int -> Renames -> ShowS)
-> (Renames -> String) -> ([Renames] -> ShowS) -> Show Renames
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Renames] -> ShowS
$cshowList :: [Renames] -> ShowS
show :: Renames -> String
$cshow :: Renames -> String
showsPrec :: Int -> Renames -> ShowS
$cshowsPrec :: Int -> Renames -> ShowS
Show)

instance Printable Renames where
  toDoc :: Renames -> Doc
toDoc = [Doc] -> Doc
PP.vcat ([Doc] -> Doc) -> (Renames -> [Doc]) -> Renames -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rename -> Doc) -> [Rename] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Rename -> Doc
forall a. Printable a => a -> Doc
toDoc ([Rename] -> [Doc]) -> (Renames -> [Rename]) -> Renames -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Renames -> [Rename]
destRenames

instance Parsable Renames where
  parser :: Parsec Text st Renames
parser = do
      ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall u. ParsecT Text u Identity ()
eolParser
      [Maybe Rename]
rs <- ParsecT Text st Identity (Maybe Rename)
-> ParsecT Text st Identity ()
-> ParsecT Text st Identity [Maybe Rename]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
Parsec.sepEndBy ParsecT Text st Identity (Maybe Rename)
forall u. ParsecT Text u Identity (Maybe Rename)
line (ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany1 ParsecT Text st Identity ()
forall u. ParsecT Text u Identity ()
eolParser)
      Renames -> Parsec Text st Renames
forall (m :: * -> *) a. Monad m => a -> m a
return (Renames -> Parsec Text st Renames)
-> Renames -> Parsec Text st Renames
forall a b. (a -> b) -> a -> b
$ [Rename] -> Renames
Renames ((Maybe Rename -> Maybe Rename) -> [Maybe Rename] -> [Rename]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Maybe Rename -> Maybe Rename
forall a. a -> a
id [Maybe Rename]
rs)
    where
      line :: ParsecT Text u Identity (Maybe Rename)
line = ParsecT Text u Identity (Maybe Rename)
forall u a. ParsecT Text u Identity (Maybe a)
comment ParsecT Text u Identity (Maybe Rename)
-> ParsecT Text u Identity (Maybe Rename)
-> ParsecT Text u Identity (Maybe Rename)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text u Identity (Maybe Rename)
forall u. ParsecT Text u Identity (Maybe Rename)
rename

      comment :: ParsecT Text u Identity (Maybe a)
comment = do
        Char
_ <- Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'#'
        ParsecT Text u Identity Char -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text u Identity Char
forall st. Parsec Text st Char
lineParser
        Maybe a -> ParsecT Text u Identity (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing

      rename :: ParsecT Text st Identity (Maybe Rename)
rename = do
        Rename
r <- Parsec Text st Rename
forall a st. Parsable a => Parsec Text st a
parser
        ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall u. ParsecT Text u Identity ()
spaceParser
        Maybe Rename -> ParsecT Text st Identity (Maybe Rename)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Rename -> ParsecT Text st Identity (Maybe Rename))
-> Maybe Rename -> ParsecT Text st Identity (Maybe Rename)
forall a b. (a -> b) -> a -> b
$ Rename -> Maybe Rename
forall a. a -> Maybe a
Just Rename
r

concatRenames :: [Renames] -> Renames
concatRenames :: [Renames] -> Renames
concatRenames = [Rename] -> Renames
Renames ([Rename] -> Renames)
-> ([Renames] -> [Rename]) -> [Renames] -> Renames
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Rename]] -> [Rename]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Rename]] -> [Rename])
-> ([Renames] -> [[Rename]]) -> [Renames] -> [Rename]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Renames -> [Rename]) -> [Renames] -> [[Rename]]
forall a b. (a -> b) -> [a] -> [b]
map Renames -> [Rename]
destRenames

-------------------------------------------------------------------------------
-- Interpretations
-------------------------------------------------------------------------------

data Interpret = Interpret (Map Symbol Name)

mk :: Map Symbol Name -> Interpret
mk :: Map Symbol Name -> Interpret
mk Map Symbol Name
m = Map Symbol Name -> Interpret
Interpret ((Symbol -> Name -> Bool) -> Map Symbol Name -> Map Symbol Name
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey Symbol -> Name -> Bool
norm Map Symbol Name
m)
  where
    norm :: Symbol -> Name -> Bool
norm Symbol
s Name
n = Symbol -> Name
symbolName Symbol
s Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n

empty :: Interpret
empty :: Interpret
empty = Map Symbol Name -> Interpret
mk Map Symbol Name
forall k a. Map k a
Map.empty

toRenames :: Interpret -> Renames
toRenames :: Interpret -> Renames
toRenames (Interpret Map Symbol Name
m) = [Rename] -> Renames
Renames (((Symbol, Name) -> Rename) -> [(Symbol, Name)] -> [Rename]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> Name -> Rename) -> (Symbol, Name) -> Rename
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Name -> Rename
Rename) (Map Symbol Name -> [(Symbol, Name)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol Name
m))

fromRenames :: Renames -> Maybe Interpret
fromRenames :: Renames -> Maybe Interpret
fromRenames (Renames [Rename]
l) = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Map Symbol Name -> Int
forall k a. Map k a -> Int
Map.size Map Symbol Name
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Rename] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Rename]
l)
    Interpret -> Maybe Interpret
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol Name -> Interpret
mk Map Symbol Name
m)
  where
    m :: Map Symbol Name
m = [(Symbol, Name)] -> Map Symbol Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, Name)] -> Map Symbol Name)
-> [(Symbol, Name)] -> Map Symbol Name
forall a b. (a -> b) -> a -> b
$ (Rename -> (Symbol, Name)) -> [Rename] -> [(Symbol, Name)]
forall a b. (a -> b) -> [a] -> [b]
map Rename -> (Symbol, Name)
destRename [Rename]
l

fromRenamesUnsafe :: Renames -> Interpret
fromRenamesUnsafe :: Renames -> Interpret
fromRenamesUnsafe Renames
r =
    case Renames -> Maybe Interpret
fromRenames Renames
r of
      Just Interpret
i -> Interpret
i
      Maybe Interpret
Nothing -> String -> Interpret
forall a. HasCallStack => String -> a
error String
"HOL.OpenTheory.Interpret.fromRenames failed"

instance Printable Interpret where
  toDoc :: Interpret -> Doc
toDoc = Renames -> Doc
forall a. Printable a => a -> Doc
toDoc (Renames -> Doc) -> (Interpret -> Renames) -> Interpret -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interpret -> Renames
toRenames

instance Parsable Interpret where
  parser :: Parsec Text st Interpret
parser = (Renames -> Interpret)
-> ParsecT Text st Identity Renames -> Parsec Text st Interpret
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Renames -> Interpret
fromRenamesUnsafe ParsecT Text st Identity Renames
forall a st. Parsable a => Parsec Text st a
parser

-------------------------------------------------------------------------------
-- Applying interpretations
-------------------------------------------------------------------------------

interpret :: Interpret -> Symbol -> Name
interpret :: Interpret -> Symbol -> Name
interpret (Interpret Map Symbol Name
m) Symbol
s =
    case Symbol -> Map Symbol Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s Map Symbol Name
m of
      Just Name
n -> Name
n
      Maybe Name
Nothing -> Symbol -> Name
symbolName Symbol
s

interpretTypeOp :: Interpret -> Name -> Name
interpretTypeOp :: Interpret -> Name -> Name
interpretTypeOp Interpret
i = Interpret -> Symbol -> Name
interpret Interpret
i (Symbol -> Name) -> (Name -> Symbol) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Symbol
TypeOpSymbol

interpretConst :: Interpret -> Name -> Name
interpretConst :: Interpret -> Name -> Name
interpretConst Interpret
i = Interpret -> Symbol -> Name
interpret Interpret
i (Symbol -> Name) -> (Name -> Symbol) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Symbol
ConstSymbol

-------------------------------------------------------------------------------
-- Composing interpretations, should satisfy
--
-- |- interpret (compose i1 i2) s == interpret i2 (interpret i1 s)
-------------------------------------------------------------------------------

compose :: Interpret -> Interpret -> Interpret
compose :: Interpret -> Interpret -> Interpret
compose Interpret
i1 Interpret
i2 = Map Symbol Name -> Interpret
mk (Map Symbol Name -> Interpret) -> Map Symbol Name -> Interpret
forall a b. (a -> b) -> a -> b
$ (Symbol -> Name -> Map Symbol Name -> Map Symbol Name)
-> Map Symbol Name -> Map Symbol Name -> Map Symbol Name
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Symbol -> Name -> Map Symbol Name -> Map Symbol Name
inc (Interpret -> Map Symbol Name
dest Interpret
i2) (Interpret -> Map Symbol Name
dest Interpret
i1)
  where
    dest :: Interpret -> Map Symbol Name
dest (Interpret Map Symbol Name
m) = Map Symbol Name
m
    inc :: Symbol -> Name -> Map Symbol Name -> Map Symbol Name
inc Symbol
s1 Name
n1 Map Symbol Name
m2 = Symbol -> Name -> Map Symbol Name -> Map Symbol Name
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
s1 (Interpret -> Symbol -> Name
interpret Interpret
i2 (Symbol -> Name -> Symbol
renameSymbol Symbol
s1 Name
n1)) Map Symbol Name
m2