tstp2agda- Proof-term reconstruction from TSTP to Agda

Safe HaskellNone




Spaced concatenation

(▪) :: forall a b. (BShow a, BShow b) => a -> b -> String infixr 4

'"foo" ▪ "bar"' = '"foo bar"'. Its main use is to simplify the concatenation of printable types separated by spaces.

class BShow a where

BShow fixes Show String instance behavior length "foo" ≠ length (show "foo") with two new instances (and overlapped) instances for String and Show a.


βshow :: a -> String


Printing with indentation

printInd :: Show a => Int -> a -> IO ()

printInd i b, prints a with b level of indentation i.

putStrLnInd :: Int -> String -> IO ()

printInd i str, prints a with str level of indentation i.

List manipulation

unique :: Ord a => [a] -> [a]

Removes duplicate elements of a list.



:: Eq a 
=> [a]

Current prefix

-> [a]


-> [a]

List to be replaced

-> [a]

Resulting list

swapPrefix a b str, replaces prefix a in str with b checking that a is a prefix of str.


agdafy :: String -> String

Metis identifiers usually contain _ characters which are invalid in Agda, agdafy replaces normalize_0_0 with normalize-0-0. This is mostly used inside the Happy parser every time an AtomicWord is created.

stdout2file :: Maybe FilePath -> IO ()

Redirect all stdout output into a file or do nothing (in case of Nothing)

checkIdScope :: Int -> String -> Set (Int, String) -> Bool

checkIdScope i t s check if any name in s has a more general scope than t with level i