- added dot notation for real numbers and basic operations on them

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualLexer.mll

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 01ddd0cf302acdede1f9b14f086864077677ce10..06bbab076ec8c3b501d30dfa3e49d196a29b6c82 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -90,6 +90,11 @@ rule token =
                    (indtyuri_of_uri ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
   | indconuri   { INDCONURI
                    (indconuri_of_uri("cic:" ^ (unquote (L.lexeme lexbuf)))) }
+  | num '.'     {
+                  let lexeme = L.lexeme lexbuf in
+                  RNUM (int_of_string
+                    (String.sub lexeme 0 (String.length lexeme - 1)))
+                }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }
   | '?' num     { let lexeme = L.lexeme lexbuf in
                    META
@@ -108,6 +113,7 @@ rule token =
   | "\\lambda"  { LAMBDA }
   | "\\pi"      { PROD }
   | "\\forall"  { PROD }
+  | "\\eqt"     { EQT }
   | ':'         { COLON }
   | '.'         { DOT }
   | "\\to"      { ARROW }
@@ -115,6 +121,10 @@ rule token =
   | dollar      { DOLLAR }
   | eof         { EOF }
   (* Arithmetical operators *)
+  | "+."        { RPLUS }
+  | "-."        { RMINUS }
+  | "*."        { RTIMES }
+  | "/."        { RDIV }
   | '+'         { PLUS }
   | '-'         { MINUS }
   | '*'         { TIMES }