]> matita.cs.unibo.it Git - helm.git/blob - components/grafite_parser/grafiteDisambiguate.ml
Up to absolute value
[helm.git] / 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 = function
40   | [x], _ -> x
41   | _ -> assert false
42 ;;
43
44   (** @param term not meaningful when context is given *)
45 let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
46   let lexicon_status = !lexicon_status_ref in
47   let (diff, metasenv, cic, _) =
48     singleton
49       (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
50         ~aliases:lexicon_status.LexiconEngine.aliases
51         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
52         ~context ~metasenv (text,prefix_len,term))
53   in
54   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
55   lexicon_status_ref := lexicon_status;
56   metasenv,cic
57 ;;
58
59   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
60    * rationale: lazy_term will be invoked in different context to obtain a term,
61    * each invocation will disambiguate the term and can add aliases. Once all
62    * disambiguations have been performed, the first returned function can be
63    * used to obtain the resulting aliases *)
64 let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
65   (fun context metasenv ugraph ->
66     let lexicon_status = !lexicon_status_ref in
67     let (diff, metasenv, cic, ugraph) =
68       singleton
69         (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
70           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
71           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
72           ~context ~metasenv
73           (text,prefix_len,term)) in
74     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
75     lexicon_status_ref := lexicon_status;
76     cic, metasenv, ugraph)
77 ;;
78
79 let disambiguate_pattern 
80   text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path) 
81 =
82   let interp path = Disambiguate.interpretate_path [] path in
83   let goal_path = HExtlib.map_option interp goal_path in
84   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
85   let wanted =
86    match wanted with
87       None -> None
88     | Some wanted ->
89        let wanted = 
90          disambiguate_lazy_term text prefix_len lexicon_status_ref wanted 
91        in
92        Some wanted
93   in
94   (wanted, hyp_paths, goal_path)
95 ;;
96
97 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
98   | `Unfold (Some t) ->
99       let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
100       `Unfold (Some t)
101   | `Normalize
102   | `Reduce
103   | `Simpl
104   | `Unfold None
105   | `Whd as kind -> kind
106 ;;
107
108 let disambiguate_tactic 
109   lexicon_status_ref context metasenv (text,prefix_len,tactic) 
110 =
111   let disambiguate_term = 
112     disambiguate_term text prefix_len lexicon_status_ref in
113   let disambiguate_pattern = 
114     disambiguate_pattern text prefix_len lexicon_status_ref in
115   let disambiguate_reduction_kind = 
116     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
117   let disambiguate_lazy_term = 
118     disambiguate_lazy_term text prefix_len lexicon_status_ref in
119    match tactic with
120     | GrafiteAst.Absurd (loc, term) -> 
121         let metasenv,cic = disambiguate_term context metasenv term in
122         metasenv,GrafiteAst.Absurd (loc, cic)
123     | GrafiteAst.Apply (loc, term) ->
124         let metasenv,cic = disambiguate_term context metasenv term in
125         metasenv,GrafiteAst.Apply (loc, cic)
126     | GrafiteAst.ApplyS (loc, term, params) ->
127         let metasenv,cic = disambiguate_term context metasenv term in
128         metasenv,GrafiteAst.ApplyS (loc, cic, params)
129     | GrafiteAst.Assumption loc ->
130         metasenv,GrafiteAst.Assumption loc
131     | GrafiteAst.Auto (loc,params) ->
132         metasenv,GrafiteAst.Auto (loc,params)
133     | GrafiteAst.Change (loc, pattern, with_what) -> 
134         let with_what = disambiguate_lazy_term with_what in
135         let pattern = disambiguate_pattern pattern in
136         metasenv,GrafiteAst.Change (loc, pattern, with_what)
137     | GrafiteAst.Clear (loc,id) ->
138         metasenv,GrafiteAst.Clear (loc,id)
139     | GrafiteAst.ClearBody (loc,id) ->
140        metasenv,GrafiteAst.ClearBody (loc,id)
141     | GrafiteAst.Constructor (loc,n) ->
142         metasenv,GrafiteAst.Constructor (loc,n)
143     | GrafiteAst.Contradiction loc ->
144         metasenv,GrafiteAst.Contradiction loc
145     | GrafiteAst.Cut (loc, ident, term) -> 
146         let metasenv,cic = disambiguate_term context metasenv term in
147         metasenv,GrafiteAst.Cut (loc, ident, cic)
148     | GrafiteAst.Decompose (loc, types, what, names) ->
149         let disambiguate (metasenv,types) = function
150            | GrafiteAst.Type _   -> assert false
151            | GrafiteAst.Ident id ->
152               (match
153                 disambiguate_term context metasenv
154                  (CicNotationPt.Ident(id, None))
155                with
156                 | metasenv,Cic.MutInd (uri, tyno, _) ->
157                     metasenv,(GrafiteAst.Type (uri, tyno) :: types)
158                 | _ ->
159                   raise (GrafiteDisambiguator.DisambiguationError
160                    (0,[[[],[],None,lazy "Decompose works only on inductive types"]])))
161         in
162         let metasenv,types =
163          List.fold_left disambiguate (metasenv,[]) types
164         in
165          metasenv,GrafiteAst.Decompose (loc, types, what, names)
166     | GrafiteAst.Demodulate loc ->
167         metasenv,GrafiteAst.Demodulate loc
168     | GrafiteAst.Destruct (loc,term) ->
169         let metasenv,term = disambiguate_term context metasenv term in
170         metasenv,GrafiteAst.Destruct(loc,term)
171     | GrafiteAst.Exact (loc, term) -> 
172         let metasenv,cic = disambiguate_term context metasenv term in
173         metasenv,GrafiteAst.Exact (loc, cic)
174     | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
175         let metasenv,what = disambiguate_term context metasenv what in
176         let metasenv,using = disambiguate_term context metasenv using in
177         metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
178     | GrafiteAst.Elim (loc, what, None, depth, idents) ->
179         let metasenv,what = disambiguate_term context metasenv what in
180         metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
181     | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
182         let metasenv,what = disambiguate_term context metasenv what in
183         let metasenv,using = disambiguate_term context metasenv using in
184         metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents)
185     | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
186         let metasenv,what = disambiguate_term context metasenv what in
187         metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
188     | GrafiteAst.Exists loc ->
189         metasenv,GrafiteAst.Exists loc 
190     | GrafiteAst.Fail loc ->
191         metasenv,GrafiteAst.Fail loc
192     | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
193         let pattern = disambiguate_pattern pattern in
194         let term = disambiguate_lazy_term term in
195         let red_kind = disambiguate_reduction_kind red_kind in
196         metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
197     | GrafiteAst.FwdSimpl (loc, hyp, names) ->
198        metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)  
199     | GrafiteAst.Fourier loc ->
200        metasenv,GrafiteAst.Fourier loc
201     | GrafiteAst.Generalize (loc,pattern,ident) ->
202         let pattern = disambiguate_pattern pattern in
203         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
204     | GrafiteAst.Goal (loc, g) ->
205         metasenv,GrafiteAst.Goal (loc, g)
206     | GrafiteAst.IdTac loc ->
207         metasenv,GrafiteAst.IdTac loc
208     | GrafiteAst.Intros (loc, num, names) ->
209         metasenv,GrafiteAst.Intros (loc, num, names)
210     | GrafiteAst.Inversion (loc, term) ->
211        let metasenv,term = disambiguate_term context metasenv term in
212         metasenv,GrafiteAst.Inversion (loc, term)
213     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
214        let f term to_what =
215           let metasenv,term = disambiguate_term context metasenv term in
216           term :: to_what
217        in
218        let to_what = List.fold_right f to_what [] in 
219        let metasenv,what = disambiguate_term context metasenv what in
220        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
221     | GrafiteAst.Left loc ->
222        metasenv,GrafiteAst.Left loc
223     | GrafiteAst.LetIn (loc, term, name) ->
224         let metasenv,term = disambiguate_term context metasenv term in
225         metasenv,GrafiteAst.LetIn (loc,term,name)
226     | GrafiteAst.Reduce (loc, red_kind, pattern) ->
227         let pattern = disambiguate_pattern pattern in
228         let red_kind = disambiguate_reduction_kind red_kind in
229         metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
230     | GrafiteAst.Reflexivity loc ->
231         metasenv,GrafiteAst.Reflexivity loc
232     | GrafiteAst.Replace (loc, pattern, with_what) -> 
233         let pattern = disambiguate_pattern pattern in
234         let with_what = disambiguate_lazy_term with_what in
235         metasenv,GrafiteAst.Replace (loc, pattern, with_what)
236     | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
237         let metasenv,term = disambiguate_term context metasenv t in
238         let pattern = disambiguate_pattern pattern in
239         metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
240     | GrafiteAst.Right loc ->
241         metasenv,GrafiteAst.Right loc
242     | GrafiteAst.Ring loc ->
243         metasenv,GrafiteAst.Ring loc
244     | GrafiteAst.Split loc ->
245         metasenv,GrafiteAst.Split loc
246     | GrafiteAst.Subst loc ->
247         metasenv, GrafiteAst.Subst loc
248     | GrafiteAst.Symmetry loc ->
249         metasenv,GrafiteAst.Symmetry loc
250     | GrafiteAst.Transitivity (loc, term) -> 
251         let metasenv,cic = disambiguate_term context metasenv term in
252         metasenv,GrafiteAst.Transitivity (loc, cic)
253       (* Nuovi casi *)
254     | GrafiteAst.Assume (loc, id, term) -> 
255         let metasenv,cic = disambiguate_term context metasenv term in
256         metasenv,GrafiteAst.Assume (loc, id, cic)
257     | GrafiteAst.Suppose (loc, term, id, term') ->
258         let metasenv,cic = disambiguate_term context metasenv term in
259         let metasenv,cic' =
260            match term' with
261               None -> metasenv,None
262             | Some t ->
263                   let metasenv,t = disambiguate_term context metasenv t in
264                   metasenv,Some t in
265         metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
266     | GrafiteAst.Bydone (loc,term) ->
267         let metasenv,cic = 
268            match term with
269               None -> metasenv,None
270              |Some t ->
271                  let metasenv,t = disambiguate_term context metasenv t in
272                  metasenv,Some t in
273                  metasenv,GrafiteAst.Bydone (loc, cic)
274     | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
275         let metasenv,cic = disambiguate_term context metasenv term in
276         let metasenv,cic' = 
277             match term' with
278               None -> metasenv,None
279             | Some t ->
280                   let metasenv,t = disambiguate_term context metasenv t in
281                   metasenv,Some t in
282         metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
283     | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') ->
284         let metasenv,cic =
285            match term with 
286              None -> metasenv,None
287            | Some t ->
288                  let metasenv,t = disambiguate_term context metasenv t in
289                  metasenv,Some t in
290         let metasenv,cic' = disambiguate_term context metasenv term' in
291         let metasenv,cic'' = 
292             match term'' with
293               None -> metasenv,None
294            |  Some t ->  
295                     let metasenv,t = disambiguate_term context metasenv t in
296                      metasenv,Some t in
297         metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
298     | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
299         let metasenv,cic = disambiguate_term context metasenv term in
300         let metasenv,cic' = disambiguate_term context metasenv term' in
301         metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
302    | GrafiteAst.Byinduction (loc, term, id) ->
303         let metasenv,cic = disambiguate_term context metasenv term in
304         metasenv,GrafiteAst.Byinduction(loc, cic, id)
305    | GrafiteAst.Thesisbecomes (loc, term) ->
306         let metasenv,cic = disambiguate_term context metasenv term in
307         metasenv,GrafiteAst.Thesisbecomes (loc, cic)
308    | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
309         let metasenv,cic = disambiguate_term context metasenv term in
310         let metasenv,cic' = disambiguate_term context metasenv term1 in
311         let metasenv,cic''= disambiguate_term context metasenv term2 in
312         metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
313    | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
314         let metasenv,cic = disambiguate_term context metasenv term in
315         let metasenv,cic'= disambiguate_term context metasenv term1 in
316         let metasenv,cic''= disambiguate_term context metasenv term2 in
317         metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')   
318    | GrafiteAst.Case (loc, id, params) ->
319         let metasenv,params' =
320          List.fold_right
321           (fun (id,term) (metasenv,params) ->
322             let metasenv,cic = disambiguate_term context metasenv term in
323              metasenv,(id,cic)::params
324           ) params (metasenv,[])
325         in
326         metasenv,GrafiteAst.Case(loc, id, params')   
327    | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
328         let metasenv,cic =
329          match term1 with
330             None -> metasenv,None
331           | Some t -> 
332              let metasenv,t = disambiguate_term context metasenv t in
333               metasenv,Some t in
334         let metasenv,cic'= disambiguate_term context metasenv term2 in
335         let metasenv,cic'' =
336          match term3 with
337             None -> metasenv,None
338           | Some t -> 
339              let metasenv,t = disambiguate_term context metasenv t in
340               metasenv,Some t in
341         metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
342
343
344 let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
345   let uri =
346    match obj with
347     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
348     | CicNotationPt.Record (_,name,_,_) ->
349        (match baseuri with
350          | Some baseuri ->
351             Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
352          | None -> raise BaseUriNotSetYet)
353     | CicNotationPt.Inductive _ -> assert false
354     | CicNotationPt.Theorem _ -> None in
355   let (diff, metasenv, cic, _) =
356     singleton
357       (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
358         ~aliases:lexicon_status.LexiconEngine.aliases
359         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
360         (text,prefix_len,obj)) in
361   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
362   lexicon_status, metasenv, cic
363   
364 let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
365   match cmd with
366    | GrafiteAst.Coercion _
367    | GrafiteAst.Default _
368    | GrafiteAst.Drop _
369    | GrafiteAst.Include _
370    | GrafiteAst.Print _
371    | GrafiteAst.Qed _
372    | GrafiteAst.Set _ as cmd ->
373        lexicon_status,metasenv,cmd
374    | GrafiteAst.Obj (loc,obj) ->
375        let lexicon_status,metasenv,obj =
376         disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in
377        lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
378    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
379       let lexicon_status_ref = ref lexicon_status in 
380       let disambiguate_term =
381        disambiguate_term text prefix_len lexicon_status_ref [] in
382       let disambiguate_term_option metasenv =
383        function
384           None -> metasenv,None
385        | Some t ->
386           let metasenv,t = disambiguate_term metasenv t in
387            metasenv, Some t
388       in
389       let metasenv,a = disambiguate_term metasenv a in
390       let metasenv,aeq = disambiguate_term metasenv aeq in
391       let metasenv,refl = disambiguate_term_option metasenv refl in
392       let metasenv,sym = disambiguate_term_option metasenv sym in
393       let metasenv,trans = disambiguate_term_option metasenv trans in
394        !lexicon_status_ref, metasenv,
395         GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
396
397 let disambiguate_macro 
398   lexicon_status_ref metasenv context (text,prefix_len, macro) 
399 =
400  let disambiguate_term = disambiguate_term text prefix_len lexicon_status_ref in
401   match macro with
402    | GrafiteAst.WMatch (loc,term) ->
403       let metasenv,term = disambiguate_term context metasenv term in
404        metasenv,GrafiteAst.WMatch (loc,term)
405    | GrafiteAst.WInstance (loc,term) ->
406       let metasenv,term = disambiguate_term context metasenv term in
407        metasenv,GrafiteAst.WInstance (loc,term)
408    | GrafiteAst.WElim (loc,term) ->
409       let metasenv,term = disambiguate_term context metasenv term in
410        metasenv,GrafiteAst.WElim (loc,term)
411    | GrafiteAst.WHint (loc,term) ->
412       let metasenv,term = disambiguate_term context metasenv term in
413        metasenv,GrafiteAst.WHint (loc,term)
414    | GrafiteAst.Check (loc,term) ->
415       let metasenv,term = disambiguate_term context metasenv term in
416        metasenv,GrafiteAst.Check (loc,term)
417    | GrafiteAst.Hint _
418    | GrafiteAst.WLocate _
419    | GrafiteAst.Inline _ as macro ->
420       metasenv,macro