(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* ->"; ":<"; "<:"; "where"; "at" ] let _ = List.iter CLexer.add_keyword vernac_kw (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) let query_command = Gram.entry_create "vernac:query_command" let subprf = Gram.entry_create "vernac:subprf" let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" let thm_token = Gram.entry_create "vernac:thm_token" let def_body = Gram.entry_create "vernac:def_body" let decl_notation = Gram.entry_create "vernac:decl_notation" 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_expr = Gram.entry_create "vernac:section_subset_expr" let make_bullet s = let n = String.length s in match s.[0] with | '-' -> Dash n | '+' -> Plus n | '*' -> Star n | _ -> assert false GEXTEND Gram GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail 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 *) [ [ 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 | c = subprf -> c ] ] ; vernac_aux: LAST [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: [ [ c = subgoal_command -> c None] ] ; subprf: [ [ s = BULLET -> VernacBullet (make_bullet s) | "{" -> VernacSubproof None | "}" -> VernacEndSubproof ] ] ; subgoal_command: [ [ 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 ] ] ; located_vernac: [ [ v = vernac -> !@loc, v ] ] ; END let warn_plural_command = CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) let test_plural_form loc kwd = function | [(_,([_],_))] -> warn_plural_command ~loc:!@loc kwd | _ -> () let test_plural_form_types loc kwd = function | [([_],_)] -> warn_plural_command ~loc:!@loc kwd | _ -> () let fresh_var env c = Namegen.next_ident_away (Id.of_string "pat") (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c)) let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion record_field decl_notation rec_definition pidentref; gallina: (* Definition, Theorem, Variable, Axiom, ... *) [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr; l = LIST0 [ "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 -> VernacAssumption (stre, nl, bl) | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> test_plural_form loc kwd bl; VernacAssumption (stre, nl, bl) | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), (id, None), b) (* Gallina inductive declarations *) | 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 (priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (Some Discharge, recs) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> 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) | 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 | IDENT "Fact" -> Fact | IDENT "Remark" -> Remark | IDENT "Corollary" -> Corollary | IDENT "Proposition" -> Proposition | IDENT "Property" -> Property ] ] ; def_token: [ [ "Definition" -> (None, Definition) | IDENT "Example" -> (None, Example) | IDENT "SubClass" -> (None, SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Some Discharge, Logical) | "Variable" -> (Some Discharge, Definitional) | "Axiom" -> (None, Logical) | "Parameter" -> (None, Definitional) | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical)) | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional)) | IDENT "Axioms" -> ("Axioms", (None, Logical)) | IDENT "Parameters" -> ("Parameters", (None, Definitional)) | IDENT "Conjectures" -> ("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 = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; r = universe_level -> (l, ord, r) ] ] ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) | "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 -> let (bl, c) = expand_pattern_binders mkCLambdaN bl c in (match c with CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = if List.exists (function LocalPattern _ -> true | _ -> false) bl then let c = CCast (!@loc, c, CastConv t) in (expand_pattern_binders mkCLambdaN bl c, None) else ((bl, c), Some t) in DefineBody (bl, red, c, tyo) | bl = binders; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; reduce: [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r | -> None ] ] ; one_decl_notation: [ [ ntn = ne_lstring; ":="; c = constr; scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ; decl_notation: [ [ "where"; l = LIST1 one_decl_notation SEP IDENT "and" -> l | -> [] ] ] ; (* Inductives and records *) opt_constructors_or_fields: [ [ ":="; lc = constructor_list_or_record_decl -> lc | -> RecordDecl (None, []) ] ] ; inductive_definition: [ [ 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) ] ] ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> Constructors ((c id)::l) | id = identref ; c = constructor_type -> Constructors [ c id ] | cstr = identref; "{"; fs = record_fields; "}" -> RecordDecl (Some cstr,fs) | "{";fs = record_fields; "}" -> RecordDecl (None,fs) | -> Constructors [] ] ] ; (* csort: [ [ s = sort -> CSort (loc,s) ] ] ; *) opt_coercion: [ [ ">" -> true | -> false ] ] ; (* (co)-fixpoints *) rec_definition: [ [ 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 = pidentref; bl = binders; ty = type_cstr; def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; type_cstr: [ [ ":"; c=lconstr -> c | -> CHole (!@loc, None, Misctypes.IntroAnonymous, None) ] ] ; (* Inductive schemes *) scheme: [ [ kind = scheme_kind -> (None,kind) | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] ; scheme_kind: [ [ IDENT "Induction"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) | IDENT "Elimination"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) | IDENT "Case"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) (* (* ... without coercions *) binder_nodef: [ [ b = binder_let -> (match b with LocalRawAssum(l,ty) -> (l,ty) | LocalRawDef _ -> Util.user_err_loc (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] ; *) (* ... with coercions *) record_field: [ [ 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)) | 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))) | l = binders; ":="; b = lconstr -> fun id -> match b with | 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)) ] ] ; record_binder: [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None, Misctypes.IntroAnonymous, None))) | id = name; f = record_binder_body -> f id ] ] ; assum_list: [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ] ; assum_coe: [ [ "("; a = simple_assum_coe; ")" -> a ] ] ; simple_assum_coe: [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr -> (not (Option.is_empty oc),(idl,c)) ] ] ; constructor_type: [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (not (Option.is_empty coe),(id,mkCProdN (!@loc) l c)) | -> fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None, Misctypes.IntroAnonymous, None)))) ] -> t l ]] ; constructor: [ [ id = identref; c=constructor_type -> c id ] ] ; of_type_with_opt_coercion: [ [ ":>>" -> Some false | ":>"; ">" -> Some false | ":>" -> Some true | ":"; ">"; ">" -> Some false | ":"; ">" -> Some true | ":" -> None ] ] ; END 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 _ | 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 let warn_deprecated_include_type = CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" (fun () -> strbrk "Include Type is deprecated; use Include instead") (* Modules and Sections *) GEXTEND Gram GLOBAL: gallina_ext module_expr module_type section_subset_expr; gallina_ext: [ [ (* Interactive module declaration *) IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; sign = of_module_type; body = is_module_expr -> VernacDefineModule (export, id, bl, sign, body) | IDENT "Module"; "Type"; id = identref; bl = LIST0 module_binder; sign = check_module_types; body = is_module_type -> VernacDeclareModuleType (id, bl, sign, body) | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; ":"; mty = module_type_inl -> VernacDeclareModule (export, id, bl, mty) (* Section beginning *) | IDENT "Section"; id = identref -> VernacBeginSection id | IDENT "Chapter"; id = identref -> VernacBeginSection id (* 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_expr -> VernacNameSectionHypSet (id, expr) (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; qidl = LIST1 global -> VernacRequire (None, export, qidl) | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token ; qidl = LIST1 global -> VernacRequire (Some ns, 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 -> warn_deprecated_include_type ~loc:!@loc (); VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false | IDENT "Export" -> Some true | -> None ] ] ; ext_module_type: [ [ "<+"; mty = module_type_inl -> mty ] ] ; ext_module_expr: [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ] ; check_module_type: [ [ "<:"; mty = module_type_inl -> mty ] ] ; check_module_types: [ [ mtys = LIST0 check_module_type -> mtys ] ] ; of_module_type: [ [ ":"; mty = module_type_inl -> Enforce mty | mtys = check_module_types -> Check mtys ] ] ; is_module_type: [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l) | -> [] ] ] ; is_module_expr: [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l) | -> [] ] ] ; functor_app_annot: [ [ "["; 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,NoInline) | me = module_expr; a = functor_app_annot -> (me,a) ] ] ; module_type_inl: [ [ "!"; me = module_type -> (me,NoInline) | me = module_type; a = functor_app_annot -> (me,a) ] ] ; (* Module binder *) module_binder: [ [ "("; export = export_token; idl = LIST1 identref; ":"; mty = module_type_inl; ")" -> (export,idl,mty) ] ] ; (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me | me1 = module_expr; me2 = module_expr_atom -> CMapply (!@loc,me1,me2) ] ] ; module_expr_atom: [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> CWith_Definition (fqid,c) | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> CWith_Module (fqid,qid) ] ] ; module_type: [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me) | mty = module_type; "with"; decl = with_declaration -> CMwith (!@loc,mty,decl) ] ] ; (* 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 = ssexpr -> SsCompl e ] | "50" [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2) | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)] | "0" [ 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 let warn_deprecated_arguments_scope = CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") let warn_deprecated_implicit_arguments = CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") let warn_deprecated_arguments_syntax = CWarnings.create ~name:"deprecated-arguments-syntax" ~category:"deprecated" (fun () -> strbrk "The \"/\" and \"!\" modifiers have an effect only " ++ strbrk "in the first arguments list. The syntax allowing" ++ strbrk " them to appear in other lists is deprecated.") (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name hint_info; gallina_ext: [ [ (* Transparent and Opaque *) IDENT "Transparent"; l = LIST1 smart_global -> VernacSetOpacity (Conv_oracle.transparent, l) | IDENT "Opaque"; l = LIST1 smart_global -> VernacSetOpacity (Conv_oracle.Opaque, l) | IDENT "Strategy"; l = LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] -> VernacSetStrategy l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical (AN qid) | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> VernacCanonical (ByNotation ntn) | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition ((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),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),None),d) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (true, f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (false, f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (true, AN qid, s, t) | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (true, ByNotation ntn, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (false, AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (false, ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | ":="; c = lconstr -> Some (false,c) | -> None ] -> VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) | IDENT "Existing"; IDENT "Instance"; id = global; info = hint_info -> VernacDeclareInstances [id, info] | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; pri = OPT [ "|"; i = natural -> i ] -> let info = { hint_priority = pri; hint_pattern = None } in let insts = List.map (fun i -> (i, info)) ids in VernacDeclareInstances insts | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is (* Arguments *) | IDENT "Arguments"; qid = smart_global; args = LIST0 argument_spec_block; more_implicits = OPT [ ","; impl = LIST1 [ impl = LIST0 more_implicits_block -> let warn_deprecated = List.exists fst impl in if warn_deprecated then warn_deprecated_arguments_syntax ~loc:!@loc (); List.flatten (List.map snd impl)] SEP "," -> impl ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> let mods = match mods with None -> [] | Some l -> List.flatten l in let slash_position = ref None in let rec parse_args i = function | [] -> [] | `Id x :: args -> x :: parse_args (i+1) args | `Slash :: args -> if Option.is_empty !slash_position then (slash_position := Some i; parse_args i args) else error "The \"/\" modifier can occur only once" in let args = parse_args 0 (List.flatten args) in let more_implicits = Option.default [] more_implicits in VernacArguments (qid, args, more_implicits, !slash_position, 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 ]; "]" -> warn_deprecated_arguments_scope ~loc:!@loc (); 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 ] -> warn_deprecated_implicit_arguments ~loc:!@loc (); VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> test_plural_form_types loc "Implicit Types" bl; VernacReserve bl | IDENT "Generalizable"; gen = [IDENT "All"; IDENT "Variables" -> Some [] | IDENT "No"; IDENT "Variables" -> None | ["Variable" | IDENT "Variables"]; idl = LIST1 identref -> Some idl ] -> VernacGeneralizable gen ] ] ; arguments_modifier: [ [ 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] | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> [`ClearImplicits; `ClearScopes] ] ] ; implicit_name: [ [ "!"; id = ident -> (id, false, true) | id = ident -> (id,false,false) | "["; "!"; id = ident; "]" -> (id,true,true) | "["; id = ident; "]" -> (id,true, false) ] ] ; scope: [ [ "%"; key = IDENT -> key ] ] ; argument_spec: [ [ b = OPT "!"; id = name ; s = OPT scope -> snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s ] ]; (* List of arguments implicit status, scope, modifiers *) argument_spec_block: [ [ item = argument_spec -> let name, recarg_like, notation_scope = item in [`Id { name=name; recarg_like=recarg_like; notation_scope=notation_scope; implicit_status = NotImplicit}] | "/" -> [`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 | Some _, Some _ -> error "scope declared twice" in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = NotImplicit}) 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 | Some _, Some _ -> error "scope declared twice" in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = Implicit}) 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 | Some _, Some _ -> error "scope declared twice" in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = MaximallyImplicit}) items ] ]; name_or_bang: [ [ b = OPT "!"; id = name -> not (Option.is_empty b), id ] ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ [ (bang,name) = name_or_bang -> (bang, [(snd name, Vernacexpr.NotImplicit)]) | "/" -> (true (* Should warn about deprecated syntax *), []) | "["; items = LIST1 name_or_bang; "]" -> (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.Implicit)) items) | "{"; items = LIST1 name_or_bang; "}" -> (List.exists fst items, List.map (fun (_,(_,name)) -> (name, Vernacexpr.MaximallyImplicit)) items) ] ]; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque | n=INT -> Conv_oracle.Level (int_of_string n) | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: [ [ name = pidentref; sup = OPT binders -> (let ((loc,id),l) = name in ((loc, Name id),l)), (Option.default [] sup) | -> ((!@loc, Anonymous), None), [] ] ] ; hint_info: [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> { hint_priority = i; hint_pattern = pat } | -> { hint_priority = None; hint_pattern = None } ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] ; reserv_tuple: [ [ "("; a = simple_reserv; ")" -> a ] ] ; simple_reserv: [ [ idl = LIST1 identref; ":"; c = lconstr -> (idl,c) ] ] ; END GEXTEND Gram GLOBAL: command query_command class_rawexpr; command: [ [ 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 = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; info = hint_info -> VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) (* System directory *) | IDENT "Pwd" -> VernacChdir None | IDENT "Cd" -> VernacChdir None | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir) (* Toplevel control *) | IDENT "Drop" -> VernacToplevelControl Drop | IDENT "Quit" -> VernacToplevelControl Quit | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; s = [ s = ne_string -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> VernacDeclareMLModule l | IDENT "Locate"; l = locatable -> VernacLocate l (* Managing load paths *) | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> VernacAddLoadPath (false, dir, alias) | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> VernacRemoveLoadPath dir (* For compatibility *) | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath -> VernacAddLoadPath (false, dir, alias) | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) | IDENT "DelPath"; dir = ne_string -> VernacRemoveLoadPath dir (* Type-Checking (pas dans le refman) *) | "Type"; c = lconstr -> VernacGlobalCheck c (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid) | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> 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 "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) (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> begin match v with | StringValue s -> (* We make a special case for warnings because appending is their natural semantics *) if CString.List.equal table ["Warnings"] then VernacSetAppendOption (table, s) else let (last, prefix) = List.sep_last table in if String.equal last "Append" && not (List.is_empty prefix) then VernacSetAppendOption (prefix, s) else VernacSetOption (table, v) | _ -> VernacSetOption (table, v) end | "Set"; table = option_table -> VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_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) (* 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) | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value -> VernacMemOption (table, v) | IDENT "Test"; table = option_table -> VernacPrintOption table | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption ([table;field], v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> VernacRemoveOption ([table], v) ]] ; 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 (Genredexpr.CbvVm None), g, c) | IDENT "Check"; c = lconstr -> 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 | IDENT "All" -> PrintFullContext | IDENT "Section"; s = global -> PrintSectionContext s | IDENT "Grammar"; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) PrintGrammar ent | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir | IDENT "Modules" -> error "Print Modules is obsolete; use Print Libraries instead" | IDENT "Libraries" -> PrintModules | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath | IDENT "ML"; IDENT "Modules" -> PrintMLModules | IDENT "Debug"; IDENT "GC" -> PrintDebugGC | IDENT "Graph" -> PrintGraph | IDENT "Classes" -> PrintClasses | IDENT "TypeClasses" -> PrintTypeClasses | IDENT "Instances"; qid = smart_global -> PrintInstances qid | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions | IDENT "Tables" -> PrintTables | IDENT "Options" -> PrintTables (* A Synonymous to Tables *) | IDENT "Hint" -> PrintHintGoal | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s | 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, 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 | IDENT "Sortclass" -> SortClass | qid = smart_global -> RefClass qid ] ] ; locatable: [ [ 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 | IDENT "Ltac"; qid = global -> LocateTactic qid ] ] ; option_value: [ [ n = integer -> IntValue (Some n) | s = STRING -> StringValue s ] ] ; option_ref_value: [ [ id = global -> QualidRefValue id | s = STRING -> StringRefValue s ] ] ; option_table: [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]] ; as_dirpath: [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] ; ne_in_or_out_modules: [ [ IDENT "inside"; l = LIST1 global -> SearchInside l | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ] ; in_or_out_modules: [ [ m = ne_in_or_out_modules -> m | -> SearchOutside [] ] ] ; comment: [ [ c = constr -> CommentConstr c | s = STRING -> CommentString s | n = natural -> CommentInt n ] ] ; positive_search_mark: [ [ "-" -> false | -> true ] ] ; scope: [ [ "%"; key = IDENT -> key ] ] ; searchabout_query: [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> (b, SearchString (s,sc)) | b = positive_search_mark; p = constr_pattern -> (b, SearchSubPattern p) ] ] ; searchabout_queries: [ [ m = ne_in_or_out_modules -> ([],m) | s = searchabout_query; l = searchabout_queries -> let (sl,m) = l in (s::sl,m) | -> ([],SearchOutside []) ] ] ; END; GEXTEND Gram command: [ [ (* State management *) IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s (* Resetting *) | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial | IDENT "Reset"; id = identref -> VernacResetName id | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n | IDENT "BackTo"; n = natural -> VernacBackTo n | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> VernacBacktrack (n,m,p) (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> VernacSetOption (["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> VernacSetOption (["Ltac";"Debug"], BoolValue false) (* registration of a custom reduction *) | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; r = Tactic.red_expr -> VernacDeclareReduction (s,r) ] ]; END ;; (* Grammar extensions *) GEXTEND Gram GLOBAL: syntax; syntax: [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> VernacOpenCloseScope (local,(true,sc)) | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> VernacOpenCloseScope (local,(false,sc)) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc, Some key) | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> VernacDelimiters (sc, None) | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> 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 (local,(op,modl),p,sc) | IDENT "Notation"; local = obsolete_locality; id = identref; idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition (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 (local,c,(s,modl),sc) | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> VernacNotationAddFormat (n,s,fmt) | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> Metasyntax.check_infix_modifiers l; let (loc,s) = s in 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 (local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] ; only_parsing: [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> Some Flags.Current | "("; IDENT "compat"; s = STRING; ")" -> Some (Coqinit.get_compat_version s) | -> None ] ] ; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] ; syntax_modifier: [ [ "at"; IDENT "level"; n = natural -> SetLevel n | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA | IDENT "only"; IDENT "printing" -> SetOnlyPrinting | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> SetCompatVersion (Coqinit.get_compat_version 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) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ] ; syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint | IDENT "binder" -> ETBinder true | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; END