task.mli 3.02 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

(** Task *)

28 29 30
type task = task_hd option

and task_hd = private {
31 32 33 34 35 36
  task_decl  : tdecl;       (* last declaration *)
  task_prev  : task;        (* context *)
  task_known : known_map;   (* known identifiers *)
  task_clone : clone_map;   (* cloning history *)
  task_used  : use_map;     (* referenced theories *)
  task_tag   : int;         (* unique task tag *)
37 38
}

39 40 41 42 43
and tdecl = private
  | Decl  of decl
  | Use   of theory
  | Clone of theory * (ident * ident) list

44
val task_known : task -> known_map
45
val task_clone : task -> clone_map
46
val task_used  : task -> use_map
47

48 49
(* constructors *)

50
val add_tdecl : task -> tdecl -> task
51
val add_decl : task -> decl -> task
52

53 54
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
55

56
(* declaration constructors + add_decl *)
Andrei Paskevich's avatar
Andrei Paskevich committed
57

58 59 60 61
val add_ty_decl : task -> ty_decl list -> task
val add_logic_decl : task -> logic_decl list -> task
val add_ind_decl : task -> ind_decl list -> task
val add_prop_decl : task -> prop_kind -> prsymbol -> fmla -> task
62

63 64 65
val add_ty_decls : task -> ty_decl list -> task
val add_logic_decls : task -> logic_decl list -> task
val add_ind_decls : task -> ind_decl list -> task
66

67
(* utilities *)
68

69 70 71
val split_theory : theory -> Spr.t option -> task list

(* bottom-up, tail-recursive traversal functions *)
72

73 74 75 76
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
val task_tdecls : task -> tdecl list
val task_decls : task -> decl list
77 78 79 80 81 82

val task_goal  : task -> prsymbol

val last_clone : task -> task
val last_use   : task -> task

83 84
(* exceptions *)

85
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
86
exception GoalFound
Andrei Paskevich's avatar
Andrei Paskevich committed
87
exception LemmaFound
88