#with_goal tactic

CHANGES.md

@@ -24,6 +24,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
 - Extend `print` query to the following arguments: `verbose`, `debug`, `flag`, `builtin`, `prover`, `prover_timeout`.
 - add a version number to the header of the index db file to prevent crash of LP when the structure of db changes.
+- Tactic `#with_goal t` which calls term tactic t with current goal of type Prop as parameter.
 
 ### Changed
 
@@ -37,6 +38,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Type of `#assume` in order to generate a new symbol and use it inside a tactic term.
 - Errors occurring while a proof is in progress now report the proof state: the goals a failing tactic was applied to, the goals before and after the tactic for a subproof-count mismatch, and the remaining goals when a proof is unfinished at `end`. The state is printed after the error message, which stays unchanged. The LSP server does not attach the proof state to tactic failures since editors display it themselves.
 - Lambdapi does not use Cmdliner anymore.
+>>>>>>> dk/master
 
 ### 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

@@ -51,6 +51,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.
 
@@ -103,3 +104,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/core/builtin.ml

@@ -240,6 +240,7 @@ let _ =
   register_typ "solve" tac;
   register_typ "symmetry" tac;
   register_typ "try" (arr tac tac);
-  register_typ "why3" tac
+  register_typ "why3" tac;
+  register_typ "with_goal" (arr (arr prop tac) tac);
 
 end

src/core/sign.ml

@@ -112,7 +112,7 @@ let link : t -> unit = fun sign ->
               StrMap.add s.sym_name s !(Ghost.sign.sign_symbols);
             s
           end
-        else assert false
+        else begin failwith s.sym_name end
   in
   let link_term mk_Appl =
     let rec link_term t =

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

src/handle/tactic.ml

@@ -197,6 +197,56 @@ 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 unfold g with
+              | Prod(p,bi) when not (binder_occur 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
@@ -226,6 +276,7 @@ type tactic =
   | T_symmetry
   | T_try
   | T_why3
+  | T_with_goal
 
 type config = (string,tactic) Hashtbl.t
 
@@ -263,6 +314,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]. *)
@@ -379,7 +431,6 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
       then Some new_ps
       else None
     with Fatal _ -> None
-
   (* [p_tactic ss g env pos t] weak head normalizes [t] and converts the
      result into a p_tactic. *)
   and p_tactic (ps:proof_state) (g:goal) (env:Env.t) (pos:Pos.popt)
@@ -476,11 +527,12 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
             | T_try, [t] -> ps, mk(P_tac_try(tac_eval t))
             | T_try, _ -> assert false
             | T_why3, _ -> ps, mk(P_tac_why3 None)
+            | T_with_goal, [t] -> ps, mk (P_tac_with_goal(p_term t))
+            | T_with_goal, _ -> assert false
           with Not_found ->
             fatal pos "Unhandled tactic expression: %a." term t
         end
       | _ -> fatal pos "Unhandled tactic expression: %a." term t
-
   and handle ps ({elt;pos} as tac) =
   if Logger.log_enabled() then log "%a" Pretty.tactic tac;
   match ps.proof_goals with
@@ -571,6 +623,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool)
             let ids = Ctxt.names c in let term = term_in ids in
             fatal pos "(%a) is not typable." term t
         | Some (_, a) -> LibTerm.count_products Eval.whnf c a
+                         - LibTerm.count_products Eval.whnf c (gt.goal_type)
       in
       let t = scope (P.appl_wild pt n) in
       tac_refine pos ps gt gs (new_problem()) t
@@ -781,6 +834,13 @@ 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;
+      let ps,t = p_tactic ps g env pos t in
+      handle ps t
   | P_tac_try t ->
       begin try handle ps t with Fatal _ -> ps end
   | P_tac_orelse(t1,t2) ->
@@ -805,7 +865,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 ps,t = p_tactic ps g env pos t in handle ps t
         else fatal pos "Cannot solve typing constraints for [%a]" term t
 
   in handle

src/parsing/pretty.ml

@@ -357,6 +357,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
 
 let rec subproof : p_subproof pp = fun ppf sp ->
   out ppf "{@[<hv2>@ %a@ @]}" proofsteps sp

src/parsing/syntax.ml

@@ -305,6 +305,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
 
@@ -359,6 +360,7 @@ let tactic_keyword : p_tactic -> string option = fun {elt;_} ->
   | P_tac_sym -> Some "symmetry"
   | P_tac_try _ -> Some "try"
   | P_tac_why3 _ -> Some "why3"
+  | P_tac_with_goal _ -> Some "with_goal"
 
 (** [tactic_keyword_pos t] returns the position of the keyword introducing
     tactic [t], or the position of the whole of [t] when no single keyword
@@ -554,6 +556,7 @@ let eq_p_tactic : p_tactic eq = fun {elt=t1;_} {elt=t2;_} ->
   match t1, t2 with
   | P_tac_all_hyps t1, P_tac_all_hyps t2
   | 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) ->
@@ -774,6 +777,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 _

tests/OK/Tactic.lp

@@ -89,6 +89,9 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
+constant symbol #with_goal : (Prop → Tactic) → Tactic;
+builtin "with_goal" ≔ #with_goal;
+
 // defined tactics
 
 symbol nothing ≔ #try #fail;

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;

tests/export_dk.sh

@@ -43,9 +43,8 @@ do
         # require escaped module name
         π/utf_path|escape_path|'a b/escape file'|require_nondkmident|262_pair_ex_2|require_symbol);;
         # use builtin strings
-        Tactic);;
         # requires Tactic
-        1374|assume|first_hyp|all_hyps|1493);;
+        1374|Tactic|assume|first_hyp|all_hyps|1493);;
         # default case
         *) translate $f.lp;;
     esac

tests/export_raw_dk.sh

@@ -57,7 +57,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|all_hyps|1435_part2|1435);;
+        why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps|with_goal|1435_part2|1435);;
         # "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|Conj|Disj|ExtraRules|Univ|1493);;
         # "inductive"