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 {
Andrei Paskevich's avatar
Andrei Paskevich committed
31 32
  tds_set : Stdecl.t;
  tds_tag : Hashweak.tag;
33
}
34

35
val tds_equal : tdecl_set -> tdecl_set -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
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 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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

Andrei Paskevich's avatar
Andrei Paskevich committed
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} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
76

77
(** {2 declaration constructors + add_decl} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
145
exception LemmaFound
146