| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
InformathAPI
Contents
- The environment
- Default source files, which can be changed in Env flags (see RunInformath -help)
- Main types involved
- Main conversion steps
- Conversion outcomes
- The conversions in more detail
- Dedukti-internal onversions
- Phases of the conversion pipeline
- Printing conversions
- Reading input for processing
- Statistics about data.
Description
This file defines top-level conversions between different formats. The main directions are from Dedukti to Agda, Lean, and Rocq on the formal side and English, French, German, and Swedish on the natural language side. Also translations directly between natural languages are possible.
Synopsis
- readEnv :: [Flag] -> IO Env
- readGFGrammar :: FilePath -> IO PGF
- readConstantTable :: PGF -> [FilePath] -> IO (ConstantTable, ConversionTable, DropTable)
- mkLanguage :: PGF -> String -> Language
- grammarFile :: String
- baseConstantFile :: String
- constantTableFile :: String
- type GFTree = Expr
- type DkJmt = Jmt
- processDeduktiModule :: Env -> Module -> [GenResult]
- processLatex :: Env -> String -> [ParseResult]
- data GenResult = GenResult {
- originalDedukti :: Jmt
- annotatedDedukti :: Jmt
- coreGF :: GFTree
- nlgResults :: [(Language, [((GFTree, String), (Scores, Int))])]
- backToDedukti :: [Jmt]
- data ParseResult = ParseResult {
- originalLine :: String
- lexedLine :: String
- termIndex :: [String]
- indexedLine :: String
- parseMessage :: String
- unknownWords :: [String]
- parseResults :: [GFTree]
- formalResults :: [(GFTree, GFTree, GFTree, [Jmt])]
- transResults :: [String]
- processJmt :: Env -> Jmt -> GenResult
- dummyGenResult :: Jmt -> GenResult
- processLatexLine :: Env -> String -> ParseResult
- applyDeduktiConversions :: Env -> DkTree a -> DkTree a
- annotateDedukti :: Env -> Jmt -> Jmt
- dedukti2core :: Jmt -> GJmt
- checkConstantTable :: Module -> PGF -> ConstantTable -> String
- printConstantTable :: ConstantTable -> String
- printGenResult :: Env -> GenResult -> [String]
- printNLGOutput :: Env -> GenResult -> [String]
- showJsonGenResult :: Env -> GenResult -> String
- printRank :: ((GFTree, String), (Scores, Int)) -> String
- showParallelData :: Env -> GenResult -> String
- printFormalismJmt :: Env -> String -> Jmt -> String
- dedukti2agda :: Env -> Jmt -> String
- dedukti2lean :: Env -> Jmt -> String
- dedukti2rocq :: Env -> Jmt -> String
- checkJmt :: Jmt -> Bool
- printParseResult :: Env -> ParseResult -> [String]
- printDeduktiOutput :: Env -> ParseResult -> [String]
- printFinalParseResult :: Env -> (GFTree, GFTree, GFTree, [Jmt]) -> String
- printResults :: Env -> [String] -> [String]
- printDeduktiEnv :: Print a => Env -> a -> String
- core2ext :: Env -> GJmt -> [GJmt]
- rankGFTreesAndNat :: Env -> [(Expr, String)] -> [((Expr, String), (Scores, Int))]
- ext2core :: GJmt -> GJmt
- gjmt2dedukti :: Env -> GJmt -> [Jmt]
- core2dedukti :: Env -> GJmt -> [Jmt]
- readDeduktiModule :: [FilePath] -> IO Module
- parseDeduktiModule :: String -> Module
- gftree2nat :: Env -> Language -> GFTree -> String
- unlex :: Env -> String -> String
- identsInDedukti :: Env -> Module -> [(String, Int)]
- unknownWordsInTex :: Env -> String -> [(String, Int)]
- missingWords :: Env -> String -> [String]
The environment
The environment, of type Env, is a large record of data and methods that affect the conversions and the way they are displayed. It is defined in the module Environment, which is not exported by the API. Most of the functions here presuppose an Env, which is read using a list of flags. This list can empty, which results in a default environment.
Flags are strings of the forms -option of -flag=value. The actual flags can be seen with RunInformath -help. The same flags can be written in the [Flag] list when calling readEnv as an API function.
Low-level access to data sources
readGFGrammar :: FilePath -> IO PGF #
The most important data source are a GF grammar (file .pgf) and a ConstantTable (file .dkgf). Both of these can be customized and passed as values of flags. The following functions read them directly, but need hardly be called explicitly.
To read the GF grammar from a .pgf file.
readConstantTable :: PGF -> [FilePath] -> IO (ConstantTable, ConversionTable, DropTable) #
To read a constant table from a .dkgf file.
mkLanguage :: PGF -> String -> Language #
To construct a concrete syntax name from a 3-letter language code.
Default source files, which can be changed in Env flags (see RunInformath -help)
grammarFile :: String #
Main types involved
Main conversion steps
processDeduktiModule :: Env -> Module -> [GenResult] #
The whole line of generation from Dedukti to formal and natural languages.
processLatex :: Env -> String -> [ParseResult] #
The whole line of parsing latex code and converting to Dedukti. This assumes that parsing units are single lines not starting with a backslash or %
Conversion outcomes
The result of conversion from Dedukti, with intermediate phases available for debugging.
Constructors
| GenResult | |
Fields
| |
data ParseResult #
The result of conversion from informal Latex text, with intermediate phases for debugging.
Constructors
| ParseResult | |
Fields
| |
The conversions in more detail
processJmt :: Env -> Jmt -> GenResult #
Processing a single Dedukti judgement.
dummyGenResult :: Jmt -> GenResult #
When just converting form Dk to another formalism, no GF is needed.
processLatexLine :: Env -> String -> ParseResult #
Processing a single line of LaTeX.
Dedukti-internal onversions
applyDeduktiConversions :: Env -> DkTree a -> DkTree a #
Selected by flags in the environment, see -help.
Phases of the conversion pipeline
annotateDedukti :: Env -> Jmt -> Jmt #
Annotate Dedukti with GF information.
dedukti2core :: Jmt -> GJmt #
From annotated Dedukti to MathCore.
checkConstantTable :: Module -> PGF -> ConstantTable -> String #
Printing conversions
Conversions starting from Dedukti
printGenResult :: Env -> GenResult -> [String] #
With or without intermediate phases, as selected by flags in Env.
printNLGOutput :: Env -> GenResult -> [String] #
Just the filan NLG results.
showJsonGenResult :: Env -> GenResult -> String #
printRank :: ((GFTree, String), (Scores, Int)) -> String #
The scores for each tree an string, in JSON.
showParallelData :: Env -> GenResult -> String #
Parallel data, usable for extracting pairs for trainingan an LLN.
printFormalismJmt :: Env -> String -> Jmt -> String #
Converting Dedukti code to different formalisms.
dedukti2agda :: Env -> Jmt -> String #
These are syntactic conversions, therefore total but may fail to typecheck in the targets. | Notice: imports may have to be added to the generated files.
dedukti2lean :: Env -> Jmt -> String #
dedukti2rocq :: Env -> Jmt -> String #
Conversions starting from natural language
printParseResult :: Env -> ParseResult -> [String] #
Print the parse results with all intermediate phases.
printDeduktiOutput :: Env -> ParseResult -> [String] #
Print just the resulting Dedukti code.
printFinalParseResult :: Env -> (GFTree, GFTree, GFTree, [Jmt]) -> String #
Print both GF trees and resulting Dedukti, in JSON.
General printing facilities
printResults :: Env -> [String] -> [String] #
Results are printed line by line, or with a Latex preamble in a document environment.
printDeduktiEnv :: Print a => Env -> a -> String #
To print Dedukti under environment options, given in flags.
Seldom explicitly needed one-step conversion.
gjmt2dedukti :: Env -> GJmt -> [Jmt] #
core2dedukti :: Env -> GJmt -> [Jmt] #
Reading input for processing
readDeduktiModule :: [FilePath] -> IO Module #
Tp read a Dedukti module from one or more files; in translations, only from one file.
parseDeduktiModule :: String -> Module #
To parse a Dedukti file into its AST.
Statistics about data.
identsInDedukti :: Env -> Module -> [(String, Int)] #
Statistics of unknown identifiers in Dedukti (not listed in .dkgf)
unknownWordsInTex :: Env -> String -> [(String, Int)] #
Statistics of unknown words in text (not recognized in .pgf).
missingWords :: Env -> String -> [String] #
List of missing words on a line.