diff options
Diffstat (limited to 'tools/coqdep_lexer.mll')
| -rwxr-xr-x | tools/coqdep_lexer.mll | 91 |
1 files changed, 44 insertions, 47 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index cc9f2175..89eeed54 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -6,75 +6,77 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqdep_lexer.mll 10721 2008-03-26 14:40:30Z notin $ i*) - +(*i $Id$ i*) + { - open Filename + open Filename open Lexing - + type mL_token = Use_module of string type spec = bool - - type coq_token = - | Require of spec * string list list - | RequireString of spec * string + + type coq_token = + | Require of string list list + | RequireString of string | Declare of string list | Load of string let comment_depth = ref 0 - + exception Fin_fichier - + let module_current_name = ref [] let module_names = ref [] let ml_module_name = ref "" - - let specif = ref false - + let mllist = ref ([] : string list) let field_name s = String.sub s 1 (String.length s - 1) + } let space = [' ' '\t' '\n' '\r'] let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = +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 dot = '.' ( space+ | eof) rule coq_action = parse | "Require" space+ - { specif := false; module_names := []; opened_file lexbuf } + { module_names := []; opened_file lexbuf } | "Require" space+ "Export" space+ - { specif := false; module_names := []; opened_file lexbuf} + { module_names := []; opened_file lexbuf} | "Require" space+ "Import" space+ - { specif := false; module_names := []; opened_file lexbuf} - | "Declare" space+ "ML" space+ "Module" space+ + { module_names := []; opened_file lexbuf} + | "Local"? "Declare" space+ "ML" space+ "Module" space+ { mllist := []; modules lexbuf} | "Load" space+ { load_file lexbuf } | "\"" { string lexbuf; coq_action lexbuf} | "(*" (* "*)" *) - { comment_depth := 1; comment lexbuf; coq_action lexbuf } - | eof - { raise Fin_fichier} - | _ + { comment_depth := 1; comment lexbuf; coq_action lexbuf } + | eof + { raise Fin_fichier} + | _ { coq_action lexbuf } and caml_action = parse - | [' ' '\010' '\013' '\009' '\012'] + - { caml_action lexbuf } - | "open" [' ' '\010' '\013' '\009' '\012']* - { caml_opened_file lexbuf } - | lowercase identchar* + | space + { caml_action lexbuf } - | uppercase identchar* + | "open" space* (caml_up_ident as id) + { Use_module (String.uncapitalize id) } + | "module" space+ caml_up_ident + { caml_action lexbuf } + | caml_low_ident { caml_action lexbuf } + | caml_up_ident { ml_module_name := Lexing.lexeme lexbuf; qual_id lexbuf } | ['0'-'9']+ @@ -130,7 +132,7 @@ and comment = parse | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" { comment lexbuf } | eof - { raise Fin_fichier } + { raise Fin_fichier } | _ { comment lexbuf } and string = parse @@ -155,7 +157,7 @@ and load_file = parse Load (if check_suffix f ".v" then chop_suffix f ".v" else f) } | coq_ident { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s } - | eof + | eof { raise Fin_fichier } | _ { load_file lexbuf } @@ -169,10 +171,6 @@ and opened_file = parse | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf } | space+ { opened_file lexbuf } - | "Implementation" - { opened_file lexbuf } - | "Specification" - { specif := true; opened_file lexbuf } | coq_ident { module_current_name := [Lexing.lexeme lexbuf]; opened_file_fields lexbuf } @@ -184,7 +182,7 @@ and opened_file = parse if Filename.check_suffix str ".v" then Filename.chop_suffix str ".v" else str in - RequireString (!specif, str) } + RequireString str } | eof { raise Fin_fichier } | _ { opened_file lexbuf } @@ -198,13 +196,13 @@ and opened_file_fields = parse { module_current_name := field_name (Lexing.lexeme lexbuf) :: !module_current_name; opened_file_fields lexbuf } - | coq_ident { module_names := + | 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 (!specif, List.rev !module_names) } + Require (List.rev !module_names) } | eof { raise Fin_fichier } | _ { opened_file_fields lexbuf } @@ -213,23 +211,22 @@ and modules = parse | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; modules lexbuf } | '"' [^'"']* '"' - { let lex = (Lexing.lexeme lexbuf) in + { 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)) } + | _ { (Declare (List.rev !mllist)) } and qual_id = parse - | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) } + | '.' [^ '.' '(' '['] { + Use_module (String.uncapitalize !ml_module_name) } | eof { raise Fin_fichier } | _ { caml_action lexbuf } -and caml_opened_file = parse - | uppercase identchar* - { let lex = (Lexing.lexeme lexbuf) in - let str = String.sub lex 0 (String.length lex) in - (Use_module (String.uncapitalize str)) } - | eof {raise Fin_fichier } - | _ { caml_action lexbuf } +and mllib_list = parse + | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf) + in s :: mllib_list lexbuf } + | space+ { mllib_list lexbuf } + | eof { [] } |