task.mli 3.98 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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 81
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
val add_prop_decl : task -> prop_kind -> prsymbol -> fmla -> task
82

83
(** {2 utilities} *)
84

85
val split_theory : theory -> Spr.t option -> task -> task list
86 87
  (** [split_theory th s] returns the tasks of [th] which end by one
      of [s]. They are in the opposite order than in the theory *)
88

89
(** {2 bottom-up, tail-recursive traversal functions} *)
90

91 92
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
93

94
val task_tdecls : task -> tdecl list
95
val task_decls  : task -> decl list
96 97 98

val task_goal  : task -> prsymbol

99
(** {2 selectors} *)
100

101 102
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
103

104 105
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
106

107 108 109 110
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
111

112 113
(* exceptions *)

114 115 116
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta

117
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
118
exception GoalFound
119
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
120
exception LemmaFound
121