diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramml.ml | 2 | ||||
| -rw-r--r-- | vernac/g_proofs.ml4 | 134 | ||||
| -rw-r--r-- | vernac/g_vernac.ml4 | 1154 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 10 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 56 | ||||
| -rw-r--r-- | vernac/pvernac.mli | 36 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 533 |
10 files changed, 1925 insertions, 8 deletions
diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 90cd7d10b..048d4d93a 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -77,7 +77,7 @@ let get_extend_vernac_rule (s, i) = | Failure _ -> raise Not_found let extend_vernac_command_grammar s nt gl = - let nt = Option.default Vernac_.command nt in + let nt = Option.default Pvernac.Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4 new file mode 100644 index 000000000..56229c765 --- /dev/null +++ b/vernac/g_proofs.ml4 @@ -0,0 +1,134 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Constrexpr +open Vernacexpr +open Proof_global +open Misctypes + +open Pcoq +open Pcoq.Prim +open Pcoq.Constr +open Pvernac.Vernac_ + +let thm_token = G_vernac.thm_token + +let hint = Gram.entry_create "hint" + +let warn_deprecated_focus = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.strbrk + "The Focus command is deprecated; use bullets or focusing brackets instead" + ) + +let warn_deprecated_focus_n n = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.(str "The Focus command is deprecated;" ++ spc () + ++ str "use '" ++ int n ++ str ": {' instead") + ) + +let warn_deprecated_unfocus = + CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" + (fun () -> Pp.strbrk "The Unfocus command is deprecated") + +(* Proof commands *) +GEXTEND Gram + GLOBAL: hint command; + + opt_hintbases: + [ [ -> [] + | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] + ; + command: + [ [ IDENT "Goal"; c = lconstr -> + VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) + | IDENT "Proof" -> VernacProof (None,None) + | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn + | IDENT "Proof"; c = lconstr -> VernacExactProof c + | IDENT "Abort" -> VernacAbort None + | IDENT "Abort"; IDENT "All" -> VernacAbortAll + | IDENT "Abort"; id = identref -> VernacAbort (Some id) + | IDENT "Existential"; n = natural; c = constr_body -> + VernacSolveExistential (n,c) + | IDENT "Admitted" -> VernacEndProof Admitted + | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None)) + | IDENT "Save"; id = identref -> + VernacEndProof (Proved (Opaque, Some id)) + | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) + | IDENT "Defined"; id=identref -> + VernacEndProof (Proved (Transparent,Some id)) + | IDENT "Restart" -> VernacRestart + | IDENT "Undo" -> VernacUndo 1 + | IDENT "Undo"; n = natural -> VernacUndo n + | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n + | IDENT "Focus" -> + warn_deprecated_focus ~loc:!@loc (); + VernacFocus None + | IDENT "Focus"; n = natural -> + warn_deprecated_focus_n n ~loc:!@loc (); + VernacFocus (Some n) + | IDENT "Unfocus" -> + warn_deprecated_unfocus ~loc:!@loc (); + VernacUnfocus + | IDENT "Unfocused" -> VernacUnfocused + | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) + | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) + | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) + | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript + | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials + | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses + | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames + | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof + | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) + | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) + | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) + | IDENT "Guarded" -> VernacCheckGuard + (* Hints for Auto and EAuto *) + | IDENT "Create"; IDENT "HintDb" ; + id = IDENT ; b = [ "discriminated" -> true | -> false ] -> + VernacCreateHintDb (id, b) + | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> + VernacRemoveHints (dbnames, ids) + | IDENT "Hint"; h = hint; + dbnames = opt_hintbases -> + VernacHints (dbnames, h) + (* Declare "Resolve" explicitly so as to be able to later extend with + "Resolve ->" and "Resolve <-" *) + | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; + info = hint_info; dbnames = opt_hintbases -> + VernacHints (dbnames, + HintsResolve (List.map (fun x -> (info, true, x)) lc)) + ] ]; + reference_or_constr: + [ [ r = global -> HintsReference r + | c = constr -> HintsConstr c ] ] + ; + hint: + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> + HintsResolve (List.map (fun x -> (info, true, x)) lc) + | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc + | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) + | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) + | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) + | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid + | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ] + ; + constr_body: + [ [ ":="; c = lconstr -> c + | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ] + ; + mode: + [ [ l = LIST1 [ "+" -> ModeInput + | "!" -> ModeNoHeadEvar + | "-" -> ModeOutput ] -> l ] ] + ; +END diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 new file mode 100644 index 000000000..6c7df8cfa --- /dev/null +++ b/vernac/g_vernac.ml4 @@ -0,0 +1,1154 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Names +open Vernacexpr +open Constrexpr +open Constrexpr_ops +open Extend +open Decl_kinds +open Declaremods +open Declarations +open Misctypes +open Tok (* necessary for camlp5 *) + +open Pcoq +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Module +open Pvernac.Vernac_ + +let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] +let _ = List.iter CLexer.add_keyword vernac_kw + +(* Rem: do not join the different GEXTEND into one, it breaks native *) +(* compilation on PowerPC and Sun architectures *) + +let query_command = Gram.entry_create "vernac:query_command" + +let subprf = Gram.entry_create "vernac:subprf" + +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" +let decl_notation = Gram.entry_create "vernac:decl_notation" +let record_field = Gram.entry_create "vernac:record_field" +let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" +let instance_name = Gram.entry_create "vernac:instance_name" +let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" + +let make_bullet s = + let open Proof_bullet in + let n = String.length s in + match s.[0] with + | '-' -> Dash n + | '+' -> Plus n + | '*' -> Star n + | _ -> assert false + +let parse_compat_version ?(allow_old = true) = let open Flags in function + | "8.8" -> Current + | "8.7" -> V8_7 + | "8.6" -> V8_6 + | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + CErrors.user_err ~hdr:"get_compat_version" + Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") + | s -> + CErrors.user_err ~hdr:"get_compat_version" + Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") + +GEXTEND Gram + GLOBAL: vernac_control gallina_ext noedit_mode subprf; + vernac_control: FIRST + [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c) + | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) + | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v) + | IDENT "Fail"; v = vernac_control -> VernacFail v + | (f, v) = vernac -> VernacExpr(f, v) ] + ] + ; + vernac: + [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v) + | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v) + + | v = vernac_poly -> v ] + ] + ; + vernac_poly: + [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v) + | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v) + | v = vernac_aux -> v ] + ] + ; + vernac_aux: + (* 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 *) + [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g) + | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g) + | g = gallina; "." -> ([], g) + | g = gallina_ext; "." -> ([], g) + | c = command; "." -> ([], c) + | c = syntax; "." -> ([], c) + | c = subprf -> ([], c) + ] ] + ; + vernac_aux: LAST + [ [ prfcom = command_entry -> ([], prfcom) ] ] + ; + noedit_mode: + [ [ c = query_command -> c None] ] + ; + + subprf: + [ [ s = BULLET -> VernacBullet (make_bullet s) + | "{" -> VernacSubproof None + | "}" -> VernacEndSubproof + ] ] + ; + + located_vernac: + [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ] + ; +END + +let warn_plural_command = + CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled + (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) + +let test_plural_form loc kwd = function + | [(_,([_],_))] -> + warn_plural_command ~loc:!@loc kwd + | _ -> () + +let test_plural_form_types loc kwd = function + | [([_],_)] -> + warn_plural_command ~loc:!@loc kwd + | _ -> () + +let lname_of_lident : lident -> lname = + CAst.map (fun s -> Name s) + +let name_of_ident_decl : ident_decl -> name_decl = + on_fst lname_of_lident + +(* Gallina declarations *) +GEXTEND Gram + GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion + record_field decl_notation rec_definition ident_decl univ_decl; + + gallina: + (* Definition, Theorem, Variable, Axiom, ... *) + [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr; + l = LIST0 + [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr -> + (id,(bl,c)) ] -> + VernacStartTheoremProof (thm, (id,(bl,c))::l) + | stre = assumption_token; nl = inline; bl = assum_list -> + VernacAssumption (stre, nl, bl) + | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> + test_plural_form loc kwd bl; + VernacAssumption (stre, nl, bl) + | d = def_token; id = ident_decl; b = def_body -> + VernacDefinition (d, name_of_ident_decl id, b) + | IDENT "Let"; id = identref; b = def_body -> + VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) + (* Gallina inductive declarations *) + | cum = OPT cumulativity_token; priv = private_token; f = finite_token; + indl = LIST1 inductive_definition SEP "with" -> + let (k,f) = f in + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in + VernacInductive (cum, priv,f,indl) + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (NoDischarge, recs) + | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (DoDischarge, recs) + | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (NoDischarge, corecs) + | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (DoDischarge, corecs) + | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l + | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; + l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) + | IDENT "Register"; IDENT "Inline"; id = identref -> + VernacRegister(id, RegisterInline) + | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l + | IDENT "Universes"; l = LIST1 identref -> VernacUniverse l + | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l + ] ] + ; + + thm_token: + [ [ "Theorem" -> Theorem + | IDENT "Lemma" -> Lemma + | IDENT "Fact" -> Fact + | IDENT "Remark" -> Remark + | IDENT "Corollary" -> Corollary + | IDENT "Proposition" -> Proposition + | IDENT "Property" -> Property ] ] + ; + def_token: + [ [ "Definition" -> (NoDischarge,Definition) + | IDENT "Example" -> (NoDischarge,Example) + | IDENT "SubClass" -> (NoDischarge,SubClass) ] ] + ; + assumption_token: + [ [ "Hypothesis" -> (DoDischarge, Logical) + | "Variable" -> (DoDischarge, Definitional) + | "Axiom" -> (NoDischarge, Logical) + | "Parameter" -> (NoDischarge, Definitional) + | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ] + ; + assumptions_token: + [ [ IDENT "Hypotheses" -> ("Hypotheses", (DoDischarge, Logical)) + | IDENT "Variables" -> ("Variables", (DoDischarge, Definitional)) + | IDENT "Axioms" -> ("Axioms", (NoDischarge, Logical)) + | IDENT "Parameters" -> ("Parameters", (NoDischarge, Definitional)) + | IDENT "Conjectures" -> ("Conjectures", (NoDischarge, Conjectural)) ] ] + ; + inline: + [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) + | IDENT "Inline" -> DefaultInline + | -> NoInline] ] + ; + univ_constraint: + [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = universe_level -> (l, ord, r) ] ] + ; + univ_decl : + [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ]; + cs = [ "|"; l' = LIST0 univ_constraint SEP ","; + ext = [ "+" -> true | -> false ]; "}" -> (l',ext) + | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ] + -> + { univdecl_instance = l; + univdecl_extensible_instance = ext; + univdecl_constraints = fst cs; + univdecl_extensible_constraints = snd cs } + ] ] + ; + ident_decl: + [ [ i = identref; l = OPT univ_decl -> (i, l) + ] ] + ; + finite_token: + [ [ IDENT "Inductive" -> (Inductive_kw,Finite) + | IDENT "CoInductive" -> (CoInductive,CoFinite) + | IDENT "Variant" -> (Variant,BiFinite) + | IDENT "Record" -> (Record,BiFinite) + | IDENT "Structure" -> (Structure,BiFinite) + | IDENT "Class" -> (Class true,BiFinite) ] ] + ; + cumulativity_token: + [ [ IDENT "Cumulative" -> VernacCumulative + | IDENT "NonCumulative" -> VernacNonCumulative ] ] + ; + private_token: + [ [ IDENT "Private" -> true | -> false ] ] + ; + (* Simple definitions *) + def_body: + [ [ bl = binders; ":="; red = reduce; c = lconstr -> + if List.exists (function CLocalPattern _ -> true | _ -> false) bl + then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) + let c = mkCLambdaN ~loc:!@loc bl c in + DefineBody ([], red, c, None) + else + (match c with + | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) + | _ -> DefineBody (bl, red, c, None)) + | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> + let ((bl, c), tyo) = + if List.exists (function CLocalPattern _ -> true | _ -> false) bl + then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) + let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in + (([],mkCLambdaN ~loc:!@loc bl c), None) + else ((bl, c), Some t) + in + DefineBody (bl, red, c, tyo) + | bl = binders; ":"; t = lconstr -> + ProveBody (bl, t) ] ] + ; + reduce: + [ [ IDENT "Eval"; r = red_expr; "in" -> Some r + | -> None ] ] + ; + one_decl_notation: + [ [ ntn = ne_lstring; ":="; c = constr; + scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] + ; + decl_notation: + [ [ "where"; l = LIST1 one_decl_notation SEP IDENT "and" -> l + | -> [] ] ] + ; + (* Inductives and records *) + opt_constructors_or_fields: + [ [ ":="; lc = constructor_list_or_record_decl -> lc + | -> RecordDecl (None, []) ] ] + ; + inductive_definition: + [ [ oc = opt_coercion; id = ident_decl; indpar = binders; + c = OPT [ ":"; c = lconstr -> c ]; + lc=opt_constructors_or_fields; ntn = decl_notation -> + (((oc,id),indpar,c,lc),ntn) ] ] + ; + constructor_list_or_record_decl: + [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l + | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + Constructors ((c id)::l) + | id = identref ; c = constructor_type -> Constructors [ c id ] + | cstr = identref; "{"; fs = record_fields; "}" -> + RecordDecl (Some cstr,fs) + | "{";fs = record_fields; "}" -> RecordDecl (None,fs) + | -> Constructors [] ] ] + ; +(* + csort: + [ [ s = sort -> CSort (loc,s) ] ] + ; +*) + opt_coercion: + [ [ ">" -> true + | -> false ] ] + ; + (* (co)-fixpoints *) + rec_definition: + [ [ id = ident_decl; + bl = binders_fixannot; + ty = type_cstr; + def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> + let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] + ; + corec_definition: + [ [ id = ident_decl; bl = binders; ty = type_cstr; + def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> + ((id,bl,ty,def),ntn) ] ] + ; + type_cstr: + [ [ ":"; c=lconstr -> c + | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] + ; + (* Inductive schemes *) + scheme: + [ [ kind = scheme_kind -> (None,kind) + | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] + ; + scheme_kind: + [ [ IDENT "Induction"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s) + | IDENT "Minimality"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s) + | IDENT "Elimination"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s) + | IDENT "Case"; "for"; ind = smart_global; + IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s) + | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] + ; + (* Various Binders *) +(* + (* ... without coercions *) + binder_nodef: + [ [ b = binder_let -> + (match b with + CLocalAssum(l,ty) -> (l,ty) + | CLocalDef _ -> + Util.user_err_loc + (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] + ; +*) + (* ... with coercions *) + record_field: + [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; + ntn = decl_notation -> (bd,pri),ntn ] ] + ; + record_fields: + [ [ f = record_field; ";"; fs = record_fields -> f :: fs + | f = record_field; ";" -> [f] + | f = record_field -> [f] + | -> [] + ] ] + ; + record_binder_body: + [ [ l = binders; oc = of_type_with_opt_coercion; + t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN ~loc:!@loc l t)) + | l = binders; oc = of_type_with_opt_coercion; + t = lconstr; ":="; b = lconstr -> fun id -> + (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t))) + | l = binders; ":="; b = lconstr -> fun id -> + match b.CAst.v with + | CCast(b', (CastConv t|CastVM t|CastNative t)) -> + (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t))) + | _ -> + (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] + ; + record_binder: + [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) + | id = name; f = record_binder_body -> f id ] ] + ; + assum_list: + [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ] + ; + assum_coe: + [ [ "("; a = simple_assum_coe; ")" -> a ] ] + ; + simple_assum_coe: + [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr -> + (not (Option.is_empty oc),(idl,c)) ] ] + ; + + constructor_type: + [[ l = binders; + t= [ coe = of_type_with_opt_coercion; c = lconstr -> + fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) + | -> + fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] + -> t l + ]] +; + + constructor: + [ [ id = identref; c=constructor_type -> c id ] ] + ; + of_type_with_opt_coercion: + [ [ ":>>" -> Some false + | ":>"; ">" -> Some false + | ":>" -> Some true + | ":"; ">"; ">" -> Some false + | ":"; ">" -> Some true + | ":" -> None ] ] + ; +END + +let only_starredidentrefs = + Gram.Entry.of_parser "test_only_starredidentrefs" + (fun strm -> + let rec aux n = + match Util.stream_nth n strm with + | KEYWORD "." -> () + | KEYWORD ")" -> () + | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) + | _ -> raise Stream.Failure in + aux 0) +let starredidentreflist_to_expr l = + match l with + | [] -> SsEmpty + | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x + +let warn_deprecated_include_type = + CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" + (fun () -> strbrk "Include Type is deprecated; use Include instead") + +(* Modules and Sections *) +GEXTEND Gram + GLOBAL: gallina_ext module_expr module_type section_subset_expr; + + gallina_ext: + [ [ (* Interactive module declaration *) + IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; sign = of_module_type; + body = is_module_expr -> + VernacDefineModule (export, id, bl, sign, body) + | IDENT "Module"; "Type"; id = identref; + bl = LIST0 module_binder; sign = check_module_types; + body = is_module_type -> + VernacDeclareModuleType (id, bl, sign, body) + | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; ":"; mty = module_type_inl -> + VernacDeclareModule (export, id, bl, mty) + (* 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 + + (* Naming a set of section hyps *) + | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr -> + VernacNameSectionHypSet (id, expr) + + (* Requiring an already compiled module *) + | IDENT "Require"; export = export_token; qidl = LIST1 global -> + VernacRequire (None, export, qidl) + | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token + ; qidl = LIST1 global -> + VernacRequire (Some ns, export, qidl) + | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) + | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) + | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> + VernacInclude(e::l) + | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> + warn_deprecated_include_type ~loc:!@loc (); + VernacInclude(e::l) ] ] + ; + export_token: + [ [ IDENT "Import" -> Some false + | IDENT "Export" -> Some true + | -> None ] ] + ; + ext_module_type: + [ [ "<+"; mty = module_type_inl -> mty ] ] + ; + ext_module_expr: + [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ] + ; + check_module_type: + [ [ "<:"; mty = module_type_inl -> mty ] ] + ; + check_module_types: + [ [ mtys = LIST0 check_module_type -> mtys ] ] + ; + of_module_type: + [ [ ":"; mty = module_type_inl -> Enforce mty + | mtys = check_module_types -> Check mtys ] ] + ; + is_module_type: + [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l) + | -> [] ] ] + ; + is_module_expr: + [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l) + | -> [] ] ] + ; + functor_app_annot: + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> + InlineAt (int_of_string i) + | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline + | -> DefaultInline + ] ] + ; + module_expr_inl: + [ [ "!"; me = module_expr -> (me,NoInline) + | me = module_expr; a = functor_app_annot -> (me,a) ] ] + ; + module_type_inl: + [ [ "!"; me = module_type -> (me,NoInline) + | me = module_type; a = functor_app_annot -> (me,a) ] ] + ; + (* Module binder *) + module_binder: + [ [ "("; export = export_token; idl = LIST1 identref; ":"; + mty = module_type_inl; ")" -> (export,idl,mty) ] ] + ; + (* Module expressions *) + module_expr: + [ [ me = module_expr_atom -> me + | me1 = module_expr; me2 = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (me1,me2) + ] ] + ; + module_expr_atom: + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ] + ; + with_declaration: + [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> + CWith_Definition (fqid,udecl,c) + | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> + CWith_Module (fqid,qid) + ] ] + ; + module_type: + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) + | "("; mt = module_type; ")" -> mt + | mty = module_type; me = module_expr_atom -> + CAst.make ~loc:!@loc @@ CMapply (mty,me) + | mty = module_type; "with"; decl = with_declaration -> + CAst.make ~loc:!@loc @@ CMwith (mty,decl) + ] ] + ; + (* Proof using *) + section_subset_expr: + [ [ only_starredidentrefs; l = LIST0 starredidentref -> + starredidentreflist_to_expr l + | e = ssexpr -> e ]] + ; + starredidentref: + [ [ i = identref -> SsSingl i + | i = identref; "*" -> SsFwdClose(SsSingl i) + | "Type" -> SsType + | "Type"; "*" -> SsFwdClose SsType ]] + ; + ssexpr: + [ "35" + [ "-"; e = ssexpr -> SsCompl e ] + | "50" + [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2) + | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)] + | "0" + [ i = starredidentref -> i + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> + starredidentreflist_to_expr l + | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> + SsFwdClose(starredidentreflist_to_expr l) + | "("; e = ssexpr; ")"-> e + | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ] + ; +END + +(* Extensions: implicits, coercions, etc. *) +GEXTEND Gram + GLOBAL: gallina_ext instance_name hint_info; + + gallina_ext: + [ [ (* Transparent and Opaque *) + IDENT "Transparent"; l = LIST1 smart_global -> + VernacSetOpacity (Conv_oracle.transparent, l) + | IDENT "Opaque"; l = LIST1 smart_global -> + VernacSetOpacity (Conv_oracle.Opaque, l) + | IDENT "Strategy"; l = + LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] -> + VernacSetStrategy l + (* Canonical structure *) + | IDENT "Canonical"; IDENT "Structure"; qid = global -> + VernacCanonical CAst.(make ~loc:!@loc @@ AN qid) + | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> + VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn) + | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> + let s = coerce_reference_to_id qid in + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) + + (* Coercions *) + | IDENT "Coercion"; qid = global; d = def_body -> + let s = coerce_reference_to_id qid in + VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) + | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; + s = class_rawexpr; ">->"; t = class_rawexpr -> + VernacIdentityCoercion (f, s, t) + | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; + t = class_rawexpr -> + VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t) + | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; + t = class_rawexpr -> + VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) + + | IDENT "Context"; c = binders -> + VernacContext c + + | IDENT "Instance"; namesup = instance_name; ":"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; + info = hint_info ; + props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | + ":="; c = lconstr -> Some (false,c) | -> None ] -> + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) + + | IDENT "Existing"; IDENT "Instance"; id = global; + info = hint_info -> + VernacDeclareInstances [id, info] + + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; + pri = OPT [ "|"; i = natural -> i ] -> + let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts + + | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is + + (* Arguments *) + | IDENT "Arguments"; qid = smart_global; + args = LIST0 argument_spec_block; + more_implicits = OPT + [ ","; impl = LIST1 + [ impl = LIST0 more_implicits_block -> List.flatten impl] + SEP "," -> impl + ]; + mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> + let mods = match mods with None -> [] | Some l -> List.flatten l in + let slash_position = ref None in + let rec parse_args i = function + | [] -> [] + | `Id x :: args -> x :: parse_args (i+1) args + | `Slash :: args -> + if Option.is_empty !slash_position then + (slash_position := Some i; parse_args i args) + else + user_err Pp.(str "The \"/\" modifier can occur only once") + in + let args = parse_args 0 (List.flatten args) in + let more_implicits = Option.default [] more_implicits in + VernacArguments (qid, args, more_implicits, !slash_position, mods) + + | IDENT "Implicit"; "Type"; bl = reserv_list -> + VernacReserve bl + + | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> + test_plural_form_types loc "Implicit Types" bl; + VernacReserve bl + + | IDENT "Generalizable"; + gen = [IDENT "All"; IDENT "Variables" -> Some [] + | IDENT "No"; IDENT "Variables" -> None + | ["Variable" | IDENT "Variables"]; + idl = LIST1 identref -> Some idl ] -> + VernacGeneralizable gen ] ] + ; + arguments_modifier: + [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase] + | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold] + | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits] + | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] + | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] + | IDENT "rename" -> [`Rename] + | IDENT "assert" -> [`Assert] + | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes] + | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> + [`ClearImplicits; `ClearScopes] + | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> + [`ClearImplicits; `ClearScopes] + ] ] + ; + scope: + [ [ "%"; key = IDENT -> key ] ] + ; + argument_spec: [ + [ b = OPT "!"; id = name ; s = OPT scope -> + id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@loc x) s + ] + ]; + (* List of arguments implicit status, scope, modifiers *) + argument_spec_block: [ + [ item = argument_spec -> + let name, recarg_like, notation_scope = item in + [`Id { name=name; recarg_like=recarg_like; + notation_scope=notation_scope; + implicit_status = NotImplicit}] + | "/" -> [`Slash] + | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = NotImplicit}) items + | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = Implicit}) items + | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> + let f x = match sc, x with + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x + | Some _, Some _ -> user_err Pp.(str "scope declared twice") in + List.map (fun (name,recarg_like,notation_scope) -> + `Id { name=name; recarg_like=recarg_like; + notation_scope=f notation_scope; + implicit_status = MaximallyImplicit}) items + ] + ]; + (* Same as [argument_spec_block], but with only implicit status and names *) + more_implicits_block: [ + [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)] + | "["; items = LIST1 name; "]" -> + List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items + | "{"; items = LIST1 name; "}" -> + List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items + ] + ]; + strategy_level: + [ [ IDENT "expand" -> Conv_oracle.Expand + | IDENT "opaque" -> Conv_oracle.Opaque + | n=INT -> Conv_oracle.Level (int_of_string n) + | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) + | IDENT "transparent" -> Conv_oracle.transparent ] ] + ; + instance_name: + [ [ name = ident_decl; sup = OPT binders -> + (CAst.map (fun id -> Name id) (fst name), snd name), + (Option.default [] sup) + | -> ((CAst.make ~loc:!@loc Anonymous), None), [] ] ] + ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { Typeclasses.hint_priority = i; hint_pattern = pat } + | -> { Typeclasses.hint_priority = None; hint_pattern = None } ] ] + ; + reserv_list: + [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] + ; + reserv_tuple: + [ [ "("; a = simple_reserv; ")" -> a ] ] + ; + simple_reserv: + [ [ idl = LIST1 identref; ":"; c = lconstr -> (idl,c) ] ] + ; + +END + +GEXTEND Gram + GLOBAL: command query_command class_rawexpr gallina_ext; + + gallina_ext: + [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> + VernacSetOption (true, table, v) + | IDENT "Export"; IDENT "Unset"; table = option_table -> + VernacUnsetOption (true, table) + ] ]; + + command: + [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l + + (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) + | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; + expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; + info = hint_info -> + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) + + (* System directory *) + | IDENT "Pwd" -> VernacChdir None + | IDENT "Cd" -> VernacChdir None + | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir) + + | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; + s = [ s = ne_string -> s | s = IDENT -> s ] -> + VernacLoad (verbosely, s) + | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> + VernacDeclareMLModule l + + | 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 = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l)) + | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> + VernacPrint (PrintModuleType qid) + | IDENT "Print"; IDENT "Module"; qid = global -> + VernacPrint (PrintModule qid) + | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> + VernacPrint (PrintNamespace ns) + | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) + + | 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) + + (* For acting on parameter tables *) + | "Set"; table = option_table; v = option_value -> + VernacSetOption (false, table, v) + | IDENT "Unset"; table = option_table -> + VernacUnsetOption (false, table) + + | IDENT "Print"; IDENT "Table"; table = option_table -> + VernacPrintOption table + + | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value + -> VernacAddOption ([table;field], v) + (* A global value below will be hidden by a field above! *) + (* In fact, we give priority to secondary tables *) + (* No syntax for tertiary tables due to conflict *) + (* (but they are unused anyway) *) + | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> + VernacAddOption ([table], v) + + | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value + -> VernacMemOption (table, v) + | IDENT "Test"; table = option_table -> + VernacPrintOption table + + | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value + -> VernacRemoveOption ([table;field], v) + | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> + VernacRemoveOption ([table], v) ]] + ; + query_command: (* TODO: rapprocher Eval et Check *) + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> + fun g -> VernacCheckMayEval (Some r, g, c) + | IDENT "Compute"; c = lconstr; "." -> + fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) + | IDENT "Check"; c = lconstr; "." -> + fun g -> VernacCheckMayEval (None, g, c) + (* Searching the environment *) + | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." -> + fun g -> VernacPrint (PrintAbout (qid,l,g)) + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchHead c,g, l) + | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchPattern c,g, l) + | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchRewrite c,g, l) + | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> + let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) + (* compatibility: SearchAbout *) + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> + fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) + (* compatibility: SearchAbout with "[ ... ]" *) + | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; + l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchAbout sl,g, l) + ] ] + ; + printable: + [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l) + | 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"; dir = OPT dirpath -> PrintLoadPath dir + | IDENT "Modules" -> + user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") + | IDENT "Libraries" -> PrintModules + + | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath + | IDENT "ML"; IDENT "Modules" -> PrintMLModules + | IDENT "Debug"; IDENT "GC" -> PrintDebugGC + | IDENT "Graph" -> PrintGraph + | IDENT "Classes" -> PrintClasses + | IDENT "TypeClasses" -> PrintTypeClasses + | IDENT "Instances"; qid = smart_global -> PrintInstances 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 + | IDENT "Options" -> PrintTables (* A Synonymous to Tables *) + | IDENT "Hint" -> PrintHintGoal + | IDENT "Hint"; qid = smart_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 [x = IDENT -> x ] -> PrintVisibility s + | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid + | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt) + | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt) + | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid) + | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid) + | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid) + | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid) + | IDENT "Strategy"; qid = smart_global -> PrintStrategy (Some qid) + | IDENT "Strategies" -> PrintStrategy None ] ] + ; + class_rawexpr: + [ [ IDENT "Funclass" -> FunClass + | IDENT "Sortclass" -> SortClass + | qid = smart_global -> RefClass qid ] ] + ; + locatable: + [ [ qid = smart_global -> LocateAny qid + | IDENT "Term"; qid = smart_global -> LocateTerm qid + | IDENT "File"; f = ne_string -> LocateFile f + | IDENT "Library"; qid = global -> LocateLibrary qid + | IDENT "Module"; qid = global -> LocateModule qid ] ] + ; + option_value: + [ [ -> BoolValue true + | n = integer -> IntValue (Some n) + | s = STRING -> StringValue s ] ] + ; + option_ref_value: + [ [ id = global -> QualidRefValue id + | s = STRING -> StringRefValue s ] ] + ; + option_table: + [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]] + ; + as_dirpath: + [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] + ; + ne_in_or_out_modules: + [ [ IDENT "inside"; l = LIST1 global -> SearchInside l + | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ] + ; + in_or_out_modules: + [ [ m = ne_in_or_out_modules -> m + | -> SearchOutside [] ] ] + ; + comment: + [ [ c = constr -> CommentConstr c + | s = STRING -> CommentString s + | n = natural -> CommentInt n ] ] + ; + positive_search_mark: + [ [ "-" -> false | -> true ] ] + ; + scope: + [ [ "%"; key = IDENT -> key ] ] + ; + searchabout_query: + [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> + (b, SearchString (s,sc)) + | b = positive_search_mark; p = constr_pattern -> + (b, SearchSubPattern p) + ] ] + ; + searchabout_queries: + [ [ m = ne_in_or_out_modules -> ([],m) + | s = searchabout_query; l = searchabout_queries -> + let (sl,m) = l in (s::sl,m) + | -> ([],SearchOutside []) + ] ] + ; + univ_name_list: + [ [ "@{" ; l = LIST0 name; "}" -> l ] ] + ; +END; + +GEXTEND Gram + command: + [ [ +(* State management *) + IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s + | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s + | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s + | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s + +(* Resetting *) + | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial + | IDENT "Reset"; id = identref -> VernacResetName id + | IDENT "Back" -> VernacBack 1 + | IDENT "Back"; n = natural -> VernacBack n + | IDENT "BackTo"; n = natural -> VernacBackTo n + +(* Tactic Debugger *) + | IDENT "Debug"; IDENT "On" -> + VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) + + | IDENT "Debug"; IDENT "Off" -> + VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) + +(* registration of a custom reduction *) + + | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; + r = red_expr -> + VernacDeclareReduction (s,r) + + ] ]; + END +;; + +(* Grammar extensions *) + +GEXTEND Gram + GLOBAL: syntax; + + syntax: + [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> + VernacOpenCloseScope (true,sc) + + | IDENT "Close"; IDENT "Scope"; sc = IDENT -> + VernacOpenCloseScope (false,sc) + + | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> + VernacDelimiters (sc, Some key) + | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> + VernacDelimiters (sc, None) + + | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; + refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) + + | IDENT "Infix"; op = ne_lstring; ":="; p = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacInfix ((op,modl),p,sc) + | IDENT "Notation"; id = identref; + idl = LIST0 ident; ":="; c = constr; b = only_parsing -> + VernacSyntacticDefinition + (id,(idl,c),b) + | IDENT "Notation"; s = lstring; ":="; + c = constr; + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacNotation (c,(s,modl),sc) + | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> + VernacNotationAddFormat (n,s,fmt) + + | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; + l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> + let s = CAst.map (fun s -> "x '"^s^"' y") s in + VernacSyntaxExtension (true,(s,l)) + + | IDENT "Reserved"; IDENT "Notation"; + s = ne_lstring; + l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] + -> VernacSyntaxExtension (false, (s,l)) + + (* "Print" "Grammar" should be here but is in "command" entry in order + to factorize with other "Print"-based vernac entries *) + ] ] + ; + only_parsing: + [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> + Some Flags.Current + | "("; IDENT "compat"; s = STRING; ")" -> + Some (parse_compat_version s) + | -> None ] ] + ; + level: + [ [ IDENT "level"; n = natural -> NumLevel n + | IDENT "next"; IDENT "level" -> NextLevel ] ] + ; + syntax_modifier: + [ [ "at"; IDENT "level"; n = natural -> SetLevel n + | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA + | IDENT "right"; IDENT "associativity" -> SetAssoc RightA + | IDENT "no"; IDENT "associativity" -> SetAssoc NonA + | IDENT "only"; IDENT "printing" -> SetOnlyPrinting + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing + | IDENT "compat"; s = STRING -> + SetCompatVersion (parse_compat_version s) + | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s]; + s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] -> + begin match s1, s2 with + | { CAst.v = k }, Some s -> SetFormat(k,s) + | s, None -> SetFormat ("text",s) end + | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; + lev = level -> SetItemLevel (x::l,lev) + | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev) + | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None) + | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) + ] ] + ; + syntax_extension_type: + [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference + | IDENT "bigint" -> ETBigint + | IDENT "binder" -> ETBinder true + | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n) + | IDENT "pattern" -> ETPattern (false,None) + | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n) + | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None) + | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n) + | IDENT "closed"; IDENT "binder" -> ETBinder false + ] ] + ; + at_level: + [ [ "at"; n = level -> n ] ] + ; + constr_as_binder_kind: + [ [ "as"; IDENT "ident" -> AsIdent + | "as"; IDENT "pattern" -> AsIdentOrPattern + | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ] + ; +END diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 76958b05f..e038f54dd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -76,15 +76,15 @@ let pr_grammar = function pr_entry Pcoq.Constr.pattern | "vernac" -> str "Entry vernac_control is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.vernac_control ++ + pr_entry Pvernac.Vernac_.vernac_control ++ str "Entry command is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.command ++ + pr_entry Pvernac.Vernac_.command ++ str "Entry syntax is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.syntax ++ + pr_entry Pvernac.Vernac_.syntax ++ str "Entry gallina is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.gallina ++ + pr_entry Pvernac.Vernac_.gallina ++ str "Entry gallina_ext is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.gallina_ext + pr_entry Pvernac.Vernac_.gallina_ext | name -> pr_registered_grammar name (**********************************************************************) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7a34e8027..3655947a5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -152,7 +152,7 @@ open Pputils | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b let pr_locality local = if local then keyword "Local" else keyword "Global" diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml new file mode 100644 index 000000000..bac882381 --- /dev/null +++ b/vernac/pvernac.ml @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pcoq + +let uncurry f (x,y) = f x y + +let uvernac = create_universe "vernac" + +module Vernac_ = + struct + let gec_vernac s = Gram.entry_create ("vernac:" ^ s) + + (* The different kinds of vernacular commands *) + let gallina = gec_vernac "gallina" + let gallina_ext = gec_vernac "gallina_ext" + let command = gec_vernac "command" + let syntax = gec_vernac "syntax_command" + let vernac_control = gec_vernac "Vernac.vernac_control" + let rec_definition = gec_vernac "Vernac.rec_definition" + let red_expr = new_entry utactic "red_expr" + let hint_info = gec_vernac "hint_info" + (* Main vernac entry *) + let main_entry = Gram.entry_create "vernac" + let noedit_mode = gec_vernac "noedit_command" + + let () = + let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in + let act_eoi = Gram.action (fun _ loc -> None) in + let rule = [ + ([ Symbols.stoken Tok.EOI ], act_eoi); + ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); + ] in + uncurry (Gram.extend main_entry) (None, [None, None, rule]) + + let command_entry_ref = ref noedit_mode + let command_entry = + Gram.Entry.of_parser "command_entry" + (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) + + end + +let main_entry = Vernac_.main_entry + +let set_command_entry e = Vernac_.command_entry_ref := e +let get_command_entry () = !Vernac_.command_entry_ref + +let () = + register_grammar Stdarg.wit_red_expr (Vernac_.red_expr); diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli new file mode 100644 index 000000000..9d999793e --- /dev/null +++ b/vernac/pvernac.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pcoq +open Genredexpr +open Vernacexpr + +val uvernac : gram_universe + +module Vernac_ : + sig + val gallina : vernac_expr Gram.entry + val gallina_ext : vernac_expr Gram.entry + val command : vernac_expr Gram.entry + val syntax : vernac_expr Gram.entry + val vernac_control : vernac_control Gram.entry + val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry + val noedit_mode : vernac_expr Gram.entry + val command_entry : vernac_expr Gram.entry + val red_expr : raw_red_expr Gram.entry + val hint_info : Typeclasses.hint_info_expr Gram.entry + end + +(** The main entry: reads an optional vernac command *) +val main_entry : (Loc.t * vernac_control) option Gram.entry + +(** Handling of the proof mode entry *) +val get_command_entry : unit -> vernac_expr Gram.entry +val set_command_entry : vernac_expr Gram.entry -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 6fceda56d..39c313ac7 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,3 +1,7 @@ +Vernacexpr +Pvernac +G_vernac +G_proofs Vernacprop Himsg ExplainErr diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7ca51db78..41c496a6b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1969,7 +1969,7 @@ let vernac_load interp fname = interp x in let parse_sentence = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Gram.entry_parse Pcoq.main_entry po with + match Pcoq.Gram.entry_parse Pvernac.main_entry po with | Some x -> x | None -> raise End_of_input) in let fname = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml new file mode 100644 index 000000000..cf0da4de2 --- /dev/null +++ b/vernac/vernacexpr.ml @@ -0,0 +1,533 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Misctypes +open Constrexpr +open Libnames + +(** Vernac expressions, produced by the parser *) +type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + +type goal_selector = Goal_select.t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll +[@@ocaml.deprecated "Use Goal_select.t"] + +type goal_identifier = string +type scope_name = string + +type goal_reference = + | OpenSubgoals + | NthGoal of int + | GoalId of Id.t + +type univ_name_list = UnivNames.univ_name_list +[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] + +type printable = + | PrintTables + | PrintFullContext + | PrintSectionContext of reference + | PrintInspect of int + | PrintGrammar of string + | PrintLoadPath of DirPath.t option + | PrintModules + | PrintModule of reference + | PrintModuleType of reference + | PrintNamespace of DirPath.t + | PrintMLLoadPath + | PrintMLModules + | PrintDebugGC + | PrintName of reference or_by_notation * UnivNames.univ_name_list option + | PrintGraph + | PrintClasses + | PrintTypeClasses + | PrintInstances of reference or_by_notation + | PrintCoercions + | PrintCoercionPaths of class_rawexpr * class_rawexpr + | PrintCanonicalConversions + | PrintUniverses of bool * string option + | PrintHint of reference or_by_notation + | PrintHintGoal + | PrintHintDbName of string + | PrintHintDb + | PrintScopes + | PrintScope of string + | PrintVisibility of string option + | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option + | PrintImplicit of reference or_by_notation + | PrintAssumptions of bool * bool * reference or_by_notation + | PrintStrategy of reference or_by_notation option + +type search_about_item = + | SearchSubPattern of constr_pattern_expr + | SearchString of string * scope_name option + +type searchable = + | SearchPattern of constr_pattern_expr + | SearchRewrite of constr_pattern_expr + | SearchHead of constr_pattern_expr + | SearchAbout of (bool * search_about_item) list + +type locatable = + | LocateAny of reference or_by_notation + | LocateTerm of reference or_by_notation + | LocateLibrary of reference + | LocateModule of reference + | LocateOther of string * reference + | LocateFile of string + +type showable = + | ShowGoal of goal_reference + | ShowProof + | ShowScript + | ShowExistentials + | ShowUniverses + | ShowProofNames + | ShowIntros of bool + | ShowMatch of reference + +type comment = + | CommentConstr of constr_expr + | CommentString of string + | CommentInt of int + +type reference_or_constr = Hints.reference_or_constr = + | HintsReference of reference + | HintsConstr of constr_expr +[@@ocaml.deprecated "Please use [Hints.hints_expr]"] + +type hint_mode = Hints.hint_mode = + | ModeInput (* No evars *) + | ModeNoHeadEvar (* No evar at the head *) + | ModeOutput (* Anything *) +[@@ocaml.deprecated "Please use [Hints.hints_expr]"] + +type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } +[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] + +type hint_info_expr = Typeclasses.hint_info_expr +[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"] + +type hints_expr = Hints.hints_expr = + | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list + | HintsImmediate of Hints.reference_or_constr list + | HintsUnfold of reference list + | HintsTransparency of reference list * bool + | HintsMode of reference * Hints.hint_mode list + | HintsConstructors of reference list + | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument +[@@ocaml.deprecated "Please use [Hints.hints_expr]"] + +type search_restriction = + | SearchInside of reference list + | SearchOutside of reference list + +type rec_flag = bool (* true = Rec; false = NoRec *) +type verbose_flag = bool (* true = Verbose; false = Silent *) +type opacity_flag = Proof_global.opacity_flag = Opaque | Transparent + [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] +type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) +type instance_flag = bool option + (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) +type export_flag = bool (* true = Export; false = Import *) +type inductive_flag = Declarations.recursivity_kind +type onlyparsing_flag = Flags.compat_version option + (* Some v = Parse only; None = Print also. + If v<>Current, it contains the name of the coq version + which this notation is trying to be compatible with *) +type locality_flag = bool (* true = Local *) + +type option_value = Goptions.option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + | StringOptValue of string option + +type option_ref_value = + | StringRefValue of string + | QualidRefValue of reference + +(** Identifier and optional list of bound universes and constraints. *) + +type sort_expr = Sorts.family + +type definition_expr = + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr + * constr_expr option + +type fixpoint_expr = + ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + +type cofixpoint_expr = + ident_decl * local_binder_expr list * constr_expr * constr_expr option + +type local_decl_expr = + | AssumExpr of lname * constr_expr + | DefExpr of lname * constr_expr * constr_expr option + +type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) +type decl_notation = lstring * constr_expr * scope_name option +type simple_binder = lident list * constr_expr +type class_binder = lident * constr_expr list +type 'a with_coercion = coercion_flag * 'a +type 'a with_instance = instance_flag * 'a +type 'a with_notation = 'a * decl_notation list +type 'a with_priority = 'a * int option +type constructor_expr = (lident * constr_expr) with_coercion +type constructor_list_or_record_decl_expr = + | Constructors of constructor_expr list + | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list +type inductive_expr = + ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * + constructor_list_or_record_decl_expr + +type one_inductive_expr = + ident_decl * local_binder_expr list * constr_expr option * constructor_expr list + +type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr +and typeclass_context = typeclass_constraint list + +type proof_expr = + ident_decl * (local_binder_expr list * constr_expr) + +type syntax_modifier = + | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option + | SetLevel of int + | SetAssoc of Extend.gram_assoc + | SetEntryType of string * Extend.simple_constr_prod_entry_key + | SetOnlyParsing + | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version + | SetFormat of string * lstring + +type proof_end = + | Admitted + (* name in `Save ident` when closing goal *) + | Proved of Proof_global.opacity_flag * lident option + +type scheme = + | InductionScheme of bool * reference or_by_notation * sort_expr + | CaseScheme of bool * reference or_by_notation * sort_expr + | EqualityScheme of reference or_by_notation + +type section_subset_expr = + | SsEmpty + | SsType + | SsSingl of lident + | SsCompl of section_subset_expr + | SsUnion of section_subset_expr * section_subset_expr + | SsSubstr of section_subset_expr * section_subset_expr + | SsFwdClose of section_subset_expr + +(** Extension identifiers for the VERNAC EXTEND mechanism. + + {b ("Extraction", 0} indicates {b Extraction {i qualid}} command. + + {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command. + + {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command. + + {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command. + + {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command. + + {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command. + + {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands. + + {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command. + + {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command. + + {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command. + + {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. + + {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. + *) +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int + +(* This type allows registering the inlining of constants in native compiler. + It will be extended with primitive inductive types and operators *) +type register_kind = + | RegisterInline + +type bullet = Proof_bullet.t +[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] + +(** {6 Types concerning the module layer} *) + +(** Rigid / flexible module signature *) + +type 'a module_signature = 'a Declaremods.module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) +[@@ocaml.deprecated "please use [Declaremods.module_signature]."] + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = Declaremods.inline = + | NoInline + | DefaultInline + | InlineAt of int +[@@ocaml.deprecated "please use [Declaremods.inline]."] + +type module_ast_inl = module_ast * Declaremods.inline +type module_binder = bool option * lident list * module_ast_inl + +(** [Some b] if locally enabled/disabled according to [b], [None] if + we should use the global flag. *) +type vernac_cumulative = VernacCumulative | VernacNonCumulative + +(** {6 The type of vernacular expressions} *) + +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string CAst.t option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = + + | VernacLoad of verbose_flag * string + (* Syntax *) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name + | VernacDelimiters of scope_name * string option + | VernacBindScope of scope_name * class_rawexpr list + | VernacInfix of (lstring * syntax_modifier list) * + constr_expr * scope_name option + | VernacNotation of + constr_expr * (lstring * syntax_modifier list) * + scope_name option + | VernacNotationAddFormat of string * string * string + + (* Gallina *) + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr + | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list + | VernacEndProof of proof_end + | VernacExactProof of constr_expr + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * + Declaremods.inline * (ident_decl list * constr_expr) with_coercion list + | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list + | VernacScheme of (lident option * scheme) list + | VernacCombinedScheme of lident * lident list + | VernacUniverse of lident list + | VernacConstraint of Glob_term.glob_constraint list + + (* Gallina extensions *) + | VernacBeginSection of lident + | VernacEndSegment of lident + | VernacRequire of + reference option * export_flag option * reference list + | VernacImport of export_flag * reference list + | VernacCanonical of reference or_by_notation + | VernacCoercion of reference or_by_notation * + class_rawexpr * class_rawexpr + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr + | VernacNameSectionHypSet of lident * section_subset_expr + + (* Type classes *) + | VernacInstance of + bool * (* abstract instance *) + local_binder_expr list * (* super *) + typeclass_constraint * (* instance name, class name, params *) + (bool * constr_expr) option * (* props *) + Typeclasses.hint_info_expr + + | VernacContext of local_binder_expr list + + | VernacDeclareInstances of + (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) + + | VernacDeclareClass of reference (* inductive or definition name *) + + (* Modules and Module Types *) + | VernacDeclareModule of bool option * lident * + module_binder list * module_ast_inl + | VernacDefineModule of bool option * lident * module_binder list * + module_ast_inl Declaremods.module_signature * module_ast_inl list + | VernacDeclareModuleType of lident * + module_binder list * module_ast_inl list * module_ast_inl list + | VernacInclude of module_ast_inl list + + (* Solving *) + + | VernacSolveExistential of int * constr_expr + + (* Auxiliary file and library management *) + | VernacAddLoadPath of rec_flag * string * DirPath.t option + | VernacRemoveLoadPath of string + | VernacAddMLPath of rec_flag * string + | VernacDeclareMLModule of string list + | VernacChdir of string option + + (* State management *) + | VernacWriteState of string + | VernacRestoreState of string + + (* Resetting *) + | VernacResetName of lident + | VernacResetInitial + | VernacBack of int + | VernacBackTo of int + + (* Commands *) + | VernacCreateHintDb of string * bool + | VernacRemoveHints of string list * reference list + | VernacHints of string list * Hints.hints_expr + | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * + onlyparsing_flag + | VernacArguments of reference or_by_notation * + vernac_argument_status list (* Main arguments status list *) * + (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * + int option (* Number of args to trigger reduction *) * + [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `DefaultImplicits ] list + | VernacReserve of simple_binder list + | VernacGeneralizable of (lident list) option + | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) + | VernacSetStrategy of + (Conv_oracle.level * reference or_by_notation list) list + | VernacUnsetOption of export_flag * Goptions.option_name + | VernacSetOption of export_flag * Goptions.option_name * option_value + | VernacAddOption of Goptions.option_name * option_ref_value list + | VernacRemoveOption of Goptions.option_name * option_ref_value list + | VernacMemOption of Goptions.option_name * option_ref_value list + | VernacPrintOption of Goptions.option_name + | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr + | VernacGlobalCheck of constr_expr + | VernacDeclareReduction of string * Genredexpr.raw_red_expr + | VernacPrint of printable + | VernacSearch of searchable * Goal_select.t option * search_restriction + | VernacLocate of locatable + | VernacRegister of lident * register_kind + | VernacComments of comment list + + (* Proof management *) + | VernacAbort of lident option + | VernacAbortAll + | VernacRestart + | VernacUndo of int + | VernacUndoTo of int + | VernacFocus of int option + | VernacUnfocus + | VernacUnfocused + | VernacBullet of Proof_bullet.t + | VernacSubproof of Goal_select.t option + | VernacEndSubproof + | VernacShow of showable + | VernacCheckGuard + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option + | VernacProofMode of string + + (* For extension *) + | VernacExtend of extend_name * Genarg.raw_generic_argument list + +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool + +type vernac_control = + | VernacExpr of vernac_flag list * vernac_expr + (* boolean is true when the `-time` batch-mode command line flag was set. + the flag is used to print differently in `-time` vs `Time foo` *) + | VernacTime of bool * vernac_control CAst.t + | VernacRedirect of string * vernac_control CAst.t + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or + alters the global state or is a control command like BackTo or is + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of proof_step + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Id.t list +and vernac_sideff_type = Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and proof_step = { (* TODO: inline with OCaml 4.03 *) + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option +} +and solving_tac = bool (* a terminator *) +and anon_abstracting_tac = bool (* abstracting anonymously its result *) +and proof_block_name = string (* open type of delimiters *) +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] |