components/cic_disambiguation/disambiguate.ml

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