]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/grafite_parser/grafiteDisambiguate.ml
Implicit annotationas are now printed
[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml
1 (*
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 (* $Id$ *)
27
28 exception BaseUriNotSetYet
29
30 type tactic = 
31  (CicNotationPt.term, CicNotationPt.term, 
32   CicNotationPt.term GrafiteAst.reduction, string) 
33    GrafiteAst.tactic
34    
35 type lazy_tactic = 
36   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
37     GrafiteAst.tactic
38
39 let singleton msg = function
40   | [x], _ -> x
41   | l, _   ->
42       let debug = 
43          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
44          msg (List.length l)
45       in
46       HLog.debug debug; assert false
47
48   (** @param term not meaningful when context is given *)
49 let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
50   let lexicon_status = !lexicon_status_ref in
51   let (diff, metasenv, cic, _) =
52     singleton "first"
53       (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
54         ~aliases:lexicon_status.LexiconEngine.aliases
55         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
56         ~context ~metasenv (text,prefix_len,term))
57   in
58   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
59   lexicon_status_ref := lexicon_status;
60   metasenv,cic
61 ;;
62
63   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
64    * rationale: lazy_term will be invoked in different context to obtain a term,
65    * each invocation will disambiguate the term and can add aliases. Once all
66    * disambiguations have been performed, the first returned function can be
67    * used to obtain the resulting aliases *)
68 let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
69   (fun context metasenv ugraph ->
70     let lexicon_status = !lexicon_status_ref in
71     let (diff, metasenv, cic, ugraph) =
72       singleton "second"
73         (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
74           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
75           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
76           ~context ~metasenv
77           (text,prefix_len,term)) in
78     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
79     lexicon_status_ref := lexicon_status;
80     cic, metasenv, ugraph)
81 ;;
82
83 let disambiguate_pattern 
84   text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path) 
85 =
86   let interp path = Disambiguate.interpretate_path [] path in
87   let goal_path = HExtlib.map_option interp goal_path in
88   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
89   let wanted =
90    match wanted with
91       None -> None
92     | Some wanted ->
93        let wanted = 
94          disambiguate_lazy_term text prefix_len lexicon_status_ref wanted 
95        in
96        Some wanted
97   in
98   (wanted, hyp_paths, goal_path)
99 ;;
100
101 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
102   | `Unfold (Some t) ->
103       let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
104       `Unfold (Some t)
105   | `Normalize
106   | `Simpl
107   | `Unfold None
108   | `Whd as kind -> kind
109 ;;
110
111 let disambiguate_auto_params 
112   disambiguate_term metasenv context (terms, params) 
113 =
114     let metasenv, terms = 
115       List.fold_right 
116        (fun t (metasenv, terms) ->
117          let metasenv,t = disambiguate_term context metasenv t in
118          metasenv,t::terms) terms (metasenv, [])
119     in
120     metasenv, (terms, params)
121 ;;
122
123 let disambiguate_just disambiguate_term context metasenv =
124  function
125     `Term t ->
126       let metasenv,t = disambiguate_term context metasenv t in
127        metasenv, `Term t
128   | `Auto params ->
129       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
130        context params
131       in
132        metasenv, `Auto params
133 ;;
134       
135 let rec disambiguate_tactic 
136   lexicon_status_ref context metasenv (text,prefix_len,tactic) 
137 =
138   let disambiguate_term = 
139     disambiguate_term text prefix_len lexicon_status_ref in
140   let disambiguate_pattern = 
141     disambiguate_pattern text prefix_len lexicon_status_ref in
142   let disambiguate_reduction_kind = 
143     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
144   let disambiguate_lazy_term = 
145     disambiguate_lazy_term text prefix_len lexicon_status_ref in
146   let disambiguate_tactic metasenv tac =
147    disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac)
148   in
149   let disambiguate_auto_params m p = 
150     disambiguate_auto_params disambiguate_term m context p
151   in
152    match tactic with
153     (* Higher  order tactics *)
154     | GrafiteAst.Progress (loc,tac) ->
155         let metasenv,tac = disambiguate_tactic metasenv tac in
156         metasenv,GrafiteAst.Progress (loc,tac)
157     | GrafiteAst.Solve (loc,tacl) ->
158         let metasenv,tacl =
159          List.fold_right
160           (fun tac (metasenv,tacl) ->
161             let metasenv,tac = disambiguate_tactic metasenv tac in
162              metasenv,tac::tacl
163           ) tacl (metasenv,[])
164         in
165          metasenv,GrafiteAst.Solve (loc,tacl)
166     | GrafiteAst.Try (loc,tac) ->
167         let metasenv,tac = disambiguate_tactic metasenv tac in
168         metasenv,GrafiteAst.Try (loc,tac)
169     | GrafiteAst.First (loc,tacl) ->
170         let metasenv,tacl =
171          List.fold_right
172           (fun tac (metasenv,tacl) ->
173             let metasenv,tac = disambiguate_tactic metasenv tac in
174              metasenv,tac::tacl
175           ) tacl (metasenv,[])
176         in
177          metasenv,GrafiteAst.First (loc,tacl)
178     | GrafiteAst.Seq (loc,tacl) ->
179         let metasenv,tacl =
180          List.fold_right
181           (fun tac (metasenv,tacl) ->
182             let metasenv,tac = disambiguate_tactic metasenv tac in
183              metasenv,tac::tacl
184           ) tacl (metasenv,[])
185         in
186          metasenv,GrafiteAst.Seq (loc,tacl)
187     | GrafiteAst.Repeat (loc,tac) ->
188         let metasenv,tac = disambiguate_tactic metasenv tac in
189         metasenv,GrafiteAst.Repeat (loc,tac)
190     | GrafiteAst.Do (loc,n,tac) ->
191         let metasenv,tac = disambiguate_tactic metasenv tac in
192         metasenv,GrafiteAst.Do (loc,n,tac)
193     | GrafiteAst.Then (loc,tac,tacl) ->
194         let metasenv,tac = disambiguate_tactic metasenv tac in
195         let metasenv,tacl =
196          List.fold_right
197           (fun tac (metasenv,tacl) ->
198             let metasenv,tac = disambiguate_tactic metasenv tac in
199              metasenv,tac::tacl
200           ) tacl (metasenv,[])
201         in
202          metasenv,GrafiteAst.Then (loc,tac,tacl)
203     (* First order tactics *)
204     | GrafiteAst.Absurd (loc, term) -> 
205         let metasenv,cic = disambiguate_term context metasenv term in
206         metasenv,GrafiteAst.Absurd (loc, cic)
207     | GrafiteAst.Apply (loc, term) ->
208         let metasenv,cic = disambiguate_term context metasenv term in
209         metasenv,GrafiteAst.Apply (loc, cic)
210     | GrafiteAst.ApplyP (loc, term) ->
211         let metasenv,cic = disambiguate_term context metasenv term in
212         metasenv,GrafiteAst.ApplyP (loc, cic)
213     | GrafiteAst.ApplyS (loc, term, params) ->
214         let metasenv, params = disambiguate_auto_params metasenv params in
215         let metasenv,cic = disambiguate_term context metasenv term in
216         metasenv,GrafiteAst.ApplyS (loc, cic, params)
217     | GrafiteAst.Assumption loc ->
218         metasenv,GrafiteAst.Assumption loc
219     | GrafiteAst.AutoBatch (loc,params) ->
220         let metasenv, params = disambiguate_auto_params metasenv params in
221         metasenv,GrafiteAst.AutoBatch (loc,params)
222     | GrafiteAst.Cases (loc, what, pattern, idents) ->
223         let metasenv,what = disambiguate_term context metasenv what in
224         let pattern = disambiguate_pattern pattern in
225         metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
226     | GrafiteAst.Change (loc, pattern, with_what) -> 
227         let with_what = disambiguate_lazy_term with_what in
228         let pattern = disambiguate_pattern pattern in
229         metasenv,GrafiteAst.Change (loc, pattern, with_what)
230     | GrafiteAst.Clear (loc,id) ->
231         metasenv,GrafiteAst.Clear (loc,id)
232     | GrafiteAst.ClearBody (loc,id) ->
233        metasenv,GrafiteAst.ClearBody (loc,id)
234     | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
235         let metasenv,t1 = disambiguate_term context metasenv t1 in
236         let metasenv,t2 = 
237           match t2 with
238           | None -> metasenv, None
239           | Some t2 -> 
240               let m, t2 = disambiguate_term context metasenv t2 in
241               m, Some t2
242         in
243         metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
244     | GrafiteAst.Constructor (loc,n) ->
245         metasenv,GrafiteAst.Constructor (loc,n)
246     | GrafiteAst.Contradiction loc ->
247         metasenv,GrafiteAst.Contradiction loc
248     | GrafiteAst.Cut (loc, ident, term) -> 
249         let metasenv,cic = disambiguate_term context metasenv term in
250         metasenv,GrafiteAst.Cut (loc, ident, cic)
251     | GrafiteAst.Decompose (loc, names) ->
252          metasenv,GrafiteAst.Decompose (loc, names)
253     | GrafiteAst.Demodulate (loc, params) ->
254         let metasenv, params = disambiguate_auto_params metasenv params in
255         metasenv,GrafiteAst.Demodulate (loc, params)
256     | GrafiteAst.Destruct (loc, Some terms) ->
257         let map term (metasenv, terms) =
258            let metasenv, term = disambiguate_term context metasenv term in
259            metasenv, term :: terms
260         in
261         let metasenv, terms = List.fold_right map terms (metasenv, []) in 
262         metasenv, GrafiteAst.Destruct(loc, Some terms)
263     | GrafiteAst.Destruct (loc, None) ->
264         metasenv,GrafiteAst.Destruct(loc,None)
265     | GrafiteAst.Exact (loc, term) -> 
266         let metasenv,cic = disambiguate_term context metasenv term in
267         metasenv,GrafiteAst.Exact (loc, cic)
268     | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
269         let metasenv,what = disambiguate_term context metasenv what in
270         let metasenv,using = disambiguate_term context metasenv using in
271         let pattern = disambiguate_pattern pattern in
272         metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
273     | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
274         let metasenv,what = disambiguate_term context metasenv what in
275         let pattern = disambiguate_pattern pattern in
276         metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
277     | GrafiteAst.ElimType (loc, what, Some using, specs) ->
278         let metasenv,what = disambiguate_term context metasenv what in
279         let metasenv,using = disambiguate_term context metasenv using in
280         metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
281     | GrafiteAst.ElimType (loc, what, None, specs) ->
282         let metasenv,what = disambiguate_term context metasenv what in
283         metasenv,GrafiteAst.ElimType (loc, what, None, specs)
284     | GrafiteAst.Exists loc ->
285         metasenv,GrafiteAst.Exists loc 
286     | GrafiteAst.Fail loc ->
287         metasenv,GrafiteAst.Fail loc
288     | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
289         let pattern = disambiguate_pattern pattern in
290         let term = disambiguate_lazy_term term in
291         let red_kind = disambiguate_reduction_kind red_kind in
292         metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
293     | GrafiteAst.FwdSimpl (loc, hyp, names) ->
294        metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)  
295     | GrafiteAst.Fourier loc ->
296        metasenv,GrafiteAst.Fourier loc
297     | GrafiteAst.Generalize (loc,pattern,ident) ->
298         let pattern = disambiguate_pattern pattern in
299         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
300     | GrafiteAst.IdTac loc ->
301         metasenv,GrafiteAst.IdTac loc
302     | GrafiteAst.Intros (loc, specs) ->
303         metasenv,GrafiteAst.Intros (loc, specs)
304     | GrafiteAst.Inversion (loc, term) ->
305        let metasenv,term = disambiguate_term context metasenv term in
306         metasenv,GrafiteAst.Inversion (loc, term)
307     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
308        let f term (metasenv, to_what) =
309           let metasenv, term = disambiguate_term context metasenv term in
310           metasenv, term :: to_what
311        in
312        let metasenv, to_what = List.fold_right f to_what (metasenv, []) in 
313        let metasenv, what = disambiguate_term context metasenv what in
314        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
315     | GrafiteAst.Left loc ->
316        metasenv,GrafiteAst.Left loc
317     | GrafiteAst.LetIn (loc, term, name) ->
318         let metasenv,term = disambiguate_term context metasenv term in
319         metasenv,GrafiteAst.LetIn (loc,term,name)
320     | GrafiteAst.Reduce (loc, red_kind, pattern) ->
321         let pattern = disambiguate_pattern pattern in
322         let red_kind = disambiguate_reduction_kind red_kind in
323         metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
324     | GrafiteAst.Reflexivity loc ->
325         metasenv,GrafiteAst.Reflexivity loc
326     | GrafiteAst.Replace (loc, pattern, with_what) -> 
327         let pattern = disambiguate_pattern pattern in
328         let with_what = disambiguate_lazy_term with_what in
329         metasenv,GrafiteAst.Replace (loc, pattern, with_what)
330     | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
331         let metasenv,term = disambiguate_term context metasenv t in
332         let pattern = disambiguate_pattern pattern in
333         metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
334     | GrafiteAst.Right loc ->
335         metasenv,GrafiteAst.Right loc
336     | GrafiteAst.Ring loc ->
337         metasenv,GrafiteAst.Ring loc
338     | GrafiteAst.Split loc ->
339         metasenv,GrafiteAst.Split loc
340     | GrafiteAst.Symmetry loc ->
341         metasenv,GrafiteAst.Symmetry loc
342     | GrafiteAst.Transitivity (loc, term) -> 
343         let metasenv,cic = disambiguate_term context metasenv term in
344         metasenv,GrafiteAst.Transitivity (loc, cic)
345       (* Nuovi casi *)
346     | GrafiteAst.Assume (loc, id, term) -> 
347         let metasenv,cic = disambiguate_term context metasenv term in
348         metasenv,GrafiteAst.Assume (loc, id, cic)
349     | GrafiteAst.Suppose (loc, term, id, term') ->
350         let metasenv,cic = disambiguate_term context metasenv term in
351         let metasenv,cic' =
352            match term' with
353               None -> metasenv,None
354             | Some t ->
355                   let metasenv,t = disambiguate_term context metasenv t in
356                   metasenv,Some t in
357         metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
358     | GrafiteAst.Bydone (loc,just) ->
359         let metasenv,just =
360          disambiguate_just disambiguate_term context metasenv just
361         in
362          metasenv,GrafiteAst.Bydone (loc, just)
363     | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
364         let metasenv,cic = disambiguate_term context metasenv term in
365         let metasenv,cic' = 
366             match term' with
367               None -> metasenv,None
368             | Some t ->
369                   let metasenv,t = disambiguate_term context metasenv t in
370                   metasenv,Some t in
371         metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
372     | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') ->
373         let metasenv,just =
374          disambiguate_just disambiguate_term context metasenv just in
375         let metasenv,cic' = disambiguate_term context metasenv term' in
376         let metasenv,cic'' = 
377             match term'' with
378               None -> metasenv,None
379            |  Some t ->  
380                     let metasenv,t = disambiguate_term context metasenv t in
381                      metasenv,Some t in
382         metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'')
383     | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
384         let metasenv,cic = disambiguate_term context metasenv term in
385         let metasenv,cic' = disambiguate_term context metasenv term' in
386         metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
387     | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
388         let metasenv,cic = disambiguate_term context metasenv term in
389         let metasenv,cic' = disambiguate_term context metasenv term' in
390         metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
391    | GrafiteAst.Byinduction (loc, term, id) ->
392         let metasenv,cic = disambiguate_term context metasenv term in
393         metasenv,GrafiteAst.Byinduction(loc, cic, id)
394    | GrafiteAst.Thesisbecomes (loc, term) ->
395         let metasenv,cic = disambiguate_term context metasenv term in
396         metasenv,GrafiteAst.Thesisbecomes (loc, cic)
397    | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) ->
398         let metasenv,just =
399          disambiguate_just disambiguate_term context metasenv just in
400         let metasenv,cic' = disambiguate_term context metasenv term1 in
401         let cic''= disambiguate_lazy_term term2 in
402         metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
403    | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
404         let metasenv,just =
405          disambiguate_just disambiguate_term context metasenv just in
406         let metasenv,cic'= disambiguate_term context metasenv term1 in
407         let metasenv,cic''= disambiguate_term context metasenv term2 in
408         metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'')   
409    | GrafiteAst.Case (loc, id, params) ->
410         let metasenv,params' =
411          List.fold_right
412           (fun (id,term) (metasenv,params) ->
413             let metasenv,cic = disambiguate_term context metasenv term in
414              metasenv,(id,cic)::params
415           ) params (metasenv,[])
416         in
417         metasenv,GrafiteAst.Case(loc, id, params')   
418    | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
419         let metasenv,cic =
420          match term1 with
421             None -> metasenv,None
422           | Some (start,t) -> 
423              let metasenv,t = disambiguate_term context metasenv t in
424               metasenv,Some (start,t) in
425         let metasenv,cic'= disambiguate_term context metasenv term2 in
426         let metasenv,cic'' =
427          match term3 with
428           | `SolveWith term ->
429              let metasenv,term = disambiguate_term context metasenv term in
430              metasenv, `SolveWith term
431           | `Auto params -> 
432               let metasenv, params = disambiguate_auto_params metasenv params in
433               metasenv,`Auto params
434           | `Term t -> 
435              let metasenv,t = disambiguate_term context metasenv t in
436               metasenv,`Term t
437           | `Proof as t -> metasenv,t in
438         metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
439
440
441 let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
442   let uri =
443    match obj with
444     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
445     | CicNotationPt.Record (_,name,_,_) ->
446        (match baseuri with
447          | Some baseuri ->
448             Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
449          | None -> raise BaseUriNotSetYet)
450     | CicNotationPt.Inductive _ -> assert false
451     | CicNotationPt.Theorem _ -> None in
452   let (diff, metasenv, cic, _) =
453     singleton "third"
454       (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
455         ~aliases:lexicon_status.LexiconEngine.aliases
456         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
457         (text,prefix_len,obj)) in
458   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
459   lexicon_status, metasenv, cic
460   
461 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
462   match cmd with
463    | GrafiteAst.Index(loc,key,uri) ->
464        let lexicon_status_ref = ref lexicon_status in 
465        let disambiguate_term =
466          disambiguate_term text prefix_len lexicon_status_ref [] in
467        let disambiguate_term_option metasenv =
468          function
469              None -> metasenv,None
470            | Some t ->
471                let metasenv,t = disambiguate_term metasenv t in
472                  metasenv, Some t
473        in
474        let metasenv,key = disambiguate_term_option metasenv key in
475        !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
476    | GrafiteAst.Coercion (loc,t,b,a,s) -> 
477        let lexicon_status_ref = ref lexicon_status in 
478        let disambiguate_term =
479          disambiguate_term text prefix_len lexicon_status_ref [] in
480       let metasenv,t = disambiguate_term metasenv t in
481       !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
482    | GrafiteAst.Default _
483    | GrafiteAst.Drop _
484    | GrafiteAst.Include _
485    | GrafiteAst.Print _
486    | GrafiteAst.Qed _
487    | GrafiteAst.Set _ as cmd ->
488        lexicon_status,metasenv,cmd
489    | GrafiteAst.Obj (loc,obj) ->
490        let lexicon_status,metasenv,obj =
491         disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
492        lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
493    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
494       let lexicon_status_ref = ref lexicon_status in 
495       let disambiguate_term =
496        disambiguate_term text prefix_len lexicon_status_ref [] in
497       let disambiguate_term_option metasenv =
498        function
499           None -> metasenv,None
500        | Some t ->
501           let metasenv,t = disambiguate_term metasenv t in
502            metasenv, Some t
503       in
504       let metasenv,a = disambiguate_term metasenv a in
505       let metasenv,aeq = disambiguate_term metasenv aeq in
506       let metasenv,refl = disambiguate_term_option metasenv refl in
507       let metasenv,sym = disambiguate_term_option metasenv sym in
508       let metasenv,trans = disambiguate_term_option metasenv trans in
509        !lexicon_status_ref, metasenv,
510         GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
511
512 let disambiguate_macro 
513   lexicon_status_ref metasenv context (text,prefix_len, macro) 
514 =
515  let disambiguate_term = disambiguate_term text prefix_len lexicon_status_ref in
516   let disambiguate_reduction_kind = 
517     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
518   match macro with
519    | GrafiteAst.WMatch (loc,term) ->
520       let metasenv,term = disambiguate_term context metasenv term in
521        metasenv,GrafiteAst.WMatch (loc,term)
522    | GrafiteAst.WInstance (loc,term) ->
523       let metasenv,term = disambiguate_term context metasenv term in
524        metasenv,GrafiteAst.WInstance (loc,term)
525    | GrafiteAst.WElim (loc,term) ->
526       let metasenv,term = disambiguate_term context metasenv term in
527        metasenv,GrafiteAst.WElim (loc,term)
528    | GrafiteAst.WHint (loc,term) ->
529       let metasenv,term = disambiguate_term context metasenv term in
530        metasenv,GrafiteAst.WHint (loc,term)
531    | GrafiteAst.Check (loc,term) ->
532       let metasenv,term = disambiguate_term context metasenv term in
533        metasenv,GrafiteAst.Check (loc,term)
534    | GrafiteAst.Eval (loc,kind,term) ->
535       let metasenv, term = disambiguate_term context metasenv term in
536       let kind = disambiguate_reduction_kind kind in
537        metasenv,GrafiteAst.Eval (loc,kind,term)
538    | GrafiteAst.AutoInteractive (loc, params) -> 
539       let metasenv, params = 
540         disambiguate_auto_params disambiguate_term metasenv context params in
541       metasenv, GrafiteAst.AutoInteractive (loc, params)
542    | GrafiteAst.Hint _
543    | GrafiteAst.WLocate _
544    | GrafiteAst.Inline _ as macro ->
545       metasenv,macro