theory.mli 6.88 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)
19

20
open Ident
21
open Ty
22
23
open Term

Andrei Paskevich's avatar
Andrei Paskevich committed
24
(** Declarations *)
25

26
(* type declaration *)
27

28
29
type ty_def =
  | Tabstract
30
  | Talgebraic of lsymbol list
31
32
33
34
35

type ty_decl = tysymbol * ty_def

(* logic declaration *)

36
type ls_defn
37

38
39
40
val make_ls_defn : lsymbol -> vsymbol list -> expr -> ls_defn
val make_fs_defn : lsymbol -> vsymbol list -> term -> ls_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ls_defn
Andrei Paskevich's avatar
Andrei Paskevich committed
41

42
43
44
val open_ls_defn : ls_defn -> lsymbol * vsymbol list * expr
val open_fs_defn : ls_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ls_defn -> lsymbol * vsymbol list * fmla
Andrei Paskevich's avatar
Andrei Paskevich committed
45

46
val ls_defn_axiom : ls_defn -> fmla
Andrei Paskevich's avatar
Andrei Paskevich committed
47

48
49
type logic_decl = lsymbol * ls_defn option

50
51
(* inductive predicate declaration *)

52
53
54
55
56
57
58
59
60
61
62
63
type prop

module Spr : Set.S with type elt = prop
module Mpr : Map.S with type key = prop
module Hpr : Hashtbl.S with type key = prop

val create_prop : preid -> prop
val pr_name     : prop -> ident

type prop_fmla = prop * fmla

type ind_decl  = lsymbol * prop_fmla list
64

65
66
67
68
69
70
71
(* proposition declaration *)

type prop_kind =
  | Paxiom
  | Plemma
  | Pgoal

72
type prop_decl = prop_kind * prop * fmla
73

Andrei Paskevich's avatar
Andrei Paskevich committed
74
(** Context and Theory *)
75

Andrei Paskevich's avatar
Andrei Paskevich committed
76
module Snm : Set.S with type elt = string
Francois Bobot's avatar
Francois Bobot committed
77
78
79
module Mnm : Map.S with type key = string

type theory = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
80
81
82
83
84
85
86
87
88
  th_name   : ident;        (* theory name *)
  th_ctxt   : context;      (* theory declarations *)
  th_export : namespace;    (* exported namespace *)
  th_local  : Sid.t;        (* locally declared idents *)
}

and namespace = private {
  ns_ts : tysymbol Mnm.t;   (* type symbols *)
  ns_ls : lsymbol Mnm.t;    (* logic symbols *)
89
  ns_pr : prop_fmla Mnm.t;  (* propositions *)
90
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
Francois Bobot's avatar
Francois Bobot committed
91
92
}

93
and context = private {
94
  ctxt_env    : env;
95
96
  ctxt_decl   : decl;
  ctxt_prev   : context option;
97
  ctxt_known  : decl Mid.t;
98
  ctxt_cloned : Sid.t Mid.t;
99
  ctxt_tag    : int;
Andrei Paskevich's avatar
Andrei Paskevich committed
100
101
}

102
103
and env

Andrei Paskevich's avatar
Andrei Paskevich committed
104
105
106
and decl = private {
  d_node : decl_node;
  d_tag  : int;
Francois Bobot's avatar
Francois Bobot committed
107
108
109
}

and decl_node =
110
111
112
  | Dtype  of ty_decl list      (* recursive types *)
  | Dlogic of logic_decl list   (* recursive functions/predicates *)
  | Dind   of ind_decl list     (* inductive predicates *)
113
  | Dprop  of prop_decl         (* axiom / lemma / goal *)
114
115
  | Duse   of theory                         (* depend on a theory *)
  | Dclone of theory * (ident * ident) list  (* replicate a theory *)
116

Andrei Paskevich's avatar
Andrei Paskevich committed
117
(** Declaration constructors *)
118

119
120
121
val create_ty_decl : ty_decl list -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
122
val create_prop_decl : prop_kind -> prop -> fmla -> decl
123

124
125
126
127
128
129
(* separate independent groups of declarations *)

val create_ty_decls : ty_decl list -> decl list
val create_logic_decls : logic_decl list -> decl list
val create_ind_decls : ind_decl list -> decl list

130
131
(* exceptions *)

132
exception ConstructorExpected of lsymbol
133
exception IllegalTypeAlias of tysymbol
134
exception UnboundTypeVar of tvsymbol
135

