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?
raise (HExtlib.Localized
(floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
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
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
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)
let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
type parsable
val parsable_statement: #status -> Ulexing.lexbuf -> parsable
val parse_statement: #status -> parsable -> GrafiteAst.statement
type parsable
val parsable_statement: #status -> Ulexing.lexbuf -> parsable
val parse_statement: #status -> parsable -> GrafiteAst.statement
+val strm_of_parsable: parsable -> Ulexing.lexbuf
and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
let matita_debug = Helm_registry.get_bool "matita.debug" in
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
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 =
| Some (asserted,ast) ->
cb status ast;
let new_statuses =
[s,None] -> s
| _::(_,Some (_,value))::_ ->
raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
[s,None] -> s
| _::(_,Some (_,value))::_ ->
raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
+ | _ -> 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
- asserted, false, status
+ asserted, false, status, str
with exn when not matita_debug ->
raise (EnrichedWithStatus (exn, status))
in
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
+ loop asserted status str
and compile ~compiling ~asserted ~include_paths fname =
if List.mem fname compiling then raise (CircularDependency fname);
and compile ~compiling ~asserted ~include_paths fname =
if List.mem fname compiling then raise (CircularDependency fname);