]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/disambiguation/disambiguate.mli
update in delayed updating
[helm.git] / matitaB / components / disambiguation / disambiguate.mli
1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
24  *)
25
26 (** {2 Disambiguation interface} *)
27
28 type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result =
29   | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list 
30   | Disamb_failure of 
31       (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
32
33 exception NoWellTypedInterpretation of (Stdpp.location * string)
34
35 exception PathNotWellFormed
36
37 type 'a disambiguator_input = string * int * 'a
38     
39 type domain = domain_tree list
40 and domain_tree = 
41   Node of Stdpp.location list * DisambiguateTypes.domain_item * domain
42
43 type ('term,'metasenv,'subst,'graph) test_result =
44   | Ok of 'term * 'metasenv * 'subst * 'graph
45   | Ko of (Stdpp.location * string) Lazy.t
46   | Uncertain of (Stdpp.location * string) Lazy.t
47
48 exception Try_again of string Lazy.t
49
50 (*
51 val set_choose_uris_callback:
52   DisambiguateTypes.interactive_user_uri_choice_type -> unit
53
54 val set_choose_interp_callback:
55   DisambiguateTypes.interactive_interpretation_choice_type -> unit
56
57 val set_choose_disamb_callback:
58   DisambiguateTypes.interactive_ast_choice_type -> unit
59
60 (** @raise Ambiguous_input if called, default value for internal
61   * choose_uris_callback if not set otherwise with set_choose_uris_callback
62   * above *)
63 val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
64
65 (** @raise Ambiguous_input if called, default value for internal
66   * choose_interp_callback if not set otherwise with set_choose_interp_callback
67   * above *)
68 val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
69 *)
70
71 val resolve : 
72   env:'alias1 DisambiguateTypes.InterprEnv.t ->
73   universe: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
74   mk_choice:('alias1 -> 'term DisambiguateTypes.codomain_item) ->
75   DisambiguateTypes.InterprEnv.key -> 'alias1 option -> 
76    [`Num_arg of string | `Args of 'term list] -> 'term
77
78 val find_in_context: string -> string option list -> int
79 val domain_of_term: context:
80   string option list -> NotationPt.term -> domain
81 val domain_of_obj: 
82   context:string option list -> NotationPt.term NotationPt.obj -> domain
83
84 val disambiguate_thing:
85   context:'context ->
86   metasenv:'metasenv ->
87   subst:'subst ->
88   use_coercions:bool ->
89   string_context_of_context:('context -> string option list) ->
90   initial_ugraph:'ugraph ->
91   expty: 'refined_thing option ->
92   mk_implicit:(bool -> 'alias) ->
93   description_of_alias:('alias -> string) ->
94   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
95   aliases:'alias DisambiguateTypes.InterprEnv.t ->
96   universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
97   lookup_in_library:(
98     DisambiguateTypes.interactive_user_uri_choice_type ->
99     DisambiguateTypes.input_or_locate_uri_type ->
100     DisambiguateTypes.Environment.key ->
101     'alias list) ->
102   uri:'uri ->
103   pp_thing:('ast_thing -> string) ->
104   pp_term:(NotationPt.term -> string) ->
105   domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
106   interpretate_thing:(
107     context:'context ->
108     env:'alias DisambiguateTypes.InterprEnv.t ->
109     universe: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
110     uri:'uri ->
111     is_path:bool -> 
112     'ast_thing -> 
113     localization_tbl:'cichash -> 
114       'raw_thing) ->
115   refine_thing:(
116     'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
117     'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> 
118       ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
119   visit:(pp_term:(NotationPt.term -> string) ->
120          (NotationPt.term -> bool) -> 'ast_thing -> 
121         ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) -> 
122   mk_localization_tbl:(int -> 'cichash) ->
123   'ast_thing disambiguator_input ->
124   (GrafiteAst.alias_spec,'ast_thing,'metasenv,'subst,'refined_thing,'ugraph) disamb_result 
125
126 type 'ast marked_ast = 
127   (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location
128
129 val bfvisit :
130   pp_term:(NotationPt.term -> string) -> 
131   (NotationPt.term -> bool) ->
132    NotationPt.term -> (NotationPt.term marked_ast) option
133
134 val bfvisit_obj :
135   pp_term:(NotationPt.term -> string) -> 
136   (NotationPt.term -> bool) ->
137    NotationPt.term NotationPt.obj -> 
138   ((NotationPt.term NotationPt.obj) marked_ast) option