{ (* $Id: *) open Lexing type mL_token = Use_module of string type spec = bool type coq_token = | Require of spec * string | RequireString of spec * string | Declare of string list let mlAccu = ref ([] : (string * string * string option) list) and mliAccu = ref ([] : (string * string * string option) list) and vAccu = ref ([] : (string * string option) list) let mlKnown = ref ([] : (string * string option) list) and mliKnown = ref ([] : (string * string option) list) and vKnown = ref ([] : (string * string option) list) and coqlibKnown = ref ([] : (string * string option) list) let coqlib = ref Coq_config.coqlib let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151 let addQueue q v = q := v :: !q let file_name = function | (s,None) -> s | (s,Some ".") -> s | (s,Some d) -> Filename.concat d s let comment_depth = ref 0 exception Fin_fichier let module_name = ref "" let specif = ref false let mllist = ref ([] : string list) } let space = [' ' '\t' '\n'] 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']+ rule coq_action = parse | "Require" space+ { specif := false; opened_file lexbuf } | "Require" space+ "Export" space+ { specif := false; opened_file lexbuf} | "Require" space+ "Syntax" space+ { specif := false; opened_file lexbuf} | "Require" space+ "Import" space+ { specif := false; opened_file lexbuf} | "Declare" space+ "ML" space+ "Module" space+ { mllist := []; modules lexbuf} | "\"" { string lexbuf; coq_action lexbuf} | "(*" { 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* { caml_action lexbuf } | uppercase identchar* { module_name := Lexing.lexeme lexbuf; qual_id lexbuf } | ['0'-'9']+ | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ | '0' ['o' 'O'] ['0'-'7']+ | '0' ['b' 'B'] ['0'-'1']+ { caml_action lexbuf } | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)? { caml_action lexbuf } | "\"" { string lexbuf; caml_action lexbuf } | "'" [^ '\\' '\''] "'" { caml_action lexbuf } | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" { caml_action lexbuf } | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" { caml_action lexbuf } | "(*" { comment_depth := 1; comment lexbuf; caml_action lexbuf } | "#" | "&" | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".." | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|" | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-" | "-." { caml_action lexbuf } | ['!' '?' '~'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * { caml_action lexbuf } | ['=' '<' '>' '@' '^' '|' '&' '$'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * { caml_action lexbuf } | ['+' '-'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * { caml_action lexbuf } | "**" ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * { caml_action lexbuf } | ['*' '/' '%'] ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] * { caml_action lexbuf } | eof { raise Fin_fichier } | _ { caml_action lexbuf } and comment = parse | "(*" { comment_depth := succ !comment_depth; comment lexbuf } | "*)" { comment_depth := pred !comment_depth; if !comment_depth > 0 then comment lexbuf } | "'" [^ '\\' '\''] "'" { comment lexbuf } | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" { comment lexbuf } | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" { comment lexbuf } | eof { raise Fin_fichier } | _ { comment lexbuf } and string = parse | '"' { () } | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] * { string lexbuf } | '\\' ['\\' '"' 'n' 't' 'b' 'r'] { string lexbuf } | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] { string lexbuf } | eof { raise Fin_fichier } | _ { string lexbuf } 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_name := (Lexing.lexeme lexbuf); opened_file_end lexbuf } and opened_file_end = parse | '.' { Require (!specif, !module_name) } | space+ { opened_file_end lexbuf } | "(*" { comment_depth := 1; comment lexbuf; opened_file_end lexbuf } | '"' [^'"']* '"' { let lex = Lexing.lexeme lexbuf in let str = String.sub lex 1 (String.length lex - 2) in RequireString (!specif, str) } | eof { raise Fin_fichier } | _ { opened_file_end lexbuf } and modules = parse | 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)) } and qual_id = parse | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !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 }