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 interpretation =
+ NotationGrammar.Entry.create "interpretation" (* level2 <-> level 3 *)
let return_term loc term = ()
-(*let fail floc msg =*)
-(* let (x, y) = CicAst.loc_of_floc floc in*)
-(* failwith (sprintf "Error at characters %d - %d: %s" x y msg)*)
+let loc_of_floc = function
+ | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
+ (loc_begin, loc_end)
+
+let fail floc msg =
+ let (x, y) = loc_of_floc floc in
+ failwith (sprintf "Error at characters %d - %d: %s" x y msg)
let int_of_string s =
try
with Failure _ ->
failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
+open CicNotationPt
+
+let boxify = function
+ | [ a ] -> a
+ | l -> Layout (Box (H, l))
+
+let fold_binder binder pt_names body =
+ let fold_cluster binder names ty body =
+ List.fold_right
+ (fun name body -> Binder (binder, (Cic.Name name, ty), body))
+ names body
+ in
+ List.fold_right
+ (fun (names, ty) body -> fold_cluster binder names ty body)
+ pt_names body
+
GEXTEND NotationGrammar
- GLOBAL: level1_pattern level2_pattern level3_interpretation;
+ GLOBAL: level1_pattern level2_pattern level3_interpretation notation
+ interpretation;
(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
- level1_pattern: [ [ p = l1_pattern -> () ] ];
- l1_pattern: [ [ p = LIST1 l1_simple_pattern -> () ] ];
+ level1_pattern: [ [ p = l1_pattern -> boxify p ] ];
+ l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ];
literal: [
- [ s = SYMBOL -> ()
- | k = KEYWORD -> ()
- ]
- ];
- sep: [ [ SYMBOL "\\SEP"; sep = literal -> () ] ];
- row_sep: [ [ SYMBOL "\\ROWSEP"; sep = literal -> () ] ];
- field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ];
- l1_box_pattern: [
- [ SYMBOL "\\HBOX"; p = l1_simple_pattern -> ()
- | SYMBOL "\\VBOX"; p = l1_simple_pattern -> ()
- | SYMBOL "\\BREAK" -> ()
+ [ s = SYMBOL -> `Symbol s
+ | k = KEYWORD -> `Keyword k
+ | n = NUMBER -> `Number n
]
];
+ sep: [ [ SYMBOL "\\SEP"; sep = literal -> sep ] ];
+(* row_sep: [ [ SYMBOL "\\ROWSEP"; sep = literal -> sep ] ];
+ field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> sep ] ]; *)
l1_magic_pattern: [
- [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> ()
- | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> ()
- | SYMBOL "\\OPT"; p = l1_simple_pattern -> ()
+ [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep)
+ | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep)
+ | SYMBOL "\\OPT"; p = l1_simple_pattern -> Opt p
]
];
l1_pattern_variable: [
- [ id = IDENT -> ()
- | SYMBOL "\\NUM"; id = IDENT -> ()
- | SYMBOL "\\IDENT"; id = IDENT -> ()
+ [ id = IDENT -> TermVar id
+ | SYMBOL "\\TERM"; id = IDENT -> TermVar id
+ | SYMBOL "\\NUM"; id = IDENT -> NumVar id
+ | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
]
];
l1_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 -> ()
+ [ 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))
| SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
SYMBOL "]" ->
- ()
+ Layout (Frac (boxify p1, boxify p2))
| SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_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 = l1_pattern; SYMBOL "\\OF"; index = SELF -> ()
+ 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)
+ | SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF ->
+ Layout (Root (arg, Layout (Box (H, index))))
+ | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
+ 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))
+ | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" ->
+ Variable (Ascription (Layout (Box (H, p)), id))
]
| "simple" NONA
- [ m = l1_magic_pattern -> ()
- | v = l1_pattern_variable -> ()
- | b = l1_box_pattern -> ()
- | n = NUMBER -> ()
- | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> ()
+ [ m = l1_magic_pattern -> Magic m
+ | v = l1_pattern_variable -> Variable v
]
];
(* }}} *)
(* {{{ Grammar for ast patterns, notation level 2 *)
- level2_pattern: [ [ p = l2_pattern -> () ] ];
+ level2_pattern: [ [ p = l2_pattern -> p ] ];
sort: [
- [ SYMBOL "\\PROP" -> ()
- | SYMBOL "\\SET" -> ()
- | SYMBOL "\\TYPE" -> ()
+ [ SYMBOL "\\PROP" -> `Prop
+ | SYMBOL "\\SET" -> `Set
+ | SYMBOL "\\TYPE" -> `Type
]
];
explicit_subst: [
]
];
possibly_typed_name: [
- [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" -> ()
- | i = IDENT -> ()
+ [ SYMBOL "("; id = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
+ Cic.Name id, Some typ
+ | id = IDENT -> Cic.Name id, None
]
];
match_pattern: [
- [ n = IDENT -> ()
- | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
- ()
+ [ id = IDENT -> id, []
+ | SYMBOL "("; id = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
+ id, vars
]
];
binder: [
- [ SYMBOL <:unicode<Pi>> (* Π *) -> ()
- | SYMBOL <:unicode<exists>> (* ∃ *) -> ()
- | SYMBOL <:unicode<forall>> (* ∀ *) -> ()
- | SYMBOL <:unicode<lambda>> (* λ *) -> ()
+ [ SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
+ | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
+ | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
+ | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
];
bound_names: [
[ vars = LIST1 IDENT SEP SYMBOL ",";
- typ = OPT [ SYMBOL ":"; p = l2_pattern -> () ] -> ()
- | LIST1 [
- SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ",";
- typ = OPT [ SYMBOL ":"; p = l2_pattern -> () ]; SYMBOL ")" -> ()
+ ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] ->
+ [ vars, ty ]
+ | clusters = LIST1 [
+ SYMBOL "(";
+ vars = LIST1 IDENT SEP SYMBOL ",";
+ ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ];
+ SYMBOL ")" ->
+ vars, ty
] ->
- ()
+ clusters
]
];
induction_kind: [
- [ IDENT "rec" -> ()
- | IDENT "corec" -> ()
+ [ IDENT "rec" -> `Inductive
+ | IDENT "corec" -> `CoInductive
]
];
let_defs: [
[ defs = LIST1 [
name = IDENT; args = bound_names;
- index_name = OPT [ IDENT "on"; idx = IDENT -> () ];
- ty = OPT [ SYMBOL ":" ; p = l2_pattern -> () ];
+ index_name = OPT [ IDENT "on"; id = IDENT -> id ];
+ ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ];
SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
- ()
+ let body = fold_binder `Lambda args body in
+ let ty =
+ match ty with
+ | None -> None
+ | Some ty -> Some (fold_binder `Pi args ty)
+ in
+ let rec position_of name p = function
+ | [] -> None, p
+ | n :: _ when n = name -> Some p, p
+ | _ :: tl -> position_of name (p + 1) tl
+ in
+ let rec find_arg name n = function
+ | [] -> fail loc (sprintf "Argument %s not found" name)
+ | (l,_) :: tl ->
+ (match position_of name 0 l with
+ | None, len -> find_arg name (n + len) tl
+ | Some where, len -> n + where)
+ in
+ let index =
+ match index_name with
+ | None -> 0
+ | Some name -> find_arg name 0 args
+ in
+ (Cic.Name name, ty), body, index
] SEP IDENT "and" ->
- ()
+ defs
]
];
l2_pattern_variable: [
- [ SYMBOL "\\NUM"; id = IDENT -> ()
- | SYMBOL "\\IDENT"; id = IDENT -> ()
- | SYMBOL "\\FRESH"; id = IDENT -> ()
+ [ SYMBOL "\\NUM"; id = IDENT -> NumVar id
+ | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
+ | SYMBOL "\\FRESH"; id = IDENT -> FreshVar id
]
];
l2_magic_pattern: [
- [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ];
- LIST1 IDENT; SYMBOL "."; p1 = l2_pattern;
- OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = l2_pattern ->
- ()
- | SYMBOL "\\DEFAULT"; id = IDENT; p1 = l2_pattern; p2 = l2_pattern -> ()
+ [ SYMBOL "\\FOLD";
+ kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ];
+ base = l2_pattern;
+ SYMBOL "\\LAMBDA"; id = IDENT; recursive = l2_pattern ->
+ Fold (kind, base, [id], recursive)
+ | SYMBOL "\\DEFAULT"; some = l2_pattern; none = l2_pattern ->
+ Default (some, none)
]
];
l2_pattern:
[ "letin" NONA
[ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = l2_pattern; "in"; p2 = l2_pattern ->
- ()
+ LetIn (var, p1, p2)
| IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
body = l2_pattern ->
- ()
+ LetRec (k, defs, body)
]
| "binder" RIGHTA
- [ b = binder; bound_names; SYMBOL "."; body = l2_pattern -> () ]
+ [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
+ fold_binder b names body
+ ]
| "extension"
[ ]
| "apply" LEFTA
- [ p1 = l2_pattern; p2 = l2_pattern -> () ]
+ [ p1 = l2_pattern; p2 = l2_pattern ->
+ let rec aux = function
+ | Appl (hd :: tl) -> aux hd @ tl
+ | term -> [term]
+ in
+ Appl (aux p1 @ [p2])
+ ]
| "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 = l2_pattern; SYMBOL "]" ];
+ [ 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)
+ | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
IDENT "match"; t = l2_pattern;
- indty_ident = OPT [ SYMBOL ":"; id = IDENT ];
+ indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
IDENT "with"; SYMBOL "[";
patterns = LIST0 [
lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
rhs = l2_pattern ->
- ()
+ lhs, rhs
] SEP SYMBOL "|";
SYMBOL "]" ->
- ()
+ Case (t, indty_ident, outtyp, patterns)
| SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" ->
- ()
- | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> ()
- | v = l2_pattern_variable -> ()
- | m = l2_magic_pattern -> ()
+ Appl [ Symbol ("cast", 0); p1; p2 ]
+ | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p
+ | v = l2_pattern_variable -> Variable v
+ | m = l2_magic_pattern -> Magic m
]
];
(* }}} *)
| SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
]
];
+(* }}} *)
+(* {{{ Notation glues *)
+ associativity: [
+ [ IDENT "left"; IDENT "associative" -> `Left
+ | IDENT "right"; IDENT "associative" -> `Right
+ ]
+ ];
+ precedence: [ [ IDENT "at"; IDENT "precedence"; n = NUMBER -> n ] ];
+ notation: [
+ [ IDENT "notation"; p1 = level1_pattern; IDENT "for"; p2 = level2_pattern;
+ assoc = OPT associativity; prec = OPT precedence ->
+ ()
+ ]
+ ];
interpretation: [
[ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
t = l3_term ->
projects / helm.git / blobdiff