helm/software/components/cic_disambiguation/cicDisambiguate.mli

   1 (*
   2  *
   3 Copyright (C) 1999-2006, HELM Team.
   4
   5 This file is part of HELM, an Hypertextual, Electronic
   6 Library of Mathematics, developed at the Computer Science
   7 Department, University of Bologna, Italy.
   8
   9 HELM is free software; you can redistribute it and/or
  10 modify it under the terms of the GNU General Public License
  11 as published by the Free Software Foundation; either version 2
  12 of the License, or (at your option) any later version.
  13
  14 HELM is distributed in the hope that it will be useful,
  15 but WITHOUT ANY WARRANTY; without even the implied warranty of
  16 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  17 GNU General Public License for more details.
  18
  19 You should have received a copy of the GNU General Public License
  20 along with this program; if not, write to the Free Software
  21 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
  22 02110-1301 USA.
  23
  24 For details, see the HELM web site: http://helm.cs.unibo.it/
  25 *)
  26
  27 val interpretate_path :
  28   context:Cic.name list -> CicNotationPt.term -> Cic.term
  29
  30 val disambiguate_term :
  31   context:Cic.context ->
  32   metasenv:Cic.metasenv ->
  33   subst:Cic.substitution ->
  34   ?goal:int ->
  35   ?initial_ugraph:CicUniv.universe_graph ->
  36   aliases:Cic.term DisambiguateTypes.environment ->
  37   universe:Cic.term DisambiguateTypes.multiple_environment option ->
  38   lookup_in_library:(
  39     DisambiguateTypes.interactive_user_uri_choice_type ->
  40     DisambiguateTypes.input_or_locate_uri_type ->
  41     DisambiguateTypes.Environment.key ->
  42     Cic.term DisambiguateTypes.codomain_item list) ->
  43   CicNotationPt.term Disambiguate.disambiguator_input ->
  44   ((DisambiguateTypes.domain_item *
  45     Cic.term DisambiguateTypes.codomain_item) list *
  46    Cic.metasenv *
  47    Cic.substitution *
  48    Cic.term*
  49    CicUniv.universe_graph) list *
  50   bool
  51
  52 val disambiguate_obj :
  53   aliases:Cic.term DisambiguateTypes.environment ->
  54   universe:Cic.term DisambiguateTypes.multiple_environment option ->
  55   uri:UriManager.uri option ->     (* required only for inductive types *)
  56   lookup_in_library:(
  57     DisambiguateTypes.interactive_user_uri_choice_type ->
  58     DisambiguateTypes.input_or_locate_uri_type ->
  59     DisambiguateTypes.Environment.key ->
  60     Cic.term DisambiguateTypes.codomain_item list) ->
  61   CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
  62   ((DisambiguateTypes.domain_item *
  63     Cic.term DisambiguateTypes.codomain_item) list *
  64    Cic.metasenv *
  65    Cic.substitution *
  66    Cic.obj *
  67    CicUniv.universe_graph) list *
  68   bool