-- Pretty-printing of formulae. WARNING: icky code inside!
{-# LANGUAGE FlexibleContexts, TypeSynonymInstances, TypeOperators, FlexibleInstances, CPP, GADTs, PatternGuards #-}
module Jukebox.TPTP.Print(prettyShow, prettyNames, showClauses, pPrintClauses, showProblem, pPrintProblem, pPrintProof)
       where

#include "errors.h"
import Prelude hiding ((<>))
import Data.Char
import Data.Maybe
import Text.PrettyPrint.HughesPJ
import qualified Jukebox.TPTP.Lexer as L
import Jukebox.Form
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import qualified Data.Set as Set
import Data.Set(Set)
import Jukebox.Name
import Jukebox.Utils
import Text.PrettyPrint.HughesPJClass
import Control.Monad.Trans.State.Strict
import Data.Symbol

pPrintClauses :: Problem Clause -> Doc
pPrintClauses :: Problem Clause -> Doc
pPrintClauses Problem Clause
prob0
  | Problem Clause -> Bool
forall a. Symbolic a => a -> Bool
isReallyFof Problem Clause
prob = [Doc] -> Doc
vcat ((Input Clause -> Doc) -> Problem Clause -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> (Clause -> Doc) -> Input Clause -> Doc
forall a. String -> (a -> Doc) -> Input a -> Doc
pPrintInput String
"cnf" Clause -> Doc
forall a. Pretty a => a -> Doc
pPrint) Problem Clause
prob)
  | Bool
otherwise = String -> Problem Form -> Doc
pPrintProblem String
"tcf" ((Input Clause -> Input Form) -> Problem Clause -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map ((Clause -> Form) -> Input Clause -> Input Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Form
toForm) Problem Clause
prob)
  where
    prob :: Problem Clause
prob = Problem Clause -> Problem Clause
forall a. Symbolic a => a -> a
prettyNames Problem Clause
prob0

showClauses :: Problem Clause -> String
showClauses :: Problem Clause -> String
showClauses = Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> (Problem Clause -> Doc) -> Problem Clause -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Problem Clause -> Doc
pPrintClauses

pPrintProblem :: String -> Problem Form -> Doc
-- "kind" is only used if the problem is typed
pPrintProblem :: String -> Problem Form -> Doc
pPrintProblem String
kind Problem Form
prob0
  | Problem Form -> Bool
forall a. Symbolic a => a -> Bool
isReallyFof Problem Form
prob = [Doc] -> Doc
vcat ((Input Form -> Doc) -> Problem Form -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> (Form -> Doc) -> Input Form -> Doc
forall a. String -> (a -> Doc) -> Input a -> Doc
pPrintInput String
"fof" (Rational -> Form -> Doc
pPrintFof Rational
0)) Problem Form
prob)
  | Bool
otherwise = [Doc] -> Doc
vcat (String -> Problem Form -> [Doc]
pPrintDecls String
kind Problem Form
prob [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (Input Form -> Doc) -> Problem Form -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> (Form -> Doc) -> Input Form -> Doc
forall a. String -> (a -> Doc) -> Input a -> Doc
pPrintInput String
kind (Rational -> Form -> Doc
pPrintTff Rational
0)) Problem Form
prob)
  where
    prob :: Problem Form
prob = Problem Form -> Problem Form
forall a. Symbolic a => a -> a
prettyNames Problem Form
prob0

-- Print a problem together with all source/derivation information.
pPrintProof :: Problem Form -> Doc
pPrintProof :: Problem Form -> Doc
pPrintProof Problem Form
prob =
  [(Input Form, (String, [Doc]))] -> Doc
pPrintAnnotProof (State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
-> (Int, Map (Kind, Form) Int) -> [(Input Form, (String, [Doc]))]
forall s a. State s a -> s -> a
evalState ([[(Input Form, (String, [Doc]))]]
-> [(Input Form, (String, [Doc]))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Input Form, (String, [Doc]))]]
 -> [(Input Form, (String, [Doc]))])
-> StateT
     (Int, Map (Kind, Form) Int)
     Identity
     [[(Input Form, (String, [Doc]))]]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Input Form
 -> State
      (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))])
-> Problem Form
-> StateT
     (Int, Map (Kind, Form) Int)
     Identity
     [[(Input Form, (String, [Doc]))]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Input Form
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
annot Problem Form
prob) (Int
1, Map (Kind, Form) Int
forall k a. Map k a
Map.empty))
  where
    fun :: String -> [Doc] -> Doc
fun String
f [] = String -> Doc
text String
f
    fun String
f [Doc]
xs = String -> Doc
text String
f Doc -> Doc -> Doc
<> Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
xs))
    list :: [Doc] -> Doc
