Commit 236d3d36 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean API documentation a bit.

parent 606f0860
......@@ -74,13 +74,13 @@ type ind_sign = Ind | Coind
type ind_list = ind_sign * ind_decl list
(* Proposition declaration *)
(** {2 Proposition declaration} *)
type prop_kind =
| Plemma (* prove, use as a premise *)
| Paxiom (* do not prove, use as a premise *)
| Pgoal (* prove, do not use as a premise *)
| Pskip (* do not prove, do not use as a premise *)
| Plemma (** prove, use as a premise *)
| Paxiom (** do not prove, use as a premise *)
| Pgoal (** prove, do not use as a premise *)
| Pskip (** do not prove, do not use as a premise *)
type prop_decl = prop_kind * prsymbol * term
......@@ -88,18 +88,18 @@ type prop_decl = prop_kind * prsymbol * term
type decl = private {
d_node : decl_node;
d_syms : Sid.t; (* idents used in declaration *)
d_news : Sid.t; (* idents introduced in declaration *)
d_tag : Weakhtbl.tag; (* unique magical tag *)
d_syms : Sid.t; (** idents used in declaration *)
d_news : Sid.t; (** idents introduced in declaration *)
d_tag : Weakhtbl.tag; (** unique magical tag *)
}
and decl_node = private
| Dtype of tysymbol (* abstract types and aliases *)
| Ddata of data_decl list (* recursive algebraic types *)
| Dparam of lsymbol (* abstract functions and predicates *)
| Dlogic of logic_decl list (* recursive functions and predicates *)
| Dind of ind_list (* (co)inductive predicates *)
| Dprop of prop_decl (* axiom / lemma / goal *)
| Dtype of tysymbol (** abstract types and aliases *)
| Ddata of data_decl list (** recursive algebraic types *)
| Dparam of lsymbol (** abstract functions and predicates *)
| Dlogic of logic_decl list (** recursive functions and predicates *)
| Dind of ind_list (** (co)inductive predicates *)
| Dprop of prop_decl (** axiom / lemma / goal *)
module Mdecl : Extmap.S with type key = decl
module Sdecl : Extset.S with module M = Mdecl
......@@ -118,7 +118,7 @@ val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_sign -> ind_decl list -> decl
val create_prop_decl : prop_kind -> prsymbol -> term -> decl
(* exceptions *)
(* {2 Exceptions} *)
exception IllegalTypeAlias of tysymbol
exception NonPositiveTypeDecl of tysymbol * lsymbol * ty
......@@ -177,7 +177,7 @@ val find_logic_definition : known_map -> lsymbol -> ls_defn option
val find_prop : known_map -> prsymbol -> term
val find_prop_decl : known_map -> prsymbol -> prop_kind * term
(** Records *)
(** {2 Records} *)
exception EmptyRecord
......
......@@ -32,7 +32,7 @@ val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_pr : namespace -> string list -> prsymbol
val ns_find_ns : namespace -> string list -> namespace
(** Meta properties *)
(** {2 Meta properties} *)
type meta_arg_type =
| MTty
......@@ -78,7 +78,7 @@ val register_meta_excl :
val lookup_meta : string -> meta
val list_metas : unit -> meta list
(** Theory *)
(** {2 Theories} *)
type theory = private {
th_name : ident; (* theory name *)
......@@ -114,9 +114,9 @@ module Htdecl : Exthtbl.S with type key = tdecl
val td_equal : tdecl -> tdecl -> bool
val td_hash : tdecl -> int
(** Constructors and utilities *)
(** {2 Constructors and utilities} *)
type theory_uc (* a theory under construction *)
type theory_uc (** a theory under construction *)
val create_theory : ?path:string list -> preid -> theory_uc
val close_theory : theory_uc -> theory
......@@ -129,13 +129,13 @@ val get_known : theory_uc -> known_map
val get_rev_decls : theory_uc -> tdecl list
val restore_path : ident -> string list * string * string list
(* [restore_path id] returns the triple (library path, theory,
(** [restore_path id] returns the triple (library path, theory,
qualified symbol name) if the ident was ever introduced in
a theory declaration. If the ident was declared in several
different theories, the first association is retained.
Raises Not_found if the ident was never declared in a theory. *)
(** Declaration constructors *)
(** {2 Declaration constructors} *)
val create_decl : decl -> tdecl
......@@ -148,12 +148,12 @@ val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
(** Use *)
(** {2 Use} *)
val create_use : theory -> tdecl
val use_export : theory_uc -> theory -> theory_uc
(** Clone *)
(** {2 Clone} *)
type th_inst = {
inst_ts : tysymbol Mts.t; (* old to new *)
......@@ -180,21 +180,21 @@ val create_null_clone : theory -> tdecl
val is_empty_sm : symbol_map -> bool
(** Meta *)
(** {2 Meta} *)
val create_meta : meta -> meta_arg list -> tdecl
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
val clone_meta : tdecl -> symbol_map -> tdecl
(* [clone_meta td_meta sm] produces from [td_meta]
* a new Meta tdecl instantiated with respect to [sm]]. *)
(** [clone_meta td_meta sm] produces from [td_meta]
a new Meta tdecl instantiated with respect to [sm]. *)
(*
val on_meta: meta-> ('a -> meta_arg list -> 'a) -> 'a -> theory -> 'a
*)
(** Base theories *)
(** {2 Base theories} *)
val builtin_theory : theory
......@@ -210,7 +210,7 @@ val tuple_theory_name : string -> int option
val add_decl_with_tuples : theory_uc -> decl -> theory_uc
(* exceptions *)
(* {2 Exceptions} *)
exception NonLocal of ident
exception CannotInstantiate of ident
......
......@@ -100,8 +100,7 @@ val set_simple_family : t -> string -> simple_family -> t
val get_int : ?default:int -> section -> string -> int
(** [get_int ~default section key] one key to one value
@raise Bad_value_type if the value associated to [key] is not of type
{!int}
@raise Bad_value_type if the value associated to [key] is not of type [int]
@raise Key_not_found if default is not given and no value is
associated to [key]
......@@ -114,8 +113,7 @@ val get_into : section -> string -> int option
val get_intl : ?default:int list -> section -> string -> int list
(** [get_intl ~default section key] one key to many value
@raise Bad_value_type if the value associated to [key] is not of
type {!int}
@raise Bad_value_type if the value associated to [key] is not of type [int]
@raise MissingField if default is not given and no values are
associated to [key]
......
......@@ -15,6 +15,8 @@ open Mlw_ty
open Mlw_ty.T
open Mlw_expr
(** *)
(** {2 Type declaration} *)
type constructor = plsymbol * plsymbol option list
......
......@@ -15,12 +15,14 @@ open Term
open Mlw_ty
open Mlw_ty.T
(** program/logic symbols *)
(** *)
(* plsymbols represent algebraic type constructors and projections.
(** {2 Program/logic symbols} *)
(** {!plsymbol}s represent algebraic type constructors and projections.
They must be fully applied and the result is equal to the application of
the lsymbol. We need this kind of symbols to cover nullary constructors,
such as Nil, which cannot be given a post-condition. They cannot be
such as [Nil], which cannot be given a post-condition. They cannot be
locally defined and therefore every type variable and region in their
type signature can be instantiated. *)
......@@ -45,12 +47,12 @@ val create_plsymbol :
preid -> field list -> field -> plsymbol
val restore_pl : lsymbol -> plsymbol
(* raises Not_found if the argument is not a pl_ls *)
(** raises [Not_found] if the argument is not a [pl_ls] *)
exception HiddenPLS of plsymbol
exception RdOnlyPLS of plsymbol
(** cloning *)
(** {2 Cloning} *)
type symbol_map = private {
sm_pure : Theory.symbol_map;
......@@ -60,7 +62,7 @@ type symbol_map = private {
val pl_clone : Theory.symbol_map -> symbol_map
(** patterns *)
(** {2 Patterns} *)
type ppattern = private {
ppat_pattern : pattern;
......@@ -79,9 +81,9 @@ type pre_ppattern =
val make_ppattern :
pre_ppattern -> ?ghost:bool -> ity -> pvsymbol Mstr.t * ppattern
(** program symbols *)
(** {2 Program symbols} *)
(* psymbols represent lambda-abstractions. They are polymorphic and
(** {!psymbol}s represent lambda-abstractions. They are polymorphic and
can be type-instantiated in some type variables and regions of
their type signature. *)
......@@ -91,12 +93,12 @@ type psymbol = private {
ps_ghost : bool;
ps_pvset : Spv.t;
ps_vars : varset;
(* this varset covers the type variables and regions of the defining
(** this varset covers the type variables and regions of the defining
lambda that cannot be instantiated. Every other type variable
and region in ps_aty is generalized and can be instantiated. *)
and region in [ps_aty] is generalized and can be instantiated. *)
ps_subst : ity_subst;
(* this substitution instantiates every type variable and region
in ps_vars to itself *)
(** this substitution instantiates every type variable and region
in [ps_vars] to itself *)
}
module Mps : Extmap.S with type key = psymbol
......@@ -108,7 +110,7 @@ val ps_equal : psymbol -> psymbol -> bool
val create_psymbol : preid -> ?ghost:bool -> aty -> psymbol
(** program expressions *)
(** {2 Program expressions} *)
type assertion_kind = Aassert | Aassume | Acheck
......@@ -184,7 +186,7 @@ val e_arrow : psymbol -> ity list -> ity -> expr
(** [e_arrow p argl res] instantiates the program function symbol [p]
into a program expression having the given types of the arguments
and the result. The resulting expression can be applied to
arguments using [e_app] given below.
arguments using {!e_app} given below.
See also [examples/use_api/mlw.ml] *)
......@@ -196,10 +198,9 @@ val aty_of_expr : expr -> aty
val e_app : expr -> expr list -> expr
(** [e_app e el] builds the application of [e] to arguments [el].
[e] is typically constructed using [e_arrow] defined above.
[e] is typically constructed using {!e_arrow} defined above.
See also [examples/use_api/mlw.ml]
*)
See also [examples/use_api/mlw.ml] *)
val e_lapp : lsymbol -> expr list -> ity -> expr
val e_plapp : plsymbol -> expr list -> ity -> expr
......@@ -212,7 +213,7 @@ val create_fun_defn : preid -> lambda -> fun_defn
val create_rec_defn : (psymbol * lambda) list -> fun_defn list
exception StaleRegion of expr * ident
(* freshness violation: a previously reset region is associated to an ident *)
(** freshness violation: a previously reset region is associated to an ident *)
val e_let : let_defn -> expr -> expr
val e_rec : fun_defn list -> expr -> expr
......@@ -248,7 +249,7 @@ val e_any : spec -> vty -> expr
val e_assert : assertion_kind -> term -> expr
val e_absurd : ity -> expr
(** expression traversal *)
(** {2 Expression traversal} *)
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
......
......@@ -20,6 +20,8 @@ open Mlw_ty.T
open Mlw_expr
open Mlw_decl
(** *)
type type_symbol =
| PT of itysymbol
| TS of tysymbol
......@@ -50,7 +52,7 @@ val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_ns : namespace -> string list -> namespace
(** Module *)
(** {2 Module} *)
type modul = private {
mod_theory: theory; (* pure theory *)
......@@ -61,7 +63,7 @@ type modul = private {
mod_used : Sid.t; (* used modules *)
}
(** Module under construction *)
(** {2 Module under construction} *)
type module_uc (* a module under construction *)
......@@ -76,25 +78,25 @@ val get_namespace : module_uc -> namespace
val get_known : module_uc -> known_map
val restore_path : ident -> string list * string * string list
(* [restore_path id] returns the triple (library path, module,
(** [restore_path id] returns the triple (library path, module,
qualified symbol name) if the ident was ever introduced in
a module declaration. If the ident was declared in several
different modules, the first association is retained.
Raises Not_found if the ident was never declared in a module. *)
(** Use and clone *)
(** {2 Use and clone} *)
val use_export : module_uc -> modul -> module_uc
val clone_export : module_uc -> modul -> th_inst -> module_uc
(** Logic decls *)
(** {2 Logic decls} *)
val add_decl : module_uc -> decl -> module_uc
val use_export_theory: module_uc -> theory -> module_uc
val clone_export_theory: module_uc -> theory -> th_inst -> module_uc
val add_meta : module_uc -> meta -> meta_arg list -> module_uc
(** Program decls *)
(** {2 Program decls} *)
val add_pdecl : wp:bool -> module_uc -> pdecl -> module_uc
(** [add_pdecl ~wp m d] adds declaration [d] in module [m].
......@@ -104,6 +106,6 @@ exception TooLateInvariant
val add_invariant : module_uc -> itysymbol -> post -> module_uc
(** Builtin symbols *)
(** {2 Builtin symbols} *)
val xs_exit : xsymbol (* exception used to break the loops *)
......@@ -13,7 +13,9 @@ open Ident
open Ty
open Term
(** individual types (first-order types w/o effects) *)
(** *)
(** {2 Individual types (first-order types w/o effects)} *)
module rec T : sig
......@@ -23,13 +25,13 @@ module rec T : sig
}
type itysymbol = private {
its_ts : tysymbol; (* "pure snapshot" type symbol *)
its_regs : region list; (* region arguments *)
its_def : ity option; (* type alias definition *)
its_ghrl : bool list; (* ghost region arguments *)
its_inv : bool; (* carries a type invariant *)
its_abst : bool; (* is an abstract (= "model") type *)
its_priv : bool; (* is a private (à la Ocaml) type *)
its_ts : tysymbol; (** "pure snapshot" type symbol *)
its_regs : region list; (** region arguments *)
its_def : ity option; (** type alias definition *)
its_ghrl : bool list; (** ghost region arguments *)
its_inv : bool; (** carries a type invariant *)
its_abst : bool; (** is an abstract (= "model") type *)
its_priv : bool; (** is a private (à la Ocaml) type *)
}
(** ity = individual type in programs, first-order, i.e. no functions *)
......@@ -91,7 +93,7 @@ val create_itysymbol :
tvsymbol list -> region list -> ity option -> itysymbol
val restore_its : tysymbol -> itysymbol
(* raises Not_found if the argument is not a its_ts *)
(** raises [Not_found] if the argument is not a its_ts *)
val ity_var : tvsymbol -> ity
val ity_pur : tysymbol -> ity list -> ity
......@@ -99,20 +101,20 @@ val ity_pur : tysymbol -> ity list -> ity
val ity_app : itysymbol -> ity list -> region list -> ity
val ity_app_fresh : itysymbol -> ity list -> ity
(* all aliases expanded, all regions removed *)
val ty_of_ity : ity -> ty
(** all aliases expanded, all regions removed *)
(* replaces every [Tyapp] with [Itypur] *)
val ity_of_ty : ty -> ity
(** replaces every [Tyapp] with [Itypur] *)
(* generic traversal functions *)
(** {2 Generic traversal functions} *)
val ity_map : (ity -> ity) -> ity -> ity
val ity_fold : ('a -> ity -> 'a) -> 'a -> ity -> 'a
val ity_all : (ity -> bool) -> ity -> bool
val ity_any : (ity -> bool) -> ity -> bool
(* traversal functions on type symbols *)
(** {2 Traversal functions on type symbols} *)
val ity_s_fold :
('a -> itysymbol -> 'a) -> ('a -> tysymbol -> 'a) -> 'a -> ity -> 'a
......@@ -140,9 +142,9 @@ val reg_occurs : region -> varset -> bool
val ity_nonghost_reg : Sreg.t -> ity -> Sreg.t
val lookup_nonghost_reg : Sreg.t -> ity -> bool
(* built-in types *)
(** {2 Built-in types} *)
val ts_unit : tysymbol (* the same as [Ty.ts_tuple 0] *)
val ts_unit : tysymbol (** the same as [Ty.ts_tuple 0] *)
val ty_unit : ty
val ity_int : ity
......@@ -171,7 +173,7 @@ val ity_full_inst : ity_subst -> ity -> ity
val reg_full_inst : ity_subst -> region -> region
(* varset manipulation *)
(** {2 Varset manipulation} *)
val vars_empty : varset
......@@ -179,10 +181,11 @@ val vars_union : varset -> varset -> varset
val vars_freeze : varset -> ity_subst
(* exception symbols *)
(** {2 Exception symbols} *)
type xsymbol = private {
xs_name : ident;
xs_ity : ity; (* closed and immutable *)
xs_ity : ity; (** closed and immutable *)
}
val xs_equal : xsymbol -> xsymbol -> bool
......@@ -195,13 +198,13 @@ val create_xsymbol : preid -> ity -> xsymbol
module Mexn: Extmap.S with type key = xsymbol
module Sexn: Extset.S with module M = Mexn
(** effects *)
(** {2 Effects} *)
type effect = private {
eff_writes : Sreg.t;
eff_raises : Sexn.t;
eff_ghostw : Sreg.t; (* ghost writes *)
eff_ghostx : Sexn.t; (* ghost raises *)
eff_ghostw : Sreg.t; (** ghost writes *)
eff_ghostx : Sexn.t; (** ghost raises *)
(* if r1 -> Some r2 then r1 appears in ty(r2) *)
eff_resets : region option Mreg.t;
eff_compar : Stv.t;
......@@ -235,7 +238,7 @@ val eff_full_inst : ity_subst -> effect -> effect
val eff_is_empty : effect -> bool
(** specification *)
(** {2 Specification} *)
type pre = term (** precondition: pre_fmla *)
type post = term (** postcondition: eps result . post_fmla *)
......@@ -256,7 +259,7 @@ type spec = {
c_letrec : int;
}
(** program variables *)
(** {2 Program variables} *)
type pvsymbol = private {
pv_vs : vsymbol;
......@@ -274,15 +277,15 @@ val pv_equal : pvsymbol -> pvsymbol -> bool
val create_pvsymbol : preid -> ?ghost:bool -> ity -> pvsymbol
val restore_pv : vsymbol -> pvsymbol
(** raises Not_found if the argument is not a pv_vs *)
(** raises [Not_found] if the argument is not a [pv_vs] *)
val t_pvset : Spv.t -> term -> Spv.t
(** raises Not_found if the term contains non-pv variables *)
(** raises [Not_found] if the term contains non-pv variables *)
val spec_pvset : Spv.t -> spec -> Spv.t
(** raises Not_found if the spec contains non-pv variables *)
(** raises [Not_found] if the spec contains non-pv variables *)
(** program types *)
(** {2 Program types} *)
type vty =
| VTvalue of ity
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment