Commit 794299db authored by Dan Frumin's avatar Dan Frumin

update the refman

parent b4fda077
......@@ -6,15 +6,30 @@ Threadpool tactics
- `tp_normalise j`: simplify the term/expression in `j ⤇ e`
- `tp_bind j e'`: if `j ⤇ e` and `e` can be decomposed as `K[e']`,
then turn the resource into `j ⤇ K[e']`. For example if, `j ⤇ f (!x + 2)`,
then invoking `tp_bind j (Load x)` converts the resource
to `j ⤇ fill [AppRCtx f, PlusLCtx 2] (!x)`.
then turn the resource into `j ⤇ K[e']`. For example if, `j ⤇ f
(!x + 2)`, then invoking `tp_bind j (Load x)` converts the resource
to `j ⤇ fill [AppRCtx f, PlusLCtx 2] (!x)`. All the tactics below,
apart from `tp_apply` use this bind facility to find a subterm in
the threadpool of an appropriate shape.
- `tp_store j`
- `tp_load j`
- `tp_rec j`
- `tp_op j`
- `tp_op j`/`tp_nat_binop j`
- `tp_cas_fail j` and `tp_cas_suc j`
- `tp_tlam j`
- `tp_fold j`
- `tp_pack j`
- `tp_fst j`, `tp_snd j`
- `tp_case_inl j`,`tp_case_inr j`
- `tp_if_true j`,`tp_if_false j`
- `tp_fork i as j "Hj"`
+ `tp_fork i as j` is the same thing as `let H := iFresh in tp_fork i as j H`
+ `tp_fork i` has a similar behaviour, but...
- `tp_alloc j as l "Hl"`
- `tp_apply j lem with "H1 ... Hn" as "S"`
Weakest precondition calculus tactics
-------------------------------------
- `wp_bind e'`: if the goal is `WP e @ E {{ Ψ }}` and `e` can be
decomposed as `K[e']`, then turn the goal into `WP e' @ E {{ v, WP K[v] @ E {{ Q }} }}`
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment