FunPrettyPrinter
-
The First-Order LoopW Proof Checker functional pretty-printer.
The functional pretty-printer converts functional terms into string.
-
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.