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.19 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

open Ident
open Ty
open Term
open Decl
open Theory2

(** Cloning map *)

Andrei Paskevich's avatar
Andrei Paskevich committed
28
type clone
29
30
31

val cloned_from : clone -> ident -> ident -> bool

Andrei Paskevich's avatar
Andrei Paskevich committed
32
33
val clone_tag : clone -> int

34
35
36
37
38
39
40
41
42
(** Task *)

type task = private {
  task_decl  : decl;
  task_prev  : task option;
  task_known : decl Mid.t;
  task_tag   : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
43
44
(* constructors *)

Francois Bobot's avatar
Francois Bobot committed
45
46
(* val init_task : task *)
(* val add_decl : task -> decl -> task *)
Andrei Paskevich's avatar
Andrei Paskevich committed
47

Francois Bobot's avatar
Francois Bobot committed
48
val add_decl : task option -> decl -> task
49

Andrei Paskevich's avatar
Andrei Paskevich committed
50
51
52
53
val split_theory : theory -> Spr.t -> (task * clone) list

val split_theory_full : theory -> (task * clone) list

54
55
56
(* bottom-up, tail-recursive traversal functions *)

val task_fold : ('a -> decl -> 'a) -> 'a -> task -> 'a
Andrei Paskevich's avatar
Andrei Paskevich committed
57

58
59
60
61
val task_iter : (decl -> unit) -> task -> unit

val task_decls : task -> decl list

62
63
val task_goal : task -> prop

64
65
66
67
(* exceptions *)

exception UnknownIdent of ident
exception RedeclaredIdent of ident
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
exception GoalNotFound

(** Task transformation *)

module Tr : sig

type 'a trans
type 'a tlist = 'a list trans

val identity   : task trans
val identity_l : task tlist

val apply : 'a trans -> (task -> 'a)
val store : (task -> 'a) -> 'a trans

val singleton : 'a trans -> 'a tlist

val compose   : task trans -> 'a trans -> 'a trans
val compose_l : task tlist -> 'a tlist -> 'a tlist

(* val conv_res : 'a trans -> ('a -> 'b) -> 'b trans *)

val fold   : (task -> 'a -> 'a     ) -> 'a -> 'a trans
val fold_l : (task -> 'a -> 'a list) -> 'a -> 'a tlist

Francois Bobot's avatar
Francois Bobot committed
93
94
val fold_map : 
  (task -> 'a * task option -> ('a * task)     ) -> 'a -> task trans
95

Francois Bobot's avatar
Francois Bobot committed
96
97
98
99
100
val fold_map_l : 
  (task -> 'a * task option -> ('a * task) list) -> 'a -> task tlist

val map   : (task -> task option -> task     ) -> task trans
val map_l : (task -> task option -> task list) -> task tlist
101
102
103
104
105
106
107

val decl   : (decl -> decl list     ) -> task trans
val decl_l : (decl -> decl list list) -> task tlist

val expr : (term -> term) -> (fmla -> fmla) -> task trans

end
108