Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

tactics.v 1.74 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
From iris_time.heap_lang Require Export lang.
Set Default Proof Using "Type".
Import heap_lang.

(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds.

The order parameter specifies the order in which these decompositions are tried.
If true, contexts are tried starting from the most nested, when false, the
first tried context is the least nested.

 *)
Ltac reshape_expr order e tac :=
  let rec go K e :=
  match e with
  | _ =>
      lazymatch order with
      | false => tac K e
      | true  => fail
      end
  | App ?e (Val ?v) => go (AppLCtx v :: K) e
  | App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
  | UnOp ?op ?e => go (UnOpCtx op :: K) e
  | BinOp ?op ?e (Val ?v) => go (BinOpLCtx op v :: K) e
  | BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
  | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
  | Pair ?e (Val ?v) => go (PairLCtx v :: K) e
  | Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
  | Fst ?e => go (FstCtx :: K) e
  | Snd ?e => go (SndCtx :: K) e
  | InjL ?e => go (InjLCtx :: K) e
  | InjR ?e => go (InjRCtx :: K) e
  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
  | Alloc ?e => go (AllocCtx :: K) e
  | Load ?e => go (LoadCtx :: K) e
  | Store ?e (Val ?v) => go (StoreLCtx v :: K) e
  | Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
  | CAS ?e0 (Val ?v1) (Val ?v2) => go (CasLCtx v1 v2 :: K) e0
  | CAS ?e0 ?e1 (Val ?v2) => go (CasMCtx e0 v2 :: K) e1
  | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
  | FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
  | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
  | _ =>
      lazymatch order with
      | false => fail
      | true  => tac K e
      end
  end in go (@nil ectx_item) e.