diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 941 |
1 files changed, 580 insertions, 361 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 87183e18..18a424a8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,35 +6,39 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_vernac.ml4,v 1.93.2.3 2004/10/12 10:11:28 herbelin Exp $ *) +(* $Id: g_vernac.ml4 8624 2006-03-13 17:38:17Z msozeau $ *) +(*i camlp4deps: "parsing/grammar.cma" i*) +open Pp +open Util open Names open Topconstr open Vernacexpr open Pcoq -open Pp open Tactic -open Util -open Constr -open Vernac_ -open Prim open Decl_kinds - open Genarg +open Extend +open Ppextend +open Goptions -let evar_constr loc = CHole loc +open Prim +open Constr +open Vernac_ +open Module -let class_rawexpr = G_basevernac.class_rawexpr -let thm_token = G_proofs.thm_token +let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] +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 filter_com (b,e) = - let (b,e) = unloc (b,e) in - Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments +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" -if !Options.v7 then +let no_hook _ _ = () GEXTEND Gram GLOBAL: vernac gallina_ext; vernac: @@ -44,163 +48,121 @@ GEXTEND Gram | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c - | n = natural; ":"; tac = Tactic.tactic; "." -> VernacSolve (n,tac,true) - | n = natural; ":"; tac = Tactic.tactic; "!!" -> VernacSolve (n,tac,false) - | n = natural; ":"; v = check_command; "." -> v (Some n) - | "["; l = vernac_list_tail -> VernacList l - - (* For translation from V7 to V8 *) - | IDENT "V7only"; v = vernac -> - filter_com loc; VernacV7only v - | IDENT "V8only"; v = vernac -> VernacV8only v - -(* - (* This is for "Grammar vernac" rules *) - | id = METAIDENT -> VernacVar (Names.id_of_string id) -*) + | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l ] ] ; - - check_command: - [ [ 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) ] ] - ; vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v ] ] ; vernac: LAST - [ [ tac = Tactic.tactic; "." -> VernacSolve (1,tac,true) - | tac = Tactic.tactic; "!!" -> VernacSolve (1,tac,false) - | IDENT "Existential"; n = natural; c = constr_body -> - VernacSolveExistential (n,c) - ] ] - ; - constr_body: - [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,t) - | ":"; t = constr; ":="; c = constr -> CCast(loc,c,t) - | ":="; c = constr -> c ] ] + [ [ gln = OPT[n=natural; ":" -> n]; + tac = subgoal_command -> tac gln ] ] ; - vernac_list_tail: - [ [ v = located_vernac; l = vernac_list_tail -> v :: l - | "]"; "." -> [] ] ] + subgoal_command: + [ [ c = check_command; "." -> c + | tac = Tactic.tactic; + use_dft_tac = [ "." -> false | "..." -> true ] -> + (fun g -> + let g = match g with Some gl -> gl | _ -> 1 in + VernacSolve(g,tac,use_dft_tac)) ] ] ; located_vernac: [ [ v = vernac -> loc, v ] ] ; END + let test_plurial_form = function - | [_,([_],_)] -> + | [(_,([_],_))] -> Options.if_verbose warning - "Keywords Variables/Hypotheses/Parameters expect more than one assumption" + "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 + (* Gallina declarations *) -if !Options.v7 then GEXTEND Gram - GLOBAL: gallina gallina_ext thm_token; + GLOBAL: gallina gallina_ext thm_token def_body; + gallina: + (* Definition, Theorem, Variable, Axiom, ... *) + [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":"; + c = lconstr -> + VernacStartTheoremProof (thm, id, (bl, c), false, no_hook) + | stre = assumption_token; bl = assum_list -> + VernacAssumption (stre, bl) + | stre = assumptions_token; bl = assum_list -> + test_plurial_form bl; + VernacAssumption (stre, bl) + | IDENT "Boxed";"Definition";id = identref; b = def_body -> + VernacDefinition ((Global,true,Definition), id, b, no_hook) + | IDENT "Unboxed";"Definition";id = identref; b = def_body -> + VernacDefinition ((Global,false,Definition), id, b, no_hook) + | (f,d) = def_token; id = identref; b = def_body -> + VernacDefinition (d, id, b, f) + (* Gallina inductive declarations *) + | f = finite_token; + indl = LIST1 inductive_definition SEP "with" -> + VernacInductive (f,indl) + | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (recs,true) + | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (recs,false) + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (recs,Options.boxed_definitions()) + | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (corecs,false) + | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] + ; + gallina_ext: + [ [ b = record_token; oc = opt_coercion; name = identref; + ps = LIST0 binder_let; ":"; + s = lconstr; ":="; cstr = OPT identref; "{"; + fs = LIST0 record_field SEP ";"; "}" -> + VernacRecord (b,(oc,name),ps,s,cstr,fs) +(* Non porté ? + | f = finite_token; s = csort; id = identref; + 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 ] ] + | IDENT "Remark" -> Remark + | IDENT "Corollary" -> Corollary + | IDENT "Proposition" -> Proposition + | IDENT "Property" -> Property ] ] ; def_token: - [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition) - | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition) - | IDENT "SubClass" -> Class.add_subclass_hook, (Global, SubClass) + [ [ "Definition" -> + no_hook, (Global, Options.boxed_definitions(), Definition) + | IDENT "Let" -> + no_hook, (Local, Options.boxed_definitions(), Definition) + | IDENT "Example" -> + no_hook, (Global, Options.boxed_definitions(), Example) + | IDENT "SubClass" -> Class.add_subclass_hook, (Global, false, SubClass) | IDENT "Local"; IDENT "SubClass" -> - Class.add_subclass_hook, (Local, SubClass) ] ] + Class.add_subclass_hook, (Local, false, SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) | "Variable" -> (Local, Definitional) | "Axiom" -> (Global, Logical) | "Parameter" -> (Global, Definitional) - | IDENT "Conjecture" -> (Global,Conjectural) ] ] + | IDENT "Conjecture" -> (Global, Conjectural) ] ] ; assumptions_token: [ [ IDENT "Hypotheses" -> (Local, Logical) | IDENT "Variables" -> (Local, Definitional) + | IDENT "Axioms" -> (Global, Logical) | IDENT "Parameters" -> (Global, Definitional) ] ] ; - of_type_with_opt_coercion: - [ [ ":>" -> true - | ":"; ">" -> true - | ":" -> false ] ] - ; - params: - [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; - c = constr -> (coe,(idl,c)) - ] ] - ; - ne_params_list: - [ [ ll = LIST1 params SEP ";" -> ll ] ] - ; - name_comma_list_tail: - [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ] - ; - ident_comma_list_tail: - [ [ ","; nal = LIST1 identref SEP "," -> nal | -> [] ] ] - ; - decl_notation: - [ [ "where"; ntn = STRING; ":="; c = constr; - scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] - ; - type_option: - [ [ ":"; c = constr -> c - | -> evar_constr loc ] ] - ; - opt_casted_constr: - [ [ c = constr; ":"; t = constr -> CCast(loc,c,t) - | c = constr -> c ] ] - ; - vardecls: - [ [ na = name; nal = name_comma_list_tail; c = type_option - -> LocalRawAssum (na::nal,c) - | na = name; "="; c = opt_casted_constr -> - LocalRawDef (na,c) - | na = name; ":="; c = opt_casted_constr -> - LocalRawDef (na,c) - ] ] - ; - binders: - [ [ "["; bl = LIST1 vardecls SEP ";"; "]" -> bl ] ] - ; - binders_list: - [ [ bls = LIST0 binders -> List.flatten bls ] ] - ; - reduce: - [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r - | -> None ] ] - ; - def_body: - [ [ bl = binders_list; ":="; red = reduce; c = constr; ":"; t = constr -> - DefineBody (bl, red, c, Some t) - | bl = binders_list; ":"; t = constr; ":="; red = reduce; c = constr -> - DefineBody (bl, red, c, Some t) - | bl = binders_list; ":="; red = reduce; c = constr -> - DefineBody (bl, red, c, None) - | bl = binders_list; ":"; t = constr -> - ProveBody (bl, t) ] ] - ; - gallina: - (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = identref; bl = binders_list; ":"; c = constr -> - VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) - | (f,d) = def_token; id = identref; b = def_body -> - VernacDefinition (d, id, b, f) - | stre = assumption_token; bl = ne_params_list -> - VernacAssumption (stre, bl) - | stre = assumptions_token; bl = ne_params_list -> - test_plurial_form bl; - VernacAssumption (stre, bl) - ] ] - ; - (* Gallina inductive declarations *) finite_token: [ [ "Inductive" -> true | "CoInductive" -> false ] ] @@ -208,192 +170,250 @@ GEXTEND Gram record_token: [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ] ; - constructor: - [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; - c = constr -> List.map (fun id -> (coe,(id,c))) idl ] ] - ; - constructor_list: - [ [ "|"; l = LIST1 constructor SEP "|" -> List.flatten l - | l = LIST1 constructor SEP "|" -> List.flatten l - | -> [] ] ] - ; - block_old_style: - [ [ ind = oneind_old_style; "with"; indl = block_old_style -> ind :: indl - | ind = oneind_old_style -> [ind] ] ] + (* Simple definitions *) + def_body: + [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> + (match c with + CCast(_,c,k,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) ] ] ; - oneind_old_style: - [ [ id = identref; ":"; c = constr; ":="; lc = constructor_list -> - (id,c,lc) ] ] + reduce: + [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r + | -> None ] ] ; - oneind: - [ [ id = identref; indpar = simple_binders_list; ":"; c = constr; - ":="; lc = constructor_list; ntn = OPT decl_notation -> + decl_notation: + [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr; + scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ] + ; + (* Inductives and records *) + inductive_definition: + [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; + ":="; lc = constructor_list; ntn = decl_notation -> (id,ntn,indpar,c,lc) ] ] ; - simple_binders_list: - [ [ bl = ne_simple_binders_list -> bl + constructor_list: + [ [ "|"; l = LIST1 constructor SEP "|" -> l + | l = LIST1 constructor SEP "|" -> l | -> [] ] ] ; +(* + csort: + [ [ s = sort -> CSort (loc,s) ] ] + ; +*) opt_coercion: [ [ ">" -> true | -> false ] ] ; - onescheme: - [ [ id = identref; ":="; dep = dep; ind = global; IDENT "Sort"; - s = sort -> (id,dep,ind,s) ] ] - ; - schemes: - [ [ recl = LIST1 onescheme SEP "with" -> recl ] ] - ; - dep: - [ [ IDENT "Induction"; IDENT "for" -> true - | IDENT "Minimality"; IDENT "for" -> false ] ] + (* (co)-fixpoints *) + rec_definition: + [ [ id = ident; bl = LIST1 binder_let; + annot = rec_annotation; type_ = type_cstr; + ":="; def = lconstr; ntn = decl_notation -> + let names = List.map snd (names_of_local_assums bl) in + let ni = + match fst 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 + ((id, (ni, snd annot), bl, type_, def),ntn) ] ] + ; + corec_definition: + [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":="; + def = lconstr -> + (id,bl,c ,def) ] ] + ; + rec_annotation: + [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) + | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) + | -> (None, CStructRec) + ] ] ; - onerec: - [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr; - ":="; def = constr; ntn = OPT decl_notation -> - let ni = List.length (List.flatten (List.map fst bl)) - 1 in - let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in - ((id, ni, bl, type_, def), ntn) ] ] + type_cstr: + [ [ ":"; c=lconstr -> c + | -> CHole loc ] ] ; - specifrec: - [ [ l = LIST1 onerec SEP "with" -> l ] ] + (* Inductive schemes *) + scheme: + [ [ id = identref; ":="; dep = dep_scheme; "for"; ind = global; + IDENT "Sort"; s = sort -> + (id,dep,ind,s) ] ] ; - onecorec: - [ [ id = base_ident; ":"; c = constr; ":="; def = constr -> - (id,[],c,def) ] ] + dep_scheme: + [ [ IDENT "Induction" -> true + | IDENT "Minimality" -> false ] ] ; - specifcorec: - [ [ l = LIST1 onecorec SEP "with" -> l ] ] + (* 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 = name; oc = of_type_with_opt_coercion; t = constr -> - (oc,AssumExpr (id,t)) - | id = name; oc = of_type_with_opt_coercion; t = constr; - ":="; b = constr -> - (oc,DefExpr (id,b,Some t)) - | id = name; ":="; b = constr -> - (false,DefExpr (id,b,None)) ] ] - ; - fields: - [ [ fs = LIST0 record_field SEP ";" -> fs ] ] - ; - simple_binders: - [ [ "["; bll = LIST1 vardecls SEP ";"; "]" -> bll ] ] - ; - ne_simple_binders_list: - [ [ bll = LIST1 simple_binders -> (List.flatten bll) ] ] - ; - fix_params: - [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c) - | idl = LIST1 name SEP "," -> (idl, evar_constr dummy_loc) - ] ] - ; - fix_binders: - [ [ "["; bll = LIST1 fix_params SEP ";"; "]" -> bll ] ] - ; - ne_fix_binders: - [ [ bll = LIST1 fix_binders -> List.flatten bll ] ] + [ [ id = name -> (false,AssumExpr(id,CHole loc)) + | id = name; oc = of_type_with_opt_coercion; t = lconstr -> + (oc,AssumExpr (id,t)) + | id = name; oc = of_type_with_opt_coercion; + t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) + | id = name; ":="; 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 identref; oc = of_type_with_opt_coercion; c = lconstr -> + (oc,(idl,c)) ] ] ; - rec_constructor: - [ [ c = identref -> Some c - | -> None ] ] - ; - gallina_ext: - [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token; - indl = block_old_style -> - let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in - VernacInductive (f,indl') - | b = record_token; oc = opt_coercion; name = identref; - ps = simple_binders_list; ":"; - s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" -> - VernacRecord (b,(oc,name),ps,s,c,fs) - ] ] - ; - gallina: - [ [ IDENT "Mutual"; f = finite_token; indl = LIST1 oneind SEP "with" -> - VernacInductive (f,indl) - | f = finite_token; indl = LIST1 oneind SEP "with" -> - VernacInductive (f,indl) - | "Fixpoint"; recs = specifrec -> VernacFixpoint recs - | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs - | IDENT "Scheme"; l = schemes -> VernacScheme l - | f = finite_token; s = csort; id = identref; - indpar = simple_binders_list; ":="; lc = constructor_list -> - VernacInductive (f,[id,None,indpar,s,lc]) ] ] + constructor: + [ [ id = identref; l = LIST0 binder_let; + coe = of_type_with_opt_coercion; c = lconstr -> + (coe,(id,G_constr.mkCProdN loc l c)) + | id = identref; l = LIST0 binder_let -> + (false,(id,G_constr.mkCProdN loc l (CHole loc))) ] ] ; - csort: - [ [ s = sort -> CSort (loc,s) ] ] + of_type_with_opt_coercion: + [ [ ":>" -> true + | ":"; ">" -> true + | ":" -> false ] ] ; +END + + +(* Modules and Sections *) +GEXTEND Gram + GLOBAL: gallina_ext module_expr module_type; + gallina_ext: - [ [ -(* Sections *) - IDENT "Section"; id = identref -> VernacBeginSection id - | IDENT "Chapter"; id = identref -> VernacBeginSection id ] ] - ; - module_vardecls: - [ [ id = identref; idl = ident_comma_list_tail; ":"; - mty = Module.module_type -> (id::idl,mty) ] ] + [ [ (* Interactive module declaration *) + IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; mty_o = OPT of_module_type; + mexpr_o = OPT is_module_expr -> + VernacDefineModule (export, id, bl, mty_o, mexpr_o) + + | IDENT "Module"; "Type"; id = identref; + bl = LIST0 module_binder; mty_o = OPT is_module_type -> + VernacDeclareModuleType (id, bl, mty_o) + + | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; mty_o = of_module_type -> + VernacDeclareModule (export, id, bl, mty_o) + (* 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 + + (* 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 = ne_string -> + VernacRequireFrom (export, specif, filename) + | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) + | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) ] ] ; - module_binders: - [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ] + export_token: + [ [ IDENT "Import" -> Some false + | IDENT "Export" -> Some true + | -> None ] ] ; - module_binders_list: - [ [ bls = LIST0 module_binders -> List.flatten bls ] ] + specif_token: + [ [ IDENT "Implementation" -> Some false + | IDENT "Specification" -> Some true + | -> None ] ] ; of_module_type: - [ [ ":"; mty = Module.module_type -> (mty, true) - | "<:"; mty = Module.module_type -> (mty, false) ] ] + [ [ ":"; mty = module_type -> (mty, true) + | "<:"; mty = module_type -> (mty, false) ] ] ; is_module_type: - [ [ ":="; mty = Module.module_type -> mty ] ] + [ [ ":="; mty = module_type -> mty ] ] ; is_module_expr: - [ [ ":="; mexpr = Module.module_expr -> mexpr ] ] + [ [ ":="; mexpr = module_expr -> mexpr ] ] ; - gallina_ext: - [ [ - (* Interactive module declaration *) - IDENT "Module"; id = identref; - bl = module_binders_list; mty_o = OPT of_module_type; - mexpr_o = OPT is_module_expr -> - VernacDefineModule (id, bl, mty_o, mexpr_o) - - | IDENT "Module"; "Type"; id = identref; - bl = module_binders_list; mty_o = OPT is_module_type -> - VernacDeclareModuleType (id, bl, mty_o) - - | IDENT "Declare"; IDENT "Module"; id = identref; - bl = module_binders_list; mty_o = OPT of_module_type; - mexpr_o = OPT is_module_expr -> - VernacDeclareModule (id, bl, mty_o, mexpr_o) - (* This end a Section a Module or a Module Type *) + (* Module binder *) + module_binder: + [ [ "("; export = export_token; idl = LIST1 identref; ":"; + mty = module_type; ")" -> (export,idl,mty) ] ] + ; - | IDENT "End"; id = identref -> VernacEndSegment id + (* Module expressions *) + module_expr: + [ [ qid = qualid -> CMEident qid + | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2) + | "("; 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 -> CMTEident qid +(* ... *) + | mty = module_type; "with"; decl = with_declaration -> + CMTEwith (mty,decl) ] ] + ; +END +(* Extensions: implicits, coercions, etc. *) +GEXTEND Gram + GLOBAL: gallina_ext; -(* Transparent and Opaque *) - | IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l) + gallina_ext: + [ [ (* Transparent and Opaque *) + IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l) | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l) -(* Canonical structure *) + (* 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 + let s = coerce_global_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook) - (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed - (they were unused and undocumented) *) + ((Global,false,CanonicalStructure),(dummy_loc,s),d, + (fun _ -> Recordops.declare_canonical_structure)) -(* Coercions *) + (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> - let s = Ast.coerce_global_to_id qid in - VernacDefinition ((Global,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + let s = coerce_global_to_id qid in + VernacDefinition ((Global,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> - let s = Ast.coerce_global_to_id qid in - VernacDefinition ((Local,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + let s = coerce_global_to_id qid in + VernacDefinition ((Local,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (Local, f, s, t) @@ -406,114 +426,230 @@ GEXTEND Gram | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (Global, qid, s, t) - | IDENT "Class"; IDENT "Local"; c = global -> - Pp.warning "Class is obsolete"; VernacNop - | IDENT "Class"; c = global -> - Pp.warning "Class is obsolete"; VernacNop -(* Implicit *) -(* - | IDENT "Syntactic"; "Definition"; id = identref; ":="; c = constr; - n = OPT [ "|"; n = natural -> n ] -> - VernacSyntacticDefinition (id,c,n) -*) - | IDENT "Syntactic"; "Definition"; id = ident; ":="; c = constr; - n = OPT [ "|"; n = natural -> n ] -> - let c = match n with - | Some n -> - let l = list_tabulate (fun _ -> (CHole (loc),None)) n in - CApp (loc,(None,c),l) - | None -> c in - VernacSyntacticDefinition (id,c,false,true) - | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> - let l = List.map (fun n -> ExplByPos n) l in - VernacDeclareImplicits (qid,Some l) - | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None) - - | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"]; - idl = LIST1 identref SEP ","; ":"; c = constr -> 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) - ] ] + (* Implicit *) + | IDENT "Implicit"; IDENT "Arguments"; qid = global; + pos = OPT [ "["; l = LIST0 ident; "]" -> l ] -> + let pos = option_app (List.map (fun id -> ExplByName id)) pos in + VernacDeclareImplicits (qid,pos) + + | IDENT "Implicit"; ["Type" | IDENT "Types"]; + idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] ; END -(* Modules management *) -if !Options.v7 then GEXTEND Gram - GLOBAL: command; + GLOBAL: command check_command class_rawexpr; - export_token: - [ [ IDENT "Import" -> false - | IDENT "Export" -> true - | -> false ] ] - ; - specif_token: - [ [ IDENT "Implementation" -> Some false - | IDENT "Specification" -> Some true - | -> None ] ] - ; command: - [ [ "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; - s = [ s = STRING -> s | s = IDENT -> s ] -> + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l + + (* 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 "ProtectedLoop" -> VernacToplevelControl ProtectedLoop + | IDENT "Quit" -> VernacToplevelControl Quit + + | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; + s = [ s = ne_string -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) -(* | "Compile"; - verbosely = - [ IDENT "Verbose" -> "Verbose" - | -> "" ]; - IDENT "Module"; - only_spec = - [ IDENT "Specification" -> "Specification" - | -> "" ]; - mname = [ s = STRING -> s | s = IDENT -> s ]; - fname = OPT [ s = STRING -> s | s = IDENT -> s ] -> ExtraVernac - let fname = match fname with Some s -> s | None -> mname in - <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec) - ($STR $mname) ($STR $fname))>> -*) - | IDENT "Read"; IDENT "Module"; qidl = LIST1 global -> - VernacRequire (None, None, qidl) - | IDENT "Require"; export = export_token; specif = specif_token; - qidl = LIST1 global -> VernacRequire (Some export, specif, qidl) -(* | IDENT "Require"; export = export_token; specif = specif_token; - id = identref; filename = STRING -> - VernacRequireFrom (export, specif, id, filename) *) - | IDENT "Require"; export = export_token; specif = specif_token; - filename = STRING -> - VernacRequireFrom (Some export, specif, filename) - | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING -> + | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> VernacDeclareMLModule l - | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) - | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - ] -] + + (* Dump of the universe graph - to file or to stdout *) + | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string -> + VernacPrint (PrintUniverses fopt) + + | 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 = global -> VernacPrint (PrintName qid) + | 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 = ne_string -> SearchString s ]; "]" -> l + | qid = global -> [SearchRef qid] ]; + l = in_or_out_modules -> + VernacSearch (SearchAbout sl, l) + + | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> + VernacAddMLPath (false, dir) + | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> + VernacAddMLPath (true, dir) + + (* Pour intervenir sur les tables de paramètres *) + | "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) ] ] ; -END + check_command: (* TODO: rapprocher Eval et Check *) + [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> + fun g -> VernacCheckMayEval (Some r, g, c) + | IDENT "Check"; c = lconstr -> + fun g -> VernacCheckMayEval (None, g, c) ] ] + ; + printable: + [ [ IDENT "Term"; qid = 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" -> PrintLoadPath + | IDENT "Modules" -> PrintModules -if !Options.v7 then -GEXTEND Gram - GLOBAL: command; + | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath + | IDENT "ML"; IDENT "Modules" -> PrintMLModules + | IDENT "Graph" -> PrintGraph + | IDENT "Classes" -> PrintClasses + | IDENT "Ltac"; qid = global -> PrintLtac 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 +(* Obsolete: was used for cooking V6.3 recipes ?? + | IDENT "Proof"; qid = global -> PrintOpaqueName qid +*) + | IDENT "Hint" -> PrintHintGoal + | IDENT "Hint"; qid = global -> PrintHint qid + | IDENT "Hint"; "*" -> PrintHintDb + | IDENT "HintDb"; s = IDENT -> PrintHintDbName s + | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s + | IDENT "Setoids" -> PrintSetoids + | IDENT "Scopes" -> PrintScopes + | IDENT "Scope"; s = IDENT -> PrintScope s + | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s + | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ] + ; + class_rawexpr: + [ [ IDENT "Funclass" -> FunClass + | IDENT "Sortclass" -> SortClass + | qid = global -> RefClass qid ] ] + ; + locatable: + [ [ qid = global -> LocateTerm qid + | IDENT "File"; f = ne_string -> LocateFile f + | IDENT "Library"; qid = global -> LocateLibrary qid + | IDENT "Module"; qid = global -> LocateModule qid + | s = ne_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 "Write"; IDENT "State"; s = ne_string -> VernacWriteState s | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s - | IDENT "Restore"; IDENT "State"; s = STRING -> VernacRestoreState s + | IDENT "Restore"; IDENT "State"; s = ne_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 + | IDENT "BackTo"; n = natural -> VernacBackTo n + | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> + VernacBacktrack (n,m,p) (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> VernacDebug true @@ -522,3 +658,86 @@ GEXTEND Gram ] ]; END ;; + +(* Grammar extensions *) + +GEXTEND Gram + GLOBAL: syntax; + + syntax: + [ [ 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 "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; + op = ne_string; ":="; p = global; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacInfix (local,(op,modl),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 = ne_string; ":="; c = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacNotation (local,c,(s,modl),sc) + + | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; + pil = LIST1 production_item; ":="; t = Tactic.tactic + -> VernacTacticNotation (n,pil,t) + + | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; + 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 *) + ] ] + ; + tactic_level: + [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] + ; + locality: + [ [ IDENT "Local" -> true | -> false ] ] + ; + level: + [ [ IDENT "level"; n = natural -> NumLevel n + | IDENT "next"; IDENT "level" -> NextLevel ] ] + ; + syntax_modifier: + [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; + lev = level -> SetItemLevel (x::l,lev) + | "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 = STRING -> (loc,s)] -> SetFormat s ] ] + ; + syntax_extension_type: + [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference + | IDENT "bigint" -> ETBigint + ] ] + ; + opt_scope: + [ [ "_" -> None | sc = IDENT -> Some sc ] ] + ; + production_item: + [ [ s = ne_string -> VTerm s + | nt = IDENT; po = OPT [ "("; p = ident; ")" -> p ] -> + VNonTerm (loc,nt,po) ] ] + ; +END |