Bug "fixed" (i.e avoided).

Bug description:
 - matitac (more precisely, MatitaEngine.assert_ng, hence the "include"
   command) parses files differently from Matita. In particular, it works on
   a camlp5 "Grammar.parsable" lexer, which is a lexer that remembers
   look-ahead tokens.
 - an "include" file can change the list of keywords for the lexer
   (e.g. when defining the "if-then-else" notation). Hence, after an include,
   the lexer to be used must change and thus the corresponding
   "Grammar.parsable" should change too. This was not the case since the
   "Grammar.parsable" was not regenerated to avoid loosing the look-ahead
   tokens

Bug avoidance:
 - we assume that the "include" command is properly terminated. Hence no
   look-ahead is performed. After each "include" command we regenerate
   the lexer to avoid the bug.

Note:
 - why don't we need to do this just after a "notation" command?
   Apparently, this is not required. However, I do not understand why.
   Is this to be better understood in the future?

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 492274f97ec50ff49196c271d24efdd949976bfd..2e64c9143b092aef1c4826f47e6badfcee23090c 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -42,15 +42,18 @@ let exc_located_wrapper f =
       raise (HExtlib.Localized 
         (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 
-type parsable = Grammar.parsable
+type parsable = Grammar.parsable * Ulexing.lexbuf
 
 let parsable_statement status buf =
  let grammar = CicNotationParser.level2_ast_grammar status in
-  Grammar.parsable grammar (Obj.magic buf)
+List.iter (fun (x,_) -> prerr_endline ("TOK: " ^ x)) (Grammar.tokens grammar "");
+  Grammar.parsable grammar (Obj.magic buf), buf
 
 let parse_statement grafite_parser parsable =
   exc_located_wrapper
-    (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) parsable))
+    (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) (fst parsable)))
+
+let strm_of_parsable (_,buf) = buf
 
 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 

diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli
index aa0fb5bdee9764f6edc70990f57a15d9c0304d64..1d006437928afb15223effad0862e6c0f3eb5055 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.mli
+++ b/matita/components/grafite_parser/grafiteParser.mli
@@ -50,3 +50,4 @@ val extend : #status as 'status ->
 type parsable
 val parsable_statement: #status -> Ulexing.lexbuf -> parsable
 val parse_statement: #status -> parsable -> GrafiteAst.statement
+val strm_of_parsable: parsable -> Ulexing.lexbuf

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 913ba87f6a835e8269bdd3973297ed7b81ddff03..f65c8432a4000f3dc9f28031eb0d5a03bc2c4174 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -174,14 +174,14 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm =
 
 and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status =
-  let asserted,stop,status = 
+ let rec loop asserted status str =
+  let asserted,stop,status,str = 
    try
      let cont =
        try Some (get_ast status ~compiling ~asserted ~include_paths str)
        with End_of_file -> None in
      match cont with
-     | None -> asserted, true, status
+     | None -> asserted, true, status, str
      | Some (asserted,ast) ->
         cb status ast;
         let new_statuses =
@@ -191,15 +191,25 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
             [s,None] -> s
           | _::(_,Some (_,value))::_ ->
                 raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
-          | _ -> assert false
+          | _ -> assert false in
+        (* CSC: complex patch to re-build the lexer since the tokens may
+           have changed. Note: this way we loose look-ahead tokens.
+           Hence the "include" command must be terminated (no look-ahead) *)
+        let str =
+         match ast with
+            (GrafiteAst.Executable
+              (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,_)))) ->
+              GrafiteParser.parsable_statement status
+               (GrafiteParser.strm_of_parsable str)
+          | _ -> str
         in
-         asserted, false, status
+         asserted, false, status, str
    with exn when not matita_debug ->
      raise (EnrichedWithStatus (exn, status))
   in
-  if stop then asserted,status else loop asserted status
+  if stop then asserted,status else loop asserted status str
  in
-  loop asserted status
+  loop asserted status str
 
 and compile ~compiling ~asserted ~include_paths fname =
   if List.mem fname compiling then raise (CircularDependency fname);