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