diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 115 |
1 files changed, 77 insertions, 38 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cf7f6af2..1f9f57f6 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -46,7 +46,7 @@ let record_field = Gram.entry_create "vernac:record_field" let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" -let section_subset_descr = Gram.entry_create "vernac:section_subset_descr" +let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" let command_entry = ref noedit_mode let set_command_entry e = command_entry := e @@ -71,6 +71,17 @@ let make_bullet s = | '*' -> Star n | _ -> assert false +(* Hack to parse "[ id" without dropping [ *) +let test_bracket_ident = + Gram.Entry.of_parser "test_bracket_ident" + (fun strm -> + match get_tok (stream_nth 0 strm) with + | KEYWORD "[" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> () + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + let default_command_entry = Gram.Entry.of_parser "command_entry" (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) @@ -79,6 +90,7 @@ GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; l = vernac_list -> VernacTime l + | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v @@ -95,12 +107,12 @@ GEXTEND Gram | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) - | v = vernac_poly -> v ] + | v = vernac_poly -> v ] ] ; - vernac_poly: + vernac_poly: [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) - | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) | v = vernac_aux -> v ] ] ; @@ -128,7 +140,7 @@ GEXTEND Gram selector: [ [ n=natural; ":" -> SelectNth n - | "["; id = ident; "]"; ":" -> SelectId id + | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id | IDENT "all" ; ":" -> SelectAll | IDENT "par" ; ":" -> SelectAllParallel ] ] ; @@ -145,7 +157,7 @@ GEXTEND Gram ] ] ; - subgoal_command: + subgoal_command: [ [ c = query_command; "." -> begin function | Some (SelectNth g) -> c (Some g) @@ -184,9 +196,9 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; + [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr; l = LIST0 - [ "with"; id = identref; bl = binders; ":"; c = lconstr -> + [ "with"; id = pidentref; bl = binders; ":"; c = lconstr -> (Some id,(bl,c,None)) ] -> VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> @@ -194,10 +206,10 @@ GEXTEND Gram | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; VernacAssumption (stre, nl, bl) - | d = def_token; id = identref; b = def_body -> + | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) | IDENT "Let"; id = identref; b = def_body -> - VernacDefinition ((Some Discharge, Definition), id, b) + VernacDefinition ((Some Discharge, Definition), (id, None), b) (* Gallina inductive declarations *) | priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -248,13 +260,17 @@ GEXTEND Gram [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) | IDENT "Variables" -> (Some Discharge, Definitional) | IDENT "Axioms" -> (None, Logical) - | IDENT "Parameters" -> (None, Definitional) ] ] + | IDENT "Parameters" -> (None, Definitional) + | IDENT "Conjectures" -> (None, Conjectural) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) | IDENT "Inline" -> DefaultInline | -> NoInline] ] ; + pidentref: + [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] + ; univ_constraint: [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; r = identref -> (l, ord, r) ] ] @@ -299,7 +315,7 @@ GEXTEND Gram | -> RecordDecl (None, []) ] ] ; inductive_definition: - [ [ oc = opt_coercion; id = identref; indpar = binders; + [ [ oc = opt_coercion; id = pidentref; indpar = binders; c = OPT [ ":"; c = lconstr -> c ]; lc=opt_constructors_or_fields; ntn = decl_notation -> (((oc,id),indpar,c,lc),ntn) ] ] @@ -309,9 +325,9 @@ GEXTEND Gram | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> Constructors ((c id)::l) | id = identref ; c = constructor_type -> Constructors [ c id ] - | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> + | cstr = identref; "{"; fs = record_fields; "}" -> RecordDecl (Some cstr,fs) - | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) + | "{";fs = record_fields; "}" -> RecordDecl (None,fs) | -> Constructors [] ] ] ; (* @@ -325,14 +341,14 @@ GEXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = identref; + [ [ id = pidentref; bl = binders_fixannot; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = identref; bl = binders; ty = type_cstr; + [ [ id = pidentref; bl = binders; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; @@ -373,6 +389,13 @@ GEXTEND Gram [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; ntn = decl_notation -> (bd,pri),ntn ] ] ; + record_fields: + [ [ f = record_field; ";"; fs = record_fields -> f :: fs + | f = record_field; ";" -> [f] + | f = record_field -> [f] + | -> [] + ] ] + ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t)) @@ -397,7 +420,7 @@ GEXTEND Gram [ [ "("; a = simple_assum_coe; ")" -> a ] ] ; simple_assum_coe: - [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> + [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr -> (not (Option.is_empty oc),(idl,c)) ] ] ; @@ -424,20 +447,24 @@ GEXTEND Gram ; END -let only_identrefs = - Gram.Entry.of_parser "test_only_identrefs" +let only_starredidentrefs = + Gram.Entry.of_parser "test_only_starredidentrefs" (fun strm -> let rec aux n = match get_tok (Util.stream_nth n strm) with | KEYWORD "." -> () | KEYWORD ")" -> () - | IDENT _ -> aux (n+1) + | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) | _ -> raise Stream.Failure in aux 0) +let starredidentreflist_to_expr l = + match l with + | [] -> SsEmpty + | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x (* Modules and Sections *) GEXTEND Gram - GLOBAL: gallina_ext module_expr module_type section_subset_descr; + GLOBAL: gallina_ext module_expr module_type section_subset_expr; gallina_ext: [ [ (* Interactive module declaration *) @@ -460,7 +487,7 @@ GEXTEND Gram | IDENT "End"; id = identref -> VernacEndSegment id (* Naming a set of section hyps *) - | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr -> + | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr -> VernacNameSectionHypSet (id, expr) (* Requiring an already compiled module *) @@ -551,22 +578,32 @@ GEXTEND Gram CMwith (!@loc,mty,decl) ] ] ; - section_subset_descr: - [ [ IDENT "All" -> SsAll - | "Type" -> SsType - | only_identrefs; l = LIST0 identref -> SsExpr (SsSet l) - | e = section_subset_expr -> SsExpr e ] ] - ; + (* Proof using *) section_subset_expr: + [ [ only_starredidentrefs; l = LIST0 starredidentref -> + starredidentreflist_to_expr l + | e = ssexpr -> e ]] + ; + starredidentref: + [ [ i = identref -> SsSingl i + | i = identref; "*" -> SsFwdClose(SsSingl i) + | "Type" -> SsSingl (!@loc, Id.of_string "Type") + | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]] + ; + ssexpr: [ "35" - [ "-"; e = section_subset_expr -> SsCompl e ] + [ "-"; e = ssexpr -> SsCompl e ] | "50" - [ e1 = section_subset_expr; "-"; e2 = section_subset_expr->SsSubstr(e1,e2) - | e1 = section_subset_expr; "+"; e2 = section_subset_expr->SsUnion(e1,e2)] + [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2) + | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)] | "0" - [ i = identref -> SsSet [i] - | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l - | "("; e = section_subset_expr; ")"-> e ] ] + [ i = starredidentref -> i + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> + starredidentreflist_to_expr l + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> + SsFwdClose(starredidentreflist_to_expr l) + | "("; e = ssexpr; ")"-> e + | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ] ; END @@ -592,15 +629,15 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Some Global,CanonicalStructure),(Loc.ghost,s),d) + ((Some Global,CanonicalStructure),((Loc.ghost,s),None),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((None,Coercion),(Loc.ghost,s),d) + VernacDefinition ((None,Coercion),((Loc.ghost,s),None),d) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d) + VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.ghost,s),None),d) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (true, f, s, t) @@ -1041,7 +1078,9 @@ GEXTEND Gram VernacOpenCloseScope (local,(false,sc)) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc,key) + VernacDelimiters (sc, Some key) + | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> + VernacDelimiters (sc, None) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 smart_global -> VernacBindScope (sc,refl) |