task.mli 4.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

MARCHE Claude's avatar
MARCHE Claude committed
12 13
(** Proof Tasks, Cloning and Meta History *)

14
open Util
15 16 17 18
open Ident
open Ty
open Term
open Decl
19
open Theory
20

21
type tdecl_set = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
22
  tds_set : Stdecl.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
23
  tds_tag : Weakhtbl.tag;
24
}
25

26
val tds_equal : tdecl_set -> tdecl_set -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
27
val tds_hash : tdecl_set -> int
François Bobot's avatar
François Bobot committed
28
val tds_compare : tdecl_set -> tdecl_set -> int
29
val tds_empty : tdecl_set
30

François Bobot's avatar
François Bobot committed
31 32
val mk_tds : Stdecl.t -> tdecl_set

33
type clone_map = tdecl_set Mid.t
34
type meta_map = tdecl_set Mmeta.t
35 36

(** Task *)
37

38 39 40
type task = task_hd option

and task_hd = private {
41 42 43 44 45
  task_decl  : tdecl;        (* last declaration *)
  task_prev  : task;         (* context *)
  task_known : known_map;    (* known identifiers *)
  task_clone : clone_map;    (* cloning history *)
  task_meta  : meta_map;     (* meta properties *)
Andrei Paskevich's avatar
Andrei Paskevich committed
46
  task_tag   : Weakhtbl.tag; (* unique magical tag *)
47 48
}

Andrei Paskevich's avatar
Andrei Paskevich committed
49
val task_equal : task -> task -> bool
50
val task_hd_equal : task_hd -> task_hd -> bool
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52 53 54
val task_hash : task -> int
val task_hd_hash : task_hd -> int

55
val task_known : task -> known_map
56
val task_clone : task -> clone_map
57
val task_meta  : task -> meta_map
58

59 60
val find_clone_tds : task -> theory -> tdecl_set
val find_meta_tds  : task -> meta -> tdecl_set
61

62
(** {2 constructors} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
63

64
val add_decl : task -> decl -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
65
val add_tdecl : task -> tdecl -> task
66

67 68
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
69
val add_meta : task -> meta -> meta_arg list -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
70

71
(** {2 declaration constructors + add_decl} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
72

73 74 75
val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task
val add_param_decl : task -> lsymbol -> task
76
val add_logic_decl : task -> logic_decl list -> task
77
val add_ind_decl : task -> ind_sign -> ind_decl list -> task
78
val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
79

80
(** {2 utilities} *)
81

82
val split_theory : theory -> Spr.t option -> task -> task list
83 84 85 86 87 88 89 90 91 92 93 94 95 96
  (** [split_theory th s t] returns the tasks of [th] added to [t]
      that end by one of [s]. They are in the opposite order than
      in the theory *)

(** {2 realization utilities} *)

val used_theories : task -> theory Mid.t
  (** returns a map from theory names to theories themselves *)

val used_symbols : theory Mid.t -> theory Mid.t
  (** takes the result of [used_theories] and returns
      a map from symbol names to their theories of origin *)

val local_decls : task -> theory Mid.t -> decl list
97
  (** takes the result of [used_symbols] and returns
98 99
      the list of declarations that are not imported
      with those theories or derived thereof *)
100

101
(** {2 bottom-up, tail-recursive traversal functions} *)
102

103 104
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
105

106
val task_tdecls : task -> tdecl list
107
val task_decls  : task -> decl list
108 109

val task_goal  : task -> prsymbol
110
val task_goal_fmla  : task -> term
François Bobot's avatar
François Bobot committed
111
val task_separate_goal : task -> tdecl * task
112

113
(** {2 selectors} *)
114

115 116
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
117

118 119
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
120

121 122 123 124
val on_tagged_ty : meta -> task -> Sty.t
val on_tagged_ts : meta -> task -> Sts.t
val on_tagged_ls : meta -> task -> Sls.t
val on_tagged_pr : meta -> task -> Spr.t
125

126 127
(* exceptions *)

128 129 130
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta

131
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
132
exception GoalFound
133
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
134
exception LemmaFound
135