-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy.agda
54 lines (43 loc) · 1.68 KB
/
Copy.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
{-# OPTIONS --without-K --exact-split --rewriting --overlapping-instances #-}
open import HoTT hiding (_<_ ; ltS ; ltSR ; _+_ ; _×_)
import lib.types.Nat as N
import lib.types.Sigma as S
open import Pi.UFin.BAut
open import Pi.Common.Misc
open import Pi.Common.Extra
open import Pi.Syntax.Pi+.Indexed as Pi+
open import Pi.Syntax.Pi^ as Pi^
open import Pi.Syntax.Pi^Helpers as Pi^
open import Pi.Syntax.Pi as Pi
open import Pi.Equiv.Translation2
import Pi.Equiv.Equiv1 as Pi+
import Pi.Equiv.Equiv0Hat as Pi^
import Pi.Equiv.Equiv1Hat as Pi^
import Pi.Equiv.Equiv0Norm as Pi^
import Pi.Equiv.Equiv1Norm as Pi^
open import Pi.UFin.UFin
open import Pi.UFin.Monoidal
open import Pi.Common.FinHelpers
open import Pi.Lehmer.FinExcept
module Pi.Examples.Copy where
open import Pi.Examples.Base
open import Pi.Examples.Toffoli
-- copy(𝔽,b₁,…,bₙ) = (b₁,b₁,…,bₙ)
copy : ∀ n → 𝟚 Pi.× 𝔹 n Pi.⟷₁ 𝟚 Pi.× 𝔹 n
copy O = id⟷₁
copy (S O) = swap⋆ ◎ cnot ◎ swap⋆
copy (S (S n)) = assocl⋆ ◎ (copy (S O) ⊗ id⟷₁) ◎ assocr⋆
copy^ : ∀ n → _
copy^ = eval₁ ∘ copy
copy+ : ∀ n → _
copy+ = Pi^.quote^₁ ∘ Pi^.quoteNorm₁ idp ∘ Pi^.evalNorm₁ ∘ copy^
open import Pi.Examples.Interp
private
test-interp-copy1 = interp-elems (copy 1)
test-interp-copy1+ = interp+-elems (Pi^.quote^₁ (eval₁ (copy 1)))
test-interp-copy1^ = interp+-elems (copy+ 1)
test-encode-interp-copy1 = map encode-interp-elems test-interp-copy1
test-interp-copy2 = interp-elems (copy 2)
test-interp-copy2+ = interp+-elems (Pi^.quote^₁ (eval₁ (copy 2)))
test-interp-copy2^ = interp+-elems (copy+ 2)
test-encode-interp-copy2 = map encode-interp-elems test-interp-copy2