#with_goal tactic

CHANGES.md

@@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `#print` to print a symbol or the current goal.
 - Export to Lean.
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
+- Tactic `#with_goal t` which calls term tactic t with current goal of type Prop as parameter.
 
 ### Changed
 
@@ -33,6 +34,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
 

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)
 

doc/tacticals.rst

@@ -46,6 +46,7 @@ The BNF grammar of tactics is in `lambdapi.bnf <https://raw.githubusercontent.co
    builtin "symmetry" ≔ …; // : T
    builtin "try" ≔ …; // : T → T
    builtin "why3" ≔ …; // : T
+   builtin "with_goal" ≔ …; // (Prop → T) → T
 
 The tactics taking a string as argument need the ``"String"`` :ref:`builtin` to be set. The string argument of ``refine`` is parsed as a term, and thus can contain underscores. If the builtin ``"and"`` is mapped to some symbol, say ``&``, then ``& t u`` is interpreted as follows: the tactic ``t`` is applied and, in case of success, the tactic ``u`` is applied. All other symbols are interpreted by the corresponding tactics.
 
@@ -98,3 +99,8 @@ An example of use is given in `Tactic.lp <https://github.com/Deducteam/lambdapi/
 -------
 
 ``try t`` applies ``t``. If ``t`` fails, then ``try t`` leaves the goal unchanged.
+
+``with_goal``
+-------------
+
+``with_goal t`` calls term tactic ``t`` on the current goal seen as a Prop. builtins must be defined to map Prf, El, => and forAll.

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"
+  }