MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

task.mli 3.5 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

(** Task *)

29
30
31
type clone_map = Stdecl.t Mid.t
type meta_map = Stdecl.t Mstr.t

32
33
34
type task = task_hd option

and task_hd = private {
35
36
37
38
  task_decl  : tdecl;       (* last declaration *)
  task_prev  : task;        (* context *)
  task_known : known_map;   (* known identifiers *)
  task_clone : clone_map;   (* cloning history *)
39
  task_meta  : meta_map;    (* meta properties *)
40
  task_tag   : int;         (* unique task tag *)
41
42
}

Andrei Paskevich's avatar
Andrei Paskevich committed
43
val task_equal : task -> task -> bool
44
val task_hd_equal : task_hd -> task_hd -> bool
45

46
val task_known : task -> known_map
47
val task_clone : task -> clone_map
48
val task_meta  : task -> meta_map
49

50
51
52
val find_clone : task -> theory -> Stdecl.t
val find_meta : task -> string -> Stdecl.t

53
(** {2 constructors} *)
Andrei Paskevich's avatar
Andrei Paskevich committed
54

55
val add_decl : task -> decl -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
56
val add_tdecl : task -> tdecl -> task
57

58
59
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
60
val add_meta : task -> string -> meta_arg list -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
61

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

64
65
66
67
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
68

69
70
71
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
72

73
(** {2 utilities} *)
74

75
val split_theory : theory -> Spr.t option -> task list
76
77
  (** [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 *)
78

79
(** {2 bottom-up, tail-recursive traversal functions} *)
80

81
82
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
83

84
val task_tdecls : task -> tdecl list
85
val task_decls  : task -> decl list
86
87
88

val task_goal  : task -> prsymbol

89
90
91
92
93
94
(* TO BE REMOVED *)

val old_task_clone : task -> Sid.t Mid.t
val old_task_use   : task -> theory Mid.t
val last_clone     : task -> task
val last_use       : task -> task
95

96
97
(* exceptions *)

98
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
99
exception GoalFound
100
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
101
exception LemmaFound
102