diff options
Diffstat (limited to 'parsing/g_basevernac.ml4')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 524 |
1 files changed, 524 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 new file mode 100644 index 00000000..c4badbc3 --- /dev/null +++ b/parsing/g_basevernac.ml4 @@ -0,0 +1,524 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: g_basevernac.ml4,v 1.83.2.2 2004/07/16 19:30:37 herbelin Exp $ *) + +open Coqast +open Extend +open Ppextend +open Vernacexpr +open Pcoq +open Vernac_ +open Goptions +open Constr +open Prim + +let vernac_kw = + [ "Quit"; "Load"; "Compile"; "Fixpoint"; "CoFixpoint"; + "Definition"; "Inductive"; "CoInductive"; + "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis"; + "."; ">->" ] +let _ = + if !Options.v7 then + List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw + +let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" +let lstring = Gram.Entry.create "lstring" + + +if !Options.v7 then +GEXTEND Gram + GLOBAL: class_rawexpr; + + class_rawexpr: + [ [ IDENT "FUNCLASS" -> FunClass + | IDENT "SORTCLASS" -> SortClass + | qid = global -> RefClass qid ] ] + ; +END; + +if !Options.v7 then +GEXTEND Gram + GLOBAL: command lstring; + + lstring: + [ [ s = STRING -> s ] ] + ; + comment: + [ [ c = constr -> CommentConstr c + | s = STRING -> CommentString s + | n = natural -> CommentInt n ] ] + ; + command: + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l + + (* System directory *) + | IDENT "Pwd" -> VernacChdir None + | IDENT "Cd" -> VernacChdir None + | IDENT "Cd"; dir = lstring -> VernacChdir (Some dir) + + (* Toplevel control *) + | IDENT "Drop" -> VernacToplevelControl Drop + | IDENT "ProtectedLoop" -> VernacToplevelControl ProtectedLoop + | "Quit" -> VernacToplevelControl Quit + + (* Dump of the universe graph - to file or to stdout *) + | IDENT "Dump"; IDENT "Universes"; fopt = OPT lstring -> + VernacPrint (PrintUniverses fopt) + + | IDENT "Locate"; l = locatable -> VernacLocate l + + (* Managing load paths *) + | IDENT "Add"; IDENT "LoadPath"; dir = lstring; alias = as_dirpath -> + VernacAddLoadPath (false, dir, alias) + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = lstring; + alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) + | IDENT "Remove"; IDENT "LoadPath"; dir = lstring -> + VernacRemoveLoadPath dir + + (* For compatibility *) + | IDENT "AddPath"; dir = lstring; alias = as_dirpath -> + VernacAddLoadPath (false, dir, alias) + | IDENT "AddRecPath"; dir = lstring; alias = as_dirpath -> + VernacAddLoadPath (true, dir, alias) + | IDENT "DelPath"; dir = lstring -> + VernacRemoveLoadPath dir + + (* 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) + | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid) + + (* 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"; + sl = [ "["; l = LIST1 [ r = global -> SearchRef r + | s = lstring -> SearchString s ]; "]" -> l + | qid = global -> [SearchRef qid] ]; + l = in_or_out_modules -> + VernacSearch (SearchAbout sl, l) + + (* TODO: rapprocher Eval et Check *) + | IDENT "Eval"; r = Tactic.red_expr; "in"; + c = constr -> VernacCheckMayEval (Some r, None, c) + | IDENT "Check"; c = constr -> + VernacCheckMayEval (None, None, c) + | "Type"; c = constr -> VernacGlobalCheck c (* pas dans le RefMan *) + + | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = lstring -> + VernacAddMLPath (false, dir) + | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = lstring -> + VernacAddMLPath (true, dir) +(* + | IDENT "SearchIsos"; c = constr -> VernacSearch (SearchIsos c) +*) + + (* 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) ] ] + ; + printable: + [ [ IDENT "Term"; qid = global -> PrintOpaqueName 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 + | "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 + | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s + | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ] + ; + locatable: + [ [ qid = global -> LocateTerm qid + | IDENT "File"; f = lstring -> LocateFile f + | IDENT "Library"; qid = global -> LocateLibrary qid + | s = lstring -> LocateNotation s ] ] + ; + option_value: + [ [ n = integer -> IntValue n + | s = lstring -> StringValue s ] ] + ; + option_ref_value: + [ [ id = global -> QualidRefValue id + | s = lstring -> 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 [] ] ] + ; +END + +(* Grammar extensions *) + +(* automatic translation of levels *) +let adapt_level n = + if n >= 10 then n*10 else + [| 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100|].(n) + +let map_modl = function + | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n)) + | SetLevel n -> SetLevel(adapt_level n) + | m -> m + +if !Options.v7 then +GEXTEND Gram + GLOBAL: syntax; + + univ: + [ [ univ = IDENT -> + set_default_action_parser (parser_type_from_name univ); univ ] ] + ; + syntax: + [ [ IDENT "Token"; s = lstring -> + Pp.warning "Token declarations are now useless"; VernacNop + + | 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" -> + VernacGrammar (rename_command_entry u,tl) + + | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" -> + VernacSyntax (u,el) + + | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = lstring; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + (s8,mv8) = + [IDENT "V8only"; + s8=OPT lstring; + mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] -> + (s8,mv8) + | -> (None,None)] -> + let s8 = match s8 with Some s -> s | _ -> s in + let mv8 = match mv8 with + Some mv8 -> mv8 + | _ -> List.map map_modl modl in + VernacSyntaxExtension (local,Some (s,modl),Some(s8,mv8)) + + | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = lstring; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> + VernacSyntaxExtension (local,None,Some(s,modl)) + + | IDENT "Open"; local = locality; IDENT "Scope"; + sc = IDENT -> VernacOpenCloseScope (local,true, sc) + + | IDENT "Close"; local = locality; IDENT "Scope"; + sc = IDENT -> VernacOpenCloseScope (local,false,sc) + + | IDENT "Delimits"; 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 = lstring; + p = global; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc]; + mv8 = + [IDENT "V8only"; + a8=entry_prec; + n8=OPT natural; + op8=OPT lstring; + mv8=["("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> []] + -> + (match (a8,n8,mv8,op8) with + | None,None,[],None -> None + | _,_,mv8,_ -> + Some(op8,Metasyntax.merge_modifiers a8 n8 mv8)) + | -> (* Means: rules are based on V7 rules *) + Some (None,[]) ] -> + let mv = Metasyntax.merge_modifiers a n modl in + let v8 = Util.option_app (function (op8,mv8) -> + let op8 = match op8 with None -> op | Some op -> op in + let mv8 = + if mv8=[] then + let mv8 = List.map map_modl mv in + let mv8 = if List.for_all + (function SetLevel _ -> false | _ -> true) mv8 + then SetLevel 10 :: mv8 else mv8 in + let mv8 = if List.for_all + (function SetAssoc _ -> false | _ -> true) mv8 + then SetAssoc Gramext.LeftA :: mv8 else mv8 in + mv8 + else mv8 in + (op8,mv8)) mv8 in + VernacInfix (local,(op,mv),p,v8,sc) + | IDENT "Distfix"; local = locality; a = entry_prec; n = natural; + s = lstring; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] -> + let (a,s,c) = Metasyntax.translate_distfix a s p in + let mv = Some(s,[SetLevel n;SetAssoc a]) in + VernacNotation (local,c,mv,mv,sc) +(* + VernacDistfix (local,a,n,s,p,sc) +*) + | IDENT "Notation"; local = locality; id = ident; ":="; c = constr; + b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> + VernacSyntacticDefinition (id,c,local,b) + | IDENT "Notation"; local = locality; s = lstring; ":="; c = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ]; + (s8,mv8) = + [IDENT "V8only"; + s8=OPT lstring; + mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] -> + (s8,mv8) + | -> (* Means: rules are based on V7 rules *) + None, Some [] ] -> + let smv8 = match s8,mv8 with + | None, None -> None (* = only interpretation *) + | Some s8, None -> Some (s8,[]) (* = only interp, new s *) + | None, Some [] -> Some (s,List.map map_modl modl) (*like v7*) + | None, Some mv8 -> Some (s,mv8) (* s like v7 *) + | Some s8, Some mv8 -> Some (s8,mv8) in + VernacNotation (local,c,Some(s,modl),smv8,sc) + | IDENT "V8Notation"; local = locality; s = lstring; ":="; c = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacNotation (local,c,None,Some(s,modl),sc) + + | IDENT "V8Infix"; local = locality; op8 = lstring; p = global; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc] -> + let mv8 = Metasyntax.merge_modifiers None None modl in + VernacInfix (local,("",[]),p,Some (op8,mv8),sc) + + (* "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 ] ] + ; + 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 + | IDENT "format"; s = [s = lstring -> (loc,s)] -> SetFormat s ] ] + ; + syntax_extension_type: + [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference + | IDENT "bigint" -> ETBigint + | i=IDENT -> ETOther ("constr",i) + ] ] + ; + 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 = lstring; pil = LIST0 production_item; "]"; + "->"; "["; t = Tactic.tactic; "]" -> (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 = lstring -> VTerm s + | nt = non_terminal; po = OPT [ "("; p = METAIDENT; ")" -> p ] -> + match po with + | Some p -> VNonTerm (loc,nt,Some (Names.id_of_string p)) + | _ -> VNonTerm (loc,nt,None) ]] + ; + 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 = lstring -> 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 = lstring; 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.constr -> + 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 |