cic_disambiguation splitted into disambiguation and cic_disambiguation

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.mli

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
deleted file mode 100644 (file)
index 92e1187..0000000
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ /dev/null
@@ -1,117 +0,0 @@
-(* 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 * string) list *
-  (Stdpp.location * string) Lazy.t *
-  bool) list
-exception PathNotWellFormed
-
-type 'a disambiguator_input = string * int * 'a
-    
-type domain = domain_tree list
-and domain_tree = 
-  Node of Stdpp.location list * DisambiguateTypes.domain_item * domain
-
-type ('term,'metasenv,'subst,'graph) test_result =
-  | Ok of 'term * 'metasenv * 'subst * 'graph
-  | Ko of (Stdpp.location * string) Lazy.t
-  | Uncertain of (Stdpp.location * string) Lazy.t
-
-exception Try_again of string Lazy.t
-
-val resolve : 
-  'term DisambiguateTypes.environment ->
-  DisambiguateTypes.Environment.key ->
-    ?num:string -> ?args:'term list -> unit -> 'term
-
-val find_in_context: string -> Cic.name list -> int
-
-val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
-val domain_of_term: context:
-  (Cic.name * 'a) option list -> CicNotationPt.term -> domain
-val domain_of_obj: 
-  context:(Cic.name * 'a) option list -> 
-    CicNotationPt.term CicNotationPt.obj -> domain
-
-module type Disambiguator =
-sig
-  val disambiguate_thing:
-    context:'context ->
-    metasenv:'metasenv ->
-    subst:'subst ->
-    mk_implicit:(bool -> 'refined_term) ->
-    initial_ugraph:'ugraph ->
-    hint: 
-      ('metasenv -> 'raw_thing -> 'raw_thing) * 
-      (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
-         ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
-    aliases:'refined_term DisambiguateTypes.codomain_item 
-      DisambiguateTypes.Environment.t ->
-    universe:'refined_term DisambiguateTypes.codomain_item list
-      DisambiguateTypes.Environment.t option ->
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      'refined_term DisambiguateTypes.codomain_item list) ->
-    uri:'uri ->
-    pp_thing:('ast_thing -> string) ->
-    domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
-    interpretate_thing:(
-      context:'context ->
-      env:'refined_term DisambiguateTypes.codomain_item
-             DisambiguateTypes.Environment.t ->
-      uri:'uri ->
-      is_path:bool -> 
-      'ast_thing -> 
-      localization_tbl:'cichash -> 
-        'raw_thing) ->
-    refine_thing:(
-      'metasenv -> 'subst -> 'context -> 'uri ->
-      'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
-        ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
-    localization_tbl:'cichash ->
-    string * int * 'ast_thing ->
-    ((DisambiguateTypes.Environment.key * 
-      'refined_term DisambiguateTypes.codomain_item) list * 
-     'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
-end
-
-module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
-