diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 14 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 9 |
2 files changed, 21 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5f729762f0..77b4f003cd 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -24,7 +24,8 @@ open Util let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "Prop"; "Set"; "Type"; ".("; "_"; ".." ] + "Prop"; "Set"; "Type"; ".("; "_"; ".."; + "`{"; "`("; ] let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw @@ -203,7 +204,12 @@ GEXTEND Gram (match c with CPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> CNotation(loc,"( _ )",([c],[])) - | _ -> c) ] ] + | _ -> c) + | "`{"; c = operconstr LEVEL "200"; "}" -> + CGeneralization (loc, Implicit, None, c) + | "`("; c = operconstr LEVEL "200"; ")" -> + CGeneralization (loc, Explicit, None, c) + ] ] ; forall: [ [ "forall" -> () @@ -400,8 +406,12 @@ GEXTEND Gram List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Explicit, b), t)) tc + | "{"; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; "}" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + | "("; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; ")" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Implicit, b), t)) tc | "["; tc = LIST1 typeclass_constraint SEP ","; "]" -> List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc ] ] diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 239d3772f0..a2cad8e170 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -92,6 +92,14 @@ let pr_notation pr s env = let pr_delimiters key strm = strm ++ str ("%"^key) +let pr_generalization bk ak c = + let hd, tl = + match bk with + | Implicit -> "{", "}" + | Explicit -> "(", ")" + in (* TODO: syntax Abstraction Kind *) + str "`" ++ str hd ++ c ++ str tl + let pr_com_at n = if Flags.do_translate() && n <> 0 then comment n else mt() @@ -597,6 +605,7 @@ let rec pr sep inherited a = | CNotation (_,"( _ )",([t],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env + | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 | CDynamic _ -> str "<dynamic>", latom |