It contains a module that allows for manipulating the associated signatures
Exceptions raised when definitions of types or constants are duplicated
Exception raised when no entry associated to a given symbol exists in a signature
type term = Logic.Lambda.Lambda.termThe (ocaml) type for the terms of the signature
type stype = Logic.Lambda.Lambda.stypeThe (ocaml) type for the types of the signature
val empty : (string * Logic.Abstract_syntax.Abstract_syntax.location) -> tempty name returns the empty signature of name name
val name : t -> string * Logic.Abstract_syntax.Abstract_syntax.locationname s returns the name of the signature s and the location of its definition
val add_entry : Logic.Abstract_syntax.Abstract_syntax.sig_entry -> t -> tadd_entry e s returns a signature where the entry e has been added
find_type id s returns the type as declared or defined in the signature s, corresponding to the symbol id in s if it exists. Raise Not_found otherwise
find_term id s returns the term together with its type, as declared or defined in the signature s, corresponding to the symbol id in s if it exists. Raise Not_found otherwise
val is_type : string -> t -> boolis_atomic_type id s returns true if id is the name of an atomic type in s and false oterwise
val is_constant :
string ->
t ->
bool * Logic.Abstract_syntax.Abstract_syntax.syntactic_behavior optionis_constant id s returns (true,Some (b,pred)) together with its syntactic behaviour b and its precedence pred if id is the name of a constant in s and false,None oterwise
precedence id s returns a Some f where f is float indicating the precedence of the infix operator id. It returns None if id is not an infix operator.
new_precedence ?before id s returns a pair consisting of a new precedence value associated to id, and the new signature taking this new value into account. If the optional string argument before is not provided, then id is given the highest precedence so far. Otherwise, it is given the precedence just below before.
type_to_string ty sg returns the string corresponding to a type ty of type Logic.Lambda.Lambda.stype) with respect to the signature sg
term_to_string t sg returns the string corresponding to a term t of type Logic.Lambda.Lambda.term) with respect to the signature sg
val id_to_string :
t ->
int ->
Logic.Abstract_syntax.Abstract_syntax.syntactic_behavior * stringid_to_string sg id looks up a constant defined or declared in a signature by its id and returns a pair of its syntactic behavior and name.
val unfold_type_definition : int -> t -> Logic.Lambda.Lambda.stypeunfold_type_definition id t returns the actual type for the type defined by id as the identifier of a type definition in the signature t. Fails with "Bug" if id does not correspond to a type definition
val unfold_term_definition : int -> t -> Logic.Lambda.Lambda.termunfold_term_definition id t returns the actual term for the term defined by id as the identifier of a term definition in the signature t. Fails with "Bug" if id does not correspond to a term definition
val expand_type : Logic.Lambda.Lambda.stype -> t -> Logic.Lambda.Lambda.stypeexpand_type t sg returns a type where all the type definitions have been expanded
val expand_term : Logic.Lambda.Lambda.term -> t -> Logic.Lambda.Lambda.termexpand_term t sg returns a term where all the term definitions have been expanded
val add_warnings : Error.warning list -> t -> tadd_warnings w s resturns a signature where the warning w have been added
get_warnings sg returns the warnigs emitted while parsing sg.
val to_string : t -> stringto_string sg returns a string describing the signature sg. Should be parsable
term_to_string t sg returns a string describing the term t wrt the signature sg.
type_to_string t sg returns a string describing the term t wrt the signature sg.
val convert_term :
Logic.Abstract_syntax.Abstract_syntax.term ->
Logic.Abstract_syntax.Abstract_syntax.type_def ->
t ->
term * stypeconvert_term t ty sg returns a the term corresponding to the parsed term t with parsed type ty wrt to the signature sg
val convert_type : Logic.Abstract_syntax.Abstract_syntax.type_def -> t -> stypeconvert_type ty sg returns a type to the parsed type ty wrt to the signature sg
type_of_constant n sg returns the type of the constant of name n as defined in the signature sg
val typecheck :
Logic.Abstract_syntax.Abstract_syntax.term ->
stype ->
t ->
termtypecheck t ty sg returns a term if, according to sg, it has type ty
fold f a sg returns f e_n (f e_n-1 ( ... ( f e_1 a) ... )) where the e_i are the entries of the signature sg. It is ensured that the e_i are provided in the same order as they have been inserted.
entry_to_data e returns a data depending of the content of the entry e in the signature sig
val get_binder_argument_functional_type :
string ->
t ->
Logic.Abstract_syntax.Abstract_syntax.abstraction optionget_binder_argument_functionnal_type s sg returns None if the constant s is not defined in sg as a binder (that is something of type ('a ?> 'b) ?> 'c ) and returns Some abs where abs is Logic.Abstract_syntax.Abstract_syntax.abstraction.Linear or Logic.Abstract_syntax.Abstract_syntax.abstraction.Non_linear otherwise and abs desribes the implication ?> in ('a ?> 'b)
is_declared e sg returns Some s if the entry e is a declaration of the string s (and not a definiton) in sg and None otherwise
eta_long_form t ty sg returns the eta-long form of t with respect to the type ty and signature sg
val is_2nd_order : t -> boolis_2nd_order s returns true if the signature s is 2nd order and false otherwise.