From f99f60902d7492902110fb091c52e58e1ed9cd32 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 19 Oct 2017 18:17:33 +0200 Subject: Use a homebrew parser to replace the GEXTEND extension points of Camlp5. The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one. --- parsing/extend.ml | 2 +- parsing/pcoq.ml | 11 ++++++++++- parsing/pcoq.mli | 3 +++ 3 files changed, 14 insertions(+), 2 deletions(-) (limited to 'parsing') diff --git a/parsing/extend.ml b/parsing/extend.ml index 6805a96edc..f57e32c884 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -101,7 +101,7 @@ type ('self, 'a) symbol = | Aself : ('self, 'self) symbol | Anext : ('self, 'self) symbol | Aentry : 'a entry -> ('self, 'a) symbol -| Aentryl : 'a entry * int -> ('self, 'a) symbol +| Aentryl : 'a entry * string -> ('self, 'a) symbol | Arules : 'a rules list -> ('self, 'a) symbol and ('self, _, 'r) rule = diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 6fdd9ea9b9..171276a700 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -17,9 +17,17 @@ let curry f x y = f (x, y) let uncurry f (x,y) = f x y (** Location Utils *) +let ploc_file_of_coq_file = function +| Loc.ToplevelInput -> "" +| Loc.InFile f -> f + let coq_file_of_ploc_file s = if s = "" then Loc.ToplevelInput else Loc.InFile s +let of_coqloc loc = + let open Loc in + Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) "" + let to_coqloc loc = { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); Loc.line_nb = Ploc.line_nb loc; @@ -236,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function | Aentry e -> Symbols.snterm (G.Entry.obj e) | Aentryl (e, n) -> - Symbols.snterml (G.Entry.obj e, string_of_int n) + Symbols.snterml (G.Entry.obj e, n) | Arules rs -> G.srules' (List.map symbol_of_rules rs) @@ -328,6 +336,7 @@ module Gram = I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil + let safe_extend e ext = grammar_extend e None ext end (** Remove extensions diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f959bd80c0..48604e1885 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -80,6 +80,8 @@ module type S = (* Get comment parsing information from the Lexer *) val comment_state : coq_parsable -> ((int * int) * string) list + val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit + (* Apparently not used *) val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a @@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) +val of_coqloc : Loc.t -> Ploc.t val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t -- cgit v1.2.3 From aaad965a84d97fdd64367138e692ebd49321ccd9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Oct 2017 11:22:23 +0200 Subject: Port g_prim to the homebrew GEXTEND parser. --- parsing/g_prim.ml4 | 122 -------------------------------------------------- parsing/g_prim.mlg | 127 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 127 insertions(+), 122 deletions(-) delete mode 100644 parsing/g_prim.ml4 create mode 100644 parsing/g_prim.mlg (limited to 'parsing') diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 deleted file mode 100644 index 91dce27fe1..0000000000 --- a/parsing/g_prim.ml4 +++ /dev/null @@ -1,122 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 1024 * 2048 then raise Exit; - n - with Failure _ | Exit -> - CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") - -GEXTEND Gram - GLOBAL: - bigint natural integer identref name ident var preident - fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation smart_global; - preident: - [ [ s = IDENT -> s ] ] - ; - ident: - [ [ s = IDENT -> Id.of_string s ] ] - ; - pattern_ident: - [ [ LEFTQMARK; id = ident -> id ] ] - ; - pattern_identref: - [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ] - ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> CAst.make ~loc:!@loc id ] ] - ; - identref: - [ [ id = ident -> CAst.make ~loc:!@loc id ] ] - ; - field: - [ [ s = FIELD -> Id.of_string s ] ] - ; - fields: - [ [ id = field; (l,id') = fields -> (l@[id],id') - | id = field -> ([],id) - ] ] - ; - fullyqualid: - [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l) - | id = ident -> CAst.make ~loc:!@loc [id] - ] ] - ; - basequalid: - [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id' - | id = ident -> qualid_of_ident ~loc:!@loc id - ] ] - ; - name: - [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous - | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ] - ; - reference: - [ [ id = ident; (l,id') = fields -> - local_make_qualid !@loc (l@[id]) id' - | id = ident -> local_make_qualid !@loc [] id - ] ] - ; - by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ] - ; - smart_global: - [ [ c = reference -> CAst.make ~loc:!@loc @@ Constrexpr.AN c - | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ] - ; - qualid: - [ [ qid = basequalid -> qid ] ] - ; - ne_string: - [ [ s = STRING -> - if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s - ] ] - ; - ne_lstring: - [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ] - ; - dirpath: - [ [ id = ident; l = LIST0 field -> - DirPath.make (List.rev (id::l)) ] ] - ; - string: - [ [ s = STRING -> s ] ] - ; - lstring: - [ [ s = string -> (CAst.make ~loc:!@loc s) ] ] - ; - integer: - [ [ i = INT -> my_int_of_string (!@loc) i - | "-"; i = INT -> - my_int_of_string (!@loc) i ] ] - ; - natural: - [ [ i = INT -> my_int_of_string (!@loc) i ] ] - ; - bigint: (* Negative numbers are dealt with elsewhere *) - [ [ i = INT -> i ] ] - ; -END diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg new file mode 100644 index 0000000000..774db97f2c --- /dev/null +++ b/parsing/g_prim.mlg @@ -0,0 +1,127 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 1024 * 2048 then raise Exit; + n + with Failure _ | Exit -> + CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") + +} + +GRAMMAR EXTEND Gram + GLOBAL: + bigint natural integer identref name ident var preident + fullyqualid qualid reference dirpath ne_lstring + ne_string string lstring pattern_ident pattern_identref by_notation smart_global; + preident: + [ [ s = IDENT -> { s } ] ] + ; + ident: + [ [ s = IDENT -> { Id.of_string s } ] ] + ; + pattern_ident: + [ [ LEFTQMARK; id = ident -> { id } ] ] + ; + pattern_identref: + [ [ id = pattern_ident -> { CAst.make ~loc id } ] ] + ; + var: (* as identref, but interpret as a term identifier in ltac *) + [ [ id = ident -> { CAst.make ~loc id } ] ] + ; + identref: + [ [ id = ident -> { CAst.make ~loc id } ] ] + ; + field: + [ [ s = FIELD -> { Id.of_string s } ] ] + ; + fields: + [ [ id = field; f = fields -> { let (l,id') = f in (l@[id],id') } + | id = field -> { ([],id) } + ] ] + ; + fullyqualid: + [ [ id = ident; f=fields -> { let (l,id') = f in CAst.make ~loc @@ id::List.rev (id'::l) } + | id = ident -> { CAst.make ~loc [id] } + ] ] + ; + basequalid: + [ [ id = ident; f=fields -> { let (l,id') = f in local_make_qualid loc (l@[id]) id' } + | id = ident -> { qualid_of_ident ~loc id } + ] ] + ; + name: + [ [ IDENT "_" -> { CAst.make ~loc Anonymous } + | id = ident -> { CAst.make ~loc @@ Name id } ] ] + ; + reference: + [ [ id = ident; f = fields -> { + let (l,id') = f in + local_make_qualid loc (l@[id]) id' } + | id = ident -> { local_make_qualid loc [] id } + ] ] + ; + by_notation: + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ] + ; + smart_global: + [ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c } + | ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ] + ; + qualid: + [ [ qid = basequalid -> { qid } ] ] + ; + ne_string: + [ [ s = STRING -> + { if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s } + ] ] + ; + ne_lstring: + [ [ s = ne_string -> { CAst.make ~loc s } ] ] + ; + dirpath: + [ [ id = ident; l = LIST0 field -> + { DirPath.make (List.rev (id::l)) } ] ] + ; + string: + [ [ s = STRING -> { s } ] ] + ; + lstring: + [ [ s = string -> { CAst.make ~loc s } ] ] + ; + integer: + [ [ i = INT -> { my_int_of_string loc i } + | "-"; i = INT -> { - my_int_of_string loc i } ] ] + ; + natural: + [ [ i = INT -> { my_int_of_string loc i } ] ] + ; + bigint: (* Negative numbers are dealt with elsewhere *) + [ [ i = INT -> { i } ] ] + ; +END -- cgit v1.2.3 From a93fd0422ecb67f052aec6a4fe9b512ccbdeaf24 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Oct 2017 13:26:52 +0200 Subject: Port g_constr to the homebrew GEXTEND parser. --- parsing/g_constr.ml4 | 521 -------------------------------------------------- parsing/g_constr.mlg | 526 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 526 insertions(+), 521 deletions(-) delete mode 100644 parsing/g_constr.ml4 create mode 100644 parsing/g_constr.mlg (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 deleted file mode 100644 index 1fa26b4556..0000000000 --- a/parsing/g_constr.ml4 +++ /dev/null @@ -1,521 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 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 - -GEXTEND 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:!@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:!@loc @@ CAppExpl((None,f,i),[]) ] ] - ; - operconstr: - [ "200" RIGHTA - [ c = binder_constr -> c ] - | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) - | c1 = operconstr; "<:"; c2 = SELF -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) - | c1 = operconstr; "<<:"; c2 = binder_constr -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) - | c1 = operconstr; "<<:"; c2 = SELF -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) - | c1 = operconstr; ":";c2 = binder_constr -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) - | c1 = operconstr; ":"; c2 = SELF -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) - | c1 = operconstr; ":>" -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastCoerce) ] - | "99" RIGHTA [ ] - | "90" RIGHTA [ ] - | "10" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args) - | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@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:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] - | "9" - [ ".."; c = operconstr LEVEL "0"; ".." -> - CAst.make ~loc:!@loc @@ CAppExpl ((None, (qualid_of_ident ~loc:!@loc ldots_var), None),[c]) ] - | "8" [ ] - | "1" LEFTA - [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - CAst.make ~loc:(!@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:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) - | c=operconstr; "%"; key=IDENT -> CAst.make ~loc:(!@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:(!@loc) @@ CNotation("( _ )",([c],[],[],[])) - | _ -> c) - | "{|"; c = record_declaration; "|}" -> c - | "{"; c = binder_constr ; "}" -> - CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[])) - | "`{"; c = operconstr LEVEL "200"; "}" -> - CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) - | "`("; c = operconstr LEVEL "200"; ")" -> - CAst.make ~loc:(!@loc) @@ CGeneralization (Explicit, None, c) - ] ] - ; - record_declaration: - [ [ fs = record_fields -> CAst.make ~loc:(!@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, mkCLambdaN ~loc:!@loc bl c) ] ] - ; - binder_constr: - [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> - mkCProdN ~loc:!@loc bl c - | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> - mkCLambdaN ~loc:!@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:!@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:!@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:!@loc @@ CLetTuple (lb,po,c1,c2) - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; - "in"; c2 = operconstr LEVEL "200" -> - CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc:!@loc ([[p]], c2)]) - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; - rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc:!@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:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc:!@loc ([[p]], c2)]) - | "if"; c=operconstr LEVEL "200"; po = return_type; - "then"; b1=operconstr LEVEL "200"; - "else"; b2=operconstr LEVEL "200" -> - CAst.make ~loc:(!@loc) @@ CIf (c, po, b1, b2) - | c=fix_constr -> c ] ] - ; - appl_arg: - [ [ id = lpar_id_coloneq; c=lconstr; ")" -> - (c,Some (CAst.make ~loc:!@loc @@ ExplByName id)) - | c=operconstr LEVEL "9" -> (c,None) ] ] - ; - atomic_constr: - [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i) - | s=sort -> CAst.make ~loc:!@loc @@ CSort s - | n=INT -> CAst.make ~loc:!@loc @@ CPrim (Numeral (n,true)) - | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s) - | "_" -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) - | "?"; "["; id=ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) - | "?"; "["; id=pattern_ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroFresh id, None) - | id=pattern_ident; inst = evar_instance -> CAst.make ~loc:!@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 - | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; - "for"; id=identref -> - 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:!@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:!@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:!@loc @@ CPatOr (p::pl) ] - | "99" RIGHTA [ ] - | "90" RIGHTA [ ] - | "10" LEFTA - [ p = pattern; "as"; na = name -> - CAst.make ~loc:!@loc @@ CPatAlias (p, na) - | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp - | "@"; r = Prim.reference; lp = LIST0 NEXT -> - CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] - | "1" LEFTA - [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ] - | "0" - [ r = Prim.reference -> CAst.make ~loc:!@loc @@ CPatAtom (Some r) - | "{|"; pat = record_patterns; "|}" -> CAst.make ~loc:!@loc @@ CPatRecord pat - | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None - | "("; p = pattern LEVEL "200"; ")" -> - (match p.CAst.v with - | CPatPrim (Numeral (n,true)) -> - CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) - | _ -> p) - | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> - let p = - match p with - | { CAst.v = CPatPrim (Numeral (n,true)) } -> - CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) - | _ -> p - in - CAst.make ~loc:!@loc @@ CPatCast (p, ty) - | n = INT -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (n,true)) - | s = string -> CAst.make ~loc:!@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:!@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 *) - [ [ (* open binder *) - 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:!@loc (Name ldots_var));id2], - Default Explicit, CAst.make ~loc:!@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:!@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:!@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:!@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:!@loc (p, ty))] - ] ] - ; - typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (CAst.make ~loc:!@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:!@loc iid), expl, c - | c = operconstr LEVEL "200" -> - (CAst.make ~loc:!@loc Anonymous), false, c - ] ] - ; - - type_cstr: - [ [ c=OPT [":"; c=lconstr -> c] -> Loc.tag ~loc:!@loc c ] ] - ; - END;; diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg new file mode 100644 index 0000000000..b2913d5d4f --- /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 *) +(* 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("( _ )",([c],[],[],[])) + | _ -> c) } + | "{|"; c = record_declaration; "|}" -> { c } + | "{"; c = binder_constr ; "}" -> + { CAst.make ~loc @@ CNotation(("{ _ }"),([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, 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("( _ )",([p],[]),[]) + | _ -> p) } + | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> + { let p = + match p with + | { CAst.v = CPatPrim (Numeral (n,true)) } -> + CAst.make ~loc @@ CPatNotation("( _ )",([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 -- cgit v1.2.3