task.mli 4.84 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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
(** Proof Tasks, Cloning and Meta History *)

22
open Util
23 24 25 26
open Ident
open Ty
open Term
open Decl
27
open Theory
28

29
type tdecl_set = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
30 31
  tds_set : Stdecl.t;
  tds_tag : Hashweak.tag;
32
}
33

34
val tds_equal : tdecl_set -> tdecl_set -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
35
val tds_hash : tdecl_set -> int
36
val tds_empty : tdecl_set
37

38
type clone_map = tdecl_set Mid.t
39
type meta_map = tdecl_set Mmeta.t
40 41

(** Task *)
42

43 44 45
type task = task_hd option

and task_hd = private {
46 47 48 49 50
  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
51
  task_tag   : Hashweak.tag; (* unique magical tag *)
52 53
}

Andrei Paskevich's avatar
Andrei Paskevich committed
54
val task_equal : task -> task -> bool
55
val task_hd_equal : task_hd -> task_hd -> bool
56

Andrei Paskevich's avatar
Andrei Paskevich committed
57 58 59
val task_hash : task -> int
val task_hd_hash : task_hd -> int

60
val task_known : task -> known_map
61
val task_clone : task -> clone_map
62
val task_meta  : task -> meta_map
63

64 65
val find_clone_tds : task -> theory -> tdecl_set
val find_meta_tds  : task -> meta -> tdecl_set
66

67
(** {2 constructors} *)
68

69
val add_decl : task -> decl -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
70
val add_tdecl : task -> tdecl -> task
71

72 73
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
74
val add_meta : task -> meta -> meta_arg list -> task
75

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

78 79 80
val add_ty_decl : task -> ty_decl list -> task
val add_logic_decl : task -> logic_decl list -> task
val add_ind_decl : task -> ind_decl list -> task
81
val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
82

83
(** {2 utilities} *)
84

85
val split_theory : theory -> Spr.t option -> task -> task list
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  (** [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 *)

val bisect : (task -> bool) -> task -> task
   (** [bisect test task] return a task included in [task] which is at
       the limit of truthness of the function test. The returned task is
       included in [task] and if any declarations are removed from it the
       task doesn't verify test anymore *)

(** {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
  (** takes the result of [used_symbols] adn returns
      the list of declarations that are not imported
      with those theories or derived thereof *)
109

110
(** {2 bottom-up, tail-recursive traversal functions} *)
111

112 113
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
114

115
val task_tdecls : task -> tdecl list
116
val task_decls  : task -> decl list
117 118

val task_goal  : task -> prsymbol
119
val task_goal_fmla  : task -> term
120

121
(** {2 selectors} *)
122

123 124
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
125

126 127
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
128

129 130 131 132
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
133

134 135
(* exceptions *)

136 137 138
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta

139
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
140
exception GoalFound
141
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
142
exception LemmaFound
143