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