helm/software/components/cic_disambiguation/disambiguate.ml

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