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

28
type clone
29 30 31

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

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;
}

45 46
(* constructors *)

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

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

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
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