diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 512 |
1 files changed, 297 insertions, 215 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 75cd7d67..70a8ec55 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,24 +8,23 @@ open Pp open Compat -open Tok +open Errors open Util open Names -open Topconstr +open Constrexpr +open Constrexpr_ops open Extend open Vernacexpr -open Pcoq -open Tactic open Decl_kinds -open Genarg -open Ppextend -open Goptions -open Declaremods +open Misctypes +open Tok (* necessary for camlp4 *) -open Prim -open Constr -open Vernac_ -open Module +open Pcoq +open Pcoq.Tactic +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Vernac_ +open Pcoq.Module let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] let _ = List.iter Lexer.add_keyword vernac_kw @@ -33,7 +32,7 @@ let _ = List.iter Lexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -let check_command = Gram.entry_create "vernac:check_command" +let query_command = Gram.entry_create "vernac:query_command" let tactic_mode = Gram.entry_create "vernac:tactic_command" let noedit_mode = Gram.entry_create "vernac:noedit_command" @@ -47,6 +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 command_entry = ref noedit_mode let set_command_entry e = command_entry := e @@ -63,81 +63,118 @@ let _ = Proof_global.register_proof_mode {Proof_global. reset = set_noedit_mode } +let make_bullet s = + let n = String.length s in + match s.[0] with + | '-' -> Dash n + | '+' -> Plus n + | '*' -> Star n + | _ -> assert false + let default_command_entry = Gram.Entry.of_parser "command_entry" (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) -let no_hook _ _ = () GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST - [ [ IDENT "Time"; v = vernac -> VernacTime v + [ [ IDENT "Time"; l = vernac_list -> VernacTime l | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v - | locality; v = vernac_aux -> v ] ] + + | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) + | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) + + (* Stm backdoor *) + | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument + | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish + | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait + | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag + | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> + VernacStm (Observe (Stateid.of_int (int_of_string id))) + | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) + | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) + + | v = vernac_poly -> v ] + ] + ; + vernac_poly: + [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v) + | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + | v = vernac_aux -> v ] + ] ; vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) - [ [ g = gallina; "." -> g + [ [ IDENT "Program"; g = gallina; "." -> VernacProgram g + | IDENT "Program"; g = gallina_ext; "." -> VernacProgram g + | g = gallina; "." -> g | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c - | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l | c = subprf -> c ] ] ; + vernac_list: + [ [ c = located_vernac -> [c] ] ] + ; vernac_aux: LAST [ [ prfcom = default_command_entry -> prfcom ] ] ; - locality: - [ [ IDENT "Local" -> locality_flag := Some (loc,true) - | IDENT "Global" -> locality_flag := Some (loc,false) - | -> locality_flag := None ] ] - ; noedit_mode: [ [ c = subgoal_command -> c None] ] ; + + selector: + [ [ n=natural; ":" -> SelectNth n + | "["; id = ident; "]"; ":" -> SelectId id + | IDENT "all" ; ":" -> SelectAll + | IDENT "par" ; ":" -> SelectAllParallel ] ] + ; + tactic_mode: - [ [ gln = OPT[n=natural; ":" -> n]; + [ [ gln = OPT selector; tac = subgoal_command -> tac gln ] ] ; subprf: - [ [ - "-" -> VernacBullet Dash - | "*" -> VernacBullet Star - | "+" -> VernacBullet Plus + [ [ s = BULLET -> VernacBullet (make_bullet s) | "{" -> VernacSubproof None | "}" -> VernacEndSubproof ] ] ; - - subgoal_command: - [ [ c = check_command; "." -> fun g -> c g - | tac = Tactic.tactic; + [ [ c = query_command; "." -> + begin function + | Some (SelectNth g) -> c (Some g) + | None -> c None + | _ -> + VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) + end + | info = OPT [IDENT "Info";n=natural -> n]; + tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] -> - (fun g -> - let g = Option.default 1 g in - VernacSolve(g,tac,use_dft_tac)) ] ] + (fun g -> + let g = Option.default (Proof_global.get_default_goal_selector ()) g in + VernacSolve(g,info,tac,use_dft_tac)) ] ] ; located_vernac: - [ [ v = vernac -> loc, v ] ] + [ [ v = vernac -> !@loc, v ] ] ; END let test_plurial_form = function | [(_,([_],_))] -> Flags.if_verbose msg_warning - (str "Keywords Variables/Hypotheses/Parameters expect more than one assumption") + (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") | _ -> () let test_plurial_form_types = function | [([_],_)] -> Flags.if_verbose msg_warning - (str "Keywords Implicit Types expect more than one type") + (strbrk "Keywords Implicit Types expect more than one type") | _ -> () (* Gallina declarations *) @@ -150,39 +187,42 @@ GEXTEND Gram [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr; l = LIST0 [ "with"; id = identref; bl = binders; ":"; c = lconstr -> - (Some id,(bl,c,None)) ] -> - VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook) + (Some id,(bl,c,None)) ] -> + VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; VernacAssumption (stre, nl, bl) - | (f,d) = def_token; id = identref; b = def_body -> - VernacDefinition (d, id, b, f) + | d = def_token; id = identref; b = def_body -> + VernacDefinition (d, id, b) + | IDENT "Let"; id = identref; b = def_body -> + VernacDefinition ((Some Discharge, Definition), id, b) (* Gallina inductive declarations *) - | f = finite_token; + | priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (f,false,indl) + VernacInductive (priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint recs + VernacFixpoint (None, recs) + | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (Some Discharge, recs) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint corecs + VernacCoFixpoint (None, corecs) + | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; - l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] - ; - gallina_ext: - [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; - ps = binders; - s = OPT [ ":"; s = lconstr -> s ]; - cfs = [ ":="; l = constructor_list_or_record_decl -> l - | -> RecordDecl (None, []) ] -> - let (recf,indf) = b in - VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]]) + l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) + | IDENT "Register"; IDENT "Inline"; id = identref -> + VernacRegister(id, RegisterInline) + | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l + | IDENT "Universes"; l = LIST1 identref -> VernacUniverse l + | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l ] ] ; + thm_token: [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma @@ -193,50 +233,48 @@ GEXTEND Gram | IDENT "Property" -> Property ] ] ; def_token: - [ [ "Definition" -> - no_hook, (Global, Definition) - | IDENT "Let" -> - no_hook, (Local, Definition) - | IDENT "Example" -> - no_hook, (Global, Example) - | IDENT "SubClass" -> - Class.add_subclass_hook, (use_locality_exp (), SubClass) ] ] + [ [ "Definition" -> (None, Definition) + | IDENT "Example" -> (None, Example) + | IDENT "SubClass" -> (None, SubClass) ] ] ; assumption_token: - [ [ "Hypothesis" -> (Local, Logical) - | "Variable" -> (Local, Definitional) - | "Axiom" -> (Global, Logical) - | "Parameter" -> (Global, Definitional) - | IDENT "Conjecture" -> (Global, Conjectural) ] ] + [ [ "Hypothesis" -> (Some Discharge, Logical) + | "Variable" -> (Some Discharge, Definitional) + | "Axiom" -> (None, Logical) + | "Parameter" -> (None, Definitional) + | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Local, Logical) - | IDENT "Variables" -> (Local, Definitional) - | IDENT "Axioms" -> (Global, Logical) - | IDENT "Parameters" -> (Global, Definitional) ] ] + [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) + | IDENT "Variables" -> (Some Discharge, Definitional) + | IDENT "Axioms" -> (None, Logical) + | IDENT "Parameters" -> (None, Definitional) ] ] ; inline: - [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i) - | IDENT "Inline" -> Some (Flags.get_inline_level()) - | -> None] ] + [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) + | IDENT "Inline" -> DefaultInline + | -> NoInline] ] + ; + univ_constraint: + [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = identref -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) - | "CoInductive" -> (CoInductive,CoFinite) ] ] - ; - infer_token: - [ [ IDENT "Infer" -> true | -> false ] ] - ; - record_token: - [ [ IDENT "Record" -> (Record,BiFinite) + | "CoInductive" -> (CoInductive,CoFinite) + | "Variant" -> (Variant,BiFinite) + | IDENT "Record" -> (Record,BiFinite) | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; + private_token: + [ [ IDENT "Private" -> true | -> false ] ] + ; (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -256,10 +294,14 @@ GEXTEND Gram | -> [] ] ] ; (* Inductives and records *) + opt_constructors_or_fields: + [ [ ":="; lc = constructor_list_or_record_decl -> lc + | -> RecordDecl (None, []) ] ] + ; inductive_definition: - [ [ id = identref; oc = opt_coercion; indpar = binders; + [ [ oc = opt_coercion; id = identref; indpar = binders; c = OPT [ ":"; c = lconstr -> c ]; - ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> + lc=opt_constructors_or_fields; ntn = decl_notation -> (((oc,id),indpar,c,lc),ntn) ] ] ; constructor_list_or_record_decl: @@ -296,7 +338,7 @@ GEXTEND Gram ; type_cstr: [ [ ":"; c=lconstr -> c - | -> CHole (loc, None) ] ] + | -> CHole (!@loc, None, Misctypes.IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: @@ -333,19 +375,19 @@ GEXTEND Gram ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t)) + t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t)) | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> fun id -> - (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) + (oc,DefExpr (id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with - | CCast(_,b, Glob_term.CastConv (_, t)) -> - (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t))) + | CCast(_,b, (CastConv t|CastVM t|CastNative t)) -> + (None,DefExpr(id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t))) | _ -> - (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ] + (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ] ; record_binder: - [ [ id = name -> (None,AssumExpr(id,CHole (loc, None))) + [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None, Misctypes.IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: @@ -356,15 +398,15 @@ GEXTEND Gram ; simple_assum_coe: [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> - (oc <> None,(idl,c)) ] ] + (not (Option.is_empty oc),(idl,c)) ] ] ; constructor_type: [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> - fun l id -> (coe <> None,(id,mkCProdN loc l c)) + fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c)) | -> - fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ] + fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None, Misctypes.IntroAnonymous, None)))) ] -> t l ]] ; @@ -382,10 +424,20 @@ GEXTEND Gram ; END +let only_identrefs = + Gram.Entry.of_parser "test_only_identrefs" + (fun strm -> + let rec aux n = + match get_tok (Util.stream_nth n strm) with + | KEYWORD "." -> () + | KEYWORD ")" -> () + | IDENT _ -> aux (n+1) + | _ -> raise Stream.Failure in + aux 0) (* Modules and Sections *) GEXTEND Gram - GLOBAL: gallina_ext module_expr module_type; + GLOBAL: gallina_ext module_expr module_type section_subset_descr; gallina_ext: [ [ (* Interactive module declaration *) @@ -407,18 +459,24 @@ GEXTEND Gram (* This end a Section a Module or a Module Type *) | IDENT "End"; id = identref -> VernacEndSegment id + (* Naming a set of section hyps *) + | IDENT "Collection"; id = identref; ":="; expr = section_subset_descr -> + VernacNameSectionHypSet (id, expr) + (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; qidl = LIST1 global -> - VernacRequire (export, None, qidl) - | IDENT "Require"; export = export_token; filename = ne_string -> - VernacRequireFrom (export, None, filename) + VernacRequire (export, qidl) + | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token + ; qidl = LIST1 global -> + let qidl = List.map (Libnames.join_reference ns) qidl in + VernacRequire (export, qidl) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> Flags.if_verbose - msg_warning (str "Include Type is deprecated; use Include instead"); + msg_warning (strbrk "Include Type is deprecated; use Include instead"); VernacInclude(e::l) ] ] ; export_token: @@ -451,32 +509,19 @@ GEXTEND Gram | -> [] ] ] ; functor_app_annot: - [ [ IDENT "inline"; "at"; IDENT "level"; i = INT -> - [InlineAt (int_of_string i)], [] - | IDENT "no"; IDENT "inline" -> [NoInline], [] - | IDENT "scope"; sc1 = IDENT; IDENT "to"; sc2 = IDENT -> [], [sc1,sc2] - ] ] - ; - functor_app_annots: - [ [ "["; l = LIST1 functor_app_annot SEP ","; "]" -> - let inl,scs = List.split l in - let inl = match List.concat inl with - | [] -> DefaultInline - | [inl] -> inl - | _ -> error "Functor application with redundant inline annotations" - in { ann_inline = inl; ann_scope_subst = List.concat scs } - | -> { ann_inline = DefaultInline; ann_scope_subst = [] } + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> + InlineAt (int_of_string i) + | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline + | -> DefaultInline ] ] ; module_expr_inl: - [ [ "!"; me = module_expr -> - (me, { ann_inline = NoInline; ann_scope_subst = []}) - | me = module_expr; a = functor_app_annots -> (me,a) ] ] + [ [ "!"; me = module_expr -> (me,NoInline) + | me = module_expr; a = functor_app_annot -> (me,a) ] ] ; module_type_inl: - [ [ "!"; me = module_type -> - (me, { ann_inline = NoInline; ann_scope_subst = []}) - | me = module_type; a = functor_app_annots -> (me,a) ] ] + [ [ "!"; me = module_type -> (me,NoInline) + | me = module_type; a = functor_app_annot -> (me,a) ] ] ; (* Module binder *) module_binder: @@ -486,7 +531,7 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CMapply (loc,me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CMapply (!@loc,me1,me2) ] ] ; module_expr_atom: @@ -502,11 +547,28 @@ GEXTEND Gram module_type: [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMapply (loc,mty,me) + | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me) | mty = module_type; "with"; decl = with_declaration -> - CMwith (loc,mty,decl) + 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 ] ] + ; + section_subset_expr: + [ "35" + [ "-"; e = section_subset_expr -> 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)] + | "0" + [ i = identref -> SsSet [i] + | "("; only_identrefs; l = LIST0 identref; ")"-> SsSet l + | "("; e = section_subset_expr; ")"-> e ] ] + ; END (* Extensions: implicits, coercions, etc. *) @@ -516,12 +578,12 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) IDENT "Transparent"; l = LIST1 smart_global -> - VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l]) + VernacSetOpacity (Conv_oracle.transparent, l) | IDENT "Opaque"; l = LIST1 smart_global -> - VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l]) + VernacSetOpacity (Conv_oracle.Opaque, l) | IDENT "Strategy"; l = - LIST1 [ lev=strategy_level; "["; q=LIST1 smart_global; "]" -> (lev,q)] -> - VernacSetOpacity (use_locality (),l) + LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] -> + VernacSetStrategy l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical (AN qid) @@ -531,50 +593,50 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(dummy_loc,s),d, - (fun _ -> Recordops.declare_canonical_structure)) + ((Some Global,CanonicalStructure),(Loc.ghost,s),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((None,Coercion),(Loc.ghost,s),d) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (enforce_locality_exp true, f, s, t) + VernacIdentityCoercion (true, f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (use_locality_exp (), f, s, t) + VernacIdentityCoercion (false, f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality_exp true, AN qid, s, t) + VernacCoercion (true, AN qid, s, t) | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality_exp true, ByNotation ntn, s, t) + VernacCoercion (true, ByNotation ntn, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality_exp (), AN qid, s, t) + VernacCoercion (false, AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality_exp (), ByNotation ntn, s, t) + VernacCoercion (false, ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] ; - props = [ ":="; "{"; r = record_declaration; "}" -> Some r | - ":="; c = lconstr -> Some c | -> None ] -> - VernacInstance (false, not (use_section_locality ()), - snd namesup, (fst namesup, expl, t), props, pri) + props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | + ":="; c = lconstr -> Some (false,c) | -> None ] -> + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) - | IDENT "Existing"; IDENT "Instance"; id = global -> - VernacDeclareInstances (not (use_section_locality ()), [id]) - | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global -> - VernacDeclareInstances (not (use_section_locality ()), ids) + | IDENT "Existing"; IDENT "Instance"; id = global; + pri = OPT [ "|"; i = natural -> i ] -> + VernacDeclareInstances ([id], pri) + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; + pri = OPT [ "|"; i = natural -> i ] -> + VernacDeclareInstances (ids, pri) | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is @@ -586,17 +648,17 @@ GEXTEND Gram | "/" -> [`Slash] | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> loc, y) x + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> loc, y) x + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> loc, y) x + | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x | Some _, Some _ -> error "scope declared twice" in List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items ] -> l ] SEP ","; @@ -609,31 +671,30 @@ GEXTEND Gram | [] -> narg, impl in let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in let nargs, rest = List.hd nargs, List.tl nargs in - if List.exists ((<>) nargs) rest then + if List.exists (fun arg -> not (Int.equal arg nargs)) rest then error "All arguments lists must have the same length"; let err_incompat x y = error ("Options \""^x^"\" and \""^y^"\" are incompatible") in - if nargs > 0 && List.mem `SimplNeverUnfold mods then + if nargs > 0 && List.mem `ReductionNeverUnfold mods then err_incompat "simpl never" "/"; - if List.mem `SimplNeverUnfold mods && - List.mem `SimplDontExposeCase mods then + if List.mem `ReductionNeverUnfold mods && + List.mem `ReductionDontExposeCase mods then err_incompat "simpl never" "simpl nomatch"; - VernacArguments (use_section_locality(), qid, impl, nargs, mods) + VernacArguments (qid, impl, nargs, mods) (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - Flags.if_verbose - msg_warning (str "Arguments Scope is deprecated; use Arguments instead"); - VernacArgumentsScope (use_section_locality (),qid,scl) + msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> Flags.if_verbose - msg_warning (str "Implicit Arguments is deprecated; use Arguments instead"); - VernacDeclareImplicits (use_section_locality (),qid,pos) + msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl @@ -647,15 +708,16 @@ GEXTEND Gram | IDENT "No"; IDENT "Variables" -> None | ["Variable" | IDENT "Variables"]; idl = LIST1 identref -> Some idl ] -> - VernacGeneralizable (use_non_locality (), gen) ] ] + VernacGeneralizable gen ] ] ; arguments_modifier: - [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase] - | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold] + [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase] + | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold] | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits] | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] | IDENT "rename" -> [`Rename] + | IDENT "assert" -> [`Assert] | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes] | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> [`ClearImplicits; `ClearScopes] @@ -674,7 +736,7 @@ GEXTEND Gram ; argument_spec: [ [ b = OPT "!"; id = name ; s = OPT scope -> - snd id, b <> None, Option.map (fun x -> loc, x) s + snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s ] ]; strategy_level: @@ -688,7 +750,7 @@ GEXTEND Gram [ [ name = identref; sup = OPT binders -> (let (loc,id) = name in (loc, Name id)), (Option.default [] sup) - | -> (loc, Anonymous), [] ] ] + | -> (!@loc, Anonymous), [] ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] @@ -703,18 +765,20 @@ GEXTEND Gram END GEXTEND Gram - GLOBAL: command check_command class_rawexpr; + GLOBAL: command query_command class_rawexpr; command: - [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l + [ [ IDENT "Ltac"; + l = LIST1 tacdef_body SEP "with" -> + VernacDeclareTacticDefinition (true, l) + + | IDENT "Comments"; l = LIST0 comment -> VernacComments l (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, not (use_section_locality ()), - snd namesup, (fst namesup, expl, t), - None, pri) + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) (* System directory *) | IDENT "Pwd" -> VernacChdir None @@ -729,7 +793,7 @@ GEXTEND Gram s = [ s = ne_string -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> - VernacDeclareMLModule (use_locality (), l) + VernacDeclareMLModule l | IDENT "Locate"; l = locatable -> VernacLocate l @@ -759,44 +823,32 @@ GEXTEND Gram VernacPrint (PrintModuleType qid) | IDENT "Print"; IDENT "Module"; qid = global -> VernacPrint (PrintModule qid) + | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> + VernacPrint (PrintNamespace ns) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) - | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid) - - (* Searching the environment *) - | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> - VernacSearch (SearchHead c, l) - | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> - VernacSearch (SearchPattern c, l) - | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> - VernacSearch (SearchRewrite c, l) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> - let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m) - (* compatibility format of SearchAbout, with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> VernacAddMLPath (false, dir) | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> VernacAddMLPath (true, dir) - (* Pour intervenir sur les tables de paramètres *) + (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (use_locality_full(),table,v) + VernacSetOption (table,v) | "Set"; table = option_table -> - VernacSetOption (use_locality_full(),table,BoolValue true) + VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_table -> - VernacUnsetOption (use_locality_full(),table) + VernacUnsetOption table | IDENT "Print"; IDENT "Table"; table = option_table -> VernacPrintOption table | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value -> VernacAddOption ([table;field], v) - (* Un value global ci-dessous va être caché par un field au dessus! *) - (* En fait, on donne priorité aux tables secondaires *) - (* Pas de syntaxe pour les tables tertiaires pour cause de conflit *) - (* (mais de toutes façons, pas utilisées) *) + (* A global value below will be hidden by a field above! *) + (* In fact, we give priority to secondary tables *) + (* No syntax for tertiary tables due to conflict *) + (* (but they are unused anyway) *) | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> VernacAddOption ([table], v) @@ -810,13 +862,31 @@ GEXTEND Gram | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> VernacRemoveOption ([table], v) ]] ; - check_command: (* TODO: rapprocher Eval et Check *) + query_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) | IDENT "Compute"; c = lconstr -> - fun g -> VernacCheckMayEval (Some Glob_term.CbvVm, g, c) + fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) | IDENT "Check"; c = lconstr -> - fun g -> VernacCheckMayEval (None, g, c) ] ] + fun g -> VernacCheckMayEval (None, g, c) + (* Searching the environment *) + | IDENT "About"; qid = smart_global -> + fun g -> VernacPrint (PrintAbout (qid,g)) + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules -> + fun g -> VernacSearch (SearchHead c,g, l) + | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> + fun g -> VernacSearch (SearchPattern c,g, l) + | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> + fun g -> VernacSearch (SearchRewrite c,g, l) + | IDENT "Search"; s = searchabout_query; l = searchabout_queries -> + let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) + (* compatibility: SearchAbout *) + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> + fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) + (* compatibility: SearchAbout with "[ ... ]" *) + | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; + l = in_or_out_modules -> fun g -> VernacSearch (SearchAbout sl,g, l) + ] ] ; printable: [ [ IDENT "Term"; qid = smart_global -> PrintName qid @@ -832,6 +902,7 @@ GEXTEND Gram | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath | IDENT "ML"; IDENT "Modules" -> PrintMLModules + | IDENT "Debug"; IDENT "GC" -> PrintDebugGC | IDENT "Graph" -> PrintGraph | IDENT "Classes" -> PrintClasses | IDENT "TypeClasses" -> PrintTypeClasses @@ -854,8 +925,12 @@ GEXTEND Gram | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt) | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt) - | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid) - | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, qid) ] ] + | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid) + | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid) + | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid) + | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid) + | IDENT "Strategy"; qid = smart_global -> PrintStrategy (Some qid) + | IDENT "Strategies" -> PrintStrategy None ] ] ; class_rawexpr: [ [ IDENT "Funclass" -> FunClass @@ -863,7 +938,8 @@ GEXTEND Gram | qid = smart_global -> RefClass qid ] ] ; locatable: - [ [ qid = smart_global -> LocateTerm qid + [ [ qid = smart_global -> LocateAny qid + | IDENT "Term"; qid = smart_global -> LocateTerm qid | IDENT "File"; f = ne_string -> LocateFile f | IDENT "Library"; qid = global -> LocateLibrary qid | IDENT "Module"; qid = global -> LocateModule qid @@ -938,16 +1014,16 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (None,["Ltac";"Debug"], BoolValue true) + VernacSetOption (["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (None,["Ltac";"Debug"], BoolValue false) + VernacSetOption (["Ltac";"Debug"], BoolValue false) (* registration of a custom reduction *) | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; r = Tactic.red_expr -> - VernacDeclareReduction (use_locality(),s,r) + VernacDeclareReduction (s,r) ] ]; END @@ -960,31 +1036,33 @@ GEXTEND Gram syntax: [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (enforce_section_locality local,true,sc) + VernacOpenCloseScope (local,(true,sc)) | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (enforce_section_locality local,false,sc) + VernacOpenCloseScope (local,(false,sc)) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc,key) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; - refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) + refl = LIST1 smart_global -> VernacBindScope (sc,refl) | IDENT "Infix"; local = obsolete_locality; op = ne_lstring; ":="; p = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix (enforce_module_locality local,(op,modl),p,sc) + VernacInfix (local,(op,modl),p,sc) | IDENT "Notation"; local = obsolete_locality; id = identref; idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition - (id,(idl,c),enforce_module_locality local,b) + (id,(idl,c),local,b) | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (enforce_module_locality local,c,(s,modl),sc) + VernacNotation (local,c,(s,modl),sc) + | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> + VernacNotationAddFormat (n,s,fmt) | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; pil = LIST1 production_item; ":="; t = Tactic.tactic @@ -994,12 +1072,12 @@ GEXTEND Gram l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; let (loc,s) = s in - VernacSyntaxExtension (use_module_locality(),((loc,"x '"^s^"' y"),l)) + VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l)) | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (enforce_module_locality local,(s,l)) + -> VernacSyntaxExtension (local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) @@ -1031,7 +1109,11 @@ GEXTEND Gram SetOnlyParsing Flags.Current | IDENT "compat"; s = STRING -> SetOnlyParsing (Coqinit.get_compat_version s) - | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s + | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; + s2 = OPT [s = STRING -> (!@loc,s)] -> + begin match s1, s2 with + | (_,k), Some s -> SetFormat(k,s) + | s, None -> SetFormat ("text",s) end | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) @@ -1049,6 +1131,6 @@ GEXTEND Gram [ [ s = ne_string -> TacTerm s | nt = IDENT; po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; - ")" -> (p,sep) ] -> TacNonTerm (loc,nt,po) ] ] + ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ] ; END |