summaryrefslogtreecommitdiff
path: root/parsing/g_constr.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_constr.mlg')
-rw-r--r--parsing/g_constr.mlg526
1 files changed, 526 insertions, 0 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
new file mode 100644
index 00000000..7cb5af78
--- /dev/null
+++ b/parsing/g_constr.mlg
@@ -0,0 +1,526 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+{
+
+open Names
+open Constr
+open Libnames
+open Glob_term
+open Constrexpr
+open Constrexpr_ops
+open Util
+open Tok
+open Namegen
+open Decl_kinds
+
+open Pcoq
+open Pcoq.Prim
+open Pcoq.Constr
+
+(* TODO: avoid this redefinition without an extra dep to Notation_ops *)
+let ldots_var = Id.of_string ".."
+
+let constr_kw =
+ [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
+ "end"; "as"; "let"; "if"; "then"; "else"; "return";
+ "Prop"; "Set"; "Type"; ".("; "_"; "..";
+ "`{"; "`("; "{|"; "|}" ]
+
+let _ = List.iter CLexer.add_keyword constr_kw
+
+let mk_cast = function
+ (c,(_,None)) -> c
+ | (c,(_,Some ty)) ->
+ let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
+ in CAst.make ?loc @@ CCast(c, CastConv ty)
+
+let binder_of_name expl { CAst.loc = loc; v = na } =
+ CLocalAssum ([CAst.make ?loc na], Default expl,
+ CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
+
+let binders_of_names l =
+ List.map (binder_of_name Explicit) l
+
+let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr =
+ let ty = match tyc with
+ Some ty -> ty
+ | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
+ (id,ann,bl,ty,body)
+
+let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr =
+ let _ = Option.map (fun { CAst.loc = aloc } ->
+ CErrors.user_err ?loc:aloc
+ ~hdr:"Constr:mk_cofixb"
+ (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
+ let ty = match tyc with
+ Some ty -> ty
+ | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
+ (id,bl,ty,body)
+
+let mk_fix(loc,kw,id,dcls) =
+ if kw then
+ let fb : fix_expr list = List.map mk_fixb dcls in
+ CAst.make ~loc @@ CFix(id,fb)
+ else
+ let fb : cofix_expr list = List.map mk_cofixb dcls in
+ CAst.make ~loc @@ CCoFix(id,fb)
+
+let mk_single_fix (loc,kw,dcl) =
+ let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
+
+let err () = raise Stream.Failure
+
+(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
+(* admissible notation "(x t)" *)
+let lpar_id_coloneq =
+ Gram.Entry.of_parser "test_lpar_id_coloneq"
+ (fun strm ->
+ match stream_nth 0 strm with
+ | KEYWORD "(" ->
+ (match stream_nth 1 strm with
+ | IDENT s ->
+ (match stream_nth 2 strm with
+ | KEYWORD ":=" ->
+ stream_njunk 3 strm;
+ Names.Id.of_string s
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
+let impl_ident_head =
+ Gram.Entry.of_parser "impl_ident_head"
+ (fun strm ->
+ match stream_nth 0 strm with
+ | KEYWORD "{" ->
+ (match stream_nth 1 strm with
+ | IDENT ("wf"|"struct"|"measure") -> err ()
+ | IDENT s ->
+ stream_njunk 2 strm;
+ Names.Id.of_string s
+ | _ -> err ())
+ | _ -> err ())
+
+let name_colon =
+ Gram.Entry.of_parser "name_colon"
+ (fun strm ->
+ match stream_nth 0 strm with
+ | IDENT s ->
+ (match stream_nth 1 strm with
+ | KEYWORD ":" ->
+ stream_njunk 2 strm;
+ Name (Names.Id.of_string s)
+ | _ -> err ())
+ | KEYWORD "_" ->
+ (match stream_nth 1 strm with
+ | KEYWORD ":" ->
+ stream_njunk 2 strm;
+ Anonymous
+ | _ -> err ())
+ | _ -> err ())
+
+let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
+
+}
+
+GRAMMAR EXTEND Gram
+ GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
+ global constr_pattern lconstr_pattern Constr.ident
+ closed_binder open_binders binder binders binders_fixannot
+ record_declaration typeclass_constraint pattern appl_arg;
+ Constr.ident:
+ [ [ id = Prim.ident -> { id } ] ]
+ ;
+ Prim.name:
+ [ [ "_" -> { CAst.make ~loc Anonymous } ] ]
+ ;
+ global:
+ [ [ r = Prim.reference -> { r } ] ]
+ ;
+ constr_pattern:
+ [ [ c = constr -> { c } ] ]
+ ;
+ lconstr_pattern:
+ [ [ c = lconstr -> { c } ] ]
+ ;
+ sort:
+ [ [ "Set" -> { GSet }
+ | "Prop" -> { GProp }
+ | "Type" -> { GType [] }
+ | "Type"; "@{"; u = universe; "}" -> { GType u }
+ ] ]
+ ;
+ sort_family:
+ [ [ "Set" -> { Sorts.InSet }
+ | "Prop" -> { Sorts.InProp }
+ | "Type" -> { Sorts.InType }
+ ] ]
+ ;
+ universe_expr:
+ [ [ id = global; "+"; n = natural -> { Some (id,n) }
+ | id = global -> { Some (id,0) }
+ | "_" -> { None }
+ ] ]
+ ;
+ universe:
+ [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
+ | u = universe_expr -> { [u] }
+ ] ]
+ ;
+ lconstr:
+ [ [ c = operconstr LEVEL "200" -> { c } ] ]
+ ;
+ constr:
+ [ [ c = operconstr LEVEL "8" -> { c }
+ | "@"; f=global; i = instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
+ ;
+ operconstr:
+ [ "200" RIGHTA
+ [ c = binder_constr -> { c } ]
+ | "100" RIGHTA
+ [ c1 = operconstr; "<:"; c2 = binder_constr ->
+ { CAst.make ~loc @@ CCast(c1, CastVM c2) }
+ | c1 = operconstr; "<:"; c2 = SELF ->
+ { CAst.make ~loc @@ CCast(c1, CastVM c2) }
+ | c1 = operconstr; "<<:"; c2 = binder_constr ->
+ { CAst.make ~loc @@ CCast(c1, CastNative c2) }
+ | c1 = operconstr; "<<:"; c2 = SELF ->
+ { CAst.make ~loc @@ CCast(c1, CastNative c2) }
+ | c1 = operconstr; ":";c2 = binder_constr ->
+ { CAst.make ~loc @@ CCast(c1, CastConv c2) }
+ | c1 = operconstr; ":"; c2 = SELF ->
+ { CAst.make ~loc @@ CCast(c1, CastConv c2) }
+ | c1 = operconstr; ":>" ->
+ { CAst.make ~loc @@ CCast(c1, CastCoerce) } ]
+ | "99" RIGHTA [ ]
+ | "90" RIGHTA [ ]
+ | "10" LEFTA
+ [ f=operconstr; args=LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
+ | "@"; f=global; i = instance; args=LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
+ | "@"; lid = pattern_identref; args=LIST1 identref ->
+ { let { CAst.loc = locid; v = id } = lid in
+ let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
+ CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
+ | "9"
+ [ ".."; c = operconstr LEVEL "0"; ".." ->
+ { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ]
+ | "8" [ ]
+ | "1" LEFTA
+ [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
+ { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) }
+ | c=operconstr; ".("; "@"; f=global;
+ args=LIST0 (operconstr LEVEL "9"); ")" ->
+ { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) }
+ | c=operconstr; "%"; key=IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
+ | "0"
+ [ c=atomic_constr -> { c }
+ | c=match_constr -> { c }
+ | "("; c = operconstr LEVEL "200"; ")" ->
+ { (match c.CAst.v with
+ | CPrim (Numeral (n,true)) ->
+ CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
+ | _ -> c) }
+ | "{|"; c = record_declaration; "|}" -> { c }
+ | "{"; c = binder_constr ; "}" ->
+ { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
+ | "`{"; c = operconstr LEVEL "200"; "}" ->
+ { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
+ | "`("; c = operconstr LEVEL "200"; ")" ->
+ { CAst.make ~loc @@ CGeneralization (Explicit, None, c) }
+ ] ]
+ ;
+ record_declaration:
+ [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ]
+ ;
+
+ record_fields:
+ [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs }
+ | f = record_field_declaration -> { [f] }
+ | -> { [] }
+ ] ]
+ ;
+
+ record_field_declaration:
+ [ [ id = global; bl = binders; ":="; c = lconstr ->
+ { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ]
+ ;
+ binder_constr:
+ [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
+ { mkCProdN ~loc bl c }
+ | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
+ { mkCLambdaN ~loc bl c }
+ | "let"; id=name; bl = binders; ty = type_cstr; ":=";
+ c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
+ { let ty,c1 = match ty, c1 with
+ | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
+ | _, _ -> ty, c1 in
+ CAst.make ~loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
+ Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) }
+ | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
+ { let fixp = mk_single_fix fx in
+ let { CAst.loc = li; v = id } = match fixp.CAst.v with
+ CFix(id,_) -> id
+ | CCoFix(id,_) -> id
+ | _ -> assert false in
+ CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) }
+ | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
+ po = return_type;
+ ":="; c1 = operconstr LEVEL "200"; "in";
+ c2 = operconstr LEVEL "200" ->
+ { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
+ | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ "in"; c2 = operconstr LEVEL "200" ->
+ { CAst.make ~loc @@
+ CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) }
+ | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
+ { CAst.make ~loc @@
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
+
+ | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
+ ":="; c1 = operconstr LEVEL "200"; rt = case_type;
+ "in"; c2 = operconstr LEVEL "200" ->
+ { CAst.make ~loc @@
+ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) }
+ | "if"; c=operconstr LEVEL "200"; po = return_type;
+ "then"; b1=operconstr LEVEL "200";
+ "else"; b2=operconstr LEVEL "200" ->
+ { CAst.make ~loc @@ CIf (c, po, b1, b2) }
+ | c=fix_constr -> { c } ] ]
+ ;
+ appl_arg:
+ [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
+ { (c,Some (CAst.make ~loc @@ ExplByName id)) }
+ | c=operconstr LEVEL "9" -> { (c,None) } ] ]
+ ;
+ atomic_constr:
+ [ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) }
+ | s=sort -> { CAst.make ~loc @@ CSort s }
+ | n=INT -> { CAst.make ~loc @@ CPrim (Numeral (n,true)) }
+ | s=string -> { CAst.make ~loc @@ CPrim (String s) }
+ | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
+ | "?"; "["; id=ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) }
+ | "?"; "["; id=pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) }
+ | id=pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
+ ;
+ inst:
+ [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ]
+ ;
+ evar_instance:
+ [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
+ | -> { [] } ] ]
+ ;
+ instance:
+ [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l }
+ | -> { None } ] ]
+ ;
+ universe_level:
+ [ [ "Set" -> { GSet }
+ | "Prop" -> { GProp }
+ | "Type" -> { GType UUnknown }
+ | "_" -> { GType UAnonymous }
+ | id = global -> { GType (UNamed id) }
+ ] ]
+ ;
+ fix_constr:
+ [ [ fx1=single_fix -> { mk_single_fix fx1 }
+ | f=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
+ "for"; id=identref ->
+ { let (_,kw,dcl1) = f in
+ mk_fix(loc,kw,id,dcl1::dcls) }
+ ] ]
+ ;
+ single_fix:
+ [ [ kw=fix_kw; dcl=fix_decl -> { (loc,kw,dcl) } ] ]
+ ;
+ fix_kw:
+ [ [ "fix" -> { true }
+ | "cofix" -> { false } ] ]
+ ;
+ fix_decl:
+ [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
+ c=operconstr LEVEL "200" ->
+ { (id,fst bl,snd bl,c,ty) } ] ]
+ ;
+ match_constr:
+ [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
+ br=branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ]
+ ;
+ case_item:
+ [ [ c=operconstr LEVEL "100";
+ ona = OPT ["as"; id=name -> { id } ];
+ ty = OPT ["in"; t=pattern -> { t } ] ->
+ { (c,ona,ty) } ] ]
+ ;
+ case_type:
+ [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ]
+ ;
+ return_type:
+ [ [ a = OPT [ na = OPT["as"; na=name -> { na } ];
+ ty = case_type -> { (na,ty) } ] ->
+ { match a with
+ | None -> None, None
+ | Some (na,t) -> (na, Some t) }
+ ] ]
+ ;
+ branches:
+ [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ]
+ ;
+ mult_pattern:
+ [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ]
+ ;
+ eqn:
+ [ [ pll = LIST1 mult_pattern SEP "|";
+ "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ]
+ ;
+ record_pattern:
+ [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ]
+ ;
+ record_patterns:
+ [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
+ | p = record_pattern; ";" -> { [p] }
+ | p = record_pattern-> { [p] }
+ | -> { [] }
+ ] ]
+ ;
+ pattern:
+ [ "200" RIGHTA [ ]
+ | "100" RIGHTA
+ [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ]
+ | "99" RIGHTA [ ]
+ | "90" RIGHTA [ ]
+ | "10" LEFTA
+ [ p = pattern; "as"; na = name ->
+ { CAst.make ~loc @@ CPatAlias (p, na) }
+ | p = pattern; lp = LIST1 NEXT -> { mkAppPattern ~loc p lp }
+ | "@"; r = Prim.reference; lp = LIST0 NEXT ->
+ { CAst.make ~loc @@ CPatCstr (r, Some lp, []) } ]
+ | "1" LEFTA
+ [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ]
+ | "0"
+ [ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) }
+ | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat }
+ | "_" -> { CAst.make ~loc @@ CPatAtom None }
+ | "("; p = pattern LEVEL "200"; ")" ->
+ { (match p.CAst.v with
+ | CPatPrim (Numeral (n,true)) ->
+ CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+ | _ -> p) }
+ | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
+ { let p =
+ match p with
+ | { CAst.v = CPatPrim (Numeral (n,true)) } ->
+ CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+ | _ -> p
+ in
+ CAst.make ~loc @@ CPatCast (p, ty) }
+ | n = INT -> { CAst.make ~loc @@ CPatPrim (Numeral (n,true)) }
+ | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
+ ;
+ impl_ident_tail:
+ [ [ "}" -> { binder_of_name Implicit }
+ | nal=LIST1 name; ":"; c=lconstr; "}" ->
+ { (fun na -> CLocalAssum (na::nal,Default Implicit,c)) }
+ | nal=LIST1 name; "}" ->
+ { (fun na -> CLocalAssum (na::nal,Default Implicit,
+ CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some loc)) @@
+ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))) }
+ | ":"; c=lconstr; "}" ->
+ { (fun na -> CLocalAssum ([na],Default Implicit,c)) }
+ ] ]
+ ;
+ fixannot:
+ [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) }
+ | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) }
+ | "{"; IDENT "measure"; m=constr; id=OPT identref;
+ rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) }
+ ] ]
+ ;
+ impl_name_head:
+ [ [ id = impl_ident_head -> { CAst.make ~loc @@ Name id } ] ]
+ ;
+ binders_fixannot:
+ [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
+ { (assum na :: fst bl), snd bl }
+ | f = fixannot -> { [], f }
+ | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
+ | -> { [], (None, CStructRec) }
+ ] ]
+ ;
+ open_binders:
+ (* Same as binders but parentheses around a closed binder are optional if
+ the latter is unique *)
+ [ [
+ id = name; idl = LIST0 name; ":"; c = lconstr ->
+ { [CLocalAssum (id::idl,Default Explicit,c)]
+ (* binders factorized with open binder *) }
+ | id = name; idl = LIST0 name; bl = binders ->
+ { binders_of_names (id::idl) @ bl }
+ | id1 = name; ".."; id2 = name ->
+ { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2],
+ Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+ | bl = closed_binder; bl' = binders ->
+ { bl@bl' }
+ ] ]
+ ;
+ binders:
+ [ [ l = LIST0 binder -> { List.flatten l } ] ]
+ ;
+ binder:
+ [ [ id = name -> { [CLocalAssum ([id],Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+ | bl = closed_binder -> { bl } ] ]
+ ;
+ closed_binder:
+ [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+ { [CLocalAssum (id::idl,Default Explicit,c)] }
+ | "("; id=name; ":"; c=lconstr; ")" ->
+ { [CLocalAssum ([id],Default Explicit,c)] }
+ | "("; id=name; ":="; c=lconstr; ")" ->
+ { (match c.CAst.v with
+ | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)]
+ | _ -> [CLocalDef (id,c,None)]) }
+ | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+ { [CLocalDef (id,c,Some t)] }
+ | "{"; id=name; "}" ->
+ { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+ | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+ { [CLocalAssum (id::idl,Default Implicit,c)] }
+ | "{"; id=name; ":"; c=lconstr; "}" ->
+ { [CLocalAssum ([id],Default Implicit,c)] }
+ | "{"; id=name; idl=LIST1 name; "}" ->
+ { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+ | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
+ { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc }
+ | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
+ { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc }
+ | "'"; p = pattern LEVEL "0" ->
+ { let (p, ty) =
+ match p.CAst.v with
+ | CPatCast (p, ty) -> (p, Some ty)
+ | _ -> (p, None)
+ in
+ [CLocalPattern (CAst.make ~loc (p, ty))] }
+ ] ]
+ ;
+ typeclass_constraint:
+ [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c }
+ | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+ { id, expl, c }
+ | iid=name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" ->
+ { (CAst.make ~loc iid), expl, c }
+ | c = operconstr LEVEL "200" ->
+ { (CAst.make ~loc Anonymous), false, c }
+ ] ]
+ ;
+
+ type_cstr:
+ [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ]
+ ;
+ END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 23:03:51 +0000