theory.mli 6.49 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

21
open Stdlib
22
open Util
23

MARCHE Claude's avatar
MARCHE Claude committed
24 25
(** Theories and Namespaces *)

26 27 28
open Ident
open Ty
open Term
29
open Decl
30

31
type namespace = {
32 33 34 35
  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 *)
36 37
}

38 39 40
val ns_find_ts : namespace -> string list -> tysymbol
val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_pr : namespace -> string list -> prsymbol
41
val ns_find_ns : namespace -> string list -> namespace
42

43 44 45
(** Meta properties *)

type meta_arg_type =
46
  | MTty
47 48 49 50 51 52 53
  | MTtysymbol
  | MTlsymbol
  | MTprsymbol
  | MTstring
  | MTint

type meta_arg =
54
  | MAty  of ty
55 56 57 58 59 60
  | MAts  of tysymbol
  | MAls  of lsymbol
  | MApr  of prsymbol
  | MAstr of string
  | MAint of int

61 62 63 64 65
type meta = private {
  meta_name : string;
  meta_type : meta_arg_type list;
  meta_excl : bool;
  meta_tag  : int;
66
  mutable meta_desc : Pp.formatted;
67
}
68

69 70
val print_meta_desc : Pp.formatter -> meta -> unit

71
module Mmeta : Map.S with type key = meta
72
module Smeta : Mmeta.Set
73
module Hmeta : Hashtbl.S with type key = meta
74

75
val meta_equal : meta -> meta -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
76
val meta_hash : meta -> int
77

78 79 80 81
val register_meta      :
  desc:Pp.formatted -> string -> meta_arg_type list -> meta
val register_meta_excl :
  desc:Pp.formatted -> string -> meta_arg_type list -> meta
François Bobot's avatar
François Bobot committed
82 83
(** Register exclusive meta, each new setting remove the previous one.
Useful for transformation or printer parameters *)
84

85 86
val lookup_meta : string -> meta
val list_metas  : unit -> meta list
87
val set_meta_desc : Pp.formatted -> meta -> unit
88

89
(** Theory *)
90

91
type theory = private {
92
  th_name   : ident;      (* theory name *)
93
  th_path   : string list;(* environment qualifiers *)
94 95 96 97 98 99 100 101 102 103
  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;
104
}
105

106
and tdecl_node = private
107 108
  | Decl  of decl
  | Use   of theory
109
  | Clone of theory * symbol_map
110
  | Meta  of meta * meta_arg list
111

112
and symbol_map = private {
113 114 115 116 117
  sm_ts : tysymbol Mts.t;
  sm_ls : lsymbol Mls.t;
  sm_pr : prsymbol Mpr.t;
}

118
module Mtdecl : Map.S with type key = tdecl
119
module Stdecl : Mtdecl.Set
120
module Htdecl : Hashtbl.S with type key = tdecl
121

122
val td_equal : tdecl -> tdecl -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
123
val td_hash : tdecl -> int
124

125
(** Constructors and utilities *)
126

127
type theory_uc  (* a theory under construction *)
128

129
val create_theory : ?path:string list -> preid -> theory_uc
130
val close_theory  : theory_uc -> theory
131

132 133
val open_namespace  : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
134
  (* the Boolean indicates [import]; the string option indicates [as T] *)
135

136
val get_namespace : theory_uc -> namespace
137 138
val get_known : theory_uc -> known_map

139 140
val get_rev_decls : theory_uc -> tdecl list

141
(** Declaration constructors *)
142

143 144 145
val create_decl : decl -> tdecl

val add_decl : theory_uc -> decl -> theory_uc
146

147 148 149
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
150
val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
151
val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
152
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
153

154 155 156 157 158
(** Use *)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
159
(** Clone *)
160 161

type th_inst = {
Francois Bobot's avatar
 
Francois Bobot committed
162
  inst_ts    : tysymbol Mts.t; (* old to new *)
163 164 165 166 167 168 169
  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
170 171 172 173 174 175
val create_inst :
  ts    : (tysymbol * tysymbol) list ->
  ls    : (lsymbol  * lsymbol)  list ->
  lemma : prsymbol list ->
  goal  : prsymbol list -> th_inst

176
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
177 178 179

val create_clone : tdecl list -> theory -> th_inst -> tdecl list

180
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
181 182 183

val create_null_clone : theory -> tdecl

184 185
val is_empty_sm : symbol_map -> bool

186 187
(** Meta *)

188
val create_meta : meta -> meta_arg list -> tdecl
189

190
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
191

192 193 194
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]]. *)
195

196
(*
197
val on_meta: meta-> ('a -> meta_arg list -> 'a) -> 'a -> theory -> 'a
198
*)
199

200 201 202 203
(** Base theories *)

val builtin_theory : theory

204 205
val bool_theory : theory

206 207
val highord_theory : theory

208
val tuple_theory : int -> theory
209

210 211
val tuple_theory_name : string -> int option

212 213
val add_decl_with_tuples : theory_uc -> decl -> theory_uc

214
(* exceptions *)
215

216 217 218
exception NonLocal of ident
exception CannotInstantiate of ident
exception BadInstance of ident * ident
219

220 221 222
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
223

224
exception KnownMeta of meta
225
exception UnknownMeta of string
226 227
exception BadMetaArity of meta * int * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
228