]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
Matitaweb: TeX-like macro handling.
[helm.git] / matitaB / components / ng_disambiguation / 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 module Ast = NotationPt
29
30 type db = {
31   (* maps (loc,domain_item) to alias *)
32   interpr: GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t;
33   (* the universe of possible interpretations for all symbols/ids/nums *)
34   multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
35   (* new_aliases: ((Stdpp.location * DisambiguateTypes.domain_item) * GrafiteAst.alias_spec) list *)
36 }
37
38 let get_interpr db =
39   db.interpr
40 ;;
41
42 let initial_status = {
43   interpr = DisambiguateTypes.InterprEnv.empty;
44   multi_aliases = DisambiguateTypes.Environment.empty;
45   (* new_aliases = [] *)
46 }
47
48 class type g_status =
49   object
50    inherit Interpretations.g_status
51    method disambiguate_db: db
52   end
53
54 class virtual status uid =
55  object (self)
56   inherit Interpretations.status uid
57   val disambiguate_db = initial_status
58   method disambiguate_db = disambiguate_db
59   method set_disambiguate_db v = {< disambiguate_db = v >}
60   method set_disambiguate_status
61    : 'status. #g_status as 'status -> 'self
62       = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
63  end
64
65 (* let eval_with_new_aliases status f =
66  let status =
67   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
68  let res = f status in
69  let new_aliases = status#disambiguate_db.new_aliases in
70   new_aliases,res
71 ;;*)
72
73 let dump_aliases out msg status =
74    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
75    DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
76     status#disambiguate_db.interpr
77
78 let add_to_interpr status new_aliases =
79    let interpr =
80     List.fold_left (fun acc (k,c) -> 
81       DisambiguateTypes.InterprEnv.add k c acc)
82       status#disambiguate_db.interpr new_aliases 
83    in
84    let new_status =
85      {status#disambiguate_db with interpr = interpr }
86    in
87     status#set_disambiguate_db new_status
88    
89 let add_to_disambiguation_univ status new_aliases =
90    let multi_aliases =
91     List.fold_left (fun acc (d,c) -> 
92       DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias 
93          d c acc)
94      status#disambiguate_db.multi_aliases new_aliases
95    in
96    let new_status =
97      {status#disambiguate_db with multi_aliases = multi_aliases }
98    in
99     status#set_disambiguate_db new_status
100
101
102 exception BaseUriNotSetYet
103
104 let singleton msg = function
105   | [x], _ -> x
106   | l, _   ->
107       let debug = 
108          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
109          msg (List.length l)
110       in
111       prerr_endline debug; assert false
112
113 let __Implicit = "__Implicit__"
114 let __Closed_Implicit = "__Closed_Implicit__"
115
116 let ncic_mk_choice status a =
117   prerr_endline "ncic_mk_choice";
118   match a with
119   | GrafiteAst.Symbol_alias (name,_, dsc) ->
120      prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc);
121      if name = __Implicit then
122        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
123      else if name = __Closed_Implicit then 
124        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
125      else
126        (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s"
127          name dsc);
128        DisambiguateChoices.lookup_symbol_by_dsc status
129         ~mk_implicit:(function 
130            | true -> NCic.Implicit `Closed
131            | false -> NCic.Implicit `Term)
132         ~mk_appl:(function 
133            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
134         ~term_of_nref:(fun nref -> NCic.Const nref)
135        name dsc)
136   | GrafiteAst.Number_alias (_,dsc) -> 
137      prerr_endline ("caso 2: " ^ dsc);
138      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
139       desc, `Num_interp
140        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
141   | GrafiteAst.Ident_alias (name, uri) -> 
142      prerr_endline ("caso 3: " ^ name);
143      uri, `Sym_interp 
144       (fun l->assert(l = []);
145         let nref = NReference.reference_of_string uri in
146          NCic.Const nref)
147 ;;
148
149
150 let mk_implicit b =
151   match b with
152   | false -> 
153       GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
154   | true -> 
155       GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
156 ;;
157
158 let nlookup_in_library 
159   interactive_user_uri_choice input_or_locate_uri item 
160 =
161   match item with
162   | DisambiguateTypes.Id id -> 
163      (try
164        let references = NCicLibrary.resolve id in
165         List.map
166          (fun u -> 
167            GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
168          ) references
169       with
170        NCicEnvironment.ObjectNotFound _ -> [])
171   | _ -> []
172 ;;
173
174 (* XXX TO BE REMOVED: no need to fix instances any more *)
175 (*let fix_instance item l =
176  match item with
177     DisambiguateTypes.Symbol (_,n) ->
178      List.map
179       (function
180           GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
181         | _ -> assert false
182       ) l
183   | DisambiguateTypes.Num n ->
184      List.map
185       (function
186           GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
187         | _ -> assert false
188       ) l
189   | DisambiguateTypes.Id _ -> l
190 ;;*)
191 let fix_instance _ l = l;;
192
193 let rec diff_term loc t u = match (t,u) with
194   | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u'
195   | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u' 
196   | Ast.Appl tl, Ast.Appl ul ->
197       List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul
198   | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) -> 
199      diff_var loc v1 v2@ diff_term loc b1 b2
200   | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) -> 
201       let ity_interp = match ity1,ity2 with
202       | Some (i,None), Some (_,Some r) -> 
203          let uri = NReference.string_of_reference r in
204          [loc,GrafiteAst.Ident_alias (i,uri)]
205       | _ -> []
206       in
207       let oty_interp = match outty1,outty2 with
208       | Some o1, Some o2 -> diff_term loc o1 o2
209       | _ -> []
210       in
211       (* pl = (case_pattern * term) list *)
212       let auxpatt (c1,u1) (c2,u2) acc =
213         let diff_cp = match c1,c2 with
214         | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) ->
215            let diff_i = match href1,href2 with
216              | None, Some r ->
217                 let uri = NReference.string_of_reference r in
218                 [loc,GrafiteAst.Ident_alias (i,uri)]
219              | _ -> []
220            in
221            let diff_vars = 
222              List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
223            in
224            diff_i @ diff_vars
225         | _ -> []
226         in
227         diff_term loc u1 u2 @ diff_cp @ acc
228       in
229       let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in
230       diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp
231   | Ast.Cast (u1,v1),Ast.Cast (u2,v2) -> 
232      diff_term loc u1 u2@diff_term loc v1 v2
233   | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) ->
234      diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2
235   | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) ->
236     let diff_funs =
237       List.fold_right2 
238         (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc ->
239            let diff_vars = 
240              List.fold_right2 
241                (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 [] 
242            in
243            diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc)
244         fl1 fl2 []
245     in  
246     diff_funs @ diff_term loc w1 w2
247   | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) ->
248       [loc,GrafiteAst.Ident_alias (n,u)]
249   | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) ->
250       [loc,GrafiteAst.Symbol_alias (s,uri,desc)]
251   | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) ->
252       [loc,GrafiteAst.Number_alias (uri,desc)]
253   | _ -> [] (* leaves *)
254 and diff_var loc (_,v1) (_,v2) = match v1,v2 with
255   | Some v1', Some v2' -> diff_term loc v1' v2'
256   | _ -> []
257 ;;
258
259 let diff_obj loc o1 o2 = match o1,o2 with
260  | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) ->
261      let diff_ls = 
262        List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
263      in
264      let diff_itys =
265        List.fold_right2
266          (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 -> 
267             let diff_cl =
268               List.fold_right2 
269                (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1)
270                cl1 cl2 []
271             in
272             diff_term loc ty1 ty2 @ diff_cl @ acc0)
273          itys1 itys2 []
274      in
275      diff_ls @ diff_itys
276  | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) ->
277      let diff_tys = match ty1,ty2 with
278      | Some ty1', Some ty2' -> diff_term loc ty1' ty2'
279      | _ -> []
280      in
281      diff_term loc b1 b2 @ diff_tys
282  | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) ->
283      let diff_ls = 
284        List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
285      in
286      let diff_fl =
287        List.fold_right2
288          (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 []
289      in
290      diff_ls @ diff_term loc ty1 ty2 @ diff_fl
291  | _ -> assert false
292 ;;
293
294 let disambiguate_nterm status expty context metasenv subst thing
295 =
296   let newast, metasenv, subst, cic =
297     singleton "first"
298       (NCicDisambiguate.disambiguate_term
299         status
300         ~aliases:status#disambiguate_db.interpr
301         ~expty 
302         ~universe:(status#disambiguate_db.multi_aliases)
303         ~lookup_in_library:nlookup_in_library
304         ~mk_choice:(ncic_mk_choice status)
305         ~mk_implicit ~fix_instance
306         ~description_of_alias:GrafiteAst.description_of_alias
307         ~context ~metasenv ~subst thing)
308   in
309   let _,_,thing' = thing in
310   let diff = diff_term Stdpp.dummy_loc thing' newast in
311   let status = add_to_interpr status diff
312   in
313    metasenv, subst, status, cic
314 ;;
315
316
317 type pattern = 
318   NotationPt.term Disambiguate.disambiguator_input option * 
319   (string * NCic.term) list * NCic.term option
320
321 let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
322   let interp path = NCicDisambiguate.disambiguate_path status path in
323   let goal_path = HExtlib.map_option interp goal_path in
324   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
325   let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
326    (wanted, hyp_paths, goal_path)
327 ;;
328
329 let disambiguate_reduction_kind text prefix_len = function
330   | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
331   | `Normalize
332   | `Simpl
333   | `Unfold None
334   | `Whd as kind -> kind
335 ;;
336
337 let disambiguate_auto_params 
338   disambiguate_term metasenv context (oterms, params) 
339 =
340   match oterms with 
341     | None -> metasenv, (None, params)
342     | Some terms ->
343         let metasenv, terms = 
344           List.fold_right 
345             (fun t (metasenv, terms) ->
346                let metasenv,t = disambiguate_term context metasenv t in
347                  metasenv,t::terms) terms (metasenv, [])
348         in
349           metasenv, (Some terms, params)
350 ;;
351
352 let disambiguate_just disambiguate_term context metasenv =
353  function
354     `Term t ->
355       let metasenv,t = disambiguate_term context metasenv t in
356        metasenv, `Term t
357   | `Auto params ->
358       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
359        context params
360       in
361        metasenv, `Auto params
362 ;;
363       
364 let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
365   let uri =
366    let baseuri = 
367      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
368    in
369    let name = 
370      match obj with
371      | NotationPt.Inductive (_,(name,_,_,_)::_)
372      | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
373      | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
374      | NotationPt.Inductive _ -> assert false
375    in
376      NUri.uri_of_string (baseuri ^ "/" ^ name)
377   in
378   let ast, _, _, cic =
379    singleton "third"
380     (NCicDisambiguate.disambiguate_obj
381       status
382       ~lookup_in_library:nlookup_in_library
383       ~description_of_alias:GrafiteAst.description_of_alias
384       ~mk_choice:(ncic_mk_choice status)
385       ~mk_implicit ~fix_instance ~uri
386       ~aliases:status#disambiguate_db.interpr
387       ~universe:(status#disambiguate_db.multi_aliases) 
388       (text,prefix_len,obj)) in
389   let diff = diff_obj Stdpp.dummy_loc obj ast in
390   let status = add_to_interpr status diff
391   in
392    status, cic
393 ;;
394
395 let disambiguate_cic_appl_pattern status args =
396  let rec disambiguate =
397   function
398     NotationPt.ApplPattern l ->
399      NotationPt.ApplPattern (List.map disambiguate l)
400   | NotationPt.VarPattern id
401      when not
402       (List.exists
403        (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
404      ->
405       let item = DisambiguateTypes.Id id in
406        begin
407         try
408          match
409           DisambiguateTypes.Environment.find item
410            (* status#disambiguate_db.aliases *)
411            status#disambiguate_db.multi_aliases
412          with
413          (* XXX : we only try the first match *)
414             GrafiteAst.Ident_alias (_,uri)::_ ->
415              NotationPt.NRefPattern (NReference.reference_of_string uri)
416           | _ -> assert false
417         with Not_found -> 
418          prerr_endline
419           ("LexiconEngine.eval_command: domain item not found: " ^ 
420           (DisambiguateTypes.string_of_domain_item item));
421          dump_aliases prerr_endline "" status;
422          raise 
423           (Failure
424            ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
425              end
426   | p -> p
427  in
428   disambiguate
429 ;;
430
431 let aliases_for_objs status refs =
432  List.concat
433   (List.map
434     (fun nref ->
435       let references = NCicLibrary.aliases_of nref in
436        List.map
437         (fun u ->
438           let name = NCicPp.r2s status true u in
439            (* FIXME : we are forgetting the interpretation of the Id
440             * but is this useful anymore?!?!? *)
441            DisambiguateTypes.Id name,
442             GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
443         ) references) refs)