helm/software/components/cic_disambiguation/disambiguate.ml

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