Module Coding

module Coding: sig .. end

Contains the type of typed terms, functions calculating type and reconstruction for a term, and printing and parsing for terms.

Coding basic things as Terms and decoding them

val check_tp : string -> Term.term -> bool

Check whether the term belongs to the given class.

exception DECODE of string

Thrown when decoding fails.

exception TOPLEVEL_ERROR of string * Term.term option

val code_list : Term.term array -> ('a -> Term.term) -> 'a list -> Term.term

val decode_list : normalized:bool -> (Term.term -> 'a) -> Term.term -> 'a list

val decode_list_opt : (Term.term -> 'a) -> Term.term -> 'a list option

val code_hlist : ('a -> Term.term) -> 'a list -> Term.term

val decode_hlist : normalized:bool -> (Term.term -> 'a) -> Term.term -> 'a list

val decode_hlist_opt : (Term.term -> 'a) -> Term.term -> 'a list option

val int_to_bits : int -> int list

val bits_to_int : int list -> int

val code_bit : int -> Term.term

val decode_bit : normalized:bool -> Term.term -> int

val decode_bit_list : normalized:bool -> Term.term -> int

val code_char : char -> Term.term

val decode_char : normalized:bool -> Term.term -> char

val code_string : ?value_prefix:bool -> string -> Term.term

val decode_string : normalized:bool -> Term.term -> string

val decode_string_opt : Term.term -> string option

val code_bool : bool -> Term.term

val decode_bool : normalized:bool -> Term.term -> bool

val code_term : Term.term -> Term.term

val code_term_incr_vars : Term.term -> Term.term

val decode_term : normalized:bool -> Term.term -> Term.term

val unpack_te : Term.term -> Term.term

Remove parse level information from the head of the term.

Rewriting rules and definitions, their coding and decoding

type rewrite_rule = bool * Term.term * Term.term

The type of Rewriting Rules.

val code_rewrite_rule : rewrite_rule -> Term.term

val decode_rewrite_rule : normalized:bool -> Term.term -> rewrite_rule

val code_input_rewrite_rule : rewrite_rule -> Term.term

val decode_input_rewrite_rule : normalized:bool -> Term.term -> rewrite_rule

val code_priority_input_rewrite_rule : rewrite_rule -> Term.term

val decode_priority_input_rewrite_rule : normalized:bool -> Term.term -> rewrite_rule

type fun_definition = string * Term.term list * Term.term

The type of Function Definitions.

val code_fun_definition : fun_definition -> Term.term

val decode_fun_definition : normalized:bool -> Term.term -> fun_definition

val decode_syntax_element : normalized:bool -> Term.term -> SyntaxDef.syntax_elem

val code_syntax_element_list : SyntaxDef.syntax_elem list -> Term.term

val decode_syntax_element_list : normalized:bool -> Term.term -> SyntaxDef.syntax_elem list

val code_syntax_definition : SyntaxDef.syntax_def -> Term.term

val decode_syntax_definition : normalized:bool -> Term.term -> SyntaxDef.syntax_def

val func_sd_of_sd : SyntaxDef.syntax_def -> SyntaxDef.syntax_def option

Term Matching

val matches : (string * Term.term) list Pervasives.ref -> Term.term * Term.term -> bool

Application of term substitutions (only flat functional substitutes).

val apply_s : (string * Term.term) list -> Term.term -> Term.term

Term Display, printing and parsing

val display_term : ?sdefs:(string * SyntaxDef.syntax_def) list ->
       ?full:[ `Full | `HeadType | `NoSupercl | `NoTypes ] -> Term.term -> string

val display_super : (string * SyntaxDef.syntax_def) list option ->
       [ `Full | `HeadType | `NoSupercl | `NoTypes ] -> Term.term array -> string

val display_term_bracketed : Term.term -> string

val display_shortly_bracketed : Term.term -> string

val display_hterm : ?types:bool ->
       ?bracketed:bool ->
       ?sdefs:(string * SyntaxDef.syntax_def) list ->
       Term.decls_set -> Term.term -> string

Convert a term to string concisely using the Greatest Lower Bound notation. With the default types=false, does not display substitutions of type variables. With bracketed=true (default is false), curly braces are added around each argument of a term.

val display_term_xml : Term.term -> string

val term_to_string : Term.term -> string

val parse_term : Aux.split_result list -> Term.term * Aux.split_result list

val term_of_string : string -> Term.term

val short_term : Term.term -> string

A concise, without supertypes, readable but not parseable form.

val split_sdef_name : string -> string option list

val pretty_print_sd : SyntaxDef.syntax_def -> string

Rewriting Rules for special built-in functions

val brackets_rules : (bool * Term.term * Term.term) list

val verbatim_rules : (bool * Term.term * Term.term) list

val if_then_else_rules : (bool * Term.term * Term.term) list

val additional_xslt_rules : (bool * Term.term * Term.term) list

val string_quote_rules : (bool * Term.term * Term.term) list