]> matita.cs.unibo.it Git - helm.git/blob - mathql/mathql_generator/mQGUtil.mli
- decompose now runs with no arguments (operates on the whole context)
[helm.git] / mathql / mathql_generator / mQGUtil.mli
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
27  *)
28
29 (* low level functions  *****************************************************)
30
31 (* these functions give the string representation used in the db  ----------*)
32
33 val string_of_position : MQGTypes.position -> string
34 val string_of_depth    : MQGTypes.depth -> string
35 val string_of_sort     : MQGTypes.sort -> string
36
37 (* these functions give the string representation used in MathQL  ----------*)
38
39 val mathql_of_position : MQGTypes.position -> string
40 val mathql_of_depth    : MQGTypes.depth -> string
41 val mathql_of_uri      : MQGTypes.uri -> string
42 val mathql_of_sort     : MQGTypes.sort -> string
43
44 val mathql_of_specs    : (string -> unit) -> MQGTypes.spec list -> unit
45
46 val position_of_mathql : string -> MQGTypes.position
47 val depth_of_mathql    : string -> MQGTypes.depth
48 val uri_of_mathql      : string -> MQGTypes.uri
49 val sort_of_mathql     : string -> MQGTypes.sort
50
51 (* high level functions  ****************************************************)
52
53 (* these functions give the textual representation used by umans  ----------*)
54
55 val text_of_position : MQGTypes.full_position -> string
56 val text_of_depth    : MQGTypes.full_position -> string -> string
57 val text_of_sort     : MQGTypes.sort -> string
58
59 (* these functions classify the positions  ---------------------------------*)
60
61 val is_main_position : MQGTypes.full_position -> bool
62 val is_conclusion    : MQGTypes.full_position -> bool
63
64 (* these function apply changes to positions  ------------------------------*)
65
66 val set_full_position : MQGTypes.full_position -> MQGTypes.optional_depth ->
67                         MQGTypes.full_position
68 val set_main_position : MQGTypes.main_position -> MQGTypes.optional_depth ->
69                         MQGTypes.main_position