list = Doc -> Doc
brackets (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma

    clause :: a -> String
clause a
n = String
"c" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n

    info :: Input b -> (Kind, b)
info Input b
inp = (Input b -> Kind
forall a. Input a -> Kind
kind Input b
inp, Input b -> b
forall a. Input a -> a
what Input b
inp)

    -- We maintain: the set of formulas printed so far,
    -- and the highest number given so far.
    findNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
    findNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
findNumber Input Form
inp =
      ((Int, Map (Kind, Form) Int) -> Maybe Int)
-> State (Int, Map (Kind, Form) Int) (Maybe Int)
forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets ((Kind, Form) -> Map (Kind, Form) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Input Form -> (Kind, Form)
forall b. Input b -> (Kind, b)
info Input Form
inp) (Map (Kind, Form) Int -> Maybe Int)
-> ((Int, Map (Kind, Form) Int) -> Map (Kind, Form) Int)
-> (Int, Map (Kind, Form) Int)
-> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Map (Kind, Form) Int) -> Map (Kind, Form) Int
forall a b. (a, b) -> b
snd)

    newNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
    newNumber :: Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
newNumber Input Form
inp = do
      (Int
n, Map (Kind, Form) Int
map) <- StateT
  (Int, Map (Kind, Form) Int) Identity (Int, Map (Kind, Form) Int)
forall (m :: * -> *) s. Monad m => StateT s m s
get
      case (Kind, Form) -> Map (Kind, Form) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Input Form -> (Kind, Form)
forall b. Input b -> (Kind, b)
info Input Form
inp) Map (Kind, Form) Int
map of
        Maybe Int
Nothing -> do
          (Int, Map (Kind, Form) Int)
-> StateT (Int, Map (Kind, Form) Int) Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, (Kind, Form) -> Int -> Map (Kind, Form) Int -> Map (Kind, Form) Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Input Form -> (Kind, Form)
forall b. Input b -> (Kind, b)
info Input Form
inp) Int
n Map (Kind, Form) Int
map)
          Maybe Int -> State (Int, Map (Kind, Form) Int) (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)
        Just Int
_ -> Maybe Int -> State (Int, Map (Kind, Form) Int) (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing

    annot :: Input Form -> State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
    annot :: Input Form
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
annot Input Form
inp
      -- Formula is identical to its parent
      | Inference String
_ String
_ [Input Form
inp'] <- Input Form -> InputSource
forall a. Input a -> InputSource
source Input Form
inp,
          let [Form
p, Form
q] = [Form] -> [Form]
forall a. Symbolic a => a -> a
prettyNames [Input Form -> Form
forall a. Input a -> a
what Input Form
inp, Input Form -> Form
forall a. Input a -> a
what Input Form
inp'] in
          Input Form -> Kind
forall a. Input a -> Kind
kind Input Form
inp Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Input Form -> Kind
forall a. Input a -> Kind
kind Input Form
inp' Bool -> Bool -> Bool
&&
          -- I have NO idea why this doesn't work without show here :(
          Form -> String
forall a. Show a => a -> String
show Form
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Form -> String
forall a. Show a => a -> String
show Form
q =
            Input Form
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
annot Input Form
inp { source :: InputSource
source = Input Form -> InputSource
forall a. Input a -> InputSource
source Input Form
inp' }
      | Bool
otherwise = do
          Maybe Int
mn <- Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
findNumber Input Form
inp
          case Maybe Int
mn of
            Just Int
_ ->
              -- Already processed this formula
              [(Input Form, (String, [Doc]))]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
forall (m :: * -> *) a. Monad m => a -> m a
return []
            Maybe Int
Nothing -> do
              let
                ret :: String
-> [Doc]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
ret String
k [Doc]
stuff = do
                  Maybe Int
res <- Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
newNumber Input Form
inp
                  case Maybe Int
res of
                    Just Int
n ->
                      [(Input Form, (String, [Doc]))]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Input Form
inp { tag :: String
tag = Int -> String
forall a. Show a => a -> String
clause Int
n }, (String
k, [Doc]
stuff))]
                    Maybe Int
Nothing ->
                      [(Input Form, (String, [Doc]))]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
forall (m :: * -> *) a. Monad m => a -> m a
return []

              case Input Form -> InputSource
forall a. Input a -> InputSource
source Input Form
inp of
                InputSource
Unknown -> String
-> [Doc]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
ret String
"plain" []
                FromFile String
file Int
_ ->
                  String
-> [Doc]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
ret (Kind -> String
forall a. Show a => a -> String
show (Input Form -> Kind
forall a. Input a -> Kind
kind Input Form
inp))
                    [String -> [Doc] -> Doc
fun String
"file" [String -> Doc
text (String -> String
escapeAtom String
file), String -> Doc
text (String -> String
escapeAtom (Input Form -> String
forall a. Input a -> String
tag Input Form
inp))]]
                Inference String
name String
status Problem Form
parents -> do
                  -- Process all parents first
                  [[(Input Form, (String, [Doc]))]]
rest <- (Input Form
 -> State
      (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))])
