]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_disambiguation/cicDisambiguate.mli
added config.ac to the tarball for debian packages
[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.mli
1 (*
2  *
3 Copyright (C) 1999-2006, HELM Team.
4
5 This file is part of HELM, an Hypertextual, Electronic
6 Library of Mathematics, developed at the Computer Science
7 Department, University of Bologna, Italy.
8
9 HELM is free software; you can redistribute it and/or
10 modify it under the terms of the GNU General Public License
11 as published by the Free Software Foundation; either version 2
12 of the License, or (at your option) any later version.
13
14 HELM is distributed in the hope that it will be useful,
15 but WITHOUT ANY WARRANTY; without even the implied warranty of
16 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
17 GNU General Public License for more details.
18
19 You should have received a copy of the GNU General Public License
20 along with this program; if not, write to the Free Software
21 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
22 02110-1301 USA.
23
24 For details, see the HELM web site: http://helm.cs.unibo.it/
25 *)
26
27 val interpretate_path :
28   context:Cic.name list -> CicNotationPt.term -> Cic.term
29
30 val disambiguate_term :
31   context:Cic.context ->
32   metasenv:Cic.metasenv -> 
33   subst:Cic.substitution ->
34   expty:Cic.term option ->
35   ?initial_ugraph:CicUniv.universe_graph -> 
36   mk_implicit:(bool -> 'alias) ->
37   description_of_alias:('alias -> string) ->
38   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
39   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
40   aliases:'alias DisambiguateTypes.Environment.t ->
41   universe:'alias list DisambiguateTypes.Environment.t option ->
42   lookup_in_library:(
43     DisambiguateTypes.interactive_user_uri_choice_type ->
44     DisambiguateTypes.input_or_locate_uri_type ->
45     DisambiguateTypes.Environment.key ->
46     'alias list) ->
47   CicNotationPt.term Disambiguate.disambiguator_input ->
48   ((DisambiguateTypes.domain_item * 'alias) list *
49    Cic.metasenv *                  
50    Cic.substitution *
51    Cic.term*
52    CicUniv.universe_graph) list * 
53   bool
54
55 val disambiguate_obj :
56   mk_implicit:(bool -> 'alias) ->
57   description_of_alias:('alias -> string) ->
58   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
59   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
60   aliases:'alias DisambiguateTypes.Environment.t ->
61   universe:'alias list DisambiguateTypes.Environment.t option ->
62   lookup_in_library:(
63     DisambiguateTypes.interactive_user_uri_choice_type ->
64     DisambiguateTypes.input_or_locate_uri_type ->
65     DisambiguateTypes.Environment.key ->
66     'alias list) ->
67   uri:UriManager.uri option ->     (* required only for inductive types *)
68   CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
69   ((DisambiguateTypes.domain_item * 'alias) list *
70    Cic.metasenv *   
71    Cic.substitution *
72    Cic.obj *
73    CicUniv.universe_graph) list * 
74   bool