more aggressive let binding

theories/lithium/interpreter.v

@@ -462,7 +462,7 @@ Ltac liCheckOwnInContext P :=
 Global Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; constructor; exact: I) : typeclass_instances.
 
 (** * Main lithium tactics *)
-Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
+Ltac convert_to_i2p_tac P bind cont := fail "No convert_to_i2p_tac provided!".
 Ltac convert_to_i2p P bind cont :=
   lazymatch P with
   | subsume ?P1 ?P2 ?T =>
@@ -471,7 +471,7 @@ Ltac convert_to_i2p P bind cont :=
   | subsume_list ?A ?ig ?l1 ?l2 ?f ?T =>
       bind T ltac:(fun H => uconstr:(subsume_list A ig l1 l2 f H));
       cont uconstr:(((_ : SubsumeList _ _ _ _ _) _))
-  | _ => let converted := convert_to_i2p_tac P in cont converted
+  | _ => convert_to_i2p_tac P bind cont
   end.
 Ltac extensible_judgment_hook := idtac.
 Ltac liExtensibleJudgement :=

theories/typing/automation.v

@@ -54,24 +54,53 @@ Ltac can_solve_tac ::= solve_goal.
 
 Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.
 
-Ltac convert_to_i2p_tac P ::=
+Ltac convert_to_i2p_tac P bind cont ::=
   lazymatch P with
-  | typed_value ?v ?T => uconstr:(((_ : TypedValue _) _))
-  | typed_bin_op ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?T => uconstr:(((_ : TypedBinOp _ _ _ _ _ _ _) _))
-  | typed_un_op ?v ?ty ?o ?ot ?T => uconstr:(((_ : TypedUnOp _ _ _ _) _))
-  | typed_call ?v ?P ?vl ?tys ?T => uconstr:(((_ : TypedCall _ _ _ _) _))
-  | typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?ot ?T => uconstr:(((_ : TypedCopyAllocId _ _ _ _ _) _))
-  | typed_place ?P ?l1 ?β1 ?ty1 ?T => uconstr:(((_ : TypedPlace _ _ _ _) _))
-  | typed_if ?ot ?v ?P ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _))
-  | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _))
-  | typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _))
-  | typed_read_end ?a ?E ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _))
-  | typed_write_end ?a ?E ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _ _) _))
-  | typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _))
-  | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _))
-  | typed_annot_expr ?n ?a ?v ?P ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) )
-  | typed_annot_stmt ?a ?l ?P ?T => uconstr:(((_ : TypedAnnotStmt _ _ _) _))
-  | typed_macro_expr ?m ?es ?T => uconstr:(((_ : TypedMacroExpr _ _) _))
+  | typed_value ?v ?T =>
+      bind T ltac:(fun H => uconstr:(typed_value v H));
+      cont uconstr:(((_ : TypedValue _) _))
+  | typed_bin_op ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?T =>
+      bind T ltac:(fun H => uconstr:(typed_bin_op v1 ty1 v2 ty2 o ot1 ot2 H));
+      cont uconstr:(((_ : TypedBinOp _ _ _ _ _ _ _) _))
+  | typed_un_op ?v ?ty ?o ?ot ?T =>
+      bind T ltac:(fun H => uconstr:(typed_un_op ?v ?ty ?o ?ot H));
+      cont uconstr:(((_ : TypedUnOp _ _ _ _) _))
+  | typed_call ?v ?P ?vl ?tys ?T =>
+      bind T ltac:(fun H => uconstr:(typed_call v P vl tys H));
+      cont uconstr:(((_ : TypedCall _ _ _ _) _))
+  | typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?ot ?T =>
+      bind T ltac:(fun H => uconstr:(typed_copy_alloc_id v1 ty1 v2 ty2 ot H));
+      cont uconstr:(((_ : TypedCopyAllocId _ _ _ _ _) _))
+  | typed_place ?P ?l1 ?β1 ?ty1 ?T =>
+      bind T ltac:(fun H => uconstr:(typed_place P l1 β1 ty1 H));
+      cont uconstr:(((_ : TypedPlace _ _ _ _) _))
+  | typed_if ?ot ?v ?P ?T1 ?T2 =>
+      cont uconstr:(((_ : TypedIf _ _ _) _ _))
+  | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q =>
+      cont uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _))
+  | typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q =>
+      cont uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _))
+  | typed_read_end ?a ?E ?l ?β ?ty ?ly ?T =>
+      bind T ltac:(fun H => uconstr:(typed_read_end a E l β ty ly H ));
+      cont uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _))
+  | typed_write_end ?a ?E ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T =>
+      bind T ltac:(fun H => uconstr:(typed_write_end a E ot v1 ty1 l2 β2 ty2 H ));
+      cont uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _ _) _))
+  | typed_addr_of_end ?l ?β ?ty ?T =>
+      bind T ltac:(fun H => uconstr:(typed_addr_of_end l β ty H));
+      cont uconstr:(((_ : TypedAddrOfEnd _ _ _) _))
+  | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T =>
+      bind T ltac:(fun H => uconstr:(typed_cas ot v1 P1 v2 P2 v3 P3 H ));
+      cont uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _))
+  | typed_annot_expr ?n ?a ?v ?P ?T =>
+      bind T ltac:(fun H => uconstr:(typed_annot_expr n a v P H ));
+      cont uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) )
+  | typed_annot_stmt ?a ?l ?P ?T =>
+      bind T ltac:(fun H => uconstr:(typed_annot_stmt a l P H ));
+      cont uconstr:(((_ : TypedAnnotStmt _ _ _) _))
+  | typed_macro_expr ?m ?es ?T =>
+      bind T ltac:(fun H => uconstr:(typed_macro_expr m es H ));
+      cont uconstr:(((_ : TypedMacroExpr _ _) _))
   end.
 
 (** * Main automation tactics *)
@@ -105,10 +134,10 @@ Ltac liRIntroduceLetInGoal :=
       li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_val_expr Σ tG e H)))
     | @typed_write ?Σ ?tG ?b ?e ?ot ?v ?ty ?Mov ?T =>
       li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_write Σ tG b e ot v ty Mov H)))
-    | @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T =>
-      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H)))
-    | @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T =>
-      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H)))
+    (* | @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T => *)
+    (*   li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H))) *)
+    (* | @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T => *)
+    (*   li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H))) *)
     end
   end.