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 test_result =
 107   | Ok of 'a * Cic.metasenv
 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: Cic.name list) ~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: Cic.name list) = 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                      let l' = List.map (aux ~localize loc context') l in
 384                       `AvoidLetIn (n,l')
 385                   | _ -> assert false
 386                 else
 387                  `AvoidLetIn (n,l')
 388               with
 389                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 390                 if localize then
 391                  `AddLetIn (aux ~localize loc context' body)
 392                 else
 393                  `AddLetIn unlocalized_body)
 394           | _ ->
 395              if localize then
 396               `AddLetIn (aux ~localize loc context' body)
 397              else
 398               `AddLetIn unlocalized_body
 399         in
 400         let inductiveFuns =
 401           List.map
 402             (fun (params, (name, typ), body, decr_idx) ->
 403               let add_binders kind t =
 404                List.fold_right
 405                 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
 406               in
 407               let cic_body =
 408                aux ~localize loc context' (add_binders `Lambda body) in
 409               let cic_type =
 410                aux_option ~localize loc context (Some `Type)
 411                 (HExtlib.map_option (add_binders `Pi) typ) in
 412               let name =
 413                 match CicNotationUtil.cic_name_of_name name with
 414                 | Cic.Anonymous ->
 415                     CicNotationPt.fail loc
 416                       "Recursive functions cannot be anonymous"
 417                 | Cic.Name name -> name
 418               in
 419               (name, decr_idx, cic_type, cic_body))
 420             defs
 421         in
 422         let fix_or_cofix n =
 423          match kind with
 424             `Inductive -> Cic.Fix (n,inductiveFuns)
 425           | `CoInductive ->
 426               let coinductiveFuns =
 427                 List.map
 428                  (fun (name, _, typ, body) -> name, typ, body)
 429                  inductiveFuns
 430               in
 431                Cic.CoFix (n,coinductiveFuns)
 432         in
 433          let counter = ref ~-1 in
 434          let build_term funs (var,_,ty,_) t =
 435           incr counter;
 436           Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
 437          in
 438           (match cic_body with
 439               `AvoidLetInNoAppl n ->
 440                 let n' = List.length inductiveFuns - n in
 441                  fix_or_cofix n'
 442             | `AvoidLetIn (n,l) ->
 443                 let n' = List.length inductiveFuns - n in
 444                  Cic.Appl (fix_or_cofix n'::l)
 445             | `AddLetIn cic_body ->
 446                 List.fold_right (build_term inductiveFuns) inductiveFuns
 447                  cic_body)
 448     | CicNotationPt.Ident _
 449     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
 450     | CicNotationPt.Ident (name, subst)
 451     | CicNotationPt.Uri (name, subst) as ast ->
 452         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
 453         (try
 454           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
 455           let index = find_in_context name context in
 456           if subst <> None then
 457             CicNotationPt.fail loc "Explicit substitutions not allowed here";
 458           Cic.Rel index
 459         with Not_found ->
 460           let cic =
 461             if is_uri ast then  (* we have the URI, build the term out of it *)
 462               try
 463                 CicUtil.term_of_uri (UriManager.uri_of_string name)
 464               with UriManager.IllFormedUri _ ->
 465                 CicNotationPt.fail loc "Ill formed URI"
 466             else
 467               resolve env (Id name) ()
 468           in
 469           let mk_subst uris =
 470             let ids_to_uris =
 471               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
 472             in
 473             (match subst with
 474             | Some subst ->
 475                 List.map
 476                   (fun (s, term) ->
 477                     (try
 478                       List.assoc s ids_to_uris, aux ~localize loc context term
 479                      with Not_found ->
 480                        raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
 481                   subst
 482             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
 483           in
 484           (try
 485             match cic with
 486             | Cic.Const (uri, []) ->
 487                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 488                 let uris = CicUtil.params_of_obj o in
 489                 Cic.Const (uri, mk_subst uris)
 490             | Cic.Var (uri, []) ->
 491                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 492                 let uris = CicUtil.params_of_obj o in
 493                 Cic.Var (uri, mk_subst uris)
 494             | Cic.MutInd (uri, i, []) ->
 495                (try
 496                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 497                  let uris = CicUtil.params_of_obj o in
 498                  Cic.MutInd (uri, i, mk_subst uris)
 499                 with
 500                  CicEnvironment.Object_not_found _ ->
 501                   (* if we are here it is probably the case that during the
 502                      definition of a mutual inductive type we have met an
 503                      occurrence of the type in one of its constructors.
 504                      However, the inductive type is not yet in the environment
 505                   *)
 506                   (*here the explicit_named_substituion is assumed to be of length 0 *)
 507                   Cic.MutInd (uri,i,[]))
 508             | Cic.MutConstruct (uri, i, j, []) ->
 509                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 510                 let uris = CicUtil.params_of_obj o in
 511                 Cic.MutConstruct (uri, i, j, mk_subst uris)
 512             | Cic.Meta _ | Cic.Implicit _ as t ->
 513 (*
 514                 debug_print (lazy (sprintf
 515                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
 516                   (CicPp.ppterm t)
 517                   (String.concat "; "
 518                     (List.map
 519                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
 520                       subst))));
 521 *)
 522                 t
 523             | _ ->
 524               raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
 525            with
 526              CicEnvironment.CircularDependency _ ->
 527                raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
 528     | CicNotationPt.Implicit -> Cic.Implicit None
 529     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
 530     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
 531     | CicNotationPt.Meta (index, subst) ->
 532         let cic_subst =
 533           List.map
 534             (function
 535                 None -> None
 536               | Some term -> Some (aux ~localize loc context term))
 537             subst
 538         in
 539         Cic.Meta (index, cic_subst)
 540     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
 541     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
 542     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
 543     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
 544     | CicNotationPt.Symbol (symbol, instance) ->
 545         resolve env (Symbol (symbol, instance)) ()
 546     | _ -> assert false (* god bless Bologna *)
 547   and aux_option ~localize loc (context: Cic.name list) annotation = function
 548     | None -> Cic.Implicit annotation
 549     | Some term -> aux ~localize loc context term
 550   in
 551    aux ~localize:true HExtlib.dummy_floc context ast
 552
 553 let interpretate_path ~context path =
 554  let localization_tbl = Cic.CicHash.create 23 in
 555   (* here we are throwing away useful localization informations!!! *)
 556   fst (
 557    interpretate_term ~create_dummy_ids:true
 558     ~context ~env:Environment.empty ~uri:None ~is_path:true
 559     path ~localization_tbl, localization_tbl)
 560
 561 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
 562  assert (context = []);
 563  assert (is_path = false);
 564  let interpretate_term = interpretate_term ~localization_tbl in
 565  match obj with
 566   | CicNotationPt.Inductive (params,tyl) ->
 567      let uri = match uri with Some uri -> uri | None -> assert false in
 568      let context,params =
 569       let context,res =
 570        List.fold_left
 571         (fun (context,res) (name,t) ->
 572           let t =
 573            match t with
 574               None -> CicNotationPt.Implicit
 575             | Some t -> t in
 576           let name = CicNotationUtil.cic_name_of_name name in
 577            name::context,(name, interpretate_term context env None false t)::res
 578         ) ([],[]) params
 579       in
 580        context,List.rev res in
 581      let add_params =
 582       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 583      let name_to_uris =
 584       snd (
 585        List.fold_left
 586         (*here the explicit_named_substituion is assumed to be of length 0 *)
 587         (fun (i,res) (name,_,_,_) ->
 588           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
 589         ) (0,[]) tyl) in
 590      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
 591      let tyl =
 592       List.map
 593        (fun (name,b,ty,cl) ->
 594          let ty' = add_params (interpretate_term context env None false ty) in
 595          let cl' =
 596           List.map
 597            (fun (name,ty) ->
 598              let ty' =
 599               add_params (interpretate_term context con_env None false ty)
 600              in
 601               name,ty'
 602            ) cl
 603          in
 604           name,b,ty',cl'
 605        ) tyl
 606      in
 607       Cic.InductiveDefinition (tyl,[],List.length params,[])
 608   | CicNotationPt.Record (params,name,ty,fields) ->
 609      let uri = match uri with Some uri -> uri | None -> assert false in
 610      let context,params =
 611       let context,res =
 612        List.fold_left
 613         (fun (context,res) (name,t) ->
 614           let t =
 615            match t with
 616               None -> CicNotationPt.Implicit
 617             | Some t -> t in
 618           let name = CicNotationUtil.cic_name_of_name name in
 619            name::context,(name, interpretate_term context env None false t)::res
 620         ) ([],[]) params
 621       in
 622        context,List.rev res in
 623      let add_params =
 624       List.fold_right
 625        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
 626      let ty' = add_params (interpretate_term context env None false ty) in
 627      let fields' =
 628       snd (
 629        List.fold_left
 630         (fun (context,res) (name,ty,_coercion,arity) ->
 631           let context' = Cic.Name name :: context in
 632            context',(name,interpretate_term context env None false ty)::res
 633         ) (context,[]) fields) in
 634      let concl =
 635       (*here the explicit_named_substituion is assumed to be of length 0 *)
 636       let mutind = Cic.MutInd (uri,0,[]) in
 637       if params = [] then mutind
 638       else
 639        Cic.Appl
 640         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
 641      let con =
 642       List.fold_left
 643        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
 644        concl fields' in
 645      let con' = add_params con in
 646      let tyl = [name,true,ty',["mk_" ^ name,con']] in
 647      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
 648       Cic.InductiveDefinition
 649        (tyl,[],List.length params,[`Class (`Record field_names)])
 650   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
 651      let attrs = [`Flavour flavour] in
 652      let ty' = interpretate_term [] env None false ty in
 653      (match bo,flavour with
 654         None,`Axiom ->
 655          Cic.Constant (name,None,ty',[],attrs)
 656       | Some bo,`Axiom -> assert false
 657       | None,_ ->
 658          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
 659       | Some bo,_ ->
 660          let bo' = Some (interpretate_term [] env None false bo) in
 661           Cic.Constant (name,bo',ty',[],attrs))
 662
 663 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
 664   | Ast.AttributedTerm (`Loc loc, term) ->
 665      domain_of_term ~loc ~context term
 666   | Ast.AttributedTerm (_, term) ->
 667       domain_of_term ~loc ~context term
 668   | Ast.Symbol (symbol, instance) ->
 669       [ Node ([loc], Symbol (symbol, instance), []) ]
 670       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
 671   | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
 672   | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
 673      ->
 674       let args_dom =
 675         List.fold_right
 676           (fun term acc -> domain_of_term ~loc ~context term @ acc)
 677           args [] in
 678       let loc =
 679        match hd with
 680           Ast.AttributedTerm (`Loc loc,_)  -> loc
 681         | _ -> loc
 682       in
 683        [ Node ([loc], Symbol (symbol, instance), args_dom) ]
 684   | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
 685   | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
 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       (try
 696         (* the next line can raise Not_found *)
 697         ignore(find_in_context name context);
 698         if subst <> None then
 699           Ast.fail loc "Explicit substitutions not allowed here"
 700         else
 701           args_dom
 702       with Not_found ->
 703         (match subst with
 704         | None -> [ Node ([loc], Id name, args_dom) ]
 705         | Some subst ->
 706             let terms =
 707               List.fold_left
 708                 (fun dom (_, term) ->
 709                   let dom' = domain_of_term ~loc ~context term in
 710                   dom @ dom')
 711                 [] subst in
 712             [ Node ([loc], Id name, terms @ args_dom) ]))
 713   | Ast.Appl terms ->
 714       List.fold_right
 715         (fun term acc -> domain_of_term ~loc ~context term @ acc)
 716         terms []
 717   | Ast.Binder (kind, (var, typ), body) ->
 718       let type_dom = domain_of_term_option ~loc ~context typ in
 719       let body_dom =
 720         domain_of_term ~loc
 721           ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
 722       (match kind with
 723       | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
 724       | _ -> type_dom @ body_dom)
 725   | Ast.Case (term, indty_ident, outtype, branches) ->
 726       let term_dom = domain_of_term ~loc ~context term in
 727       let outtype_dom = domain_of_term_option ~loc ~context outtype in
 728       let rec get_first_constructor = function
 729         | [] -> []
 730         | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
 731         | _ :: tl -> get_first_constructor tl in
 732       let do_branch =
 733        function
 734           Ast.Pattern (head, _, args), term ->
 735            let (term_context, args_domain) =
 736              List.fold_left
 737                (fun (cont, dom) (name, typ) ->
 738                  (CicNotationUtil.cic_name_of_name name :: cont,
 739                   (match typ with
 740                   | None -> dom
 741                   | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
 742                (context, []) args
 743            in
 744             domain_of_term ~loc ~context:term_context term @ args_domain
 745         | Ast.Wildcard, term ->
 746             domain_of_term ~loc ~context term
 747       in
 748       let branches_dom =
 749         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
 750       (match indty_ident with
 751        | None -> get_first_constructor branches
 752        | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
 753       @ term_dom @ outtype_dom @ branches_dom
 754   | Ast.Cast (term, ty) ->
 755       let term_dom = domain_of_term ~loc ~context term in
 756       let ty_dom = domain_of_term ~loc ~context ty in
 757       term_dom @ ty_dom
 758   | Ast.LetIn ((var, typ), body, where) ->
 759       let body_dom = domain_of_term ~loc ~context body in
 760       let type_dom = domain_of_term_option ~loc ~context typ in
 761       let where_dom =
 762         domain_of_term ~loc
 763           ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
 764       body_dom @ type_dom @ where_dom
 765   | Ast.LetRec (kind, defs, where) ->
 766       let add_defs context =
 767         List.fold_left
 768           (fun acc (_, (var, _), _, _) ->
 769             CicNotationUtil.cic_name_of_name var :: acc
 770           ) context defs in
 771       let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
 772       let defs_dom =
 773         List.fold_left
 774           (fun dom (params, (_, typ), body, _) ->
 775             let context' =
 776              add_defs
 777               (List.fold_left
 778                 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
 779                 context params)
 780             in
 781             List.rev
 782              (snd
 783                (List.fold_left
 784                 (fun (context,res) (var,ty) ->
 785                   CicNotationUtil.cic_name_of_name var :: context,
 786                   domain_of_term_option ~loc ~context ty @ res)
 787                 (add_defs context,[]) params))
 788             @ dom
 789             @ domain_of_term_option ~loc ~context:context' typ
 790             @ domain_of_term ~loc ~context:context' body
 791           ) [] defs
 792       in
 793       defs_dom @ where_dom
 794   | Ast.Ident (name, subst) ->
 795       (try
 796         (* the next line can raise Not_found *)
 797         ignore(find_in_context name context);
 798         if subst <> None then
 799           Ast.fail loc "Explicit substitutions not allowed here"
 800         else
 801           []
 802       with Not_found ->
 803         (match subst with
 804         | None -> [ Node ([loc], Id name, []) ]
 805         | Some subst ->
 806             let terms =
 807               List.fold_left
 808                 (fun dom (_, term) ->
 809                   let dom' = domain_of_term ~loc ~context term in
 810                   dom @ dom')
 811                 [] subst in
 812             [ Node ([loc], Id name, terms) ]))
 813   | Ast.Uri _ -> []
 814   | Ast.Implicit -> []
 815   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
 816   | Ast.Meta (index, local_context) ->
 817       List.fold_left
 818        (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
 819        [] local_context
 820   | Ast.Sort _ -> []
 821   | Ast.UserInput
 822   | Ast.Literal _
 823   | Ast.Layout _
 824   | Ast.Magic _
 825   | Ast.Variable _ -> assert false
 826
 827 and domain_of_term_option ~loc ~context = function
 828   | None -> []
 829   | Some t -> domain_of_term ~loc ~context t
 830
 831 let domain_of_term ~context term =
 832  uniq_domain (domain_of_term ~context term)
 833
 834 let domain_of_obj ~context ast =
 835  assert (context = []);
 836   match ast with
 837    | Ast.Theorem (_,_,ty,bo) ->
 838       domain_of_term [] ty
 839       @ (match bo with
 840           None -> []
 841         | Some bo -> domain_of_term [] bo)
 842    | Ast.Inductive (params,tyl) ->
 843       let context, dom =
 844        List.fold_left
 845         (fun (context, dom) (var, ty) ->
 846           let context' = CicNotationUtil.cic_name_of_name var :: context in
 847           match ty with
 848              None -> context', dom
 849            | Some ty -> context', dom @ domain_of_term context ty
 850         ) ([], []) params in
 851       let context_w_types =
 852         List.rev_map
 853           (fun (var, _, _, _) -> Cic.Name var) tyl
 854         @ context in
 855       dom
 856       @ List.flatten (
 857          List.map
 858           (fun (_,_,ty,cl) ->
 859             domain_of_term context ty
 860             @ List.flatten (
 861                List.map
 862                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
 863                 tyl)
 864    | CicNotationPt.Record (params,var,ty,fields) ->
 865       let context, dom =
 866        List.fold_left
 867         (fun (context, dom) (var, ty) ->
 868           let context' = CicNotationUtil.cic_name_of_name var :: context in
 869           match ty with
 870              None -> context', dom
 871            | Some ty -> context', dom @ domain_of_term context ty
 872         ) ([], []) params in
 873       let context_w_types = Cic.Name var :: context in
 874       dom
 875       @ domain_of_term context ty
 876       @ snd
 877          (List.fold_left
 878           (fun (context,res) (name,ty,_,_) ->
 879             Cic.Name name::context, res @ domain_of_term context ty
 880           ) (context_w_types,[]) fields)
 881
 882 let domain_of_obj ~context obj =
 883  uniq_domain (domain_of_obj ~context obj)
 884
 885   (* dom1 \ dom2 *)
 886 let domain_diff dom1 dom2 =
 887 (* let domain_diff = Domain.diff *)
 888   let is_in_dom2 elt =
 889     List.exists
 890      (function
 891        | Symbol (symb, 0) ->
 892           (match elt with
 893               Symbol (symb',_) when symb = symb' -> true
 894             | _ -> false)
 895        | Num i ->
 896           (match elt with
 897               Num _ -> true
 898             | _ -> false)
 899        | item -> elt = item
 900      ) dom2
 901   in
 902    let rec aux =
 903     function
 904        [] -> []
 905      | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
 906      | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
 907    in
 908     aux dom1
 909
 910 module type Disambiguator =
 911 sig
 912   val disambiguate_term :
 913     ?fresh_instances:bool ->
 914     dbd:HSql.dbd ->
 915     context:Cic.context ->
 916     metasenv:Cic.metasenv ->
 917     ?initial_ugraph:CicUniv.universe_graph ->
 918     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
 919     universe:DisambiguateTypes.multiple_environment option ->
 920     CicNotationPt.term disambiguator_input ->
 921     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
 922      Cic.metasenv *                  (* new metasenv *)
 923      Cic.term*
 924      CicUniv.universe_graph) list *  (* disambiguated term *)
 925     bool
 926
 927   val disambiguate_obj :
 928     ?fresh_instances:bool ->
 929     dbd:HSql.dbd ->
 930     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
 931     universe:DisambiguateTypes.multiple_environment option ->
 932     uri:UriManager.uri option ->     (* required only for inductive types *)
 933     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
 934     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
 935      Cic.metasenv *                  (* new metasenv *)
 936      Cic.obj *
 937      CicUniv.universe_graph) list *  (* disambiguated obj *)
 938     bool
 939 end
 940
 941 module Make (C: Callbacks) =
 942   struct
 943     let choices_of_id dbd id =
 944       let uris = Whelp.locate ~dbd id in
 945       let uris =
 946        match uris with
 947         | [] ->
 948            (match
 949              (C.input_or_locate_uri
 950                ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
 951            with
 952            | None -> []
 953            | Some uri -> [uri])
 954         | [uri] -> [uri]
 955         | _ ->
 956             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
 957              ~ok:"Try selected." ~enable_button_for_non_vars:true
 958              ~title:"Ambiguous input." ~id
 959              ~msg: ("Ambiguous input \"" ^ id ^
 960                 "\". Please, choose one or more interpretations:")
 961              uris
 962       in
 963       List.map
 964         (fun uri ->
 965           (UriManager.string_of_uri uri,
 966            let term =
 967              try
 968                CicUtil.term_of_uri uri
 969              with exn ->
 970                debug_print (lazy (UriManager.string_of_uri uri));
 971                debug_print (lazy (Printexc.to_string exn));
 972                assert false
 973             in
 974            fun _ _ _ -> term))
 975         uris
 976
 977 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 978
 979     let disambiguate_thing ~dbd ~context ~metasenv
 980       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
 981       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
 982       (thing_txt,thing_txt_prefix_len,thing)
 983     =
 984       debug_print (lazy "DISAMBIGUATE INPUT");
 985       let disambiguate_context =  (* cic context -> disambiguate context *)
 986         List.map
 987           (function None -> Cic.Anonymous | Some (name, _) -> name)
 988           context
 989       in
 990       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
 991       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
 992       debug_print
 993        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
 994 (*
 995       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
 996         (DisambiguatePp.pp_environment aliases)));
 997       debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
 998         (match universe with None -> "None" | Some _ -> "Some _")));
 999 *)
1000       let current_dom =
1001         Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1002       let todo_dom = domain_diff thing_dom current_dom in
1003       debug_print
1004        (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1005       (* (2) lookup function for any item (Id/Symbol/Num) *)
1006       let lookup_choices =
1007         fun item ->
1008           let choices =
1009             let lookup_in_library () =
1010               match item with
1011               | Id id -> choices_of_id dbd id
1012               | Symbol (symb, _) ->
1013                  (try
1014                    List.map DisambiguateChoices.mk_choice
1015                     (TermAcicContent.lookup_interpretations symb)
1016                   with
1017                    TermAcicContent.Interpretation_not_found -> [])
1018               | Num instance ->
1019                   DisambiguateChoices.lookup_num_choices ()
1020             in
1021             match universe with
1022             | None -> lookup_in_library ()
1023             | Some e ->
1024                 (try
1025                   let item =
1026                     match item with
1027                     | Symbol (symb, _) -> Symbol (symb, 0)
1028                     | item -> item
1029                   in
1030                   Environment.find item e
1031                 with Not_found -> lookup_in_library ())
1032           in
1033           choices
1034       in
1035 (*
1036       (* <benchmark> *)
1037       let _ =
1038         if benchmark then begin
1039           let per_item_choices =
1040             List.map
1041               (fun dom_item ->
1042                 try
1043                   let len = List.length (lookup_choices dom_item) in
1044                   debug_print (lazy (sprintf "BENCHMARK %s: %d"
1045                     (string_of_domain_item dom_item) len));
1046                   len
1047                 with No_choices _ -> 0)
1048               thing_dom
1049           in
1050           max_refinements := List.fold_left ( * ) 1 per_item_choices;
1051           actual_refinements := 0;
1052           domain_size := List.length thing_dom;
1053           choices_avg :=
1054             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1055         end
1056       in
1057       (* </benchmark> *)
1058 *)
1059
1060       (* (3) test an interpretation filling with meta uninterpreted identifiers
1061        *)
1062       let test_env aliases todo_dom ugraph =
1063         let rec aux env = function
1064           | [] -> env
1065           | Node (_, item, l) :: tl ->
1066               let env =
1067                 Environment.add item
1068                  ("Implicit",
1069                    (match item with
1070                       | Id _ | Num _ ->
1071                           (fun _ _ _ -> Cic.Implicit (Some `Closed))
1072                       | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1073                  env in
1074               aux (aux env l) tl in
1075         let filled_env = aux aliases todo_dom in
1076         try
1077           let localization_tbl = Cic.CicHash.create 503 in
1078           let cic_thing =
1079             interpretate_thing ~context:disambiguate_context ~env:filled_env
1080              ~uri ~is_path:false thing ~localization_tbl
1081           in
1082 let foo () =
1083           let k,ugraph1 =
1084            refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1085           in
1086             (k , ugraph1 )
1087 in refine_profiler.HExtlib.profile foo ()
1088         with
1089         | Try_again msg -> Uncertain (None,msg), ugraph
1090         | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1091       in
1092       (* (4) build all possible interpretations *)
1093       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1094       (* aux returns triples Ok/Uncertain/Ko *)
1095       (* rem_dom is the concatenation of all the remainin domains *)
1096       let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1097         debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1098         match todo_dom with
1099         | [] ->
1100             assert (lookup_in_todo_dom = None);
1101             (match test_env aliases rem_dom base_univ with
1102             | Ok (thing, metasenv),new_univ ->
1103                [ aliases, diff, metasenv, thing, new_univ ], [], []
1104             | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1105             | Uncertain (loc,msg),new_univ ->
1106                [],[aliases,diff,loc,msg,new_univ],[])
1107         | Node (locs,item,inner_dom) :: remaining_dom ->
1108             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1109              (string_of_domain_item item)));
1110             let choices =
1111              match lookup_in_todo_dom with
1112                 None -> lookup_choices item
1113               | Some choices -> choices in
1114             match choices with
1115                [] ->
1116                 [], [],
1117                  [aliases, diff, Some (List.hd locs),
1118                   lazy ("No choices for " ^ string_of_domain_item item),
1119                   true]
1120 (*
1121              | [codomain_item] ->
1122                  (* just one choice. We perform a one-step look-up and
1123                     if the next set of choices is also a singleton we
1124                     skip this refinement step *)
1125                  debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1126                  let new_env = Environment.add item codomain_item aliases in
1127                  let new_diff = (item,codomain_item)::diff in
1128                  let lookup_in_todo_dom,next_choice_is_single =
1129                   match remaining_dom with
1130                      [] -> None,false
1131                    | (_,he)::_ ->
1132                       let choices = lookup_choices he in
1133                        Some choices,List.length choices = 1
1134                  in
1135                   if next_choice_is_single then
1136                    aux new_env new_diff lookup_in_todo_dom remaining_dom
1137                     base_univ
1138                   else
1139                     (match test_env new_env remaining_dom base_univ with
1140                     | Ok (thing, metasenv),new_univ ->
1141                         (match remaining_dom with
1142                         | [] ->
1143                            [ new_env, new_diff, metasenv, thing, new_univ ], []
1144                         | _ ->
1145                            aux new_env new_diff lookup_in_todo_dom
1146                             remaining_dom new_univ)
1147                     | Uncertain (loc,msg),new_univ ->
1148                         (match remaining_dom with
1149                         | [] -> [], [new_env,new_diff,loc,msg,true]
1150                         | _ ->
1151                            aux new_env new_diff lookup_in_todo_dom
1152                             remaining_dom new_univ)
1153                     | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1154 *)
1155              | _::_ ->
1156                  let mark_not_significant failures =
1157                    List.map
1158                     (fun (env, diff, loc, msg, _b) ->
1159                       env, diff, loc, msg, false)
1160                     failures in
1161                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1162                   if ok_l <> [] || uncertain_l <> [] then
1163                    ok_l,uncertain_l,mark_not_significant error_l
1164                   else
1165                    outcome in
1166                let rec filter univ = function
1167                 | [] -> [],[],[]
1168                 | codomain_item :: tl ->
1169                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1170                     let new_env = Environment.add item codomain_item aliases in
1171                     let new_diff = (item,codomain_item)::diff in
1172                     (match
1173                       test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1174                      with
1175                     | Ok (thing, metasenv),new_univ ->
1176                         let res =
1177                           (match inner_dom with
1178                           | [] ->
1179                              [new_env,new_diff,metasenv,thing,new_univ], [], []
1180                           | _ ->
1181                              aux new_env new_diff None inner_dom
1182                               (remaining_dom@rem_dom) new_univ
1183                           )
1184                         in
1185                          res @@ filter univ tl
1186                     | Uncertain (loc,msg),new_univ ->
1187                         let res =
1188                           (match inner_dom with
1189                           | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1190                           | _ ->
1191                              aux new_env new_diff None inner_dom
1192                               (remaining_dom@rem_dom) new_univ
1193                           )
1194                         in
1195                          res @@ filter univ tl
1196                     | Ko (loc,msg),_ ->
1197                         let res = [],[],[new_env,new_diff,loc,msg,true] in
1198                          res @@ filter univ tl)
1199                in
1200                 let ok_l,uncertain_l,error_l =
1201                  classify_errors (filter base_univ choices)
1202                 in
1203                  let res_after_ok_l =
1204                   List.fold_right
1205                    (fun (env,diff,_,_,univ) res ->
1206                      aux env diff None remaining_dom rem_dom univ @@ res
1207                    ) ok_l ([],[],error_l)
1208                 in
1209                  List.fold_right
1210                   (fun (env,diff,_,_,univ) res ->
1211                     aux env diff None remaining_dom rem_dom univ @@ res
1212                   ) uncertain_l res_after_ok_l
1213       in
1214       let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1215        match test_env aliases todo_dom base_univ with
1216         | Ok _,_
1217         | Uncertain _,_ ->
1218            aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1219         | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1220       let base_univ = initial_ugraph in
1221       try
1222         let res =
1223          match aux' aliases [] None todo_dom base_univ with
1224          | [],uncertain,errors ->
1225             let errors =
1226              List.map
1227               (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1228               ) uncertain @ errors
1229             in
1230             let errors =
1231              List.map
1232               (fun (env,diff,loc,msg,significant) ->
1233                 let env' =
1234                  filter_map_domain
1235                    (fun locs domain_item ->
1236                      try
1237                       let description =
1238                        fst (Environment.find domain_item env)
1239                       in
1240                        Some (locs,descr_of_domain_item domain_item,description)
1241                      with
1242                       Not_found -> None)
1243                    thing_dom
1244                 in
1245                  env',diff,loc,msg,significant
1246               ) errors
1247             in
1248              raise (NoWellTypedInterpretation (0,errors))
1249          | [_,diff,metasenv,t,ugraph],_,_ ->
1250              debug_print (lazy "SINGLE INTERPRETATION");
1251              [diff,metasenv,t,ugraph], false
1252          | l,_,_ ->
1253              debug_print
1254                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1255              let choices =
1256                List.map
1257                  (fun (env, _, _, _, _) ->
1258                    map_domain
1259                      (fun locs domain_item ->
1260                        let description =
1261                          fst (Environment.find domain_item env)
1262                        in
1263                        locs,descr_of_domain_item domain_item, description)
1264                      thing_dom)
1265                  l
1266              in
1267              let choosed =
1268                C.interactive_interpretation_choice
1269                  thing_txt thing_txt_prefix_len choices
1270              in
1271              (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1272               true
1273         in
1274          res
1275      with
1276       CicEnvironment.CircularDependency s ->
1277         failwith "Disambiguate: circular dependency"
1278
1279     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1280       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1281       (text,prefix_len,term)
1282     =
1283       let term =
1284         if fresh_instances then CicNotationUtil.freshen_term term else term
1285       in
1286       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1287         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1288         ~domain_of_thing:domain_of_term
1289         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1290         ~refine_thing:refine_term (text,prefix_len,term)
1291
1292     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1293      (text,prefix_len,obj)
1294     =
1295       let obj =
1296         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1297       in
1298       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1299         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1300         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1301         (text,prefix_len,obj)
1302   end
1303