From c8f818c7fd711a54d5bf17e3ecd24f66725d01d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment?= <clef-men@orange.fr>
Date: Sun, 24 Nov 2024 15:38:05 +0100
Subject: [PATCH] Add custom intro patterns.
---
iris/proofmode/intro_patterns.v | 12 ++++-
iris/proofmode/ltac_tactics.v | 88 +++++++++++++++++++++------------
iris/proofmode/tokens.v | 4 +-
3 files changed, 70 insertions(+), 34 deletions(-)
diff --git a/iris/proofmode/intro_patterns.v b/iris/proofmode/intro_patterns.v
index 4e734ec3c..ba7e19a84 100644
--- a/iris/proofmode/intro_patterns.v
+++ b/iris/proofmode/intro_patterns.v
@@ -1,4 +1,5 @@
From stdpp Require Export strings.
+From stdpp Require Import pretty.
From iris.proofmode Require Import base tokens sel_patterns.
From iris.prelude Require Import options.
@@ -24,7 +25,8 @@ Inductive intro_pat :=
| IForall : intro_pat
| IAll : intro_pat
| IClear : sel_pat → intro_pat
- | IClearFrame : sel_pat → intro_pat.
+ | IClearFrame : sel_pat → intro_pat
+ | ICustom : string → list string → intro_pat.
Module intro_pat.
Inductive stack_item :=
@@ -85,6 +87,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TBracketL :: ts => parse_go ts (StList :: k)
| TBar :: ts => parse_go ts (StBar :: k)
| TBracketR :: ts => close_list k [] [] ≫= parse_go ts
+ | TParenL :: TColon :: TName custom :: ts => parse_custom custom [] ts k
| TParenL :: ts => parse_go ts (StConjList :: k)
| TAmp :: ts => parse_go ts (StAmp :: k)
| TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
@@ -115,6 +118,13 @@ with parse_clear (ts : list token) (k : stack) : option stack :=
| TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
| TBraceR :: ts => parse_go ts k
| _ => None
+ end
+with parse_custom custom args ts k :=
+ match ts with
+ | TName arg :: ts => parse_custom custom (arg :: args) ts k
+ | TNat i :: ts => parse_custom custom (pretty i :: args) ts k
+ | TParenR :: ts => parse_go ts (StPat (ICustom custom (rev args)) :: k)
+ | _ => None
end.
Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 1018168a7..0352452f0 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -7,6 +7,11 @@ From iris.proofmode Require Export classes notation.
From iris.prelude Require Import options.
Export ident.
+Class CustomIpat (custom : string) :=
+ custom_ipat : list string → option string.
+#[global] Arguments custom_ipat custom {CustomIpat} args : rename.
+#[global] Hint Mode CustomIpat + : typeclass_instances.
+
(** Tactic used for solving side-conditions arising from TC resolution in [iMod]
and [iInv]. *)
Ltac iSolveSideCondition :=
@@ -298,7 +303,7 @@ Tactic Notation "iAssumption" :=
|exact Hass
|pm_reduce; tc_solve ||
fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
- |assert_fails (is_evar P);
+ |assert_fails (is_evar P);
assert (P = False%I) as Hass by reflexivity;
apply (tac_false_destruct _ j p P);
[pm_reflexivity
@@ -1570,38 +1575,57 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat1)
(** * Introduction tactic *)
Ltac _iIntros_go pats startproof :=
- lazymatch pats with
- | [] =>
- lazymatch startproof with
- | true => iStartProof
- | false => idtac
+ let rec go pats startproof :=
+ lazymatch pats with
+ | [] =>
+ lazymatch startproof with
+ | true => iStartProof
+ | false => idtac
+ end
+ (* Optimizations to avoid generating fresh names *)
+ | IPure (IGallinaNamed ?s) :: ?pats =>
+ let i := fresh in
+ iIntro (i);
+ rename_by_string i s;
+ _iIntros_go pats startproof
+ | IPure IGallinaAnon :: ?pats => iIntro (?); _iIntros_go pats startproof
+ | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; _iIntros_go pats false
+ | IDrop :: ?pats => iIntro _; _iIntros_go pats startproof
+ | IIdent ?H :: ?pats => iIntro H; _iIntros_go pats startproof
+ (* Introduction patterns that can only occur at the top-level *)
+ | IPureIntro :: ?pats => iPureIntro; _iIntros_go pats false
+ | IModalIntro :: ?pats => iModIntro; _iIntros_go pats false
+ | IForall :: ?pats => repeat iIntroForall; _iIntros_go pats startproof
+ | IAll :: ?pats => repeat (iIntroForall || iIntro); _iIntros_go pats startproof
+ (* Clearing and simplifying introduction patterns *)
+ | ISimpl :: ?pats => simpl; _iIntros_go pats startproof
+ | IClear ?H :: ?pats => iClear H; _iIntros_go pats false
+ | IClearFrame ?H :: ?pats => iFrame H; _iIntros_go pats false
+ | IDone :: ?pats => try done; _iIntros_go pats startproof
+ (* Introduction + destruct *)
+ | IIntuitionistic ?pat :: ?pats =>
+ let H := iFresh in iIntro #H; iDestructHyp H as pat; _iIntros_go pats false
+ | ICustom ?custom ?args :: ?pats =>
+ first
+ [ lazymatch eval cbv in (custom_ipat custom args) with
+ | None =>
+ fail 1 "iIntros: invalid arguments for custom intro pattern:" custom
+ | Some ?pat =>
+ lazymatch eval cbv in (intro_pat.parse pat) with
+ | None =>
+ fail 1 "iIntros: invalid intro pattern generated by custom intro pattern:" custom
+ | Some ?pats' =>
+ let pats := eval cbv in (pats' ++ pats) in
+ go pats startproof
+ end
+ end
+ | fail 1 "iIntros: unrecognized custom intro pattern:" custom
+ ]
+ | ?pat :: ?pats =>
+ let H := iFresh in iIntro H; iDestructHyp H as pat; _iIntros_go pats false
end
- (* Optimizations to avoid generating fresh names *)
- | IPure (IGallinaNamed ?s) :: ?pats =>
- let i := fresh in
- iIntro (i);
- rename_by_string i s;
- _iIntros_go pats startproof
- | IPure IGallinaAnon :: ?pats => iIntro (?); _iIntros_go pats startproof
- | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; _iIntros_go pats false
- | IDrop :: ?pats => iIntro _; _iIntros_go pats startproof
- | IIdent ?H :: ?pats => iIntro H; _iIntros_go pats startproof
- (* Introduction patterns that can only occur at the top-level *)
- | IPureIntro :: ?pats => iPureIntro; _iIntros_go pats false
- | IModalIntro :: ?pats => iModIntro; _iIntros_go pats false
- | IForall :: ?pats => repeat iIntroForall; _iIntros_go pats startproof
- | IAll :: ?pats => repeat (iIntroForall || iIntro); _iIntros_go pats startproof
- (* Clearing and simplifying introduction patterns *)
- | ISimpl :: ?pats => simpl; _iIntros_go pats startproof
- | IClear ?H :: ?pats => iClear H; _iIntros_go pats false
- | IClearFrame ?H :: ?pats => iFrame H; _iIntros_go pats false
- | IDone :: ?pats => try done; _iIntros_go pats startproof
- (* Introduction + destruct *)
- | IIntuitionistic ?pat :: ?pats =>
- let H := iFresh in iIntro #H; iDestructHyp H as pat; _iIntros_go pats false
- | ?pat :: ?pats =>
- let H := iFresh in iIntro H; iDestructHyp H as pat; _iIntros_go pats false
- end.
+ in
+ go pats startproof.
Ltac _iIntros0 pat :=
let pats := intro_pat.parse pat in
diff --git a/iris/proofmode/tokens.v b/iris/proofmode/tokens.v
index 8885c26d9..e761bcb80 100644
--- a/iris/proofmode/tokens.v
+++ b/iris/proofmode/tokens.v
@@ -26,7 +26,8 @@ Inductive token :=
| TAll : token
| TMinus : token
| TSep : token
- | TArrow : direction → token.
+ | TArrow : direction → token
+ | TColon : token.
Inductive state :=
| SName : string → state
@@ -70,6 +71,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
| String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
| String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
+ | String ":" s => tokenize_go s (TColon :: cons_state kn k) SNone
| String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
(String (Ascii.Ascii false false false true false false false true)
(String (Ascii.Ascii true true true false true false false true) s)) =>
--
GitLab