Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

task.mli 2.31 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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
(**************************************************************************)
(*                                                                        *)
(*  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

(** Environment *)

type env

type retrieve_theory = env -> string list -> theory Mnm.t

val create_env : retrieve_theory -> env

val find_theory : env -> string list -> string -> theory

val env_tag : env -> int

exception TheoryNotFound of string list * string

(** Cloning map *)

type clone = private {
  cl_map : Sid.t Mid.t;
  cl_tag : int
}

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

(** Task *)

type task = private {
  task_decl  : decl;
  task_prev  : task option;
  task_known : decl Mid.t;
  task_clone : clone;
  task_env   : env;
  task_tag   : int;
}

val add_decl : task -> decl -> task

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

val task_fold : ('a -> decl -> 'a) -> 'a -> task -> 'a
val task_iter : (decl -> unit) -> task -> unit

(* top-down list of declarations *)
val task_decls : task -> decl list

(* exceptions *)

exception UnknownIdent of ident
exception RedeclaredIdent of ident