]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/disambiguation/disambiguate.ml
Debugging code commented out.
[helm.git] / matitaB / components / disambiguation / disambiguate.ml
1 (* Copyright (C) 2004, HELM Team.
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 open Printf
29
30 open DisambiguateTypes
31
32 module Ast = NotationPt
33
34 (* the integer is an offset to be added to each location *)
35 exception Ambiguous_input
36 (* the integer is an offset to be added to each location *)
37 exception NoWellTypedInterpretation of
38  int *
39  ((Stdpp.location list * string * string) list *
40   (DisambiguateTypes.domain_item * string) list *
41   (Stdpp.location * string) Lazy.t * bool) list
42 exception PathNotWellFormed
43
44   (** raised when an environment is not enough informative to decide *)
45 exception Try_again of string Lazy.t
46
47 type ('alias,'term) aliases =
48  bool * 'term DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t
49 type 'a disambiguator_input = string * int * 'a
50
51 type domain = domain_tree list
52 and domain_tree = Node of Stdpp.location list * domain_item * domain
53
54 let mono_uris_callback ~selection_mode ?ok
55           ?(enable_button_for_non_vars = true) ~title ~msg ~id =
56  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
57       "matita.auto_disambiguation"
58  then
59   function l -> l
60  else
61   raise Ambiguous_input
62
63 let mono_interp_callback _ _ _ = raise Ambiguous_input
64
65 let _choose_uris_callback = ref mono_uris_callback
66 let _choose_interp_callback = ref mono_interp_callback
67 let set_choose_uris_callback f = _choose_uris_callback := f
68 let set_choose_interp_callback f = _choose_interp_callback := f
69
70 let interactive_user_uri_choice = !_choose_uris_callback
71 let interactive_interpretation_choice interp = !_choose_interp_callback interp
72 let input_or_locate_uri ~(title:string) ?id () = None
73   (* Zack: I try to avoid using this callback. I therefore assume that
74   * the presence of an identifier that can't be resolved via "locate"
75   * query is a syntax error *)
76   
77
78 let rec string_of_domain =
79  function
80     [] -> ""
81   | Node (_,domain_item,l)::tl ->
82      DisambiguateTypes.string_of_domain_item domain_item ^
83       " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl
84
85 let rec filter_map_domain f =
86  function
87     [] -> []
88   | Node (locs,domain_item,l)::tl ->
89      match f locs domain_item with
90         None -> filter_map_domain f l @ filter_map_domain f tl
91       | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl
92
93 let rec map_domain f =
94  function
95     [] -> []
96   | Node (locs,domain_item,l)::tl ->
97      f locs domain_item :: map_domain f l @ map_domain f tl
98
99 let uniq_domain dom =
100  let rec aux seen =
101   function
102      [] -> seen,[]
103    | Node (locs,domain_item,l)::tl ->
104       if List.mem domain_item seen then
105        let seen,l = aux seen l in
106        let seen,tl = aux seen tl in
107         seen, l @ tl
108       else
109        let seen,l = aux (domain_item::seen) l in
110        let seen,tl = aux seen tl in
111         seen, Node (locs,domain_item,l)::tl
112  in
113   snd (aux [] dom)
114
115 let debug = false
116 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
117
118 (*
119   (** print benchmark information *)
120 let benchmark = true
121 let max_refinements = ref 0       (* benchmarking is not thread safe *)
122 let actual_refinements = ref 0
123 let domain_size = ref 0
124 let choices_avg = ref 0.
125 *)
126
127 type ('term,'metasenv,'subst,'graph) test_result =
128   | Ok of 'term * 'metasenv * 'subst * 'graph
129   | Ko of (Stdpp.location * string) Lazy.t
130   | Uncertain of (Stdpp.location * string) Lazy.t
131
132 let resolve ~env ~mk_choice (item: domain_item) arg =
133   try
134    match snd (mk_choice (Environment.find item env)), arg with
135       `Num_interp f, `Num_arg n -> f n
136     | `Sym_interp f, `Args l -> f l
137     | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f []
138     | _,_ -> assert false
139   with Not_found -> 
140     failwith ("Domain item not found: " ^ 
141       (DisambiguateTypes.string_of_domain_item item))
142
143   (* TODO move it to Cic *)
144 let find_in_context name context =
145   let rec aux acc = function
146     | [] -> raise Not_found
147     | Some hd :: tl when hd = name -> acc
148     | _ :: tl ->  aux (acc + 1) tl
149   in
150   aux 1 context
151
152 let string_of_name =
153  function
154   | Ast.Ident (n, _) -> Some n
155   | _ -> assert false
156 ;;
157
158 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
159   | Ast.AttributedTerm (`Loc loc, term) ->
160      domain_of_term ~loc ~context term
161   | Ast.AttributedTerm (_, term) ->
162       domain_of_term ~loc ~context term
163   | Ast.Symbol (name, attr) ->
164       [ Node ([loc], Symbol (name,attr), []) ]
165       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
166   | Ast.Appl (Ast.Symbol (name, attr)  as hd :: args)
167   | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args)
168      ->
169       let args_dom =
170         List.fold_right
171           (fun term acc -> domain_of_term ~loc ~context term @ acc)
172           args [] in
173       let loc =
174        match hd with
175           Ast.AttributedTerm (`Loc loc,_)  -> loc
176         | _ -> loc
177       in
178        [ Node ([loc], Symbol (name,attr), args_dom) ]
179   | Ast.Appl (Ast.Ident (id,uri) as hd :: args)
180   | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) ->
181       let uri = match uri with
182         | `Uri u -> Some u
183         | _ -> None
184       in
185       let args_dom =
186         List.fold_right
187           (fun term acc -> domain_of_term ~loc ~context term @ acc)
188           args [] in
189       let loc =
190        match hd with
191           Ast.AttributedTerm (`Loc loc,_)  -> loc
192         | _ -> loc
193       in
194       (try
195         (* the next line can raise Not_found *)
196         ignore(find_in_context id context);
197           args_dom
198       with Not_found ->
199         [ Node ([loc], Id (id,uri), args_dom) ] )
200   | Ast.Appl terms ->
201       List.fold_right
202         (fun term acc -> domain_of_term ~loc ~context term @ acc)
203         terms []
204   | Ast.Binder (kind, (var, typ), body) ->
205       let type_dom = domain_of_term_option ~loc ~context typ in
206       let body_dom =
207         domain_of_term ~loc
208           ~context:(string_of_name var :: context) body in
209       (match kind with
210       | `Exists -> [ Node ([loc], Symbol ("exists",None), (type_dom @ body_dom)) ]
211       | _ -> type_dom @ body_dom)
212   | Ast.Case (term, indty_ident, outtype, branches) ->
213       let term_dom = domain_of_term ~loc ~context term in
214       let outtype_dom = domain_of_term_option ~loc ~context outtype in
215       let rec get_first_constructor = function
216         | [] -> []
217         | (Ast.Pattern (head, Some r, _), _) :: _ -> 
218              [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ]
219         | (Ast.Pattern (head, None, _), _) :: _ -> 
220              [ Node ([loc], Id (head,None), []) ]
221         | _ :: tl -> get_first_constructor tl in
222       let do_branch =
223        function
224           Ast.Pattern (head, _, args), term ->
225            let (term_context, args_domain) =
226              List.fold_left
227                (fun (cont, dom) (name, typ) ->
228                  (string_of_name name :: cont,
229                   (match typ with
230                   | None -> dom
231                   | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
232                (context, []) args
233            in
234             domain_of_term ~loc ~context:term_context term @ args_domain
235         | Ast.Wildcard, term ->
236             domain_of_term ~loc ~context term
237       in
238       let branches_dom =
239         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
240       (match indty_ident with
241        | None -> get_first_constructor branches
242        | Some (ident, None) -> [ Node ([loc], Id (ident,None) , []) ]
243        | Some (ident, Some r) -> 
244            [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ])
245       @ term_dom @ outtype_dom @ branches_dom
246   | Ast.Cast (term, ty) ->
247       let term_dom = domain_of_term ~loc ~context term in
248       let ty_dom = domain_of_term ~loc ~context ty in
249       term_dom @ ty_dom
250   | Ast.LetIn ((var, typ), body, where) ->
251       let body_dom = domain_of_term ~loc ~context body in
252       let type_dom = domain_of_term_option ~loc ~context typ in
253       let where_dom =
254         domain_of_term ~loc ~context:(string_of_name var :: context) where in
255       body_dom @ type_dom @ where_dom
256   | Ast.LetRec (kind, defs, where) ->
257       let add_defs context =
258         List.fold_left
259           (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
260           ) context defs in
261       let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
262       let defs_dom =
263         List.fold_left
264           (fun dom (params, (_, typ), body, _) ->
265             let context' =
266              add_defs
267               (List.fold_left
268                 (fun acc (var,_) -> string_of_name var :: acc)
269                 context params)
270             in
271             List.rev
272              (snd
273                (List.fold_left
274                 (fun (context,res) (var,ty) ->
275                   string_of_name var :: context,
276                   domain_of_term_option ~loc ~context ty @ res)
277                 (add_defs context,[]) params))
278             @ dom
279             @ domain_of_term_option ~loc ~context:context' typ
280             @ domain_of_term ~loc ~context:context' body
281           ) [] defs
282       in
283       defs_dom @ where_dom
284   | Ast.Ident (name, x) ->
285       let x = match x with
286         | `Uri u -> Some u
287         | _ -> None
288       in
289       (try
290         (* the next line can raise Not_found *)
291         ignore(find_in_context name context); []
292       with Not_found ->
293         (*
294         (match subst with
295         | None -> [ Node ([loc], Id name, []) ]
296         | Some subst ->
297             let terms =
298               List.fold_left
299                 (fun dom (_, term) ->
300                   let dom' = domain_of_term ~loc ~context term in
301                   dom @ dom')
302                 [] subst in
303             [ Node ([loc], Id name, terms) ]))*)
304         [ Node ([loc], Id (name,x), []) ])
305   | Ast.NRef _ -> []
306   | Ast.NCic _ -> []
307   | Ast.Implicit _ -> []
308   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
309   | Ast.Meta (index, local_context) ->
310       List.fold_left
311        (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
312        [] local_context
313   | Ast.Sort _ -> []
314   | Ast.UserInput
315   | Ast.Literal _
316   | Ast.Layout _
317   | Ast.Magic _
318   | Ast.Variable _ -> assert false
319
320 and domain_of_term_option ~loc ~context = function
321   | None -> []
322   | Some t -> domain_of_term ~loc ~context t
323
324 let domain_of_term ~context term = 
325  uniq_domain (domain_of_term ~context term)
326
327 let domain_of_obj ~context ast =
328  assert (context = []);
329   match ast with
330    | Ast.Theorem (_,_,ty,bo,_) ->
331       domain_of_term [] ty
332       @ (match bo with
333           None -> []
334         | Some bo -> domain_of_term [] bo)
335    | Ast.Inductive (params,tyl) ->
336       let context, dom = 
337        List.fold_left
338         (fun (context, dom) (var, ty) ->
339           let context' = string_of_name var :: context in
340           match ty with
341              None -> context', dom
342            | Some ty -> context', dom @ domain_of_term context ty
343         ) ([], []) params in
344       let context_w_types =
345         List.rev_map (fun (var, _, _, _) -> Some var) tyl @ context in
346       dom
347       @ List.flatten (
348          List.map
349           (fun (_,_,ty,cl) ->
350             domain_of_term context ty
351             @ List.flatten (
352                List.map
353                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
354                 tyl)
355    | Ast.Record (params,var,ty,fields) ->
356       let context, dom = 
357        List.fold_left
358         (fun (context, dom) (var, ty) ->
359           let context' = string_of_name var :: context in
360           match ty with
361              None -> context', dom
362            | Some ty -> context', dom @ domain_of_term context ty
363         ) ([], []) params in
364       let context_w_types = Some var :: context in
365       dom
366       @ domain_of_term context ty
367       @ snd
368          (List.fold_left
369           (fun (context,res) (name,ty,_,_) ->
370             Some name::context, res @ domain_of_term context ty
371           ) (context_w_types,[]) fields)
372
373 let domain_of_obj ~context obj = 
374  uniq_domain (domain_of_obj ~context obj)
375
376   (* dom1 \ dom2 *)
377 let domain_diff dom1 dom2 =
378 (* let domain_diff = Domain.diff *)
379   let is_in_dom2 elt =
380     List.exists
381      (function
382        | Symbol (symb,None) ->
383           (match elt with
384               Symbol (symb',_) when symb = symb' -> true
385             | _ -> false)
386        | Num _ ->
387           (match elt with
388               Num _ -> true
389             | _ -> false)
390        | item -> elt = item
391      ) dom2
392   in
393    let rec aux =
394     function
395        [] -> []
396      | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
397      | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
398    in
399     aux dom1
400
401 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
402
403 (* generic function lifting splitting from type T to type (T list) *) 
404 let rec list_split item_split ctx pre post =
405   match post with
406   | [] -> []
407   | x :: post' ->
408       (item_split (fun v1 -> ctx (pre@v1::post')) x)@
409         list_split item_split ctx (pre@[x]) post'
410 ;;
411
412 (* splits a 'term capture_variable *)
413 let var_split ctx = function
414   | (_,None) -> []
415   | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
416 ;;
417
418 let ity_split ctx (n,isind,ty,cl) = 
419   [(fun x -> ctx (n,isind,x,cl)),ty]@
420   list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty]) 
421     (fun x -> ctx (n,isind,ty,x)) [] cl
422 ;;
423
424 let field_split ctx (n,ty,b,m) =
425         [(fun x -> ctx (n,x,b,m)),ty]
426 ;;
427
428 (* splits a defn. in a mutual LetRec block *)
429 let letrecaux_split ctx (args,f,bo,n) =
430         list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
431         var_split (fun x -> ctx (args,x,bo,n)) f@
432         [(fun x -> ctx (args,f,x,n)),bo]
433 ;;
434
435 (* splits a pattern (for case analysis) *)
436 let pattern_split ctx = function
437   | Ast.Wildcard -> []
438   | Ast.Pattern (s,href,pl) -> 
439      let rec auxpatt pre = function
440      | [] -> []
441      | (x,Some y as x')::post' ->
442          ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
443          ::auxpatt (pre@[x']) post'
444      | (x,None as x')::post' -> auxpatt (pre@[x']) post'
445      in auxpatt [] pl
446 ;;
447
448   (* this function is used to get the children of a given node, together with
449    * their context 
450    * contexts are expressed in the form of functions Ast -> Ast *)
451 (* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
452 let rec split ctx = function
453   | Ast.AttributedTerm (attr,t) -> 
454      [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t]
455   | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl
456   | Ast.Binder (k,((n,None) as n'),body) -> 
457      [ (fun v -> ctx (Ast.Binder (k,n',v))),body]
458   | Ast.Binder (k,((n,Some ty) as n'),body) -> 
459      [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty 
460      ;(fun v -> ctx (Ast.Binder (k,n',v))),body]
461   | Ast.Case (t,ity,outty,pl) -> 
462      let outty_split = match outty with
463      | None -> []
464      | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
465      in
466      ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
467        outty_split@list_split
468          (fun ctx0 (p,x) -> 
469             ((fun y -> ctx0 (p,y)),x)::pattern_split 
470               (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
471               [] pl
472   | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u
473                   ; (fun x -> ctx (Ast.Cast (u,x))),v ]
474   | Ast.LetIn ((n,None) as n',u,v) ->
475                   [ (fun x -> ctx (Ast.LetIn (n',x,v))), u
476                   ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
477   | Ast.LetIn ((n,Some t) as n',u,v) ->
478                   [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t
479                   ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
480                   ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
481   | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
482       list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
483   | _ -> [] (* leaves *)
484 ;;
485
486
487 (* top_split : 'a -> ((term -> 'a) * term) list
488  * returns all the possible top-level (ctx,t) for its input *)
489 let bfvisit ~pp_term top_split test t = 
490   let rec aux = function
491   | [] -> None
492   | (ctx0,t0 as hd)::tl ->
493 (*      prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
494       prerr_endline ("t0 = " ^ pp_term t0); 
495       if test t0 then (prerr_endline "caso 1"; Some hd)
496       else 
497               let t0' = split ctx0 t0 in
498               (prerr_endline ("caso 2: length t0' = " ^ string_of_int
499               (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
500   (* in aux [(fun x -> x),t] *)
501   in aux (top_split t)
502 ;;
503
504 let obj_split (o:Ast.term Ast.obj) = match o with
505   | Ast.Inductive (ls,itl) -> 
506       list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
507       list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl 
508   | Ast.Theorem (flav,n,ty,None,p) ->
509       [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty]
510   | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
511       [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty
512       ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
513   | Ast.Record (ls,n,ty,fl) ->
514       list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
515       [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
516       list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl 
517 ;;
518
519 let bfvisit_obj = bfvisit obj_split;;
520
521 let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;;
522
523 (*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
524   let mk_alias = function
525     | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
526     | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
527     | Ast.Num _ -> DisambiguateTypes.Num None
528     | _ -> assert false
529   in
530   let lookup_choices =
531      fun item ->
532       (*match universe with
533       | None -> 
534           lookup_in_library 
535             interactive_user_uri_choice 
536             input_or_locate_uri item
537       | Some e ->
538           (try Environment.find item e
539           with Not_found -> [])
540 *)
541           (try Environment.find item universe
542           with Not_found -> [])
543    in
544    match t with
545    | Ast.Ident (_,None)
546    | Ast.Num (_,None) 
547    | Ast.Symbol (_,None) -> 
548        let choices = lookup_choices (mk_alias t) in
549        if List.length choices <> 1 then t
550        else List.hd choices
551      (* but we lose info on closedness *)
552    | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t
553 ;;
554 *)
555
556 let domain_item_of_ast = function
557   | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
558   | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
559   | Ast.Num (n,_) -> DisambiguateTypes.Num None
560   | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
561   | _ -> assert false
562 ;;
563
564 let ast_of_alias_spec t alias = match (t,alias) with
565   | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
566   | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) -> 
567       Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
568   | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
569   | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
570   | _ -> assert false
571 ;;
572
573 let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri 
574   ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
575   try
576    let localization_tbl = mk_localization_tbl 503 in
577     let cic_thing =
578       interpretate_thing ~context ~env
579        ~uri ~is_path:false t ~localization_tbl
580     in
581     let foo () =
582            refine_thing metasenv subst context uri
583             ~use_coercions cic_thing expty ugraph ~localization_tbl
584     in match (refine_profiler.HExtlib.profile foo ()) with
585     | Ko _ -> false
586     | _ -> true
587   with
588      (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
589      | Invalid_choice loc_msg -> Ko loc_msg*)
590      | Invalid_choice _ -> false
591      | _ -> true
592 ;;
593
594 let rec disambiguate_list
595   ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
596   ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts =
597   let disambiguate_list = 
598     disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
599       ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
600       ~mk_localization_tbl ~pp_thing ~pp_term
601   in
602   let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty 
603     ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
604   in
605   let find_choices item = 
606     let a2s = function
607     | GrafiteAst.Ident_alias (id,_)
608     | GrafiteAst.Symbol_alias (id,_,_) -> id
609     | GrafiteAst.Number_alias _ -> "NUM"
610     in
611     let d2s = function
612     | Id (id,_)
613     | Symbol (id,_) -> id
614     | Num _ -> "NUM"
615     in
616     let res =
617       Environment.find item universe 
618     in
619     prerr_endline (Printf.sprintf "choices for %s :\n%s"
620       (d2s item) (String.concat ", " (List.map a2s res)));
621     res
622   in
623
624   let get_instances ctx t = 
625     try 
626       let choices = find_choices (domain_item_of_ast t) in
627       List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices
628     with
629     | Not_found -> []
630   in
631
632   match ts with
633   | [] -> None
634   | t0 :: tl ->
635       prerr_endline ("disambiguation of t0 = " ^ pp_thing t0); 
636       let is_ambiguous = function
637       | Ast.Ident (_,`Ambiguous)
638       | Ast.Num (_,None)
639       | Ast.Symbol (_,None) -> true
640       | Ast.Case (_,Some (ity,None),_,_) -> 
641           (prerr_endline ("ambiguous case" ^ ity);true)
642       | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
643       | Ast.Case (_,Some (ity,Some r),_,_) -> 
644           (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
645       | Ast.Ident (n,`Uri u) -> 
646           (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
647       | _ -> false
648       in
649       let astpp = function
650               | Ast.Ident (id,_) -> "ID " ^ id
651               | Ast.Num _ -> "NUM"
652               | Ast.Symbol (sym,_) -> "SYM " ^ sym
653               | _ -> "ERROR!"
654       in
655       (* get first ambiguous subterm (or return disambiguated term) *)
656       match visit ~pp_term is_ambiguous t0 with
657       | None -> 
658           prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
659           Some (t0,tl)
660       | Some (ctx, t) -> 
661         prerr_endline ("disambiguating node " ^ astpp t ^
662         "\nin " ^ pp_thing (ctx t));
663         (* get possible instantiations of t *)
664         let instances = get_instances ctx t in
665         (* perforate ambiguous subterms and test refinement *)
666         let survivors = List.filter test_interpr instances in
667         disambiguate_list (survivors@tl) 
668 ;;
669
670
671 (*  let rec aux l =
672     match l with
673     | [] -> None
674     | (ctx,u)::vl -> 
675         if test u 
676           then (ctx,u)
677           else aux (vl@split ctx u)
678   in aux [t]
679 ;;*) 
680
681 (* let rec instantiate_ast = function
682   | Ident (n,Some _)
683   | Symbol (s,Some _)
684   | Num (n,Some _) as t -> []
685   | Ident (n,None) -> (* output: all possible instantiations of n *)
686   | Symbol (s,None) ->
687   | Num (n,None) -> 
688
689
690   | AttributedTerm (a,u) -> AttributedTerm (a,f u)
691   | Appl tl -> Appl (List.map f tl)
692   | Binder (k,n,body) -> Binder (k,n,f body)
693   | Case (t,ity,oty,pl) -> 
694       let pl' = List.map (fun (p,u) -> p,f u) pl in 
695       Case (f t,ity,map_option f oty,pl')
696   | Cast (u,v) -> Cast (f u,f v)
697   | LetIn (n,u,v) -> LetIn (n,f u,f v)
698   | LetRec -> ada (* TODO *)
699   | t -> t
700 *)
701
702 let disambiguate_thing 
703   ~context ~metasenv ~subst ~use_coercions
704   ~string_context_of_context
705   ~initial_ugraph:base_univ ~expty
706   ~mk_implicit ~description_of_alias ~fix_instance
707   ~aliases ~universe ~lookup_in_library 
708   ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing 
709   ~visit ~mk_localization_tbl
710   (thing_txt,thing_txt_prefix_len,thing)
711 =
712 (* XXX: will be thrown away *)
713   let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing 
714   in
715   let rec aux_env env = function
716    | [] -> env
717    | Node (_, item, l) :: tl ->
718        let env =
719          Environment.add item
720           (mk_implicit
721             (match item with | Id _ | Num _ -> true | Symbol _ -> false))
722           env in
723        aux_env (aux_env env l) tl in
724   let env = aux_env aliases todo_dom in
725
726   let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty 
727     ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
728   in
729 (* real function *)
730   let rec aux tl =
731     match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
732       ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
733       ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
734       ~pp_term tl with
735     | None -> []
736     | Some (t,tl') -> t::aux tl'
737   in
738
739   let refine t = 
740     let localization_tbl = mk_localization_tbl 503 in
741     match refine_thing metasenv subst context uri
742       ~use_coercions
743       (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
744       expty base_univ ~localization_tbl with
745     | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
746     | Uncertain x ->
747         let _,err = Lazy.force x in
748         prerr_endline ("refinement uncertain after disambiguation: " ^ err);
749         assert false
750     | _ -> assert false
751   in
752   if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
753   else
754     let res = aux [thing] in
755     let res =
756       HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res
757     in
758     match res with
759     | [] -> raise (NoWellTypedInterpretation (0,[]))
760     | [t] -> res,false
761     | _ -> res,true
762 ;;
763
764 (*
765 let disambiguate_thing 
766   ~context ~metasenv ~subst ~use_coercions
767   ~string_context_of_context
768   ~initial_ugraph:base_univ ~expty
769   ~mk_implicit ~description_of_alias ~fix_instance
770   ~aliases ~universe ~lookup_in_library 
771   ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
772   ~mk_localization_tbl
773   (thing_txt,thing_txt_prefix_len,thing)
774 =
775   debug_print (lazy "DISAMBIGUATE INPUT");
776   debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
777   let thing_dom =
778     domain_of_thing ~context:(string_context_of_context context) thing in
779   debug_print
780    (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
781    let current_dom =
782      Environment.fold (fun item _ dom -> item :: dom) aliases [] in
783    let todo_dom = domain_diff thing_dom current_dom in
784    debug_print
785     (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
786    (* (2) lookup function for any item (Id/Symbol/Num) *)
787    let lookup_choices =
788      fun item ->
789       match universe with
790       | None -> 
791           lookup_in_library 
792             interactive_user_uri_choice 
793             input_or_locate_uri item
794       | Some e ->
795           (try
796             fix_instance item (Environment.find item e)
797           with Not_found -> [])
798    in
799
800    (* items with 1 choice are interpreted ASAP *)
801    let aliases, todo_dom = 
802      let rec aux (aliases,acc) = function 
803        | [] -> aliases, acc
804        | (Node (_, item,extra) as node) :: tl -> 
805            let choices = lookup_choices item in
806            if List.length choices <> 1 then aux (aliases, acc@[node]) tl
807            else
808            let tl = tl @ extra in
809            if Environment.mem item aliases then aux (aliases, acc) tl
810            else aux (Environment.add item (List.hd choices) aliases, acc) tl
811      in
812        aux (aliases,[]) todo_dom
813    in
814
815 (*
816       (* <benchmark> *)
817       let _ =
818         if benchmark then begin
819           let per_item_choices =
820             List.map
821               (fun dom_item ->
822                 try
823                   let len = List.length (lookup_choices dom_item) in
824                   debug_print (lazy (sprintf "BENCHMARK %s: %d"
825                     (string_of_domain_item dom_item) len));
826                   len
827                 with No_choices _ -> 0)
828               thing_dom
829           in
830           max_refinements := List.fold_left ( * ) 1 per_item_choices;
831           actual_refinements := 0;
832           domain_size := List.length thing_dom;
833           choices_avg :=
834             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
835         end
836       in
837       (* </benchmark> *)
838 *)
839
840    (* (3) test an interpretation filling with meta uninterpreted identifiers
841     *)
842    let test_env aliases todo_dom ugraph = 
843      try
844       let rec aux env = function
845        | [] -> env
846        | Node (_, item, l) :: tl ->
847            let env =
848              Environment.add item
849               (mk_implicit
850                 (match item with | Id _ | Num _ -> true | Symbol _ -> false))
851               env in
852            aux (aux env l) tl in
853       let filled_env = aux aliases todo_dom in
854       let localization_tbl = mk_localization_tbl 503 in
855        let cic_thing =
856          interpretate_thing ~context ~env:filled_env
857           ~uri ~is_path:false thing ~localization_tbl
858        in
859 let foo () =
860         refine_thing metasenv subst context uri
861          ~use_coercions cic_thing expty ugraph ~localization_tbl
862 in refine_profiler.HExtlib.profile foo ()
863      with
864      | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
865      | Invalid_choice loc_msg -> Ko loc_msg
866    in
867    (* (4) build all possible interpretations *)
868    let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
869    (* aux returns triples Ok/Uncertain/Ko *)
870    (* rem_dom is the concatenation of all the remainin domains *)
871    let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
872      debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
873      match todo_dom with
874      | [] ->
875          assert (lookup_in_todo_dom = None);
876          (match test_env aliases rem_dom base_univ with
877          | Ok (thing, metasenv,subst,new_univ) -> 
878             [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
879          | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
880          | Uncertain loc_msg ->
881             [],[aliases,diff,loc_msg],[])
882      | Node (locs,item,inner_dom) :: remaining_dom ->
883          debug_print (lazy (sprintf "CHOOSED ITEM: %s"
884           (string_of_domain_item item)));
885          let choices =
886           match lookup_in_todo_dom with
887              None -> lookup_choices item
888            | Some choices -> choices in
889          match choices with
890             [] ->
891              [], [],
892               [aliases, diff, 
893                (lazy (List.hd locs,
894                  "No choices for " ^ string_of_domain_item item)),
895                true]
896 (*
897           | [codomain_item] ->
898               (* just one choice. We perform a one-step look-up and
899                  if the next set of choices is also a singleton we
900                  skip this refinement step *)
901               debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
902               let new_env = Environment.add item codomain_item aliases in
903               let new_diff = (item,codomain_item)::diff in
904               let lookup_in_todo_dom,next_choice_is_single =
905                match remaining_dom with
906                   [] -> None,false
907                 | (_,he)::_ ->
908                    let choices = lookup_choices he in
909                     Some choices,List.length choices = 1
910               in
911                if next_choice_is_single then
912                 aux new_env new_diff lookup_in_todo_dom remaining_dom
913                  base_univ
914                else
915                  (match test_env new_env remaining_dom base_univ with
916                  | Ok (thing, metasenv),new_univ ->
917                      (match remaining_dom with
918                      | [] ->
919                         [ new_env, new_diff, metasenv, thing, new_univ ], []
920                      | _ ->
921                         aux new_env new_diff lookup_in_todo_dom
922                          remaining_dom new_univ)
923                  | Uncertain (loc,msg),new_univ ->
924                      (match remaining_dom with
925                      | [] -> [], [new_env,new_diff,loc,msg,true]
926                      | _ ->
927                         aux new_env new_diff lookup_in_todo_dom
928                          remaining_dom new_univ)
929                  | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
930 *)
931           | _::_ ->
932               let mark_not_significant failures =
933                 List.map
934                  (fun (env, diff, loc_msg, _b) ->
935                    env, diff, loc_msg, false)
936                  failures in
937               let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
938                if ok_l <> [] || uncertain_l <> [] then
939                 ok_l,uncertain_l,mark_not_significant error_l
940                else
941                 outcome in
942             let rec filter = function 
943              | [] -> [],[],[]
944              | codomain_item :: tl ->
945                  (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
946                 let new_env = Environment.add item codomain_item aliases in
947                 let new_diff = (item,codomain_item)::diff in
948                 (match
949                   test_env new_env 
950                     (inner_dom@remaining_dom@rem_dom) base_univ
951                  with
952                 | Ok (thing, metasenv,subst,new_univ) ->
953 (*                     prerr_endline "OK"; *)
954                     let res = 
955                       (match inner_dom with
956                       | [] ->
957                          [new_env,new_diff,metasenv,subst,thing,new_univ],
958                          [], []
959                       | _ ->
960                          aux new_env new_diff None inner_dom
961                           (remaining_dom@rem_dom) 
962                       ) 
963                     in
964                      res @@ filter tl
965                 | Uncertain loc_msg ->
966 (*                     prerr_endline ("UNCERTAIN"); *)
967                     let res =
968                       (match inner_dom with
969                       | [] -> [],[new_env,new_diff,loc_msg],[]
970                       | _ ->
971                          aux new_env new_diff None inner_dom
972                           (remaining_dom@rem_dom) 
973                       )
974                     in
975                      res @@ filter tl
976                 | Ko loc_msg ->
977 (*                     prerr_endline "KO"; *)
978                     let res = [],[],[new_env,new_diff,loc_msg,true] in
979                      res @@ filter tl)
980            in
981             let ok_l,uncertain_l,error_l =
982              classify_errors (filter choices)
983             in
984              let res_after_ok_l =
985               List.fold_right
986                (fun (env,diff,_,_,_,_) res ->
987                  aux env diff None remaining_dom rem_dom @@ res
988                ) ok_l ([],[],error_l)
989             in
990              List.fold_right
991               (fun (env,diff,_) res ->
992                 aux env diff None remaining_dom rem_dom @@ res
993               ) uncertain_l res_after_ok_l
994   in
995   let aux' aliases diff lookup_in_todo_dom todo_dom =
996    if todo_dom = [] then
997      aux aliases diff lookup_in_todo_dom todo_dom [] 
998    else
999      match test_env aliases todo_dom base_univ with
1000       | Ok _ 
1001       | Uncertain _ ->
1002          aux aliases diff lookup_in_todo_dom todo_dom [] 
1003       | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
1004   in
1005     let res =
1006      match aux' aliases [] None todo_dom with
1007      | [],uncertain,errors ->
1008         let errors =
1009          List.map
1010           (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
1011           ) uncertain @ errors
1012         in
1013         let errors =
1014          List.map
1015           (fun (env,diff,loc_msg,significant) ->
1016             let env' =
1017              filter_map_domain
1018                (fun locs domain_item ->
1019                  try
1020                   let description =
1021                    description_of_alias (Environment.find domain_item env)
1022                   in
1023                    Some (locs,descr_of_domain_item domain_item,description)
1024                  with
1025                   Not_found -> None)
1026                thing_dom
1027             in
1028             let diff= List.map (fun a,b -> a,description_of_alias b) diff in
1029              env',diff,loc_msg,significant
1030           ) errors
1031         in
1032          raise (NoWellTypedInterpretation (0,errors))
1033      | [_,diff,metasenv,subst,t,ugraph],_,_ ->
1034          debug_print (lazy "SINGLE INTERPRETATION");
1035          [diff,metasenv,subst,t,ugraph], false
1036      | l,_,_ ->
1037          debug_print 
1038            (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1039          let choices =
1040            List.map
1041              (fun (env, _, _, _, _, _) ->
1042                map_domain
1043                  (fun locs domain_item ->
1044                    let description =
1045                      description_of_alias (Environment.find domain_item env)
1046                    in
1047                    locs,descr_of_domain_item domain_item, description)
1048                  thing_dom)
1049              l
1050          in
1051          let choosed = 
1052            interactive_interpretation_choice 
1053              thing_txt thing_txt_prefix_len choices 
1054          in
1055          (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
1056            choosed),
1057           true
1058     in
1059      res
1060      *)