Overview  Index  Help 

ProofDerivPrettyPrinter


The First-Order LoopW Type Inference proof derivation pretty-printer. The proof derivation pretty-printer converts proof abstract syntax into string containing both program and typing derivation.

Opened structures

PrettyPrinterKeywords

BasePrettyPrinter

ProofAst

CoreAstUtils

               
Value summary

val append_with_lemma
           appends a lemma number reference to a string list representing a program.

val complete
           completes to string list in order to have the same list size.

val init
          Lemma counter

val lemma_fusion
           concatenates two string; if they represent a lemma number reference, it glues them together.

val make_spc
           builds a string containing the given number of white spaces.

val max_width
           calculates the longest string in a string list.

val next
          Lemma counter

val stringOfCommand
           converts command typing derivation into string accordingly to the formula/tex demand.

val stringOfExpression
           converts expression typing derivation into string accordingly to the formula/tex demand.

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

val stringOfSequence
           converts sequence typing derivation into string accordingly to the formula/tex demand.

val stringOfTab_T
           builds a string with | and spaces for typing tabular display.

val stringOfTyping
    : bool -> bool -> string list -> ProofAst.program -> string list

           converts program with typing derivation into string accordingly to the formula/tex demand.

val stringOfValue
           converts value typing derivation into string accordingly to the formula/tex demand.

val tabulate
           appends at the end of each string of a string list an amount of white spaces in order to have exactly string of the same given size.

 

       
Value detail

init

val init

Lemma counter


next

val next

Lemma counter


stringOfTab_T

fun stringOfTab_T n

builds a string with | and spaces for typing tabular display.

Parameters:
tex
the tex flag.
n
the number of tabs.
Returns:
the string tab.

append_with_lemma

fun append_with_lemma tab l s

appends a lemma number reference to a string list representing a program. If the program string list is empty, it returns a new line ; else it appends the lemma number reference to the last line.

Parameters:
tab
the number of tabs.
l
the string list representing the program.
s
the string representation of the lemma number.
Returns:
the string representation of the program with lemma reference.

lemma_fusion

fun lemma_fusion s1 s2

concatenates two string; if they represent a lemma number reference, it glues them together.

Parameters:
s1
the first string.
s2
the second string.
Returns:
the concatenation of s1 and s2.

stringOfCommand

fun stringOfCommand tab form tex c

converts command typing derivation 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.
c
the command.
Returns:
the string representation of the command typing derivation.

stringOfSequence

fun stringOfSequence tab form tex s

converts sequence typing derivation 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.
s
the sequence.
Returns:
the string representation of the sequence typing derivation.

stringOfExpression

fun stringOfExpression tab form tex e

converts expression typing derivation 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.
e
the expression.
Returns:
the string representation of the expression typing derivation.

stringOfExpressionList

fun stringOfExpressionList tab form tex el

converts expression list 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.
el
the expression list.
Returns:
the string representation of the expression list typing derivation.

stringOfValue

fun stringOfValue tab form tex v

converts value typing derivation 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.
v
the value.
Returns:
the string representation of the value typing derivation.

max_width

fun max_width sl

calculates the longest string in a string list.

Parameters:
sl
the string list.
Returns:
the size of the longest string in sl.

make_spc

fun make_spc n

builds a string containing the given number of white spaces.

Parameters:
n
the number of white spaces.
Returns:
the string with n spaces.

tabulate

fun tabulate max

appends at the end of each string of a string list an amount of white spaces in order to have exactly string of the same given size.

Parameters:
max
the size each string of sl must be.
sl
the string list.
Returns:
sl with each string augmented to size max.

complete

fun complete (l1, l2)

completes to string list in order to have the same list size.

Parameters:
l1
the first string list.
l2
the second string list.
Returns:
the pair of lists having with the shortest one completed with empty strings.

stringOfTyping

fun stringOfTyping form tex p
    : bool -> bool -> string list -> ProofAst.program -> string list

converts program with typing derivation into string accordingly to the formula/tex demand.

Parameters:
form
the formula-display (instead of imperative types) flag.
tex
the tex flag.
pr
the string representation of the untyped program.
p
the program.
Returns:
the string representation of p along with its partial typing derivation.

 


Overview  Index  Help