ProofPrettyPrinter
-
The First-Order LoopW Type Inference proof syntax pretty-printer.
The proof pretty-printer converts proof abstract syntax into string.
-
stringOfSubst
fun stringOfSubst ott subst
-
converts a substitution into a string.
-
- Parameters:
-
-
ott
-
the ott flag indicates to display only subst terms individualy between [].
-
subst
-
the subtitution as (id, term) list.
- Returns:
-
the string representation of subst.
stringOfExistentialIntro
fun stringOfExistentialIntro tab subst (j, omega)
-
converts a substitution with an environment to a existential quantification introduction string list for ott.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
subst
-
the subtitution as (id, term) list.
-
j
-
the existential quantification identifier list.
-
omega
-
the formula
- Returns:
-
the string list representation of the existential introduction list.
stringOfNegExistElim
fun stringOfNegExistElim subst (j, omega)
-
converts a substitution with a type list to a negation existential quantification elimination string for ott.
-
- Parameters:
-
-
subst
-
the subtitution as (id, term) list.
-
j
-
the existential quantification identifier list.
-
omega
-
the formula
- Returns:
-
the string representation of the negation existential quantification elimination.
stringOfCommand_internal
fun stringOfCommand_internal tab form tex typ ott c
-
converts command into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
c
-
the command.
- Returns:
-
the string representation of the command.
stringOfSequence_internal
fun stringOfSequence_internal tab form tex typ ott s
-
converts sequence into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
s
-
the sequence.
- Returns:
-
the string representation of the sequence.
stringOfExpression_internal
fun stringOfExpression_internal tab form tex typ ott e
-
converts expression into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
e
-
the expression.
- Returns:
-
the string representation of the expression.
stringOfTypedExpression_internal
fun stringOfTypedExpression_internal tab form tex typ ott e
-
converts a pair expression * type into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
e
-
the expression.
- Returns:
-
the string representation of the expression.
stringOfExpressionList
fun stringOfExpressionList tab form tex typ ott exp_list
-
converts a list of expression into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
exp_list
-
the expression list.
- Returns:
-
the string representation of the expression list.
stringOfTypedExpressionList
fun stringOfTypedExpressionList tab form tex typ ott exp_list
-
converts a list of typed expression into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
exp_list
-
the typed expression list.
- Returns:
-
the string representation of the typed expression list.
stringOfValue_internal
fun stringOfValue_internal tab form tex typ ott v
-
converts value into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
tab
-
the tabulation level.
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
typ
-
flag indicating whether types have to be displayed.
-
ott
-
flag indicating whether the output must respect ott/twelf specific syntax.
-
v
-
the value.
- Returns:
-
the string representation of the value.
stringOfProgram
fun stringOfProgram form tex p : bool -> bool -> ProofAst.program -> string list
-
converts program into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
form
-
the formula-display (instead of imperative types) flag.
-
tex
-
the tex flag.
-
p
-
the program.
- Returns:
-
the string representation of p.
stringOfProgram_Ott
fun stringOfProgram_Ott p : ProofAst.program -> string list
-
converts program into string, generating ott-oriented type and syntax.
-
- Parameters:
-
-
p
-
the program.
- Returns:
-
the string representation of p.
stringOfProgram_Untyped
fun stringOfProgram_Untyped form tex p
: bool -> bool -> ProofAst.program -> string list
-
converts program into string accordingly to the formula/tex demand,
without any type information.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
p
-
the program.
- Returns:
-
the string representation of p.