diff options
author | Gregory Malecha <gmalecha@cs.harvard.edu> | 2014-08-01 21:22:11 -0400 |
---|---|---|
committer | Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 14:13:24 +0200 |
commit | b45474e03dbba3687db4c7452432e686c32f60a4 (patch) | |
tree | 75f4977dff2a6cb580ab4dc55655a9d6390230bf /tools | |
parent | d8f73aee76e8b63db97f41e978b579477a82ed50 (diff) |
Support for Timeout n and From ..
- The state machine gets kind of complex
maybe it should become a parser at some point?
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdep_common.ml | 2 | ||||
-rw-r--r-- | tools/coqdep_lexer.mll | 46 |
2 files changed, 43 insertions, 5 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c965fb098..d7532dba6 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -128,7 +128,7 @@ let error_cannot_parse s (i,j) = let warning_module_notfound f s = eprintf "*** Warning: in file %s, library " f; - eprintf "%s.v is required and has not been found in loadpath!\n" + eprintf "%s.v is required and has not been found in the loadpath!\n" (String.concat "." s); flush stderr diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 7d2978b25..4cb5e0087 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -49,6 +49,8 @@ let syntax_error lexbuf = raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) + + let from_pre_ident = ref None } let space = [' ' '\t' '\n' '\r'] @@ -81,17 +83,21 @@ rule coq_action = parse | "Require" space+ { require_file lexbuf } | "Require" space+ "Export" space+ - { require_file lexbuf} + { require_file lexbuf } | "Require" space+ "Import" space+ - { require_file lexbuf} + { require_file lexbuf } | "Local"? "Declare" space+ "ML" space+ "Module" space+ - { mllist := []; modules lexbuf} + { mllist := []; modules lexbuf } | "Load" space+ { load_file lexbuf } | "Add" space+ "LoadPath" space+ { add_loadpath lexbuf } | "Time" space+ { coq_action lexbuf } + | "Timeout" space+ ['0'-'9']+ space+ + { coq_action lexbuf } + | "From" space+ + { from_rule lexbuf } | space+ { coq_action lexbuf } | "(*" @@ -101,6 +107,33 @@ rule coq_action = parse | _ { skip_to_dot lexbuf; coq_action lexbuf } +and from_rule = parse + | "(*" + { comment_depth := 1; comment lexbuf; require_file lexbuf } + | space+ + { from_rule lexbuf } + | coq_ident + { module_current_name := [Lexing.lexeme lexbuf]; + from_pre_ident := Some (coq_qual_id_tail lexbuf); + module_names := []; + consume_require lexbuf } + | eof + { syntax_error lexbuf } + | _ + { syntax_error lexbuf } + +and consume_require = parse + | "(*" + { comment_depth := 1; comment lexbuf; consume_require lexbuf } + | space+ + { consume_require lexbuf } + | "Require" space+ + { require_file lexbuf } + | eof + { syntax_error lexbuf } + | _ + { syntax_error lexbuf } + and add_loadpath = parse | "(*" { comment_depth := 1; comment lexbuf; add_loadpath lexbuf } @@ -228,7 +261,12 @@ and require_file = parse module_names := [coq_qual_id_tail lexbuf]; let qid = coq_qual_id_list lexbuf in parse_dot lexbuf; - Require qid } + match !from_pre_ident with + None -> + Require qid + | Some from -> + (from_pre_ident := None ; + Require (List.map (fun x -> from @ x) qid)) } | '"' [^'"']* '"' (*'"'*) { let s = Lexing.lexeme lexbuf in parse_dot lexbuf; |