From b7779155a6bb8868e0d33e1211a92d5f39e0c3a8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 19 Mar 2011 00:00:31 +0000 Subject: [PATCH] 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? --- .../grafite_parser/grafiteParser.ml | 9 ++++--- .../grafite_parser/grafiteParser.mli | 1 + matita/matita/matitaEngine.ml | 24 +++++++++++++------ 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 492274f97..2e64c9143 100644 --- 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 aa0fb5bde..1d0064379 100644 --- 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 913ba87f6..f65c8432a 100644 --- 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); -- 2.39.2