136
137
138
exception InvalidIndDecl of lsymbol * prop
exception TooSpecificIndDecl of lsymbol * prop * term
exception NonPositiveIndDecl of lsymbol * prop * lsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
139

140
exception IllegalConstructor of lsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
141
exception BadLogicDecl of ident
142
exception UnboundVars of Svs.t
143
144
exception ClashIdent of ident
exception EmptyDecl
145

146
147
148
149
150
151
152
153
154
155
(** Environements *)

type retrieve_theory = env -> string list -> theory Mnm.t

val create_env : retrieve_theory -> env

exception TheoryNotFound of string list * string

val find_theory : env -> string list -> string -> theory

156
157
val env_tag : env -> int

Andrei Paskevich's avatar
Andrei Paskevich committed
158
159
160
(** Context constructors and utilities *)

type th_inst = {
161
162
163
164
  inst_ts    : tysymbol Mts.t;
  inst_ls    : lsymbol  Mls.t;
  inst_lemma : Spr.t;
  inst_goal  : Spr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
165
}
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166

167
168
val empty_inst : th_inst

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
169
170
module Context : sig

171
  val init_context : env -> context
Andrei Paskevich's avatar
Andrei Paskevich committed
172

173
  val add_decl : context -> decl -> context
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174

Andrei Paskevich's avatar
Andrei Paskevich committed
175
176
  val use_export   : context -> theory -> context
  val clone_export : context -> theory -> th_inst -> context
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177

178
179
  (* bottom-up, tail-recursive traversal functions *)
  val ctxt_fold : ('a -> decl -> 'a) -> 'a -> context -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
180
  val ctxt_iter : (decl -> unit) -> context -> unit
181

182
183
  (* top-down list of declarations *)
  val get_decls : context -> decl list
184

Andrei Paskevich's avatar
Andrei Paskevich committed
185
186
  exception UnknownIdent of ident
  exception RedeclaredIdent of ident
187
188

  exception NonLocal of ident
Andrei Paskevich's avatar
Andrei Paskevich committed
189
  exception CannotInstantiate of ident
190
  exception BadInstance of ident * ident
191

Andrei Paskevich's avatar
Andrei Paskevich committed
192
end
193

194
195
196
197
198
199
200
201
202
(** Namespace search tools *)

val ns_find_ts   : namespace -> string list -> tysymbol
val ns_find_ls   : namespace -> string list -> lsymbol
val ns_find_pr   : namespace -> string list -> prop_fmla

val ns_find_prop : namespace -> string list -> prop
val ns_find_fmla : namespace -> string list -> fmla

Andrei Paskevich's avatar
Andrei Paskevich committed
203
(** Theory constructors and utilities *)
204

Andrei Paskevich's avatar
Andrei Paskevich committed
205
type theory_uc  (* a theory under construction *)
206

207
module TheoryUC : sig
208

209
  val create_theory : env -> preid -> theory_uc
Andrei Paskevich's avatar
Andrei Paskevich committed
210
  val close_theory  : theory_uc -> theory
211

Andrei Paskevich's avatar
Andrei Paskevich committed
212
  val add_decl : theory_uc -> decl -> theory_uc
213

Andrei Paskevich's avatar
Andrei Paskevich committed
214
  val open_namespace  : theory_uc -> theory_uc
215
  val close_namespace : theory_uc -> bool -> string option -> theory_uc
216

Andrei Paskevich's avatar
Andrei Paskevich committed
217
218
  val use_export   : theory_uc -> theory -> theory_uc
  val clone_export : theory_uc -> theory -> th_inst -> theory_uc
219

Andrei Paskevich's avatar
Andrei Paskevich committed
220
221
222
223
224
  val get_namespace : theory_uc -> namespace

  exception CloseTheory
  exception NoOpenedNamespace
  exception ClashSymbol of string
225

Andrei Paskevich's avatar
Andrei Paskevich committed
226
end
227

228
229
val builtin_name : string

230
(*
231
232
(** Debugging *)

233
val print_ident : Format.formatter -> ident -> unit
234
val print_uc : Format.formatter -> theory_uc -> unit
235
val print_ctxt : Format.formatter -> context -> unit
236
val print_th : Format.formatter -> theory -> unit
237
238
239
240

(* Utils *)

exception NotGoalContext
241
val goal_of_ctxt : context -> prop
242
243
(* goal_of_ctxt ctxt return the goal of a goal context
   the ctxt must end with a goal.*)
244
*)