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   mk_implicit:(bool -> 'alias) ->
  37   description_of_alias:('alias -> string) ->
  38   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
  39   aliases:'alias DisambiguateTypes.Environment.t ->
  40   universe:'alias list DisambiguateTypes.Environment.t option ->
  41   lookup_in_library:(
  42     DisambiguateTypes.interactive_user_uri_choice_type ->
  43     DisambiguateTypes.input_or_locate_uri_type ->
  44     DisambiguateTypes.Environment.key ->
  45     'alias list) ->
  46   CicNotationPt.term Disambiguate.disambiguator_input ->
  47   ((DisambiguateTypes.domain_item * 'alias) list *
  48    Cic.metasenv *
  49    Cic.substitution *
  50    Cic.term*
  51    CicUniv.universe_graph) list *
  52   bool
  53
  54 val disambiguate_obj :
  55   mk_implicit:(bool -> 'alias) ->
  56   description_of_alias:('alias -> string) ->
  57   mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
  58   aliases:'alias DisambiguateTypes.Environment.t ->
  59   universe:'alias list DisambiguateTypes.Environment.t option ->
  60   lookup_in_library:(
  61     DisambiguateTypes.interactive_user_uri_choice_type ->
  62     DisambiguateTypes.input_or_locate_uri_type ->
  63     DisambiguateTypes.Environment.key ->
  64     'alias list) ->
  65   uri:UriManager.uri option ->     (* required only for inductive types *)
  66   CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
  67   ((DisambiguateTypes.domain_item * 'alias) list *
  68    Cic.metasenv *
  69    Cic.substitution *
  70    Cic.obj *
  71    CicUniv.universe_graph) list *
  72   bool