Overview  Index  Help 

BasePrettyPrinter


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

Opened structures

PrettyPrinterKeywords

ProofAst

               
Value summary

val getNat
           converts a term into an integer if it is an unary natural number into an integer, returning NONE if not.

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

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

val stringOfNegType
           converts negation type into string accordingly to the formula/tex demand.

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 stringOfProcType
           converts procedural type 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.

stringOfIdent

fun stringOfIdent i : ProofAst.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.

 


Overview  Index  Help