(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) open GrafiteTypes let singleton = function | [x], _ -> x | _ -> assert false (** @param term not meaningful when context is given *) let disambiguate_term ?context status_ref goal term = let status = !status_ref in let context = match context with | Some c -> c | None -> GrafiteTypes.get_proof_context status goal in let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~context ~metasenv:(GrafiteTypes.get_proof_metasenv status) term) in let status = GrafiteTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status diff in status_ref := status; cic (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term * rationale: lazy_term will be invoked in different context to obtain a term, * each invocation will disambiguate the term and can add aliases. Once all * disambiguations have been performed, the first returned function can be * used to obtain the resulting aliases *) let disambiguate_lazy_term status_ref term = (fun context metasenv ugraph -> let status = !status_ref in let (diff, metasenv, cic, ugraph) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ()) ~initial_ugraph:ugraph ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~context ~metasenv term) in let status = GrafiteTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status diff in status_ref := status; cic, metasenv, ugraph) let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = let interp path = Disambiguate.interpretate_path [] path in let goal_path = HExtlib.map_option interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in let wanted = match wanted with None -> None | Some wanted -> let wanted = disambiguate_lazy_term status_ref wanted in Some wanted in (wanted, hyp_paths, goal_path) let disambiguate_reduction_kind aliases_ref = function | `Unfold (Some t) -> let t = disambiguate_lazy_term aliases_ref t in `Unfold (Some t) | `Normalize | `Reduce | `Simpl | `Unfold None | `Whd as kind -> kind let disambiguate_tactic status goal tactic = let status_ref = ref status in let tactic = match tactic with | GrafiteAst.Absurd (loc, term) -> let cic = disambiguate_term status_ref goal term in GrafiteAst.Absurd (loc, cic) | GrafiteAst.Apply (loc, term) -> let cic = disambiguate_term status_ref goal term in GrafiteAst.Apply (loc, cic) | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> GrafiteAst.Auto (loc,depth,width,paramodulation,full) | GrafiteAst.Change (loc, pattern, with_what) -> let with_what = disambiguate_lazy_term status_ref with_what in let pattern = disambiguate_pattern status_ref pattern in GrafiteAst.Change (loc, pattern, with_what) | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id) | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id) | GrafiteAst.Compare (loc,term) -> let term = disambiguate_term status_ref goal term in GrafiteAst.Compare (loc,term) | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n) | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc | GrafiteAst.Cut (loc, ident, term) -> let cic = disambiguate_term status_ref goal term in GrafiteAst.Cut (loc, ident, cic) | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc | GrafiteAst.Decompose (loc, types, what, names) -> let disambiguate types = function | GrafiteAst.Type _ -> assert false | GrafiteAst.Ident id -> (match disambiguate_term status_ref goal (CicNotationPt.Ident (id, None)) with | Cic.MutInd (uri, tyno, _) -> (GrafiteAst.Type (uri, tyno) :: types) | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]]))) in let types = List.fold_left disambiguate [] types in GrafiteAst.Decompose (loc, types, what, names) | GrafiteAst.Discriminate (loc,term) -> let term = disambiguate_term status_ref goal term in GrafiteAst.Discriminate(loc,term) | GrafiteAst.Exact (loc, term) -> let cic = disambiguate_term status_ref goal term in GrafiteAst.Exact (loc, cic) | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> let what = disambiguate_term status_ref goal what in let using = disambiguate_term status_ref goal using in GrafiteAst.Elim (loc, what, Some using, depth, idents) | GrafiteAst.Elim (loc, what, None, depth, idents) -> let what = disambiguate_term status_ref goal what in GrafiteAst.Elim (loc, what, None, depth, idents) | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> let what = disambiguate_term status_ref goal what in let using = disambiguate_term status_ref goal using in GrafiteAst.ElimType (loc, what, Some using, depth, idents) | GrafiteAst.ElimType (loc, what, None, depth, idents) -> let what = disambiguate_term status_ref goal what in GrafiteAst.ElimType (loc, what, None, depth, idents) | GrafiteAst.Exists loc -> GrafiteAst.Exists loc | GrafiteAst.Fail loc -> GrafiteAst.Fail loc | GrafiteAst.Fold (loc,red_kind, term, pattern) -> let pattern = disambiguate_pattern status_ref pattern in let term = disambiguate_lazy_term status_ref term in let red_kind = disambiguate_reduction_kind status_ref red_kind in GrafiteAst.Fold (loc, red_kind, term, pattern) | GrafiteAst.FwdSimpl (loc, hyp, names) -> GrafiteAst.FwdSimpl (loc, hyp, names) | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc | GrafiteAst.Generalize (loc,pattern,ident) -> let pattern = disambiguate_pattern status_ref pattern in GrafiteAst.Generalize (loc,pattern,ident) | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g) | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc | GrafiteAst.Injection (loc, term) -> let term = disambiguate_term status_ref goal term in GrafiteAst.Injection (loc,term) | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names) | GrafiteAst.Inversion (loc, term) -> let term = disambiguate_term status_ref goal term in GrafiteAst.Inversion (loc, term) | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> let f term to_what = let term = disambiguate_term status_ref goal term in term :: to_what in let to_what = List.fold_right f to_what [] in let what = disambiguate_term status_ref goal what in GrafiteAst.LApply (loc, depth, to_what, what, ident) | GrafiteAst.Left loc -> GrafiteAst.Left loc | GrafiteAst.LetIn (loc, term, name) -> let term = disambiguate_term status_ref goal term in GrafiteAst.LetIn (loc,term,name) | GrafiteAst.Reduce (loc, red_kind, pattern) -> let pattern = disambiguate_pattern status_ref pattern in let red_kind = disambiguate_reduction_kind status_ref red_kind in GrafiteAst.Reduce(loc, red_kind, pattern) | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc | GrafiteAst.Replace (loc, pattern, with_what) -> let pattern = disambiguate_pattern status_ref pattern in let with_what = disambiguate_lazy_term status_ref with_what in GrafiteAst.Replace (loc, pattern, with_what) | GrafiteAst.Rewrite (loc, dir, t, pattern) -> let term = disambiguate_term status_ref goal t in let pattern = disambiguate_pattern status_ref pattern in GrafiteAst.Rewrite (loc, dir, term, pattern) | GrafiteAst.Right loc -> GrafiteAst.Right loc | GrafiteAst.Ring loc -> GrafiteAst.Ring loc | GrafiteAst.Split loc -> GrafiteAst.Split loc | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc | GrafiteAst.Transitivity (loc, term) -> let cic = disambiguate_term status_ref goal term in GrafiteAst.Transitivity (loc, cic) in status_ref, tactic let disambiguate_obj status obj = let uri = match obj with | CicNotationPt.Inductive (_,(name,_,_,_)::_) | CicNotationPt.Record (_,name,_,_) -> Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind")) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ()) ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) in let proof_status = match status.proof_status with | No_proof -> Intermediate metasenv | Incomplete_proof _ | Proof _ -> raise (GrafiteTypes.Command_error "imbricated proofs not allowed") | Intermediate _ -> assert false in let status = { status with proof_status = proof_status } in let status = MatitaSync.set_proof_aliases status diff in status, cic let disambiguate_command status = function | GrafiteAst.Alias _ | GrafiteAst.Coercion _ | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Dump _ | GrafiteAst.Include _ | GrafiteAst.Interpretation _ | GrafiteAst.Notation _ | GrafiteAst.Qed _ | GrafiteAst.Render _ | GrafiteAst.Set _ as cmd -> status,cmd | GrafiteAst.Obj (loc,obj) -> let status,obj = disambiguate_obj status obj in status, GrafiteAst.Obj (loc,obj)