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

36
37
38
type task = task_hd option

and task_hd = private {
39
  task_decl  : decl;
40
  task_prev  : task;
41
42
43
44
  task_known : decl Mid.t;
  task_tag   : int;
}

Andrei Paskevich's avatar
Andrei Paskevich committed
45
46
(* constructors *)

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

50
val add_decl : task -> decl -> task
51

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

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

56
57
58
(* bottom-up, tail-recursive traversal functions *)

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

60
61
62
63
val task_iter : (decl -> unit) -> task -> unit

val task_decls : task -> decl list

64
65
val task_goal : task -> prop

66
67
68
69
(* exceptions *)

exception UnknownIdent of ident
exception RedeclaredIdent of ident
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
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 *)

92
93
val fold   : (task_hd -> 'a -> 'a     ) -> 'a -> 'a trans
val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
94

95
96
val fold_map :
  (task_hd -> 'a * task -> ('a * task)     ) -> 'a -> task trans
97

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

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

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
110