pmodule.mli 5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
open Wstdlib
13
open Ident
Andrei Paskevich's avatar
Andrei Paskevich committed
14 15 16
open Ty
open Term
open Decl
17 18 19
open Theory
open Ity
open Expr
20
open Pdecl
21 22 23 24 25 26

(** *)

type prog_symbol =
  | PV of pvsymbol
  | RS of rsymbol
27
  | OO of Srs.t
28 29 30 31

type namespace = {
  ns_ts : itysymbol   Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
32
  ns_xs : xsymbol     Mstr.t;  (* exception symbols *)
33 34 35 36 37
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
}

val ns_find_prog_symbol : namespace -> string list -> prog_symbol

38
val ns_find_its : namespace -> string list -> itysymbol
39 40 41 42 43
val ns_find_pv  : namespace -> string list -> pvsymbol
val ns_find_rs  : namespace -> string list -> rsymbol
val ns_find_xs  : namespace -> string list -> xsymbol
val ns_find_ns  : namespace -> string list -> namespace

44
type overload =
45 46 47
  | FixedRes of ity (* t -> t -> ... -> T *)
  | SameType        (* t -> t -> ... -> t *)
  | NoOver          (* neither *)
48 49 50

val overload_of_rs : rsymbol -> overload

51 52
val ref_attr : Ident.attribute

53 54
exception IncompatibleNotation of string

55 56
(** {2 Module} *)

57
type pmodule = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
58 59 60 61 62 63 64 65 66 67 68
  mod_theory : theory;        (* pure theory *)
  mod_units  : mod_unit list; (* module declarations *)
  mod_export : namespace;     (* exported namespace *)
  mod_known  : known_map;     (* known identifiers *)
  mod_local  : Sid.t;         (* locally declared idents *)
  mod_used   : Sid.t;         (* used modules *)
}

and mod_unit =
  | Udecl  of pdecl
  | Uuse   of pmodule
Andrei Paskevich's avatar
Andrei Paskevich committed
69
  | Uclone of mod_inst
Andrei Paskevich's avatar
Andrei Paskevich committed
70
  | Umeta  of meta * meta_arg list
71
  | Uscope of string * mod_unit list
Andrei Paskevich's avatar
Andrei Paskevich committed
72

73
and mod_inst = {
Andrei Paskevich's avatar
Andrei Paskevich committed
74
  mi_mod : pmodule;
75 76
  mi_ty  : ity Mts.t;
  mi_ts  : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
77 78
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
79
  mi_pk  : prop_kind Mpr.t;
80
  mi_pv  : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  mi_rs  : rsymbol Mrs.t;
82
  mi_xs  : xsymbol Mxs.t;
83
  mi_df  : prop_kind;
84 85
}

86 87
val empty_mod_inst: pmodule -> mod_inst

88 89
(** {2 Module under construction} *)

90
type pmodule_uc = private {
91
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
92
  muc_units  : mod_unit list;
93 94 95 96 97
  muc_import : namespace list;
  muc_export : namespace list;
  muc_known  : known_map;
  muc_local  : Sid.t;
  muc_used   : Sid.t;
98
  muc_env    : Env.env;
99 100
}

101 102
val create_module : Env.env -> ?path:string list -> preid -> pmodule_uc
val close_module  : pmodule_uc -> pmodule
103

104 105 106
val open_scope   : pmodule_uc -> string -> pmodule_uc
val close_scope  : pmodule_uc -> import:bool -> pmodule_uc
val import_scope : pmodule_uc -> string list -> pmodule_uc
107 108 109 110 111 112 113 114 115

val restore_path : ident -> string list * string * string list
(** [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.
   If [id] is a module name, the third component is an empty list.
   Raises Not_found if the ident was never declared in/as a module. *)

116 117 118 119
val restore_module_id : ident -> pmodule
(** retrieves a module from a program symbol defined in it
    Raises Not_found if the ident was never declared in/as a module. *)

120
val restore_module : theory -> pmodule
121 122 123 124 125
(** retrieves a module from its underlying theory
    raises [Not_found] if no such module exists *)

(** {2 Use and clone} *)

126
val use_export : pmodule_uc -> pmodule -> pmodule_uc
127

128
val clone_export : pmodule_uc -> pmodule -> mod_inst -> pmodule_uc
Andrei Paskevich's avatar
Andrei Paskevich committed
129

130 131
(** {2 Logic decls} *)

132
val add_meta : pmodule_uc -> meta -> meta_arg list -> pmodule_uc
133 134 135

(** {2 Program decls} *)

136
val add_pdecl : ?warn:bool -> vc:bool -> pmodule_uc -> pdecl -> pmodule_uc
137 138
(** [add_pdecl ~vc m d] adds declaration [d] in module [m].
    If [vc] is [true], VC is computed and added to [m]. *)
139 140 141

(** {2 Builtin symbols} *)

142 143 144 145 146
val builtin_module : pmodule
val bool_module : pmodule
val unit_module : pmodule
val highord_module : pmodule
val tuple_module : int -> pmodule
147 148 149 150
val ref_module : pmodule

val its_ref     : itysymbol
val ts_ref      : tysymbol
151
val rs_ref      : rsymbol
152 153 154 155
val rs_ref_cons : rsymbol
val rs_ref_proj : rsymbol
val ls_ref_cons : lsymbol
val ls_ref_proj : lsymbol
156 157 158 159 160

(** {2 WhyML language} *)

open Env

161
type mlw_file = pmodule Mstr.t
162 163 164

val mlw_language : mlw_file language

165 166
val mlw_language_builtin : pathname -> mlw_file

167 168
exception ModuleNotFound of pathname * string

169
val read_module : env -> pathname -> string -> pmodule
Andrei Paskevich's avatar
Andrei Paskevich committed
170 171 172 173 174

(** {2 Pretty-printing} *)

val print_unit : Format.formatter -> mod_unit -> unit
val print_module : Format.formatter -> pmodule -> unit