theory.mli 5.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 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 37 38
type fs_defn
type ps_defn

39
type logic_decl =
40 41
  | Lfunction  of lsymbol * fs_defn option
  | Lpredicate of lsymbol * ps_defn option
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43 44 45 46 47 48 49 50 51
val make_fs_defn : lsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ps_defn

val open_fs_defn : fs_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> lsymbol * vsymbol list * fmla

val fs_defn_axiom : fs_defn -> fmla
val ps_defn_axiom : ps_defn -> fmla

52 53 54 55
(* inductive predicate declaration *)

type ind_decl = lsymbol * (ident * fmla) list

56 57 58 59 60 61 62 63 64
(* proposition declaration *)

type prop_kind =
  | Paxiom
  | Plemma
  | Pgoal

type prop_decl = prop_kind * ident * fmla

Andrei Paskevich's avatar
Andrei Paskevich committed
65
(** Context and Theory *)
66

Andrei Paskevich's avatar
Andrei Paskevich committed
67
module Snm : Set.S with type elt = string
Francois Bobot's avatar
Francois Bobot committed
68 69 70
module Mnm : Map.S with type key = string

type theory = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
71 72 73 74 75 76 77 78 79 80 81
  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 *)
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
  ns_pr : fmla Mnm.t;       (* propositions *)
Francois Bobot's avatar
Francois Bobot committed
82 83
}

84 85
and context = private {
  ctxt_decls : (decl * context) option;
Andrei Paskevich's avatar
Andrei Paskevich committed
86 87 88 89 90 91 92
  ctxt_known : decl Mid.t;
  ctxt_tag   : int;
}

and decl = private {
  d_node : decl_node;
  d_tag  : int;
Francois Bobot's avatar
Francois Bobot committed
93 94 95
}

and decl_node =
96 97 98 99 100 101
  | Dtype  of ty_decl list      (* mutually recursive types *)
  | Dlogic of logic_decl list   (* mutually recursive functions/predicates *)
  | Dind   of ind_decl          (* inductive predicate *)
  | Dprop  of prop_decl         (* axiom / lemma / goal *)
  | Duse   of theory                (* depend on a theory *)
  | Dclone of (ident * ident) list  (* replicate a theory *)
102

Andrei Paskevich's avatar
Andrei Paskevich committed
103
(** Declaration constructors *)
104

105 106 107
val create_type : ty_decl list -> decl
val create_logic : logic_decl list -> decl
val create_prop : prop_kind -> preid -> fmla -> decl
108
val create_ind : lsymbol -> (preid * fmla) list -> decl
109

110 111
(* exceptions *)

112
exception ConstructorExpected of lsymbol
113 114
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
115

116
exception IllegalConstructor of lsymbol
117
exception UnboundVars of Svs.t
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
118
exception BadDecl of ident
119

Andrei Paskevich's avatar
Andrei Paskevich committed
120 121 122 123 124 125
(** Context constructors and utilities *)

type th_inst = {
  inst_ts : tysymbol Mts.t;
  inst_ls : lsymbol  Mls.t;
}
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126 127 128

module Context : sig

Andrei Paskevich's avatar
Andrei Paskevich committed
129 130
  val empty_context : context

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

Andrei Paskevich's avatar
Andrei Paskevich committed
133 134
  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
135

136 137
  (* bottom-up, tail-recursive traversal functions *)
  val ctxt_fold : ('a -> decl -> 'a) -> 'a -> context -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
138
  val ctxt_iter : (decl -> unit) -> context -> unit
139

140 141
  (* top-down list of declarations *)
  val get_decls : context -> decl list
142

Andrei Paskevich's avatar
Andrei Paskevich committed
143 144 145
  exception UnknownIdent of ident
  exception RedeclaredIdent of ident
  exception CannotInstantiate of ident
146

Andrei Paskevich's avatar
Andrei Paskevich committed
147
end
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149
(** Theory constructors and utilities *)
150

Andrei Paskevich's avatar
Andrei Paskevich committed
151
type theory_uc  (* a theory under construction *)
152

Andrei Paskevich's avatar
Andrei Paskevich committed
153
module Theory : sig
154

Andrei Paskevich's avatar
Andrei Paskevich committed
155 156
  val create_theory : preid -> theory_uc
  val close_theory  : theory_uc -> theory
157

Andrei Paskevich's avatar
Andrei Paskevich committed
158
  val add_decl : theory_uc -> decl -> theory_uc
159

Andrei Paskevich's avatar
Andrei Paskevich committed
160 161
  val open_namespace  : theory_uc -> theory_uc
  val close_namespace : theory_uc -> string -> import:bool -> theory_uc
162

Andrei Paskevich's avatar
Andrei Paskevich committed
163 164
  val use_export   : theory_uc -> theory -> theory_uc
  val clone_export : theory_uc -> theory -> th_inst -> theory_uc
165

Andrei Paskevich's avatar
Andrei Paskevich committed
166 167 168 169 170
  val get_namespace : theory_uc -> namespace

  exception CloseTheory
  exception NoOpenedNamespace
  exception ClashSymbol of string
171

Andrei Paskevich's avatar
Andrei Paskevich committed
172
end
173 174 175

(** Debugging *)

176 177
val print_uc : Format.formatter -> theory_uc -> unit
val print_th : Format.formatter -> theory -> unit