helm/ocaml/cic_textual_parser/cicTextualLexer.mll

   1 {
   2  open CicTextualParser;;
   3  module L = Lexing;;
   4  module U = UriManager;;
   5
   6  let indtyuri_of_uri uri =
   7   let index_sharp =  String.index uri '#' in
   8   let index_num = index_sharp + 3 in
   9    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
  10     int_of_string (String.sub uri index_num (String.length uri - index_num)) - 1
  11    )
  12  ;;
  13
  14  let indconuri_of_uri uri =
  15   let index_sharp =  String.index uri '#' in
  16   let index_div = String.rindex uri '/' in
  17   let index_con = index_div + 1 in
  18    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
  19     int_of_string
  20      (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
  21     int_of_string
  22      (String.sub uri index_con (String.length uri - index_con))
  23    )
  24  ;;
  25 }
  26 let num = ['1'-'9']['0'-'9']* | '0'
  27 let ident = ['A'-'Z' 'a'-'z' '_' '-']*
  28 let baseuri = '/'(ident '/')* ident '.'
  29 let conuri = baseuri ("con" | "var")
  30 let indtyuri = baseuri "ind#1/" num
  31 let indconuri = baseuri "ind#1/" num "/" num
  32 let blanks = [' ' '\t' '\n']
  33 rule token =
  34  parse
  35     blanks      { token lexbuf } (* skip blanks *)
  36   | "alias"     { ALIAS }
  37   | "Case"      { CASE }
  38   | "Fix"       { FIX }
  39   | "CoFix"     { COFIX }
  40   | "Set"       { SET }
  41   | "Prop"      { PROP }
  42   | "Type"      { TYPE }
  43   | ident       { ID (L.lexeme lexbuf) }
  44   | conuri      { CONURI (U.uri_of_string ("cic:" ^ L.lexeme lexbuf)) }
  45   | indtyuri    { INDTYURI (indtyuri_of_uri ("cic:" ^ L.lexeme lexbuf)) }
  46   | indconuri   { INDCONURI (indconuri_of_uri("cic:" ^ L.lexeme lexbuf)) }
  47   | num         { NUM (int_of_string (L.lexeme lexbuf)) }
  48   | '?' num     { META (int_of_string (L.lexeme lexbuf)) }
  49   | ":>"        { CAST }
  50   | ":="        { LETIN }
  51   | '?'         { IMPLICIT }
  52   | '('         { LPAREN }
  53   | ')'         { RPAREN }
  54   | '{'         { LCURLY }
  55   | '}'         { RCURLY }
  56   | ';'         { SEMICOLON }
  57   | '\\'        { LAMBDA }
  58   | '!'         { PROD }
  59   | ':'         { COLON }
  60   | '.'         { DOT }
  61   | eof         { EOF }
  62 {}