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