BasePrettyPrinter
-
The First-Order LoopW Type Inference base pretty-printer.
The base pretty-printer converts terms, formulas, and ident abstract syntax into string.
-
stringOfTab
fun stringOfTab n : int -> string
-
builds a string with spaces for tabular display.
-
- Parameters:
-
-
n
-
the number of tabs.
- Returns:
-
the string tab.
stringOfIdent
fun stringOfIdent i : CoreAst.ident -> string
-
converts identifiers into string.
-
- Parameters:
-
-
i
-
the identifier.
- Returns:
-
the string representation of i.
stringOfIdentList
fun stringOfIdentList il : ProofAst.ident list -> string
-
converts identifier lists into string.
-
- Parameters:
-
-
il
-
the identifier list.
- Returns:
-
the string representation of il.
getNat
fun getNat t
-
converts a term into an integer if it is an unary natural number into an integer, returning NONE if not.
-
- Parameters:
-
-
t
-
the term.
- Returns:
-
an integer Option.
stringOfTerm
fun stringOfTerm t : bool -> ProofAst.term -> string
-
converts terms abstract syntax into string.
-
- Parameters:
-
-
t
-
the term.
- Returns:
-
the string representation of t.
stringOfProcType
fun stringOfProcType form tex ott idlist1 typlist1 idlist2 typlist2
-
converts procedural type into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the ott flag.
-
idlist1
-
the identifier list of universal quantification.
-
typlist1
-
the formula list on the left hand side of the implication.
-
idlist2
-
the identifier list of existential quantification.
-
typlist2
-
the formula list on the right hand side of the implication.
- Returns:
-
the string representation of the procedural type.
stringOfNegType
fun stringOfNegType form tex ott idlist typlist
-
converts negation type into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the tex flag.
-
idlist
-
the identifier list of universal quantification.
-
typlist
-
the formula list.
- Returns:
-
the string representation of the negation type.
stringOfType
fun stringOfType form tex f : bool -> bool -> bool -> ProofAst.formula -> string
-
converts formulas/types abstract syntax into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the tex flag.
-
f
-
the formula.
- Returns:
-
the string representation of f.
stringOfQuantifiedTypeList
fun stringOfQuantifiedTypeList form tex ott i il
: bool ->
bool -> bool -> ProofAst.ident list -> ProofAst.formula list -> string
-
converts quantified type list into string.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the tex flag.
-
i
-
the quantifier identifier list.
-
il
-
the type list.
- Returns:
-
the string representation of i il.
stringOfTypedIdent
fun stringOfTypedIdent form tex ott i
: bool -> bool -> bool -> ProofAst.ident * ProofAst.formula -> string
-
converts typed identifiers into string.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the tex flag.
-
i
-
the identifier.
- Returns:
-
the string representation of i.
stringOfTypedIdentList
fun stringOfTypedIdentList form tex ott il
: bool -> bool -> bool -> (ProofAst.ident * ProofAst.formula) list -> string
-
converts typed identifier lists into string.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the tex flag.
-
il
-
the typed identifier list.
- Returns:
-
the string representation of il.
stringOfQuantifiedTypedIdentList
fun stringOfQuantifiedTypedIdentList form tex ott i il
: bool ->
bool ->
bool ->
ProofAst.ident list ->
(ProofAst.ident * ProofAst.formula) list -> string
-
converts quantified typed identifier lists into string.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
ott
-
the tex flag.
-
i
-
the quantifier identifier list.
-
il
-
the typed identifier list.
- Returns:
-
the string representation of i il.
stringOfParamList
fun stringOfParamList form tex displayType idlist mode typidlist
: bool ->
bool ->
bool ->
ProofAst.ident list ->
string -> (ProofAst.ident * ProofAst.formula) list -> string
-
converts parameter list into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
displayType
-
flag indicating whether types have to be displayed.
-
idlist
-
the identifier/quantification list.
-
mode
-
the mode in or out.
-
typidlist
-
the typed identifier list of formal parameters.
- Returns:
-
the string representation of the parameter list.