diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 524 |
1 files changed, 524 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 new file mode 100644 index 00000000..e2eecf55 --- /dev/null +++ b/parsing/g_vernac.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_vernac.ml4,v 1.93.2.2 2004/07/16 20:51:12 herbelin Exp $ *) + +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 + +let evar_constr loc = CHole loc + +let class_rawexpr = G_basevernac.class_rawexpr +let thm_token = G_proofs.thm_token + +(* 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 + +if !Options.v7 then +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 + | 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) +*) + ] ] + ; + + 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 ] ] + ; + vernac_list_tail: + [ [ v = located_vernac; l = vernac_list_tail -> v :: l + | "]"; "." -> [] ] ] + ; + 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" + | _ -> () + +(* Gallina declarations *) +if !Options.v7 then +GEXTEND Gram + GLOBAL: gallina gallina_ext thm_token; + + thm_token: + [ [ "Theorem" -> Theorem + | IDENT "Lemma" -> Lemma + | IDENT "Fact" -> Fact + | IDENT "Remark" -> Remark ] ] + ; + def_token: + [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition) + | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition) + | IDENT "SubClass" -> Class.add_subclass_hook, (Global, SubClass) + | IDENT "Local"; IDENT "SubClass" -> + Class.add_subclass_hook, (Local, SubClass) ] ] + ; + assumption_token: + [ [ "Hypothesis" -> (Local, Logical) + | "Variable" -> (Local, Definitional) + | "Axiom" -> (Global, Logical) + | "Parameter" -> (Global, Definitional) + | IDENT "Conjecture" -> (Global,Conjectural) ] ] + ; + assumptions_token: + [ [ IDENT "Hypotheses" -> (Local, Logical) + | IDENT "Variables" -> (Local, Definitional) + | 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; ":"; c = constr -> + VernacStartTheoremProof (thm, id, ([], 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 ] ] + ; + 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] ] ] + ; + oneind_old_style: + [ [ id = identref; ":"; c = constr; ":="; lc = constructor_list -> + (id,c,lc) ] ] + ; + oneind: + [ [ id = identref; indpar = simple_binders_list; ":"; c = constr; + ":="; lc = constructor_list; ntn = OPT decl_notation -> + (id,ntn,indpar,c,lc) ] ] + ; + simple_binders_list: + [ [ bl = ne_simple_binders_list -> bl + | -> [] ] ] + ; + 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 ] ] + ; + 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) ] ] + ; + specifrec: + [ [ l = LIST1 onerec SEP "with" -> l ] ] + ; + onecorec: + [ [ id = base_ident; ":"; c = constr; ":="; def = constr -> + (id,[],c,def) ] ] + ; + specifcorec: + [ [ l = LIST1 onecorec SEP "with" -> l ] ] + ; + 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 ] ] + ; + 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]) ] ] + ; + csort: + [ [ s = sort -> CSort (loc,s) ] ] + ; + 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) ] ] + ; + module_binders: + [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ] + ; + module_binders_list: + [ [ bls = LIST0 module_binders -> List.flatten bls ] ] + ; + of_module_type: + [ [ ":"; mty = Module.module_type -> (mty, true) + | "<:"; mty = Module.module_type -> (mty, false) ] ] + ; + is_module_type: + [ [ ":="; mty = Module.module_type -> mty ] ] + ; + is_module_expr: + [ [ ":="; mexpr = Module.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 *) + + | IDENT "End"; id = identref -> VernacEndSegment id + + +(* 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,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook) + (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed + (they were unused and undocumented) *) + +(* 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) + | 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) + | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; + ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> + VernacIdentityCoercion (Local, f, s, t) + | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; + 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) + | 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) + ] ] + ; +END + +(* Modules management *) +if !Options.v7 then +GEXTEND Gram + GLOBAL: command; + + 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 ] -> + 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 -> + VernacDeclareMLModule l + | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) + | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) + ] +] + ; +END + +if !Options.v7 then +GEXTEND Gram + GLOBAL: command; + + 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 +;; |