X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Lexer.mll;fp=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Lexer.mll;h=0000000000000000000000000000000000000000;hb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;hp=0ef38a919b55604548d120eaf607004d2d961e52;hpb=281f0c7b4fc0d5b97025625af2ecff85edebbb5c;p=helm.git diff --git a/helm/software/components/binaries/transcript/v8Lexer.mll b/helm/software/components/binaries/transcript/v8Lexer.mll deleted file mode 100644 index 0ef38a919..000000000 --- a/helm/software/components/binaries/transcript/v8Lexer.mll +++ /dev/null @@ -1,104 +0,0 @@ -{ - module O = Options - module P = V8Parser - - 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' '\r']+ -let ALPHA = ['A'-'Z' 'a'-'z' '_'] -let FIG = ['0'-'9'] -let ID = ALPHA (ALPHA | FIG | "\'")* -let RAWID = QT [^ '"']* QT -let NUM = "-"? FIG+ - -rule token = parse - | "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 "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 "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 "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 "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 } - | "(*" { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s } - | "*)" { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s } - | "(" { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s } - | ")" { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s } - | "{" { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s } - | "}" { 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 "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 }