decl.mli 4.91 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

MARCHE Claude's avatar
MARCHE Claude committed
20 21
(** Logic Declarations *)

22 23 24 25
open Ident
open Ty
open Term

Simon Cruanes's avatar
Simon Cruanes committed
26
(** {2 Type declaration} *)
27 28 29 30 31 32 33

type ty_def =
  | Tabstract
  | Talgebraic of lsymbol list

type ty_decl = tysymbol * ty_def

MARCHE Claude's avatar
MARCHE Claude committed
34
(** {2 Logic symbols declaration} *)
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49

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

Simon Cruanes's avatar
Simon Cruanes committed
50
(** {2 Inductive predicate declaration} *)
51

52
type prsymbol = private {
53 54
  pr_name : ident;
}
55

56 57 58
module Spr : Set.S with type elt = prsymbol
module Mpr : Map.S with type key = prsymbol
module Hpr : Hashtbl.S with type key = prsymbol
59
module Wpr : Hashweak.S with type key = prsymbol
60

61
val create_prsymbol : preid -> prsymbol
62

63 64
val pr_equal : prsymbol -> prsymbol -> bool

Andrei Paskevich's avatar
Andrei Paskevich committed
65 66
val pr_hash : prsymbol -> int

67
type ind_decl = lsymbol * (prsymbol * fmla) list
68

69 70 71
(* Proposition declaration *)

type prop_kind =
72 73 74 75
  | Plemma    (* prove, use as a premise *)
  | Paxiom    (* do not prove, use as a premise *)
  | Pgoal     (* prove, do not use as a premise *)
  | Pskip     (* do not prove, do not use as a premise *)
76

77
type prop_decl = prop_kind * prsymbol * fmla
78

Simon Cruanes's avatar
Simon Cruanes committed
79
(** {2 Declaration type} *)
80 81 82

type decl = private {
  d_node : decl_node;
83 84
  d_syms : Sid.t;         (* idents used in declaration *)
  d_news : Sid.t;         (* idents introduced in declaration *)
Andrei Paskevich's avatar
Andrei Paskevich committed
85
  d_tag  : Hashweak.tag;  (* unique magical tag *)
86 87 88 89 90 91 92 93
}

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

Andrei Paskevich's avatar
Andrei Paskevich committed
94 95
module Sdecl : Set.S with type elt = decl
module Mdecl : Map.S with type key = decl
Andrei Paskevich's avatar
Andrei Paskevich committed
96
module Wdecl : Hashweak.S with type key = decl
Andrei Paskevich's avatar
Andrei Paskevich committed
97

98
val d_equal : decl -> decl -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
99
val d_hash : decl -> int
100

Simon Cruanes's avatar
Simon Cruanes committed
101
(** {2 Declaration constructors} *)
102 103 104 105

val create_ty_decl : ty_decl list -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
106
val create_prop_decl : prop_kind -> prsymbol -> fmla -> decl
107 108 109 110 111

(* exceptions *)

exception IllegalTypeAlias of tysymbol

112 113 114
exception InvalidIndDecl of lsymbol * prsymbol
exception TooSpecificIndDecl of lsymbol * prsymbol * term
exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol
115

116
exception BadLogicDecl of ident * ident
117
exception UnboundVar of vsymbol
118
exception ClashIdent of ident
119

120
exception EmptyDecl
121 122
exception EmptyAlgDecl of tysymbol
exception EmptyIndDecl of lsymbol
123

Simon Cruanes's avatar
Simon Cruanes committed
124
(** {2 Utilities} *)
125 126

val decl_map : (term -> term) -> (fmla -> fmla) -> decl -> decl
127
val decl_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> decl -> 'a
128

129 130 131 132
val decl_map_fold :
  ('a -> term -> 'a * term) -> ('a -> fmla -> 'a * fmla) ->
      'a -> decl -> 'a * decl

Simon Cruanes's avatar
Simon Cruanes committed
133
(** {2 Known identifiers} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
134

135
type known_map = decl Mid.t
Andrei Paskevich's avatar
Andrei Paskevich committed
136

137
val known_id : known_map -> ident -> unit
138 139
val known_add_decl : known_map -> decl -> known_map
val merge_known : known_map -> known_map -> known_map
Andrei Paskevich's avatar
Andrei Paskevich committed
140 141 142 143

exception KnownIdent of ident
exception UnknownIdent of ident
exception RedeclaredIdent of ident
144 145 146
exception NonExhaustiveExpr of (pattern list * expr)

val find_constructors : known_map -> tysymbol -> lsymbol list
147
val find_inductive_cases : known_map -> lsymbol -> (prsymbol * fmla) list
148
val find_prop : known_map -> prsymbol -> fmla
149
val find_prop_decl : known_map -> prsymbol -> prop_kind * fmla
Andrei Paskevich's avatar
Andrei Paskevich committed
150