merged cic_notation with disambiguation: good luck!

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 15947f3f238b00d0f9ad875c221f04e3a2e0127a..91b40fbee1fc1faa92868d8d01a774db3591b66f 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -32,8 +32,10 @@ type pretty_printer_id = pattern_id
 let default_prec = 50
 let default_assoc = Gramext.NonA
 
+module Ast = CicNotationPt
+
 type term_info =
-  { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
+  { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, string) Hashtbl.t;
   }
 
@@ -62,15 +64,6 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
-module Ast = CicNotationPt
-module Parser = CicNotationParser
-
-let string_of_name = function
-  | Cic.Name s -> s
-  | Cic.Anonymous -> "_"
-
-let ident_of_name n = Ast.Ident (string_of_name n, None)
-
 let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
 let resolve_binder = function
@@ -92,7 +85,7 @@ let pp_ast0 t k =
   in
   let rec aux = function
     | Ast.Appl ts ->
-        Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
+        Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc),
           Ast.Layout
            (Ast.Box ((Ast.HOV, true, true),
                      (CicNotationUtil.dress
@@ -100,14 +93,14 @@ let pp_ast0 t k =
                         (List.map k ts)))))
     | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
     | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
-        Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+        Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             aux_ty ty;
            Ast.Layout Ast.Break;                        
             binder_symbol "\\to";
             k body])))
     | Ast.Binder (binder_kind, (id, ty), body) ->
-        Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+        Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             binder_symbol (resolve_binder binder_kind);
             k id;
@@ -164,13 +157,15 @@ let ast_of_acic0 term_info acic k =
           | `Set | `Type -> `Pi
           | `Prop | `CProp -> `Forall
         in
-        idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t))
-    | Cic.ACast (id,v,t) ->
-        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t])
+        idref id (Ast.Binder (binder_kind,
+          (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
+    | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t))
     | Cic.ALambda (id,n,s,t) ->
-        idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t))
+        idref id (Ast.Binder (`Lambda,
+          (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
     | Cic.ALetIn (id,n,s,t) ->
-        idref id (Ast.LetIn ((ident_of_name n, None), k s, k t))
+        idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+          k s, k t))
     | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
     | Cic.AConst (id,uri,substs) ->
         register_uri id (UriManager.string_of_uri uri);
@@ -196,7 +191,7 @@ let ast_of_acic0 term_info acic k =
           match (ty, pat) with
           | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
               let (cv, rhs) = eat_branch t t' in
-              (ident_of_name name, Some (k s)) :: cv, rhs
+              (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
           | _, _ -> [], k pat
         in
         let patterns =
@@ -243,6 +238,7 @@ let ast_of_acic0 term_info acic k =
 
 let level1_patterns21 = Hashtbl.create 211
 let level2_patterns32 = Hashtbl.create 211
+let interpretations = Hashtbl.create 211  (* symb -> id list ref *)
 
 let compiled21 = ref None
 let compiled32 = ref None
@@ -296,7 +292,7 @@ let instantiate21 env (* precedence associativity *) l1 =
         let sep =
           match sep_opt with
             | None -> []
-            | Some l -> [ CicNotationPt.Literal l ]
+            | Some l -> [ Ast.Literal l ]
        in
         let rec instantiate_list acc = function
           | [] -> List.rev acc
@@ -367,7 +363,7 @@ let rec pp_ast1 term =
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
-    | GrafiteAst.IdentArg (n, name) ->
+    | Ast.IdentArg (n, name) ->
         let t = (try List.assoc name env with Not_found -> assert false) in
         let rec count_lambda = function
           | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
@@ -393,7 +389,7 @@ let rec ast_of_acic1 term_info annterm =
       let env' =
         List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
       in
-      let symbol, args, uris =
+      let _, symbol, args, _, uris =
         try
           Hashtbl.find level2_patterns32 pid
         with Not_found -> assert false
@@ -422,14 +418,34 @@ let fresh_id =
     incr counter;
     !counter
 
-let add_interpretation (symbol, args) appl_pattern =
+let add_interpretation dsc (symbol, args) appl_pattern =
   let id = fresh_id () in
   let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in
-  Hashtbl.add level2_patterns32 id (symbol, args, uris);
+  Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris);
   pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
   load_patterns32 !pattern32_matrix;
+  (try
+    let ids = Hashtbl.find interpretations symbol in
+    ids := id :: !ids
+  with Not_found -> Hashtbl.add interpretations symbol (ref [id]));
   id
 
+exception Interpretation_not_found
+exception Pretty_printer_not_found
+
+let lookup_interpretations symbol =
+  try
+    List.map
+      (fun id ->
+        let (dsc, _, args, appl_pattern, _) =
+          try
+            Hashtbl.find level2_patterns32 id
+          with Not_found -> assert false 
+        in
+        dsc, args, appl_pattern)
+      !(Hashtbl.find interpretations symbol)
+  with Not_found -> raise Interpretation_not_found
+
 let add_pretty_printer
   ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
 =
@@ -440,11 +456,11 @@ let add_pretty_printer
   load_patterns21 !pattern21_matrix;
   id
 
-exception Interpretation_not_found
-exception Pretty_printer_not_found
-
 let remove_interpretation id =
   (try
+    let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in
+    let ids = Hashtbl.find interpretations symbol in
+    ids := List.filter ((<>) id) !ids;
     Hashtbl.remove level2_patterns32 id;
   with Not_found -> raise Interpretation_not_found);
   pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;