Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Util
21
22
23
24
open Ident
open Ty
open Term
open Decl
25
open Theory
26

27
28
29
(** Clone and meta history *)

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

35
36
val tds_equal : tdecl_set -> tdecl_set -> bool

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

(** Task *)
41

42
43
44
type task = task_hd option

and task_hd = private {
45
46
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 *)
  task_weak  : Hashweak.key; (* weak hashtable key *)
  task_tag   : int;          (* unique task 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

57
val task_known : task -> known_map
58
val task_clone : task -> clone_map
59
val task_meta  : task -> meta_map
60

61
val find_clone : task -> theory -> tdecl_set
62
val find_meta  : task -> meta -> tdecl_set
63

64
(** {2 constructors} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
65

66
val add_decl : task -> decl -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
67
val add_tdecl : task -> tdecl -> task
68

69
70
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
71
val add_meta : task -> meta -> meta_arg list -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
72

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

75
76
77
78
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
79

80
81
82
val add_ty_decls : task -> ty_decl list -> task
val add_logic_decls : task -> logic_decl list -> task
val add_ind_decls : task -> ind_decl list -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
83

84
(** {2 utilities} *)
85

86
val split_theory : theory -> Spr.t option -> task -> task list
87
88
  (** [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 *)
89

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

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

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

val task_goal  : task -> prsymbol

100
(* special selector for metaproperties of a single ident *)
101

102
exception NotTaggingMeta of meta
103

104
105
106
val find_tagged_ts : meta -> tdecl_set -> Sts.t -> Sts.t
val find_tagged_ls : meta -> tdecl_set -> Sls.t -> Sls.t
val find_tagged_pr : meta -> tdecl_set -> Spr.t -> Spr.t
107

108
109
(* special selector for exclusive metaproperties *)

110
exception NotExclusiveMeta of meta
111

112
val get_meta_excl : meta -> tdecl_set -> meta_arg list option
113

114
115
(* exceptions *)

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