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