#with_goal tactic - #1430
#with_goal tactic#1430bodeveix wants to merge 17 commits into
Conversation
There was a problem hiding this comment.
Hi Jean-Paul.
-
If there are problems with assume, please open an issue with an example, and propose a separate PR to solve that problem.
-
A more general approach to with_goal, not requiring gconf.ml, would be to generate a unification problem goal == Prf ?M, solve it to instantiate ?M and, in case of success, handle the tactic (t ?M).
Yes but I suppose this would need another tactic to solve the unification problem automatically.
|
I see the problem with assume. I'll fix it this afternoon. |
|
The goal is now matched with (Prf _) through LP standard unification. The example uses the new encoding of Set and Prop declared in Univ. The corresponding unification rules replace what was done in OCaml. |
fblanqui
left a comment
fblanqui
left a comment
There was a problem hiding this comment.
Hi JP. Here are some comments.
| register_typ "try" (arr tac tac); | ||
| register_typ "why3" tac | ||
| register_typ "why3" tac; | ||
| register_typ "with_goal" (arr (arr prop tac) tac); |
There was a problem hiding this comment.
Why restricting goals to Prop? It could be of type Π l:L, U l → Tactic.
There was a problem hiding this comment.
OK, I have changed to this profile: Π [l], (U l → Tactic) → Tactic. In general the parameter is not polymorphic.
| s | ||
| end | ||
| else assert false | ||
| else begin failwith s.sym_name end |
There was a problem hiding this comment.
please use the qualified name:
Console.out 0 "link: didn't find %a" Raw.sym s
and add let qsym = qsym let _ = qsym in Core.Print.Raw
| | 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 |
| - 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 |
| - 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. |
There was a problem hiding this comment.
applies the tactic producing term t to the current goal
There was a problem hiding this comment.
I have changed the comment: Tactic #with_goal t applies the tactic t with current goal as parameter.
|
|
||
| * ``command.ml``: command handling | ||
| * ``compile.ml``: file parsing and compiling (.lpo files) | ||
| * ``gconf.ml``: builtins needed to build current goal (tactic #with_goal) |
2 participants
The tactic term with_goal (only available in eval) calls its parameter tactic with the current goal seen as a Prop.