-> Problem Form
-> StateT
     (Int, Map (Kind, Form) Int)
     Identity
     [[(Input Form, (String, [Doc]))]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Input Form
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
annot Problem Form
parents
                  [Int]
nums <- (Maybe Int -> Int) -> [Maybe Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust ([Maybe Int] -> [Int])
-> StateT (Int, Map (Kind, Form) Int) Identity [Maybe Int]
-> StateT (Int, Map (Kind, Form) Int) Identity [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int))
-> Problem Form
-> StateT (Int, Map (Kind, Form) Int) Identity [Maybe Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Input Form -> State (Int, Map (Kind, Form) Int) (Maybe Int)
findNumber Problem Form
parents

                  ([(Input Form, (String, [Doc]))]
 -> [(Input Form, (String, [Doc]))])
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([[(Input Form, (String, [Doc]))]]
-> [(Input Form, (String, [Doc]))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Input Form, (String, [Doc]))]]
rest [(Input Form, (String, [Doc]))]
-> [(Input Form, (String, [Doc]))]
-> [(Input Form, (String, [Doc]))]
forall a. [a] -> [a] -> [a]
++) (State (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
 -> State
      (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))])
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
forall a b. (a -> b) -> a -> b
$
                    String
-> [Doc]
-> State
     (Int, Map (Kind, Form) Int) [(Input Form, (String, [Doc]))]
ret String
"plain"
                      [String -> [Doc] -> Doc
fun String
"inference" [
                        String -> Doc
text String
name, [Doc] -> Doc
list [String -> [Doc] -> Doc
fun String
"status" [String -> Doc
text String
status]],
                        [Doc] -> Doc
list [String -> Doc
text (Int -> String
forall a. Show a => a -> String
clause Int
n) | Int
n <- [Int]
nums]]]

pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc
pPrintAnnotProof :: [(Input Form, (String, [Doc]))] -> Doc
pPrintAnnotProof [(Input Form, (String, [Doc]))]
annots0 =
  [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
    [ [Doc] -> Doc
vcat (String -> Problem Form -> [Doc]
pPrintDecls String
"tff" Problem Form
inps) | Bool -> Bool
not (Problem Form -> Bool
forall a. Symbolic a => a -> Bool
isReallyFof Problem Form
inps) ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
    [ String -> String -> String -> [Doc] -> Doc
pPrintClause (Form -> String
family Form
x) (Input Form -> String
forall a. Input a -> String
tag Input Form
inp) String
k (Form -> Doc
pp Form
xDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:[Doc]
rest)
    | (Input Form
inp, (String
k, [Doc]
rest)) <- [(Input Form, (String, [Doc]))]
annots,
      let x :: Form
x = Input Form -> Form
forall a. Input a -> a
what Input Form
inp ]
  where
    inps0 :: Problem Form
inps0 = ((Input Form, (String, [Doc])) -> Input Form)
-> [(Input Form, (String, [Doc]))] -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map (Input Form, (String, [Doc])) -> Input Form
forall a b. (a, b) -> a
fst [(Input Form, (String, [Doc]))]
annots0
    inps :: Problem Form
inps = Problem Form -> Problem Form
forall a. Symbolic a => a -> a
prettyNames Problem Form
inps0
    annots :: [(Input Form, (String, [Doc]))]
annots = Problem Form
-> [(String, [Doc])] -> [(Input Form, (String, [Doc]))]
forall a b. [a] -> [b] -> [(a, b)]
zip Problem Form
inps (((Input Form, (String, [Doc])) -> (String, [Doc]))
-> [(Input Form, (String, [Doc]))] -> [(String, [Doc])]
forall a b. (a -> b) -> [a] -> [b]
map (Input Form, (String, [Doc])) -> (String, [Doc])
forall a b. (a, b) -> b
snd [(Input Form, (String, [Doc]))]
annots0)

    family :: Form -> String
family Form
x
      | Form -> Bool
forall a. Symbolic a => a -> Bool
isReallyFof Form
x Bool -> Bool -> Bool
&& Maybe Clause -> Bool
forall a. Maybe a -> Bool
isJust (Form -> Maybe Clause
toClause Form
x) = String
"cnf"
      | Form -> Bool
forall a. Symbolic a => a -> Bool
isReallyFof Form
x = String
"fof"
      | Bool
otherwise = String
"tff"

    pp :: Form -> Doc
pp Form
x
      | Form -> Bool
forall a. Symbolic a => a -> Bool
isReallyFof Form
x =
        case Form -> Maybe Clause
toClause Form
x of
          Maybe Clause
Nothing -> Rational -> Form -> Doc
pPrintFof Rational
0 Form
x
          Just Clause
cl -> Clause -> Doc
forall a. Pretty a => a -> Doc
pPrint Clause
cl
      | Bool
otherwise =
        Rational -> Form -> Doc
pPrintTff Rational
0 Form
x

showProblem :: Problem Form -> String
showProblem :: Problem Form -> String
showProblem = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Problem Form -> Doc) -> Problem Form -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Problem Form -> Doc
pPrintProblem String
"tff"

isReallyFof :: Symbolic a => a -> Bool
isReallyFof :: a -> Bool
isReallyFof = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
p ([Type] -> Bool) -> (a -> [Type]) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Type]
forall a. Symbolic a => a -> [Type]
types
  where
    p :: Type -> Bool
