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 let __Implicit = "__Implicit__"
  49 let __Closed_Implicit = "__Closed_Implicit__"
  50
  51 let cic_mk_choice = function
  52   | LexiconAst.Symbol_alias (name, _, dsc) ->
  53      if name = __Implicit then
  54        dsc, `Sym_interp (fun _ -> Cic.Implicit None)
  55      else if name = __Closed_Implicit then
  56        dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed))
  57      else
  58        DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc
  59   | LexiconAst.Number_alias (_, dsc) ->
  60      DisambiguateChoices.lookup_num_by_dsc dsc
  61   | LexiconAst.Ident_alias (name, uri) ->
  62      uri, `Sym_interp
  63       (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri))
  64 ;;
  65
  66 let ncic_mk_choice = function
  67   | LexiconAst.Symbol_alias (name, _, dsc) ->
  68      if name = __Implicit then
  69        dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
  70      else if name = __Closed_Implicit then
  71        dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
  72      else
  73        DisambiguateChoices.lookup_symbol_by_dsc
  74         ~mk_implicit:(function
  75            | true -> NCic.Implicit `Closed
  76            | false -> NCic.Implicit `Term)
  77         ~mk_appl:(function
  78            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
  79         ~term_of_uri:(fun uri ->
  80            fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
  81        name dsc
  82   | LexiconAst.Number_alias (_, dsc) ->
  83        let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
  84        desc, `Num_interp
  85          (fun num ->
  86             fst (OCic2NCic.convert_term
  87               (UriManager.uri_of_string "cic:/xxx/x.con")
  88               (match f with `Num_interp f -> f num | _ -> assert false)))
  89   | LexiconAst.Ident_alias (name, uri) ->
  90      uri, `Sym_interp
  91       (fun l->assert(l = []);
  92         if String.sub uri 5 9 = "ng_matita" then
  93          let nuri =
  94           NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
  95          in
  96           NCic.Const
  97            (NReference.reference_of_spec nuri (NReference.Def 0))
  98         else
  99          let uri = UriManager.uri_of_string uri in
 100           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
 101 ;;
 102
 103
 104 let mk_implicit b =
 105   match b with
 106   | false ->
 107       LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
 108   | true ->
 109       LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
 110 ;;
 111
 112 let lookup_in_library
 113   interactive_user_uri_choice input_or_locate_uri item
 114 =
 115   let mk_ident_alias id u =
 116     LexiconAst.Ident_alias (id,UriManager.string_of_uri u)
 117   in
 118   let mk_num_alias instance =
 119     List.map
 120      (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc))
 121      (DisambiguateChoices.lookup_num_choices())
 122   in
 123   let mk_symbol_alias symb ino (dsc, _,_) =
 124      LexiconAst.Symbol_alias (symb,ino,dsc)
 125   in
 126   let dbd = LibraryDb.instance () in
 127   let choices_of_id id =
 128     let uris = Whelp.locate ~dbd id in
 129      match uris with
 130       | [] ->
 131          (match
 132            (input_or_locate_uri
 133              ~title:("URI matching \"" ^ id ^ "\" unknown.")
 134              ?id:(Some id) ())
 135          with
 136          | None -> []
 137          | Some uri -> [uri])
 138       | [uri] -> [uri]
 139       | _ ->
 140           interactive_user_uri_choice ~selection_mode:`MULTIPLE
 141            ?ok:(Some "Try selected.")
 142            ?enable_button_for_non_vars:(Some true)
 143            ~title:"Ambiguous input."
 144            ~msg: ("Ambiguous input \"" ^ id ^
 145               "\". Please, choose one or more interpretations:")
 146            ~id
 147            uris
 148   in
 149   match item with
 150   | DisambiguateTypes.Id id ->
 151       let uris = choices_of_id id in
 152       List.map (mk_ident_alias id) uris
 153   | DisambiguateTypes.Symbol (symb, ino) ->
 154    (try
 155      List.map (mk_symbol_alias symb ino)
 156       (TermAcicContent.lookup_interpretations symb)
 157     with
 158      TermAcicContent.Interpretation_not_found -> [])
 159   | DisambiguateTypes.Num instance -> mk_num_alias instance
 160 ;;
 161
 162   (** @param term not meaningful when context is given *)
 163 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 164 term =
 165   let lexicon_status = !lexicon_status_ref in
 166   let (diff, metasenv, subst, cic, _) =
 167     singleton "first"
 168       (CicDisambiguate.disambiguate_term
 169         ~aliases:lexicon_status.LexiconEngine.aliases
 170         ~expty ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 171         ~lookup_in_library
 172         ~mk_choice:cic_mk_choice
 173         ~mk_implicit
 174         ~description_of_alias:LexiconAst.description_of_alias
 175         ~context ~metasenv ~subst:[] (text,prefix_len,term))
 176   in
 177   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 178   lexicon_status_ref := lexicon_status;
 179   metasenv,(*subst,*) cic
 180 ;;
 181
 182 let disambiguate_nterm expty lexicon_status context metasenv subst thing
 183 =
 184   let diff, metasenv, subst, cic =
 185     singleton "first"
 186       (NCicDisambiguate.disambiguate_term
 187         ~coercion_db:(NCicCoercion.db ())
 188         ~aliases:lexicon_status.LexiconEngine.aliases
 189         ~expty
 190         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 191         ~lookup_in_library
 192         ~mk_choice:ncic_mk_choice
 193         ~mk_implicit
 194         ~description_of_alias:LexiconAst.description_of_alias
 195         ~context ~metasenv ~subst thing)
 196   in
 197   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 198   metasenv, subst, lexicon_status, cic
 199 ;;
 200
 201
 202   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
 203    * rationale: lazy_term will be invoked in different context to obtain a term,
 204    * each invocation will disambiguate the term and can add aliases. Once all
 205    * disambiguations have been performed, the first returned function can be
 206    * used to obtain the resulting aliases *)
 207 let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
 208   (fun context metasenv ugraph ->
 209     let lexicon_status = !lexicon_status_ref in
 210     let (diff, metasenv, _, cic, ugraph) =
 211       singleton "second"
 212         (CicDisambiguate.disambiguate_term
 213           ~lookup_in_library
 214           ~mk_choice:cic_mk_choice
 215           ~mk_implicit
 216           ~description_of_alias:LexiconAst.description_of_alias
 217           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
 218           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 219           ~context ~metasenv ~subst:[]
 220           (text,prefix_len,term) ~expty) in
 221     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 222     lexicon_status_ref := lexicon_status;
 223     cic, metasenv, ugraph)
 224 ;;
 225
 226 let disambiguate_pattern
 227   text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path)
 228 =
 229   let interp path =CicDisambiguate.interpretate_path [] path in
 230   let goal_path = HExtlib.map_option interp goal_path in
 231   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 232   let wanted =
 233    match wanted with
 234       None -> None
 235     | Some wanted ->
 236        let wanted =
 237          disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted
 238        in
 239        Some wanted
 240   in
 241   (wanted, hyp_paths, goal_path)
 242 ;;
 243
 244 type pattern =
 245   CicNotationPt.term Disambiguate.disambiguator_input option *
 246   (string * NCic.term) list * NCic.term option
 247
 248 let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
 249   let interp path = NCicDisambiguate.disambiguate_path path in
 250   let goal_path = HExtlib.map_option interp goal_path in
 251   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 252   let wanted =
 253     match wanted with None -> None | Some x -> Some (text,prefix_len,x)
 254   in
 255    (wanted, hyp_paths, goal_path)
 256 ;;
 257
 258 let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
 259   | `Unfold (Some t) ->
 260       let t =
 261          disambiguate_lazy_term None text prefix_len lexicon_status_ref t in
 262       `Unfold (Some t)
 263   | `Normalize
 264   | `Simpl
 265   | `Unfold None
 266   | `Whd as kind -> kind
 267 ;;
 268
 269 let disambiguate_auto_params
 270   disambiguate_term metasenv context (terms, params)
 271 =
 272     let metasenv, terms =
 273       List.fold_right
 274        (fun t (metasenv, terms) ->
 275          let metasenv,t = disambiguate_term context metasenv t in
 276          metasenv,t::terms) terms (metasenv, [])
 277     in
 278     metasenv, (terms, params)
 279 ;;
 280
 281 let disambiguate_just disambiguate_term context metasenv =
 282  function
 283     `Term t ->
 284       let metasenv,t = disambiguate_term context metasenv t in
 285        metasenv, `Term t
 286   | `Auto params ->
 287       let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
 288        context params
 289       in
 290        metasenv, `Auto params
 291 ;;
 292
 293 let rec disambiguate_tactic
 294   lexicon_status_ref context metasenv goal (text,prefix_len,tactic)
 295 =
 296   let disambiguate_term_hint =
 297     let _,_,expty =
 298       List.find (fun (x,_,_) -> Some x = goal) metasenv
 299     in
 300     disambiguate_term (Some expty) text prefix_len lexicon_status_ref in
 301   let disambiguate_term =
 302     disambiguate_term None text prefix_len lexicon_status_ref in
 303   let disambiguate_pattern =
 304     disambiguate_pattern text prefix_len lexicon_status_ref in
 305   let disambiguate_reduction_kind =
 306     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
 307   let disambiguate_lazy_term =
 308     disambiguate_lazy_term None text prefix_len lexicon_status_ref in
 309   let disambiguate_tactic metasenv tac =
 310    disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac)
 311   in
 312   let disambiguate_auto_params m p =
 313     disambiguate_auto_params disambiguate_term m context p
 314   in
 315    match tactic with
 316     (* Higher  order tactics *)
 317     | GrafiteAst.Progress (loc,tac) ->
 318         let metasenv,tac = disambiguate_tactic metasenv tac in
 319         metasenv,GrafiteAst.Progress (loc,tac)
 320     | GrafiteAst.Solve (loc,tacl) ->
 321         let metasenv,tacl =
 322          List.fold_right
 323           (fun tac (metasenv,tacl) ->
 324             let metasenv,tac = disambiguate_tactic metasenv tac in
 325              metasenv,tac::tacl
 326           ) tacl (metasenv,[])
 327         in
 328          metasenv,GrafiteAst.Solve (loc,tacl)
 329     | GrafiteAst.Try (loc,tac) ->
 330         let metasenv,tac = disambiguate_tactic metasenv tac in
 331         metasenv,GrafiteAst.Try (loc,tac)
 332     | GrafiteAst.First (loc,tacl) ->
 333         let metasenv,tacl =
 334          List.fold_right
 335           (fun tac (metasenv,tacl) ->
 336             let metasenv,tac = disambiguate_tactic metasenv tac in
 337              metasenv,tac::tacl
 338           ) tacl (metasenv,[])
 339         in
 340          metasenv,GrafiteAst.First (loc,tacl)
 341     | GrafiteAst.Seq (loc,tacl) ->
 342         let metasenv,tacl =
 343          List.fold_right
 344           (fun tac (metasenv,tacl) ->
 345             let metasenv,tac = disambiguate_tactic metasenv tac in
 346              metasenv,tac::tacl
 347           ) tacl (metasenv,[])
 348         in
 349          metasenv,GrafiteAst.Seq (loc,tacl)
 350     | GrafiteAst.Repeat (loc,tac) ->
 351         let metasenv,tac = disambiguate_tactic metasenv tac in
 352         metasenv,GrafiteAst.Repeat (loc,tac)
 353     | GrafiteAst.Do (loc,n,tac) ->
 354         let metasenv,tac = disambiguate_tactic metasenv tac in
 355         metasenv,GrafiteAst.Do (loc,n,tac)
 356     | GrafiteAst.Then (loc,tac,tacl) ->
 357         let metasenv,tac = disambiguate_tactic metasenv tac in
 358         let metasenv,tacl =
 359          List.fold_right
 360           (fun tac (metasenv,tacl) ->
 361             let metasenv,tac = disambiguate_tactic metasenv tac in
 362              metasenv,tac::tacl
 363           ) tacl (metasenv,[])
 364         in
 365          metasenv,GrafiteAst.Then (loc,tac,tacl)
 366     (* First order tactics *)
 367     | GrafiteAst.Absurd (loc, term) ->
 368         let metasenv,cic = disambiguate_term context metasenv term in
 369         metasenv,GrafiteAst.Absurd (loc, cic)
 370     | GrafiteAst.Apply (loc, term) ->
 371         let metasenv,cic = disambiguate_term context metasenv term in
 372         metasenv,GrafiteAst.Apply (loc, cic)
 373     | GrafiteAst.ApplyRule (loc, term) ->
 374         let metasenv,cic = disambiguate_term_hint context metasenv term in
 375         metasenv,GrafiteAst.ApplyRule (loc, cic)
 376     | GrafiteAst.ApplyP (loc, term) ->
 377         let metasenv,cic = disambiguate_term context metasenv term in
 378         metasenv,GrafiteAst.ApplyP (loc, cic)
 379     | GrafiteAst.ApplyS (loc, term, params) ->
 380         let metasenv, params = disambiguate_auto_params metasenv params in
 381         let metasenv,cic = disambiguate_term context metasenv term in
 382         metasenv,GrafiteAst.ApplyS (loc, cic, params)
 383     | GrafiteAst.Assumption loc ->
 384         metasenv,GrafiteAst.Assumption loc
 385     | GrafiteAst.AutoBatch (loc,params) ->
 386         let metasenv, params = disambiguate_auto_params metasenv params in
 387         metasenv,GrafiteAst.AutoBatch (loc,params)
 388     | GrafiteAst.Cases (loc, what, pattern, idents) ->
 389         let metasenv,what = disambiguate_term context metasenv what in
 390         let pattern = disambiguate_pattern pattern in
 391         metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
 392     | GrafiteAst.Change (loc, pattern, with_what) ->
 393         let with_what = disambiguate_lazy_term with_what in
 394         let pattern = disambiguate_pattern pattern in
 395         metasenv,GrafiteAst.Change (loc, pattern, with_what)
 396     | GrafiteAst.Clear (loc,id) ->
 397         metasenv,GrafiteAst.Clear (loc,id)
 398     | GrafiteAst.ClearBody (loc,id) ->
 399        metasenv,GrafiteAst.ClearBody (loc,id)
 400     | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
 401         let metasenv,t1 = disambiguate_term context metasenv t1 in
 402         let metasenv,t2 =
 403           match t2 with
 404           | None -> metasenv, None
 405           | Some t2 ->
 406               let m, t2 = disambiguate_term context metasenv t2 in
 407               m, Some t2
 408         in
 409         metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
 410     | GrafiteAst.Constructor (loc,n) ->
 411         metasenv,GrafiteAst.Constructor (loc,n)
 412     | GrafiteAst.Contradiction loc ->
 413         metasenv,GrafiteAst.Contradiction loc
 414     | GrafiteAst.Cut (loc, ident, term) ->
 415         let metasenv,cic = disambiguate_term context metasenv term in
 416         metasenv,GrafiteAst.Cut (loc, ident, cic)
 417     | GrafiteAst.Decompose (loc, names) ->
 418          metasenv,GrafiteAst.Decompose (loc, names)
 419     | GrafiteAst.Demodulate (loc, params) ->
 420         let metasenv, params = disambiguate_auto_params metasenv params in
 421         metasenv,GrafiteAst.Demodulate (loc, params)
 422     | GrafiteAst.Destruct (loc, Some terms) ->
 423         let map term (metasenv, terms) =
 424            let metasenv, term = disambiguate_term context metasenv term in
 425            metasenv, term :: terms
 426         in
 427         let metasenv, terms = List.fold_right map terms (metasenv, []) in
 428         metasenv, GrafiteAst.Destruct(loc, Some terms)
 429     | GrafiteAst.Destruct (loc, None) ->
 430         metasenv,GrafiteAst.Destruct(loc,None)
 431     | GrafiteAst.Exact (loc, term) ->
 432         let metasenv,cic = disambiguate_term context metasenv term in
 433         metasenv,GrafiteAst.Exact (loc, cic)
 434     | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
 435         let metasenv,what = disambiguate_term context metasenv what in
 436         let metasenv,using = disambiguate_term context metasenv using in
 437         let pattern = disambiguate_pattern pattern in
 438         metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
 439     | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
 440         let metasenv,what = disambiguate_term context metasenv what in
 441         let pattern = disambiguate_pattern pattern in
 442         metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
 443     | GrafiteAst.ElimType (loc, what, Some using, specs) ->
 444         let metasenv,what = disambiguate_term context metasenv what in
 445         let metasenv,using = disambiguate_term context metasenv using in
 446         metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
 447     | GrafiteAst.ElimType (loc, what, None, specs) ->
 448         let metasenv,what = disambiguate_term context metasenv what in
 449         metasenv,GrafiteAst.ElimType (loc, what, None, specs)
 450     | GrafiteAst.Exists loc ->
 451         metasenv,GrafiteAst.Exists loc
 452     | GrafiteAst.Fail loc ->
 453         metasenv,GrafiteAst.Fail loc
 454     | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
 455         let pattern = disambiguate_pattern pattern in
 456         let term = disambiguate_lazy_term term in
 457         let red_kind = disambiguate_reduction_kind red_kind in
 458         metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
 459     | GrafiteAst.FwdSimpl (loc, hyp, names) ->
 460        metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
 461     | GrafiteAst.Fourier loc ->
 462        metasenv,GrafiteAst.Fourier loc
 463     | GrafiteAst.Generalize (loc,pattern,ident) ->
 464         let pattern = disambiguate_pattern pattern in
 465         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
 466     | GrafiteAst.IdTac loc ->
 467         metasenv,GrafiteAst.IdTac loc
 468     | GrafiteAst.Intros (loc, specs) ->
 469         metasenv,GrafiteAst.Intros (loc, specs)
 470     | GrafiteAst.Inversion (loc, term) ->
 471        let metasenv,term = disambiguate_term context metasenv term in
 472         metasenv,GrafiteAst.Inversion (loc, term)
 473     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
 474        let f term (metasenv, to_what) =
 475           let metasenv, term = disambiguate_term context metasenv term in
 476           metasenv, term :: to_what
 477        in
 478        let metasenv, to_what = List.fold_right f to_what (metasenv, []) in
 479        let metasenv, what = disambiguate_term context metasenv what in
 480        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
 481     | GrafiteAst.Left loc ->
 482        metasenv,GrafiteAst.Left loc
 483     | GrafiteAst.LetIn (loc, term, name) ->
 484         let metasenv,term = disambiguate_term context metasenv term in
 485         metasenv,GrafiteAst.LetIn (loc,term,name)
 486     | GrafiteAst.Reduce (loc, red_kind, pattern) ->
 487         let pattern = disambiguate_pattern pattern in
 488         let red_kind = disambiguate_reduction_kind red_kind in
 489         metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
 490     | GrafiteAst.Reflexivity loc ->
 491         metasenv,GrafiteAst.Reflexivity loc
 492     | GrafiteAst.Replace (loc, pattern, with_what) ->
 493         let pattern = disambiguate_pattern pattern in
 494         let with_what = disambiguate_lazy_term with_what in
 495         metasenv,GrafiteAst.Replace (loc, pattern, with_what)
 496     | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
 497         let metasenv,term = disambiguate_term context metasenv t in
 498         let pattern = disambiguate_pattern pattern in
 499         metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
 500     | GrafiteAst.Right loc ->
 501         metasenv,GrafiteAst.Right loc
 502     | GrafiteAst.Ring loc ->
 503         metasenv,GrafiteAst.Ring loc
 504     | GrafiteAst.Split loc ->
 505         metasenv,GrafiteAst.Split loc
 506     | GrafiteAst.Symmetry loc ->
 507         metasenv,GrafiteAst.Symmetry loc
 508     | GrafiteAst.Transitivity (loc, term) ->
 509         let metasenv,cic = disambiguate_term context metasenv term in
 510         metasenv,GrafiteAst.Transitivity (loc, cic)
 511       (* Nuovi casi *)
 512     | GrafiteAst.Assume (loc, id, term) ->
 513         let metasenv,cic = disambiguate_term context metasenv term in
 514         metasenv,GrafiteAst.Assume (loc, id, cic)
 515     | GrafiteAst.Suppose (loc, term, id, term') ->
 516         let metasenv,cic = disambiguate_term context metasenv term in
 517         let metasenv,cic' =
 518            match term' with
 519               None -> metasenv,None
 520             | Some t ->
 521                   let metasenv,t = disambiguate_term context metasenv t in
 522                   metasenv,Some t in
 523         metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
 524     | GrafiteAst.Bydone (loc,just) ->
 525         let metasenv,just =
 526          disambiguate_just disambiguate_term context metasenv just
 527         in
 528          metasenv,GrafiteAst.Bydone (loc, just)
 529     | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
 530         let metasenv,cic = disambiguate_term context metasenv term in
 531         let metasenv,cic' =
 532             match term' with
 533               None -> metasenv,None
 534             | Some t ->
 535                   let metasenv,t = disambiguate_term context metasenv t in
 536                   metasenv,Some t in
 537         metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
 538     | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') ->
 539         let metasenv,just =
 540          disambiguate_just disambiguate_term context metasenv just in
 541         let metasenv,cic' = disambiguate_term context metasenv term' in
 542         let metasenv,cic'' =
 543             match term'' with
 544               None -> metasenv,None
 545            |  Some t ->
 546                     let metasenv,t = disambiguate_term context metasenv t in
 547                      metasenv,Some t in
 548         metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'')
 549     | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
 550         let metasenv,cic = disambiguate_term context metasenv term in
 551         let metasenv,cic' = disambiguate_term context metasenv term' in
 552         metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
 553     | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
 554         let metasenv,cic = disambiguate_term context metasenv term in
 555         let metasenv,cic' = disambiguate_term context metasenv term' in
 556         metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
 557    | GrafiteAst.Byinduction (loc, term, id) ->
 558         let metasenv,cic = disambiguate_term context metasenv term in
 559         metasenv,GrafiteAst.Byinduction(loc, cic, id)
 560    | GrafiteAst.Thesisbecomes (loc, term) ->
 561         let metasenv,cic = disambiguate_term context metasenv term in
 562         metasenv,GrafiteAst.Thesisbecomes (loc, cic)
 563    | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) ->
 564         let metasenv,just =
 565          disambiguate_just disambiguate_term context metasenv just in
 566         let metasenv,cic' = disambiguate_term context metasenv term1 in
 567         let cic''= disambiguate_lazy_term term2 in
 568         metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
 569    | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
 570         let metasenv,just =
 571          disambiguate_just disambiguate_term context metasenv just in
 572         let metasenv,cic'= disambiguate_term context metasenv term1 in
 573         let metasenv,cic''= disambiguate_term context metasenv term2 in
 574         metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'')
 575    | GrafiteAst.Case (loc, id, params) ->
 576         let metasenv,params' =
 577          List.fold_right
 578           (fun (id,term) (metasenv,params) ->
 579             let metasenv,cic = disambiguate_term context metasenv term in
 580              metasenv,(id,cic)::params
 581           ) params (metasenv,[])
 582         in
 583         metasenv,GrafiteAst.Case(loc, id, params')
 584    | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
 585         let metasenv,cic =
 586          match term1 with
 587             None -> metasenv,None
 588           | Some (start,t) ->
 589              let metasenv,t = disambiguate_term context metasenv t in
 590               metasenv,Some (start,t) in
 591         let metasenv,cic'= disambiguate_term context metasenv term2 in
 592         let metasenv,cic'' =
 593          match term3 with
 594           | `SolveWith term ->
 595              let metasenv,term = disambiguate_term context metasenv term in
 596              metasenv, `SolveWith term
 597           | `Auto params ->
 598               let metasenv, params = disambiguate_auto_params metasenv params in
 599               metasenv,`Auto params
 600           | `Term t ->
 601              let metasenv,t = disambiguate_term context metasenv t in
 602               metasenv,`Term t
 603           | `Proof as t -> metasenv,t in
 604         metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
 605
 606 let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
 607   let uri =
 608    let baseuri =
 609      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
 610    in
 611    let name =
 612      match obj with
 613      | CicNotationPt.Inductive (_,(name,_,_,_)::_)
 614      | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
 615      | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
 616      | CicNotationPt.Inductive _ -> assert false
 617    in
 618      UriManager.uri_of_string (baseuri ^ "/" ^ name)
 619   in
 620  let _try_new cic =
 621   (NCicLibrary.clear_cache ();
 622    NCicEnvironment.invalidate ();
 623    OCic2NCic.clear ();
 624    let graph =
 625      match cic with
 626      | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) ->
 627          let _, ugraph =
 628            CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
 629          in
 630            ugraph
 631      | Some (Cic.Constant (_,_, ty,_,_)) ->
 632          let _, ugraph =
 633                  CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
 634          in
 635            ugraph
 636      | _ -> CicUniv.empty_ugraph
 637    in
 638
 639 (*
 640    prerr_endline "PRIMA COERCIONS";
 641    let _,l = CicUniv.do_rank graph in
 642    List.iter (fun k ->
 643      prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
 644      (CicUniv.get_rank k))) l;
 645 *)
 646
 647    let graph =
 648        List.fold_left
 649          (fun graph (_,_,l) ->
 650            List.fold_left
 651              (fun graph (uri,_,_) ->
 652                 let _,g = CicTypeChecker.typecheck uri in
 653                 CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
 654              graph l)
 655        graph (CoercDb.to_list ())
 656    in
 657    ignore(CicUniv.do_rank graph);
 658
 659
 660 (*
 661    prerr_endline "DOPO COERCIONS";
 662    let _,l = CicUniv.do_rank graph in
 663    List.iter (fun k ->
 664      prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
 665      (CicUniv.get_rank k))) l;
 666 *)
 667
 668
 669    prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
 670    let time = Unix.gettimeofday () in
 671        (try
 672          (match
 673           NCicDisambiguate.disambiguate_obj
 674            ~lookup_in_library
 675            ~description_of_alias:LexiconAst.description_of_alias
 676            ~mk_choice:ncic_mk_choice
 677            ~mk_implicit
 678            ~uri:(OCic2NCic.nuri_of_ouri uri)
 679            ~coercion_db:(NCicCoercion.db ())
 680            ~aliases:lexicon_status.LexiconEngine.aliases
 681            ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 682            (text,prefix_len,obj)
 683          with
 684          | [_,_,_,obj],_ ->
 685           let time = Unix.gettimeofday () -. time in
 686 (*           NCicTypeChecker.typecheck_obj obj; *)
 687           prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
 688 (*
 689           let obj =
 690             let u,i,m,_,o = obj in
 691             u,i,m,[],o
 692           in
 693 *)
 694           prerr_endline (NCicPp.ppobj obj)
 695          | _ ->
 696           prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!!  "))
 697        with
 698        | MultiPassDisambiguator.DisambiguationError (_,s) ->
 699         prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
 700           ^UriManager.string_of_uri uri^
 701           "):\n" ^
 702          String.concat "\n"
 703           (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
 704 (*        | exn -> prerr_endline (Printexc.to_string exn) *)
 705        )
 706   )
 707  in
 708
 709
 710  try
 711 (*   let time = Unix.gettimeofday () in  *)
 712
 713
 714   let (diff, metasenv, _, cic, _) =
 715     singleton "third"
 716       (CicDisambiguate.disambiguate_obj
 717         ~lookup_in_library
 718         ~mk_choice:cic_mk_choice
 719         ~mk_implicit
 720         ~description_of_alias:LexiconAst.description_of_alias
 721         ~aliases:lexicon_status.LexiconEngine.aliases
 722         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
 723         ~uri:(Some uri)
 724         (text,prefix_len,obj)) in
 725
 726
 727 (*
 728   let time = Unix.gettimeofday () -. time in
 729   prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
 730     UriManager.string_of_uri uri ^"): " ^ string_of_float time);
 731 *)
 732 (*    try_new (Some cic);   *)
 733
 734
 735   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
 736   lexicon_status, metasenv, cic
 737
 738  with
 739  | Sys.Break as exn -> raise exn
 740  | exn ->
 741 (*    try_new None; *)
 742    raise exn
 743
 744 ;;
 745
 746 let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
 747   match cmd with
 748    | GrafiteAst.NObj(loc,obj) -> lexicon_status, metasenv, GrafiteAst.NObj(loc,obj)
 749    | GrafiteAst.Index(loc,key,uri) ->
 750        let lexicon_status_ref = ref lexicon_status in
 751        let disambiguate_term =
 752          disambiguate_term None text prefix_len lexicon_status_ref [] in
 753        let disambiguate_term_option metasenv =
 754          function
 755              None -> metasenv,None
 756            | Some t ->
 757                let metasenv,t = disambiguate_term metasenv t in
 758                  metasenv, Some t
 759        in
 760        let metasenv,key = disambiguate_term_option metasenv key in
 761        !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
 762    | GrafiteAst.Select (loc,uri) ->
 763         lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
 764    | GrafiteAst.Pump(loc,i) ->
 765         lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
 766    | GrafiteAst.PreferCoercion (loc,t) ->
 767        let lexicon_status_ref = ref lexicon_status in
 768        let disambiguate_term =
 769          disambiguate_term None text prefix_len lexicon_status_ref [] in
 770       let metasenv,t = disambiguate_term metasenv t in
 771       !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
 772    | GrafiteAst.Coercion (loc,t,b,a,s) ->
 773        let lexicon_status_ref = ref lexicon_status in
 774        let disambiguate_term =
 775          disambiguate_term None text prefix_len lexicon_status_ref [] in
 776       let metasenv,t = disambiguate_term metasenv t in
 777       !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
 778    | GrafiteAst.Inverter (loc,n,indty,params) ->
 779        let lexicon_status_ref = ref lexicon_status in
 780        let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in
 781       let metasenv,indty = disambiguate_term metasenv indty in
 782       !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
 783    | GrafiteAst.UnificationHint (loc, t, n) ->
 784        let lexicon_status_ref = ref lexicon_status in
 785        let disambiguate_term =
 786          disambiguate_term None text prefix_len lexicon_status_ref [] in
 787       let metasenv,t = disambiguate_term metasenv t in
 788       !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n)
 789    | GrafiteAst.Default _
 790    | GrafiteAst.Drop _
 791    | GrafiteAst.Include _
 792    | GrafiteAst.Print _
 793    | GrafiteAst.Qed _
 794    | GrafiteAst.NQed _
 795    | GrafiteAst.Set _ as cmd ->
 796        lexicon_status,metasenv,cmd
 797    | GrafiteAst.Obj (loc,obj) ->
 798        let lexicon_status,metasenv,obj =
 799         disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
 800        lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
 801    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
 802       let lexicon_status_ref = ref lexicon_status in
 803       let disambiguate_term =
 804        disambiguate_term None text prefix_len lexicon_status_ref [] in
 805       let disambiguate_term_option metasenv =
 806        function
 807           None -> metasenv,None
 808        | Some t ->
 809           let metasenv,t = disambiguate_term metasenv t in
 810            metasenv, Some t
 811       in
 812       let metasenv,a = disambiguate_term metasenv a in
 813       let metasenv,aeq = disambiguate_term metasenv aeq in
 814       let metasenv,refl = disambiguate_term_option metasenv refl in
 815       let metasenv,sym = disambiguate_term_option metasenv sym in
 816       let metasenv,trans = disambiguate_term_option metasenv trans in
 817        !lexicon_status_ref, metasenv,
 818         GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 819
 820 let disambiguate_macro
 821   lexicon_status_ref metasenv context (text,prefix_len, macro)
 822 =
 823  let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in
 824   let disambiguate_reduction_kind =
 825     disambiguate_reduction_kind text prefix_len lexicon_status_ref in
 826   match macro with
 827    | GrafiteAst.WMatch (loc,term) ->
 828       let metasenv,term = disambiguate_term context metasenv term in
 829        metasenv,GrafiteAst.WMatch (loc,term)
 830    | GrafiteAst.WInstance (loc,term) ->
 831       let metasenv,term = disambiguate_term context metasenv term in
 832        metasenv,GrafiteAst.WInstance (loc,term)
 833    | GrafiteAst.WElim (loc,term) ->
 834       let metasenv,term = disambiguate_term context metasenv term in
 835        metasenv,GrafiteAst.WElim (loc,term)
 836    | GrafiteAst.WHint (loc,term) ->
 837       let metasenv,term = disambiguate_term context metasenv term in
 838        metasenv,GrafiteAst.WHint (loc,term)
 839    | GrafiteAst.Check (loc,term) ->
 840       let metasenv,term = disambiguate_term context metasenv term in
 841        metasenv,GrafiteAst.Check (loc,term)
 842    | GrafiteAst.Eval (loc,kind,term) ->
 843       let metasenv, term = disambiguate_term context metasenv term in
 844       let kind = disambiguate_reduction_kind kind in
 845        metasenv,GrafiteAst.Eval (loc,kind,term)
 846    | GrafiteAst.AutoInteractive (loc, params) ->
 847       let metasenv, params =
 848         disambiguate_auto_params disambiguate_term metasenv context params in
 849       metasenv, GrafiteAst.AutoInteractive (loc, params)
 850    | GrafiteAst.Hint _
 851    | GrafiteAst.WLocate _
 852    | GrafiteAst.Inline _ as macro ->
 853       metasenv,macro