snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationLexer.ml

diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml
index 3c262ceec1854c27a502b9c56f1d8853a04bd430..26dc5aacae4b9e8f83ec1f9863d1b700e13fdd6f 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationLexer.ml
+++ b/helm/ocaml/cic_notation/cicNotationLexer.ml
@@ -39,12 +39,45 @@ let regexp delim_begin = "\\["
 let regexp delim_end = "\\]"
 
 let regexp keyword = '"' ident '"'
+let regexp qkeyword = "'" ident "'"
 
 let regexp implicit = '?'
 let regexp meta = implicit number
 
 let regexp csymbol = '\'' ident
 
+let regexp begin_group = "@{" | "${"
+let regexp end_group = '}'
+let regexp wildcard = "$_"
+let regexp ast_ident = "@" ident
+let regexp ast_csymbol = "@" csymbol
+let regexp meta_ident = "$" ident
+let regexp meta_anonymous = "$_"
+let regexp qstring = '"' [^ '"']* '"'
+
+let level1_layouts = 
+  [ "sub"; "sup";
+    "below"; "above";
+    "over"; "atop"; "frac";
+    "sqrt"; "root"
+  ]
+
+let level2_meta_keywords =
+  [ "if"; "then"; "else";
+    "fold"; "left"; "right"; "rec";
+    "fail";
+    "default";
+    "anonymous"; "ident"; "number"; "term"; "fresh"
+  ]
+
+let level1_keywords =
+  [ "hbox"; "hvbox"; "hovbox"; "vbox";
+    "break";
+    "list0"; "list1"; "sep";
+    "opt";
+    "term"; "ident"; "number"
+  ]
+
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
   ident ('/' ident)*                  (* path *)
@@ -58,8 +91,7 @@ let error_at_end lexbuf msg =
   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
   raise (Error (begin_cnum, end_cnum, msg))
 
-let return lexbuf token =
-  let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+let return_with_loc token begin_cnum end_cnum =
   (* TODO handle line/column numbers *)
   let flocation_begin =
     { Lexing.pos_fname = "";
@@ -69,6 +101,10 @@ let return lexbuf token =
   let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in
   (token, (flocation_begin, flocation_end))
 
+let return lexbuf token =
+  let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+    return_with_loc token begin_cnum end_cnum
+
 let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf)
 
 let remove_quotes s = String.sub s 1 (String.length s - 2)
@@ -104,22 +140,84 @@ let expand_macro lexbuf =
 
 let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf)
 
-let rec token = lexer
-  | xml_blank+ -> token lexbuf
+let remove_quotes s = String.sub s 1 (String.length s - 2)
+let remove_left_quote s = String.sub s 1 (String.length s - 1)
+
+let rec level2_pattern_token_group counter buffer = lexer
+  | end_group -> 
+      if (counter > 0) then
+       Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
+      snd (Ulexing.loc lexbuf)
+  | begin_group -> 
+      Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
+      ignore (level2_pattern_token_group (counter + 1) buffer lexbuf) ;
+      level2_pattern_token_group counter buffer lexbuf
+  | _ -> 
+      Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
+      level2_pattern_token_group counter buffer lexbuf
+
+let read_unparsed_group token_name lexbuf =
+  let buffer = Buffer.create 16 in
+  let begin_cnum, _ = Ulexing.loc lexbuf in
+  let end_cnum = level2_pattern_token_group 0 buffer lexbuf in
+    return_with_loc (token_name, Buffer.contents buffer) begin_cnum end_cnum
+
+let rec level2_meta_token = lexer
+  | xml_blank+ -> level2_meta_token lexbuf
+  | ident ->
+      let s = Ulexing.utf8_lexeme lexbuf in
+       begin
+         if List.mem s level2_meta_keywords then
+           return lexbuf ("", s)
+         else
+           return lexbuf ("IDENT", s)
+       end
+  | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
+  | ast_ident -> return lexbuf ("UNPARSED_AST", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+  | ast_csymbol ->  return lexbuf ("UNPARSED_AST", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+  | eof -> return lexbuf ("EOI", "")
+
+let rec level2_ast_token = lexer
+  | xml_blank+ -> level2_ast_token lexbuf
   | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf)
   | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf)
   | ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
   | keyword -> return lexbuf (keyword lexbuf)
-  | delim_begin -> return lexbuf ("DELIM", Ulexing.utf8_lexeme lexbuf)
-  | delim_end -> return lexbuf ("DELIM",  Ulexing.utf8_lexeme lexbuf)
   | tex_token -> return lexbuf (expand_macro lexbuf)
   | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
-  | eof -> return lexbuf ("EOI", "")
+  | qstring -> return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
   | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
+  | "${" -> read_unparsed_group "UNPARSED_META" lexbuf
+  | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
+  | '(' -> return lexbuf ("LPAREN", "")
+  | ')' -> return lexbuf ("RPAREN", "")
+  | meta_ident -> return lexbuf ("UNPARSED_META", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+  | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
+  | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
+  | eof -> return lexbuf ("EOI", "")
+
+let rec level1_pattern_token = lexer
+  | xml_blank+ -> level1_pattern_token lexbuf
+  | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
+  | ident ->
+      let s = Ulexing.utf8_lexeme lexbuf in
+       begin
+         if List.mem s level1_keywords then
+           return lexbuf ("", s)
+         else
+           return lexbuf ("IDENT", s)
+       end
+  | tex_token -> return lexbuf (expand_macro lexbuf)
+  | qkeyword -> return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
+  | '(' -> return lexbuf ("LPAREN", "")
+  | ')' -> return lexbuf ("RPAREN", "")
+  | eof -> return lexbuf ("EOI", "")
   | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
 
 (* API implementation *)
 
-let notation_lexer = mk_lexer token
+let level1_pattern_lexer = mk_lexer level1_pattern_token
+let level2_ast_lexer = mk_lexer level2_ast_token
+let level2_meta_lexer = mk_lexer level2_meta_token