Module `Signature.Data_Signature`Source

This module signature describes the interface for modules implementing signatures

Exceptions raised when definitions of types or constants are duplicated

Sourceexception Duplicate_type_definition

Sourceexception Duplicate_term_definition

Exception raised when no entry associated to a given symbol exists in a signature

Sourceexception Not_found

Sourcetype t

The type of the signature as abstract object

Sourcetype id

The type of signature ids, in order to distinguish them beyond their name

Sourcetype entry

The type of the entries of the signature

Sourcetype term = Logic.Lambda.Lambda.term

The (ocaml) type for the terms of the signature

Sourcetype stype = Logic.Lambda.Lambda.stype

The (ocaml) type for the types of the signature

Sourcetype data =

| Type of stype
| Term of term * stype
(*
the type for data that can be added to a signature
*)

Source

val empty : 
  filename:string ->
  (string * Logic.Abstract_syntax.Abstract_syntax.location) ->
  t

empty name returns the empty signature of name name

Sourceval name : t -> string * Logic.Abstract_syntax.Abstract_syntax.location

name s returns the name of the signature s and the location of its definition

Sourceval full_name : t -> (string * id) * string

full_name sg returns (n, id, filename) where n is the name of the signature, id its id, and filename the name of the file in which the signature sg was defined.

Sourceval add_entry : Logic.Abstract_syntax.Abstract_syntax.sig_entry -> t -> t

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

Sourceval find_term : string -> t -> term * stype

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

Sourceval is_type : ?atomic:bool -> string -> t -> bool

is_type ~atomic id s returns true if id is the name of a declared atomic or if s is a defined type and atomic is set to false (default), and false oterwise

Source

val is_constant : 
  string ->
  t ->
  bool
  * (Logic.Abstract_syntax.Abstract_syntax.syntactic_behavior * bool * bool)
      option

is_constant id s returns (true,Some ((b, pred), is_macro, has_atomic_type)) together with its syntactic behaviour b, its precedence pred, is_macro set to true if the constant is a defined one (a macro), false otherwise, has_atomic_type is set to true if its (expanded) type is atomic, false otherwise, 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.

Sourceval new_precedence : ?before:string -> string -> t -> float * t

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.

Sourceval pp_type : t -> Format.formatter -> stype -> unit

pp_type sg fmt ty pretty prints the type ty according to the signature sg on the formatter fmt.

Sourceval pp_term : t -> Format.formatter -> term -> unit

pp_type sg fmt t pretty prints the term t according to the signature sg on the formatter fmt.

Source

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.

Sourceval unfold_type_definition : int -> t -> Logic.Lambda.Lambda.stype

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

Sourceval unfold_term_definition : int -> t -> Logic.Lambda.Lambda.term

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

Sourceval expand_type : Logic.Lambda.Lambda.stype -> t -> Logic.Lambda.Lambda.stype

expand_type t sg returns a type where all the type definitions have been expanded

Sourceval expand_term : Logic.Lambda.Lambda.term -> t -> Logic.Lambda.Lambda.term

expand_term t sg returns a term where all the term definitions have been expanded

Sourceval pp : Format.formatter -> t -> unit

pp fmt sg pretty prints the signature sg on the formatter fmt. Should be parsable

Source

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

Sourceval convert_type : Logic.Abstract_syntax.Abstract_syntax.type_def -> t -> stype

convert_type ty sg returns a type to the parsed type ty wrt to the signature sg

Sourceval type_of_constant : string -> t -> stype

type_of_constant n sg returns the type of the constant of name n as defined in the signature sg

Source

val typecheck : 
  Logic.Abstract_syntax.Abstract_syntax.term ->
  stype ->
  t ->
  term * bool

typecheck t ty sg returns a pair (t', is_almost_linear) term if, according to sg, it has type ty. is_almost_linear is true if t' is almost linear, false otherwise.

Sourceval fold : (entry -> 'a -> 'a) -> 'a -> t -> 'a

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.

Sourceval entry_to_data : entry -> data

entry_to_data e returns a data depending of the content of the entry e in the signature sig

Source

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)

Sourceval is_declared : entry -> t -> string option

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

Sourceval eta_long_form : term -> stype -> t -> term

eta_long_form t ty sg returns the eta-long form of t with respect to the type ty and signature sg

Sourceval unfold : term -> t -> term

unfold t sg returns a normalized term where all the defined subterms of t have been expanded according to their definition in sg.

Sourceval is_2nd_order : t -> bool

is_2nd_order s returns true if the signature s is 2nd order and false otherwise.

Sourceval is_atomic : stype -> t -> bool

is_atomic t sig returne true if the type t is atomic accorging to sig.

Source

val gen_term_list : 
  t ->
  stype ->
  int ->
  int ->
  bool ->
  term UtilsLib.LazyList.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/acgtk.acgData/AcgData/Signature/Data_Signature/index.html

Module `Signature.Data_Signature`Source

package acgtk

Install

Dune Dependency

Authors

Maintainers

Sources

doc/acgtk.acgData/AcgData/Signature/Data_Signature/index.html

Module Signature.Data_SignatureSource

Module `Signature.Data_Signature`Source