p Type
O = Bool
True
    p (Type Name
ty) | Name
ty Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
i = Bool
True
    p Type
_ = Bool
False
    i :: Name
i = String -> Name
forall a. Named a => a -> Name
name String
"$i"

pPrintDecls :: String -> Problem Form -> [Doc]
pPrintDecls :: String -> Problem Form -> [Doc]
pPrintDecls String
kind Problem Form
prob =
  (Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
typeDecl ([Type] -> [Type]
forall a. Ord a => [a] -> [a]
usort (Problem Form -> [Type]
forall a. Symbolic a => a -> [Type]
types Problem Form
prob)) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
  ((Name ::: FunType) -> Doc) -> [Name ::: FunType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name ::: FunType) -> Doc
forall a a. (Show a, Pretty a) => (a ::: a) -> Doc
funcDecl ([Name ::: FunType] -> [Name ::: FunType]
forall a. Ord a => [a] -> [a]
usort (Problem Form -> [Name ::: FunType]
forall a. Symbolic a => a -> [Name ::: FunType]
functions Problem Form
prob))
  where
    typeDecl :: Type -> Doc
typeDecl Type
O = Doc
empty
    typeDecl (Type Name
ty) | Name
ty Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
i = Doc
empty
    typeDecl Type
ty = Type -> Doc -> Doc
forall a. Show a => a -> Doc -> Doc
typeClause Type
ty (String -> Doc
text String
"$tType")
    i :: Name
i = String -> Name
forall a. Named a => a -> Name
name String
"$i"

    funcDecl :: (a ::: a) -> Doc
funcDecl (a
f ::: a
ty) = a -> Doc -> Doc
forall a. Show a => a -> Doc -> Doc
typeClause a
f (a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
ty)

    typeClause :: Show a => a -> Doc -> Doc
    typeClause :: a -> Doc -> Doc
typeClause a
name Doc
ty =
      String -> String -> String -> [Doc] -> Doc
pPrintClause String
kind String
"type" String
"type"
        [String -> Doc
text (String -> String
escapeAtom (a -> String
forall a. Show a => a -> String
show a
name)) Doc -> Doc -> Doc
<> Doc
colon Doc -> Doc -> Doc
<+> Doc
ty]

instance Pretty a => Pretty (Input a) where
  pPrint :: Input a -> Doc
pPrint = String -> (a -> Doc) -> Input a -> Doc
forall a. String -> (a -> Doc) -> Input a -> Doc
pPrintInput String
"tff" a -> Doc
forall a. Pretty a => a -> Doc
pPrint
instance Pretty a => Show (Input a) where
  show :: Input a -> String
show = Input a -> String
forall a. Pretty a => a -> String
prettyShow

pPrintInput :: String -> (a -> Doc) -> Input a -> Doc
pPrintInput :: String -> (a -> Doc) -> Input a -> Doc
pPrintInput String
family a -> Doc
pp Input a
i =
  String -> String -> String -> [Doc] -> Doc
pPrintClause String
family (Input a -> String
forall a. Input a -> String
tag Input a
i) (Kind -> String
forall a. Show a => a -> String
show (Input a -> Kind
forall a. Input a -> Kind
kind Input a
i)) [a -> Doc
pp (Input a -> a
forall a. Input a -> a
what Input a
i)]

pPrintClause :: String -> String -> String -> [Doc] -> Doc
pPrintClause :: String -> String -> String -> [Doc] -> Doc
pPrintClause String
family String
name String
kind [Doc]
rest =
  String -> Doc
text String
family Doc -> Doc -> Doc
<> Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([String -> Doc
text (String -> String
escapeAtom String
name), String -> Doc
text String
kind] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
rest))) Doc -> Doc -> Doc
<> String -> Doc
text String
"."

instance Pretty Clause where
  pPrint :: Clause -> Doc
