(***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* ->"; ":<"; "<:" ] let _ = List.iter (fun s -> Lexer.add_token ("",s)) 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 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" GEXTEND Gram GLOBAL: vernac gallina_ext; vernac: (* 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 | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l ] ] ; vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v ] ] ; vernac: LAST [ [ gln = OPT[n=natural; ":" -> n]; tac = subgoal_command; "." -> tac gln ] ] ; subgoal_command: [ [ c = check_command -> c | d = use_default_tac; tac = Tactic.tactic -> (fun g -> let g = match g with Some gl -> gl | _ -> 1 in VernacSolve(g,tac,d)) ] ] ; located_vernac: [ [ v = vernac -> loc, v ] ] ; use_default_tac: [ [ "!!" -> false | -> true ] ] ; END let test_plurial_form = function | [_] -> Options.if_verbose warning "Keywords Variables/Hypotheses/Parameters expect more than one assumption" | _ -> () let no_coercion loc (c,x) = if c then Util.user_err_loc (loc,"no_coercion",Pp.str"no coercion allowed here"); x let flatten_assum l = List.flatten (List.map (fun (oc,(idl,t)) -> List.map (fun id -> (oc,(id,t))) idl) l) (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body; gallina: (* Definition, Theorem, Variable, Axiom, ... *) [ [ thm = thm_token; id = base_ident; (* bl = LIST0 binder; *) ":"; c = lconstr -> let bl = [] in VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) | (f,d,e) = def_token; id = base_ident; b = def_body -> VernacDefinition (d, id, b, f, e) | stre = assumption_token; bl = assum_list -> VernacAssumption (stre, flatten_assum bl) | stre = assumptions_token; bl = assum_list -> let l = flatten_assum bl in test_plurial_form l; VernacAssumption (stre, l) (* Gallina inductive declarations *) | (* Non porté (?) : OPT[IDENT "Mutual"];*) f = finite_token; indl = LIST1 inductive_definition SEP "with" -> VernacInductive (f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint recs | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint corecs | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] ; gallina_ext: [ [ b = record_token; oc = opt_coercion; name = base_ident; ps = LIST0 binder_let; ":"; s = lconstr; ":="; cstr = OPT base_ident; "{"; fs = LIST0 record_field SEP ";"; "}" -> VernacRecord (b,(oc,name),ps,s,cstr,fs) (* Non porté ? | f = finite_token; s = csort; id = base_ident; indpar = LIST0 simple_binder; ":="; lc = constructor_list -> VernacInductive (f,[id,None,indpar,s,lc]) *) ] ] ; thm_token: [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma | IDENT "Fact" -> Fact | IDENT "Remark" -> Remark ] ] ; def_token: [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition | IDENT "SubClass" -> Class.add_subclass_hook, Global, GCoercion | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, Local, LCoercion ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) | "Variable" -> (Local, Definitional) | "Axiom" -> (Global, Logical) | "Parameter" -> (Global, Definitional) ] ] ; assumptions_token: [ [ IDENT "Hypotheses" -> (Local, Logical) | IDENT "Variables" -> (Local, Definitional) | IDENT "Axioms" -> (Global, Logical) | IDENT "Parameters" -> (Global, Definitional) ] ] ; finite_token: [ [ "Inductive" -> true | "CoInductive" -> false ] ] ; record_token: [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ] ; (* Simple definitions *) def_body: [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> (match c with CCast(_,c,t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) | bl = LIST0 binder_let; ":"; t = lconstr -> ProveBody (bl, t) ] ] ; reduce: [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r | -> None ] ] ; decl_notation: [ [ OPT [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,scopt) ] ] ] ; (* Inductives and records *) inductive_definition: [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr; ntn = decl_notation; ":="; lc = constructor_list -> (id,ntn,indpar,c,lc) ] ] ; constructor_list: [ [ "|"; l = LIST1 constructor SEP "|" -> l | l = LIST1 constructor SEP "|" -> l | -> [] ] ] ; (* csort: [ [ s = sort -> CSort (loc,s) ] ] ; *) opt_coercion: [ [ ">" -> true | -> false ] ] ; (* (co)-fixpoints *) rec_definition: [ [ id = base_ident; bl = LIST1 binder_nodef; annot = OPT rec_annotation; type_ = type_cstr; ntn = decl_notation; ":="; def = lconstr -> let names = List.map snd (List.flatten (List.map fst bl)) in let ni = match annot with Some id -> (try list_index (Name id) names - 1 with Not_found -> Util.user_err_loc (loc,"Fixpoint", Pp.str "No argument named " ++ Nameops.pr_id id)) | None -> if List.length names > 1 then Util.user_err_loc (loc,"Fixpoint", Pp.str "the recursive argument needs to be specified"); 0 in let loc0 = fst (List.hd (fst (List.hd bl))) in let loc1 = join_loc loc0 (constr_loc type_) in let loc2 = join_loc loc0 (constr_loc def) in ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)),ntn) ] ] ; corec_definition: [ [ id = base_ident; bl = LIST0 binder_nodef; c = type_cstr; ":="; def = lconstr -> (id,CProdN(loc,bl,c),CLambdaN(loc,bl,def)) ] ] ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ] ; type_cstr: [ [ ":"; c=lconstr -> c | -> CHole loc ] ] ; (* Inductive schemes *) scheme: [ [ id = base_ident; ":="; dep = dep_scheme; "for"; ind = global; IDENT "Sort"; s = sort -> (id,dep,ind,s) ] ] ; dep_scheme: [ [ IDENT "Induction" -> true | IDENT "Minimality" -> false ] ] ; (* 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: [ [ id = base_ident -> (false,AssumExpr(id,CHole loc)) | id = base_ident; oc = of_type_with_opt_coercion; t = lconstr -> (oc,AssumExpr (id,t)) | id = base_ident; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) | id = base_ident; ":="; b = lconstr -> match b with CCast(_,b,t) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; assum_list: [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ] ; assum_coe: [ [ "("; a = simple_assum_coe; ")" -> a ] ] ; simple_assum_coe: [ [ idl = LIST1 base_ident; oc = of_type_with_opt_coercion; c = lconstr -> (oc,(idl,c)) ] ] ; constructor: [ [ id = base_ident; l = LIST0 binder_let; coe = of_type_with_opt_coercion; c = lconstr -> (coe,(id,G_constrnew.mkCProdN loc l c)) | id = base_ident; l = LIST0 binder_let -> (false,(id,G_constrnew.mkCProdN loc l (CHole loc))) ] ] ; of_type_with_opt_coercion: [ [ ":>" -> true | ":"; ">" -> true | ":" -> false ] ] ; END (* Modules and Sections *) GEXTEND Gram GLOBAL: gallina_ext module_expr module_type; gallina_ext: [ [ (* Interactive module declaration *) IDENT "Module"; id = base_ident; bl = LIST0 module_binder; mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr -> VernacDefineModule (id, bl, mty_o, mexpr_o) | IDENT "Module"; "Type"; id = base_ident; bl = LIST0 module_binder; mty_o = OPT is_module_type -> VernacDeclareModuleType (id, bl, mty_o) | IDENT "Declare"; IDENT "Module"; id = base_ident; bl = LIST0 module_binder; mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr -> VernacDeclareModule (id, bl, mty_o, mexpr_o) (* Section beginning *) | IDENT "Section"; id = base_ident -> VernacBeginSection id | IDENT "Chapter"; id = base_ident -> VernacBeginSection id (* This end a Section a Module or a Module Type *) | IDENT "End"; id = base_ident -> VernacEndSegment id (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; specif = specif_token; qidl = LIST1 global -> VernacRequire (export, specif, qidl) | IDENT "Require"; export = export_token; specif = specif_token; filename = STRING -> VernacRequireFrom (export, specif, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) ] ] ; export_token: [ [ IDENT "Import" -> Some false | IDENT "Export" -> Some true | IDENT "Closed" -> None | -> Some false ] ] ; specif_token: [ [ IDENT "Implementation" -> Some false | IDENT "Specification" -> Some true | -> None ] ] ; of_module_type: [ [ ":"; mty = module_type -> (mty, true) | "<:"; mty = module_type -> (mty, false) ] ] ; is_module_type: [ [ ":="; mty = module_type -> mty ] ] ; is_module_expr: [ [ ":="; mexpr = module_expr -> mexpr ] ] ; (* Module binder *) module_binder: [ [ "("; idl = LIST1 base_ident; ":"; mty = module_type; ")" -> (idl,mty) ] ] ; (* Module expressions *) module_expr: [ [ qid = qualid -> CMEident qid | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2) | "("; me = module_expr; ")" -> me (* ... *) ] ] ; with_declaration: [ [ "Definition"; id = base_ident; ":="; c = Constr.lconstr -> CWith_Definition (id,c) | IDENT "Module"; id = base_ident; ":="; qid = qualid -> CWith_Module (id,qid) ] ] ; module_type: [ [ qid = qualid -> CMTEident qid (* ... *) | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl) ] ] ; END (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ (* Transparent and Opaque *) IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l) | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l) (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in VernacDefinition (Global,s,d,Recordobj.add_object_hook,SCanonical) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in VernacDefinition (Global,s,d,Class.add_coercion_hook,GCoercion) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in VernacDefinition (Local,s,d,Class.add_coercion_hook,LCoercion) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (Local, f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (Global, f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (Local, qid, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (Global, qid, s, t) (* Implicit *) (* Obsolete | IDENT "Syntactic"; IDENT "Definition"; id = IDENT; ":="; c = lconstr; n = OPT [ "|"; n = natural -> n ] -> let c = match n with | Some n -> let l = list_tabulate (fun _ -> (CHole (loc),None)) n in CApp (loc,c,l) | None -> c in VernacNotation (false,c,Some("'"^id^"'",[]),None,None) *) | IDENT "Implicit"; IDENT "Arguments"; qid = global; pos = OPT [ "["; l = LIST0 natural; "]" -> l ] -> VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"]; idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c) (* For compatibility *) | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" -> VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"), BoolValue true) | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" -> VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"), BoolValue false) ] ] ; END GEXTEND Gram GLOBAL: command check_command class_rawexpr; command: [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l (* System directory *) | IDENT "Pwd" -> VernacChdir None | IDENT "Cd" -> VernacChdir None | IDENT "Cd"; dir = STRING -> VernacChdir (Some dir) (* Toplevel control *) | IDENT "Drop" -> VernacToplevelControl Drop | IDENT "ProtectedLoop" -> VernacToplevelControl ProtectedLoop | IDENT "Quit" -> VernacToplevelControl Quit | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; s = [ s = STRING -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING -> VernacDeclareMLModule l (* Dump of the universe graph - to file or to stdout *) | IDENT "Dump"; IDENT "Universes"; fopt = OPT STRING -> VernacPrint (PrintUniverses fopt) | IDENT "Locate"; l = locatable -> VernacLocate l (* Managing load paths *) | IDENT "Add"; IDENT "LoadPath"; dir = STRING; alias = as_dirpath -> VernacAddLoadPath (false, dir, alias) | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = STRING; alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) | IDENT "Remove"; IDENT "LoadPath"; dir = STRING -> VernacRemoveLoadPath dir (* For compatibility *) | IDENT "AddPath"; dir = STRING; "as"; alias = as_dirpath -> VernacAddLoadPath (false, dir, alias) | IDENT "AddRecPath"; dir = STRING; "as"; alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) | IDENT "DelPath"; dir = STRING -> VernacRemoveLoadPath dir (* Type-Checking (pas dans le refman) *) | "Type"; c = constr -> VernacGlobalCheck c (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p | IDENT "Print"; qid = global -> VernacPrint (PrintName qid) | IDENT "Print" -> VernacPrint PrintLocalContext | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> VernacPrint (PrintModuleType qid) | IDENT "Print"; IDENT "Module"; qid = global -> VernacPrint (PrintModule qid) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) (* Searching the environment *) | IDENT "Search"; qid = global; l = in_or_out_modules -> VernacSearch (SearchHead qid, 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"; qid = global; l = in_or_out_modules -> VernacSearch (SearchAbout qid, l) | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING -> VernacAddMLPath (false, dir) | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = STRING -> VernacAddMLPath (true, dir) (* Pour intervenir sur les tables de paramètres *) | "Set"; table = IDENT; field = IDENT; v = option_value -> VernacSetOption (SecondaryTable (table,field),v) | "Set"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value -> VernacAddOption (SecondaryTable (table,field),lv) | "Set"; table = IDENT; field = IDENT -> VernacSetOption (SecondaryTable (table,field),BoolValue true) | IDENT "Unset"; table = IDENT; field = IDENT -> VernacUnsetOption (SecondaryTable (table,field)) | IDENT "Unset"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value -> VernacRemoveOption (SecondaryTable (table,field),lv) | "Set"; table = IDENT; value = option_value -> VernacSetOption (PrimaryTable table, value) | "Set"; table = IDENT -> VernacSetOption (PrimaryTable table, BoolValue true) | IDENT "Unset"; table = IDENT -> VernacUnsetOption (PrimaryTable table) | IDENT "Print"; IDENT "Table"; table = IDENT; field = IDENT -> VernacPrintOption (SecondaryTable (table,field)) | IDENT "Print"; IDENT "Table"; table = IDENT -> VernacPrintOption (PrimaryTable table) | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value -> VernacAddOption (SecondaryTable (table,field), v) (* Un value global ci-dessous va être caché par un field au dessus! *) | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> VernacAddOption (PrimaryTable table, v) | IDENT "Test"; table = IDENT; field = IDENT; v = LIST1 option_ref_value -> VernacMemOption (SecondaryTable (table,field), v) | IDENT "Test"; table = IDENT; field = IDENT -> VernacPrintOption (SecondaryTable (table,field)) | IDENT "Test"; table = IDENT; v = LIST1 option_ref_value -> VernacMemOption (PrimaryTable table, v) | IDENT "Test"; table = IDENT -> VernacPrintOption (PrimaryTable table) | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption (SecondaryTable (table,field), v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> VernacRemoveOption (PrimaryTable table, v) ] ] ; check_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr -> fun g -> VernacCheckMayEval (Some r, g, c) | IDENT "Check"; c = constr -> fun g -> VernacCheckMayEval (None, g, c) ] ] ; printable: [ [ IDENT "Term"; qid = global -> PrintName qid | IDENT "All" -> PrintFullContext | IDENT "Section"; s = global -> PrintSectionContext s | IDENT "Grammar"; uni = IDENT; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) PrintGrammar (uni, ent) | IDENT "LoadPath" -> PrintLoadPath | IDENT "Modules" -> PrintModules | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath | IDENT "ML"; IDENT "Modules" -> PrintMLModules | IDENT "Graph" -> PrintGraph | IDENT "Classes" -> PrintClasses | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) | IDENT "Tables" -> PrintTables | IDENT "Proof"; qid = global -> PrintOpaqueName qid | IDENT "Hint" -> PrintHintGoal | IDENT "Hint"; qid = global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s ] ] ; class_rawexpr: [ [ IDENT "Funclass" -> FunClass | IDENT "Sortclass" -> SortClass | qid = global -> RefClass qid ] ] ; locatable: [ [ qid = global -> LocateTerm qid | IDENT "File"; f = STRING -> LocateFile f | IDENT "Library"; qid = global -> LocateLibrary qid | s = STRING -> LocateNotation s ] ] ; option_value: [ [ n = integer -> IntValue n | s = STRING -> StringValue s ] ] ; option_ref_value: [ [ id = global -> QualidRefValue id | s = STRING -> StringRefValue s ] ] ; as_dirpath: [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] ; in_or_out_modules: [ [ IDENT "inside"; l = LIST1 global -> SearchInside l | IDENT "outside"; l = LIST1 global -> SearchOutside l | -> SearchOutside [] ] ] ; comment: [ [ c = constr -> CommentConstr c | s = STRING -> CommentString s | n = natural -> CommentInt n ] ] ; END; GEXTEND Gram command: [ [ (* State management *) IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s | IDENT "Write"; IDENT "State"; s = STRING -> VernacWriteState s | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s | IDENT "Restore"; IDENT "State"; s = STRING -> VernacRestoreState s (* Resetting *) | IDENT "Reset"; id = identref -> VernacResetName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> VernacDebug true | IDENT "Debug"; IDENT "Off" -> VernacDebug false ] ]; END ;; (* Grammar extensions *) GEXTEND Gram GLOBAL: syntax; syntax: [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> VernacOpenScope (local,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) | IDENT "Arguments"; IDENT "Scope"; qid = global; "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl) | IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *) op = STRING; p = global; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in VernacInfix (local,a,n,op,p,b,None,sc) | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr; l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing] | -> [] ] -> VernacNotation (local,c,Some("'"^s^"'",l),None,None) | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (local,c,Some(s,modl),None,sc) | IDENT "Tactic"; IDENT "Notation"; s = STRING; pil = LIST0 production_item; ":="; t = Tactic.tactic -> VernacTacticGrammar ["",(s,pil),t] (* | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic"; (* OPT [ ":"; IDENT "tactic" ]; *) ":="; OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> VernacTacticGrammar tl *) | IDENT "Grammar"; u = univ; tl = LIST1 grammar_entry SEP "with" -> failwith "Grammar for constr not supported in v8; use Notation" (* VernacGrammar (rename_command_entry u,tl) *) | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP "," -> failwith "Syntax not supported in v8; use Notation" (* VernacSyntax (u,el) *) | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> VernacSyntaxExtension (local,Some(s,l),None) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] ; locality: [ [ IDENT "Local" -> true | -> false ] ] ; univ: [ [ univ = IDENT -> set_default_action_parser (parser_type_from_name univ); univ ] ] ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] ; syntax_modifier: [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev) | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; lev = level -> SetItemLevel (x::l,lev) | IDENT "at"; IDENT "level"; n = natural -> SetLevel n | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) | IDENT "only"; IDENT "parsing" -> SetOnlyParsing ] ] ; syntax_extension_type: [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint | e=IDENT -> ETOther("constr",e) ] ] ; opt_scope: [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ] ; (* Syntax entries for Grammar. Only grammar_entry is exported *) grammar_entry: [[ nont = IDENT; set_entry_type; ":="; ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" -> (rename_command_entry nont,ep,rl) ]] ; entry_prec: [[ IDENT "LEFTA" -> Some Gramext.LeftA | IDENT "RIGHTA" -> Some Gramext.RightA | IDENT "NONA" -> Some Gramext.NonA | -> None ]] ; (* grammar_tactic_rule: [[ (* name = rule_name; *) "["; s = STRING; pil = LIST0 production_item; "]"; "->"; "["; t = Tactic.tactic; "]" -> let name="" in (name,(s,pil),t) ]] ; *) grammar_rule: [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->"; a = action -> (name, pil, a) ]] ; rule_name: [[ name = IDENT -> name ]] ; production_item: [[ s = STRING -> VTerm s | nt = non_terminal; po = OPT [ "("; p = ident; ")" -> p ] -> VNonTerm (loc,nt,po) ]] ; non_terminal: [[ u = IDENT; ":"; nt = IDENT -> NtQual(rename_command_entry u, rename_command_entry nt) | nt = IDENT -> NtShort (rename_command_entry nt) ]] ; (* Syntax entries for Syntax. Only syntax_entry is exported *) syntax_entry: [ [ IDENT "level"; p = precedence; ":"; OPT "|"; rl = LIST1 syntax_rule SEP "|" -> (p,rl) ] ] ; syntax_rule: [ [ nm = IDENT; "["; s = astpat; "]"; "->"; u = unparsing -> (nm,s,u) ] ] ; precedence: [ [ a = natural -> a (* | "["; a1 = natural; a2 = natural; a3 = natural; "]" -> (a1,a2,a3)*) ] ] ; unparsing: [ [ "["; ll = LIST0 next_hunks; "]" -> ll ] ] ; next_hunks: [ [ IDENT "FNL" -> UNP_FNL | IDENT "TAB" -> UNP_TAB | c = STRING -> RO c | "["; x = [ b = box; ll = LIST0 next_hunks -> UNP_BOX (b,ll) | n = natural; m = natural -> UNP_BRK (n, m) | IDENT "TBRK"; n = natural; m = natural -> UNP_TBRK (n, m) ]; "]" -> x | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln_or_extern -> pr ] -> match oprec with | Some (ext,pr) -> PH (e,ext,pr) | None -> PH (e,None,Any) ]] ; box: [ [ "<"; bk = box_kind; ">" -> bk ] ] ; box_kind: [ [ IDENT "h"; n = natural -> PpHB n | IDENT "v"; n = natural -> PpVB n | IDENT "hv"; n = natural -> PpHVB n | IDENT "hov"; n = natural -> PpHOVB n | IDENT "t" -> PpTB ] ] ; paren_reln_or_extern: [ [ IDENT "L" -> None, L | IDENT "E" -> None, E | pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] -> match precrec with | Some p -> Some pprim, Prec p | None -> Some pprim, Any ] ] ; (* meta-syntax entries *) astpat: [ [ "<<" ; a = Prim.ast; ">>" -> a | a = Constr.lconstr -> Termast.ast_of_rawconstr (Constrintern.interp_rawconstr Evd.empty (Global.env()) a) ] ] ; action: [ [ IDENT "let"; p = Prim.astlist; et = set_internal_entry_type; "="; e1 = action; "in"; e = action -> Ast.CaseAction (loc,e1,et,[p,e]) | IDENT "case"; a = action; et = set_internal_entry_type; "of"; cl = LIST1 case SEP "|"; IDENT "esac" -> Ast.CaseAction (loc,a,et,cl) | "["; a = default_action_parser; "]" -> Ast.SimpleAction (loc,a) ] ] ; case: [[ p = Prim.astlist; "->"; a = action -> (p,a) ]] ; set_internal_entry_type: [[ ":"; IDENT "ast"; IDENT "list" -> Ast.ETastl | [ ":"; IDENT "ast" -> () | -> () ] -> Ast.ETast ]] ; set_entry_type: [[ ":"; et = entry_type -> set_default_action_parser et | -> () ]] ; entry_type: [[ IDENT "ast"; IDENT "list" -> Util.error "type ast list no longer supported" | IDENT "ast" -> Util.error "type ast no longer supported" | IDENT "constr" -> ConstrParser | IDENT "pattern" -> CasesPatternParser | IDENT "tactic" -> assert false | IDENT "vernac" -> Util.error "vernac extensions no longer supported" ] ] ; END (* Reinstall tactic and vernac extensions *) let _ = Egrammar.reset_extend_grammars_v8()