Source code on Github{-# OPTIONS --safe --without-K #-}
module Tactic.Inline where
import Data.Nat as ℕ; import Data.Nat.Properties as ℕ
import Data.List as L
open import Relation.Unary using () renaming (Decidable to Decidable¹)
open import Relation.Nullary.Decidable using () renaming (map′ to mapDec)
open import Algebra.Core using (Op₁)
open import Class.Functor
open import Class.Monad
open import Class.Semigroup
open import Class.DecEq
open import Class.Show
open import Class.MonadTC.Instances
open import Class.MonadError.Instances
open import Meta.Prelude
open import Reflection.Syntax
open import Reflection.Utils using (apply∗)
open import Reflection.Utils.Debug; open Debug ("tactic.inline" , 100)
open import Reflection using (TC)
instance
iTC = MonadTC-TC
iTCE = MonadError-TC
private
pattern `case_of_ x y = quote case_of_ ∙⟦ x ∣ y ⟧
$inline : Bool → Name → Term → TC ⊤
$inline genType n' `e = do
e@(def n xs) ← return `e
where _ → _IMPOSSIBLE_
printLn $ "** Inlining " ◇ show n ◇ "(" ◇ show xs ◇ ")"
if genType
then (declareDef (vArg n') =<< inferType e)
else return tt
function cs ← getDefinition n
where _ → _IMPOSSIBLE_
print $ show n ◇ "'s clauses: "
void $ forM cs λ c → print $ " - " ◇ show c
print ""
let cs' = goᶜ n n' xs <$> cs
print $ "\n" ◇ show n' ◇ "'s clauses: "
void $ forM cs' λ c → print $ " - " ◇ show c
print ""
defineFun n' cs'
where module _ (n n' : Name) (xs : Args Term) (let ∣xs∣ = length xs) where
lookupVar : ℕ → ℕ → Maybe Term
lookupVar lvl x
with x ℕ.<? lvl
... | yes _ = nothing
... | no x≮ =
let record { quotient = k } = ℕ.≤⇒≤″ (ℕ.≮⇒≥ x≮)
in unArg <$> xs ⁉ (∣xs∣ ∸ suc k)
mutual
go : ℕ → Op₁ Term
go lvl = λ where
(var x as) → let as′ = go∗ lvl as in case lookupVar lvl x of λ where
nothing → var x as′
(just t) → apply∗ t as′
(def 𝕟 as) → let as′ = go∗ lvl as in
if 𝕟 == n then
def n' (drop ∣xs∣ as′)
else
def 𝕟 as′
(con c as) → con c (go∗ lvl as)
(pi (arg i ty) (abs x t)) → pi (arg i $ go lvl ty) (abs x $ go (suc lvl) t)
(lam v (abs x t)) → lam v (abs x $ go (suc lvl) t)
(pat-lam cs (vArg a ∷ [])) → `case go lvl a of pat-lam (goCls lvl cs) []
(pat-lam cs as) → pat-lam (goCls lvl cs) (go∗ lvl as)
(agda-sort s) → agda-sort (goSort lvl s)
(meta x as) → meta x (go∗ lvl as)
t → t
go∗ : ℕ → Op₁ (Args Term)
go∗ lvl = λ where
[] → []
(arg i x ∷ as) → arg i (go lvl x) ∷ go∗ lvl as
goSort : ℕ → Op₁ Sort
goSort lvl = λ where
(set t) → set $ go lvl t
(prop t) → prop $ go lvl t
s → s
goC : ℕ → Op₁ Clause
goC lvl = λ where
(clause tel ps t) →
let lvl' = lvl ℕ.+ length tel
in clause (goTel lvl tel) (goPs lvl' ps) (go lvl' t)
(absurd-clause tel ps) →
let lvl' = lvl ℕ.+ length tel
in absurd-clause (goTel lvl tel) (goPs lvl' ps)
goCls : ℕ → Op₁ (List Clause)
goCls lvl = λ where
[] → []
(c ∷ cs) → goC lvl c ∷ goCls lvl cs
goP : ℕ → Op₁ Pattern
goP lvl = λ where
(con c ps) → con c (goPs lvl ps)
(dot t) → dot (go lvl t)
(var x) → case lookupVar lvl x of λ where
nothing → var x
(just t) → dot t
p → p
goPs : ℕ → Op₁ (Args Pattern)
goPs lvl = λ where
[] → []
(arg i p ∷ ps) → arg i (goP lvl p) ∷ goPs lvl ps
goTel : ℕ → Op₁ Telescope
goTel lvl = λ where
[] → []
((x , arg i t) ∷ tel) → (x , arg i (go lvl t)) ∷ goTel (suc lvl) tel
goᶜ : Clause → Clause
goᶜ = λ where
(clause tel ps t) → let n = length tel ∸ ∣xs∣ in
clause (instTel tel) (instPs n ps) (go n t)
(absurd-clause tel ps) → let n = length tel ∸ ∣xs∣ in
absurd-clause (instTel tel) (instPs n ps)
where
instTel : Op₁ Telescope
instTel = goTel 0 ∘ drop ∣xs∣
instPs : ℕ → Op₁ (Args Pattern)
instPs n = goPs n ∘ drop ∣xs∣
inline inlineDecl : Name → Term → TC ⊤
inline = $inline false
inlineDecl = $inline true
private
unquoteDecl sucs = inlineDecl sucs (quoteTerm (L.map suc))
_ = sucs (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
∋ refl
data Even : ℕ → Set where
zero : Even 0
suc : ∀ {n} → Even n → Even (suc (suc n))
even? : Decidable¹ Even
even? = λ where
0 → yes zero
1 → no λ ()
(suc (suc n)) → mapDec suc (λ where (suc p) → p) (even? n)
open import Data.List.Relation.Unary.All using (All; []; _∷_; all?)
unquoteDecl evens? = inlineDecl evens? (quoteTerm (all? even?))
_ = evens? (0 ∷ 2 ∷ []) ≡ yes (zero ∷ suc zero ∷ [])
∋ refl
module _ (n m : ℕ) where
unquoteDecl ⟫evens? = inlineDecl ⟫evens? (quoteTerm (all? even?))
_ = ⟫evens? (0 ∷ 2 ∷ []) ≡ yes (zero ∷ suc zero ∷ [])
∋ refl
module _ {A B : Set} (f : A → B) where
map' : List A → List B
map' [] = []
map' (x ∷ xs) = f x ∷ map' xs
unquoteDecl sucs' = inlineDecl sucs' (quoteTerm (map' {B = ℕ} suc))
_ = sucs' (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
∋ refl
data Odd : ℕ → Set where
one : Odd 1
suc : ∀ {n} → Odd n → Odd (suc (suc n))
mutual
odd? : Decidable¹ Odd
odd? = λ where
0 → no λ ()
1 → yes one
(suc (suc n)) → mapDec suc (λ where (suc p) → p) (odd? n)
unquoteDecl mevens? = inlineDecl mevens? (quoteTerm (all? even?))
unquoteDecl modds? = inlineDecl modds? (quoteTerm (all? odd?))
_ = mevens? (0 ∷ 2 ∷ []) ≡ yes (zero ∷ suc zero ∷ [])
∋ refl
_ : modds? (1 ∷ 3 ∷ []) ≡ yes (one ∷ suc one ∷ [])
_ = refl
toEvenOdd : ℕ → ℕ × Maybe ℕ
toEvenOdd n with even? n
... | yes _ = n , nothing
... | no _ = pred n , just 1
toOdd : ℕ → Maybe ℕ
toOdd = proj₂ ∘ toEvenOdd
unquoteDecl toOdds = inlineDecl toOdds (quoteTerm (L.mapMaybe toOdd))
_ = toOdds (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ≡ (1 ∷ 1 ∷ [])
∋ refl
refl? : ℕ → Set
refl? n = case n ≟ n of λ where
(yes p) → ⊤
(no ¬p) → ⊥
unquoteDecl refl42 = inlineDecl refl42 (quoteTerm (refl? 42))