theory.mli 5.73 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

open Ident
open Ty
open Term
23
open Decl
24

25
(** Namespace *)
26 27 28 29

module Snm : Set.S with type elt = string
module Mnm : Map.S with type key = string

30
type namespace = private {
31 32
  ns_ts : tysymbol Mnm.t;   (* type symbols *)
  ns_ls : lsymbol Mnm.t;    (* logic symbols *)
33
  ns_pr : prsymbol Mnm.t;   (* propositions *)
34 35 36
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
}

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

41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
(** Meta properties *)

type meta_arg_type =
  | MTtysymbol
  | MTlsymbol
  | MTprsymbol
  | MTstring
  | MTint

type meta_arg =
  | MAts  of tysymbol
  | MAls  of lsymbol
  | MApr  of prsymbol
  | MAstr of string
  | MAint of int

57
type meta
58

59 60 61
module Smeta : Set.S with type elt = meta
module Mmeta : Map.S with type key = meta
module Hmeta : Hashtbl.S with type key = meta
62

63 64 65 66 67 68 69 70 71 72 73
val meta_equal : meta -> meta -> bool

val register_meta      : string -> meta_arg_type list -> meta
val register_meta_excl : string -> meta_arg_type list -> meta
val lookup_meta        : string -> meta

val meta_name     : meta -> string
val meta_arg_type : meta -> meta_arg_type list
val is_meta_excl  : meta -> bool

val list_metas : unit -> meta list
74

75
(** Theory *)
76

77
type theory = private {
78 79 80 81 82 83 84 85 86 87 88
  th_name   : ident;      (* theory name *)
  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;
89
}
90

91
and tdecl_node = private
92 93
  | Decl  of decl
  | Use   of theory
94
  | Clone of theory * tysymbol Mts.t * lsymbol Mls.t * prsymbol Mpr.t
95
  | Meta  of meta * meta_arg list
96

97 98 99 100
module Stdecl : Set.S with type elt = tdecl
module Mtdecl : Map.S with type key = tdecl
module Htdecl : Hashtbl.S with type key = tdecl
module Wtdecl : Hashweak.S with type key = tdecl
101

102
val td_equal : tdecl -> tdecl -> bool
103

104
(** Constructors and utilities *)
105

106
type theory_uc  (* a theory under construction *)
107

108 109
val create_theory : preid -> theory_uc
val close_theory  : theory_uc -> theory
110

111 112
val open_namespace  : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
113

114
val get_namespace : theory_uc -> namespace
115 116 117
val get_known : theory_uc -> known_map

(** Declaration constructors *)
118

119 120 121
val create_decl : decl -> tdecl

val add_decl : theory_uc -> decl -> theory_uc
122 123 124 125 126 127 128 129 130 131

val add_ty_decl : theory_uc -> ty_decl list -> theory_uc
val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
val add_ind_decl : theory_uc -> ind_decl list -> theory_uc
val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> fmla -> theory_uc

val add_ty_decls : theory_uc -> ty_decl list -> theory_uc
val add_logic_decls : theory_uc -> logic_decl list -> theory_uc
val add_ind_decls : theory_uc -> ind_decl list -> theory_uc

132 133 134 135 136 137
(** Use *)

val create_use : theory -> tdecl

val use_export : theory_uc -> theory -> theory_uc

Andrei Paskevich's avatar
Andrei Paskevich committed
138
(** Clone *)
139 140

type th_inst = {
Francois Bobot's avatar
 
Francois Bobot committed
141
  inst_ts    : tysymbol Mts.t; (* old to new *)
142 143 144 145 146 147 148
  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
149 150 151 152 153 154
val create_inst :
  ts    : (tysymbol * tysymbol) list ->
  ls    : (lsymbol  * lsymbol)  list ->
  lemma : prsymbol list ->
  goal  : prsymbol list -> th_inst

155
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
156 157 158

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

159
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
160 161 162 163 164

val create_null_clone : theory -> tdecl

(** Meta *)

165
val create_meta : meta -> meta_arg list -> tdecl
166

167
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
168 169 170 171 172 173 174 175 176 177 178

val clone_meta : tdecl -> theory -> tdecl -> tdecl
(* [clone_meta td_meta th td_clone] produces from [td_meta]
 * a new Meta tdecl instantiated with respect to [td_clone].
 * The [th] argument must be the same as in [td_clone]. *)

(** Base theories *)

val builtin_theory : theory

val tuple_theory : int -> theory
179

180
(* exceptions *)
181

182 183 184
exception NonLocal of ident
exception CannotInstantiate of ident
exception BadInstance of ident * ident
185

186 187 188
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
189

190
exception KnownMeta of meta
191
exception UnknownMeta of string
192 193
exception BadMetaArity of meta * int * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
194