pPrint (Clause (Bind Set Variable
_ [Literal]
ts)) =
    (Variable -> Doc) -> Rational -> String -> String -> [Form] -> Doc
pPrintConnective Variable -> Doc
forall a. HasCallStack => a
undefined Rational
0 String
"$false" String
"|" ((Literal -> Form) -> [Literal] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Form
Literal [Literal]
ts)

instance Show Clause where
  show :: Clause -> String
show = Clause -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty Type where
  pPrint :: Type -> Doc
pPrint Type
O = String -> Doc
text String
"$o"
  pPrint Type
ty = String -> Doc
text (String -> Doc) -> (Type -> String) -> Type -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escapeAtom (String -> String) -> (Type -> String) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Show a => a -> String
show (Name -> String) -> (Type -> Name) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Name
tname (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Type
ty

instance Show Type where
  show :: Type -> String
show = Type -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty FunType where
  pPrint :: FunType -> Doc
pPrint FunType{args :: FunType -> [Type]
args = [Type]
args, res :: FunType -> Type
res = Type
res} =
    case [Type]
args of
      [] -> Type -> Doc
forall a. Pretty a => a -> Doc
pPrint Type
res
      [Type]
args -> [Type] -> Doc
forall a. Pretty a => [a] -> Doc
pPrintTypes [Type]
args Doc -> Doc -> Doc
<+> String -> Doc
text String
">" Doc -> Doc -> Doc
<+>
              Type -> Doc
forall a. Pretty a => a -> Doc
pPrint Type
res
    where
      pPrintTypes :: [a] -> Doc
pPrintTypes [a
arg] = a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
arg
      pPrintTypes [a]
args =
        Doc -> Doc
parens (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text String
" *") ([Doc] -> [Doc]) -> ([a] -> [Doc]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pPrint ([a] -> Doc) -> [a] -> Doc
forall a b. (a -> b) -> a -> b
$ [a]
args

instance Show FunType where
  show :: FunType -> String
show = FunType -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty Name where
  pPrint :: Name -> Doc
pPrint = String -> Doc
text (String -> Doc) -> (Name -> String) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Show a => a -> String
show

instance Show L.Token where
  show :: Token -> String
show L.Atom{tokenName :: Token -> Symbol
L.tokenName = Symbol
x} = String -> String
escapeAtom (Symbol -> String
unintern Symbol
x)
  show L.Defined{defined :: Token -> Defined
L.defined = Defined
x} = Defined -> String
forall a. Show a => a -> String
show Defined
x
  show L.Var{tokenName :: Token -> Symbol
L.tokenName = Symbol
x} = Symbol -> String
unintern Symbol
x
  show L.DistinctObject{tokenName :: Token -> Symbol
L.tokenName = Symbol
x} = Char -> String -> String
quote Char
'"' (Symbol -> String
unintern Symbol
x)
  show L.Number{value :: Token -> Integer
L.value = Integer
x} = Integer -> String
forall a. Show a => a -> String
show Integer
x
  show L.Punct{kind :: Token -> Punct
L.kind = Punct
x} = Punct -> String
forall a. Show a => a -> String
show Punct
x
  show Token
L.Eof = String
"end of file"
  show Token
L.Error = String
"lexical error"

escapeAtom :: String -> String
escapeAtom :: String -> String
escapeAtom String
s | Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s') Bool -> Bool -> Bool
&& Char -> Bool
isLower (String -> Char
forall a. [a] -> a
head String
s') Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isNormal String
s' = String
s
             | Bool
otherwise = Char -> String -> String
quote Char
'\'' String
s
  where isNormal :: Char -> Bool
isNormal Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
        s' :: String
s' = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'$') String
s

quote :: Char -> String -> String
quote :: Char -> String -> String
quote Char
c String
s = [Char
c] String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escape String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
c]
  where escape :: Char -> String
escape Char
c' | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c' = [Char
'\\', Char
c]
        escape Char
'\\' = String
"\\\\"
        escape Char
c = [Char
c]

instance Pretty Term where
  pPrint :: Term -> Doc
pPrint (Var (Name
v ::: Type
_)) =
    Name -> Doc
forall a. Pretty a => a -> Doc
pPrint Name
v
  pPrint ((Name
f ::: FunType
_) :@: []) =
    case Name
f of
      Fixed Integer{} Maybe String
_ -> String -> Doc
text (Name -> String
forall a. Show a => a -> String
show Name
f)
      Fixed Rational{} Maybe String
_ -> String -> Doc
text (Name -> String
forall a. Show a => a -> String
show Name
f)
      Fixed Real{} Maybe String
_ -> String -> Doc
text (Name -> String
forall a. Show a => a -> String
show Name
f)
      Name
_ -> String -> Doc
text (String -> String
escapeAtom (Name -> String
forall a. Show a => a -> String
show Name
f))
  pPrint ((Name
f ::: FunType
_) :@: [Term]
ts) =
    String -> Doc
text (String -> String
escapeAtom (Name -> String
forall a. Show a => a -> String
show Name
f)) Doc -> Doc -> Doc
<>
    Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
forall a. Pretty a => a -> Doc
pPrint [Term]
ts)))

