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

43 44
(* constructors *)

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

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

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