Trick: the refiner always subst-expands the outtype, so that the beta-redex

[helm.git] / helm / software / components / binaries / transcript / v8Lexer.mll

diff --git a/helm/software/components/binaries/transcript/v8Lexer.mll b/helm/software/components/binaries/transcript/v8Lexer.mll
index 5a90aabf75b91769e47c214b7864679f958b8028..0ef38a919b55604548d120eaf607004d2d961e52 100644 (file)
--- a/helm/software/components/binaries/transcript/v8Lexer.mll
+++ b/helm/software/components/binaries/transcript/v8Lexer.mll
@@ -1,7 +1,17 @@
 {
+   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    = '"'
@@ -19,7 +29,9 @@ rule token = parse
    | "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    }
@@ -27,11 +39,16 @@ rule token = parse
    | "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    }
@@ -41,16 +58,29 @@ rule token = parse
    | "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 "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    }
@@ -68,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      }