instance Show Term where
  show :: Term -> String
show = Term -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty Atomic where
  pPrint :: Atomic -> Doc
pPrint (Term
t :=: Term
u) = Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
t Doc -> Doc -> Doc
<> String -> Doc
text String
"=" Doc -> Doc -> Doc
<> Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
u
  pPrint (Tru Term
t) = Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
t

instance Show Atomic where
  show :: Atomic -> String
show = Atomic -> String
forall a. Pretty a => a -> String
prettyShow

instance Pretty Form where
  pPrintPrec :: PrettyLevel -> Rational -> Form -> Doc
pPrintPrec PrettyLevel
_ = Rational -> Form -> Doc
pPrintTff

instance Show Form where
  show :: Form -> String
show = Form -> String
forall a. Pretty a => a -> String
prettyShow

pPrintFof, pPrintTff :: Rational -> Form -> Doc
pPrintFof :: Rational -> Form -> Doc
pPrintFof = (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm (\(Name
x ::: Type
_) -> Name -> Doc
forall a. Pretty a => a -> Doc
pPrint Name
x)
pPrintTff :: Rational -> Form -> Doc
pPrintTff = (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm (\(Name
x ::: Type
ty) -> Name -> Doc
forall a. Pretty a => a -> Doc
pPrint Name
x Doc -> Doc -> Doc
<> Doc
colon Doc -> Doc -> Doc
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pPrint Type
ty)

pPrintForm :: (Variable -> Doc) -> Rational -> Form -> Doc
-- We use two precedences, the lowest for binary connectives
-- and the highest for everything else.
pPrintForm :: (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
_bind Rational
_p (Literal (Pos (Term
t :=: Term
u))) =
  Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
t Doc -> Doc -> Doc
<> String -> Doc
text String
"=" Doc -> Doc -> Doc
<> Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
u
pPrintForm Variable -> Doc
_bind Rational
_p (Literal (Neg (Term
t :=: Term
u))) =
  Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
t Doc -> Doc -> Doc
<> String -> Doc
text String
"!=" Doc -> Doc -> Doc
<> Term -> Doc
forall a. Pretty a => a -> Doc
pPrint Term
u
pPrintForm Variable -> Doc
_bind Rational
p (Literal (Pos Atomic
t)) = PrettyLevel -> Rational -> Atomic -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
prettyNormal Rational
p Atomic
t
pPrintForm Variable -> Doc
bind Rational
p (Literal (Neg Atomic
t)) = (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
bind Rational
p (Form -> Form
Not (Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos Atomic
t)))
pPrintForm Variable -> Doc
bind Rational
_p (Not Form
f) = String -> Doc
text String
"~" Doc -> Doc -> Doc
<> (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
bind Rational
1 Form
f
pPrintForm Variable -> Doc
bind Rational
p (And [Form]
ts) = (Variable -> Doc) -> Rational -> String -> String -> [Form] -> Doc
pPrintConnective Variable -> Doc
bind Rational
p String
"$true" String
"&" [Form]
ts
pPrintForm Variable -> Doc
bind Rational
p (Or [Form]
ts) = (Variable -> Doc) -> Rational -> String -> String -> [Form] -> Doc
pPrintConnective Variable -> Doc
bind Rational
p String
"$false" String
"|" [Form]
ts
pPrintForm Variable -> Doc
bind Rational
p (Equiv Form
t Form
u) = (Variable -> Doc) -> Rational -> String -> String -> [Form] -> Doc
pPrintConnective Variable -> Doc
bind Rational
p String
forall a. HasCallStack => a
undefined String
"<=>" [Form
t, Form
u]
pPrintForm Variable -> Doc
bind Rational
_p (ForAll (Bind Set Variable
vs Form
f)) = (Variable -> Doc) -> String -> Set Variable -> Form -> Doc
pPrintQuant Variable -> Doc
bind String
"!" Set Variable
vs Form
f
pPrintForm Variable -> Doc
bind Rational
_p (Exists (Bind Set Variable
vs Form
f)) = (Variable -> Doc) -> String -> Set Variable -> Form -> Doc
pPrintQuant Variable -> Doc
bind String
"?" Set Variable
vs Form
f
pPrintForm Variable -> Doc
bind Rational
p (Connective Connective
c Form
t Form
u) = (Variable -> Doc) -> Rational -> String -> String -> [Form] -> Doc
pPrintConnective Variable -> Doc
bind Rational
p (String -> String
forall a. HasCallStack => String -> a
error String
"pPrint: Connective") (Connective -> String
forall a. Show a => a -> String
show Connective
c) [Form
t, Form
u]

instance Show Connective where
  show :: Connective -> String
show Connective
Implies = String
"=>"
  show Connective
Follows = String
"<="
  show Connective
Xor = String
"<~>"
  show Connective
Nor = String
"~|"
  show Connective
Nand = String
"~&"

pPrintConnective :: (Variable -> Doc) -> Rational -> String -> String -> [Form] -> Doc
pPrintConnective Variable -> Doc
_bind Rational
_p String
ident String
_op [] = String -> Doc
text String
ident
pPrintConnective Variable -> Doc
bind Rational
p String
_ident String
_op [Form
x] = (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
bind Rational
p Form
x
pPrintConnective Variable -> Doc
bind Rational
p String
_ident String
op (Form
x:[Form]
xs) =
  Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
hsep (Form -> Doc
ppr Form
xDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:[ Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
op Doc -> Doc -> Doc
<+> Form -> Doc
ppr Form
x) | Form
x <- [Form]
xs ])
      where ppr :: Form -> Doc
ppr = (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
bind Rational
1
            
pPrintQuant :: (Variable -> Doc) -> String -> Set.Set Variable -> Form -> Doc
pPrintQuant :: (Variable -> Doc) -> String -> Set Variable -> Form -> Doc
pPrintQuant Variable -> Doc
bind String
q Set Variable
vs Form
f
  | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
vs = (Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
bind Rational
1 Form
f
  | Bool
otherwise =
    [Doc] -> Doc
hsep [
      String -> Doc
text String
q Doc -> Doc -> Doc
<> Doc -> Doc
brackets ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((Variable -> Doc) -> [Variable] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Doc
bind (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs)))) Doc -> Doc -> Doc
<> Doc
colon,
      Int -> Doc -> Doc
nest Int
2 ((Variable -> Doc) -> Rational -> Form -> Doc
pPrintForm Variable -> Doc
bind Rational
1 Form
f)]

instance Show Kind where
  show :: Kind -> String
show (Ax AxKind
kind) = AxKind -> String
forall a. Show a => a -> String
show AxKind
kind
  show (Conj ConjKind
kind) = ConjKind -> String
forall a. Show a => a -> String
show ConjKind
kind

instance Show AxKind where
  show :: AxKind -> String
show AxKind
Axiom = String
"axiom"
  show AxKind
Hypothesis = String
"hypothesis"
  show AxKind
Definition = String
"definition"
  show AxKind
Assumption = String
"assumption"
  show AxKind
Lemma = String
"lemma"
  show AxKind
TheoremKind = String
"theorem"
  show AxKind
NegatedConjecture = String
"negated_conjecture"

instance Show ConjKind where
  show :: ConjKind -> String
show ConjKind
Conjecture = String
"conjecture"
  show ConjKind
Question = String
"question"

prettyNames :: Symbolic a => a -> a
prettyNames :: a -> a
prettyNames a
x0 = (Name -> Name) -> a -> a
forall a. Symbolic a => (Name -> Name) -> a -> a
mapName Name -> Name
replace a
x
  where
    replace :: Name -> Name
replace name :: Name
name@Fixed{}  = Name
name
    replace Name
x = Name -> Name -> Map Name Name -> Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Name
forall a. Named a => a -> Name
name (Name -> String
forall a. Named a => a -> String
base Name
x)) Name
x Map Name Name
sub

    sub :: Map Name Name
sub = Map Name Name
globalsScope Map Name Name -> Map Name Name -> Map Name Name
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Set String -> a -> Map Name Name
forall a. Symbolic a => Set String -> a -> Map Name Name
pretty Set String
globalsUsed a
x

    pretty :: Symbolic a => Set String -> a -> Map Name Name
    pretty :: Set String -> a -> Map Name Name
pretty Set String
used a
x =
      case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
x of
        TypeOf a
Bind_ -> Set String -> Bind a -> Map Name Name
forall a. Symbolic a => Set String -> Bind a -> Map Name Name
bind Set String
used a
Bind a
x
        TypeOf a
_ -> (forall a1. Symbolic a1 => a1 -> Map Name Name)
-> a -> Map Name Name
forall a b.
(Symbolic a, Monoid b) =>
(forall a1. Symbolic a1 => a1 -> b) -> a -> b
collect (Set String -> a1 -> Map Name Name
forall a. Symbolic a => Set String -> a -> Map Name Name
pretty Set String
used) a
x

    bind :: Symbolic a => Set String -> Bind a -> Map Name Name
    bind :: Set String -> Bind a -> Map Name Name
bind Set String
used (Bind Set Variable
vs a
x) =
      Map Name Name
scope Map Name Name -> Map Name Name -> Map Name Name
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Set String -> a -> Map Name Name
forall a. Symbolic a => Set String -> a -> Map Name Name
pretty Set String
used' a
x
      where
        (Map Name Name
scope, Set String
used') = Set String -> [Name] -> (Map Name Name, Set String)
forall (t :: * -> *).
Foldable t =>
Set String -> t Name -> (Map Name Name, Set String)
add Set String
used ((Variable -> Name) -> [Variable] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Name
forall a. Named a => a -> Name
name (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs))

    add :: Set String -> t Name -> (Map Name Name, Set String)
add Set String
used t Name
names =
      (Name
 -> (Map Name Name, Set String) -> (Map Name Name, Set String))
-> (Map Name Name, Set String)
-> t Name
-> (Map Name Name, Set String)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> (Map Name Name, Set String) -> (Map Name Name, Set String)
add1 (Map Name Name
forall k a. Map k a
Map.empty, Set String
used) t Name
names

    add1 :: Name -> (Map Name Name, Set String) -> (Map Name Name, Set String)
add1 (Fixed FixedName
xs Maybe String
_) (Map Name Name
scope, Set String
used) =
      (Map Name Name
scope, String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (FixedName -> String
forall a. Show a => a -> String
show FixedName
xs) Set String
used)
    add1 x :: Name
x@(Unique Int64
_ Symbol
base Maybe String
_ Renamer
f) (Map Name Name
scope, Set String
used) =
      String
-> Renamer
-> Name
-> (Map Name Name, Set String)
-> (Map Name Name, Set String)
forall t a t.
(Num t, Enum t, Ord a, Named a) =>
t
-> (t -> t -> Renaming)
-> a
-> (Map a Name, Set String)
-> (Map a Name, Set String)
addWith (Symbol -> String
unintern Symbol
base) Renamer
f Name
x (Map Name Name
scope, Set String
used)
    add1 x :: Name
x@(Variant Name
y [Name]
_ Renamer
f) (Map Name Name
scope, Set String
used) =
      String
-> Renamer
-> Name
-> (Map Name Name, Set String)
-> (Map Name Name, Set String)
forall t a t.
(Num t, Enum t, Ord a, Named a) =>
t
-> (t -> t -> Renaming)
-> a
-> (Map a Name, Set String)
-> (Map a Name, Set String)
addWith (Name -> String
forall a. Named a => a -> String
base Name
y) Renamer
f Name
x (Map Name Name
scope, Set String
used)

    addWith :: t
-> (t -> t -> Renaming)
-> a
-> (Map a Name, Set String)
-> (Map a Name, Set String)
addWith t
base t -> t -> Renaming
f a
x (Map a Name
scope, Set String
used) =
      (a -> Name -> Map a Name -> Map a Name
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
x (Maybe String -> Name -> Name
withMaybeLabel (a -> Maybe String
forall a. Named a => a -> Maybe String
label a
x) (String -> Name
forall a. Named a => a -> Name
name String
winner)) Map a Name
scope,
       String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
winner ([String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList [String]
taken Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set String
used))
      where
        cands :: [Renaming]
cands = [t -> t -> Renaming
f t
base t
n | t
n <- [t
0..]]
        Renaming [String]
taken String
winner =
          [Renaming] -> Renaming
forall a. [a] -> a
head [Renaming
c | c :: Renaming
c@(Renaming [String]
xs String
x) <- [Renaming]
cands,
                Bool -> Bool
not ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
y Set String
used | String
y <- String
xString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
xs ])]

    globals :: [Name]
globals =
      [Name] -> [Name]
forall a. Ord a => [a] -> [a]
usort ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$
        [ Name
f | Name
f ::: FunType
_ <- a -> [Name ::: FunType]
forall a. Symbolic a => a -> [Name ::: FunType]
functions a
x ] [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
        [ Name
ty | Type Name
ty <- a -> [Type]
forall a. Symbolic a => a -> [Type]
types a
x ]
    (Map Name Name
globalsScope, Set String
globalsUsed) = Set String -> [Name] -> (Map Name Name, Set String)
forall (t :: * -> *).
Foldable t =>
Set String -> t Name -> (Map Name Name, Set String)
add Set String
fixed [Name]
globals

    fixed :: Set String
fixed = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList [ FixedName -> String
forall a. Show a => a -> String
show FixedName
xs | Fixed FixedName
xs Maybe String
_ <- a -> [Name]
forall a. Symbolic a => a -> [Name]
names a
x ]

    x :: a
x = a -> (a -> NameM a) -> a
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run a
x0 a -> NameM a
forall a. Symbolic a => a -> NameM a
uniqueNames