Matitaweb: Fixes a bug in the extensible parser which caused Matita to crash

[helm.git] / matitaB / components / content_pres / cicNotationParser.ml

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 6736211d4e67fbf5b88990b1bf93535f74b2d5e9..fcd209307fd73e6c1202e3439a6791ef968d24c2 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -30,7 +30,9 @@ open Printf
 module Ast = NotationPt
 module Env = NotationEnv
 
-let prerr_endline _ = () 
+module StringSet = Set.Make(String)
+
+(* let prerr_endline _ = () *)
 
 exception Parse_error of string
 exception Level_not_found of int
@@ -45,7 +47,7 @@ type ('a,'b,'c,'d,'e) grammars = {
   term: 'b Grammar.Entry.e;
   ident: 'e Grammar.Entry.e;
   sym_attributes: (string option * string option) Grammar.Entry.e;
-  sym_table: (string * Stdpp.location Grammar.Entry.e) list;
+  sym_table: ([ `Sym of string | `Kwd of string ] * Stdpp.location Grammar.Entry.e) list;
   let_defs: 'c Grammar.Entry.e;
   let_codefs: 'c Grammar.Entry.e;
   protected_binder_vars: 'd Grammar.Entry.e;
@@ -90,39 +92,45 @@ let level_of precedence =
     raise (Level_not_found precedence);
   string_of_int precedence 
 
-let add_symbol_to_grammar_explicit level2_ast_grammar 
-    sym_attributes sym_table s =
+let add_item_to_grammar_explicit level2_ast_grammar 
+    sym_attributes sym_table item = 
+  let stok, nonterm = match item with
+  | `Sym sy -> Gramext.Stoken ("SYMBOL",sy), "sym" ^ sy
+  | `Kwd i -> Gramext.Stoken("",i), "kwd" ^ i
+  in
   try
-    let _ = List.assoc s sym_table
+    let _ = List.assoc item sym_table
     in sym_table
   with Not_found -> 
-    let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) in
+(*    let entry = Grammar.Entry.create level2_ast_grammar ("sym" ^ s) in *)
+    let entry = Grammar.Entry.create level2_ast_grammar nonterm in 
     Grammar.extend
     [ Grammar.Entry.obj entry,
       None,
       [ None,
         Some (*Gramext.NonA*) Gramext.NonA,
-        [ [Gramext.Stoken ("SYMBOL",s)], (* concrete l1 syntax *) 
-          (Gramext.action (fun _ loc -> None, loc))
-        ; [Gramext.Stoken ("ATAG","")
+        [ [stok], (* concrete l1 syntax *) 
+          (Gramext.action (fun _ loc -> (* None, *) loc))
+(*        ; [Gramext.Stoken ("ATAG","")
           ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
           ;Gramext.Stoken ("SYMBOL","\005")
-          ;Gramext.Stoken ("SYMBOL",s)
+          ;stok
           ;Gramext.Stoken ("ATAGEND","")],
-          (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
+          (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc)) *)
         ]]];
 (*  prerr_endline ("adding to grammar symbol " ^ s); *)
-  (s,entry)::sym_table
+  (item,entry)::sym_table
  
 
-let add_symbol_to_grammar status s =
+let add_item_to_grammar status item =
   let sym_attributes = status#notation_parser_db.grammars.sym_attributes in
   let sym_table = status#notation_parser_db.grammars.sym_table in
   let level2_ast_grammar =
     status#notation_parser_db.grammars.level2_ast_grammar
   in
   let sym_table = 
-    add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes sym_table s
+    add_item_to_grammar_explicit level2_ast_grammar sym_attributes sym_table
+      item
   in
   let grammars =
     { status#notation_parser_db.grammars with sym_table = sym_table }
@@ -134,21 +142,34 @@ let add_symbol_to_grammar status s =
 let gram_symbol status s =
   let sym_table = status#notation_parser_db.grammars.sym_table in
   let entry =
-    try List.assoc s sym_table
+    try List.assoc (`Sym s) sym_table
     with Not_found ->
      (let syms = List.map fst (status#notation_parser_db.grammars.sym_table) in
-      let syms = List.map (fun x -> "\"" ^ x ^ "\"") syms in
-      prerr_endline ("new symbol non-terminals: " ^ (String.concat ", " syms));
-      prerr_endline ("unable to find symbol \"" ^ s ^ "\""); assert false)
+      let syms = List.map (fun x -> match x with `Sym x | `Kwd x -> "\"" ^ x ^ "\"") syms in
+      prerr_endline ("new symbol/keyword non-terminals: " ^ (String.concat ", " syms));
+      prerr_endline ("unable to find symbol \"" ^ s ^ "\""); 
+      (* XXX: typing error
+       * Gramext.Stoken("SYMBOL", s) *)
+       assert false)
   in
   Gramext.Snterm (Grammar.Entry.obj entry)
 
-let gram_ident status =
- Gramext.Snterm (Grammar.Entry.obj
+let gram_ident status = 
+  Gramext.Snterm (Grammar.Entry.obj
   (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
   (*Gramext.Stoken ("IDENT", s)*)
 let gram_number s = Gramext.Stoken ("NUMBER", s)
-let gram_keyword s = Gramext.Stoken ("", s)
+let gram_keyword status s =
+  let sym_table = status#notation_parser_db.grammars.sym_table in
+    try Gramext.Snterm (Grammar.Entry.obj 
+          (List.assoc (`Kwd s) sym_table))
+    with Not_found ->
+     (let syms = List.map fst (status#notation_parser_db.grammars.sym_table) in
+      let syms = List.map (fun x -> match x with `Sym x | `Kwd x -> "\"" ^ x ^ "\"") syms in
+      (* prerr_endline ("new symbol/keyword non-terminals: " ^ (String.concat ", " syms));
+        prerr_endline ("unable to find keyword \"" ^ s ^ "\""); *)
+      Gramext.Stoken("", s))
+  
 let gram_term status = function
   | Ast.Self _ -> Gramext.Sself
   | Ast.Level precedence ->
@@ -161,7 +182,7 @@ let gram_term status = function
 let gram_of_literal status =
   function
   | `Symbol (s,_) -> gram_symbol status s
-  | `Keyword (s,_) -> gram_keyword s
+  | `Keyword (s,_) -> gram_keyword status s
   | `Number (s,_) -> gram_number s
 
 let make_action status action bindings =
@@ -170,7 +191,7 @@ let make_action status action bindings =
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> 
         Gramext.action 
-         (fun (_,(loc: Ast.location)) ->
+         (fun ((*_,*)(loc: Ast.location)) ->
            let uri,desc = 
              try
                CicNotationLexer.LocalizeEnv.find loc
@@ -229,8 +250,11 @@ let update_sym_grammar status pattern =
         assert false
   and aux_literal status =
     function
-    | `Symbol (s,_) -> add_symbol_to_grammar status s
-    | `Keyword _ -> status
+    | `Symbol (s,_) -> add_item_to_grammar status (`Sym s)
+    | `Keyword (s,_) ->  
+         if not (List.mem s CicNotationLexer.initial_keywords)
+            then add_item_to_grammar status (`Kwd s)
+            else status
     | `Number _ -> status
   and aux_layout status = function
     | Ast.Sub (p1, p2) -> aux (aux status p1) p2
@@ -279,7 +303,7 @@ let extract_term_production status pattern =
     | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
     | `Keyword (s,_) ->
         (* assumption: s will be registered as a keyword with the lexer *)
-        [NoBinding, gram_keyword s]
+        [NoBinding, gram_keyword status s]
     | `Number (s,_) -> [NoBinding, gram_number s]
   and aux_layout = function
     | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
@@ -916,6 +940,7 @@ END
   grammars
 ;;
 
+
 let initial_grammars loctable keywords =
   let lexers = CicNotationLexer.mk_lexers loctable keywords in
   let level1_pattern_grammar = 
@@ -938,8 +963,8 @@ let initial_grammars loctable keywords =
     Grammar.Entry.create level2_ast_grammar "atag_attributes" in
   let sym_table = 
     List.fold_left 
-      (add_symbol_to_grammar_explicit level2_ast_grammar sym_attributes) 
-      [] initial_symbols
+      (add_item_to_grammar_explicit level2_ast_grammar sym_attributes) 
+      [] (List.map (fun s -> `Sym s) initial_symbols)
   in
   let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
   let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in
@@ -1001,7 +1026,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         [ None,
           Some (*Gramext.NonA*) Gramext.NonA,
           [ p_atoms, (* concrete l1 syntax *) 
-            (make_action status
+            (make_action status 
               (fun (env: NotationEnv.t) (loc: Ast.location) ->
                 (action env loc))
               p_bindings) ]]];