exception Parse_error of Token.flocation * string
-module NotationLexer =
-struct
- type te = string * string
- let lexer = CicNotationLexer.notation_lexer
-end
-module NotationGrammar = Grammar.GMake (NotationLexer)
+let grammar = Grammar.gcreate CicNotationLexer.notation_lexer
-let level1_pattern = NotationGrammar.Entry.create "level1_pattern"
-let level2_pattern = NotationGrammar.Entry.create "level2_pattern"
-let level3_interpretation = NotationGrammar.Entry.create "level3_interpretation"
-let notation = NotationGrammar.Entry.create "notation" (* level1 <-> level 2 *)
+let level1_pattern = Grammar.Entry.create grammar "level1_pattern"
+let level2_pattern = Grammar.Entry.create grammar "level2_pattern"
+let level3_term = Grammar.Entry.create grammar "level3_term"
+let notation = Grammar.Entry.create grammar "notation" (* level1 <-> level 2 *)
let interpretation =
- NotationGrammar.Entry.create "interpretation" (* level2 <-> level 3 *)
+ Grammar.Entry.create grammar "interpretation" (* level2 <-> level 3 *)
let return_term loc term = ()
(fun (names, ty) body -> fold_cluster binder names ty body)
pt_names body
-GEXTEND NotationGrammar
- GLOBAL: level1_pattern level2_pattern level3_interpretation notation
- interpretation;
+let return_term loc term = AttributedTerm (`Loc loc, term)
+
+EXTEND
+ GLOBAL: level1_pattern level2_pattern level3_term
+ notation interpretation;
(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
- level1_pattern: [ [ p = l1_pattern -> boxify p ] ];
+ level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ];
l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ];
literal: [
[ s = SYMBOL -> `Symbol s
];
l1_simple_pattern:
[ "layout" LEFTA
- [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> Layout (Sub (p1, p2))
- | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> Layout (Sup (p1, p2))
- | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> Layout (Below (p1, p2))
- | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> Layout (Above (p1, p2))
+ [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF ->
+ return_term loc (Layout (Sub (p1, p2)))
+ | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF ->
+ return_term loc (Layout (Sup (p1, p2)))
+ | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF ->
+ return_term loc (Layout (Below (p1, p2)))
+ | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF ->
+ return_term loc (Layout (Above (p1, p2)))
| SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
SYMBOL "]" ->
- Layout (Frac (boxify p1, boxify p2))
+ return_term loc (Layout (Frac (boxify p1, boxify p2)))
| SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern;
SYMBOL "]" ->
- Layout (Atop (boxify p1, boxify p2))
+ return_term loc (Layout (Atop (boxify p1, boxify p2)))
(* | SYMBOL "\\ARRAY"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
- Array (p, csep, rsep) *)
- | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> Layout (Frac (p1, p2))
- | SYMBOL "\\SQRT"; p = SELF -> Layout (Sqrt p)
+ return_term loc (Array (p, csep, rsep)) *)
+ | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF ->
+ return_term loc (Layout (Frac (p1, p2)))
+ | SYMBOL "\\SQRT"; p = SELF -> return_term loc (Layout (Sqrt p))
| SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF ->
- Layout (Root (arg, Layout (Box (H, index))))
+ return_term loc (Layout (Root (arg, Layout (Box (H, index)))))
| SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
- Layout (Box (H, p))
+ return_term loc (Layout (Box (H, p)))
| SYMBOL "\\VBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
- Layout (Box (V, p))
- | SYMBOL "\\BREAK" -> Layout Break
- | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> Layout (Box (H, p))
+ return_term loc (Layout (Box (V, p)))
+ | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
+ | SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
+ return_term loc (Layout (Box (H, p)))
| SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" ->
- Variable (Ascription (Layout (Box (H, p)), id))
+ return_term loc (Variable (Ascription (Layout (Box (H, p)), id)))
]
| "simple" NONA
- [ m = l1_magic_pattern -> Magic m
- | v = l1_pattern_variable -> Variable v
+ [ m = l1_magic_pattern -> return_term loc (Magic m)
+ | v = l1_pattern_variable -> return_term loc (Variable v)
+ | l = literal -> return_term loc (Literal l)
]
];
(* }}} *)
[ "letin" NONA
[ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = l2_pattern; "in"; p2 = l2_pattern ->
- LetIn (var, p1, p2)
+ return_term loc (LetIn (var, p1, p2))
| IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
body = l2_pattern ->
- LetRec (k, defs, body)
+ return_term loc (LetRec (k, defs, body))
]
| "binder" RIGHTA
[ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
- fold_binder b names body
+ return_term loc (fold_binder b names body)
]
| "extension"
[ ]
| "apply" LEFTA
[ p1 = l2_pattern; p2 = l2_pattern ->
let rec aux = function
- | Appl (hd :: tl) -> aux hd @ tl
+ | Appl (hd :: tl)
+ | AttributedTerm (_, Appl (hd :: tl)) ->
+ aux hd @ tl
| term -> [term]
in
- Appl (aux p1 @ [p2])
+ return_term loc (Appl (aux p1 @ [p2]))
]
| "simple" NONA
- [ id = IDENT -> Ident (id, None)
- | id = IDENT; s = explicit_subst -> Ident (id, Some s)
- | u = URI -> Uri (u, None)
- | n = NUMBER -> Num (n, 0)
- | IMPLICIT -> Implicit
- | m = META -> Meta (int_of_string m, [])
- | m = META; s = meta_subst -> Meta (int_of_string m, s)
- | s = sort -> Sort s
- | s = SYMBOL -> Symbol (s, 0)
+ [ id = IDENT -> return_term loc (Ident (id, None))
+ | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
+ | u = URI -> return_term loc (Uri (u, None))
+ | n = NUMBER -> return_term loc (Num (n, 0))
+ | IMPLICIT -> return_term loc (Implicit)
+ | m = META -> return_term loc (Meta (int_of_string m, []))
+ | m = META; s = meta_subst -> return_term loc (Meta (int_of_string m, s))
+ | s = sort -> return_term loc (Sort s)
+ | s = SYMBOL -> return_term loc (Symbol (s, 0))
| outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
IDENT "match"; t = l2_pattern;
indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
lhs, rhs
] SEP SYMBOL "|";
SYMBOL "]" ->
- Case (t, indty_ident, outtyp, patterns)
+ return_term loc (Case (t, indty_ident, outtyp, patterns))
| SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" ->
- Appl [ Symbol ("cast", 0); p1; p2 ]
+ return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ])
| SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p
- | v = l2_pattern_variable -> Variable v
- | m = l2_magic_pattern -> Magic m
+ | v = l2_pattern_variable -> return_term loc (Variable v)
+ | m = l2_magic_pattern -> return_term loc (Magic m)
]
];
(* }}} *)
(* {{{ Grammar for interpretation, notation level 3 *)
- level3_interpretation: [ [ i = interpretation -> () ] ];
argument: [
- [ i = IDENT -> ()
- | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> ()
- | SYMBOL <:unicode<eta>> (* η *); i = IDENT; SYMBOL "."; a = SELF -> ()
+ [ id = IDENT -> IdentArg id
+ | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a)
+ | SYMBOL <:unicode<eta>> (* η *); id = IDENT; SYMBOL "."; a = SELF ->
+ EtaArg (Some id, a)
]
];
- l3_term: [
- [ u = URI -> ()
- | a = argument -> ()
- | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
+ level3_term: [
+ [ u = URI -> UriPattern u
+ | a = argument -> ArgPattern a
+ | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
+ (match terms with
+ | [] -> assert false
+ | [term] -> term
+ | terms -> ApplPattern terms)
]
];
(* }}} *)
];
interpretation: [
[ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
- t = l3_term ->
+ t = level3_term ->
()
]
];
raise (Parse_error (floc, (Printexc.to_string exn)))
let parse_syntax_pattern stream =
- exc_located_wrapper
- (fun () ->
- (NotationGrammar.Entry.parse level1_pattern
- (NotationGrammar.parsable stream)))
+ exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
let parse_ast_pattern stream =
- exc_located_wrapper
- (fun () ->
- (NotationGrammar.Entry.parse level2_pattern
- (NotationGrammar.parsable stream)))
+ exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
let parse_interpretation stream =
- exc_located_wrapper
- (fun () ->
- (NotationGrammar.Entry.parse level3_interpretation
- (NotationGrammar.parsable stream)))
+ exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
(* vim:set encoding=utf8 foldmethod=marker: *)
projects / helm.git / commitdiff