helm/software/components/grafite_parser/grafiteDisambiguate.ml

   1 (*
   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 exception BaseUriNotSetYet
  29
  30 type tactic =
  31  (CicNotationPt.term, CicNotationPt.term,
  32   CicNotationPt.term GrafiteAst.reduction, string)
  33    GrafiteAst.tactic
  34
  35 type lazy_tactic =
  36   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
  37     GrafiteAst.tactic
  38
  39 let singleton msg = function
  40   | [x], _ -> x
  41   | l, _   ->
  42       let debug =
  43          Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
  44          msg (List.length l)
  45       in
  46       HLog.debug debug; assert false
  47
  48 (*
  49 let cic_codomain_of_uri uri =
  50   (UriManager.string_of_uri uri,
  51    let term =
  52      try
  53        CicUtil.term_of_uri uri
  54      with exn ->
  55        assert false
  56     in
  57    fun _ _ _ -> term)
  58 ;;
  59 *)
  60
  61 (*let cic_num_choices = DisambiguateChoices.lookup_num_choices;;*)
  62
  63 let __Implicit = "__Implicit__"
  64 let __Closed_Implicit = "__Closed_Implicit__"
  65
  66 let cic_mk_choice = function
  67   | LexiconAst.Symbol_alias (name, _, dsc) ->
  68      if name = __Implicit then
  69        dsc, `Sym_interp (fun _ -> Cic.Implicit None)
  70      else if name = __Closed_Implicit then
  71        dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed))
  72      else
  73        DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc
  74   | LexiconAst.Number_alias (_, dsc) ->
  75      DisambiguateChoices.lookup_num_by_dsc dsc
  76   | LexiconAst.Ident_alias (name, uri) ->
  77      uri, `Sym_interp
  78       (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri))
  79 ;;
  80
  81 let cic_mk_implicit b =
  82   match b with
  83   | false ->
  84       LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
  85   | true ->
  86       LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
  87 ;;
  88
  89 let ncic_codomain_of_uri uri =
  90   (UriManager.string_of_uri uri,
  91    let term =
  92      try
  93        fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))
  94      with exn ->
  95        assert false
  96     in
  97    fun _ _ _ -> term)
  98 ;;
  99
 100 let ncic_num_choices _ = (*assert false*) [];;
 101 let ncic_mk_choice =
 102   DisambiguateChoices.mk_choice
 103   ~mk_implicit:(function
 104      | true -> NCic.Implicit `Closed
 105      | false -> NCic.Implicit `Term)
 106   ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
 107   ~term_of_uri:(fun uri ->
 108        fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
 109 ;;
 110
 111 let lookup_in_library
 112   interactive_user_uri_choice input_or_locate_uri item
 113 =
 114   let mk_ident_alias id u =
 115     LexiconAst.Ident_alias (id,UriManager.string_of_uri u)
 116   in
 117   let mk_num_alias instance =
 118     List.map
 119      (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc))
 120      (DisambiguateChoices.lookup_num_choices())
 121   in
 122   let mk_symbol_alias symb ino (dsc, _,_) =
 123      LexiconAst.Symbol_alias (symb,ino,dsc)
 124   in
 125   let dbd = LibraryDb.instance () in
 126   let choices_of_id id =
 127     let uris = Whelp.locate ~dbd id in
 128      match uris with
 129       | [] ->
 130          (match
 131            (input_or_locate_uri
 132              ~title:("URI matching \"" ^ id ^ "\" unknown.")
 133              ?id:(Some id) ())
 134          with
 135          | None -> []
 136          | Some uri -> [uri])
 137       | [uri] -> [uri]
 138       | _ ->
 139           interactive_user_uri_choice ~selection_mode:`MULTIPLE
 140            ?ok:(Some "Try selected.")
 141            ?enable_button_for_non_vars:(Some true)
 142            ~title:"Ambiguous input."
 143            ~msg: ("Ambiguous input \"" ^ id ^
 144               "\". Please, choose one or more interpretations:")
 145            ~id
 146            uris
 147   in
 148   match item with
 149   | DisambiguateTypes.Id id ->
 150       let uris = choices_of_id id in
 151       List.map (mk_ident_alias id) uris
 152   | DisambiguateTypes.Symbol (symb, ino) ->
 153    (try
 154      List.map (mk_symbol_alias symb ino)
 155       (TermAcicContent.lookup_interpretations symb)
 156     with
 157      TermAcicContent.Interpretation_not_found -> [])
 158   | DisambiguateTypes.Num instance -> mk_num_alias instance
 159 ;;
 160
 161   (** @param term not meaningful when context is given *)
 162 let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
 163 term =
 164   let lexicon_status = !lexicon_status_ref in
 165   let (diff, metasenv, subst, cic, _) =
 166     singleton "first"
 167       (CicDisambiguate.disambiguate_term
 168         ~aliases:lexicon_status.LexiconEngine.aliases
 169         ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 170         ~lookup_in_library
 171         ~mk_choice:cic_mk_choice
 172         ~mk_implicit:cic_mk_implicit
 173         ~description_of_alias:LexiconAst.description_of_alias
 174         ~context ~metasenv ~subst:[] (text,prefix_len,term))
 175   in
 176   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 177   lexicon_status_ref := lexicon_status;
 178   metasenv,(*subst,*) cic
 179 ;;
 180
 181   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
 182    * rationale: lazy_term will be invoked in different context to obtain a term,
 183    * each invocation will disambiguate the term and can add aliases. Once all
 184    * disambiguations have been performed, the first returned function can be
 185    * used to obtain the resulting aliases *)
 186 let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
 187   (fun context metasenv ugraph ->
 188     let lexicon_status = !lexicon_status_ref in
 189     let (diff, metasenv, _, cic, ugraph) =
 190       singleton "second"
 191         (CicDisambiguate.disambiguate_term
 192           ~lookup_in_library
 193           ~mk_choice:cic_mk_choice
 194           ~mk_implicit:cic_mk_implicit
 195           ~description_of_alias:LexiconAst.description_of_alias
 196           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
 197           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 198           ~context ~metasenv ~subst:[] ?goal
 199           (text,prefix_len,term)) in
 200     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 201     lexicon_status_ref := lexicon_status;
 202     cic, metasenv, ugraph)
 203 ;;
 204
 205 let disambiguate_pattern
 206   text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path)
 207 =
 208   let interp path =CicDisambiguate.interpretate_path [] path in
 209   let goal_path = HExtlib.map_option interp goal_path in
 210   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 211   let wanted =
 212    match wanted with
 213       None -> None
 214     | Some wanted ->
 215        let wanted =
 216          disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted
 217        in
 218        Some wanted
 219   in
 220   (wanted, hyp_paths, goal_path)
 221 ;;
 222
 223 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 224   | `Unfold (Some t) ->
 225       let t =
 226          disambiguate_lazy_term None text prefix_len lexicon_status_ref t in
 227       `Unfold (Some t)
 228   | `Normalize
 229   | `Simpl
 230   | `Unfold None
 231   | `Whd as kind -> kind
 232 ;;
 233
 234 let disambiguate_auto_params
 235   disambiguate_term metasenv context (terms, params)
 236 =
 237     let metasenv, terms =
 238       List.fold_right
 239        (fun t (metasenv, terms) ->
 240          let metasenv,t = disambiguate_term context metasenv t in
 241          metasenv,t::terms) terms (metasenv, [])
 242     in
 243     metasenv, (terms, params)
 244 ;;
 245
 246 let disambiguate_just disambiguate_term context metasenv =
 247  function
 248     `Term t ->
 249       let metasenv,t = disambiguate_term context metasenv t in
 250        metasenv, `Term t
 251   | `Auto params ->
 252       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
 253        context params
 254       in
 255        metasenv, `Auto params
 256 ;;
 257
 258 let rec disambiguate_tactic
 259   lexicon_status_ref context metasenv goal (text,prefix_len,tactic)
 260 =
 261   let disambiguate_term_hint =
 262     disambiguate_term goal text prefix_len lexicon_status_ref in
 263   let disambiguate_term =
 264     disambiguate_term None text prefix_len lexicon_status_ref in
 265   let disambiguate_pattern =
 266     disambiguate_pattern text prefix_len lexicon_status_ref in
 267   let disambiguate_reduction_kind =
 268     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
 269   let disambiguate_lazy_term =
 270     disambiguate_lazy_term None text prefix_len lexicon_status_ref in
 271   let disambiguate_tactic metasenv tac =
 272    disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac)
 273   in
 274   let disambiguate_auto_params m p =
 275     disambiguate_auto_params disambiguate_term m context p
 276   in
 277    match tactic with
 278     (* Higher  order tactics *)
 279     | GrafiteAst.Progress (loc,tac) ->
 280         let metasenv,tac = disambiguate_tactic metasenv tac in
 281         metasenv,GrafiteAst.Progress (loc,tac)
 282     | GrafiteAst.Solve (loc,tacl) ->
 283         let metasenv,tacl =
 284          List.fold_right
 285           (fun tac (metasenv,tacl) ->
 286             let metasenv,tac = disambiguate_tactic metasenv tac in
 287              metasenv,tac::tacl
 288           ) tacl (metasenv,[])
 289         in
 290          metasenv,GrafiteAst.Solve (loc,tacl)
 291     | GrafiteAst.Try (loc,tac) ->
 292         let metasenv,tac = disambiguate_tactic metasenv tac in
 293         metasenv,GrafiteAst.Try (loc,tac)
 294     | GrafiteAst.First (loc,tacl) ->
 295         let metasenv,tacl =
 296          List.fold_right
 297           (fun tac (metasenv,tacl) ->
 298             let metasenv,tac = disambiguate_tactic metasenv tac in
 299              metasenv,tac::tacl
 300           ) tacl (metasenv,[])
 301         in
 302          metasenv,GrafiteAst.First (loc,tacl)
 303     | GrafiteAst.Seq (loc,tacl) ->
 304         let metasenv,tacl =
 305          List.fold_right
 306           (fun tac (metasenv,tacl) ->
 307             let metasenv,tac = disambiguate_tactic metasenv tac in
 308              metasenv,tac::tacl
 309           ) tacl (metasenv,[])
 310         in
 311          metasenv,GrafiteAst.Seq (loc,tacl)
 312     | GrafiteAst.Repeat (loc,tac) ->
 313         let metasenv,tac = disambiguate_tactic metasenv tac in
 314         metasenv,GrafiteAst.Repeat (loc,tac)
 315     | GrafiteAst.Do (loc,n,tac) ->
 316         let metasenv,tac = disambiguate_tactic metasenv tac in
 317         metasenv,GrafiteAst.Do (loc,n,tac)
 318     | GrafiteAst.Then (loc,tac,tacl) ->
 319         let metasenv,tac = disambiguate_tactic metasenv tac in
 320         let metasenv,tacl =
 321          List.fold_right
 322           (fun tac (metasenv,tacl) ->
 323             let metasenv,tac = disambiguate_tactic metasenv tac in
 324              metasenv,tac::tacl
 325           ) tacl (metasenv,[])
 326         in
 327          metasenv,GrafiteAst.Then (loc,tac,tacl)
 328     (* First order tactics *)
 329     | GrafiteAst.Absurd (loc, term) ->
 330         let metasenv,cic = disambiguate_term context metasenv term in
 331         metasenv,GrafiteAst.Absurd (loc, cic)
 332     | GrafiteAst.Apply (loc, term) ->
 333         let metasenv,cic = disambiguate_term context metasenv term in
 334         metasenv,GrafiteAst.Apply (loc, cic)
 335     | GrafiteAst.ApplyRule (loc, term) ->
 336         let metasenv,cic = disambiguate_term_hint context metasenv term in
 337         metasenv,GrafiteAst.ApplyRule (loc, cic)
 338     | GrafiteAst.ApplyP (loc, term) ->
 339         let metasenv,cic = disambiguate_term context metasenv term in
 340         metasenv,GrafiteAst.ApplyP (loc, cic)
 341     | GrafiteAst.ApplyS (loc, term, params) ->
 342         let metasenv, params = disambiguate_auto_params metasenv params in
 343         let metasenv,cic = disambiguate_term context metasenv term in
 344         metasenv,GrafiteAst.ApplyS (loc, cic, params)
 345     | GrafiteAst.Assumption loc ->
 346         metasenv,GrafiteAst.Assumption loc
 347     | GrafiteAst.AutoBatch (loc,params) ->
 348         let metasenv, params = disambiguate_auto_params metasenv params in
 349         metasenv,GrafiteAst.AutoBatch (loc,params)
 350     | GrafiteAst.Cases (loc, what, pattern, idents) ->
 351         let metasenv,what = disambiguate_term context metasenv what in
 352         let pattern = disambiguate_pattern pattern in
 353         metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
 354     | GrafiteAst.Change (loc, pattern, with_what) ->
 355         let with_what = disambiguate_lazy_term with_what in
 356         let pattern = disambiguate_pattern pattern in
 357         metasenv,GrafiteAst.Change (loc, pattern, with_what)
 358     | GrafiteAst.Clear (loc,id) ->
 359         metasenv,GrafiteAst.Clear (loc,id)
 360     | GrafiteAst.ClearBody (loc,id) ->
 361        metasenv,GrafiteAst.ClearBody (loc,id)
 362     | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
 363         let metasenv,t1 = disambiguate_term context metasenv t1 in
 364         let metasenv,t2 =
 365           match t2 with
 366           | None -> metasenv, None
 367           | Some t2 ->
 368               let m, t2 = disambiguate_term context metasenv t2 in
 369               m, Some t2
 370         in
 371         metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
 372     | GrafiteAst.Constructor (loc,n) ->
 373         metasenv,GrafiteAst.Constructor (loc,n)
 374     | GrafiteAst.Contradiction loc ->
 375         metasenv,GrafiteAst.Contradiction loc
 376     | GrafiteAst.Cut (loc, ident, term) ->
 377         let metasenv,cic = disambiguate_term context metasenv term in
 378         metasenv,GrafiteAst.Cut (loc, ident, cic)
 379     | GrafiteAst.Decompose (loc, names) ->
 380          metasenv,GrafiteAst.Decompose (loc, names)
 381     | GrafiteAst.Demodulate (loc, params) ->
 382         let metasenv, params = disambiguate_auto_params metasenv params in
 383         metasenv,GrafiteAst.Demodulate (loc, params)
 384     | GrafiteAst.Destruct (loc, Some terms) ->
 385         let map term (metasenv, terms) =
 386            let metasenv, term = disambiguate_term context metasenv term in
 387            metasenv, term :: terms
 388         in
 389         let metasenv, terms = List.fold_right map terms (metasenv, []) in
 390         metasenv, GrafiteAst.Destruct(loc, Some terms)
 391     | GrafiteAst.Destruct (loc, None) ->
 392         metasenv,GrafiteAst.Destruct(loc,None)
 393     | GrafiteAst.Exact (loc, term) ->
 394         let metasenv,cic = disambiguate_term context metasenv term in
 395         metasenv,GrafiteAst.Exact (loc, cic)
 396     | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
 397         let metasenv,what = disambiguate_term context metasenv what in
 398         let metasenv,using = disambiguate_term context metasenv using in
 399         let pattern = disambiguate_pattern pattern in
 400         metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
 401     | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
 402         let metasenv,what = disambiguate_term context metasenv what in
 403         let pattern = disambiguate_pattern pattern in
 404         metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
 405     | GrafiteAst.ElimType (loc, what, Some using, specs) ->
 406         let metasenv,what = disambiguate_term context metasenv what in
 407         let metasenv,using = disambiguate_term context metasenv using in
 408         metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
 409     | GrafiteAst.ElimType (loc, what, None, specs) ->
 410         let metasenv,what = disambiguate_term context metasenv what in
 411         metasenv,GrafiteAst.ElimType (loc, what, None, specs)
 412     | GrafiteAst.Exists loc ->
 413         metasenv,GrafiteAst.Exists loc
 414     | GrafiteAst.Fail loc ->
 415         metasenv,GrafiteAst.Fail loc
 416     | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
 417         let pattern = disambiguate_pattern pattern in
 418         let term = disambiguate_lazy_term term in
 419         let red_kind = disambiguate_reduction_kind red_kind in
 420         metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
 421     | GrafiteAst.FwdSimpl (loc, hyp, names) ->
 422        metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
 423     | GrafiteAst.Fourier loc ->
 424        metasenv,GrafiteAst.Fourier loc
 425     | GrafiteAst.Generalize (loc,pattern,ident) ->
 426         let pattern = disambiguate_pattern pattern in
 427         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
 428     | GrafiteAst.IdTac loc ->
 429         metasenv,GrafiteAst.IdTac loc
 430     | GrafiteAst.Intros (loc, specs) ->
 431         metasenv,GrafiteAst.Intros (loc, specs)
 432     | GrafiteAst.Inversion (loc, term) ->
 433        let metasenv,term = disambiguate_term context metasenv term in
 434         metasenv,GrafiteAst.Inversion (loc, term)
 435     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
 436        let f term (metasenv, to_what) =
 437           let metasenv, term = disambiguate_term context metasenv term in
 438           metasenv, term :: to_what
 439        in
 440        let metasenv, to_what = List.fold_right f to_what (metasenv, []) in
 441        let metasenv, what = disambiguate_term context metasenv what in
 442        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
 443     | GrafiteAst.Left loc ->
 444        metasenv,GrafiteAst.Left loc
 445     | GrafiteAst.LetIn (loc, term, name) ->
 446         let metasenv,term = disambiguate_term context metasenv term in
 447         metasenv,GrafiteAst.LetIn (loc,term,name)
 448     | GrafiteAst.Reduce (loc, red_kind, pattern) ->
 449         let pattern = disambiguate_pattern pattern in
 450         let red_kind = disambiguate_reduction_kind red_kind in
 451         metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
 452     | GrafiteAst.Reflexivity loc ->
 453         metasenv,GrafiteAst.Reflexivity loc
 454     | GrafiteAst.Replace (loc, pattern, with_what) ->
 455         let pattern = disambiguate_pattern pattern in
 456         let with_what = disambiguate_lazy_term with_what in
 457         metasenv,GrafiteAst.Replace (loc, pattern, with_what)
 458     | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
 459         let metasenv,term = disambiguate_term context metasenv t in
 460         let pattern = disambiguate_pattern pattern in
 461         metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
 462     | GrafiteAst.Right loc ->
 463         metasenv,GrafiteAst.Right loc
 464     | GrafiteAst.Ring loc ->
 465         metasenv,GrafiteAst.Ring loc
 466     | GrafiteAst.Split loc ->
 467         metasenv,GrafiteAst.Split loc
 468     | GrafiteAst.Symmetry loc ->
 469         metasenv,GrafiteAst.Symmetry loc
 470     | GrafiteAst.Transitivity (loc, term) ->
 471         let metasenv,cic = disambiguate_term context metasenv term in
 472         metasenv,GrafiteAst.Transitivity (loc, cic)
 473       (* Nuovi casi *)
 474     | GrafiteAst.Assume (loc, id, term) ->
 475         let metasenv,cic = disambiguate_term context metasenv term in
 476         metasenv,GrafiteAst.Assume (loc, id, cic)
 477     | GrafiteAst.Suppose (loc, term, id, term') ->
 478         let metasenv,cic = disambiguate_term context metasenv term in
 479         let metasenv,cic' =
 480            match term' with
 481               None -> metasenv,None
 482             | Some t ->
 483                   let metasenv,t = disambiguate_term context metasenv t in
 484                   metasenv,Some t in
 485         metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
 486     | GrafiteAst.Bydone (loc,just) ->
 487         let metasenv,just =
 488          disambiguate_just disambiguate_term context metasenv just
 489         in
 490          metasenv,GrafiteAst.Bydone (loc, just)
 491     | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
 492         let metasenv,cic = disambiguate_term context metasenv term in
 493         let metasenv,cic' =
 494             match term' with
 495               None -> metasenv,None
 496             | Some t ->
 497                   let metasenv,t = disambiguate_term context metasenv t in
 498                   metasenv,Some t in
 499         metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
 500     | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') ->
 501         let metasenv,just =
 502          disambiguate_just disambiguate_term context metasenv just in
 503         let metasenv,cic' = disambiguate_term context metasenv term' in
 504         let metasenv,cic'' =
 505             match term'' with
 506               None -> metasenv,None
 507            |  Some t ->
 508                     let metasenv,t = disambiguate_term context metasenv t in
 509                      metasenv,Some t in
 510         metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'')
 511     | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
 512         let metasenv,cic = disambiguate_term context metasenv term in
 513         let metasenv,cic' = disambiguate_term context metasenv term' in
 514         metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
 515     | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
 516         let metasenv,cic = disambiguate_term context metasenv term in
 517         let metasenv,cic' = disambiguate_term context metasenv term' in
 518         metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
 519    | GrafiteAst.Byinduction (loc, term, id) ->
 520         let metasenv,cic = disambiguate_term context metasenv term in
 521         metasenv,GrafiteAst.Byinduction(loc, cic, id)
 522    | GrafiteAst.Thesisbecomes (loc, term) ->
 523         let metasenv,cic = disambiguate_term context metasenv term in
 524         metasenv,GrafiteAst.Thesisbecomes (loc, cic)
 525    | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) ->
 526         let metasenv,just =
 527          disambiguate_just disambiguate_term context metasenv just in
 528         let metasenv,cic' = disambiguate_term context metasenv term1 in
 529         let cic''= disambiguate_lazy_term term2 in
 530         metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
 531    | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
 532         let metasenv,just =
 533          disambiguate_just disambiguate_term context metasenv just in
 534         let metasenv,cic'= disambiguate_term context metasenv term1 in
 535         let metasenv,cic''= disambiguate_term context metasenv term2 in
 536         metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'')
 537    | GrafiteAst.Case (loc, id, params) ->
 538         let metasenv,params' =
 539          List.fold_right
 540           (fun (id,term) (metasenv,params) ->
 541             let metasenv,cic = disambiguate_term context metasenv term in
 542              metasenv,(id,cic)::params
 543           ) params (metasenv,[])
 544         in
 545         metasenv,GrafiteAst.Case(loc, id, params')
 546    | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
 547         let metasenv,cic =
 548          match term1 with
 549             None -> metasenv,None
 550           | Some (start,t) ->
 551              let metasenv,t = disambiguate_term context metasenv t in
 552               metasenv,Some (start,t) in
 553         let metasenv,cic'= disambiguate_term context metasenv term2 in
 554         let metasenv,cic'' =
 555          match term3 with
 556           | `SolveWith term ->
 557              let metasenv,term = disambiguate_term context metasenv term in
 558              metasenv, `SolveWith term
 559           | `Auto params ->
 560               let metasenv, params = disambiguate_auto_params metasenv params in
 561               metasenv,`Auto params
 562           | `Term t ->
 563              let metasenv,t = disambiguate_term context metasenv t in
 564               metasenv,`Term t
 565           | `Proof as t -> metasenv,t in
 566         metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
 567
 568 let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
 569   let uri =
 570    match obj with
 571     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
 572     | CicNotationPt.Record (_,name,_,_) ->
 573        (match baseuri with
 574          | Some baseuri ->
 575             Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
 576          | None -> raise BaseUriNotSetYet)
 577     | CicNotationPt.Inductive _ -> assert false
 578     | CicNotationPt.Theorem _ -> None in
 579 (*
 580   (match obj with
 581       CicNotationPt.Theorem (_,_,ty,_) ->
 582        (try
 583          (match
 584           NCicDisambiguate.disambiguate_term
 585            ~lookup_in_library:(lookup_in_library ncic_codomain_of_uri
 586            ncic_mk_choice ncic_num_choices)
 587            ~context:[] ~metasenv:[] ~subst:[]
 588            ~aliases:DisambiguateTypes.Environment.empty
 589            ~universe:(Some DisambiguateTypes.Environment.empty)
 590            (text,prefix_len,ty)
 591          with
 592          | [_,metasenv,subst,ty],_ ->
 593           prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!!  " ^
 594            NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
 595          | _ ->
 596           prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!!  "))
 597        with
 598        | MultiPassDisambiguator.DisambiguationError (_,s) ->
 599         prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE:\n" ^
 600          String.concat "\n"
 601           (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
 602 (*        | exn -> prerr_endline (Printexc.to_string exn) *)
 603        )
 604     | _ -> ()
 605   );
 606 *)
 607   let (diff, metasenv, _, cic, _) =
 608     singleton "third"
 609       (CicDisambiguate.disambiguate_obj
 610         ~lookup_in_library
 611         ~mk_choice:cic_mk_choice
 612         ~mk_implicit:cic_mk_implicit
 613         ~description_of_alias:LexiconAst.description_of_alias
 614         ~aliases:lexicon_status.LexiconEngine.aliases
 615         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
 616         (text,prefix_len,obj)) in
 617   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 618   lexicon_status, metasenv, cic
 619
 620 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
 621   match cmd with
 622    | GrafiteAst.Index(loc,key,uri) ->
 623        let lexicon_status_ref = ref lexicon_status in
 624        let disambiguate_term =
 625          disambiguate_term None text prefix_len lexicon_status_ref [] in
 626        let disambiguate_term_option metasenv =
 627          function
 628              None -> metasenv,None
 629            | Some t ->
 630                let metasenv,t = disambiguate_term metasenv t in
 631                  metasenv, Some t
 632        in
 633        let metasenv,key = disambiguate_term_option metasenv key in
 634        !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
 635    | GrafiteAst.Coercion (loc,t,b,a,s) ->
 636        let lexicon_status_ref = ref lexicon_status in
 637        let disambiguate_term =
 638          disambiguate_term None text prefix_len lexicon_status_ref [] in
 639       let metasenv,t = disambiguate_term metasenv t in
 640       !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
 641    | GrafiteAst.Default _
 642    | GrafiteAst.Drop _
 643    | GrafiteAst.Include _
 644    | GrafiteAst.Print _
 645    | GrafiteAst.Qed _
 646    | GrafiteAst.Set _ as cmd ->
 647        lexicon_status,metasenv,cmd
 648    | GrafiteAst.Obj (loc,obj) ->
 649        let lexicon_status,metasenv,obj =
 650         disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
 651        lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
 652    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
 653       let lexicon_status_ref = ref lexicon_status in
 654       let disambiguate_term =
 655        disambiguate_term None text prefix_len lexicon_status_ref [] in
 656       let disambiguate_term_option metasenv =
 657        function
 658           None -> metasenv,None
 659        | Some t ->
 660           let metasenv,t = disambiguate_term metasenv t in
 661            metasenv, Some t
 662       in
 663       let metasenv,a = disambiguate_term metasenv a in
 664       let metasenv,aeq = disambiguate_term metasenv aeq in
 665       let metasenv,refl = disambiguate_term_option metasenv refl in
 666       let metasenv,sym = disambiguate_term_option metasenv sym in
 667       let metasenv,trans = disambiguate_term_option metasenv trans in
 668        !lexicon_status_ref, metasenv,
 669         GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 670
 671 let disambiguate_macro
 672   lexicon_status_ref metasenv context (text,prefix_len, macro)
 673 =
 674  let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in
 675   let disambiguate_reduction_kind =
 676     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
 677   match macro with
 678    | GrafiteAst.WMatch (loc,term) ->
 679       let metasenv,term = disambiguate_term context metasenv term in
 680        metasenv,GrafiteAst.WMatch (loc,term)
 681    | GrafiteAst.WInstance (loc,term) ->
 682       let metasenv,term = disambiguate_term context metasenv term in
 683        metasenv,GrafiteAst.WInstance (loc,term)
 684    | GrafiteAst.WElim (loc,term) ->
 685       let metasenv,term = disambiguate_term context metasenv term in
 686        metasenv,GrafiteAst.WElim (loc,term)
 687    | GrafiteAst.WHint (loc,term) ->
 688       let metasenv,term = disambiguate_term context metasenv term in
 689        metasenv,GrafiteAst.WHint (loc,term)
 690    | GrafiteAst.Check (loc,term) ->
 691       let metasenv,term = disambiguate_term context metasenv term in
 692        metasenv,GrafiteAst.Check (loc,term)
 693    | GrafiteAst.Eval (loc,kind,term) ->
 694       let metasenv, term = disambiguate_term context metasenv term in
 695       let kind = disambiguate_reduction_kind kind in
 696        metasenv,GrafiteAst.Eval (loc,kind,term)
 697    | GrafiteAst.AutoInteractive (loc, params) ->
 698       let metasenv, params =
 699         disambiguate_auto_params disambiguate_term metasenv context params in
 700       metasenv, GrafiteAst.AutoInteractive (loc, params)
 701    | GrafiteAst.Hint _
 702    | GrafiteAst.WLocate _
 703    | GrafiteAst.Inline _ as macro ->
 704       metasenv,macro