From e7c3645eed3088a7a395b10f2f029e249674bdc5 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Fri, 26 Jun 2026 20:06:58 +0200 Subject: [PATCH 1/5] with_goal --- CHANGES.md | 2 ++ doc/structure.rst | 1 + doc/tacticals.rst | 6 ++++ src/handle/gconf.ml | 48 ++++++++++++++++++++++++++++++++ src/handle/tactic.ml | 62 ++++++++++++++++++++++++++++++++++++++++-- src/parsing/pretty.ml | 1 + src/parsing/syntax.ml | 3 ++ tests/OK/Tactic.lp | 6 +++- tests/export_dk.sh | 2 +- tests/export_raw_dk.sh | 2 +- 10 files changed, 128 insertions(+), 5 deletions(-) create mode 100644 src/handle/gconf.ml diff --git a/CHANGES.md b/CHANGES.md index 494c786f9..2b45ec6dc 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -21,6 +21,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - Tactic `first_hyp t` which iterates parameterized tactic term t with each hypothsis as parameter until it succeeds. - Tactic `#print` to print a symbol or the current goal. - Export to Lean. +- Tactic `#with_goal t` which calls term tactic t with current goal of type Prop as parameter. ### Changed @@ -32,6 +33,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - LSP server: position of the error is removed from diagnostics when the error occurs in the file currently open in the editor. - Syntax of search query is modified as follows : `in` is used instead of `|` (filtering). `with` is used instead of `,` (conjunction). `|` is used instead of `;` (disjunction). - Type of `#assume` in order to generate a new symbol and use it inside a tactic term. +- Type of `#refine' is in fact `String -> Tactic` ### Fixed diff --git a/doc/structure.rst b/doc/structure.rst index ec7b20853..3273b8b1f 100644 --- a/doc/structure.rst +++ b/doc/structure.rst @@ -87,6 +87,7 @@ Overview of directories and files * ``command.ml``: command handling * ``compile.ml``: file parsing and compiling (.lpo files) + * ``gconf.ml``: builtins needed to build current goal (tactic #with_goal) * ``inductive.ml``: generation of induction principles * ``query.ml``: handling of queries (commands that do not change the signature or the proof state) diff --git a/doc/tacticals.rst b/doc/tacticals.rst index 01e52bbb5..478b402ea 100644 --- a/doc/tacticals.rst +++ b/doc/tacticals.rst @@ -38,6 +38,7 @@ The BNF grammar of tactics is in `lambdapi.bnf and forAll. diff --git a/src/handle/gconf.ml b/src/handle/gconf.ml new file mode 100644 index 000000000..9f56414ac --- /dev/null +++ b/src/handle/gconf.ml @@ -0,0 +1,48 @@ +(** Configuration for tactics based on first-order logic. *) + +open Common open Error +open Core open Term + +type config = + { symb_Prop: sym (** Type of propositions. *) + ; symb_P : sym (** Encoding of propositions. *) + ; symb_Set : sym (** Type of sets. *) + ; symb_T : sym (** Encoding of types. *) + ; symb_imp : sym (** Implication(⇒) symbol. *) + ; symb_all : sym (** Forall(∀) symbol. *) + } + +(** [get_config ss pos] build the configuration using [ss]. *) +let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> + let builtin = Builtin.get ss pos [] in + let symb_P = builtin "P" and symb_T = builtin "T" in + let symb_Prop = + match unfold Timed.(!(symb_P.sym_type)) with + | Prod(a,_) -> + begin + match unfold a with + | Symb s -> s + | _ -> + fatal pos "The type of %a is not of the form Prop → _ \ + with Prop a symbol." Print.sym symb_P + end + | _ -> fatal pos "The type of %a is not a product" Print.sym symb_P + and symb_Set = + match unfold Timed.(!(symb_T.sym_type)) with + | Prod(a,_) -> + begin + match unfold a with + | Symb s -> s + | _ -> + fatal pos "The type of %a is not of the form Prop → _ \ + with Prop a symbol." Print.sym symb_T + end + | _ -> fatal pos "The type of %a is not a product" Print.sym symb_T + in + { symb_Prop + ; symb_P + ; symb_Set + ; symb_T + ; symb_imp = builtin "imp" + ; symb_all = builtin "all" + } diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 269e567d4..6ee5fc402 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -194,6 +194,54 @@ let get_prod_ids env = else List.rev acc in aux [] +(** [get_goal pos ps gt] tries to build a goal [g] such as typing goal + [gt] = [Prf p]. It uses builtins P, T, imp and all. +*) +let get_goal: popt -> Sig_state.t -> goal_typ -> Term.term = fun pos ss gt -> + let cfg = Gconf.get_config ss pos in + let imp = mk_Symb (cfg.symb_imp) in + let all = mk_Symb (cfg.symb_all) in + + (* Extract the term from the goal type (get “u” from “Prf u”). *) + let is_prf g = + match get_args g with + | t, (u::_) when is_symb cfg.symb_P t -> Some u + | _ -> None + in + let is_set g = + match get_args g with + | t, (u::_) when is_symb cfg.symb_T t -> Some u + | _ -> None + in + let rec as_prop g = + match is_prf g with + | Some u -> u + | None -> match g with + | Prod(p,bi) when binder_name bi = "_" -> + begin + let (_,q) = unbind bi in + match is_prf p with + Some u -> mk_Appl(mk_Appl (imp,u), as_prop q) + | None -> + fatal pos "Goal %a not of the form (%a _ [-> ...])." + term gt.goal_type sym cfg.symb_P + end + | Prod(p,bi) -> + begin + let (v,q) = unbind bi in + match is_set p with + Some u -> + let q = as_prop q in + mk_Appl(mk_Appl(all, u), mk_Abst(p,bind_var v q)) + | None -> + fatal pos "Goal %a not of the form (%a _ [-> ...])." term gt.goal_type sym cfg.symb_P + end + | _ -> fatal pos "Goal %a not of the form (%a _ [-> ...])." term gt.goal_type sym cfg.symb_P + in + let r = as_prop gt.goal_type in + (* wrn None "goal [%a]" term r; *) + r + (** Builtin tactic names. *) type tactic = | T_admit @@ -222,6 +270,7 @@ type tactic = | T_symmetry | T_try | T_why3 + | T_with_goal type config = (string,tactic) Hashtbl.t @@ -258,6 +307,7 @@ let get_config (ss:Sig_state.t) (pos:Pos.popt) : config = add "symmetry" T_symmetry; add "try" T_try; add "why3" T_why3; + add "with_goal" T_with_goal; t (** [p_term pos t] converts the term [t] into a p_term at position [pos]. *) @@ -363,8 +413,8 @@ let p_tactic (ss:Sig_state.t) (g:goal) (env:Env.t) (pos:Pos.popt) (t:term) | T_apply, [_;t] -> P_tac_apply (p_term t) | T_apply, _ -> assert false | T_assume, [prefix;_;Abst (_, t)] -> - let v = new_var (string_of_term pos prefix) in - let n = Pos.make pos (uniq_name v) in + let v = uniq_name (new_var (string_of_term pos prefix)) in + let n = Pos.make pos v and v = new_var v in P_tac_and (Pos.make pos (P_tac_assume [Some n]), tac_eval (subst t (mk_Vari v))) | T_assume, _ -> assert false @@ -420,6 +470,8 @@ let p_tactic (ss:Sig_state.t) (g:goal) (env:Env.t) (pos:Pos.popt) (t:term) | T_try, [t] -> P_tac_try(tac_eval t) | T_try, _ -> assert false | T_why3, _ -> P_tac_why3 None + | T_with_goal, [t] -> P_tac_with_goal (p_term t) + | T_with_goal, _ -> assert false with Not_found -> fatal pos "Unhandled tactic expression: %a." term t end @@ -717,6 +769,12 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool) Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt | _ -> assert false end + | P_tac_with_goal t -> + let goal = get_goal pos ss gt in + let t = scope t in + let t = mk_Appl (t, goal) in + if (Logger.log_enabled ()) then log "WITH_GOAL [%a]\n" term t; + handle ps (p_tactic ss g env pos t) | P_tac_try t -> begin try handle ps t with Fatal _ -> ps end | P_tac_orelse(t1,t2) -> diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 759eb0bfd..21140ba5a 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -341,6 +341,7 @@ let rec tactic : p_tactic pp = fun ppf { elt; _ } -> | P_tac_why3 p -> let prover ppf s = out ppf " \"%s\"" s in out ppf "why3%a" (Option.pp prover) p + | P_tac_with_goal t -> out ppf "with_goal %a" term t end let rec subproof : p_subproof pp = fun ppf sp -> diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 18bef499a..ad25f451a 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -291,6 +291,7 @@ type p_tactic_aux = | P_tac_sym | P_tac_try of p_tactic | P_tac_why3 of string option + | P_tac_with_goal of p_term and p_tactic = p_tactic_aux loc @@ -455,6 +456,7 @@ let eq_simp_flag : simp_flag eq = fun s1 s2 -> let eq_p_tactic : p_tactic eq = fun {elt=t1;_} {elt=t2;_} -> match t1, t2 with | P_tac_first_hyp t1, P_tac_first_hyp t2 + | P_tac_with_goal t1, P_tac_with_goal t2 | P_tac_apply t1, P_tac_apply t2 | P_tac_refine t1, P_tac_refine t2 -> eq_p_term t1 t2 | P_tac_have(i1,t1), P_tac_have(i2,t2) -> @@ -673,6 +675,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = | P_tac_refl | P_tac_sym | P_tac_why3 _ + | P_tac_with_goal _ | P_tac_solve | P_tac_fail | P_tac_focus _ diff --git a/tests/OK/Tactic.lp b/tests/OK/Tactic.lp index 03cbcab7c..bad50b7ca 100644 --- a/tests/OK/Tactic.lp +++ b/tests/OK/Tactic.lp @@ -46,7 +46,8 @@ builtin "induction" ≔ #induction; constant symbol #orelse : Tactic → Tactic → Tactic; builtin "orelse" ≔ #orelse; -constant symbol #refine [p] : π p → Tactic; +/*constant symbol #refine [p] : π p → Tactic;*/ +constant symbol #refine: String → Tactic; builtin "refine" ≔ #refine; constant symbol #reflexivity : Tactic; @@ -82,6 +83,9 @@ builtin "try" ≔ #try; constant symbol #why3 : Tactic; builtin "why3" ≔ #why3; +constant symbol #with_goal : (Prop → Tactic) → Tactic; +builtin "with_goal" ≔ #with_goal; + constant symbol #change : Tactic; builtin "change" ≔ #change; diff --git a/tests/export_dk.sh b/tests/export_dk.sh index 9bfdc18f9..0f9ade9b7 100755 --- a/tests/export_dk.sh +++ b/tests/export_dk.sh @@ -48,7 +48,7 @@ do # use builtin strings Tactic|1374);; # requires an excluded file - assume|first_hyp);; + assume|first_hyp|with_goal);; # default case *) translate $f.lp;; esac diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh index e42d45a28..6e26249bf 100755 --- a/tests/export_raw_dk.sh +++ b/tests/export_raw_dk.sh @@ -59,7 +59,7 @@ do # module alias alias);; # proofs - why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp);; + why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|with_goal);; # "open" triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|1374|Option|String|HOL|Impred|PropExt|Classic|Comp|Pos|Z|1217|1151|B1|B2|C1|C2|C3|Epsilon|1313|FunExt|Prod);; # "inductive" From 1fc6476823c8f815fea33ca79bb4fdad6ba32036 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Sat, 27 Jun 2026 14:29:09 +0200 Subject: [PATCH 2/5] with_goal example --- tests/OK/with_goal.lp | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/OK/with_goal.lp diff --git a/tests/OK/with_goal.lp b/tests/OK/with_goal.lp new file mode 100644 index 000000000..6cedb391d --- /dev/null +++ b/tests/OK/with_goal.lp @@ -0,0 +1,24 @@ +require open tests.OK.Tactic; + +injective symbol σ: Prop → Set; +rule π $P ↪ τ (σ $P); + +constant symbol ∀[T]: (τ T → Prop) → Prop; +notation ∀ quantifier; +rule π (@∀ $T $P) ↪ Π (x: τ $T), π ($P x); +constant symbol ⇒: Prop → Prop → Prop; +notation ⇒ infix right 7; +builtin "imp" ≔ ⇒; +builtin "all" ≔ ∀; +constant symbol T: Set; +constant symbol P: τ T → Prop; + +sequential symbol prove: Prop → Tactic; +rule prove (@∀ $T $P) ↪ #assume "x" (λ (x: τ $T), prove ($P x)) +with prove ($P ⇒ $Q) ↪ #assume "h" (λ (h: π $P), prove $Q) +with prove _ ↪ #print "" & #assumption; + +symbol test : Π x, π (P x) → π (P x) ≔ +begin + eval (#with_goal prove); +end; From 7e0e8d58773dab86f032e2cf1ef0b4cc6b85a6eb Mon Sep 17 00:00:00 2001 From: bodeveix Date: Sat, 27 Jun 2026 14:34:51 +0200 Subject: [PATCH 3/5] long lines --- src/handle/tactic.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 6ee5fc402..73f31b07f 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -194,7 +194,7 @@ let get_prod_ids env = else List.rev acc in aux [] -(** [get_goal pos ps gt] tries to build a goal [g] such as typing goal +(** [get_goal pos ps gt] tries to build a goal [g] such as typing goal [gt] = [Prf p]. It uses builtins P, T, imp and all. *) let get_goal: popt -> Sig_state.t -> goal_typ -> Term.term = fun pos ss gt -> @@ -234,9 +234,11 @@ let get_goal: popt -> Sig_state.t -> goal_typ -> Term.term = fun pos ss gt -> let q = as_prop q in mk_Appl(mk_Appl(all, u), mk_Abst(p,bind_var v q)) | None -> - fatal pos "Goal %a not of the form (%a _ [-> ...])." term gt.goal_type sym cfg.symb_P + fatal pos "Goal %a not of the form (%a _ [-> ...])." + term gt.goal_type sym cfg.symb_P end - | _ -> fatal pos "Goal %a not of the form (%a _ [-> ...])." term gt.goal_type sym cfg.symb_P + | _ -> fatal pos "Goal %a not of the form (%a _ [-> ...])." + term gt.goal_type sym cfg.symb_P in let r = as_prop gt.goal_type in (* wrn None "goal [%a]" term r; *) From 3d7f1929d9794420297f6074ab3804239f6f4f02 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 1 Jul 2026 15:03:36 +0200 Subject: [PATCH 4/5] remarks --- src/handle/tactic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index ad0e975ce..763cb8f34 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -216,8 +216,8 @@ let get_goal: popt -> Sig_state.t -> goal_typ -> Term.term = fun pos ss gt -> let rec as_prop g = match is_prf g with | Some u -> u - | None -> match g with - | Prod(p,bi) when binder_name bi = "_" -> + | None -> match unfold g with + | Prod(p,bi) when not (binder_occur bi) -> begin let (_,q) = unbind bi in match is_prf p with From 6adf7774b9f4f9e8f6e16572a9418a61f4575e34 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Mon, 6 Jul 2026 20:03:39 +0200 Subject: [PATCH 5/5] merge --- src/handle/tactic.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 7d138ece9..c8a7ec4bb 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -579,7 +579,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool) let v = unfold (mk_Vari v) in let t = mk_Appl (mk_Appl (t, p), v) in if Logger.log_enabled () then log "ALL_HYPS on %a\n" term v; - try let ps, t = p_tactic ps g env pos t in handle ps t + try handle ps (p_tactic ss g env pos t) with Fatal _ -> ps in let ps' = List.fold_left try_assumption ps gt.goal_hyps in @@ -639,7 +639,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool) | P_tac_first_hyp pt -> let t = scope pt in let f (_,(v,a,_)) = - let ps, t = p_tactic ps g env pos (mk_Appl(mk_Appl(t,a),mk_Vari v)) in + let t = p_tactic ss g env pos (mk_Appl(mk_Appl(t,a),mk_Vari v)) in progress ps t in begin match List.find_map f gt.goal_hyps with @@ -833,7 +833,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool) fatal pt.pos "Cannot infer the type of [%a]" term t | Some(t,_) -> if Unif.solve_noexn p then - let ps, t = p_tactic ps g env pos t in handle ps t + let t = p_tactic ss g env pos t in handle ps t else fatal pos "Cannot solve typing constraints for [%a]" term t in handle