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