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