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

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

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

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

25
val tds_equal : tdecl_set -> tdecl_set -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
26
val tds_hash : tdecl_set -> int
27
val tds_compare : tdecl_set -> tdecl_set -> int
28
val tds_empty : tdecl_set
29

30 31
val mk_tds : Stdecl.t -> tdecl_set

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

(** Task *)
36

37 38 39
type task = task_hd option

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

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

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

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

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

61
(** {2 constructors} *)
62

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

66 67
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
68
val add_meta : task -> meta -> meta_arg list -> task
69

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

72 73 74
val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task
val add_param_decl : task -> lsymbol -> task
75
val add_logic_decl : task -> logic_decl list -> task
76
val add_ind_decl : task -> ind_sign -> ind_decl list -> task
77
val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
78

79
(** {2 utilities} *)
80

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

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

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

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

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

111
val task_separate_goal : task -> tdecl * task
MARCHE Claude's avatar
MARCHE Claude committed
112 113 114
(** [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 *)
115

116
(** {2 selectors} *)
117

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

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

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

129 130
(* exceptions *)

131 132 133
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta

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