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