theory.mli 5.54 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 57 58 59 60 61
(** 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

type meta_arg_real =
  | MARid  of ident
  | MARstr of string
  | MARint of int

62 63
val register_meta     : string -> meta_arg_type list -> unit
val register_meta_exc : string -> meta_arg_type list -> unit
64 65

val lookup_meta : string -> meta_arg_type list
66
val is_meta_exc : string -> bool
67 68

val list_meta : unit -> string list
69

70
(** Theory *)
71

72
type theory = private {
73 74 75 76 77 78 79 80 81 82 83
  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;
84
}
85

86
and tdecl_node = private
87 88
  | Decl  of decl
  | Use   of theory
89 90
  | Clone of theory * ident Mid.t
  | Meta  of string * meta_arg_real list
91

92 93 94 95
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
96

97
val td_equal : tdecl -> tdecl -> bool
98

99
(** Constructors and utilities *)
100

101
type theory_uc  (* a theory under construction *)
102

103 104
val create_theory : preid -> theory_uc
val close_theory  : theory_uc -> theory
105

106 107
val open_namespace  : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
108

109
val get_namespace : theory_uc -> namespace
110 111 112
val get_known : theory_uc -> known_map

(** Declaration constructors *)
113

114 115 116
val create_decl : decl -> tdecl

val add_decl : theory_uc -> decl -> theory_uc
117 118 119 120 121 122 123 124 125 126

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

127 128 129 130 131 132
(** Use *)

val create_use : theory -> tdecl

val use_export : theory_uc -> theory -> theory_uc

Andrei Paskevich's avatar
Andrei Paskevich committed
133
(** Clone *)
134 135

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

150
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
151 152 153

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

154
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173

val create_null_clone : theory -> tdecl

(** Meta *)

val create_meta : string -> meta_arg list -> tdecl

val add_meta : theory_uc -> string -> meta_arg list -> theory_uc

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
174

175
(* exceptions *)
176

177 178 179
exception NonLocal of ident
exception CannotInstantiate of ident
exception BadInstance of ident * ident
180

181 182 183
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
184

185 186 187 188 189
exception KnownMeta of string
exception UnknownMeta of string
exception BadMetaArity of string * int * int
exception MetaTypeMismatch of string * meta_arg_type * meta_arg_type