helm/software/components/cic_disambiguation/disambiguate.ml

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