]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_textual_parser/cicTextualLexer.mll
lazily ==> call_by_name (since it is really a call_by_name!)
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualLexer.mll
index 1be084795a11505eb80764da93da88e1ad79d5b6..58e6cf35b12d877e6fe61a2e251d6b3a5d34e7ca 100644 (file)
@@ -52,14 +52,14 @@ let num = ['1'-'9']['0'-'9']* | '0'
 let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-']
 let ident = alfa (alfa | num)*
 let baseuri = '/'(ident '/')* ident '.'
-let conuri = baseuri ("con" | "var")
+let conuri = baseuri "con"
+let varuri = baseuri "var"
 let indtyuri = baseuri "ind#1/" num
 let indconuri = baseuri "ind#1/" num "/" num
 let blanks = [' ' '\t' '\n']
 rule token =
  parse
     blanks      { token lexbuf } (* skip blanks *)
-  | "alias"     { ALIAS }
   | "Case"      { CASE }
   | "Fix"       { FIX }
   | "CoFix"     { COFIX }
@@ -68,6 +68,7 @@ rule token =
   | "Type"      { TYPE }
   | ident       { ID (L.lexeme lexbuf) }
   | conuri      { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
+  | varuri      { VARURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
   | indtyuri    { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) }
   | indconuri   { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }