From 957704d5487d50342967351a47c76c4142bb9edb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 21 Feb 2024 20:53:41 +0100 Subject: [PATCH] fix tac_solve (fix #1041) --- src/core/libMeta.ml | 22 ++++++++----- src/core/unif.ml | 78 ++++++++++++++++++++++---------------------- src/handle/tactic.ml | 32 +++++++++++++----- tests/KO/1041.lp | 43 ++++++++++++++++++++++++ tests/OK/try.lp | 2 +- 5 files changed, 119 insertions(+), 58 deletions(-) create mode 100644 tests/KO/1041.lp diff --git a/src/core/libMeta.ml b/src/core/libMeta.ml index efae4454c..a1e72ea3a 100644 --- a/src/core/libMeta.ml +++ b/src/core/libMeta.ml @@ -3,6 +3,11 @@ open Lplib open Term open Timed +open Common + +(** Logging function for unification. *) +let log = Logger.make 'a' "meta" "metavariables" +let log = log.pp let meta_counter : int Stdlib.ref = Stdlib.ref (-1) @@ -11,12 +16,13 @@ let reset_meta_counter () = Stdlib.(meta_counter := -1) (** [fresh p ?name a n] creates a fresh metavariable of type [a] and arity [n] with the optional name [name], and adds it to [p]. *) -let fresh : problem -> term -> int -> meta = - fun p a n -> +let fresh : problem -> term -> int -> meta = fun p a n -> let m = {meta_key = Stdlib.(incr meta_counter; !meta_counter); - meta_type = ref a; meta_arity = n; - meta_value = ref None } in - p := {!p with metas = MetaSet.add m !p.metas}; m + meta_type = ref a; meta_arity = n; meta_value = ref None } in + if Logger.log_enabled() then log "fresh ?%d" m.meta_key; + p := {!p with metas = MetaSet.add m !p.metas}; + if Logger.log_enabled() then log "%a" Print.problem p; + m (** [fresh_box p a n] is the boxed counterpart of [fresh_meta]. It is only useful in the rare cases where the type of a metavariable @@ -40,8 +46,7 @@ let set : problem -> meta -> tmbinder -> unit = fun p m v -> (** [make p ctx a] creates a fresh metavariable term of type [a] in the context [ctx], and adds it to [p]. *) -let make : problem -> ctxt -> term -> term = - fun p ctx a -> +let make : problem -> ctxt -> term -> term = fun p ctx a -> let a, k = Ctxt.to_prod ctx a in let m = fresh p a k in let get_var (x,_,d) = if d = None then Some (mk_Vari x) else None in @@ -51,8 +56,7 @@ let make : problem -> ctxt -> term -> term = a fresh {e boxed} metavariable in {e boxed} context [bctx] of {e boxed} type [a]. It is the same as [lift (make p c b)] (provided that [bctx] is boxed [c] and [a] is boxed [b]), but more efficient. *) -let bmake : problem -> bctxt -> tbox -> tbox = - fun p bctx a -> +let bmake : problem -> bctxt -> tbox -> tbox = fun p bctx a -> let (a, k) = Ctxt.to_prod_box bctx a in let m = fresh_box p a k in let get_var (x, _) = _Vari x in diff --git a/src/core/unif.ml b/src/core/unif.ml index cb8aae77b..8b96d18aa 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -8,8 +8,8 @@ open LibTerm open Print (** Logging function for unification. *) -let log_unif = Logger.make 'u' "unif" "unification" -let log_unif = log_unif.pp +let log = Logger.make 'u' "unif" "unification" +let log = log.pp (** Given a meta [m] of type [Πx1:a1,..,Πxn:an,b], [set_to_prod p m] sets [m] to a product term of the form [Πy:m1[x1;..;xn],m2[x1;..;xn;y]] with [m1] @@ -32,7 +32,7 @@ let set_to_prod : problem -> meta -> unit = fun p m -> (* result *) let r = _Prod a b in if Logger.log_enabled () then - log_unif (red "%a ≔ %a") meta m term (Bindlib.unbox r); + log (red "%a ≔ %a") meta m term (Bindlib.unbox r); LibMeta.set p m (Bindlib.unbox (Bindlib.bind_mvar vs r)) (** [type_app c a ts] returns [Some u] where [u] is a type of [add_args x ts] @@ -46,14 +46,14 @@ let rec type_app : ctxt -> term -> term list -> term option = fun c a ts -> (** [add_constr p c] adds the constraint [c] into [p.to_solve]. *) let add_constr : problem -> constr -> unit = fun p c -> - if Logger.log_enabled () then log_unif (mag "add %a") constr c; + if Logger.log_enabled () then log (mag "add %a") constr c; p := {!p with to_solve = c::!p.to_solve} (** [try_unif_rules p c s t] tries to simplify the unification problem [c ⊢ s ≡ t] with the user-defined unification rules. *) let try_unif_rules : problem -> ctxt -> term -> term -> bool = fun p c s t -> - if Logger.log_enabled () then log_unif "check unif_rules"; + if Logger.log_enabled () then log "check unif_rules"; let exception No_match in let open Unif_rule in try @@ -82,10 +82,10 @@ let try_unif_rules : problem -> ctxt -> term -> term -> bool = Error.fatal_no_pos "Untypable unification problem." in let cs = List.map (fun (t,u) -> sanitise (c,t,u)) (unpack rhs) in - if Logger.log_enabled () then log_unif "rewrites to: %a" constrs cs; + if Logger.log_enabled () then log "rewrites to: %a" constrs cs; true with No_match -> - if Logger.log_enabled () then log_unif "found no unif_rule"; + if Logger.log_enabled () then log "found no unif_rule"; false (** [instantiable c m ts u] tells whether, in a problem [m[ts]=u], [m] can @@ -115,36 +115,35 @@ let do_type_check = Stdlib.ref true metavariables of [p]. *) let instantiate : problem -> ctxt -> meta -> term array -> term -> bool = fun p c m ts u -> - if Logger.log_enabled () then log_unif "try instantiate"; + if Logger.log_enabled () then log "try instantiate"; match instantiation c m ts u with | Some b when Bindlib.is_closed b -> - let do_instantiate() = - if Logger.log_enabled () then - log_unif (red "%a ≔ %a") meta m term u; + let do_instantiate p = + if Logger.log_enabled () then log (red "%a ≔ %a") meta m term u; LibMeta.set p m (Bindlib.unbox b); p := {!p with recompute = true}; true in if Stdlib.(!do_type_check) then begin - if Logger.log_enabled () then log_unif "check typing"; + if Logger.log_enabled () then log "check typing"; let typ_mts = match type_app c !(m.meta_type) (Array.to_list ts) with | Some a -> a | None -> assert false in - if Infer.check_noexn p c u typ_mts <> None then do_instantiate() - else (if Logger.log_enabled () then log_unif "typing failed"; false) + if Infer.check_noexn p c u typ_mts <> None then do_instantiate p + else (if Logger.log_enabled () then log "typing failed"; false) end - else do_instantiate() + else do_instantiate p | i -> if Logger.log_enabled () then begin match i with | None -> - if LibMeta.occurs m c u then log_unif "occur check failed" - else log_unif "arguments are not distinct variables: %a" + if LibMeta.occurs m c u then log "occur check failed" + else log "arguments are not distinct variables: %a" (Array.pp term "; ") ts - | Some _ -> log_unif "not closed" + | Some _ -> log "not closed" end; false @@ -155,9 +154,9 @@ let instantiate : problem -> ctxt -> meta -> term array -> term -> bool = let add_to_unsolved : problem -> ctxt -> term -> term -> unit = fun p c t1 t2 -> if Eval.pure_eq_modulo c t1 t2 then - (if Logger.log_enabled () then log_unif "equivalent terms") + (if Logger.log_enabled () then log "equivalent terms") else if not (try_unif_rules p c t1 t2) then - (if Logger.log_enabled () then log_unif "move to unsolved"; + (if Logger.log_enabled () then log "move to unsolved"; p := {!p with unsolved = (c,t1,t2)::!p.unsolved}) (** [decompose p c ts1 ts2] tries to decompose a problem of the form [h ts1 ≡ @@ -165,7 +164,7 @@ let add_to_unsolved : problem -> ctxt -> term -> term -> unit = [t1;..;tn]] and [ts2 = [u1;..;un]]. *) let decompose : problem -> ctxt -> term list -> term list -> unit = fun p c ts1 ts2 -> - if Logger.log_enabled () && ts1 <> [] then log_unif "decompose"; + if Logger.log_enabled () && ts1 <> [] then log "decompose"; List.iter2 (fun a b -> add_constr p (c,a,b)) ts1 ts2 (** For a problem of the form [h1 ≡ h2] with [h1 = m[ts]], [h2 = Πx:_,_] (or @@ -174,7 +173,7 @@ let decompose : problem -> ctxt -> term list -> term list -> unit = [p]. *) let imitate_prod : problem -> ctxt -> meta -> term -> term -> unit = fun p c m h1 h2 -> - if Logger.log_enabled () then log_unif "imitate_prod %a" meta m; + if Logger.log_enabled () then log "imitate_prod %a" meta m; set_to_prod p m; add_constr p (c,h1,h2) (** For a problem [m[vs] ≡ s(ts)] in context [c], where [vs] are distinct @@ -189,7 +188,7 @@ let imitate_inj : -> bool = fun p c m vs us s ts -> if Logger.log_enabled () then - log_unif "imitate_inj %a ≡ %a" term (add_args (mk_Meta(m,vs)) us) + log "imitate_inj %a ≡ %a" term (add_args (mk_Meta(m,vs)) us) term (add_args (mk_Symb s) ts); let exception Cannot_imitate in try @@ -216,7 +215,7 @@ let imitate_inj : | _ -> raise Cannot_imitate in build (List.length ts) [] !(s.sym_type) in - if Logger.log_enabled () then log_unif (red "%a ≔ %a") meta m term t; + if Logger.log_enabled () then log (red "%a ≔ %a") meta m term t; LibMeta.set p m (binds vars lift t); true with Cannot_imitate | Invalid_argument _ -> false @@ -242,7 +241,7 @@ let imitate_lam_cond : term -> term list -> bool = fun h ts -> a new metavariable of arity [n+1] and type [Πx1:a1,..,Πxn:an,Πx:m2[x1,..,xn],TYPE], and do as in the previous case. *) let imitate_lam : problem -> ctxt -> meta -> unit = fun p c m -> - if Logger.log_enabled () then log_unif "imitate_lam %a" meta m; + if Logger.log_enabled () then log "imitate_lam %a" meta m; let n = m.meta_arity in let env, t = Env.of_prod_nth c n !(m.meta_type) in let of_prod a b = @@ -280,19 +279,19 @@ let imitate_lam : problem -> ctxt -> meta -> unit = fun p c m -> let xu1 = _Abst a (Bindlib.bind_var x u1) in let v = Bindlib.bind_mvar (Env.vars env) xu1 in if Logger.log_enabled () then - log_unif (red "%a ≔ %a") meta m term (Bindlib.unbox xu1); + log (red "%a ≔ %a") meta m term (Bindlib.unbox xu1); LibMeta.set p m (Bindlib.unbox v) (** [inverse_opt s ts v] returns [Some(t, inverse s v)] if [ts=[t]], [s] is injective and [inverse s v] does not fail, and [None] otherwise. *) let inverse_opt : sym -> term list -> term -> (term * term) option = fun s ts v -> - if Logger.log_enabled () then log_unif "try inverse %a" sym s; + if Logger.log_enabled () then log "try inverse %a" sym s; try match ts with | [t] when is_injective s -> Some (t, Inverse.inverse s v) | _ -> raise Not_found - with Not_found -> if Logger.log_enabled () then log_unif "failed"; None + with Not_found -> if Logger.log_enabled () then log "failed"; None (** Exception raised when a constraint is not solvable. *) exception Unsolvable @@ -316,7 +315,7 @@ let inverse : problem -> ctxt -> term -> sym -> term list -> term -> unit = match unfold t2 with | Prod _ when is_constant s -> error t1 t2 | _ -> - if Logger.log_enabled () then log_unif "move to unsolved"; + if Logger.log_enabled () then log "move to unsolved"; p := {!p with unsolved = (c, t1, t2)::!p.unsolved} (** [sym_sym_whnf p c t1 s1 ts1 t2 s2 ts2 p] handles the case [s1(ts1) = @@ -341,14 +340,15 @@ let sym_sym_whnf : Otherwise, [p.to_solve] is empty but [p.unsolved] may still contain constraints that could not be simplified. *) let solve : problem -> unit = fun p -> - while !p.to_solve <> [] || (!p.recompute && !p.unsolved <> []) do + while !p.to_solve <> [] || (!p.recompute && !p.unsolved <> []) do begin + log "solve %a" problem p; match !p.to_solve with | [] -> - if Logger.log_enabled () then log_unif "recompute"; + if Logger.log_enabled () then log "recompute"; p := {!p with to_solve = !p.unsolved; unsolved = []; recompute = false} | (c,t1,t2)::to_solve -> (*if Logger.log_enabled () then - log_unif "%d constraints" (1 + List.length to_solve);*) + log "%d constraints" (1 + List.length to_solve);*) (* We remove the first constraint from [p] for not looping. *) p := {!p with to_solve}; @@ -356,9 +356,9 @@ let solve : problem -> unit = fun p -> (* We first try without normalizing wrt user-defined rules. *) let tags = [`NoRw; `NoExpand] in let t1 = Eval.whnf ~tags c t1 and t2 = Eval.whnf ~tags c t2 in - if Logger.log_enabled () then log_unif (gre "solve %a") constr (c,t1,t2); + if Logger.log_enabled () then log (gre "solve %a") constr (c,t1,t2); if Eval.pure_eq_modulo ~tags c t1 t2 then - (if Logger.log_enabled () then log_unif "equivalent terms") + (if Logger.log_enabled () then log "equivalent terms") else let h1, ts1 = get_args t1 and h2, ts2 = get_args t2 in @@ -369,7 +369,7 @@ let solve : problem -> unit = fun p -> | Prod(a1,b1), Prod(a2,b2) | Abst(a1,b1), Abst(a2,b2) -> (* [ts1] and [ts2] must be empty because of typing or normalization. *) - if Logger.log_enabled () then log_unif "decompose"; + if Logger.log_enabled () then log "decompose"; add_constr p (c,a1,a2); let (x,b1,b2) = Bindlib.unbind2 b1 b2 in let c' = (x,a1,None)::c in @@ -414,9 +414,9 @@ let solve : problem -> unit = fun p -> | _ -> (* We normalize wrt user-defined rules and try again. *) - if Logger.log_enabled () then log_unif "whnf"; + if Logger.log_enabled () then log "whnf"; let t1 = Eval.whnf c t1 and t2 = Eval.whnf c t2 in - if Logger.log_enabled () then log_unif (gre "solve %a") constr (c,t1,t2); + if Logger.log_enabled () then log (gre "solve %a") constr (c,t1,t2); let h1, ts1 = get_args t1 and h2, ts2 = get_args t2 in match h1, h2 with @@ -426,7 +426,7 @@ let solve : problem -> unit = fun p -> | Prod(a1,b1), Prod(a2,b2) | Abst(a1,b1), Abst(a2,b2) -> (* [ts1] and [ts2] must be empty because of typing or normalization. *) - if Logger.log_enabled () then log_unif "decompose"; + if Logger.log_enabled () then log "decompose"; add_constr p (c,a1,a2); let (x,b1,b2) = Bindlib.unbind2 b1 b2 in let c' = (x,a1,None)::c in @@ -482,7 +482,7 @@ let solve : problem -> unit = fun p -> | _, Symb s -> inverse p c t2 s ts2 t1 | _ -> add_to_unsolved p c t1 t2 - done + end done (** [solve_noexn ~type_check p] tries to simplify the constraints of [p]. It returns [false] if it finds a constraint that cannot be diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index abee6a8eb..619fc678d 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -75,24 +75,38 @@ let tac_admit: Sig_state.t -> popt -> proof_state -> goal_typ -> proof_state = state [ps] and fails if constraints are unsolvable. *) let tac_solve : popt -> proof_state -> proof_state = fun pos ps -> if Logger.log_enabled () then log "@[tac_solve@ %a@]" goals ps; + (* convert the proof_state into a problem *) let gs_typ, gs_unif = List.partition is_typ ps.proof_goals in let p = new_problem() in - let f ms = function + let add_meta ms = function | Unif _ -> ms | Typ gt -> MetaSet.add gt.goal_meta ms in - p := {!p with metas = List.fold_left f MetaSet.empty gs_typ + p := {!p with metas = List.fold_left add_meta MetaSet.empty gs_typ ; to_solve = List.rev_map get_constr gs_unif}; + (* try to solve the problem *) if not (Unif.solve_noexn p) then fatal pos "Unification goals are unsatisfiable."; - (* remove in [gs_typ] the goals that have been instantiated, and simplify - the others. *) - let not_instantiated = function - | Typ gt when !(gt.goal_meta.meta_value) <> None -> None - | gt -> Some (Goal.simpl Eval.simplify gt) + (* compute the new list of goals by preserving the order of initial goals + and adding the new goals at the end *) + let non_instantiated = function + | Typ gt -> !(gt.goal_meta.meta_value) = None + | _ -> assert false in - let gs_typ = List.filter_map not_instantiated gs_typ in - {ps with proof_goals = List.map (fun c -> Unif c) !p.unsolved @ gs_typ} + let gs_typ = List.filter non_instantiated gs_typ in + let is_eq_goal_meta m = function + | Typ gt -> m == gt.goal_meta + | _ -> assert false + in + let add_goal m gs = + if List.exists (is_eq_goal_meta m) gs_typ then gs + else Goal.of_meta m :: gs + in + let proof_goals = + gs_typ @ MetaSet.fold add_goal (!p).metas + (List.map (fun c -> Unif c) (!p).unsolved) + in + {ps with proof_goals} (** [tac_refine pos ps gt gs p t] refines the typing goal [gt] with [t]. [p] is the set of metavariables created by the scoping of [t]. *) diff --git a/tests/KO/1041.lp b/tests/KO/1041.lp new file mode 100644 index 000000000..fe28c6b7d --- /dev/null +++ b/tests/KO/1041.lp @@ -0,0 +1,43 @@ +constant symbol Prop : TYPE; +builtin "Prop" ≔ Prop; +injective symbol π : Prop → TYPE; // `p +builtin "P" ≔ π; + +constant symbol Set : TYPE; +injective symbol τ : Set → TYPE; +builtin "T" ≔ τ; + +constant symbol ⊥ : Prop; // \bot + +constant symbol ⇒ : Prop → Prop → Prop; notation ⇒ infix right 5; // => +rule π ($p ⇒ $q) ↪ π $p → π $q; + +symbol ¬ p ≔ p ⇒ ⊥; // ~~ or \neg +notation ¬ prefix 35; + +constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall +rule π (∀ $f) ↪ Π x, π ($f x); + +injective symbol πᶜ p ≔ π (¬ ¬ p); + +flag "print_implicits" on; +flag "print_domains" on; +//flag "print_meta_types" on; + +symbol ∀ᶜ [a] p ≔ `∀ x : τ a, ¬ ¬ (p x); notation ∀ᶜ quantifier; + +//debug +hiuta; +opaque symbol ∀ᶜᵢ p : (Π x, πᶜ (p x)) → πᶜ (∀ᶜ p) ≔ +begin + print; + //debug -hiuta; + assume p Hnnpx Hnnnpx; + apply Hnnnpx; + assume x Hnnp; + apply Hnnpx x; + assume Hnp; + apply Hnnp; + apply Hnp; +end; + +print ∀ᶜᵢ; diff --git a/tests/OK/try.lp b/tests/OK/try.lp index 065506da3..fff5b2d95 100644 --- a/tests/OK/try.lp +++ b/tests/OK/try.lp @@ -47,7 +47,7 @@ symbol ∨ₑ [p q r] : P (p ∨ q) → (P p → P r) → (P q → P r) → P r; symbol ¬: Prop → Prop; notation ¬ prefix 2; -symbol eq_simp x : P ((x = x) = ⊤); +symbol eq_simp [a] (x:T a) : P ((x = x) = ⊤); symbol eq_simp_neg_l x : P ((¬ x = x) = ⊥); symbol eq_simp_refl_r x : P ((¬ x = x) = ⊥); symbol eq_simp_2 x : P ((⊥ = x) = ¬ x);