From 260965dcf60d793ba01110ace8945cf51ef6531f Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:34:01 +0000 Subject: Makes the new Proofview.tactic the basic type of Ltac. On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/quote/quote.ml | 54 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 32 insertions(+), 22 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 92b27c3e83..0cf4d3bb49 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -109,6 +109,7 @@ open Pattern open Patternops open Matching open Tacmach +open Proofview.Notations (*i*) (*s First, we need to access some Coq constants @@ -219,14 +220,16 @@ let compute_rhs bodyi index_of_f = (*s Now the function [compute_ivs] itself *) -let compute_ivs gl f cs = +let compute_ivs f cs = let cst = try destConst f with DestKO -> i_can't_do_that () in let body = Environ.constant_value (Global.env()) cst in match decomp_term body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in - begin match decomp_term body3 with + Tacmach.New.pf_apply Reductionops.is_conv >- fun is_conv -> + Goal.return + begin match decomp_term body3 with | Case(_,p,c,lci) -> (*

Case c of c1 ... cn end *) let n_lhs_rhs = ref [] and v_lhs = ref (None : constr option) @@ -245,8 +248,7 @@ let compute_ivs gl f cs = (* Then we test if the RHS is the RHS for variables *) else begin match decompose_app bodyi with | vmf, [_; _; a3; a4 ] - when isRel a3 && isRel a4 && - pf_conv_x gl vmf + when isRel a3 && isRel a4 && is_conv vmf (Lazy.force coq_varmap_find)-> v_lhs := Some (compute_lhs (snd (List.hd args3)) @@ -389,7 +391,10 @@ module Constrhash = Hashtbl.Make [ivs : inversion_scheme]\\ [lc: constr list]\\ [gl: goal sigma]\\ *) -let quote_terms ivs lc gl = +let quote_terms ivs lc = + (* spiwack: [Goal.return () >- fun () -> … ] suspends the effects in + [Coqlib.check_required_library]. *) + Goal.return () >- fun () -> Coqlib.check_required_library ["Coq";"quote";"Quote"]; let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) @@ -436,36 +441,41 @@ let quote_terms ivs lc gl = auxl ivs.normal_lhs_rhs in let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) - ivs.return_type )) + Goal.return begin + (lp, (btree_of_array (Array.of_list (List.rev !varlist)) + ivs.return_type )) + end (*s actually we could "quote" a list of terms instead of a single term. Ring for example needs that, but Ring doesn't use Quote yet. *) -let quote f lid gl = - let f = pf_global gl f in - let cl = List.map (pf_global gl) lid in - let ivs = compute_ivs gl f cl in - let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with +let quote f lid = + Tacmach.New.pf_global f >>- fun f -> + Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl -> + compute_ivs f cl >>- fun ivs -> + Goal.concl >>- fun concl -> + quote_terms ivs [concl] >>- fun quoted_terms -> + let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false in match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl - -let gen_quote cont c f lid gl = - let f = pf_global gl f in - let cl = List.map (pf_global gl) lid in - let ivs = compute_ivs gl f cl in - let (p, vm) = match quote_terms ivs [c] gl with + | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast) + | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast) + +let gen_quote cont c f lid = + Tacmach.New.pf_global f >>- fun f -> + Goal.sensitive_list_map Tacmach.New.pf_global lid >>- fun cl -> + compute_ivs f cl >>- fun ivs -> + quote_terms ivs [c] >>- fun quoted_terms -> + let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false in match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) gl - | Some _ -> cont (mkApp (f, [| vm; p |])) gl + | None -> cont (mkApp (f, [| p |])) + | Some _ -> cont (mkApp (f, [| vm; p |])) (*i -- cgit v1.2.3