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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module Ast = NotationPt
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 *)
42 let initial_status = {
43 interpr = DisambiguateTypes.InterprEnv.empty;
44 multi_aliases = DisambiguateTypes.Environment.empty;
45 (* new_aliases = [] *)
50 inherit Interpretations.g_status
51 inherit NCicLibrary.g_status
52 method disambiguate_db: db
55 class virtual status uid =
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
71 (* let eval_with_new_aliases status f =
73 status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
75 let new_aliases = status#disambiguate_db.new_aliases in
79 (* reports the first source of ambiguity and its possible interpretations *)
80 exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
82 (* reports disambiguation errors *)
84 (* location of a choice point *)
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)
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
99 let add_to_interpr status new_aliases =
101 List.fold_left (fun acc (k,c) ->
102 DisambiguateTypes.InterprEnv.add k c acc)
103 status#disambiguate_db.interpr new_aliases
106 {status#disambiguate_db with interpr = interpr }
108 status#set_disambiguate_db new_status
110 let add_to_disambiguation_univ status new_aliases =
112 List.fold_left (fun acc (d,c) ->
113 DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
115 status#disambiguate_db.multi_aliases new_aliases
118 {status#disambiguate_db with multi_aliases = multi_aliases }
120 status#set_disambiguate_db new_status
123 exception BaseUriNotSetYet
125 let __Implicit = "__Implicit__"
126 let __Closed_Implicit = "__Closed_Implicit__"
128 let ncic_mk_choice status a =
129 prerr_endline "ncic_mk_choice";
131 | GrafiteAst.Symbol_alias (name,_, dsc) ->
132 prerr_endline ("caso 1: " ^ name ^ "; " ^ dsc);
133 if name = __Implicit then
134 dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
135 else if name = __Closed_Implicit then
136 dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
138 (prerr_endline (Printf.sprintf "mk_choice: symbol %s, interpr %s"
140 DisambiguateChoices.lookup_symbol_by_dsc status
141 ~mk_implicit:(function
142 | true -> NCic.Implicit `Closed
143 | false -> NCic.Implicit `Term)
145 (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
146 ~term_of_nref:(fun nref -> NCic.Const nref)
148 | GrafiteAst.Number_alias (_,dsc) ->
149 prerr_endline ("caso 2: " ^ dsc);
150 let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
152 (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
153 | GrafiteAst.Ident_alias (name, uri) ->
154 prerr_endline ("caso 3: " ^ name);
156 (fun l->assert(l = []);
157 let nref = NReference.reference_of_string uri in
165 GrafiteAst.Symbol_alias (__Implicit,None,"Fake Implicit")
167 GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
170 let nlookup_in_library status
171 interactive_user_uri_choice input_or_locate_uri item
174 | DisambiguateTypes.Id id ->
176 let references = NCicLibrary.resolve status id in
179 GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
182 NCicEnvironment.ObjectNotFound _ -> [])
186 (* XXX TO BE REMOVED: no need to fix instances any more *)
187 (*let fix_instance item l =
189 DisambiguateTypes.Symbol (_,n) ->
192 GrafiteAst.Symbol_alias (s,d) -> GrafiteAst.Symbol_alias (s,n,d)
195 | DisambiguateTypes.Num n ->
198 GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
201 | DisambiguateTypes.Id _ -> l
203 let fix_instance _ l = l;;
205 let rec diff_term loc t u = match (t,u) with
206 | Ast.AttributedTerm (`Loc l,t'), Ast.AttributedTerm (_,u') -> diff_term l t' u'
207 | Ast.AttributedTerm (_,t'), Ast.AttributedTerm (_,u') -> diff_term loc t' u'
208 | Ast.Appl tl, Ast.Appl ul ->
209 List.fold_left2 (fun acc t0 u0 -> diff_term loc t0 u0@acc) [] tl ul
210 | Ast.Binder (_,v1,b1), Ast.Binder (_,v2,b2) ->
211 diff_var loc v1 v2@ diff_term loc b1 b2
212 | Ast.Case (t1,ity1,outty1,pl1),Ast.Case (t2,ity2,outty2,pl2) ->
213 let ity_interp = match ity1,ity2 with
214 | Some (i,None), Some (_,Some r) ->
215 let uri = NReference.string_of_reference r in
216 [loc,GrafiteAst.Ident_alias (i,uri)]
219 let oty_interp = match outty1,outty2 with
220 | Some o1, Some o2 -> diff_term loc o1 o2
223 (* pl = (case_pattern * term) list *)
224 let auxpatt (c1,u1) (c2,u2) acc =
225 let diff_cp = match c1,c2 with
226 | Ast.Pattern (i,href1,vars1), Ast.Pattern (_,href2,vars2) ->
227 let diff_i = match href1,href2 with
229 let uri = NReference.string_of_reference r in
230 [loc,GrafiteAst.Ident_alias (i,uri)]
234 List.fold_right2 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
239 diff_term loc u1 u2 @ diff_cp @ acc
241 let pl_interp = List.fold_right2 auxpatt pl1 pl2 [] in
242 diff_term loc t1 t2 @ ity_interp @ oty_interp @ pl_interp
243 | Ast.Cast (u1,v1),Ast.Cast (u2,v2) ->
244 diff_term loc u1 u2@diff_term loc v1 v2
245 | Ast.LetIn (var1,u1,v1),Ast.LetIn (var2,u2,v2) ->
246 diff_var loc var1 var2 @ diff_term loc u1 u2 @ diff_term loc v1 v2
247 | Ast.LetRec (_,fl1,w1),Ast.LetRec (_,fl2,w2) ->
250 (fun (vars1,f1,b1,_) (vars2,f2,b2,_) acc ->
253 (fun v1 v2 acc0 -> diff_var loc v1 v2 @ acc0) vars1 vars2 []
255 diff_vars @ diff_var loc f1 f2 @ diff_term loc b1 b2 @ acc)
258 diff_funs @ diff_term loc w1 w2
259 | Ast.Ident (n,`Ambiguous),Ast.Ident (_,`Uri u) ->
260 [loc,GrafiteAst.Ident_alias (n,u)]
261 | Ast.Symbol (s, None),Ast.Symbol(_,Some (uri,desc)) ->
262 [loc,GrafiteAst.Symbol_alias (s,uri,desc)]
263 | Ast.Num (_, None),Ast.Num (_,Some (uri,desc)) ->
264 [loc,GrafiteAst.Number_alias (uri,desc)]
265 | _ -> [] (* leaves *)
266 and diff_var loc (_,v1) (_,v2) = match v1,v2 with
267 | Some v1', Some v2' -> diff_term loc v1' v2'
271 let diff_obj loc o1 o2 = match o1,o2 with
272 | Ast.Inductive (ls1,itys1), Ast.Inductive (ls2,itys2) ->
274 List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
278 (fun (i1,_,ty1,cl1) (i2,_,ty2,cl2) acc0 ->
281 (fun (_,u) (_,v) acc1 -> diff_term loc u v @ acc1)
284 diff_term loc ty1 ty2 @ diff_cl @ acc0)
288 | Ast.Theorem (_,i1,b1,ty1,_), Ast.Theorem (_,i2,b2,ty2,_) ->
289 let diff_tys = match ty1,ty2 with
290 | Some ty1', Some ty2' -> diff_term loc ty1' ty2'
293 diff_term loc b1 b2 @ diff_tys
294 | Ast.Record (ls1,_,ty1,fl1),Ast.Record (ls2,_,ty2,fl2) ->
296 List.fold_right2 (fun v1 v2 acc -> diff_var loc v1 v2 @ acc) ls1 ls2 []
300 (fun (_,f1,_,_) (_,f2,_,_) acc -> diff_term loc f1 f2 @ acc) fl1 fl2 []
302 diff_ls @ diff_term loc ty1 ty2 @ diff_fl
306 (* this function, called on a list of choices that must
307 * be different, never fails and returns the location of
308 * the first ambiguity (and its possible interpretations) *)
309 let rec find_diffs l =
310 let loc,_ = List.hd (List.hd l) in
311 let hds = List.map (fun x -> snd (List.hd x)) l in
312 let uniq_hds = HExtlib.list_uniq (List.sort Pervasives.compare hds) in
314 if List.length uniq_hds > 1
317 let tls = List.map List.tl l in
321 (* clusterize a list of errors according to the last chosen interpretation *)
322 let clusterize diff (eframe,loc0) =
323 let rec aux = function
325 | (_,choice,_,_ as x)::l0 ->
326 let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in
327 (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) ::
331 let disambiguate_nterm status expty context metasenv subst thing
333 let _,_,thing' = thing in
334 match NCicDisambiguate.disambiguate_term
336 ~aliases:status#disambiguate_db.interpr
338 ~universe:(status#disambiguate_db.multi_aliases)
339 ~lookup_in_library:(nlookup_in_library status)
340 ~mk_choice:(ncic_mk_choice status)
341 ~mk_implicit ~fix_instance
342 ~description_of_alias:GrafiteAst.description_of_alias
343 ~context ~metasenv ~subst thing
345 | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] ->
346 let diff = diff_term Stdpp.dummy_loc thing' newast in
347 let status = add_to_interpr status diff
349 metasenv, subst, status, cic
350 | Disambiguate.Disamb_success (_::_ as choices) ->
352 List.map (fun (ast,_,_,_,_) ->
353 diff_term Stdpp.dummy_loc thing' ast) choices
355 raise (Ambiguous_input (find_diffs diffs))
356 | Disambiguate.Disamb_failure (l,_) ->
357 raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l))
362 NotationPt.term Disambiguate.disambiguator_input option *
363 (string * NCic.term) list * NCic.term option
365 let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
366 let interp path = NCicDisambiguate.disambiguate_path status path in
367 let goal_path = HExtlib.map_option interp goal_path in
368 let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
369 let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
370 (wanted, hyp_paths, goal_path)
373 let disambiguate_reduction_kind text prefix_len = function
374 | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
378 | `Whd as kind -> kind
381 let disambiguate_auto_params
382 disambiguate_term metasenv context (oterms, params)
385 | None -> metasenv, (None, params)
387 let metasenv, terms =
389 (fun t (metasenv, terms) ->
390 let metasenv,t = disambiguate_term context metasenv t in
391 metasenv,t::terms) terms (metasenv, [])
393 metasenv, (Some terms, params)
396 let disambiguate_just disambiguate_term context metasenv =
399 let metasenv,t = disambiguate_term context metasenv t in
402 let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
405 metasenv, `Auto params
408 let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
411 match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
415 | NotationPt.Inductive (_,(name,_,_,_)::_)
416 | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
417 | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
418 | NotationPt.Inductive _ -> assert false
420 NUri.uri_of_string (baseuri ^ "/" ^ name)
423 match NCicDisambiguate.disambiguate_obj
425 ~lookup_in_library:(nlookup_in_library status)
426 ~description_of_alias:GrafiteAst.description_of_alias
427 ~mk_choice:(ncic_mk_choice status)
428 ~mk_implicit ~fix_instance ~uri
429 ~aliases:status#disambiguate_db.interpr
430 ~universe:(status#disambiguate_db.multi_aliases)
433 | Disambiguate.Disamb_success [newast,_,_,cic,_] ->
434 let diff = diff_obj Stdpp.dummy_loc obj newast in
435 let status = add_to_interpr status diff
437 | Disambiguate.Disamb_success (_::_ as choices) ->
439 List.map (fun (ast,_,_,_,_) ->
440 diff_obj Stdpp.dummy_loc obj ast) choices
442 raise (Ambiguous_input (find_diffs diffs))
443 | Disambiguate.Disamb_failure (l,_) ->
444 raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l))
448 let disambiguate_cic_appl_pattern status args =
449 let rec disambiguate =
451 NotationPt.ApplPattern l ->
452 NotationPt.ApplPattern (List.map disambiguate l)
453 | NotationPt.VarPattern id
456 (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
458 let item = DisambiguateTypes.Id id in
462 DisambiguateTypes.Environment.find item
463 (* status#disambiguate_db.aliases *)
464 status#disambiguate_db.multi_aliases
466 (* XXX : we only try the first match *)
467 GrafiteAst.Ident_alias (_,uri)::_ ->
468 NotationPt.NRefPattern (NReference.reference_of_string uri)
472 ("LexiconEngine.eval_command: domain item not found: " ^
473 (DisambiguateTypes.string_of_domain_item item));
474 dump_aliases prerr_endline "" status;
477 ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
484 let aliases_for_objs status refs =
488 let references = NCicLibrary.aliases_of status nref in
491 let name = NCicPp.r2s status true u in
492 (* FIXME : we are forgetting the interpretation of the Id
493 * but is this useful anymore?!?!? *)
494 DisambiguateTypes.Id name,
495 GrafiteAst.Ident_alias (name,NReference.string_of_reference u)