task.mli 4.19 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9
(*                                                                  *)
(*  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.                           *)
(********************************************************************)
10

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

13 14 15 16
open Ident
open Ty
open Term
open Decl
17
open Theory
18

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

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

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

31
type clone_map = tdecl_set Mid.t
32
type meta_map = tdecl_set Mmeta.t
33 34

(** Task *)
35

36 37 38
type task = task_hd option

and task_hd = private {
39 40 41 42 43
  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
44
  task_tag   : Weakhtbl.tag; (* unique magical tag *)
45 46
}

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

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

53
val task_known : task -> known_map
54
val task_clone : task -> clone_map
55
val task_meta  : task -> meta_map
56

57 58
val find_clone_tds : task -> theory -> tdecl_set
val find_meta_tds  : task -> meta -> tdecl_set
59

60
(** {2 constructors} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
61

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

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

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

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

78
(** {2 utilities} *)
79

80
val split_theory : theory -> Spr.t option -> task -> task list
81 82 83 84 85 86 87 88 89 90 91 92 93 94
  (** [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
95
  (** takes the result of [used_symbols] and returns
96 97
      the list of declarations that are not imported
      with those theories or derived thereof *)
98

99
(** {2 bottom-up, tail-recursive traversal functions} *)
100

101 102
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
103

104
val task_tdecls : task -> tdecl list
105
val task_decls  : task -> decl list
106 107

val task_goal  : task -> prsymbol
108
val task_goal_fmla  : task -> term
MARCHE Claude's avatar
MARCHE Claude committed
109

François Bobot's avatar
François Bobot committed
110
val task_separate_goal : task -> tdecl * task
MARCHE Claude's avatar
MARCHE Claude committed
111 112 113
(** [task_separate_goal t] returns a pair [(g,t')] where [g] is the
    goal of the task [t] and [t'] is the rest.  raises [GoalNotFound]
    if task [t] has no goal *)
114

115
(** {2 selectors} *)
116

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

120 121
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
122

123 124 125 126
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
127

128 129
(* exceptions *)

130 131 132
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta

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