From ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 13:33:28 +0200 Subject: Unification constraint handling (#4763, #5149) Refine fix for bug #4763, fixing #5149 Tactic [Refine.solve_constraints] and global option Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of unification constraints and evar candidates to be solved. run_tactic now calls [solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics. The option allows to unset the forced solving unification constraints at each ".", letting the user control the places where the use of heuristics is done. Fix test-suite files too. --- ltac/extratactics.ml4 | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d0318fb5f6..e6498e02b2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -370,6 +370,11 @@ TACTIC EXTEND simple_refine | [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ] END +(* Solve unification constraints using heuristics or fail if any remain *) +TACTIC EXTEND solve_constraints +[ "solve_constraints" ] -> [ Refine.solve_constraints ] +END + (**********************************************************************) (* Inversion lemmas (Leminv) *) -- cgit v1.2.3 From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 24 Oct 2016 18:18:33 +0200 Subject: Lets Hints/Instances take an optional pattern In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. --- ltac/extratactics.ml4 | 3 ++- ltac/rewrite.ml | 8 ++++---- 2 files changed, 6 insertions(+), 5 deletions(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d0318fb5f6..063bfbe6d0 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -316,7 +316,8 @@ let project_hint pri l2r r = in let ctx = Evd.universe_context_set sigma in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) + let info = Vernacexpr.({hint_priority = pri; hint_pattern = None}) in + (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = Hints.add_hints true bl diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 4d7c5d0e4b..44efdd383f 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1788,7 +1788,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = new_instance (Flags.is_universe_polymorphism ()) binders instance (Some (true, CRecord (Loc.ghost,fields))) - ~global ~generalize:false ~refine:false None + ~global ~generalize:false ~refine:false Hints.empty_hint_info let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -1969,7 +1969,7 @@ let add_morphism_infer glob m n = Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) None glob + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob poly (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else @@ -1980,7 +1980,7 @@ let add_morphism_infer glob m n = let hook _ = function | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) None + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob poly (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false @@ -2004,7 +2004,7 @@ let add_morphism glob binders m s n = let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~global:glob poly binders instance (Some (true, CRecord (Loc.ghost,[]))) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) -- cgit v1.2.3 From b57c7005d81b35b2ae6c45e6ac3088a73b3c43b2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 26 Oct 2016 18:31:03 +0200 Subject: Fix Typeclasses eauto := bfs. --- ltac/g_class.ml4 | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index 18df596eb8..1adf197d6b 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -44,11 +44,22 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug | [ ] -> [ false ] END +let pr_search_strategy _prc _prlc _prt = function + | Dfs -> Pp.str "dfs" + | Bfs -> Pp.str "bfs" + +ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy +| [ "bfs" ] -> [ Bfs ] +| [ "dfs" ] -> [ Dfs ] +| [ ] -> [ Dfs ] +END + (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [ + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ set_typeclasses_debug d; + set_typeclasses_strategy s; set_typeclasses_depth depth ] END -- cgit v1.2.3 From a477dca64bb71a98fb92875df438d44d1fe54400 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 26 Oct 2016 19:20:08 +0200 Subject: Fix handling of only_classes at toplevel --- ltac/extratactics.ml4 | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 063bfbe6d0..d9780dcc8c 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -348,11 +348,12 @@ let constr_flags = { Pretyping.fail_evar = false; Pretyping.expand_evars = true } -let refine_tac ist simple c = +let refine_tac ist simple with_classes c = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let flags = constr_flags in + let flags = + { constr_flags with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in @@ -364,11 +365,23 @@ let refine_tac ist simple c = end } TACTIC EXTEND refine -| [ "refine" uconstr(c) ] -> [ refine_tac ist false c ] +| [ "refine" uconstr(c) ] -> + [ refine_tac ist false true c ] END TACTIC EXTEND simple_refine -| [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ] +| [ "simple" "refine" uconstr(c) ] -> + [ refine_tac ist true true c ] +END + +TACTIC EXTEND notcs_refine +| [ "notypeclasses" "refine" uconstr(c) ] -> + [ refine_tac ist false false c ] +END + +TACTIC EXTEND notcs_simple_refine +| [ "simple" "notypeclasses" "refine" uconstr(c) ] -> + [ refine_tac ist true false c ] END (**********************************************************************) -- cgit v1.2.3 From a4cecc13cde3239d6a86f98ba6bba0e4554306bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 3 Nov 2016 16:25:06 +0100 Subject: Rework search_strategy option handling --- ltac/g_class.ml4 | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'ltac') diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index 1adf197d6b..7e26b5d189 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -45,13 +45,14 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug END let pr_search_strategy _prc _prlc _prt = function - | Dfs -> Pp.str "dfs" - | Bfs -> Pp.str "bfs" + | Some Dfs -> Pp.str "dfs" + | Some Bfs -> Pp.str "bfs" + | None -> Pp.mt () ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy -| [ "bfs" ] -> [ Bfs ] -| [ "dfs" ] -> [ Dfs ] -| [ ] -> [ Dfs ] +| [ "(bfs)" ] -> [ Some Bfs ] +| [ "(dfs)" ] -> [ Some Dfs ] +| [ ] -> [ None ] END (* true = All transparent, false = Opaque if possible *) @@ -59,15 +60,17 @@ END VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ set_typeclasses_debug d; - set_typeclasses_strategy s; + Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth ] END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + [ typeclasses_eauto ~strategy:Bfs ~depth:d l ] | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto d l ] + [ typeclasses_eauto ~depth:d l ] | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [ typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ] END -- cgit v1.2.3 From e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 7 Nov 2016 08:41:21 +0100 Subject: More explicit name for status of unification constraints. --- ltac/extratactics.ml4 | 4 ++-- ltac/g_auto.ml4 | 2 +- ltac/tacinterp.ml | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e6498e02b2..2cca760c38 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -38,7 +38,7 @@ DECLARE PLUGIN "extratactics" let with_delayed_uconstr ist c tac = let flags = { Pretyping.use_typeclasses = false; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = Some Pfedit.solve_by_implicit_tactic; fail_evar = false; expand_evars = true @@ -342,7 +342,7 @@ END let constr_flags = { Pretyping.use_typeclasses = true; - Pretyping.use_unif_heuristics = true; + Pretyping.solve_unification_constraints = true; Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic; Pretyping.fail_evar = false; Pretyping.expand_evars = true } diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 8bc2ffd654..22a2d7fc2f 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -43,7 +43,7 @@ END let eval_uconstrs ist cs = let flags = { Pretyping.use_typeclasses = false; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = Some Pfedit.solve_by_implicit_tactic; fail_evar = false; expand_evars = true diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 08e67a0c2f..b9dcc4e18d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -646,7 +646,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let constr_flags = { use_typeclasses = true; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = Some solve_by_implicit_tactic; fail_evar = true; expand_evars = true } @@ -661,21 +661,21 @@ let interp_type = interp_constr_gen IsType let open_constr_use_classes_flags = { use_typeclasses = true; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = Some solve_by_implicit_tactic; fail_evar = false; expand_evars = true } let open_constr_no_classes_flags = { use_typeclasses = false; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = Some solve_by_implicit_tactic; fail_evar = false; expand_evars = true } let pure_open_constr_flags = { use_typeclasses = false; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = None; fail_evar = false; expand_evars = false } -- cgit v1.2.3 From 1f36cdefd841526f804bd2dd51c1d88309333376 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Nov 2016 14:47:15 +0100 Subject: Fixes to compile with ocaml 4.01 --- ltac/extratactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d9780dcc8c..8ae95c315b 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -316,7 +316,7 @@ let project_hint pri l2r r = in let ctx = Evd.universe_context_set sigma in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in - let info = Vernacexpr.({hint_priority = pri; hint_pattern = None}) in + let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = -- cgit v1.2.3