From a907911788bf1229fbf04e3125e0c1755f90d96a Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 31 May 2005 22:39:27 +0000
Subject: [PATCH] snapshot (ported to new "typed" ids_to_inner_sort table)

---
 helm/ocaml/cic_notation/cicNotationRew.ml |  5 ++++-
 helm/ocaml/cic_notation/test_parser.ml    | 18 ------------------
 2 files changed, 4 insertions(+), 19 deletions(-)

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index a3a06f922..b979e84c9 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -375,7 +375,10 @@ let compiler32 (t: Patterns.t) success_k fail_k =
       k
     else if Patterns.are_empty t then begin
       (match t with
-      | _::_::_ -> warning "Ambiguous patterns"
+      | _::_::_ ->
+          (* optimization possible here: throw away all except one of the rules
+           * which lead to ambiguity *)
+          warning "Ambiguous patterns"
       | _ -> ());
       return_closure success_k
     end else
diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index 05a80d982..26ece217d 100644
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -29,23 +29,6 @@ let _ =
   Helm_registry.set "getter.mode" "remote";
   Helm_registry.set "getter.url" "http://helm.cs.unibo.it:58081/"
 
-  (* ORRIBLE HACK! conversion:
-   * (Cic.id, string) Hashtbl.t -> (Cic.id, CicNotationtPt.sort_kind) Hashtbl.t
-   *)
-let patch_sort_tbl tbl =
-  let sort_of_string = function
-    | "Prop" -> `Prop
-    | "Set" -> `Set
-    | "Type" | "?" -> `Type
-    | "CProp" -> `CProp
-    | _ -> assert false
-  in
-  let tbl' = Hashtbl.create (Hashtbl.length tbl) in
-  Hashtbl.iter
-    (fun id sort_str -> Hashtbl.add tbl' id (sort_of_string sort_str))
-    tbl;
-  tbl'
-
 let _ =
   let module P = CicNotationPt in
   let level = ref ~-1 in
@@ -125,7 +108,6 @@ let _ =
                   | Cic.AVariable (_, _, _, ty, _, _) -> ty
                   | _ -> assert false
                 in
-                let id_to_sort = patch_sort_tbl id_to_sort in
                 let time1 = Unix.gettimeofday () in
                 let t, id_to_uri =
                   CicNotationRew.ast_of_acic id_to_sort annterm
-- 
2.39.2