exception Parse_error of Token.flocation * string
-let grammar = Grammar.gcreate CicNotationLexer.level1_lexer
+module Level1Lexer =
+struct
+ type te = string * string
+ let lexer = CicNotationLexer.syntax_pattern_lexer
+end
+module Level1Parser = Grammar.GMake (Level1Lexer)
-let level1 = Grammar.Entry.create grammar "level1"
+module Level2Lexer =
+struct
+ type te = string * string
+ let lexer = CicNotationLexer.ast_pattern_lexer
+end
+module Level2Parser = Grammar.GMake (Level2Lexer)
+
+let level1_pattern = Level1Parser.Entry.create "level1_pattern"
+let level2_pattern = Level2Parser.Entry.create "level2_pattern"
let return_term loc term = ()
with Failure _ ->
failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
-EXTEND
- GLOBAL: level1;
-
- level1: [ [ p = pattern -> () ] ];
-
+(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
+GEXTEND Level1Parser
+ GLOBAL: level1_pattern;
+ level1_pattern: [ [ p = pattern -> () ] ];
pattern: [ [ p = LIST1 simple_pattern -> () ] ];
-
literal: [
[ s = SYMBOL -> ()
| k = KEYWORD -> ()
]
];
-
sep: [ [ SYMBOL "\\SEP"; sep = literal -> () ] ];
row_sep: [ [ SYMBOL "\\ROWSEP"; sep = literal -> () ] ];
field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ];
-
- box_token: [
+ box_pattern: [
[ SYMBOL "\\HBOX"; p = simple_pattern -> ()
| SYMBOL "\\VBOX"; p = simple_pattern -> ()
| SYMBOL "\\BREAK" -> ()
]
];
+ magic_pattern: [
+ [ SYMBOL "\\LIST0"; p = simple_pattern; sep = OPT sep -> ()
+ | SYMBOL "\\LIST1"; p = simple_pattern; sep = OPT sep -> ()
+ | SYMBOL "\\OPT"; p = simple_pattern -> ()
+ ]
+ ];
+ pattern_variable: [
+ [ id = IDENT -> ()
+ | SYMBOL "\\NUM"; id = IDENT -> ()
+ | SYMBOL "\\IDENT"; id = IDENT -> ()
+ ]
+ ];
+ simple_pattern:
+ [ "layout" LEFTA
+ [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> ()
+ | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> ()
+ | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> ()
+ | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> ()
+ | SYMBOL "["; p1 = pattern; SYMBOL "\\OVER"; p2 = pattern; SYMBOL "]" ->
+ ()
+ | SYMBOL "["; p1 = pattern; SYMBOL "\\ATOP"; p2 = pattern; SYMBOL "]" ->
+ ()
+ | SYMBOL "\\ARRAY"; p = SELF; fsep = OPT field_sep; rsep = OPT row_sep ->
+ ()
+ | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> ()
+ | SYMBOL "\\SQRT"; p = SELF -> ()
+ | SYMBOL "\\ROOT"; arg = pattern; SYMBOL "\\OF"; index = SELF -> ()
+ ]
+ | "simple" NONA
+ [ m = magic_pattern -> ()
+ | v = pattern_variable -> ()
+ | b = box_pattern -> ()
+ | n = NUMBER -> ()
+ | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
+ ]
+ ];
+END
+(* }}} *)
- layout_schemata: [
- [ SYMBOL "\\ARRAY"; p = simple_pattern; fsep = OPT field_sep;
- rsep = OPT row_sep ->
+(* {{{ Grammar for ast patterns, notation level 2 *)
+GEXTEND Level2Parser
+ GLOBAL: level2_pattern;
+ level2_pattern: [ [ p = pattern -> () ] ];
+ sort: [
+ [ SYMBOL "\\PROP" -> ()
+ | SYMBOL "\\SET" -> ()
+ | SYMBOL "\\TYPE" -> ()
+ ]
+ ];
+ explicit_subst: [
+ [ (* TODO explicit substitution *)
+ ]
+ ];
+ meta_subst: [
+ [ (* TODO meta substitution *)
+ ]
+ ];
+ possibly_typed_name: [
+ [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = pattern; SYMBOL ")" -> ()
+ | i = IDENT -> ()
+ ]
+ ];
+ match_pattern: [
+ [ n = IDENT -> ()
+ | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
()
- | SYMBOL "\\FRAC"; p1 = simple_pattern; p2 = simple_pattern -> ()
- | SYMBOL "\\SQRT"; p = simple_pattern -> ()
- | SYMBOL "\\ROOT"; p1 = simple_pattern; SYMBOL "\\OF";
- p2 = simple_pattern ->
+ ]
+ ];
+ binder: [
+ [ SYMBOL <:unicode<Pi>> (* Π *) -> ()
+ | SYMBOL <:unicode<exists>> (* ∃ *) -> ()
+ | SYMBOL <:unicode<forall>> (* ∀ *) -> ()
+ | SYMBOL <:unicode<lambda>> (* λ *) -> ()
+ ]
+ ];
+ bound_names: [
+ [ vars = LIST1 IDENT SEP SYMBOL ",";
+ typ = OPT [ SYMBOL ":"; p = pattern -> () ] -> ()
+ | LIST1 [
+ SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ",";
+ typ = OPT [ SYMBOL ":"; p = pattern -> () ]; SYMBOL ")" -> ()
+ ] ->
()
- (* TODO XXX many issues here:
- * - "^^" is lexed as two "^" symbols
- * - "a_b" is lexed as IDENT "a_b" *)
- | p1 = simple_pattern; SYMBOL "^"; p2 = simple_pattern -> ()
- | p1 = simple_pattern; SYMBOL "^"; SYMBOL "^"; p2 = simple_pattern -> ()
- | p1 = simple_pattern; SYMBOL "_"; p2 = simple_pattern -> ()
- | p1 = simple_pattern; SYMBOL "_"; SYMBOL "_"; p2 = simple_pattern -> ()
]
];
-
- simple_pattern: [
- [ SYMBOL "\\LIST0"; p = simple_pattern; sep = OPT sep -> ()
- | SYMBOL "\\LIST1"; p = simple_pattern; sep = OPT sep -> ()
- | b = box_token -> ()
- | id = IDENT -> ()
- | SYMBOL "\\NUM"; id = IDENT -> ()
+ induction_kind: [
+ [ IDENT "rec" -> ()
+ | IDENT "corec" -> ()
+ ]
+ ];
+ let_defs: [
+ [ defs = LIST1 [
+ name = IDENT; args = bound_names;
+ index_name = OPT [ IDENT "on"; idx = IDENT -> () ];
+ ty = OPT [ SYMBOL ":" ; p = pattern -> () ];
+ SYMBOL <:unicode<def>> (* ≝ *); body = pattern ->
+ ()
+ ] SEP IDENT "and" ->
+ ()
+ ]
+ ];
+ pattern_variable: [
+ [ SYMBOL "\\NUM"; id = IDENT -> ()
| SYMBOL "\\IDENT"; id = IDENT -> ()
- | SYMBOL "\\OPT"; p = simple_pattern -> ()
- | l = layout_schemata -> ()
- | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
+ | SYMBOL "\\FRESH"; id = IDENT -> ()
]
];
+ magic_pattern: [
+ [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ];
+ LIST1 IDENT; SYMBOL "."; p1 = pattern;
+ OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = pattern ->
+ ()
+ | SYMBOL "\\DEFAULT"; id = IDENT; p1 = pattern; p2 = pattern -> ()
+ ]
+ ];
+ pattern:
+ [ "letin" NONA
+ [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ p1 = pattern; "in"; p2 = pattern ->
+ ()
+ | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
+ body = pattern ->
+ ()
+ ]
+ | "binder" RIGHTA
+ [ b = binder; bound_names; SYMBOL "."; body = pattern -> () ]
+ | "extension"
+ [ ]
+ | "apply" LEFTA
+ [ p1 = pattern; p2 = pattern -> () ]
+ | "simple" NONA
+ [ i = IDENT -> ()
+ | i = IDENT; s = explicit_subst -> ()
+ | n = NUMBER -> ()
+ | IMPLICIT -> ()
+ | m = META -> ()
+ | m = META; s = meta_subst -> ()
+ | s = sort -> ()
+ | s = SYMBOL -> ()
+ | u = URI -> ()
+ | outtyp = OPT [ SYMBOL "["; typ = pattern; SYMBOL "]" ];
+ IDENT "match"; t = pattern;
+ indty_ident = OPT [ SYMBOL ":"; id = IDENT ];
+ IDENT "with"; SYMBOL "[";
+ patterns = LIST0 [
+ lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
+ rhs = pattern ->
+ ()
+ ] SEP SYMBOL "|";
+ SYMBOL "]" ->
+ ()
+ | SYMBOL "("; p1 = pattern; SYMBOL ":"; p2 = pattern; SYMBOL ")" -> ()
+ | SYMBOL "("; p = pattern; SYMBOL ")" -> ()
+ | v = pattern_variable -> ()
+ | m = magic_pattern -> ()
+ ]
+ ];
END
+(* }}} *)
let exc_located_wrapper f =
try
| Stdpp.Exc_located (floc, exn) ->
raise (Parse_error (floc, (Printexc.to_string exn)))
-let parse_level1_pattern stream =
- exc_located_wrapper (fun () -> (Grammar.Entry.parse level1 stream))
+let parse_syntax_pattern stream =
+ exc_located_wrapper
+ (fun () ->
+ (Level1Parser.Entry.parse level1_pattern (Level1Parser.parsable stream)))
+
+let parse_ast_pattern stream =
+ exc_located_wrapper
+ (fun () ->
+ (Level2Parser.Entry.parse level2_pattern (Level2Parser.parsable stream)))
-(* vim:set encoding=utf8: *)
+(* vim:set encoding=utf8 foldmethod=marker: *)
projects / helm.git / blobdiff