X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualLexer.mll;h=613645bc489ed28b2fa9ff82b27af0ad76454f99;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=31878bfe6e83d68405f1759597f7d5ac5840d4d4;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index 31878bfe6..613645bc4 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
+++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
@@ -31,43 +31,53 @@
  let indtyuri_of_uri uri =
   let index_sharp =  String.index uri '#' in
   let index_num = index_sharp + 3 in
-   (UriManager.uri_of_string (String.sub uri 0 index_sharp),
-    int_of_string (String.sub uri index_num (String.length uri - index_num)) - 1
-   )
+   try
+    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+     int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1
+    )
+   with
+    Failure msg ->
+     raise (CicTextualParser0.LexerFailure "Not an inductive URI")
  ;;
 
  let indconuri_of_uri uri =
   let index_sharp =  String.index uri '#' in
   let index_div = String.rindex uri '/' in
   let index_con = index_div + 1 in
-   (UriManager.uri_of_string (String.sub uri 0 index_sharp),
-    int_of_string
-     (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
-    int_of_string
-     (String.sub uri index_con (String.length uri - index_con))
-   )
+   try
+    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+     int_of_string
+      (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
+     int_of_string
+      (String.sub uri index_con (String.length uri - index_con))
+    )
+   with
+    Failure msg ->
+     raise (CicTextualParser0.LexerFailure "Not a constructor URI")
  ;;
 }
 let num = ['1'-'9']['0'-'9']* | '0'
-let alfa = ['A'-'Z' 'a'-'z' '_']
+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 }
   | "Set"       { SET }
   | "Prop"      { PROP }
   | "Type"      { TYPE }
+  | "CProp"     { CPROP }
   | 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)) }