Overview  Index  Help 

FunPrettyPrinter


The First-Order LoopW Proof Checker functional pretty-printer. The functional pretty-printer converts functional terms into string.

Opened structures

FunAst

PrettyPrinterKeywords

BasePrettyPrinter

               
Value summary

val append_last
           appends a string at the end of the last string of a string list.

val init

val next

val stringOfEnv : (FunAst.ident * FunAst.expType) list -> string
           builds a string representation of a typing environment.

val stringOfTerm : FunAst.typed_term -> string list
           builds a string representation of a term.

val stringOfTerm_compact
           builds a compact string representation of a term.

val stringOfTerm_expanded
           builds a expanded string representation of a term.

val stringOfType : FunAst.expType -> string
           converts formulas/types abstract syntax into string.

val stringOfTypedIdent
           converts typed identifiers into string.

val stringOfTypedIdentList
           converts typed identifier lists into string.

 

       
Value detail

append_last

fun append_last l s

appends a string at the end of the last string of a string list.

Parameters:
l
the string list [s1, ..., sn].
s
the string to append.
Returns:
[s1, ..., sn ^ s] (or [] if l = []).

stringOfType

fun stringOfType t : FunAst.expType -> string

converts formulas/types abstract syntax into string.

Parameters:
t
the type.
Returns:
the string representation of t.

stringOfTypedIdent

fun stringOfTypedIdent (id, t)

converts typed identifiers into string.

Parameters:
id
the identifier.
t
the type.
Returns:
the string representation of (id, t).

stringOfTypedIdentList

fun stringOfTypedIdentList il

converts typed identifier lists into string.

Parameters:
il
the typed identifier list.
Returns:
the string representation of il.

stringOfEnv

fun stringOfEnv env : (FunAst.ident * FunAst.expType) list -> string

builds a string representation of a typing environment.

Parameters:
env
the environment.
Returns:
the string representation of env.

init

val init


next

val next


stringOfTerm_compact

fun stringOfTerm_compact t

builds a compact string representation of a term.

Parameters:
t
the term.
Returns:
the string representation of proof obligations and the compact string representation of t.

stringOfTerm_expanded

fun stringOfTerm_expanded t

builds a expanded string representation of a term.

Parameters:
t
the term.
Returns:
the string representation of proof obligations and the expanded string representation of t.

stringOfTerm

fun stringOfTerm t : FunAst.typed_term -> string list

builds a string representation of a term.

Parameters:
t
the term.
Returns:
the string representation of t.

 


Overview  Index  Help