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