diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 139 |
1 files changed, 63 insertions, 76 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 122c0b0b2..be0f4d678 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -10,12 +10,12 @@ open Util open Names -open Coqast open Tacexpr open Extend open Genarg -open Symbols +open Topconstr open Decl_kinds +open Ppextend (* Toplevel control exceptions *) exception ProtectedLoop @@ -30,41 +30,41 @@ type def_kind = DEFINITION | LET | LOCAL | THEOREM | LETTOP | DECL | REMARK open Libnames open Nametab -type class_rawexpr = FunClass | SortClass | RefClass of qualid located +type class_rawexpr = FunClass | SortClass | RefClass of reference type printable = | PrintTables | PrintLocalContext | PrintFullContext - | PrintSectionContext of qualid located + | PrintSectionContext of reference | PrintInspect of int | PrintGrammar of string * string | PrintLoadPath | PrintModules - | PrintModule of qualid located - | PrintModuleType of qualid located + | PrintModule of reference + | PrintModuleType of reference | PrintMLLoadPath | PrintMLModules - | PrintName of qualid located - | PrintOpaqueName of qualid located + | PrintName of reference + | PrintOpaqueName of reference | PrintGraph | PrintClasses | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintUniverses of string option - | PrintHint of qualid located + | PrintHint of reference | PrintHintGoal | PrintHintDbName of string | PrintHintDb type searchable = - | SearchPattern of pattern_ast - | SearchRewrite of pattern_ast - | SearchHead of qualid located + | SearchPattern of pattern_expr + | SearchRewrite of pattern_expr + | SearchHead of reference type locatable = - | LocateTerm of qualid located - | LocateLibrary of qualid located + | LocateTerm of reference + | LocateLibrary of reference | LocateFile of string type goable = @@ -87,22 +87,22 @@ type showable = | ExplainTree of int list type comment = - | CommentConstr of constr_ast + | CommentConstr of constr_expr | CommentString of string | CommentInt of int -type raw_constr_ast = t +type raw_constr_expr = constr_expr type hints = - | HintsResolve of (identifier option * constr_ast) list - | HintsImmediate of (identifier option * constr_ast) list - | HintsUnfold of (identifier option * qualid located) list - | HintsConstructors of identifier * qualid located - | HintsExtern of identifier * int * raw_constr_ast * raw_tactic_expr + | HintsResolve of (identifier option * constr_expr) list + | HintsImmediate of (identifier option * constr_expr) list + | HintsUnfold of (identifier option * reference) list + | HintsConstructors of identifier * reference + | HintsExtern of identifier * int * raw_constr_expr * raw_tactic_expr type search_restriction = - | SearchInside of qualid located list - | SearchOutside of qualid located list + | SearchInside of reference list + | SearchOutside of reference list type option_value = | StringValue of string @@ -111,7 +111,7 @@ type option_value = type option_ref_value = | StringRefValue of string - | QualidRefValue of qualid located + | QualidRefValue of reference type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) @@ -122,36 +122,23 @@ type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = bool (* true = Inductive; false = CoInductive *) -type sort_expr = t +type sort_expr = Rawterm.rawsort -type simple_binder = identifier * constr_ast +type simple_binder = identifier * constr_expr type 'a with_coercion = coercion_flag * 'a type constructor_expr = simple_binder with_coercion type inductive_expr = - identifier * simple_binder list * constr_ast * constructor_expr list -type fixpoint_expr = - identifier * simple_binder list * constr_ast * constr_ast -type cofixpoint_expr = - identifier * constr_ast * constr_ast -type local_binder = - | LocalRawDef of identifier * constr_ast - | LocalRawAssum of identifier list * constr_ast + identifier * simple_binder list * constr_expr * constructor_expr list type definition_expr = - | ProveBody of local_binder list * constr_ast - | DefineBody of local_binder list * raw_red_expr option * constr_ast - * constr_ast option + | ProveBody of local_binder list * constr_expr + | DefineBody of local_binder list * raw_red_expr option * constr_expr + * constr_expr option type local_decl_expr = - | AssumExpr of identifier * constr_ast - | DefExpr of identifier * constr_ast * constr_ast option + | AssumExpr of identifier * constr_expr + | DefExpr of identifier * constr_expr * constr_expr option -type precedence = int -type grammar_entry_ast = - (loc * string) * Ast.entry_type option * - grammar_associativity * raw_grammar_rule list - -type module_ast = Coqast.t -type module_binder = identifier list * module_ast +type module_binder = identifier list * module_type_ast type vernac_expr = (* Control *) @@ -161,35 +148,35 @@ type vernac_expr = | VernacVar of identifier (* Syntax *) - | VernacGrammar of string * grammar_entry_ast list + | VernacGrammar of string * raw_grammar_entry list | VernacTacticGrammar of (string * (string * grammar_production list) * raw_tactic_expr) list - | VernacSyntax of string * syntax_entry_ast list + | VernacSyntax of string * raw_syntax_entry list + | VernacSyntaxExtension of string * syntax_modifier list | VernacOpenScope of scope_name | VernacDelimiters of scope_name * (string * string) - | VernacArgumentsScope of qualid located * scope_name option list + | VernacArgumentsScope of reference * scope_name option list | VernacInfix of - grammar_associativity * precedence * string * qualid located - * scope_name option + grammar_associativity * precedence * string * reference * + scope_name option | VernacDistfix of - grammar_associativity * precedence * string * qualid located - * scope_name option + grammar_associativity * precedence * string * reference * + scope_name option | VernacNotation of - grammar_associativity * precedence * string * constr_ast - * (string * precedence) list * scope_name option + string * constr_expr * syntax_modifier list * scope_name option (* Gallina *) | VernacDefinition of definition_kind * identifier * definition_expr * - Proof_type.declaration_hook + declaration_hook | VernacStartTheoremProof of theorem_kind * identifier * - (local_binder list * Coqast.t) * bool * Proof_type.declaration_hook + (local_binder list * constr_expr) * bool * declaration_hook | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option - | VernacExactProof of constr_ast + | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * simple_binder with_coercion list | VernacInductive of inductive_flag * inductive_expr list | VernacFixpoint of fixpoint_expr list | VernacCoFixpoint of cofixpoint_expr list - | VernacScheme of (identifier * bool * qualid located * sort_expr) list + | VernacScheme of (identifier * bool * reference * sort_expr) list (* Gallina extensions *) | VernacRecord of identifier with_coercion * simple_binder list @@ -197,22 +184,22 @@ type vernac_expr = | VernacBeginSection of identifier | VernacEndSegment of identifier | VernacRequire of - export_flag option * specif_flag option * qualid located list - | VernacImport of export_flag * qualid located list - | VernacCanonical of qualid located - | VernacCoercion of strength * qualid located * class_rawexpr * class_rawexpr + export_flag option * specif_flag option * reference list + | VernacImport of export_flag * reference list + | VernacCanonical of reference + | VernacCoercion of strength * reference * class_rawexpr * class_rawexpr | VernacIdentityCoercion of strength * identifier * class_rawexpr * class_rawexpr (* Modules and Module Types *) | VernacDeclareModule of identifier * - module_binder list * module_ast option * module_ast option + module_binder list * module_type_ast option * module_ast option | VernacDeclareModuleType of identifier * - module_binder list * module_ast option + module_binder list * module_type_ast option (* Solving *) | VernacSolve of int * raw_tactic_expr - | VernacSolveExistential of int * constr_ast + | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) | VernacRequireFrom of export_flag * specif_flag option * identifier * string @@ -227,7 +214,7 @@ type vernac_expr = | VernacRestoreState of string (* Resetting *) - | VernacResetName of identifier + | VernacResetName of identifier located | VernacResetInitial | VernacBack of int @@ -236,18 +223,18 @@ type vernac_expr = loc * (identifier located * raw_tactic_expr) list | VernacHints of string list * hints | VernacHintDestruct of - identifier * (bool,unit) location * constr_ast * int * raw_tactic_expr - | VernacSyntacticDefinition of identifier * constr_ast * int option - | VernacDeclareImplicits of qualid located * int list option - | VernacSetOpacity of opacity_flag * qualid located list + identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr + | VernacSyntacticDefinition of identifier * constr_expr * int option + | VernacDeclareImplicits of reference * int list option + | VernacSetOpacity of opacity_flag * reference list | VernacUnsetOption of Goptions.option_name | VernacSetOption of 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_ast - | VernacGlobalCheck of constr_ast + | VernacCheckMayEval of raw_red_expr option * int option * constr_expr + | VernacGlobalCheck of constr_expr | VernacPrint of printable | VernacSearch of searchable * search_restriction | VernacLocate of locatable @@ -255,12 +242,12 @@ type vernac_expr = | VernacNop (* Proof management *) - | VernacGoal of constr_ast - | VernacAbort of identifier option + | VernacGoal of constr_expr + | VernacAbort of identifier located option | VernacAbortAll | VernacRestart | VernacSuspend - | VernacResume of identifier option + | VernacResume of identifier located option | VernacUndo of int | VernacFocus of int option | VernacUnfocus |