snapshot (ported to new "typed" ids_to_inner_sort table)

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index a3a06f922d68ac446982334a4e03e7de31c204cd..b979e84c99f255aa313a3382106455d79d7702ad 100644 (file)
--- 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 05a80d982fdfd95cb893535f5c9739a51f22d73b..26ece217d9240337876e525f27c339ac32798cc1 100644 (file)
--- 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