Overview  Index  Help 

ProofPrettyPrinter


The First-Order LoopW Type Inference proof syntax pretty-printer. The proof pretty-printer converts proof abstract syntax into string.

Opened structures

PrettyPrinterKeywords

BasePrettyPrinter

ProofAst

               
Value summary

val stringOfCommand_internal
           converts command into string accordingly to the formula/tex demand.

val stringOfExistentialIntro
           converts a substitution with an environment to a existential quantification introduction string list for ott.

val stringOfExpressionList
           converts a list of expression into string accordingly to the formula/tex demand.

val stringOfExpression_internal
           converts expression into string accordingly to the formula/tex demand.

val stringOfNegExistElim
           converts a substitution with a type list to a negation existential quantification elimination string for ott.

val stringOfProgram : bool -> bool -> ProofAst.program -> string list
           converts program into string accordingly to the formula/tex demand.

val stringOfProgram_Ott : ProofAst.program -> string list
           converts program into string, generating ott-oriented type and syntax.

val stringOfProgram_Untyped : bool -> bool -> ProofAst.program -> string list
           converts program into string accordingly to the formula/tex demand, without any type information.

val stringOfSequence_internal
           converts sequence into string accordingly to the formula/tex demand.

val stringOfSubst
           converts a substitution into a string.

val stringOfTypedExpressionList
           converts a list of typed expression into string accordingly to the formula/tex demand.

val stringOfTypedExpression_internal
           converts a pair expression * type into string accordingly to the formula/tex demand.

val stringOfValue_internal
           converts value into string accordingly to the formula/tex demand.

 

       
Value detail

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.

 


Overview  Index  Help