(************************************************************************)
(* 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