task.mli 2.17 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
(**************************************************************************)
(*                                                                        *)
(*  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
24
open Theory
25 26 27

(** Cloning map *)

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30 31
type clone = private {
  cl_map : clone_map;
  cl_tag : int
}
32 33 34 35 36

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

(** Task *)

37 38 39
type task = task_hd option

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

46 47
(* constructors *)

48
val add_decl : task -> decl -> task
49

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

52 53 54
(* bottom-up, tail-recursive traversal functions *)

val task_fold : ('a -> decl -> 'a) -> 'a -> task -> 'a
55

56 57 58 59
val task_iter : (decl -> unit) -> task -> unit

val task_decls : task -> decl list

60 61
val task_goal : task -> prop

62 63 64 65
(* exceptions *)

exception UnknownIdent of ident
exception RedeclaredIdent of ident
66
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
67
exception GoalFound
Andrei Paskevich's avatar
Andrei Paskevich committed
68
exception LemmaFound
69