theory.mli 4.12 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 : prop Mnm.t;       (* propositions *)
34 35 36
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
}

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

41 42
val ns_find_prop : namespace -> string list -> prop
val ns_find_fmla : namespace -> string list -> fmla
43

44
(** Theory *)
45

46 47 48 49
type theory = private {
  th_name   : ident;        (* theory name *)
  th_decls  : tdecl list;   (* theory declarations *)
  th_export : namespace;    (* exported namespace *)
50
  th_known  : known_map;    (* known identifiers *)
51
  th_clone  : clone_map;    (* cloning history *)
52
  th_used   : use_map;      (* referenced theories *)
53 54
  th_local  : Sid.t;        (* locally declared idents *)
}
55

56 57 58
and tdecl = private
  | Decl  of decl
  | Use   of theory
59
  | Clone of theory * (ident * ident) list
60

61 62
and use_map = theory Mid.t

63
and clone_map = Sid.t Mid.t
64

65
val builtin_theory : theory
66

67
(** Constructors and utilities *)
68

69
type theory_uc  (* a theory under construction *)
70

71 72
val create_theory : preid -> theory_uc
val close_theory  : theory_uc -> theory
73

74
val add_decl : theory_uc -> decl -> theory_uc
Andrei Paskevich's avatar
Andrei Paskevich committed
75
val use_export : theory_uc -> theory -> theory_uc
76

77 78
val open_namespace  : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
79

80
val get_namespace : theory_uc -> namespace
81

82 83 84 85 86 87 88 89 90 91 92
(** Declaration constructors + add_decl *)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
93
(** Clone *)
94 95

type th_inst = {
Francois Bobot's avatar
 
Francois Bobot committed
96
  inst_ts    : tysymbol Mts.t; (* old to new *)
97 98 99 100 101 102 103
  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
104 105 106 107 108 109
val create_inst :
  ts    : (tysymbol * tysymbol) list ->
  ls    : (lsymbol  * lsymbol)  list ->
  lemma : prsymbol list ->
  goal  : prsymbol list -> th_inst

110
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
111

112
val merge_clone  : clone_map -> theory -> (ident * ident) list -> clone_map
113

114
(* exceptions *)
115

116 117 118
exception NonLocal of ident
exception CannotInstantiate of ident
exception BadInstance of ident * ident
119

120 121 122
exception CloseTheory
exception NoOpenedNamespace
exception ClashSymbol of string
123