Overview  Index  Help 

BASE_PRETTY_PRINTER

All Known Implementing Modules:

BasePrettyPrinterProofPrettyPrinterProofCheckerFunPrettyPrinter


The First-Order LoopW Proof Checker base pretty-printer. The base pretty-printer converts terms, formulas, and ident abstract syntax into string.

           
Value summary

val stringOfIdent : ProofAst.ident -> string
           converts identifiers into string.

val stringOfIdentList : ProofAst.ident list -> string
           converts identifier lists into string.

val stringOfParamList
    : bool ->
        bool ->
          bool ->
            ProofAst.ident list ->
              string -> (ProofAst.ident * ProofAst.formula) list -> string

           converts parameter list into string accordingly to the formula/tex demand.

val stringOfQuantifiedTypedIdentList
    : bool ->
        bool ->
          bool ->
            ProofAst.ident list ->
              (ProofAst.ident * ProofAst.formula) list -> string

           converts quantified typed identifier lists into string.

val stringOfQuantifiedTypeList
    : bool ->
        bool -> bool -> ProofAst.ident list -> ProofAst.formula list -> string

           converts quantified type list into string.

val stringOfTab : int -> string
           builds a string with spaces for tabular display.

val stringOfTerm : bool -> ProofAst.term -> string
           converts terms abstract syntax into string.

val stringOfType : bool -> bool -> bool -> ProofAst.formula -> string
           converts formulas/types abstract syntax into string accordingly to the formula/tex demand.

val stringOfTypedIdent
    : bool -> bool -> bool -> ProofAst.ident * ProofAst.formula -> string

           converts typed identifiers into string.

val stringOfTypedIdentList
    : bool -> bool -> bool -> (ProofAst.ident * ProofAst.formula) list -> string

           converts typed identifier lists into string.

 

       
Value detail

stringOfTab

fun stringOfTab n : int -> string

builds a string with spaces for tabular display.

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

stringOfTerm

fun stringOfTerm ott t : bool -> ProofAst.term -> string

converts terms abstract syntax into string.

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

stringOfType

fun stringOfType form tex ott 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 ott 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-display (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.

stringOfIdent

fun stringOfIdent i : ProofAst.ident -> string

converts identifiers into string.

Parameters:
i
the identifier.
Returns:
the string representation of i.

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.

stringOfIdentList

fun stringOfIdentList il : ProofAst.ident list -> string

converts identifier lists into string.

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

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-display (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-display (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-display (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.

 


Overview  Index  Help