helm/software/components/cic_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 open UriManager
  32
  33 module Ast = CicNotationPt
  34
  35 (* the integer is an offset to be added to each location *)
  36 exception NoWellTypedInterpretation of
  37  int *
  38  ((Stdpp.location list * string * string) list *
  39   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
  40   Stdpp.location option * string Lazy.t * bool) list
  41 exception PathNotWellFormed
  42
  43   (** raised when an environment is not enough informative to decide *)
  44 exception Try_again of string Lazy.t
  45
  46 type aliases = bool * DisambiguateTypes.environment
  47 type 'a disambiguator_input = string * int * 'a
  48
  49 type domain = domain_tree list
  50 and domain_tree = Node of Stdpp.location list * domain_item * domain
  51
  52 let rec string_of_domain =
  53  function
  54     [] -> ""
  55   | Node (_,domain_item,l)::tl ->
  56      DisambiguateTypes.string_of_domain_item domain_item ^
  57       " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl
  58
  59 let rec filter_map_domain f =
  60  function
  61     [] -> []
  62   | Node (locs,domain_item,l)::tl ->
  63      match f locs domain_item with
  64         None -> filter_map_domain f l @ filter_map_domain f tl
  65       | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl
  66
  67 let rec map_domain f =
  68  function
  69     [] -> []
  70   | Node (locs,domain_item,l)::tl ->
  71      f locs domain_item :: map_domain f l @ map_domain f tl
  72
  73 let uniq_domain dom =
  74  let rec aux seen =
  75   function
  76      [] -> seen,[]
  77    | Node (locs,domain_item,l)::tl ->
  78       if List.mem domain_item seen then
  79        let seen,l = aux seen l in
  80        let seen,tl = aux seen tl in
  81         seen, l @ tl
  82       else
  83        let seen,l = aux (domain_item::seen) l in
  84        let seen,tl = aux seen tl in
  85         seen, Node (locs,domain_item,l)::tl
  86  in
  87   snd (aux [] dom)
  88
  89 let debug = false
  90 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  91
  92 (*
  93   (** print benchmark information *)
  94 let benchmark = true
  95 let max_refinements = ref 0       (* benchmarking is not thread safe *)
  96 let actual_refinements = ref 0
  97 let domain_size = ref 0
  98 let choices_avg = ref 0.
  99 *)
 100
 101 let descr_of_domain_item = function
 102  | Id s -> s
 103  | Symbol (s, _) -> s
 104  | Num i -> string_of_int i
 105
 106 type ('a,'m) test_result =
 107   | Ok of 'a * 'm
 108   | Ko of Stdpp.location option * string Lazy.t
 109   | Uncertain of Stdpp.location option * string Lazy.t
 110
 111 let refine_term metasenv context uri term ugraph ~localization_tbl =
 112 (*   if benchmark then incr actual_refinements; *)
 113   assert (uri=None);
 114     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
 115     try
 116       let term', _, metasenv',ugraph1 =
 117         CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
 118         (Ok (term', metasenv')),ugraph1
 119     with
 120      exn ->
 121       let rec process_exn loc =
 122        function
 123           HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
 124         | CicRefine.Uncertain msg ->
 125             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
 126             Uncertain (loc,msg),ugraph
 127         | CicRefine.RefineFailure msg ->
 128             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
 129               (CicPp.ppterm term) (Lazy.force msg)));
 130             Ko (loc,msg),ugraph
 131        | exn -> raise exn
 132       in
 133        process_exn None exn
 134
 135 let refine_obj metasenv context uri obj ugraph ~localization_tbl =
 136  assert (context = []);
 137    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
 138    try
 139      let obj', metasenv,ugraph =
 140       CicRefine.typecheck metasenv uri obj ~localization_tbl
 141      in
 142        (Ok (obj', metasenv)),ugraph
 143    with
 144      exn ->
 145       let rec process_exn loc =
 146        function
 147           HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
 148         | CicRefine.Uncertain msg ->
 149             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
 150             Uncertain (loc,msg),ugraph
 151         | CicRefine.RefineFailure msg ->
 152             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
 153               (CicPp.ppobj obj) (Lazy.force msg))) ;
 154             Ko (loc,msg),ugraph
 155        | exn -> raise exn
 156       in
 157        process_exn None exn
 158
 159 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
 160   try
 161     snd (Environment.find item env) env num args
 162   with Not_found ->
 163     failwith ("Domain item not found: " ^
 164       (DisambiguateTypes.string_of_domain_item item))
 165
 166   (* TODO move it to Cic *)
 167 let find_in_context name context =
 168   let rec aux acc = function
 169     | [] -> raise Not_found
 170     | Cic.Name hd :: tl when hd = name -> acc
 171     | _ :: tl ->  aux (acc + 1) tl
 172   in
 173   aux 1 context
 174
 175 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 176      ~localization_tbl
 177 =
 178   (* create_dummy_ids shouldbe used only for interpretating patterns *)
 179   assert (uri = None);
 180   let rec aux ~localize loc context = function
 181     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
 182         let res = aux ~localize loc context term in
 183          if localize then Cic.CicHash.add localization_tbl res loc;
 184          res
 185     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
 186     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
 187         let cic_args = List.map (aux ~localize loc context) args in
 188         resolve env (Symbol (symb, i)) ~args:cic_args ()
 189     | CicNotationPt.Appl terms ->
 190        Cic.Appl (List.map (aux ~localize loc context) terms)
 191     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
 192         let cic_type = aux_option ~localize loc context (Some `Type) typ in
 193         let cic_name = CicNotationUtil.cic_name_of_name var in
 194         let cic_body = aux ~localize loc (cic_name :: context) body in
 195         (match binder_kind with
 196         | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
 197         | `Pi
 198         | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
 199         | `Exists ->
 200             resolve env (Symbol ("exists", 0))
 201               ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
 202     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
 203         let cic_term = aux ~localize loc context term in
 204         let cic_outtype = aux_option ~localize loc context None outtype in
 205         let do_branch ((head, _, args), term) =
 206          let rec do_branch' context = function
 207            | [] -> aux ~localize loc context term
 208            | (name, typ) :: tl ->
 209                let cic_name = CicNotationUtil.cic_name_of_name name in
 210                let cic_body = do_branch' (cic_name :: context) tl in
 211                let typ =
 212                  match typ with
 213                  | None -> Cic.Implicit (Some `Type)
 214                  | Some typ -> aux ~localize loc context typ
 215                in
 216                Cic.Lambda (cic_name, typ, cic_body)
 217          in
 218           do_branch' context args
 219         in
 220         let indtype_uri, indtype_no =
 221           if create_dummy_ids then
 222             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
 223           else
 224           match indty_ident with
 225           | Some (indty_ident, _) ->
 226              (match resolve env (Id indty_ident) () with
 227               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
 228               | Cic.Implicit _ ->
 229                  raise (Try_again (lazy "The type of the term to be matched
 230                   is still unknown"))
 231               | _ ->
 232                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
 233           | None ->
 234               let rec fst_constructor =
 235                 function
 236                    (Ast.Pattern (head, _, _), _) :: _ -> head
 237                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
 238                  | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
 239               in
 240               (match resolve env (Id (fst_constructor branches)) () with
 241               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
 242                   (indtype_uri, indtype_no)
 243               | Cic.Implicit _ ->
 244                  raise (Try_again (lazy "The type of the term to be matched
 245                   is still unknown"))
 246               | _ ->
 247                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
 248         in
 249         let branches =
 250          if create_dummy_ids then
 251           List.map
 252            (function
 253                Ast.Wildcard,term -> ("wildcard",None,[]), term
 254              | Ast.Pattern _,_ ->
 255                 raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
 256            ) branches
 257          else
 258          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
 259             Cic.InductiveDefinition (il,_,leftsno,_) ->
 260              let _,_,_,cl =
 261               try
 262                List.nth il indtype_no
 263               with _ -> assert false
 264              in
 265               let rec count_prod t =
 266                 match CicReduction.whd [] t with
 267                     Cic.Prod (_, _, t) -> 1 + (count_prod t)
 268                   | _ -> 0
 269               in
 270               let rec sort branches cl =
 271                match cl with
 272                   [] ->
 273                    let rec analyze unused unrecognized useless =
 274                     function
 275                        [] ->
 276                         if unrecognized != [] then
 277                          raise (Invalid_choice
 278                           (Some loc,
 279                            lazy
 280                             ("Unrecognized constructors: " ^
 281                              String.concat " " unrecognized)))
 282                         else if useless > 0 then
 283                          raise (Invalid_choice
 284                           (Some loc,
 285                            lazy
 286                             ("The last " ^ string_of_int useless ^
 287                              "case" ^ if useless > 1 then "s are" else " is" ^
 288                              " unused")))
 289                         else
 290                          []
 291                      | (Ast.Wildcard,_)::tl when not unused ->
 292                          analyze true unrecognized useless tl
 293                      | (Ast.Pattern (head,_,_),_)::tl when not unused ->
 294                          analyze unused (head::unrecognized) useless tl
 295                      | _::tl -> analyze unused unrecognized (useless + 1) tl
 296                    in
 297                     analyze false [] 0 branches
 298                 | (name,ty)::cltl ->
 299                    let rec find_and_remove =
 300                     function
 301                        [] ->
 302                         raise
 303                          (Invalid_choice
 304                           (Some loc, lazy ("Missing case: " ^ name)))
 305                      | ((Ast.Wildcard, _) as branch :: _) as branches ->
 306                          branch, branches
 307                      | (Ast.Pattern (name',_,_),_) as branch :: tl
 308                         when name = name' ->
 309                          branch,tl
 310                      | branch::tl ->
 311                         let found,rest = find_and_remove tl in
 312                          found, branch::rest
 313                    in
 314                     let branch,tl = find_and_remove branches in
 315                     match branch with
 316                        Ast.Pattern (name,y,args),term ->
 317                         if List.length args = count_prod ty - leftsno then
 318                          ((name,y,args),term)::sort tl cltl
 319                         else
 320                          raise
 321                           (Invalid_choice
 322                            (Some loc,
 323                              lazy ("Wrong number of arguments for " ^ name)))
 324                      | Ast.Wildcard,term ->
 325                         let rec mk_lambdas =
 326                          function
 327                             0 -> term
 328                           | n ->
 329                              CicNotationPt.Binder
 330                               (`Lambda, (CicNotationPt.Ident ("_", None), None),
 331                                 mk_lambdas (n - 1))
 332                         in
 333                          (("wildcard",None,[]),
 334                           mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
 335               in
 336                sort branches cl
 337           | _ -> assert false
 338         in
 339         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
 340           (List.map do_branch branches))
 341     | CicNotationPt.Cast (t1, t2) ->
 342         let cic_t1 = aux ~localize loc context t1 in
 343         let cic_t2 = aux ~localize loc context t2 in
 344         Cic.Cast (cic_t1, cic_t2)
 345     | CicNotationPt.LetIn ((name, typ), def, body) ->
 346         let cic_def = aux ~localize loc context def in
 347         let cic_name = CicNotationUtil.cic_name_of_name name in
 348         let cic_typ =
 349           match typ with
 350           | None -> Cic.Implicit (Some `Type)
 351           | Some t -> aux ~localize loc context t
 352         in
 353         let cic_body = aux ~localize loc (cic_name :: context) body in
 354         Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
 355     | CicNotationPt.LetRec (kind, defs, body) ->
 356         let context' =
 357           List.fold_left
 358             (fun acc (_, (name, _), _, _) ->
 359               CicNotationUtil.cic_name_of_name name :: acc)
 360             context defs
 361         in
 362         let cic_body =
 363          let unlocalized_body = aux ~localize:false loc context' body in
 364          match unlocalized_body with
 365             Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
 366           | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
 367              (try
 368                let l' =
 369                 List.map
 370                  (function t ->
 371                    let t',subst,metasenv =
 372                     CicMetaSubst.delift_rels [] [] (List.length defs) t
 373                    in
 374                     assert (subst=[]);
 375                     assert (metasenv=[]);
 376                     t') l
 377                in
 378                 (* We can avoid the LetIn. But maybe we need to recompute l'
 379                    so that it is localized *)
 380                 if localize then
 381                  match body with
 382                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
 383                      (* since we avoid the letin, the context has no
 384                       * recfuns in it *)
 385                      let l' = List.map (aux ~localize loc context) l in
 386                       `AvoidLetIn (n,l')
 387                   | _ -> assert false
 388                 else
 389                  `AvoidLetIn (n,l')
 390               with
 391                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 392                 if localize then
 393                  `AddLetIn (aux ~localize loc context' body)
 394                 else
 395                  `AddLetIn unlocalized_body)
 396           | _ ->
 397              if localize then
 398               `AddLetIn (aux ~localize loc context' body)
 399              else
 400               `AddLetIn unlocalized_body
 401         in
 402         let inductiveFuns =
 403           List.map
 404             (fun (params, (name, typ), body, decr_idx) ->
 405               let add_binders kind t =
 406                List.fold_right
 407                 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
 408               in
 409               let cic_body =
 410                aux ~localize loc context' (add_binders `Lambda body) in
 411               let cic_type =
 412                aux_option ~localize loc context (Some `Type)
 413                 (HExtlib.map_option (add_binders `Pi) typ) in
 414               let name =
 415                 match CicNotationUtil.cic_name_of_name name with
 416                 | Cic.Anonymous ->
 417                     CicNotationPt.fail loc
 418                       "Recursive functions cannot be anonymous"
 419                 | Cic.Name name -> name
 420               in
 421               (name, decr_idx, cic_type, cic_body))
 422             defs
 423         in
 424         let fix_or_cofix n =
 425          match kind with
 426             `Inductive -> Cic.Fix (n,inductiveFuns)
 427           | `CoInductive ->
 428               let coinductiveFuns =
 429                 List.map
 430                  (fun (name, _, typ, body) -> name, typ, body)
 431                  inductiveFuns
 432               in
 433                Cic.CoFix (n,coinductiveFuns)
 434         in
 435          let counter = ref ~-1 in
 436          let build_term funs (var,_,ty,_) t =
 437           incr counter;
 438           Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
 439          in
 440           (match cic_body with
 441               `AvoidLetInNoAppl n ->
 442                 let n' = List.length inductiveFuns - n in
 443                  fix_or_cofix n'
 444             | `AvoidLetIn (n,l) ->
 445                 let n' = List.length inductiveFuns - n in
 446                  Cic.Appl (fix_or_cofix n'::l)
 447             | `AddLetIn cic_body ->
 448                 List.fold_right (build_term inductiveFuns) inductiveFuns
 449                  cic_body)
 450     | CicNotationPt.Ident _
 451     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
 452     | CicNotationPt.Ident (name, subst)
 453     | CicNotationPt.Uri (name, subst) as ast ->
 454         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
 455         (try
 456           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
 457           let index = find_in_context name context in
 458           if subst <> None then
 459             CicNotationPt.fail loc "Explicit substitutions not allowed here";
 460           Cic.Rel index
 461         with Not_found ->
 462           let cic =
 463             if is_uri ast then  (* we have the URI, build the term out of it *)
 464               try
 465                 CicUtil.term_of_uri (UriManager.uri_of_string name)
 466               with UriManager.IllFormedUri _ ->
 467                 CicNotationPt.fail loc "Ill formed URI"
 468             else
 469               resolve env (Id name) ()
 470           in
 471           let mk_subst uris =
 472             let ids_to_uris =
 473               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
 474             in
 475             (match subst with
 476             | Some subst ->
 477                 List.map
 478                   (fun (s, term) ->
 479                     (try
 480                       List.assoc s ids_to_uris, aux ~localize loc context term
 481                      with Not_found ->
 482                        raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
 483                   subst
 484             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
 485           in
 486           (try
 487             match cic with
 488             | Cic.Const (uri, []) ->
 489                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 490                 let uris = CicUtil.params_of_obj o in
 491                 Cic.Const (uri, mk_subst uris)
 492             | Cic.Var (uri, []) ->
 493                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 494                 let uris = CicUtil.params_of_obj o in
 495                 Cic.Var (uri, mk_subst uris)
 496             | Cic.MutInd (uri, i, []) ->
 497                (try
 498                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 499                  let uris = CicUtil.params_of_obj o in
 500                  Cic.MutInd (uri, i, mk_subst uris)
 501                 with
 502                  CicEnvironment.Object_not_found _ ->
 503                   (* if we are here it is probably the case that during the
 504                      definition of a mutual inductive type we have met an
 505                      occurrence of the type in one of its constructors.
 506                      However, the inductive type is not yet in the environment
 507                   *)
 508                   (*here the explicit_named_substituion is assumed to be of length 0 *)
 509                   Cic.MutInd (uri,i,[]))
 510             | Cic.MutConstruct (uri, i, j, []) ->
 511                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 512                 let uris = CicUtil.params_of_obj o in
 513                 Cic.MutConstruct (uri, i, j, mk_subst uris)
 514             | Cic.Meta _ | Cic.Implicit _ as t ->
 515 (*
 516                 debug_print (lazy (sprintf
 517                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
 518                   (CicPp.ppterm t)
 519                   (String.concat "; "
 520                     (List.map
 521                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
 522                       subst))));
 523 *)
 524                 t
 525             | _ ->
 526               raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
 527            with
 528              CicEnvironment.CircularDependency _ ->
 529                raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
 530     | CicNotationPt.Implicit -> Cic.Implicit None
 531     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
 532     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
 533     | CicNotationPt.Meta (index, subst) ->
 534         let cic_subst =
 535           List.map
 536             (function
 537                 None -> None
 538               | Some term -> Some (aux ~localize loc context term))
 539             subst
 540         in
 541         Cic.Meta (index, cic_subst)
 542     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
 543     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
 544     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
 545     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
 546     | CicNotationPt.Symbol (symbol, instance) ->
 547         resolve env (Symbol (symbol, instance)) ()
 548     | _ -> assert false (* god bless Bologna *)
 549   and aux_option ~localize loc context annotation = function
 550     | None -> Cic.Implicit annotation
 551     | Some term -> aux ~localize loc context term
 552   in
 553    aux ~localize:true HExtlib.dummy_floc context ast
 554
 555 let interpretate_path ~context path =
 556  let localization_tbl = Cic.CicHash.create 23 in
 557   (* here we are throwing away useful localization informations!!! *)
 558   fst (
 559    interpretate_term ~create_dummy_ids:true
 560     ~context ~env:Environment.empty ~uri:None ~is_path:true
 561     path ~localization_tbl, localization_tbl)
 562
 563 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
 564  assert (context = []);
 565  assert (is_path = false);
 566  let interpretate_term = interpretate_term ~localization_tbl in
 567  match obj with
 568   | CicNotationPt.Inductive (params,tyl) ->
 569      let uri = match uri with Some uri -> uri | None -> assert false in
 570      let context,params =
 571       let context,res =
 572        List.fold_left
 573         (fun (context,res) (name,t) ->
 574           let t =
 575            match t with
 576               None -> CicNotationPt.Implicit
 577             | Some t -> t in
 578           let name = CicNotationUtil.cic_name_of_name name in
 579            name::context,(name, interpretate_term context env None false t)::res
 580         ) ([],[]) params
 581       in
 582        context,List.rev res in
 583      let add_params =
 584       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 585      let name_to_uris =
 586       snd (
 587        List.fold_left
 588         (*here the explicit_named_substituion is assumed to be of length 0 *)
 589         (fun (i,res) (name,_,_,_) ->
 590           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
 591         ) (0,[]) tyl) in
 592      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
 593      let tyl =
 594       List.map
 595        (fun (name,b,ty,cl) ->
 596          let ty' = add_params (interpretate_term context env None false ty) in
 597          let cl' =
 598           List.map
 599            (fun (name,ty) ->
 600              let ty' =
 601               add_params (interpretate_term context con_env None false ty)
 602              in
 603               name,ty'
 604            ) cl
 605          in
 606           name,b,ty',cl'
 607        ) tyl
 608      in
 609       Cic.InductiveDefinition (tyl,[],List.length params,[])
 610   | CicNotationPt.Record (params,name,ty,fields) ->
 611      let uri = match uri with Some uri -> uri | None -> assert false in
 612      let context,params =
 613       let context,res =
 614        List.fold_left
 615         (fun (context,res) (name,t) ->
 616           let t =
 617            match t with
 618               None -> CicNotationPt.Implicit
 619             | Some t -> t in
 620           let name = CicNotationUtil.cic_name_of_name name in
 621            name::context,(name, interpretate_term context env None false t)::res
 622         ) ([],[]) params
 623       in
 624        context,List.rev res in
 625      let add_params =
 626       List.fold_right
 627        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 628      let ty' = add_params (interpretate_term context env None false ty) in
 629      let fields' =
 630       snd (
 631        List.fold_left
 632         (fun (context,res) (name,ty,_coercion,arity) ->
 633           let context' = Cic.Name name :: context in
 634            context',(name,interpretate_term context env None false ty)::res
 635         ) (context,[]) fields) in
 636      let concl =
 637       (*here the explicit_named_substituion is assumed to be of length 0 *)
 638       let mutind = Cic.MutInd (uri,0,[]) in
 639       if params = [] then mutind
 640       else
 641        Cic.Appl
 642         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
 643      let con =
 644       List.fold_left
 645        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
 646        concl fields' in
 647      let con' = add_params con in
 648      let tyl = [name,true,ty',["mk_" ^ name,con']] in
 649      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
 650       Cic.InductiveDefinition
 651        (tyl,[],List.length params,[`Class (`Record field_names)])
 652   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
 653      let attrs = [`Flavour flavour] in
 654      let ty' = interpretate_term [] env None false ty in
 655      (match bo,flavour with
 656         None,`Axiom ->
 657          Cic.Constant (name,None,ty',[],attrs)
 658       | Some bo,`Axiom -> assert false
 659       | None,_ ->
 660          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
 661       | Some bo,_ ->
 662          let bo' = Some (interpretate_term [] env None false bo) in
 663           Cic.Constant (name,bo',ty',[],attrs))
 664 ;;
 665
 666 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 667      ~localization_tbl
 668 =
 669   let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
 670 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
 671 ~localization_tbl
 672 ;;
 673
 674
 675 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
 676   | Ast.AttributedTerm (`Loc loc, term) ->
 677      domain_of_term ~loc ~context term
 678   | Ast.AttributedTerm (_, term) ->
 679       domain_of_term ~loc ~context term
 680   | Ast.Symbol (symbol, instance) ->
 681       [ Node ([loc], Symbol (symbol, instance), []) ]
 682       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
 683   | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
 684   | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
 685      ->
 686       let args_dom =
 687         List.fold_right
 688           (fun term acc -> domain_of_term ~loc ~context term @ acc)
 689           args [] in
 690       let loc =
 691        match hd with
 692           Ast.AttributedTerm (`Loc loc,_)  -> loc
 693         | _ -> loc
 694       in
 695        [ Node ([loc], Symbol (symbol, instance), args_dom) ]
 696   | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
 697   | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
 698       let args_dom =
 699         List.fold_right
 700           (fun term acc -> domain_of_term ~loc ~context term @ acc)
 701           args [] in
 702       let loc =
 703        match hd with
 704           Ast.AttributedTerm (`Loc loc,_)  -> loc
 705         | _ -> loc
 706       in
 707       (try
 708         (* the next line can raise Not_found *)
 709         ignore(find_in_context name context);
 710         if subst <> None then
 711           Ast.fail loc "Explicit substitutions not allowed here"
 712         else
 713           args_dom
 714       with Not_found ->
 715         (match subst with
 716         | None -> [ Node ([loc], Id name, args_dom) ]
 717         | Some subst ->
 718             let terms =
 719               List.fold_left
 720                 (fun dom (_, term) ->
 721                   let dom' = domain_of_term ~loc ~context term in
 722                   dom @ dom')
 723                 [] subst in
 724             [ Node ([loc], Id name, terms @ args_dom) ]))
 725   | Ast.Appl terms ->
 726       List.fold_right
 727         (fun term acc -> domain_of_term ~loc ~context term @ acc)
 728         terms []
 729   | Ast.Binder (kind, (var, typ), body) ->
 730       let type_dom = domain_of_term_option ~loc ~context typ in
 731       let body_dom =
 732         domain_of_term ~loc
 733           ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
 734       (match kind with
 735       | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
 736       | _ -> type_dom @ body_dom)
 737   | Ast.Case (term, indty_ident, outtype, branches) ->
 738       let term_dom = domain_of_term ~loc ~context term in
 739       let outtype_dom = domain_of_term_option ~loc ~context outtype in
 740       let rec get_first_constructor = function
 741         | [] -> []
 742         | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
 743         | _ :: tl -> get_first_constructor tl in
 744       let do_branch =
 745        function
 746           Ast.Pattern (head, _, args), term ->
 747            let (term_context, args_domain) =
 748              List.fold_left
 749                (fun (cont, dom) (name, typ) ->
 750                  (CicNotationUtil.cic_name_of_name name :: cont,
 751                   (match typ with
 752                   | None -> dom
 753                   | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
 754                (context, []) args
 755            in
 756             domain_of_term ~loc ~context:term_context term @ args_domain
 757         | Ast.Wildcard, term ->
 758             domain_of_term ~loc ~context term
 759       in
 760       let branches_dom =
 761         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
 762       (match indty_ident with
 763        | None -> get_first_constructor branches
 764        | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
 765       @ term_dom @ outtype_dom @ branches_dom
 766   | Ast.Cast (term, ty) ->
 767       let term_dom = domain_of_term ~loc ~context term in
 768       let ty_dom = domain_of_term ~loc ~context ty in
 769       term_dom @ ty_dom
 770   | Ast.LetIn ((var, typ), body, where) ->
 771       let body_dom = domain_of_term ~loc ~context body in
 772       let type_dom = domain_of_term_option ~loc ~context typ in
 773       let where_dom =
 774         domain_of_term ~loc
 775           ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
 776       body_dom @ type_dom @ where_dom
 777   | Ast.LetRec (kind, defs, where) ->
 778       let add_defs context =
 779         List.fold_left
 780           (fun acc (_, (var, _), _, _) ->
 781             CicNotationUtil.cic_name_of_name var :: acc
 782           ) context defs in
 783       let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
 784       let defs_dom =
 785         List.fold_left
 786           (fun dom (params, (_, typ), body, _) ->
 787             let context' =
 788              add_defs
 789               (List.fold_left
 790                 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
 791                 context params)
 792             in
 793             List.rev
 794              (snd
 795                (List.fold_left
 796                 (fun (context,res) (var,ty) ->
 797                   CicNotationUtil.cic_name_of_name var :: context,
 798                   domain_of_term_option ~loc ~context ty @ res)
 799                 (add_defs context,[]) params))
 800             @ dom
 801             @ domain_of_term_option ~loc ~context:context' typ
 802             @ domain_of_term ~loc ~context:context' body
 803           ) [] defs
 804       in
 805       defs_dom @ where_dom
 806   | Ast.Ident (name, subst) ->
 807       (try
 808         (* the next line can raise Not_found *)
 809         ignore(find_in_context name context);
 810         if subst <> None then
 811           Ast.fail loc "Explicit substitutions not allowed here"
 812         else
 813           []
 814       with Not_found ->
 815         (match subst with
 816         | None -> [ Node ([loc], Id name, []) ]
 817         | Some subst ->
 818             let terms =
 819               List.fold_left
 820                 (fun dom (_, term) ->
 821                   let dom' = domain_of_term ~loc ~context term in
 822                   dom @ dom')
 823                 [] subst in
 824             [ Node ([loc], Id name, terms) ]))
 825   | Ast.Uri _ -> []
 826   | Ast.Implicit -> []
 827   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
 828   | Ast.Meta (index, local_context) ->
 829       List.fold_left
 830        (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
 831        [] local_context
 832   | Ast.Sort _ -> []
 833   | Ast.UserInput
 834   | Ast.Literal _
 835   | Ast.Layout _
 836   | Ast.Magic _
 837   | Ast.Variable _ -> assert false
 838
 839 and domain_of_term_option ~loc ~context = function
 840   | None -> []
 841   | Some t -> domain_of_term ~loc ~context t
 842
 843 let domain_of_term ~context term =
 844  uniq_domain (domain_of_term ~context term)
 845
 846 let domain_of_obj ~context ast =
 847  let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
 848  assert (context = []);
 849   match ast with
 850    | Ast.Theorem (_,_,ty,bo) ->
 851       domain_of_term [] ty
 852       @ (match bo with
 853           None -> []
 854         | Some bo -> domain_of_term [] bo)
 855    | Ast.Inductive (params,tyl) ->
 856       let context, dom =
 857        List.fold_left
 858         (fun (context, dom) (var, ty) ->
 859           let context' = CicNotationUtil.cic_name_of_name var :: context in
 860           match ty with
 861              None -> context', dom
 862            | Some ty -> context', dom @ domain_of_term context ty
 863         ) ([], []) params in
 864       let context_w_types =
 865         List.rev_map
 866           (fun (var, _, _, _) -> Cic.Name var) tyl
 867         @ context in
 868       dom
 869       @ List.flatten (
 870          List.map
 871           (fun (_,_,ty,cl) ->
 872             domain_of_term context ty
 873             @ List.flatten (
 874                List.map
 875                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
 876                 tyl)
 877    | CicNotationPt.Record (params,var,ty,fields) ->
 878       let context, dom =
 879        List.fold_left
 880         (fun (context, dom) (var, ty) ->
 881           let context' = CicNotationUtil.cic_name_of_name var :: context in
 882           match ty with
 883              None -> context', dom
 884            | Some ty -> context', dom @ domain_of_term context ty
 885         ) ([], []) params in
 886       let context_w_types = Cic.Name var :: context in
 887       dom
 888       @ domain_of_term context ty
 889       @ snd
 890          (List.fold_left
 891           (fun (context,res) (name,ty,_,_) ->
 892             Cic.Name name::context, res @ domain_of_term context ty
 893           ) (context_w_types,[]) fields)
 894
 895 let domain_of_obj ~context obj =
 896  uniq_domain (domain_of_obj ~context obj)
 897
 898 let domain_of_ast_term = domain_of_term;;
 899
 900 let domain_of_term ~context term =
 901  let context =
 902    List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
 903  in
 904  domain_of_term ~context term
 905
 906   (* dom1 \ dom2 *)
 907 let domain_diff dom1 dom2 =
 908 (* let domain_diff = Domain.diff *)
 909   let is_in_dom2 elt =
 910     List.exists
 911      (function
 912        | Symbol (symb, 0) ->
 913           (match elt with
 914               Symbol (symb',_) when symb = symb' -> true
 915             | _ -> false)
 916        | Num i ->
 917           (match elt with
 918               Num _ -> true
 919             | _ -> false)
 920        | item -> elt = item
 921      ) dom2
 922   in
 923    let rec aux =
 924     function
 925        [] -> []
 926      | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
 927      | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
 928    in
 929     aux dom1
 930
 931 module type Disambiguator =
 932 sig
 933   val disambiguate_thing:
 934     dbd:HSql.dbd ->
 935     context:'context ->
 936     metasenv:'metasenv ->
 937     initial_ugraph:'ugraph ->
 938     hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
 939           (('refined_thing,'metasenv) test_result -> 'ugraph ->
 940               ('refined_thing,'metasenv) test_result * 'ugraph) ->
 941     aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
 942     universe:DisambiguateTypes.codomain_item list
 943              DisambiguateTypes.Environment.t option ->
 944     uri:'uri ->
 945     pp_thing:('ast_thing -> string) ->
 946     domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
 947     interpretate_thing:(context:'context ->
 948                         env:DisambiguateTypes.codomain_item
 949                             DisambiguateTypes.Environment.t ->
 950                         uri:'uri ->
 951                         is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
 952     refine_thing:('metasenv ->
 953                   'context ->
 954                   'uri ->
 955                   'raw_thing ->
 956                   'ugraph -> localization_tbl:'cichash -> ('refined_thing,
 957                   'metasenv) test_result * 'ugraph) ->
 958     localization_tbl:'cichash ->
 959     string * int * 'ast_thing ->
 960     ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
 961      list * 'metasenv * 'refined_thing * 'ugraph)
 962     list * bool
 963
 964   val disambiguate_term :
 965     ?fresh_instances:bool ->
 966     dbd:HSql.dbd ->
 967     context:Cic.context ->
 968     metasenv:Cic.metasenv -> ?goal:int ->
 969     ?initial_ugraph:CicUniv.universe_graph ->
 970     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
 971     universe:DisambiguateTypes.multiple_environment option ->
 972     CicNotationPt.term disambiguator_input ->
 973     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
 974      Cic.metasenv *                  (* new metasenv *)
 975      Cic.term*
 976      CicUniv.universe_graph) list *  (* disambiguated term *)
 977     bool
 978
 979   val disambiguate_obj :
 980     ?fresh_instances:bool ->
 981     dbd:HSql.dbd ->
 982     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
 983     universe:DisambiguateTypes.multiple_environment option ->
 984     uri:UriManager.uri option ->     (* required only for inductive types *)
 985     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
 986     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
 987      Cic.metasenv *                  (* new metasenv *)
 988      Cic.obj *
 989      CicUniv.universe_graph) list *  (* disambiguated obj *)
 990     bool
 991 end
 992
 993 module Make (C: Callbacks) =
 994   struct
 995     let choices_of_id dbd id =
 996       let uris = Whelp.locate ~dbd id in
 997       let uris =
 998        match uris with
 999         | [] ->
1000            (match
1001              (C.input_or_locate_uri
1002                ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
1003            with
1004            | None -> []
1005            | Some uri -> [uri])
1006         | [uri] -> [uri]
1007         | _ ->
1008             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
1009              ~ok:"Try selected." ~enable_button_for_non_vars:true
1010              ~title:"Ambiguous input." ~id
1011              ~msg: ("Ambiguous input \"" ^ id ^
1012                 "\". Please, choose one or more interpretations:")
1013              uris
1014       in
1015       List.map
1016         (fun uri ->
1017           (UriManager.string_of_uri uri,
1018            let term =
1019              try
1020                CicUtil.term_of_uri uri
1021              with exn ->
1022                debug_print (lazy (UriManager.string_of_uri uri));
1023                debug_print (lazy (Printexc.to_string exn));
1024                assert false
1025             in
1026            fun _ _ _ -> term))
1027         uris
1028
1029 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
1030
1031     let disambiguate_thing ~dbd ~context ~metasenv
1032       ~initial_ugraph ~hint
1033       ~aliases ~universe
1034       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
1035       ~localization_tbl
1036       (thing_txt,thing_txt_prefix_len,thing)
1037     =
1038       debug_print (lazy "DISAMBIGUATE INPUT");
1039       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
1040       let thing_dom = domain_of_thing ~context thing in
1041       debug_print
1042        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
1043 (*
1044       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
1045         (DisambiguatePp.pp_environment aliases)));
1046       debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
1047         (match universe with None -> "None" | Some _ -> "Some _")));
1048 *)
1049       let current_dom =
1050         Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1051       let todo_dom = domain_diff thing_dom current_dom in
1052       debug_print
1053        (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1054       (* (2) lookup function for any item (Id/Symbol/Num) *)
1055       let lookup_choices =
1056         fun item ->
1057           let choices =
1058             let lookup_in_library () =
1059               match item with
1060               | Id id -> choices_of_id dbd id
1061               | Symbol (symb, _) ->
1062                  (try
1063                    List.map DisambiguateChoices.mk_choice
1064                     (TermAcicContent.lookup_interpretations symb)
1065                   with
1066                    TermAcicContent.Interpretation_not_found -> [])
1067               | Num instance ->
1068                   DisambiguateChoices.lookup_num_choices ()
1069             in
1070             match universe with
1071             | None -> lookup_in_library ()
1072             | Some e ->
1073                 (try
1074                   let item =
1075                     match item with
1076                     | Symbol (symb, _) -> Symbol (symb, 0)
1077                     | item -> item
1078                   in
1079                   Environment.find item e
1080                 with Not_found -> lookup_in_library ())
1081           in
1082           choices
1083       in
1084 (*
1085       (* <benchmark> *)
1086       let _ =
1087         if benchmark then begin
1088           let per_item_choices =
1089             List.map
1090               (fun dom_item ->
1091                 try
1092                   let len = List.length (lookup_choices dom_item) in
1093                   debug_print (lazy (sprintf "BENCHMARK %s: %d"
1094                     (string_of_domain_item dom_item) len));
1095                   len
1096                 with No_choices _ -> 0)
1097               thing_dom
1098           in
1099           max_refinements := List.fold_left ( * ) 1 per_item_choices;
1100           actual_refinements := 0;
1101           domain_size := List.length thing_dom;
1102           choices_avg :=
1103             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1104         end
1105       in
1106       (* </benchmark> *)
1107 *)
1108
1109       (* (3) test an interpretation filling with meta uninterpreted identifiers
1110        *)
1111       let test_env aliases todo_dom ugraph =
1112         let rec aux env = function
1113           | [] -> env
1114           | Node (_, item, l) :: tl ->
1115               let env =
1116                 Environment.add item
1117                  ("Implicit",
1118                    (match item with
1119                       | Id _ | Num _ ->
1120                           (fun _ _ _ -> Cic.Implicit (Some `Closed))
1121                       | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1122                  env in
1123               aux (aux env l) tl in
1124         let filled_env = aux aliases todo_dom in
1125         try
1126           let cic_thing =
1127             interpretate_thing ~context ~env:filled_env
1128              ~uri ~is_path:false thing ~localization_tbl
1129           in
1130           let cic_thing = (fst hint) metasenv cic_thing in
1131 let foo () =
1132           let k,ugraph1 =
1133            refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1134           in
1135           let k, ugraph1 = (snd hint) k ugraph1 in
1136             (k , ugraph1 )
1137 in refine_profiler.HExtlib.profile foo ()
1138         with
1139         | Try_again msg -> Uncertain (None,msg), ugraph
1140         | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1141       in
1142       (* (4) build all possible interpretations *)
1143       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1144       (* aux returns triples Ok/Uncertain/Ko *)
1145       (* rem_dom is the concatenation of all the remainin domains *)
1146       let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1147         debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1148         match todo_dom with
1149         | [] ->
1150             assert (lookup_in_todo_dom = None);
1151             (match test_env aliases rem_dom base_univ with
1152             | Ok (thing, metasenv),new_univ ->
1153                [ aliases, diff, metasenv, thing, new_univ ], [], []
1154             | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1155             | Uncertain (loc,msg),new_univ ->
1156                [],[aliases,diff,loc,msg,new_univ],[])
1157         | Node (locs,item,inner_dom) :: remaining_dom ->
1158             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1159              (string_of_domain_item item)));
1160             let choices =
1161              match lookup_in_todo_dom with
1162                 None -> lookup_choices item
1163               | Some choices -> choices in
1164             match choices with
1165                [] ->
1166                 [], [],
1167                  [aliases, diff, Some (List.hd locs),
1168                   lazy ("No choices for " ^ string_of_domain_item item),
1169                   true]
1170 (*
1171              | [codomain_item] ->
1172                  (* just one choice. We perform a one-step look-up and
1173                     if the next set of choices is also a singleton we
1174                     skip this refinement step *)
1175                  debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1176                  let new_env = Environment.add item codomain_item aliases in
1177                  let new_diff = (item,codomain_item)::diff in
1178                  let lookup_in_todo_dom,next_choice_is_single =
1179                   match remaining_dom with
1180                      [] -> None,false
1181                    | (_,he)::_ ->
1182                       let choices = lookup_choices he in
1183                        Some choices,List.length choices = 1
1184                  in
1185                   if next_choice_is_single then
1186                    aux new_env new_diff lookup_in_todo_dom remaining_dom
1187                     base_univ
1188                   else
1189                     (match test_env new_env remaining_dom base_univ with
1190                     | Ok (thing, metasenv),new_univ ->
1191                         (match remaining_dom with
1192                         | [] ->
1193                            [ new_env, new_diff, metasenv, thing, new_univ ], []
1194                         | _ ->
1195                            aux new_env new_diff lookup_in_todo_dom
1196                             remaining_dom new_univ)
1197                     | Uncertain (loc,msg),new_univ ->
1198                         (match remaining_dom with
1199                         | [] -> [], [new_env,new_diff,loc,msg,true]
1200                         | _ ->
1201                            aux new_env new_diff lookup_in_todo_dom
1202                             remaining_dom new_univ)
1203                     | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1204 *)
1205              | _::_ ->
1206                  let mark_not_significant failures =
1207                    List.map
1208                     (fun (env, diff, loc, msg, _b) ->
1209                       env, diff, loc, msg, false)
1210                     failures in
1211                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1212                   if ok_l <> [] || uncertain_l <> [] then
1213                    ok_l,uncertain_l,mark_not_significant error_l
1214                   else
1215                    outcome in
1216                let rec filter univ = function
1217                 | [] -> [],[],[]
1218                 | codomain_item :: tl ->
1219                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1220                     let new_env = Environment.add item codomain_item aliases in
1221                     let new_diff = (item,codomain_item)::diff in
1222                     (match
1223                       test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1224                      with
1225                     | Ok (thing, metasenv),new_univ ->
1226                         let res =
1227                           (match inner_dom with
1228                           | [] ->
1229                              [new_env,new_diff,metasenv,thing,new_univ], [], []
1230                           | _ ->
1231                              aux new_env new_diff None inner_dom
1232                               (remaining_dom@rem_dom) new_univ
1233                           )
1234                         in
1235                          res @@ filter univ tl
1236                     | Uncertain (loc,msg),new_univ ->
1237                         let res =
1238                           (match inner_dom with
1239                           | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1240                           | _ ->
1241                              aux new_env new_diff None inner_dom
1242                               (remaining_dom@rem_dom) new_univ
1243                           )
1244                         in
1245                          res @@ filter univ tl
1246                     | Ko (loc,msg),_ ->
1247                         let res = [],[],[new_env,new_diff,loc,msg,true] in
1248                          res @@ filter univ tl)
1249                in
1250                 let ok_l,uncertain_l,error_l =
1251                  classify_errors (filter base_univ choices)
1252                 in
1253                  let res_after_ok_l =
1254                   List.fold_right
1255                    (fun (env,diff,_,_,univ) res ->
1256                      aux env diff None remaining_dom rem_dom univ @@ res
1257                    ) ok_l ([],[],error_l)
1258                 in
1259                  List.fold_right
1260                   (fun (env,diff,_,_,univ) res ->
1261                     aux env diff None remaining_dom rem_dom univ @@ res
1262                   ) uncertain_l res_after_ok_l
1263       in
1264       let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1265        match test_env aliases todo_dom base_univ with
1266         | Ok _,_
1267         | Uncertain _,_ ->
1268            aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1269         | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1270       let base_univ = initial_ugraph in
1271       try
1272         let res =
1273          match aux' aliases [] None todo_dom base_univ with
1274          | [],uncertain,errors ->
1275             let errors =
1276              List.map
1277               (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1278               ) uncertain @ errors
1279             in
1280             let errors =
1281              List.map
1282               (fun (env,diff,loc,msg,significant) ->
1283                 let env' =
1284                  filter_map_domain
1285                    (fun locs domain_item ->
1286                      try
1287                       let description =
1288                        fst (Environment.find domain_item env)
1289                       in
1290                        Some (locs,descr_of_domain_item domain_item,description)
1291                      with
1292                       Not_found -> None)
1293                    thing_dom
1294                 in
1295                  env',diff,loc,msg,significant
1296               ) errors
1297             in
1298              raise (NoWellTypedInterpretation (0,errors))
1299          | [_,diff,metasenv,t,ugraph],_,_ ->
1300              debug_print (lazy "SINGLE INTERPRETATION");
1301              [diff,metasenv,t,ugraph], false
1302          | l,_,_ ->
1303              debug_print
1304                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1305              let choices =
1306                List.map
1307                  (fun (env, _, _, _, _) ->
1308                    map_domain
1309                      (fun locs domain_item ->
1310                        let description =
1311                          fst (Environment.find domain_item env)
1312                        in
1313                        locs,descr_of_domain_item domain_item, description)
1314                      thing_dom)
1315                  l
1316              in
1317              let choosed =
1318                C.interactive_interpretation_choice
1319                  thing_txt thing_txt_prefix_len choices
1320              in
1321              (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1322               true
1323         in
1324          res
1325      with
1326       CicEnvironment.CircularDependency s ->
1327         failwith "Disambiguate: circular dependency"
1328
1329     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1330       ?goal
1331       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1332       (text,prefix_len,term)
1333     =
1334       let term =
1335         if fresh_instances then CicNotationUtil.freshen_term term else term
1336       in
1337       let hint = match goal with
1338         | None -> (fun _ x -> x), fun k u -> k, u
1339         | Some i ->
1340             (fun metasenv t ->
1341               let _,c,ty = CicUtil.lookup_meta i metasenv in
1342               assert(c=context);
1343               Cic.Cast(t,ty)),
1344             function
1345             | Ok (t,m) -> fun ug ->
1346                 (match t with
1347                 | Cic.Cast(t,_) -> Ok (t,m), ug
1348                 | _ -> assert false)
1349             | k -> fun ug -> k, ug
1350       in
1351       let localization_tbl = Cic.CicHash.create 503 in
1352       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1353         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1354         ~domain_of_thing:domain_of_term
1355         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1356         ~refine_thing:refine_term (text,prefix_len,term)
1357         ~localization_tbl
1358         ~hint
1359
1360     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1361      (text,prefix_len,obj)
1362     =
1363       let obj =
1364         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1365       in
1366       let hint =
1367         (fun _ x -> x),
1368         fun k u -> k, u
1369       in
1370       let localization_tbl = Cic.CicHash.create 503 in
1371       disambiguate_thing ~dbd ~context:[] ~metasenv:[]
1372         ~aliases ~universe ~uri
1373         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1374         ~initial_ugraph:CicUniv.empty_ugraph
1375         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1376         ~localization_tbl
1377         ~hint
1378         (text,prefix_len,obj)
1379
1380   end
1381
1382