theory.mli 5.96 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12 13
open Stdlib

MARCHE Claude's avatar
MARCHE Claude committed
14 15
(** Theories and Namespaces *)

16 17 18
open Ident
open Ty
open Term
19
open Decl
20

21
type namespace = {
22 23 24 25
  ns_ts : tysymbol Mstr.t;   (* type symbols *)
  ns_ls : lsymbol Mstr.t;    (* logic symbols *)
  ns_pr : prsymbol Mstr.t;   (* propositions *)
  ns_ns : namespace Mstr.t;  (* inner namespaces *)
26 27
}

28 29 30
val ns_find_ts : namespace -> string list -> tysymbol
val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_pr : namespace -> string list -> prsymbol
31
val ns_find_ns : namespace -> string list -> namespace
32

33 34 35
(** Meta properties *)

type meta_arg_type =
36
  | MTty
37 38 39 40 41 42 43
  | MTtysymbol
  | MTlsymbol
  | MTprsymbol
  | MTstring
  | MTint

type meta_arg =
44
  | MAty  of ty
45 46 47 48 49 50
  | MAts  of tysymbol
  | MAls  of lsymbol
  | MApr  of prsymbol
  | MAstr of string
  | MAint of int

51 52 53 54
type meta = private {
  meta_name : string;
  meta_type : meta_arg_type list;
  meta_excl : bool;
55
  meta_desc : Pp.formatted;
56 57
  meta_tag  : int;
}
58

59 60
val print_meta_desc : Pp.formatter -> meta -> unit

61 62 63
module Mmeta : Extmap.S with type key = meta
module Smeta : Extset.S with module M = Mmeta
module Hmeta : Exthtbl.S with type key = meta
64

65
val meta_equal : meta -> meta -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
66
val meta_hash : meta -> int
67

68
val register_meta :
69
  desc:Pp.formatted -> string -> meta_arg_type list -> meta
70

71 72
val register_meta_excl :
  desc:Pp.formatted -> string -> meta_arg_type list -> meta
73 74
(** With exclusive metas, each new meta cancels the previous one.
    Useful for transformation or printer parameters *)
75

76 77
val lookup_meta : string -> meta
val list_metas  : unit -> meta list
78

79
(** Theory *)
80

81
type theory = private {
82
  th_name   : ident;      (* theory name *)
83
  th_path   : string list;(* environment qualifiers *)
84 85 86 87 88 89 90 91 92 93
  th_decls  : tdecl list; (* theory declarations *)
  th_export : namespace;  (* exported namespace *)
  th_known  : known_map;  (* known identifiers *)
  th_local  : Sid.t;      (* locally declared idents *)
  th_used   : Sid.t;      (* used theories *)
}

and tdecl = private {
  td_node : tdecl_node;
  td_tag  : int;
94
}
95

96
and tdecl_node = private
97 98
  | Decl  of decl
  | Use   of theory
99
  | Clone of theory * symbol_map
100
  | Meta  of meta * meta_arg list
101

102
and symbol_map = private {
103 104 105 106 107
  sm_ts : tysymbol Mts.t;
  sm_ls : lsymbol Mls.t;
  sm_pr : prsymbol Mpr.t;
}

108 109 110
module Mtdecl : Extmap.S with type key = tdecl
module Stdecl : Extset.S with module M = Mtdecl
module Htdecl : Exthtbl.S with type key = tdecl
111

112
val td_equal : tdecl -> tdecl -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
113
val td_hash : tdecl -> int
114

115
(** Constructors and utilities *)
116

117
type theory_uc  (* a theory under construction *)
118

119
val create_theory : ?path:string list -> preid -> theory_uc
120
val close_theory  : theory_uc -> theory
121

122 123
val open_namespace  : theory_uc -> string -> theory_uc
val close_namespace : theory_uc -> bool (* import *) -> theory_uc
124

125
val get_namespace : theory_uc -> namespace
126
val get_known : theory_uc -> known_map
127 128
val get_rev_decls : theory_uc -> tdecl list

129 130 131 132 133 134 135
val restore_path : ident -> string list * string * string list
(* [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. *)

136
(** Declaration constructors *)
137

138 139 140
val create_decl : decl -> tdecl

val add_decl : theory_uc -> decl -> theory_uc
141

142 143 144
val add_ty_decl : theory_uc -> tysymbol -> theory_uc
val add_data_decl : theory_uc -> data_decl list -> theory_uc
val add_param_decl : theory_uc -> lsymbol -> theory_uc
145
val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
146
val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
147
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
148

149 150 151 152 153
(** Use *)

val create_use : theory -> tdecl
val use_export : theory_uc -> theory -> theory_uc

Andrei Paskevich's avatar
Andrei Paskevich committed
154
(** Clone *)
155 156

type th_inst = {
157
  inst_ts    : tysymbol Mts.t; (* old to new *)
158 159 160 161 162 163 164
  inst_ls    : lsymbol  Mls.t;
  inst_lemma : Spr.t;
  inst_goal  : Spr.t;
}

val empty_inst : th_inst

Andrei Paskevich's avatar
Andrei Paskevich committed
165 166 167 168 169 170
val create_inst :
  ts    : (tysymbol * tysymbol) list ->
  ls    : (lsymbol  * lsymbol)  list ->
  lemma : prsymbol list ->
  goal  : prsymbol list -> th_inst

171
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
172

173
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
174 175 176

val create_null_clone : theory -> tdecl

177 178
val is_empty_sm : symbol_map -> bool

179 180
(** Meta *)

181
val create_meta : meta -> meta_arg list -> tdecl
182

183
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
184

185 186 187
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]]. *)
188

189
(*
190
val on_meta: meta-> ('a -> meta_arg list -> 'a) -> 'a -> theory -> 'a
191
*)
192

193 194 195 196
(** Base theories *)

val builtin_theory : theory

197 198
val bool_theory : theory

199 200
val highord_theory : theory

201
val tuple_theory : int -> theory
202

203 204
val tuple_theory_name : string -> int option

205 206
val add_decl_with_tuples : theory_uc -> decl -> theory_uc

207
(* exceptions *)
208

209 210 211
exception NonLocal of ident
exception CannotInstantiate of ident
exception BadInstance of ident * ident
212

213 214 215
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
216

217
exception KnownMeta of meta
218
exception UnknownMeta of string
219 220
exception BadMetaArity of meta * int * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
221