Commit b9352f9e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add simple library for priority levels.

parent cd511950
......@@ -117,6 +117,7 @@ iris/program_logic/total_lifting.v
iris/program_logic/total_ectx_lifting.v
iris/program_logic/atomic.v
iris/proofmode/base.v
iris/proofmode/level.v
iris/proofmode/ident_name.v
iris/proofmode/string_ident.v
iris/proofmode/tokens.v
......
From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
(** This library provides tactics to set a current priority level and to test
if a required priority level is above the current level. Priorities are
represented by natural numbers ([nat]) and indexed by a kind.
- [set_level K n]: Sets the current level of kind [K] to [n].
- [clear_level K]: Clears the current level of [K].
- [at_level K n tac]: Sets the current level of [K] to [n], executes [tac ()],
and restores the level of [K] to the old value. Note that [tac] is a closure
to ensure it is not evaluated eagerly.
- [allowed_level K n]: Succeeds if [n] is below (or equal) to the current level
of [K], fails otherwise.
The class [AllowedLevel K n] is a wrapper around [allowed_level K n] that can be
used to define premises of type classes.
Level kinds are represented by [Type]s, and they are typically defined through
a record without any fields. For example [Record TestLevel := {}].
The library is implemented by adding a dummy element [current_level K n] to the
context to keep track of the current level.
*)
Record current_level (K : Type) (n : nat) := {}.
Ltac clear_level K :=
repeat lazymatch goal with
| H : current_level K _ |- _ => clear H
end.
Ltac set_level K n :=
clear_level K;
assert (current_level K n) by constructor.
Tactic Notation "at_level" constr(K) constr(n) tactic3(tac) :=
lazymatch goal with
| H : current_level K ?n' |- _ => set_level K n; tac (); set_level K n'
| _ => set_level K n; tac (); clear_level K
end.
Ltac allowed_level K n :=
lazymatch goal with
| H : current_level K ?n' |- _ =>
lazymatch eval vm_compute in (bool_decide (n n')%nat) with
| true => idtac
| false => fail "level" n "not above" n'
end
| _ => fail "no level set"
end.
Class AllowedLevel (K : Type) (n : nat) := { }.
Global Hint Extern 0 (AllowedLevel ?K ?n) =>
allowed_level K n; constructor : typeclass_instances.
(** TODO: Move test elsewhere *)
Record TestLevel := {}.
Goal True.
Fail allowed_level TestLevel 0. (* no level set *)
set_level TestLevel 3.
allowed_level TestLevel 0.
allowed_level TestLevel 1.
allowed_level TestLevel 2.
allowed_level TestLevel 3.
Fail allowed_level TestLevel 4. (* level 4 not above 3 *)
at_level TestLevel 4 (fun _ => allowed_level TestLevel 4).
Fail at_level TestLevel 4 (fun _ => allowed_level TestLevel 5). (* level 5 not above 4. *)
Fail allowed_level TestLevel 4. (* level 4 not above 3 *)
Abort.
Supports Markdown
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