[NoBinding, gram_keyword s]
| `Number s -> [NoBinding, gram_number s]
and aux_layout = function
- | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
- | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
- | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
- | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
- | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
- | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
- | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
- | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
+ | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2
+ | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2
+ | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below "] @ aux p2
+ | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above "] @ aux p2
+ | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac "] @ aux p2
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+ | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop "] @ aux p2
+ | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over "] @ aux p2
| Ast.Root (p1, p2) ->
- [NoBinding, gram_symbol "\\root"] @ aux p2
- @ [NoBinding, gram_symbol "\\of"] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
+ [NoBinding, gram_symbol "\\root "] @ aux p2
+ @ [NoBinding, gram_symbol "\\of "] @ aux p1
+ | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p
| Ast.Break -> []
| Ast.Box (_, pl) -> List.flatten (List.map aux pl)
| Ast.Group pl -> List.flatten (List.map aux pl)
| Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl)
+ | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl)
+ | Ast.Maction l -> List.flatten (List.map aux l)
and aux_magic magic =
match magic with
| Ast.Opt p ->
match magic with
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
| [],[] -> 0
| [],_ -> ~-1
| _,[] -> 1
- | ((s1::tl1) as x),((s2::tl2) as y) ->
+ | ((s1::tl1) ),((s2::tl2) ) ->
if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
- else Pervasives.compare x y
+ else
+ let res =
+ try Pervasives.compare s1 s2
+ with Invalid_argument _ -> 0
+ in
+ if res = 0 then aux (tl1, tl2) else res
in
aux (x,y)
type checked_l1_pattern = CL1P of CicNotationPt.term * int
-let check_l1_pattern level1_pattern level associativity =
+let check_l1_pattern level1_pattern pponly level associativity =
let variables = ref 0 in
let symbols = ref 0 in
let rec aux = function
| Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
| Ast.Group pl -> Ast.Group (List.map aux pl)
| Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl)
+ | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl)
+ | Ast.Maction l as t ->
+ if not pponly then
+ raise(Parse_error("Maction can be used only in output notations"))
+ else t
and aux_magic magic =
match magic with
| Ast.Opt p -> Ast.Opt (aux p)
mstyle: [
[ id = IDENT;
v = [ IDENT | NUMBER | COLOR | FLOATWITHUNIT ] -> id, v]];
+ mpadded: [
+ [ id = IDENT;
+ v = [ PERCENTAGE ] -> id, v]];
l1_simple_pattern:
[ "layout" LEFTA
- [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
+ [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
- | p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\sup "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
- | p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\below "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
- | p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\above "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
- | p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\over "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
- | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\atop "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
- | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
+ | p1 = SELF; SYMBOL "\\frac "; p2 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
- | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
+ | SYMBOL "\\infrule "; p1 = SELF; p2 = SELF; p3 = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
- | SYMBOL "\\sqrt"; p = SELF ->
+ | SYMBOL "\\sqrt "; p = SELF ->
return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
- | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
+ | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF ->
return_term_of_level loc
(fun l -> Ast.Layout (Ast.Root (arg l, index l)))
| "hbox"; LPAREN; p = l1_pattern; RPAREN ->
return_term_of_level loc
(fun l ->
Ast.Layout (Ast.Mstyle (m, t l)))
+ | "mpadded"; m = LIST1 mpadded ; LPAREN; t = l1_pattern; RPAREN ->
+ return_term_of_level loc
+ (fun l ->
+ Ast.Layout (Ast.Mpadded (m, t l)))
+ | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] ->
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Maction (List.map (fun x ->
+ CicNotationUtil.group (x l)) m)))
| LPAREN; p = l1_pattern; RPAREN ->
return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
]
sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
+ | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
| "Type" -> `Type (CicUniv.fresh ())
+ | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
| "CProp" -> `CProp (CicUniv.fresh ())
]
];
explicit_subst: [
- [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
+ [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *)
SYMBOL "[";
substs = LIST1 [
i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
[ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
id, Some typ
| arg = single_arg -> arg, None
+ | id = PIDENT -> Ast.Ident (id, None), None
| SYMBOL "_" -> Ast.Ident ("_", None), None
+ | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
+ Ast.Ident (id, None), Some typ
| LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
Ast.Ident ("_", None), Some typ
]
];
match_pattern: [
- [ id = IDENT -> Ast.Pattern (id, None, [])
+ [ SYMBOL "_" -> Ast.Wildcard
+ | id = IDENT -> Ast.Pattern (id, None, [])
| LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
Ast.Pattern (id, None, vars)
| id = IDENT; vars = LIST1 possibly_typed_name ->
Ast.Pattern (id, None, vars)
- | SYMBOL "_" -> Ast.Wildcard
]
];
binder: [
]
];
binder_vars: [
- [ vars = [
- l = LIST1 single_arg SEP SYMBOL "," -> l
- | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
+ [ vars = [ l =
+ [ l = LIST1 single_arg SEP SYMBOL "," -> l
+ | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," ->
+ List.map (fun x -> Ast.Ident(x,None)) l
+ ] -> l ];
typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
]
];
];
term: LEVEL "10"
[
- [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ [ "let";
+ var =
+ [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
+ id, Some typ
+ | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
+ Ast.Ident(id,None), ty ];
+ SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
| LETCOREC; defs = let_defs; "in";
return_term loc (Ast.Ident (id, Some s))
| s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
| u = URI -> return_term loc (Ast.Uri (u, None))
+ | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
| n = NUMBER -> return_term loc (Ast.Num (n, 0))
- | IMPLICIT -> return_term loc (Ast.Implicit)
+ | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
+ | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
| PLACEHOLDER -> return_term loc Ast.UserInput
| m = META -> return_term loc (Ast.Meta (int_of_string m, []))
| m = META; s = meta_substs ->
try
f ()
with
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ | Ploc.Exc (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc, Parse_error msg))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
+ raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
+ | Ploc.Exc (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
let parse_level1_pattern precedence lexbuf =
projects / helm.git / blobdiff