From ab8e47207245277cb5b92b80a92ae78ede5bfafe Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 12 Dec 2017 15:32:59 +0000 Subject: [vernac] vernac_expr no longer recursive --- intf/vernacexpr.ml | 12 ++++---- parsing/g_vernac.ml4 | 32 ++++++++++---------- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 4 +-- plugins/ssr/ssrvernac.ml4 | 4 +-- printing/ppvernac.ml | 53 +++++++++++++++++---------------- stm/proofBlockDelimiter.ml | 4 +-- stm/stm.ml | 9 +++--- stm/vernac_classifier.ml | 14 +++++---- vernac/vernacentries.ml | 53 ++++++++++++++++----------------- vernac/vernacprop.ml | 8 ++--- 11 files changed, 98 insertions(+), 97 deletions(-) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index ba8dd4182..f35eab47f 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -323,7 +323,7 @@ type vernac_argument_status = { implicit_status : vernac_implicit_status; } -type vernac_expr = +type nonrec vernac_expr = | VernacLoad of verbose_flag * string (* Syntax *) @@ -472,13 +472,13 @@ type vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list - (* Flags *) - | VernacProgram of vernac_expr - | VernacPolymorphic of bool * vernac_expr - | VernacLocal of bool * vernac_expr +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool type vernac_control = - | VernacExpr of vernac_expr + | 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 located diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 92e60f465..d498bda34 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -72,36 +72,36 @@ GEXTEND Gram | 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 - | v = vernac -> VernacExpr(v) ] + | (f, v) = vernac -> VernacExpr(f, v) ] ] ; vernac: - [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) - | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) + [ [ 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"; v = vernac_aux -> VernacPolymorphic (true, v) - | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) + [ [ 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 + [ [ 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 ] ] + [ [ prfcom = command_entry -> ([], prfcom) ] ] ; noedit_mode: [ [ c = query_command -> c None] ] @@ -621,11 +621,9 @@ GEXTEND Gram VernacCanonical (AN qid) | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> VernacCanonical (ByNotation ntn) - | IDENT "Canonical"; IDENT "Structure"; qid = global; - d = def_body -> + | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacLocal(false, - VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d)) + VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 2fd6f53c4..4b828a702 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b4e17c5d1..0b929b8ca 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 4f530a0ae..c0479dd24 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -551,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d ))) + ((Loc.tag s),None), d) ]]; END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1..1d7436e9f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -535,17 +535,25 @@ open Decl_kinds | SsFwdClose e -> "("^aux e^")*" in Pp.str (aux e) - let rec pr_vernac_expr v = + let pr_extend s cl = + let pr_arg a = + try pr_gen a + with Failure _ -> str "" in + try + let rl = Egramml.get_extend_vernac_rule s in + let rec aux rl cl = + match rl, cl with + | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl + | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | [], [] -> [] + | _ -> assert false in + hov 1 (pr_sequence identity (aux rl cl)) + with Not_found -> + hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") + + let pr_vernac_expr v = let return = tag_vernac v in match v with - | VernacPolymorphic (poly, v) -> - let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac_expr v) - | VernacProgram v -> - return (keyword "Program" ++ spc() ++ pr_vernac_expr v) - | VernacLocal (local, v) -> - return (pr_locality local ++ spc() ++ pr_vernac_expr v) - | VernacLoad (f,s) -> return ( keyword "Load" @@ -1203,26 +1211,21 @@ open Decl_kinds | VernacEndSubproof -> return (str "}") - and pr_extend s cl = - let pr_arg a = - try pr_gen a - with Failure _ -> str "" in - try - let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = - match rl, cl with - | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl - | [], [] -> [] - | _ -> assert false in - hov 1 (pr_sequence identity (aux rl cl)) - with Not_found -> - hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") +let pr_vernac_flag = + function + | VernacPolymorphic true -> keyword "Polymorphic" + | VernacPolymorphic false -> keyword "Monomorphic" + | VernacProgram -> keyword "Program" + | VernacLocal local -> pr_locality local let rec pr_vernac_control v = let return = tag_vernac v in match v with - | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v' + | VernacExpr (f, v') -> + List.fold_right + (fun f a -> pr_vernac_flag f ++ spc() ++ a) + f + (pr_vernac_expr v' ++ sep_end v') | VernacTime (_,(_,v)) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, (_,v)) -> diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b5b9a01..bebc4d5d5 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -96,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b))) + recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) } | `Not -> `Leaks @@ -125,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof) + recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) } | `Not -> `Leaks diff --git a/stm/stm.ml b/stm/stm.ml index 7045df0ed..5f4fe6565 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1498,7 +1498,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1646,7 +1646,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> @@ -2177,7 +2177,7 @@ let collect_proof keep cur hd brkind id = (try let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in - v.expr <- VernacExpr(VernacProof(t, Some hint)); + v.expr <- VernacExpr([], VernacProof(t, Some hint)); `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2872,10 +2872,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let rec opacity_of_produced_term = function + let opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity - | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2fa47ba43..99b56d484 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -49,17 +49,13 @@ let declare_vernac_classifier classifiers := !classifiers @ [s,f] let classify_vernac e = - let rec static_classifier ~poly e = match e with + let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | ( VernacSetOption (l,_) | VernacUnsetOption l) when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> VtSideff [], VtNow - (* Nested vernac exprs *) - | VernacProgram e -> static_classifier ~poly e - | VernacLocal (_,e) -> static_classifier ~poly e - | VernacPolymorphic (b, e) -> static_classifier ~poly:b e (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater @@ -193,7 +189,13 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function - | VernacExpr e -> static_classifier ~poly e + | VernacExpr (f, e) -> + let poly = List.fold_left (fun poly f -> + match f with + | VernacPolymorphic b -> b + | (VernacProgram | VernacLocal _) -> poly + ) poly f in + static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) -> static_control_classifier ~poly e diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ae62fcfeb..814dc1411 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1959,11 +1959,6 @@ let interp ?proof ~atts ~st c = (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - (* Handled elsewhere *) - | VernacProgram _ - | VernacPolymorphic _ - | VernacLocal _ -> assert false - (* Syntax *) | VernacSyntaxExtension (infix, sl) -> vernac_syntax_extension atts infix sl @@ -2200,10 +2195,31 @@ let with_fail st b f = let interp ?(verbosely=true) ?proof ~st (loc,c) = let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in + let flags f atts = + List.fold_left + (fun (polymorphism, atts) f -> + match f with + | VernacProgram when not atts.program -> + (polymorphism, { atts with program = true }) + | VernacProgram -> + user_err Pp.(str "Program mode specified twice") + | VernacPolymorphic b when polymorphism = None -> + (Some b, atts) + | VernacPolymorphic _ -> + user_err Pp.(str "Polymorphism specified twice") + | VernacLocal b when Option.is_empty atts.locality -> + (polymorphism, { atts with locality = Some b }) + | VernacLocal _ -> + user_err Pp.(str "Locality specified twice") + ) + (None, atts) + f + in let rec control = function - | VernacExpr v -> - let atts = { loc; locality = None; polymorphic = false; program = orig_program_mode; } in - aux ~atts v + | VernacExpr (f, v) -> + let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in + aux ~polymorphism ~atts v + | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> current_timeout := Some n; control v @@ -2212,25 +2228,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | VernacTime (batch, (_loc,v)) -> System.with_time ~batch control v; - and aux ?polymorphism ~atts = function - - | VernacProgram c when not atts.program -> - aux ?polymorphism ~atts:{ atts with program = true } c - - | VernacProgram _ -> - user_err Pp.(str "Program mode specified twice") - - | VernacPolymorphic (b, c) when polymorphism = None -> - aux ~polymorphism:b ~atts:atts c - - | VernacPolymorphic (b, c) -> - user_err Pp.(str "Polymorphism specified twice") - - | VernacLocal (b, c) when Option.is_empty atts.locality -> - aux ?polymorphism ~atts:{atts with locality = Some b} c - - | VernacLocal _ -> - user_err Pp.(str "Locality specified twice") + and aux ~polymorphism ~atts : _ -> unit = + function | VernacLoad (_,fname) -> vernac_load control fname diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 4fdc78dd2..3932d1c7b 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -12,14 +12,14 @@ open Vernacexpr let rec under_control = function - | VernacExpr c -> c + | VernacExpr (_, c) -> c | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function - | VernacExpr c -> false + | VernacExpr _ -> false | VernacRedirect (_,(_,c)) | VernacTime (_,(_,c)) | VernacTimeout (_,c) -> has_Fail c @@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function (* NB: Reset is now allowed again as asked by A. Chlipala *) let is_reset = function - | VernacExpr VernacResetInitial - | VernacExpr (VernacResetName _) -> true + | VernacExpr ( _, VernacResetInitial) + | VernacExpr (_, VernacResetName _) -> true | _ -> false let is_debug cmd = match under_control cmd with -- cgit v1.2.3