mlw_module.mli 4.33 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11

12 13
(** {1 Program modules} *)

14
open Stdlib
15 16
open Ident
open Ty
17 18
open Term
open Decl
19 20
open Theory
open Mlw_ty
21
open Mlw_ty.T
22 23 24
open Mlw_expr
open Mlw_decl

25 26 27 28 29
type type_symbol =
  | PT of itysymbol
  | TS of tysymbol

type prog_symbol =
30 31 32
  | PV of pvsymbol
  | PS of psymbol
  | PL of plsymbol
33 34
  | XS of xsymbol
  | LS of lsymbol
35

36 37 38 39
type namespace = {
  ns_ts : type_symbol Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
40 41
}

42 43 44 45 46 47 48 49 50 51 52 53
val ns_find_type_symbol : namespace -> string list -> type_symbol
val ns_find_prog_symbol : namespace -> string list -> prog_symbol

val ns_find_its : namespace -> string list -> itysymbol
val ns_find_ts  : namespace -> string list -> tysymbol
val ns_find_pv  : namespace -> string list -> pvsymbol
val ns_find_ps  : namespace -> string list -> psymbol
val ns_find_pl  : namespace -> string list -> plsymbol
val ns_find_xs  : namespace -> string list -> xsymbol
val ns_find_ls  : namespace -> string list -> lsymbol

val ns_find_ns  : namespace -> string list -> namespace
54

55
(** {2 Module} *)
56 57 58 59 60

type modul = private {
  mod_theory: theory;			(* pure theory *)
  mod_decls : pdecl list;		(* module declarations *)
  mod_export: namespace;		(* exported namespace *)
61
  mod_known : Mlw_decl.known_map;	(* known identifiers *)
62
  mod_local : Sid.t;			(* locally declared idents *)
63
  mod_used  : Sid.t;			(* used modules *)
64 65
}

66
(** {2 Module under construction} *)
67 68 69

type module_uc (* a module under construction *)

70
val create_module : Env.env -> ?path:string list -> preid -> module_uc
71 72
val close_module  : module_uc -> modul

73 74
val open_namespace  : module_uc -> string -> module_uc
val close_namespace : module_uc -> bool -> module_uc
75

76
val get_theory : module_uc -> theory_uc
77
val get_namespace : module_uc -> namespace
78
val get_known : module_uc -> Mlw_decl.known_map
79

80
val restore_path : ident -> string list * string * string list
81
(** [restore_path id] returns the triple (library path, module,
82 83 84
   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.
85 86
   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. *)
87

88 89 90 91
val restore_module : theory -> modul
(** retrieves a module from its underlying theory
    raises [Not_found] if no such module exists *)

92
(** {2 Use and clone} *)
93

94
val use_export : module_uc -> modul -> module_uc
95 96 97 98 99 100 101

type mod_inst = {
  inst_pv : pvsymbol Mpv.t;
  inst_ps : psymbol Mps.t;
}

val clone_export : module_uc -> modul -> mod_inst -> th_inst -> module_uc
102

103
(** {2 Logic decls} *)
104 105 106 107 108 109

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

110
(** {2 Program decls} *)
111

112
val add_pdecl : wp:bool -> module_uc -> pdecl -> module_uc
113
(** [add_pdecl ~wp m d] adds declaration [d] in module [m].
114
    If [wp] is [true], VC is computed and added to [m]. *)
115

116 117
exception TooLateInvariant

118 119
val add_invariant : module_uc -> itysymbol -> post -> module_uc

120
(** {2 Builtin symbols} *)
121 122

val xs_exit : xsymbol (* exception used to break the loops *)
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138

(** {2 WhyML language} *)

open Env

type mlw_file = modul Mstr.t * theory Mstr.t

val mlw_language : mlw_file language

exception ModuleNotFound of pathname * string
exception ModuleOrTheoryNotFound of pathname * string

type module_or_theory = Module of modul | Theory of theory

val read_module : env -> pathname -> string -> modul
val read_module_or_theory : env -> pathname -> string -> module_or_theory