X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Lexer.mll;h=0ef38a919b55604548d120eaf607004d2d961e52;hb=281f0c7b4fc0d5b97025625af2ecff85edebbb5c;hp=cddb728bd49b7044cf8b27dcfa4c4794077deed4;hpb=c5e25191f05bb2662fc738bfb2742eb03b941510;p=helm.git diff --git a/helm/software/components/binaries/transcript/v8Lexer.mll b/helm/software/components/binaries/transcript/v8Lexer.mll index cddb728bd..0ef38a919 100644 --- a/helm/software/components/binaries/transcript/v8Lexer.mll +++ b/helm/software/components/binaries/transcript/v8Lexer.mll @@ -1,11 +1,21 @@ { + module O = Options module P = V8Parser - let out t s = () (* prerr_endline (t ^ " " ^ s) *) + let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) + + let check s = + let c = Char.code s.[0] in + if c <= 127 then s else + let escaped = Printf.sprintf "\\%3u\\" c in + begin + if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped; + escaped + end } let QT = '"' -let SPC = [' ' '\t' '\n']+ +let SPC = [' ' '\t' '\n' '\r']+ let ALPHA = ['A'-'Z' 'a'-'z' '_'] let FIG = ['0'-'9'] let ID = ALPHA (ALPHA | FIG | "\'")* @@ -13,49 +23,70 @@ let RAWID = QT [^ '"']* QT let NUM = "-"? FIG+ rule token = parse - | "Let" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } | "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Fixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "CoFixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } | "Qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } + | "Save" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } | "Defined" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } | "Proof" { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s } | "Variable" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } | "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } | "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } | "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Axiom" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } + | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } + | "Parameter" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } + | "Parameters" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } | "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } + | "CoInductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } | "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } + | "Scheme" { let s = Lexing.lexeme lexbuf in out "GEN" s; P.GEN s } | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "End" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Hint" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Unset" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Print" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Opaque" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Transparent" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Ltac" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Tactic" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "Declare" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s } + | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Hints" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } | "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s } | "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } - | "Import" { let s = Lexing.lexeme lexbuf in out "IP" s; P.IP s } + | "Import" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } | "Load" { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s } | "Set" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Reset" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } | "Implicit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Delimit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Bind" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Arguments" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Open" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "V7only" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } | "Notation" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Reserved" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } | "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Grammar" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Syntax" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Add" SPC "Morphism" + { let s = Lexing.lexeme lexbuf in out "MOR" s; P.MOR s } + | "Add" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } | "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } | "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s } - | "let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } + | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s } | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s } + | "with" { let s = Lexing.lexeme lexbuf in out "WITH" s; P.WITH s } | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s } | ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s } | RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s } | NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s } | ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s } + | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s } | "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s } | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } | "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } @@ -67,5 +98,7 @@ rule token = parse | "}" { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s } | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s } | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s } - | _ { let s = Lexing.lexeme lexbuf in out "SPEC" s; P.EXTRA s } + | "," { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s } + | _ + { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s } | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF }