Tactic: new inline macro

omelkonian · omelkonian · commit 06c6605228f2 · 2025-03-06T12:22:07.000Z
diff --git a/Class/Convertible.agda b/Class/Convertible.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe --without-K #-}
 module Class.Convertible where
 
 open import Class.Convertible.Core public
diff --git a/Class/Convertible/Core.agda b/Class/Convertible/Core.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe --without-K #-}
 module Class.Convertible.Core where
 
 open import Meta.Prelude
diff --git a/Class/Convertible/Foreign.agda b/Class/Convertible/Foreign.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --without-K #-}
+module Class.Convertible.Foreign where
+
+open import Meta.Prelude
+
+open import Class.Functor
+open import Class.Bifunctor
+
+open import Class.Convertible.Core
+open import Class.HasHsType.Core
+
+open import Foreign.Haskell using (Pair; Either)
+open import Foreign.Haskell.Coerce using (coerce)
+
+instance
+  Convertible-Pair : Convertible₂ _×_ Pair
+  Convertible-Pair = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
diff --git a/Class/Convertible/Instances.agda b/Class/Convertible/Instances.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe --without-K #-}
 module Class.Convertible.Instances where
 
 open import Meta.Prelude
@@ -6,15 +7,11 @@ open import Class.Functor
 open import Class.Bifunctor
 
 open import Class.Convertible.Core
-
 open import Class.HasHsType.Core
 
 HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
 HsConvertible A = Convertible A (HsType A)
 
-open import Foreign.Haskell using (Pair; Either)
-open import Foreign.Haskell.Coerce using (coerce)
-
 instance
   Convertible-ℕ : Convertible ℕ ℕ
   Convertible-ℕ = λ where
@@ -27,19 +24,9 @@ instance
   Convertible-× : Convertible₂ _×_ _×_
   Convertible-× = Bifunctor⇒Convertible
 
-  Convertible-Pair : Convertible₂ _×_ Pair
-  Convertible-Pair = λ where
-    .to   → coerce ∘ bimap to to
-    .from → bimap from from ∘ coerce
-
   Convertible-⊎ : Convertible₂ _⊎_ _⊎_
   Convertible-⊎ = Bifunctor⇒Convertible
 
-  Convertible-Either : Convertible₂ _⊎_ Either
-  Convertible-Either = λ where
-    .to   → coerce ∘ bimap to to
-    .from → bimap from from ∘ coerce
-
   Convertible-List : Convertible₁ List List
   Convertible-List = λ where
     .to   → fmap to
diff --git a/Class/HasHsType.agda b/Class/HasHsType.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe --without-K #-}
 module Class.HasHsType where
 
 open import Class.HasHsType.Core public
diff --git a/Class/HasHsType/Core.agda b/Class/HasHsType/Core.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe --without-K #-}
 module Class.HasHsType.Core where
 
 open import Meta.Prelude
