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

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

30
type tdecl_set = private {
31 32
  tds_set : Stdecl.t;
  tds_tag : Hashweak.tag;
33
}
34

35
val tds_equal : tdecl_set -> tdecl_set -> bool
36
val tds_hash : tdecl_set -> int
37
val tds_empty : tdecl_set
38

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

(** Task *)
43

44 45 46
type task = task_hd option

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

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

58 59 60
val task_hash : task -> int
val task_hd_hash : task_hd -> int

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

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

68
(** {2 constructors} *)
69

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

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

77
(** {2 declaration constructors + add_decl} *)
78

79 80 81
val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task
val add_param_decl : task -> lsymbol -> task
82
val add_logic_decl : task -> logic_decl list -> task
83
val add_ind_decl : task -> ind_sign -> ind_decl list -> task
84
val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
85

86
(** {2 utilities} *)
87

88
val split_theory : theory -> Spr.t option -> task -> task list
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
109
  (** takes the result of [used_symbols] and returns
110 111
      the list of declarations that are not imported
      with those theories or derived thereof *)
112

113
(** {2 bottom-up, tail-recursive traversal functions} *)
114

115 116
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
117

118
val task_tdecls : task -> tdecl list
119
val task_decls  : task -> decl list
120 121

val task_goal  : task -> prsymbol
122
val task_goal_fmla  : task -> term
123

124
(** {2 selectors} *)
125

126 127
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
128

129 130
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
131

132 133 134 135
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
136

137 138
(* exceptions *)

139 140 141
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta

142
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
143
exception GoalFound
144
exception SkipFound
145
exception LemmaFound
146