diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 321 |
1 files changed, 195 insertions, 126 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 4da16ea7..4a2a218b 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) open Util open Names @@ -18,7 +18,6 @@ open Decl_kinds open Ppextend (* Toplevel control exceptions *) -exception ProtectedLoop exception Drop exception Quit @@ -27,11 +26,11 @@ open Nametab type lident = identifier located type lname = name located -type lstring = string +type lstring = string located type lreference = reference -type class_rawexpr = FunClass | SortClass | RefClass of reference - +type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + type printable = | PrintTables | PrintFullContext @@ -44,18 +43,17 @@ type printable = | PrintModuleType of reference | PrintMLLoadPath | PrintMLModules - | PrintName of reference - | PrintOpaqueName of reference + | PrintName of reference or_by_notation | PrintGraph | PrintClasses | PrintTypeClasses - | PrintInstances of reference + | PrintInstances of reference or_by_notation | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions | PrintUniverses of string option - | PrintHint of reference + | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string | PrintRewriteHintDbName of string @@ -63,9 +61,9 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference - | PrintImplicit of reference - | PrintAssumptions of bool * reference + | PrintAbout of reference or_by_notation + | PrintImplicit of reference or_by_notation + | PrintAssumptions of bool * reference or_by_notation type search_about_item = | SearchSubPattern of constr_pattern_expr @@ -74,15 +72,15 @@ type search_about_item = type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr - | SearchHead of reference + | SearchHead of constr_pattern_expr | SearchAbout of (bool * search_about_item) list type locatable = - | LocateTerm of reference + | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference + | LocateTactic of reference | LocateFile of string - | LocateNotation of notation type goable = | GoTo of int @@ -110,7 +108,7 @@ type comment = | CommentString of string | CommentInt of int -type hints = +type hints_expr = | HintsResolve of (int option * bool * constr_expr) list | HintsImmediate of constr_expr list | HintsUnfold of reference list @@ -124,15 +122,6 @@ type search_restriction = | SearchInside of reference list | SearchOutside of reference list -type option_value = - | StringValue of string - | IntValue of int - | BoolValue of bool - -type option_ref_value = - | StringRefValue of string - | QualidRefValue of reference - type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) type opacity_flag = bool (* true = Opaque; false = Transparent *) @@ -142,6 +131,17 @@ type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = Decl_kinds.recursivity_kind type onlyparsing_flag = bool (* true = Parse only; false = Print also *) +type infer_flag = bool (* true = try to Infer record; false = nothing *) +type full_locality_flag = bool option (* true = Local; false = Global *) + +type option_value = + | StringValue of string + | IntValue of int + | BoolValue of bool + +type option_ref_value = + | StringRefValue of string + | QualidRefValue of reference type sort_expr = Rawterm.rawsort @@ -150,69 +150,89 @@ type definition_expr = | DefineBody of local_binder list * raw_red_expr option * constr_expr * constr_expr option +type fixpoint_expr = + identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + +type cofixpoint_expr = + identifier located * local_binder 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 | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = (string * constr_expr * scope_name option) option +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_notation = 'a * decl_notation +type 'a with_notation = 'a * decl_notation list 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_coercion with_notation list type inductive_expr = - lident with_coercion * local_binder list * constr_expr option * inductive_kind * + lident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr -type module_binder = bool option * lident list * module_type_ast +type one_inductive_expr = + lident * local_binder list * constr_expr option * constructor_expr list + +type module_binder = bool option * lident list * module_ast_inl -type grammar_production = - | VTerm of string - | VNonTerm of loc * string * Names.identifier option +type grammar_tactic_prod_item_expr = + | TacTerm of string + | TacNonTerm of loc * string * (Names.identifier * string) option + +type syntax_modifier = + | SetItemLevel of string list * production_level + | SetLevel of int + | SetAssoc of Gramext.g_assoc + | SetEntryType of string * simple_constr_prod_entry_key + | SetOnlyParsing + | SetFormat of string located type proof_end = | Admitted | Proved of opacity_flag * (lident * theorem_kind option) option type scheme = - | InductionScheme of bool * lreference * sort_expr - | EqualityScheme of lreference + | InductionScheme of bool * reference or_by_notation * sort_expr + | EqualityScheme of reference or_by_notation type vernac_expr = (* Control *) | VernacList of located_vernac_expr list - | VernacLoad of verbose_flag * lstring + | VernacLoad of verbose_flag * string | VernacTime of vernac_expr + | VernacTimeout of int * vernac_expr + | VernacFail of vernac_expr - (* Syntax *) - | VernacTacticNotation of int * grammar_production list * raw_tactic_expr + (* Syntax *) + | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) | VernacOpenCloseScope of (locality_flag * bool * scope_name) - | VernacDelimiters of scope_name * lstring + | VernacDelimiters of scope_name * string | VernacBindScope of scope_name * class_rawexpr list - | VernacArgumentsScope of locality_flag * lreference * scope_name option list + | VernacArgumentsScope of locality_flag * reference or_by_notation * + scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * - lreference * scope_name option + constr_expr * scope_name option | VernacNotation of locality_flag * constr_expr * (lstring * syntax_modifier list) * scope_name option (* Gallina *) - | VernacDefinition of definition_kind * lident * definition_expr * + | VernacDefinition of definition_kind * lident * definition_expr * declaration_hook - | VernacStartTheoremProof of theorem_kind * - (lident option * (local_binder list * constr_expr)) list * + | VernacStartTheoremProof of theorem_kind * + (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * bool * declaration_hook | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list - | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list - | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool - | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool + | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list + | VernacFixpoint of (fixpoint_expr * decl_notation list) list * bool + | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list * bool | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list @@ -222,20 +242,15 @@ type vernac_expr = | VernacRequire of export_flag option * specif_flag option * lreference list | VernacImport of export_flag * lreference list - | VernacCanonical of lreference - | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of locality * lident * + | VernacCanonical of reference or_by_notation + | VernacCoercion of locality * reference or_by_notation * + class_rawexpr * class_rawexpr + | VernacIdentityCoercion of locality * lident * class_rawexpr * class_rawexpr (* Type classes *) -(* | VernacClass of *) -(* lident * (\* name *\) *) -(* local_binder list * (\* params *\) *) -(* sort_expr located option * (\* arity *\) *) -(* local_binder list * (\* constraints *\) *) -(* (lident * bool * constr_expr) list (\* props, with substructure hints *\) *) - | VernacInstance of + bool * (* abstract instance *) bool * (* global *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) @@ -243,18 +258,20 @@ type vernac_expr = int option (* Priority *) | VernacContext of local_binder list - + | VernacDeclareInstance of - lident (* instance name *) + bool (* global *) * reference (* instance name *) + + | VernacDeclareClass of reference (* inductive or definition name *) (* Modules and Module Types *) - | VernacDeclareModule of bool option * lident * - module_binder list * (module_type_ast * bool) - | VernacDefineModule of bool option * lident * - module_binder list * (module_type_ast * bool) option * module_ast option - | VernacDeclareModuleType of lident * - module_binder list * module_type_ast option - | VernacInclude of include_ast + | VernacDeclareModule of bool option * lident * + module_binder list * module_ast_inl + | VernacDefineModule of bool option * lident * + module_binder list * module_ast_inl 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 *) @@ -269,16 +286,16 @@ type vernac_expr = (* Auxiliary file and library management *) - | VernacRequireFrom of export_flag option * specif_flag option * lstring - | VernacAddLoadPath of rec_flag * lstring * dir_path option - | VernacRemoveLoadPath of lstring - | VernacAddMLPath of rec_flag * lstring - | VernacDeclareMLModule of lstring list - | VernacChdir of lstring option + | VernacRequireFrom of export_flag option * specif_flag option * string + | VernacAddLoadPath of rec_flag * string * dir_path option + | VernacRemoveLoadPath of string + | VernacAddMLPath of rec_flag * string + | VernacDeclareMLModule of locality_flag * string list + | VernacChdir of string option (* State management *) - | VernacWriteState of lstring - | VernacRestoreState of lstring + | VernacWriteState of string + | VernacRestoreState of string (* Resetting *) | VernacRemoveName of lident @@ -289,24 +306,26 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of - rec_flag * (reference * bool * raw_tactic_expr) list - | VernacCreateHintDb of locality_flag * lstring * bool - | VernacHints of locality_flag * lstring list * hints + (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list) + | VernacCreateHintDb of locality_flag * string * bool + | VernacHints of locality_flag * string list * hints_expr | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag - | VernacDeclareImplicits of locality_flag * lreference * + | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list option - | VernacReserve of lident list * constr_expr + | VernacReserve of simple_binder list + | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of - locality_flag * (Conv_oracle.level * lreference list) list - | VernacUnsetOption of Goptions.option_name - | VernacSetOption of Goptions.option_name * option_value + locality_flag * (Conv_oracle.level * reference or_by_notation list) list + | VernacUnsetOption of full_locality_flag * Goptions.option_name + | VernacSetOption of full_locality_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 raw_red_expr option * int option * constr_expr | VernacGlobalCheck of constr_expr + | VernacDeclareReduction of locality_flag * string * raw_red_expr | VernacPrint of printable | VernacSearch of searchable * search_restriction | VernacLocate of locatable @@ -340,68 +359,118 @@ and located_vernac_expr = loc * vernac_expr (* Locating errors raised just after the dot is parsed but before the interpretation phase *) -exception DuringSyntaxChecking of exn +exception DuringSyntaxChecking of exn located -let syntax_checking_error s = - raise (DuringSyntaxChecking (UserError ("",Pp.str s))) +let syntax_checking_error loc s = + raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s))) +(**********************************************************************) (* Managing locality *) let locality_flag = ref None let local_of_bool = function true -> Local | false -> Global +let is_true = function Some (_,b) -> b | _ -> false +let is_false = function Some (_,b) -> not b | _ -> false + let check_locality () = - if !locality_flag = Some true then - syntax_checking_error "This command does not support the \"Local\" prefix."; - if !locality_flag = Some false then - syntax_checking_error "This command does not support the \"Global\" prefix." + match !locality_flag with + | Some (loc,true) -> + syntax_checking_error loc + "This command does not support the \"Local\" prefix."; + | Some (loc,false) -> + syntax_checking_error loc + "This command does not support the \"Global\" prefix." + | None -> () + +(** Extracting the locality flag *) -let use_locality () = - let local = match !locality_flag with Some true -> true | _ -> false in +(* Commands which supported an inlined Local flag *) + +let enforce_locality_full local = + let local = + match !locality_flag with + | Some (_,false) when local -> + error "Cannot be simultaneously Local and Global." + | Some (_,true) when local -> + error "Use only prefix \"Local\"." + | None -> + if local then begin + Flags.if_verbose + Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix."); + Some true + end else + None + | Some (_,b) -> Some b in locality_flag := None; local -let use_locality_exp () = local_of_bool (use_locality ()) +(* Commands which did not supported an inlined Local flag (synonym of + [enforce_locality_full false]) *) -let use_section_locality () = - let local = - match !locality_flag with Some b -> b | None -> Lib.sections_are_opened () - in +let use_locality_full () = + let r = Option.map snd !locality_flag in locality_flag := None; - local + r + +(** Positioning locality for commands supporting discharging and export + outside of modules *) + +(* For commands whose default is to discharge and export: + Global is the default and is neutral; + Local in a section deactivates discharge, + Local not in a section deactivates export *) + +let make_locality = function Some true -> true | _ -> false + +let use_locality () = make_locality (use_locality_full ()) + +let use_locality_exp () = local_of_bool (use_locality ()) + +let enforce_locality local = make_locality (enforce_locality_full local) + +let enforce_locality_exp local = local_of_bool (enforce_locality local) + +(* For commands whose default is not to discharge and not to export: + Global forces discharge and export; + Local is the default and is neutral *) let use_non_locality () = - let local = match !locality_flag with Some false -> false | _ -> true in - locality_flag := None; - local + match use_locality_full () with Some false -> false | _ -> true -let enforce_locality () = - let local = - match !locality_flag with - | Some false -> - error "Cannot be simultaneously Local and Global." - | _ -> - Flags.if_verbose - Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; - true in - locality_flag := None; - local +(* For commands whose default is to not discharge but to export: + Global in sections forces discharge, Global not in section is the default; + Local in sections is the default, Local not in section forces non-export *) -let enforce_locality_exp () = local_of_bool (enforce_locality ()) +let make_section_locality = + function Some b -> b | None -> Lib.sections_are_opened () + +let use_section_locality () = + make_section_locality (use_locality_full ()) + +let enforce_section_locality local = + make_section_locality (enforce_locality_full local) + +(** Positioning locality for commands supporting export but not discharge *) + +(* For commands whose default is to export (if not in section): + Global in sections is forbidden, Global not in section is neutral; + Local in sections is the default, Local not in section forces non-export *) + +let make_module_locality = function + | Some false -> + if Lib.sections_are_opened () then + error "This command does not support the Global option in sections."; + false + | Some true -> true + | None -> false + +let use_module_locality () = + make_module_locality (use_locality_full ()) + +let enforce_module_locality local = + make_module_locality (enforce_locality_full local) + +(**********************************************************************) -let enforce_locality_of local = - let local = - match !locality_flag with - | Some false when local -> - error "Cannot be simultaneously Local and Global." - | Some true when local -> - error "Use only prefix \"Local\"." - | None -> - if local then - Flags.if_verbose - Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; - local - | Some b -> b in - locality_flag := None; - local |