(* Copyright (C) 2004, 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/ *) (** {2 Disambiguation interface} *) (* the integer is an offset to be added to each location *) (* list of located error messages, each list is a tuple: * - environment in string form * - environment patch * - location * - error message * - significancy of the error message, if false the error is likely to be * useless for the final user ... *) exception NoWellTypedInterpretation of int * ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Stdpp.location option * string Lazy.t * bool) list exception PathNotWellFormed val interpretate_path : context:Cic.name list -> CicNotationPt.term -> Cic.term type 'a disambiguator_input = string * int * 'a module type Disambiguator = sig (** @param fresh_instances when set to true fresh instances will be generated * for each number _and_ symbol in the disambiguation domain. Instances of the * input AST will be ignored. Defaults to false. *) val disambiguate_term : ?fresh_instances:bool -> dbd:HSql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.term * CicUniv.universe_graph) list * (* disambiguated term *) bool (* has interactive_interpretation_choice been invoked? *) (** @param fresh_instances as per disambiguate_term *) val disambiguate_obj : ?fresh_instances:bool -> dbd:HSql.dbd -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) CicNotationPt.term CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * CicUniv.universe_graph) list * (* disambiguated obj *) bool (* has interactive_interpretation_choice been invoked? *) end module Make (C : DisambiguateTypes.Callbacks) : Disambiguator