diff --git a/Class/HasHsType/Foreign.agda b/Class/HasHsType/Foreign.agda
@@ -0,0 +1,17 @@
+{-# OPTIONS --without-K #-}
+module Class.HasHsType.Foreign where
+
+open import Meta.Prelude
+
+open import Class.HasHsType.Core
+
+open import Foreign.Haskell.Pair using (Pair)
+open import Foreign.Haskell.Either using (Either)
+
+module _ ⦃ _ : HasHsType A ⦄ ⦃ _ : HasHsType B ⦄ where instance
+
+  iHsTy-Sum : HasHsType (A ⊎ B)
+  iHsTy-Sum .HasHsType.HsType = Either (HsType A) (HsType B)
+
+  iHsTy-Pair : HasHsType (A × B)
+  iHsTy-Pair .HasHsType.HsType = Pair (HsType A) (HsType B)
diff --git a/Class/HasHsType/Instances.agda b/Class/HasHsType/Instances.agda
@@ -1,10 +1,8 @@
+{-# OPTIONS --safe --without-K #-}
 module Class.HasHsType.Instances where
 
 open import Meta.Prelude
 
-open import Foreign.Haskell.Pair using (Pair)
-open import Foreign.Haskell.Either using (Either)
-
 open import Class.HasHsType.Core
 
 instance
@@ -21,12 +19,5 @@ module _ ⦃ _ : HasHsType A ⦄ where instance
   iHsTy-Maybe : HasHsType (Maybe A)
   iHsTy-Maybe .HasHsType.HsType = Maybe (HsType A)
 
-  module _ ⦃ _ : HasHsType B ⦄ where instance
-    iHsTy-Fun : HasHsType (A → B)
-    iHsTy-Fun .HasHsType.HsType = HsType A → HsType B
-
-    iHsTy-Sum : HasHsType (A ⊎ B)
-    iHsTy-Sum .HasHsType.HsType = Either (HsType A) (HsType B)
-
-    iHsTy-Pair : HasHsType (A × B)
-    iHsTy-Pair .HasHsType.HsType = Pair (HsType A) (HsType B)
+  iHsTy-Fun : ⦃ HasHsType B ⦄ → HasHsType (A → B)
+  iHsTy-Fun {B = B} .HasHsType.HsType = HsType A → HsType B
diff --git a/Meta/Prelude.agda b/Meta/Prelude.agda
@@ -5,7 +5,9 @@ module Meta.Prelude where
 -- ** stdlib re-exports
 open import Level public
   renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ)
-open import Function public
+variable
+  ℓ ℓ′ ℓ″ : Level
+  A B C D : Set ℓ
 
 open import Data.Bool public
   hiding (_≟_; _≤_; _≤?_; _<_; _<?_)
@@ -25,22 +27,26 @@ open import Data.Nat public
 open import Data.String public
   using (String; _<+>_)
 
+open import Function public
+open import Relation.Nullary public
+  using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality public
   hiding (preorder; setoid; [_]; module ≡-Reasoning; decSetoid)
 
 -- ** helper funs
-lookupᵇ : {A B : Set} → (A → A → Bool) → List (A × B) → A → Maybe B
+lookupᵇ : (A → A → Bool) → List (A × B) → A → Maybe B
 lookupᵇ f [] n = nothing
 lookupᵇ f ((k , v) ∷ l) n = if f k n then just v else lookupᵇ f l n
 
-zipWithIndex : {A B : Set} → (ℕ → A → B) → List A → List B
+zipWithIndex : (ℕ → A → B) → List A → List B
 zipWithIndex f l = zipWith f (upTo $ length l) l
   where open import Data.Fin; open import Data.List
 
-enumerate : {A : Set} → List A → List (ℕ × A)
+enumerate : List A → List (ℕ × A)
 enumerate = zipWithIndex _,_
 
--- ** variables
-variable
-  ℓ ℓ′ ℓ″ : Level
-  A B C D : Set ℓ
+_⁉_ : List A → ℕ → Maybe A
+_⁉_ = λ where
+  []       _       → nothing
+  (x ∷ _)  zero    → just x
+  (_ ∷ xs) (suc n) → xs ⁉ n
diff --git a/Reflection/Utils/Args.agda b/Reflection/Utils/Args.agda
@@ -64,3 +64,13 @@ hide = λ where
 apply⋯ : Args Type → Name → Type
 apply⋯ is n = def n $ remove-iArgs $
   map (λ{ (n , arg i _) → arg i (♯ (length is ∸ suc (toℕ n)))}) (zip (allFin $ length is) is)
+
+-- Applying a list of arguments to a term of any shape.
+apply∗ : Term → Args Term → Term
+apply∗ f xs = case f of λ where
+  (def n as)      → def n (as ++ xs)
+  (con c as)      → con c (as ++ xs)
+  (var x as)      → var x (as ++ xs)
+  (pat-lam cs as) → pat-lam cs (as ++ xs)
+  (meta x as)     → meta x (as ++ xs)
+  f               → f
diff --git a/Reflection/Utils/Records.agda b/Reflection/Utils/Records.agda
@@ -5,18 +5,13 @@ open import Meta.Prelude
 open import Meta.Init
 
 open import Data.List using (map)
-open import Relation.Nullary.Decidable using (⌊_⌋)
-
-import Reflection.AST.Name as Name
+open import Class.DecEq using (_==_)
 
 mkRecord : List (Name × Term) → Term
-mkRecord fs = pat-lam (map (λ where (fn , e) → clause [] [ vArg (proj fn) ] e) fs) []
+mkRecord fs = pat-lam (map (λ (fn , e) → clause [] [ vArg (proj fn) ] e) fs) []
 
 updateField : List Name → Term → Name → Term → Term
 updateField fs rexp fn fexp =
-  pat-lam (flip map fs $ λ f →
-    if ⌊ f Name.≟ fn ⌋ then
-      clause [] [ vArg (proj fn) ] fexp
-    else
-      clause [] [ vArg (proj f) ] (f ∙⟦ rexp ⟧)
-    ) []
+  flip pat-lam [] $ flip map fs $ λ f →
+    clause [] [ vArg (proj f) ] $
+      if f == fn then fexp else (f ∙⟦ rexp ⟧)
diff --git a/Tactic.agda b/Tactic.agda
@@ -1,10 +1,11 @@
 module Tactic where
 
 open import Tactic.Try public
-open import Tactic.Rewrite public
+open import Tactic.Rewrite public; open import Tactic.Rewrite.Tests
 open import Tactic.Extra public
 open import Tactic.Existentials public
 open import Tactic.ByEq public
+open import Tactic.Inline public
 
 open import Tactic.AnyOf public
 open import Tactic.Assumption public
@@ -17,6 +18,5 @@ open import Tactic.ReduceDec public
 
 open import Tactic.Derive.DecEq public
 open import Tactic.Derive.Show public
-open import Tactic.Derive.HsType public
-open import Tactic.Derive.HsType.Tests
+open import Tactic.Derive.HsType public; open import Tactic.Derive.HsType.Tests
 open import Tactic.Derive.Convertible public
diff --git a/Tactic/Assumption.agda b/Tactic/Assumption.agda
@@ -18,8 +18,7 @@ open import Reflection.Tactic
 open import Reflection.Utils
 open import Reflection.Utils.TCI
 
-instance
-  _ = Functor-M
+instance _ = Functor-M
 
 assumption' : ITactic
 assumption' = inDebugPath "assumption" do
diff --git a/Tactic/ByEq.agda b/Tactic/ByEq.agda
@@ -3,10 +3,10 @@ module Tactic.ByEq where
 
 open import Meta.Init hiding (TC)
 open import Meta.Prelude
-open import Class.Functor.Core; open import Class.Functor.Instances
-open import Class.Monad.Core; open import Class.Monad.Instances
+open import Class.Functor
+open import Class.Monad
 open import Reflection using (TC; withNormalisation; inferType; unify)
-open import Reflection.Utils
+open import Reflection.Utils using (argTys)
 
 -- Introduce as many arguments as possible and then:
 --   1. for those of type `_ ≡ _`, unify with  `refl`
diff --git a/Tactic/Derive/Convertible.agda b/Tactic/Derive/Convertible.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --with-K #-}
 module Tactic.Derive.Convertible where
 
 open import Meta.Prelude
diff --git a/Tactic/Derive/DecEq.agda b/Tactic/Derive/DecEq.agda
@@ -7,7 +7,7 @@
 -- - maybe more
 
 {-# OPTIONS -v allTactics:100 #-}
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --with-K #-}
 module Tactic.Derive.DecEq where
 
 open import Meta.Prelude
@@ -33,8 +33,7 @@ open import Class.Traversable
 open import Tactic.ClauseBuilder
 open import Tactic.Derive (quote DecEq) (quote _≟_)
 
-instance
-  _ = ContextMonad-MonadTC
+instance _ = ContextMonad-MonadTC
 
 open ClauseExprM
 
diff --git a/Tactic/Derive/HsType.agda b/Tactic/Derive/HsType.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --with-K #-}
 module Tactic.Derive.HsType where
 
 open import Meta.Init hiding (TC; Monad-TC; MonadError-TC)
diff --git a/Tactic/Derive/Show.agda b/Tactic/Derive/Show.agda
@@ -1,7 +1,7 @@
 -- Deriving show.
 
 {-# OPTIONS -v allTactics:100 #-}
-{-# OPTIONS --safe #-}
+{-# OPTIONS --safe --with-K #-}
 module Tactic.Derive.Show where
 
 open import Meta.Prelude
diff --git a/Tactic/Existentials.agda b/Tactic/Existentials.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe --without-K #-}
 module Tactic.Existentials where
 
 open import Meta.Prelude
diff --git a/Tactic/Extra.agda b/Tactic/Extra.agda
@@ -1,4 +1,5 @@
-{-# OPTIONS -v extra:100 #-}
+{-# OPTIONS --safe --without-K #-}
+-- {-# OPTIONS -v tactic.extra:100 #-}
 module Tactic.Extra where
 
 open import Meta.Prelude
@@ -21,7 +22,7 @@ open import Class.Monad
 open import Class.Semigroup
 open import Class.Show
 
-open Debug ("extra" , 100)
+open Debug ("tactic.extra" , 100)
 
 macro
   ∶t : Name → Hole → TC ⊤
diff --git a/Tactic/Inline.agda b/Tactic/Inline.agda
diff --git a/Tactic/Rewrite.agda b/Tactic/Rewrite.agda
diff --git a/Tactic/Rewrite/Tests.agda b/Tactic/Rewrite/Tests.agda
diff --git a/Tactic/Try.agda b/Tactic/Try.agda
diff --git a/standard-library-meta.agda b/standard-library-meta.agda

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+{-# OPTIONS --safe --without-K #-}`
`1`	`2`	`module Class.Convertible where`
`2`	`3`
`3`	`4`	`open import Class.Convertible.Core public`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+{-# OPTIONS --safe --without-K #-}`
`1`	`2`	`module Class.Convertible.Core where`
`2`	`3`
`3`	`4`	`open import Meta.Prelude`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+{-# OPTIONS --safe --without-K #-}`
`1`	`2`	`module Class.HasHsType where`
`2`	`3`
`3`	`4`	`open import Class.HasHsType.Core public`
Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+{-# OPTIONS --safe --without-K #-}`
`1`	`2`	`module Class.HasHsType.Core where`
`2`	`3`
`3`	`4`	`open import Meta.Prelude`