- factorized DisambiguateChoices module

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e64087cf6f3ad61ab81f478be9be57b7658f92dd..786971fc11cddcecab7d6e11a6785923753135f2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -28,7 +28,6 @@ open Printf
 open DisambiguateTypes
 open UriManager
 
-exception Invalid_choice
 exception No_choices of domain_item
 exception NoWellTypedInterpretation
 
@@ -43,18 +42,6 @@ let descr_of_domain_item = function
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 
-let symbol_choices = Hashtbl.create 1023
-let num_choices = ref []
-
-let add_symbol_choice symbol codomain_item =
-  let current_choices =
-    try
-      Hashtbl.find symbol_choices symbol
-    with Not_found -> []
-  in
-  Hashtbl.replace symbol_choices symbol (codomain_item :: current_choices)
-let add_num_choice choice = num_choices := choice :: !num_choices
-
 type test_result =
   | Ok of Cic.term * Cic.metasenv
   | Ko
@@ -128,7 +115,7 @@ let interpretate ~context ~env ast =
           match resolve env (Id indty_ident) () with
           | Cic.MutInd (uri, tyno, _) -> uri, tyno
           | Cic.Implicit -> raise Try_again
-          | _ -> raise Invalid_choice
+          | _ -> raise DisambiguateChoices.Invalid_choice
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
@@ -338,9 +325,8 @@ module Make (C: Callbacks) =
                 let choices = choices_of_id mqi_handle id in
                 Hashtbl.add id_choices id choices;
                 choices)
-          | Symbol (symb, _) ->
-              (try Hashtbl.find symbol_choices symb with Not_found -> [])
-          | Num instance -> !num_choices
+          | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
+          | Num instance -> DisambiguateChoices.lookup_num_choices ()
         in
         if choices = [] then raise (No_choices item);
         choices
@@ -361,7 +347,7 @@ module Make (C: Callbacks) =
           refine metasenv context cic_term
         with
         | Try_again -> Uncertain
-        | Invalid_choice -> Ko
+        | DisambiguateChoices.Invalid_choice -> Ko
       in
       (* (4) build all possible interpretations *)
       let rec aux current_env todo_dom =