helm/ocaml/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 open Printf
  27
  28 open DisambiguateTypes
  29 open UriManager
  30
  31 exception No_choices of domain_item
  32 exception NoWellTypedInterpretation
  33 exception PathNotWellFormed
  34
  35   (** raised when an environment is not enough informative to decide *)
  36 exception Try_again
  37
  38 type aliases = bool * DisambiguateTypes.environment
  39
  40 let debug = false
  41 let debug_print = if debug then prerr_endline else ignore
  42
  43 (*
  44   (** print benchmark information *)
  45 let benchmark = true
  46 let max_refinements = ref 0       (* benchmarking is not thread safe *)
  47 let actual_refinements = ref 0
  48 let domain_size = ref 0
  49 let choices_avg = ref 0.
  50 *)
  51
  52 let floc_of_loc (loc_begin, loc_end) =
  53   let floc_begin =
  54     { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
  55       Lexing.pos_cnum = loc_begin }
  56   in
  57   let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
  58   (floc_begin, floc_end)
  59
  60 let dummy_floc = floc_of_loc (-1, -1)
  61
  62 let descr_of_domain_item = function
  63  | Id s -> s
  64  | Symbol (s, _) -> s
  65  | Num i -> string_of_int i
  66
  67 type 'a test_result =
  68   | Ok of 'a * Cic.metasenv
  69   | Ko
  70   | Uncertain
  71
  72 let refine_term metasenv context uri term ugraph =
  73 (*   if benchmark then incr actual_refinements; *)
  74   assert (uri=None);
  75   let metasenv, term =
  76     CicMkImplicit.expand_implicits metasenv [] context term in
  77     debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
  78     try
  79       let term', _, metasenv',ugraph1 =
  80         CicRefine.type_of_aux' metasenv context term ugraph in
  81         (Ok (term', metasenv')),ugraph1
  82     with
  83       | CicRefine.Uncertain s ->
  84           debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
  85           Uncertain,ugraph
  86       | CicRefine.RefineFailure msg ->
  87           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
  88             (CicPp.ppterm term) msg);
  89           Ko,ugraph
  90
  91 let refine_obj metasenv context uri obj ugraph =
  92  assert (context = []);
  93  let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
  94    debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj));
  95    try
  96      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
  97        (Ok (obj', metasenv)),ugraph
  98    with
  99      | CicRefine.Uncertain s ->
 100          debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ;
 101          Uncertain,ugraph
 102      | CicRefine.RefineFailure msg ->
 103          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
 104            (CicPp.ppobj obj) msg);
 105          Ko,ugraph
 106
 107 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
 108   try
 109     snd (Environment.find item env) env num args
 110   with Not_found ->
 111     failwith ("Domain item not found: " ^
 112       (DisambiguateTypes.string_of_domain_item item))
 113
 114   (* TODO move it to Cic *)
 115 let find_in_environment name (context: Cic.name list) =
 116   let rec aux acc = function
 117     | [] -> raise Not_found
 118     | Cic.Name hd :: tl when hd = name -> acc
 119     | _ :: tl ->  aux (acc + 1) tl
 120   in
 121   aux 1 context
 122
 123 let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
 124   assert (uri = None);
 125   let rec aux loc (context: Cic.name list) = function
 126     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
 127         aux loc context term
 128     | CicNotationPt.AttributedTerm (_, term) -> aux loc context term
 129     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
 130         let cic_args = List.map (aux loc context) args in
 131         resolve env (Symbol (symb, i)) ~args:cic_args ()
 132     | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
 133     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
 134         let cic_type = aux_option loc context (Some `Type) typ in
 135         let cic_name = CicNotationUtil.cic_name_of_name var in
 136         let cic_body = aux loc (cic_name :: context) body in
 137         (match binder_kind with
 138         | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
 139         | `Pi
 140         | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
 141         | `Exists ->
 142             resolve env (Symbol ("exists", 0))
 143               ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
 144     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
 145         let cic_term = aux loc context term in
 146         let cic_outtype = aux_option loc context None outtype in
 147         let do_branch ((head, args), term) =
 148           let rec do_branch' context = function
 149             | [] -> aux loc context term
 150             | (name, typ) :: tl ->
 151                 let cic_name = CicNotationUtil.cic_name_of_name name in
 152                 let cic_body = do_branch' (cic_name :: context) tl in
 153                 let typ =
 154                   match typ with
 155                   | None -> Cic.Implicit (Some `Type)
 156                   | Some typ -> aux loc context typ
 157                 in
 158                 Cic.Lambda (cic_name, typ, cic_body)
 159           in
 160           do_branch' context args
 161         in
 162         let (indtype_uri, indtype_no) =
 163           match indty_ident with
 164           | Some indty_ident ->
 165               (match resolve env (Id indty_ident) () with
 166               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
 167               | Cic.Implicit _ -> raise Try_again
 168               | _ -> raise Invalid_choice)
 169           | None ->
 170               let fst_constructor =
 171                 match branches with
 172                 | ((head, _), _) :: _ -> head
 173                 | [] -> raise Invalid_choice
 174               in
 175               (match resolve env (Id fst_constructor) () with
 176               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
 177                   (indtype_uri, indtype_no)
 178               | Cic.Implicit _ -> raise Try_again
 179               | _ -> raise Invalid_choice)
 180         in
 181         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
 182           (List.map do_branch branches))
 183     | CicNotationPt.Cast (t1, t2) ->
 184         let cic_t1 = aux loc context t1 in
 185         let cic_t2 = aux loc context t2 in
 186         Cic.Cast (cic_t1, cic_t2)
 187     | CicNotationPt.LetIn ((name, typ), def, body) ->
 188         let cic_def = aux loc context def in
 189         let cic_name = CicNotationUtil.cic_name_of_name name in
 190         let cic_def =
 191           match typ with
 192           | None -> cic_def
 193           | Some t -> Cic.Cast (cic_def, aux loc context t)
 194         in
 195         let cic_body = aux loc (cic_name :: context) body in
 196         Cic.LetIn (cic_name, cic_def, cic_body)
 197     | CicNotationPt.LetRec (kind, defs, body) ->
 198         let context' =
 199           List.fold_left
 200             (fun acc ((name, _), _, _) ->
 201               CicNotationUtil.cic_name_of_name name :: acc)
 202             context defs
 203         in
 204         let cic_body = aux loc context' body in
 205         let inductiveFuns =
 206           List.map
 207             (fun ((name, typ), body, decr_idx) ->
 208               let cic_body = aux loc context' body in
 209               let cic_type = aux_option loc context (Some `Type) typ in
 210               let name =
 211                 match CicNotationUtil.cic_name_of_name name with
 212                 | Cic.Anonymous ->
 213                     CicNotationPt.fail loc
 214                       "Recursive functions cannot be anonymous"
 215                 | Cic.Name name -> name
 216               in
 217               (name, decr_idx, cic_type, cic_body))
 218             defs
 219         in
 220         let counter = ref ~-1 in
 221         let build_term funs =
 222           (* this is the body of the fold_right function below. Rationale: Fix
 223            * and CoFix cases differs only in an additional index in the
 224            * inductiveFun list, see Cic.term *)
 225           match kind with
 226           | `Inductive ->
 227               (fun (var, _, _, _) cic ->
 228                 incr counter;
 229                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
 230           | `CoInductive ->
 231               let funs =
 232                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
 233               in
 234               (fun (var, _, _, _) cic ->
 235                 incr counter;
 236                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
 237         in
 238         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
 239     | CicNotationPt.Ident _
 240     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
 241     | CicNotationPt.Ident (name, subst)
 242     | CicNotationPt.Uri (name, subst) as ast ->
 243         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
 244         (try
 245           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
 246           let index = find_in_environment name context in
 247           if subst <> None then
 248             CicNotationPt.fail loc "Explicit substitutions not allowed here";
 249           Cic.Rel index
 250         with Not_found ->
 251           let cic =
 252             if is_uri ast then  (* we have the URI, build the term out of it *)
 253               try
 254                 CicUtil.term_of_uri (UriManager.uri_of_string name)
 255               with UriManager.IllFormedUri _ ->
 256                 CicNotationPt.fail loc "Ill formed URI"
 257             else
 258               resolve env (Id name) ()
 259           in
 260           let mk_subst uris =
 261             let ids_to_uris =
 262               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
 263             in
 264             (match subst with
 265             | Some subst ->
 266                 List.map
 267                   (fun (s, term) ->
 268                     (try
 269                       List.assoc s ids_to_uris, aux loc context term
 270                      with Not_found ->
 271                        raise Invalid_choice))
 272                   subst
 273             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
 274           in
 275           (try
 276             match cic with
 277             | Cic.Const (uri, []) ->
 278                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 279                 let uris = CicUtil.params_of_obj o in
 280                 Cic.Const (uri, mk_subst uris)
 281             | Cic.Var (uri, []) ->
 282                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 283                 let uris = CicUtil.params_of_obj o in
 284                 Cic.Var (uri, mk_subst uris)
 285             | Cic.MutInd (uri, i, []) ->
 286                (try
 287                  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 288                  let uris = CicUtil.params_of_obj o in
 289                  Cic.MutInd (uri, i, mk_subst uris)
 290                 with
 291                  CicEnvironment.Object_not_found _ ->
 292                   (* if we are here it is probably the case that during the
 293                      definition of a mutual inductive type we have met an
 294                      occurrence of the type in one of its constructors.
 295                      However, the inductive type is not yet in the environment
 296                   *)
 297                   (*here the explicit_named_substituion is assumed to be of length 0 *)
 298                   Cic.MutInd (uri,i,[]))
 299             | Cic.MutConstruct (uri, i, j, []) ->
 300                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 301                 let uris = CicUtil.params_of_obj o in
 302                 Cic.MutConstruct (uri, i, j, mk_subst uris)
 303             | Cic.Meta _ | Cic.Implicit _ as t ->
 304 (*
 305                 debug_print (sprintf
 306                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
 307                   (CicPp.ppterm t)
 308                   (String.concat "; "
 309                     (List.map
 310                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
 311                       subst)));
 312 *)
 313                 t
 314             | _ ->
 315               raise Invalid_choice
 316            with
 317              CicEnvironment.CircularDependency _ ->
 318                raise Invalid_choice))
 319     | CicNotationPt.Implicit -> Cic.Implicit None
 320     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
 321     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
 322     | CicNotationPt.Meta (index, subst) ->
 323         let cic_subst =
 324           List.map
 325             (function None -> None | Some term -> Some (aux loc context term))
 326             subst
 327         in
 328         Cic.Meta (index, cic_subst)
 329     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
 330     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
 331     | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
 332     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
 333     | CicNotationPt.Symbol (symbol, instance) ->
 334         resolve env (Symbol (symbol, instance)) ()
 335     | _ -> assert false (* god bless Bologna *)
 336   and aux_option loc (context: Cic.name list) annotation = function
 337     | None -> Cic.Implicit annotation
 338     | Some term -> aux loc context term
 339   in
 340   match ast with
 341   | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
 342   | term -> aux dummy_floc context term
 343
 344 let interpretate_path ~context path =
 345  interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path
 346
 347 let interpretate_obj ~context ~env ~uri ~is_path obj =
 348  assert (context = []);
 349  assert (is_path = false);
 350  match obj with
 351   | GrafiteAst.Inductive (params,tyl) ->
 352      let uri = match uri with Some uri -> uri | None -> assert false in
 353      let context,params =
 354       let context,res =
 355        List.fold_left
 356         (fun (context,res) (name,t) ->
 357           Cic.Name name :: context,
 358           (name, interpretate_term context env None false t)::res
 359         ) ([],[]) params
 360       in
 361        context,List.rev res in
 362      let add_params =
 363       List.fold_right
 364        (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
 365      let name_to_uris =
 366       snd (
 367        List.fold_left
 368         (*here the explicit_named_substituion is assumed to be of length 0 *)
 369         (fun (i,res) (name,_,_,_) ->
 370           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
 371         ) (0,[]) tyl) in
 372      let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in
 373      let undebrujin t =
 374       snd
 375        (List.fold_right
 376          (fun (name,_,_,_) (i,t) ->
 377            (*here the explicit_named_substituion is assumed to be of length 0 *)
 378            let t' = Cic.MutInd (uri,i,[])  in
 379            let t = CicSubstitution.subst t' t in
 380             i - 1,t
 381          ) tyl (List.length tyl - 1,t)) in
 382      let tyl =
 383       List.map
 384        (fun (name,b,ty,cl) ->
 385          let ty' = add_params (interpretate_term context env None false ty) in
 386          let cl' =
 387           List.map
 388            (fun (name,ty) ->
 389              let ty' =
 390               add_params (interpretate_term context con_env None false ty)
 391              in
 392               name,undebrujin ty'
 393            ) cl
 394          in
 395           name,b,ty',cl'
 396        ) tyl
 397      in
 398       Cic.InductiveDefinition (tyl,[],List.length params,[])
 399   | GrafiteAst.Record (params,name,ty,fields) ->
 400      let uri = match uri with Some uri -> uri | None -> assert false in
 401      let context,params =
 402       let context,res =
 403        List.fold_left
 404         (fun (context,res) (name,t) ->
 405           (Cic.Name name :: context),
 406           (name, interpretate_term context env None false t)::res
 407         ) ([],[]) params
 408       in
 409        context,List.rev res in
 410      let add_params =
 411       List.fold_right
 412        (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
 413      let ty' = add_params (interpretate_term context env None false ty) in
 414      let fields' =
 415       snd (
 416        List.fold_left
 417         (fun (context,res) (name,ty) ->
 418           let context' = Cic.Name name :: context in
 419            context',(name,interpretate_term context env None false ty)::res
 420         ) (context,[]) fields) in
 421      let concl =
 422       (*here the explicit_named_substituion is assumed to be of length 0 *)
 423       let mutind = Cic.MutInd (uri,0,[]) in
 424       if params = [] then mutind
 425       else
 426        Cic.Appl
 427         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
 428      let con =
 429       List.fold_left
 430        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
 431        concl fields' in
 432      let con' = add_params con in
 433      let tyl = [name,true,ty',["mk_" ^ name,con']] in
 434      let field_names = List.map fst fields in
 435       Cic.InductiveDefinition
 436        (tyl,[],List.length params,[`Class (`Record field_names)])
 437   | GrafiteAst.Theorem (flavour, name, ty, bo) ->
 438      let attrs = [`Flavour flavour] in
 439      let ty' = interpretate_term [] env None false ty in
 440      (match bo with
 441         None ->
 442          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
 443       | Some bo ->
 444          let bo' = Some (interpretate_term [] env None false bo) in
 445           Cic.Constant (name,bo',ty',[],attrs))
 446
 447
 448   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
 449 let rev_uniq =
 450   let module SortedItem =
 451     struct
 452       type t = DisambiguateTypes.domain_item
 453       let compare = Pervasives.compare
 454     end
 455   in
 456   let module Set = Set.Make (SortedItem) in
 457   fun l ->
 458     let rev_l = List.rev l in
 459     let (_, uniq_rev_l) =
 460       List.fold_left
 461         (fun (members, rev_l) elt ->
 462           if Set.mem elt members then
 463             (members, rev_l)
 464           else
 465             Set.add elt members, elt :: rev_l)
 466         (Set.empty, []) rev_l
 467     in
 468     List.rev uniq_rev_l
 469
 470 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
 471  * Domain item more in deep in the list will be processed first.
 472  *)
 473 let rec domain_rev_of_term ?(loc = dummy_floc) context = function
 474   | CicNotationPt.AttributedTerm (`Loc loc, term) ->
 475      domain_rev_of_term ~loc context term
 476   | CicNotationPt.AttributedTerm (_, term) ->
 477       domain_rev_of_term ~loc context term
 478   | CicNotationPt.Appl terms ->
 479       List.fold_left
 480        (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
 481   | CicNotationPt.Binder (kind, (var, typ), body) ->
 482       let kind_dom =
 483         match kind with
 484         | `Exists -> [ Symbol ("exists", 0) ]
 485         | _ -> []
 486       in
 487       let type_dom = domain_rev_of_term_option loc context typ in
 488       let body_dom =
 489         domain_rev_of_term ~loc
 490           (CicNotationUtil.cic_name_of_name var :: context) body
 491       in
 492       body_dom @ type_dom @ kind_dom
 493   | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
 494       let term_dom = domain_rev_of_term ~loc context term in
 495       let outtype_dom = domain_rev_of_term_option loc context outtype in
 496       let get_first_constructor = function
 497         | [] -> []
 498         | ((head, _), _) :: _ -> [ Id head ]
 499       in
 500       let do_branch ((head, args), term) =
 501         let (term_context, args_domain) =
 502           List.fold_left
 503             (fun (cont, dom) (name, typ) ->
 504               (CicNotationUtil.cic_name_of_name name :: cont,
 505                (match typ with
 506                | None -> dom
 507                | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
 508             (context, []) args
 509         in
 510         args_domain @ domain_rev_of_term ~loc term_context term
 511       in
 512       let branches_dom =
 513         List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
 514       in
 515       branches_dom @ outtype_dom @ term_dom @
 516       (match indty_ident with
 517        | None -> get_first_constructor branches
 518        | Some ident -> [ Id ident ])
 519   | CicNotationPt.Cast (term, ty) ->
 520       let term_dom = domain_rev_of_term ~loc context term in
 521       let ty_dom = domain_rev_of_term ~loc context ty in
 522       ty_dom @ term_dom
 523   | CicNotationPt.LetIn ((var, typ), body, where) ->
 524       let body_dom = domain_rev_of_term ~loc context body in
 525       let type_dom = domain_rev_of_term_option loc context typ in
 526       let where_dom =
 527         domain_rev_of_term ~loc
 528           (CicNotationUtil.cic_name_of_name var :: context) where
 529       in
 530       where_dom @ type_dom @ body_dom
 531   | CicNotationPt.LetRec (kind, defs, where) ->
 532       let context' =
 533         List.fold_left
 534           (fun acc ((var, typ), _, _) ->
 535             CicNotationUtil.cic_name_of_name var :: acc)
 536           context defs
 537       in
 538       let where_dom = domain_rev_of_term ~loc context' where in
 539       let defs_dom =
 540         List.fold_left
 541           (fun dom ((_, typ), body, _) ->
 542             domain_rev_of_term ~loc context' body @
 543             domain_rev_of_term_option loc context typ)
 544           [] defs
 545       in
 546       where_dom @ defs_dom
 547   | CicNotationPt.Ident (name, subst) ->
 548       (try
 549         let index = find_in_environment name context in
 550         if subst <> None then
 551           CicNotationPt.fail loc "Explicit substitutions not allowed here"
 552         else
 553           []
 554       with Not_found ->
 555         (match subst with
 556         | None -> [Id name]
 557         | Some subst ->
 558             List.fold_left
 559               (fun dom (_, term) ->
 560                 let dom' = domain_rev_of_term ~loc context term in
 561                 dom' @ dom)
 562               [Id name] subst))
 563   | CicNotationPt.Uri _ -> []
 564   | CicNotationPt.Implicit -> []
 565   | CicNotationPt.Num (num, i) -> [ Num i ]
 566   | CicNotationPt.Meta (index, local_context) ->
 567       List.fold_left
 568        (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
 569         local_context
 570   | CicNotationPt.Sort _ -> []
 571   | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
 572   | CicNotationPt.UserInput
 573   | CicNotationPt.Literal _
 574   | CicNotationPt.Layout _
 575   | CicNotationPt.Magic _
 576   | CicNotationPt.Variable _ -> assert false
 577
 578 and domain_rev_of_term_option loc context = function
 579   | None -> []
 580   | Some t -> domain_rev_of_term ~loc context t
 581
 582 let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast)
 583
 584 let domain_of_obj ~context ast =
 585  assert (context = []);
 586  let domain_rev =
 587   match ast with
 588    | GrafiteAst.Theorem (_,_,ty,bo) ->
 589       (match bo with
 590           None -> []
 591         | Some bo -> domain_rev_of_term [] bo) @
 592       domain_of_term [] ty
 593    | GrafiteAst.Inductive (params,tyl) ->
 594       let dom =
 595        List.flatten (
 596         List.rev_map
 597          (fun (_,_,ty,cl) ->
 598            List.flatten (
 599             List.rev_map
 600              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
 601             domain_rev_of_term [] ty) tyl) in
 602       let dom =
 603        List.fold_left
 604         (fun dom (_,ty) ->
 605           domain_rev_of_term [] ty @ dom
 606         ) dom params
 607       in
 608        List.filter
 609         (fun name ->
 610           not (  List.exists (fun (name',_) -> name = Id name') params
 611               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
 612         ) dom
 613    | GrafiteAst.Record (params,_,ty,fields) ->
 614       let dom =
 615        List.flatten
 616         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
 617       let dom =
 618        List.filter
 619         (fun name->
 620           not (  List.exists (fun (name',_) -> name = Id name') params
 621               || List.exists (fun (name',_) -> name = Id name') fields)
 622         ) dom
 623       in
 624        List.fold_left
 625         (fun dom (_,ty) ->
 626           domain_rev_of_term [] ty @ dom
 627         ) (dom @ domain_rev_of_term [] ty) params
 628  in
 629   rev_uniq domain_rev
 630
 631   (* dom1 \ dom2 *)
 632 let domain_diff dom1 dom2 =
 633 (* let domain_diff = Domain.diff *)
 634   let is_in_dom2 =
 635     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
 636       (fun _ -> false) dom2
 637   in
 638   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 639
 640 module type Disambiguator =
 641 sig
 642   val disambiguate_term :
 643     ?fresh_instances:bool ->
 644     dbd:Mysql.dbd ->
 645     context:Cic.context ->
 646     metasenv:Cic.metasenv ->
 647     ?initial_ugraph:CicUniv.universe_graph ->
 648     aliases:aliases ->  (* previous interpretation status *)
 649     CicNotationPt.term ->
 650     (environment *                   (* new interpretation status *)
 651      Cic.metasenv *                  (* new metasenv *)
 652      Cic.term*
 653      CicUniv.universe_graph) list *  (* disambiguated term *)
 654     bool
 655
 656   val disambiguate_obj :
 657     ?fresh_instances:bool ->
 658     dbd:Mysql.dbd ->
 659     aliases:aliases ->           (* previous interpretation status *)
 660     uri:UriManager.uri option ->     (* required only for inductive types *)
 661     GrafiteAst.obj ->
 662     (environment *                   (* new interpretation status *)
 663      Cic.metasenv *                  (* new metasenv *)
 664      Cic.obj *
 665      CicUniv.universe_graph) list *  (* disambiguated obj *)
 666     bool
 667 end
 668
 669 module Make (C: Callbacks) =
 670   struct
 671     let choices_of_id dbd id =
 672       let uris = MetadataQuery.locate ~dbd id in
 673       let uris =
 674        match uris with
 675         | [] ->
 676            [(C.input_or_locate_uri
 677             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
 678         | [uri] -> [uri]
 679         | _ ->
 680             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
 681              ~ok:"Try selected." ~enable_button_for_non_vars:true
 682              ~title:"Ambiguous input." ~id
 683              ~msg: ("Ambiguous input \"" ^ id ^
 684                 "\". Please, choose one or more interpretations:")
 685              uris
 686       in
 687       List.map
 688         (fun uri ->
 689           (UriManager.string_of_uri uri,
 690            let term =
 691              try
 692                CicUtil.term_of_uri uri
 693              with exn ->
 694                debug_print (UriManager.string_of_uri uri);
 695                debug_print (Printexc.to_string exn);
 696                assert false
 697             in
 698            fun _ _ _ -> term))
 699         uris
 700
 701     let disambiguate_thing ~dbd ~context ~metasenv
 702       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases
 703       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
 704     =
 705       debug_print "DISAMBIGUATE INPUT";
 706       let current_env, multi_aliases_env =
 707         match aliases with
 708         | false, e -> Environment.hd e, None
 709         | true, e -> Environment.empty, Some e
 710       in
 711       let disambiguate_context =  (* cic context -> disambiguate context *)
 712         List.map
 713           (function None -> Cic.Anonymous | Some (name, _) -> name)
 714           context
 715       in
 716       debug_print ("TERM IS: " ^ (pp_thing thing));
 717       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
 718       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
 719         (string_of_domain thing_dom));
 720       debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
 721         (DisambiguatePp.pp_environment (snd aliases)));
 722       let current_dom =
 723         Environment.fold (fun item _ dom -> item :: dom) current_env []
 724       in
 725       let todo_dom = domain_diff thing_dom current_dom in
 726       (* (2) lookup function for any item (Id/Symbol/Num) *)
 727       let lookup_choices =
 728         let id_choices = Hashtbl.create 1023 in
 729         fun item ->
 730           let choices =
 731             let lookup_in_library () =
 732               match item with
 733               | Id id -> choices_of_id dbd id
 734               | Symbol (symb, _) ->
 735                   List.map DisambiguateChoices.mk_choice
 736                     (CicNotationRew.lookup_interpretations symb)
 737               | Num instance ->
 738                   DisambiguateChoices.lookup_num_choices ()
 739             in
 740             match multi_aliases_env with
 741             | None -> lookup_in_library ()
 742             | Some e ->
 743                 (try
 744                   Environment.find item e
 745                 with Not_found -> lookup_in_library ())
 746           in
 747           if choices = [] then raise (No_choices item);
 748           choices
 749       in
 750 (*
 751       (* <benchmark> *)
 752       let _ =
 753         if benchmark then begin
 754           let per_item_choices =
 755             List.map
 756               (fun dom_item ->
 757                 try
 758                   let len = List.length (lookup_choices dom_item) in
 759                   debug_print (sprintf "BENCHMARK %s: %d"
 760                     (string_of_domain_item dom_item) len);
 761                   len
 762                 with No_choices _ -> 0)
 763               thing_dom
 764           in
 765           max_refinements := List.fold_left ( * ) 1 per_item_choices;
 766           actual_refinements := 0;
 767           domain_size := List.length thing_dom;
 768           choices_avg :=
 769             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
 770         end
 771       in
 772       (* </benchmark> *)
 773 *)
 774
 775       (* (3) test an interpretation filling with meta uninterpreted identifiers
 776        *)
 777       let test_env current_env todo_dom ugraph =
 778         let filled_env =
 779           List.fold_left
 780             (fun env item ->
 781                Environment.add item
 782                ("Implicit",
 783                  (match item with
 784                     | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
 785                     | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
 786             current_env todo_dom
 787         in
 788         try
 789           let cic_thing =
 790             interpretate_thing ~context:disambiguate_context ~env:filled_env
 791              ~uri ~is_path:false thing
 792           in
 793           let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
 794             (k , ugraph1 )
 795         with
 796         | Try_again -> Uncertain, ugraph
 797         | Invalid_choice -> Ko, ugraph
 798       in
 799       (* (4) build all possible interpretations *)
 800       let rec aux current_env todo_dom base_univ =
 801         match todo_dom with
 802         | [] ->
 803             (match test_env current_env [] base_univ with
 804             | Ok (thing, metasenv),new_univ ->
 805                [ current_env, metasenv, thing, new_univ ]
 806             | Ko,_ | Uncertain,_ -> [])
 807         | item :: remaining_dom ->
 808             debug_print (sprintf "CHOOSED ITEM: %s"
 809              (string_of_domain_item item));
 810             let choices = lookup_choices item in
 811             let rec filter univ = function
 812               | [] -> []
 813               | codomain_item :: tl ->
 814                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
 815                   let new_env =
 816                     Environment.add item codomain_item current_env
 817                   in
 818                   (match test_env new_env remaining_dom univ with
 819                   | Ok (thing, metasenv),new_univ ->
 820                       (match remaining_dom with
 821                       | [] -> [ new_env, metasenv, thing, new_univ ]
 822                       | _ -> aux new_env remaining_dom new_univ )@
 823                         filter univ tl
 824                   | Uncertain,new_univ ->
 825                       (match remaining_dom with
 826                       | [] -> []
 827                       | _ -> aux new_env remaining_dom new_univ )@
 828                         filter univ tl
 829                   | Ko,_ -> filter univ tl)
 830             in
 831             filter base_univ choices
 832       in
 833       let base_univ = initial_ugraph in
 834       try
 835         let res =
 836          match aux current_env todo_dom base_univ with
 837          | [] -> raise NoWellTypedInterpretation
 838          | [ e,me,t,u ] ->
 839              debug_print "SINGLE INTERPRETATION";
 840              [ e,me,t,u ], false
 841          | l ->
 842              debug_print (sprintf "MANY INTERPRETATIONS (%d)" (List.length l));
 843              let choices =
 844                List.map
 845                  (fun (env, _, _, _) ->
 846                    List.map
 847                      (fun domain_item ->
 848                        let description =
 849                          fst (Environment.find domain_item env)
 850                        in
 851                        (descr_of_domain_item domain_item, description))
 852                      thing_dom)
 853                  l
 854              in
 855              let choosed = C.interactive_interpretation_choice choices in
 856              (List.map (List.nth l) choosed), true
 857         in
 858 (*
 859         (if benchmark then
 860           let res_size = List.length res in
 861           debug_print (sprintf
 862             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
 863             "BENCHMARK:   estimated %.2f")
 864             !actual_refinements !max_refinements !domain_size res_size
 865             !choices_avg
 866             (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
 867 *)
 868       let choices, b = res in
 869       (List.map
 870         (fun (env, metasenv, t, ugraph) ->
 871           Environment.fold Environment.cons env (snd aliases),
 872           metasenv, t, ugraph)
 873         choices),
 874       b
 875      with
 876       CicEnvironment.CircularDependency s ->
 877         failwith "Disambiguate: circular dependency"
 878
 879     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
 880       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
 881     =
 882       let term =
 883         if fresh_instances then CicNotationUtil.freshen_term term else term
 884       in
 885       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
 886         ~uri:None ~pp_thing:CicNotationPp.pp_term
 887         ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
 888         ~refine_thing:refine_term term
 889
 890     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~uri obj =
 891       let obj =
 892         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
 893       in
 894       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
 895         ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
 896         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
 897         obj
 898   end
 899
 900 module Trivial =
 901 struct
 902   exception Ambiguous_term of string
 903   exception Exit
 904   module Callbacks =
 905   struct
 906     let interactive_user_uri_choice ~selection_mode ?ok
 907           ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
 908               raise Exit
 909     let interactive_interpretation_choice interp = raise Exit
 910     let input_or_locate_uri ~(title:string) ?id = raise Exit
 911   end
 912   module Disambiguator = Make (Callbacks)
 913   let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
 914     ?(aliases = DisambiguateTypes.Environment.empty) term
 915   =
 916     let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
 917     try
 918       fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
 919         ?initial_ugraph ~aliases:(false, aliases))
 920     with Exit -> raise (Ambiguous_term term)
 921 end
 922