Make reshape_expr more robust.

It now also reshapes expressions as values for contexts that need
values such as AppECtx.

heap_lang/tactics.v

@@ -30,25 +30,32 @@ Ltac inv_step :=
 (** 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. *)
+Ltac reshape_val e tac :=
+  let rec go e :=
+  match e with
+  | of_val ?v => v
+  | Rec ?f ?x ?e => constr:(RecV f x e)
+  | Lit ?l => constr:(LitV l)
+  | Pair ?e1 ?e2 =>
+    let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
+  | InjL ?e => let v := reshape_val e in constr:(InjLV v)
+  | InjR ?e => let v := reshape_val e in constr:(InjRV v)
+  | Loc ?l => constr:(LocV l)
+  end in let v := go e in first [tac v | fail 2].
+
 Ltac reshape_expr e tac :=
   let rec go K e :=
   match e with
   | _ => tac (reverse K) e
-  | App ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
-     end
-  | UnOp ?op ?e =>
-     go (UnOpCtx op :: K) e
+  | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
+  | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
+  | UnOp ?op ?e => go (UnOpCtx op :: K) e
   | BinOp ?op ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (BinOpRCtx op v1 :: K) e2 | _ => go (BinOpLCtx op e2 :: K) e1
-     end
+     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
+  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
   | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
-  | Pair ?e1 ?e2 =>
-     lazymatch e1 with
-     | of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
-     end
+  | Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
+  | Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
   | Fst ?e => go (FstCtx :: K) e
   | Snd ?e => go (SndCtx :: K) e
   | InjL ?e => go (InjLCtx :: K) e
@@ -56,16 +63,12 @@ Ltac reshape_expr e tac :=
   | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
   | Alloc ?e => go (AllocCtx :: K) e
   | Load ?e => go (LoadCtx :: K) e
-  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1 || go (StoreRCtx e1 :: K) e2
-  | Cas ?e0 ?e1 ?e2 =>
-     lazymatch e0 with
-     | of_val ?v0 =>
-        lazymatch e1 with
-        | of_val ?v1 => go (CasRCtx v0 v1 :: K) e2
-        | _ => go (CasMCtx v0 e2 :: K) e1
-        end
-     | _ => go (CasLCtx e1 e2 :: K) e0
-     end
+  | Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
+  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
+  | Cas ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
+     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
+     | go (CasMCtx v0 e2 :: K) e1 ])
+  | Cas ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
   end in go (@nil ectx_item) e.
 
 (** The tactic [do_step tac] solves goals of the shape [reducible], [prim_step]