aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tools/coqdep_common.ml19
-rw-r--r--tools/coqdep_lexer.mli6
-rw-r--r--tools/coqdep_lexer.mll218
3 files changed, 172 insertions, 71 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 5f530c0670..45949b9246 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -115,6 +115,10 @@ let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
let clash_v = ref ([]: (string list * string list) list)
+let error_cannot_parse s (i,j) =
+ Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
+ exit 1
+
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"
@@ -123,12 +127,12 @@ let warning_module_notfound f s =
let warning_notfound f s =
eprintf "*** Warning: in file %s, the file " f;
- eprintf "%s.v is required and has not been found !\n" s;
+ eprintf "%s.v is required and has not been found!\n" s;
flush stderr
let warning_declare f s =
eprintf "*** Warning: in file %s, declared ML module " f;
- eprintf "%s has not been found !\n" s;
+ eprintf "%s has not been found!\n" s;
flush stderr
let warning_clash file dir =
@@ -245,11 +249,7 @@ let traite_fichier_modules md ext =
| None -> a_faire) "" list
with
| Sys_error _ -> ""
- | Syntax_error (i,j) ->
- Printf.eprintf "File \"%s%s\", characters %i-%i:\nError: Syntax error\n"
- md ext i j;
- exit 1
-
+ | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
(* Makefile's escaping rules are awful: $ is escaped by doubling and
other special characters are escaped by backslash prefixing while
@@ -350,9 +350,10 @@ let traite_fichier_Coq verbose f =
printf " %s.v" (canonize file_str)
with Not_found -> ()
end
+ | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
done
- with Fin_fichier -> ();
- close_in chan
+ with Fin_fichier -> close_in chan
+ | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j)
with Sys_error _ -> ()
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index 2605862707..6b6e0da973 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -8,11 +8,15 @@
type mL_token = Use_module of string
+type qualid = string list
+
type coq_token =
- Require of string list list
+ Require of qualid list
| RequireString of string
| Declare of string list
| Load of string
+ | AddLoadPath of string
+ | AddRecLoadPath of string * qualid
exception Fin_fichier
exception Syntax_error of int * int
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index e0bf1daec7..159c6d3c6a 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -13,11 +13,15 @@
type mL_token = Use_module of string
+ type qualid = string list
+
type coq_token =
- | Require of string list list
+ | Require of qualid list
| RequireString of string
- | Declare of string list
+ | Declare of string list (* Names are assumed to be uncapitalized *)
| Load of string
+ | AddLoadPath of string
+ | AddRecLoadPath of string * qualid
let comment_depth = ref 0
@@ -27,11 +31,24 @@
let module_current_name = ref []
let module_names = ref []
let ml_module_name = ref ""
+ let loadpath = ref ""
let mllist = ref ([] : string list)
let field_name s = String.sub s 1 (String.length s - 1)
+ let unquote_string s =
+ String.sub s 1 (String.length s - 2)
+
+ let unquote_vfile_string s =
+ let f = unquote_string s in
+ if check_suffix f ".v" then chop_suffix f ".v" else f
+
+ let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
+ lexbuf.lex_curr_p <- lexbuf.lex_start_p
+
+ let syntax_error lexbuf =
+ raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
}
let space = [' ' '\t' '\n' '\r']
@@ -39,31 +56,71 @@ let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
let identchar =
['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
-let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+
-let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+
let caml_up_ident = uppercase identchar*
let caml_low_ident = lowercase identchar*
+
+let coq_firstchar =
+ (* This is only an approximation, refer to lib/util.ml for correct def *)
+ ['A'-'Z' 'a'-'z' '_'] |
+ (* superscript 1 *)
+ '\194' '\185' |
+ (* utf-8 latin 1 supplement *)
+ '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] |
+ (* utf-8 letters *)
+ '\206' (['\145'-'\161'] | ['\163'-'\187'])
+ '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+ | '\129' [ '\176'-'\187' ] (* superscripts *)
+ | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let coq_identchar = coq_firstchar | ['\'' '0'-'9']
+let coq_ident = coq_firstchar coq_identchar*
+let coq_field = '.' coq_ident
+
let dot = '.' ( space+ | eof)
rule coq_action = parse
| "Require" space+
- { module_names := []; opened_file lexbuf }
+ { require_file lexbuf }
| "Require" space+ "Export" space+
- { module_names := []; opened_file lexbuf}
+ { require_file lexbuf}
| "Require" space+ "Import" space+
- { module_names := []; opened_file lexbuf}
+ { require_file lexbuf}
| "Local"? "Declare" space+ "ML" space+ "Module" space+
{ mllist := []; modules lexbuf}
| "Load" space+
{ load_file lexbuf }
- | "\""
- { string lexbuf; coq_action lexbuf}
- | "(*" (* "*)" *)
+ | "Add" space+ "LoadPath" space+
+ { add_loadpath lexbuf }
+ | space+
+ { coq_action lexbuf }
+ | "(*"
{ comment_depth := 1; comment lexbuf; coq_action lexbuf }
| eof
{ raise Fin_fichier}
| _
- { coq_action lexbuf }
+ { skip_to_dot lexbuf; coq_action lexbuf }
+
+and add_loadpath = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; add_loadpath lexbuf }
+ | space+
+ { add_loadpath lexbuf }
+ | eof
+ { syntax_error lexbuf }
+ | '"' [^ '"']* '"' (*'"'*)
+ { loadpath := unquote_string (lexeme lexbuf);
+ add_loadpath_as lexbuf }
+
+and add_loadpath_as = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; add_loadpath_as lexbuf }
+ | space+
+ { add_loadpath_as lexbuf }
+ | "as"
+ { let qid = coq_qual_id lexbuf in
+ skip_to_dot lexbuf;
+ AddRecLoadPath (!loadpath,qid) }
+ | dot
+ { AddLoadPath !loadpath }
and caml_action = parse
| space +
@@ -130,7 +187,8 @@ and comment = parse
{ comment lexbuf }
| eof
{ raise Fin_fichier }
- | _ { comment lexbuf }
+ | _
+ { comment lexbuf }
and string = parse
| '"' (* '"' *)
@@ -149,69 +207,108 @@ and string = parse
and load_file = parse
| '"' [^ '"']* '"' (*'"'*)
{ let s = lexeme lexbuf in
- let f = String.sub s 1 (String.length s - 2) in
- skip_to_dot lexbuf;
- Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
+ parse_dot lexbuf;
+ Load (unquote_vfile_string s) }
| coq_ident
{ let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
| eof
- { raise Fin_fichier }
+ { syntax_error lexbuf }
| _
- { load_file lexbuf }
+ { syntax_error lexbuf }
+
+and require_file = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; require_file lexbuf }
+ | space+
+ { require_file lexbuf }
+ | coq_ident
+ { module_current_name := [Lexing.lexeme lexbuf];
+ module_names := [coq_qual_id_tail lexbuf];
+ let qid = coq_qual_id_list lexbuf in
+ parse_dot lexbuf;
+ Require qid }
+ | '"' [^'"']* '"' (*'"'*)
+ { let s = Lexing.lexeme lexbuf in
+ parse_dot lexbuf;
+ RequireString (unquote_vfile_string s) }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { syntax_error lexbuf }
and skip_to_dot = parse
| dot { () }
- | eof { () }
+ | eof { syntax_error lexbuf }
| _ { skip_to_dot lexbuf }
-and opened_file = parse
- | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf }
+and parse_dot = parse
+ | dot { () }
+ | eof { syntax_error lexbuf }
+ | _ { syntax_error lexbuf }
+
+and coq_qual_id = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; coq_qual_id lexbuf }
| space+
- { opened_file lexbuf }
+ { coq_qual_id lexbuf }
| coq_ident
- { module_current_name := [Lexing.lexeme lexbuf];
- opened_file_fields lexbuf }
-
- | '"' [^'"']* '"' { (*'"'*)
- let lex = Lexing.lexeme lexbuf in
- let str = String.sub lex 1 (String.length lex - 2) in
- let str =
- if Filename.check_suffix str ".v" then
- Filename.chop_suffix str ".v"
- else str in
- RequireString str }
- | eof { raise Fin_fichier }
- | _ { opened_file lexbuf }
-
-and opened_file_fields = parse
- | "(*" (* "*)" *)
- { comment_depth := 1; comment lexbuf;
- opened_file_fields lexbuf }
+ { module_current_name := [Lexing.lexeme lexbuf];
+ coq_qual_id_tail lexbuf }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { backtrack lexbuf;
+ let qid = List.rev !module_current_name in
+ module_current_name := [];
+ qid }
+
+and coq_qual_id_tail = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; coq_qual_id_tail lexbuf }
| space+
- { opened_file_fields lexbuf }
+ { coq_qual_id_tail lexbuf }
| coq_field
- { module_current_name :=
- field_name (Lexing.lexeme lexbuf) :: !module_current_name;
- opened_file_fields lexbuf }
- | coq_ident { module_names :=
- List.rev !module_current_name :: !module_names;
- module_current_name := [Lexing.lexeme lexbuf];
- opened_file_fields lexbuf }
- | dot { module_names :=
- List.rev !module_current_name :: !module_names;
- Require (List.rev !module_names) }
- | eof { raise Fin_fichier }
- | _ { opened_file_fields lexbuf }
+ { module_current_name :=
+ field_name (Lexing.lexeme lexbuf) :: !module_current_name;
+ coq_qual_id_tail lexbuf }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { backtrack lexbuf;
+ let qid = List.rev !module_current_name in
+ module_current_name := [];
+ qid }
+
+and coq_qual_id_list = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; coq_qual_id_list lexbuf }
+ | space+
+ { coq_qual_id_list lexbuf }
+ | coq_ident
+ { module_current_name := [Lexing.lexeme lexbuf];
+ module_names := coq_qual_id_tail lexbuf :: !module_names;
+ coq_qual_id_list lexbuf
+ }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { backtrack lexbuf;
+ List.rev !module_names }
and modules = parse
- | space+ { modules lexbuf }
- | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf;
- modules lexbuf }
+ | space+
+ { modules lexbuf }
+ | "(*"
+ { comment_depth := 1; comment lexbuf;
+ modules lexbuf }
| '"' [^'"']* '"'
- { let lex = (Lexing.lexeme lexbuf) in
- let str = String.sub lex 1 (String.length lex - 2) in
- mllist := str :: !mllist; modules lexbuf}
- | _ { (Declare (List.rev !mllist)) }
+ { let lex = (Lexing.lexeme lexbuf) in
+ let str = String.sub lex 1 (String.length lex - 2) in
+ mllist := str :: !mllist; modules lexbuf}
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { (Declare (List.rev !mllist)) }
and qual_id = parse
| '.' [^ '.' '(' '['] {
@@ -225,8 +322,7 @@ and mllib_list = parse
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
| eof { [] }
- | _ { raise (Syntax_error (Lexing.lexeme_start lexbuf,
- Lexing.lexeme_end lexbuf)) }
+ | _ { syntax_error lexbuf }
and ocamldep_parse = parse
| [^ ':' ]* ':' { mllib_list lexbuf }
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 10:55:31 +0000