theory.mli 6.98 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 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
(**************************************************************************)
(*                                                                        *)
(*  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

(** Declarations *)

(* type declaration *)

type ty_def =
  | Tabstract
  | Talgebraic of lsymbol list

type ty_decl = tysymbol * ty_def

(* logic declaration *)

type ls_defn

type logic_decl = lsymbol * ls_defn option

val make_ls_defn : lsymbol -> vsymbol list -> expr -> logic_decl
val make_fs_defn : lsymbol -> vsymbol list -> term -> logic_decl
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> logic_decl

val open_ls_defn : ls_defn -> vsymbol list * expr
val open_fs_defn : ls_defn -> vsymbol list * term
val open_ps_defn : ls_defn -> vsymbol list * fmla

val ls_defn_axiom : ls_defn -> fmla

(* inductive predicate declaration *)

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

(* proposition declaration *)

type prop_kind =
  | Paxiom
  | Plemma
  | Pgoal

type prop_decl = prop_kind * prop * fmla

(** Context and Theory *)

module Snm : Set.S with type elt = string
module Mnm : Map.S with type key = string

type theory = private {
  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_pr : prop_fmla Mnm.t;  (* propositions *)
  ns_ns : namespace Mnm.t;  (* inner namespaces *)
}

and context = private {
  ctxt_env    : env;
  ctxt_decl   : decl;
  ctxt_prev   : context option;
  ctxt_known  : decl Mid.t;
  ctxt_cloned : Sid.t Mid.t;
  ctxt_tag    : int;
}

and env

and decl = private {
  d_node : decl_node;
  d_tag  : int;
}

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

(** Declaration constructors *)

val create_ty_decl : ty_decl list -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
val create_prop_decl : prop_kind -> prop -> fmla -> decl

(* 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

(* exceptions *)

exception ConstructorExpected of lsymbol
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of tvsymbol

exception InvalidIndDecl of lsymbol * prop
exception TooSpecificIndDecl of lsymbol * prop * term
exception NonPositiveIndDecl of lsymbol * prop * lsymbol

exception IllegalConstructor of lsymbol
exception BadLogicDecl of ident
exception UnboundVars of Svs.t
exception ClashIdent of ident
exception EmptyDecl

(** Environements *)

type retrieve_theory = env -> string list -> theory Mnm.t
  (* a function of type retrieve_theory is a partial function it can
     raise Not_found if it can't retrieve this theory*)

val create_env : retrieve_theory -> env


exception TheoryNotFound of string list * string

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

val env_tag : env -> int

(** Context constructors and utilities *)

type th_inst = {
  inst_ts    : tysymbol Mts.t;
  inst_ls    : lsymbol  Mls.t;
  inst_lemma : Spr.t;
  inst_goal  : Spr.t;
}

val empty_inst : th_inst

module Context : sig

  val init_context : env -> context

  val add_decl : context -> decl -> context

  val use_export   : context -> theory -> context
  val clone_export : context -> theory -> th_inst -> context

  (* bottom-up, tail-recursive traversal functions *)
  val ctxt_fold : ('a -> decl -> 'a) -> 'a -> context -> 'a
  val ctxt_iter : (decl -> unit) -> context -> unit

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

  exception UnknownIdent of ident
  exception RedeclaredIdent of ident

  exception NonLocal of ident
  exception CannotInstantiate of ident
  exception BadInstance of ident * ident

end

(** 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

(** Theory constructors and utilities *)

type theory_uc  (* a theory under construction *)

module TheoryUC : sig

  val create_theory : env -> preid -> theory_uc
  val close_theory  : theory_uc -> theory

  val add_decl : theory_uc -> decl -> theory_uc

  val open_namespace  : theory_uc -> theory_uc
  val close_namespace : theory_uc -> bool -> string option -> theory_uc

  val use_export   : theory_uc -> theory -> theory_uc
  val clone_export : theory_uc -> theory -> th_inst -> theory_uc

  val get_namespace : theory_uc -> namespace

  exception CloseTheory
  exception NoOpenedNamespace
  exception ClashSymbol of string

end

val builtin_name : string

(*
(** Debugging *)

val print_ident : Format.formatter -> ident -> unit
val print_uc : Format.formatter -> theory_uc -> unit
val print_ctxt : Format.formatter -> context -> unit
val print_th : Format.formatter -> theory -> unit

(* Utils *)

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