package acgtk
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2743321ae4cc97400856eb503a876cbcbd08435ebc750276399a97481d001d41
md5=04c1e14f98e2c8fd966ef7ef30b38323
doc/acgtkLib.acgData/AcgData/Signature/Data_Signature/index.html
Module Signature.Data_Signature
Source
Exceptions raised when definitions of types or constants are duplicated
Exception raised when no entry associated to a given symbol exists in a signature
The type of the signature as abstract object
The type of the entries of the signature
The (ocaml) type for the terms of the signature
The (ocaml) type for the types of the signature
empty name
returns the empty signature of name name
name s
returns the name of the signature s
and the location of its definition
add_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
is_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 option
is_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 * string
id_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.
unfold_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
unfold_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
expand_type t sg
returns a type where all the type definitions have been expanded
expand_term t sg
returns a term where all the term definitions have been expanded
add_warnings w s
resturns a signature where the warning w
have been added
get_warnings sg
returns the warnigs emitted while parsing sg
.
to_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 * stype
convert_term t ty sg
returns a the term corresponding to the parsed term t
with parsed type ty
wrt to the signature sg
convert_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
typecheck 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 option
get_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