theory.mli 3.16 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 Ty
21 22
open Term

23 24 25
type ty_def = 
  | Ty_abstract
  | Ty_algebraic of fsymbol list
26

27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
type ty_decl = tysymbol * ty_def 

type logic_decl = 
  | Lfunction  of fsymbol * (vsymbol list * term) option (* FIXME: binders *)
  | Lpredicate of psymbol * (vsymbol list * fmla) option (* FIXME: binders *)
  | Linductive of psymbol * (Name.t * fmla) list

type prop_kind = 
  | Axiom | Lemma | Goal

type decl =
  | Dtype  of ty_decl list
  | Dlogic of logic_decl list
  | Dprop  of prop_kind * Name.t * fmla

type decl_or_use =
  | Decl of decl
  | Use of t

and t = private {
47 48 49
  t_name : Name.t;
  t_namespace : namespace;
  t_decls : decl_or_use list;
50
}
51

52 53 54
and namespace

(** Building *)
55

56
type th
57
  (** a theory under construction *)
58

59
val create_theory : Name.t -> th
60

61 62
val open_namespace : th -> th
val close_namespace : th -> Name.t -> import:bool -> th
63

64
val use_export : th -> t -> th
65

66 67 68 69
type th_inst = {
  inst_ts : tysymbol Mts.t;
  inst_fs : fsymbol  Mfs.t;
  inst_ps : psymbol  Mps.t;
70 71
}

72
val clone_export : th -> t -> th_inst -> th
73

74
val add_decl : th -> decl -> th
75

76 77 78
val close_theory : th -> t

(** Querying *)
79

80
val get_namespace : th -> namespace
81

82 83 84 85 86
val find_tysymbol : namespace -> string -> tysymbol
val find_fsymbol  : namespace -> string -> fsymbol
val find_psymbol  : namespace -> string -> psymbol
val find_namespace: namespace -> string -> namespace
val find_fmla     : namespace -> string -> fmla
87

88 89 90 91 92 93
val mem_tysymbol : namespace -> string -> bool
val mem_fsymbol  : namespace -> string -> bool
val mem_psymbol  : namespace -> string -> bool
val mem_namespace: namespace -> string -> bool
val mem_fmla     : namespace -> string -> bool

94 95 96 97 98 99 100 101 102 103 104
(** Error reporting *)

type error

exception Error of error

val report : Format.formatter -> error -> unit


(** Debugging *)

105 106
val print_th : Format.formatter -> th -> unit
val print_t  : Format.formatter -> t  -> unit