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