module Hornpp: sig end
Pretty printing of specifications in abstract syntax (multi-process)
prefixes of identifiers:
c_ constant symbolr_ reserved function symbol (including type coercion)t_ type (predicate)v_ valueP_ parameterV_ private variableQ_ quantified variable
Separators for pp_list.
val comma_sep : unit -> unit
standard comma separation to use for pp_list
val semicol_sep : unit -> unit
standard semicolumn separation to use for pp_list
val null_sep : unit -> unit
standard null separation to use for pp_list
val newline_sep : unit -> unit
standard new line separation to use for pp_list
val newline2_sep : unit -> unit
double new line separation to use for pp_list
Pretty printing functions for clauses aand clauses components.
val hornpp_id : Symbols.eva_symbol_list -> Abstract.eva_id -> unit
hornpp_id sl i
prints the given identifier i
using the given symbol list sl.
see above for the prefixes of identifiers.
val hornpp_lid : Symbols.eva_symbol_list -> Abstract.eva_lid -> unit
hornpp_lid sl i
prints the given located identifier i
using the given symbol list sl.
see above for the prefixes of identifiers.
val hornpp_label : Abstract.eva_label -> unit
hornpp_label l
prints the given label l.
val hornpp_llabel : Abstract.eva_llabel -> unit
hornpp_label l
prints the given located label l.
val hornpp_type : Abstract.eva_type -> unit
hornpp_type t
prints the given type t.
val hornpp_ltype : Abstract.eva_ltype -> unit
hornpp_ltype t
prints the given located type t.
val hornpp_scope : Abstract.eva_scope -> unit
hornpp_scope s
prints the given scope s.
val hornpp_lscope : Abstract.eva_lscope -> unit
hornpp_lscope s
prints the given located scope s.
val hornpp_value : Abstract.eva_value -> unit
hornpp_value v
prints the given value v.
val hornpp_lvalue : Abstract.eva_lvalue -> unit
hornpp_lvalue v
prints the given located value v.
val hornpp_term : Symbols.eva_symbol_list -> Abstract.eva_term -> unit
hornpp_term sl t
prints the given term t
using the given symbol list sl.
val hornpp_lterm : Symbols.eva_symbol_list -> Abstract.eva_lterm -> unit
hornpp_lterm sl t
prints the given located term t
using the given symbol list sl.
val hornpp_literal : string -> Symbols.eva_symbol_list -> Clause.literal -> unit
hornpp_literal sign sl l
prints the given literal l
preceeded by the given string sign
and using the given symbol list sl.
val hornpp_tclause : Symbols.eva_symbol_list -> Clause.tclause -> unit
hornpp_tclause sl c
print the given tclause c
using the given symbol list sl.
val hornpp_clause : Symbols.eva_symbol_list -> Clause.clause -> unit
hornpp_clause sl c
print the given clause c
using the given symbol list sl.
pretty print the given specification
as a set of Horn clauses.