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      *)