]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/bin/roles/rolesTypes.ml
update in binaries for λδ
[helm.git] / matita / matita / contribs / lambdadelta / bin / roles / rolesTypes.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic
3     ||A||  Library of Mathematics, developed at the Computer Science
4     ||T||  Department, University of Bologna, Italy.
5     ||I||
6     ||T||  HELM is free software; you can redistribute it and/or
7     ||A||  modify it under the terms of the GNU General Public License
8     \   /  version 2 or (at your option) any later version.
9      \ /   This software is distributed as is, NO WARRANTY.
10       V_______________________________________________________________ *)
11
12 type version = int list
13
14 type name = string list
15
16 type names = (bool*name) list
17
18 type obj = version * name
19
20 type objs = (bool*obj) list
21
22 type role = {
23   mutable v: version;
24   mutable o: objs;
25   mutable n: names;
26 }
27
28 type roles = (bool*role) list
29
30 type status = {
31   mutable r: roles;
32   mutable s: version;
33   mutable t: objs;
34   mutable w: names;
35 }
36
37 type pointer = int list
38
39 type error = EWrongExt of string
40            | EStage of version
41            | ENoStage
42            | EWaiting
43            | ENameClash of name
44            | EObjClash of obj
45            | ERoleClash of role
46            | ENoEntry
47            | EWrongSelect
48            | EWrongVersion
49            | ETops
50            | EWrongRequest of string * string
51
52 exception Error of error