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 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 | module Arith where
data Nat : Set where
Z : Nat
S : Nat -> Nat
infix 40 _+_
_+_ : Nat -> Nat -> Nat
Z + n = n
S m + n = S (m + n)
infix 30 _≡_
data _≡_ {a : Set} (x : a) : a -> Set where
refl : x ≡ x
≡-succ : {m n : Nat} -> m ≡ n -> S m ≡ S n
≡-succ refl = refl
lemma₁ : (m n : Nat) -> S m + n ≡ m + S n
lemma₁ Z n = refl
lemma₁ (S m) n = ≡-succ (lemma₁ m n)
lemma₂ : (m : Nat) -> m ≡ m + Z
lemma₂ Z = refl
lemma₂ (S m) = ≡-succ (lemma₂ m)
⟨_,_⟩_ : {a : Set}{x y : a} (P : a -> Set) -> x ≡ y -> P x -> P y
⟨ P , refl ⟩ x = x
data FunList (a : Set) (b : Set) : Set where
Done : b -> FunList a b
More : a -> FunList a (a -> b) -> FunList a b
infixr 50 _::_
data Vec (a : Set) : Nat -> Set where
[] : Vec a Z
_::_ : {n : Nat} -> a -> Vec a n -> Vec a (S n)
infixr 20 _,_
data Σ (a : Set) (P : a -> Set) : Set where
_,_ : (x : a) -> (w : P x) -> Σ a P
infixr 20 _×_
_×_ : Set -> Set -> Set
a × b = Σ a (\_ -> b)
reverse : forall {a n} -> Vec a n -> Vec a n
reverse {a} l = ⟨ Vec a , refl ⟩ go [] l
where
go : forall {a m n} -> Vec a m -> Vec a n -> Vec a (m + n)
go {a} {m} acc [] = ⟨ Vec a , lemma₂ m ⟩ acc
go {a} {m} {S n} acc (x :: xs) = ⟨ Vec a , lemma₁ m n ⟩ go (x :: acc) xs
Order : (n : Nat) (a b : Set) -> Set
Order Z a b = b
Order (S n) a b = Order n a (a -> b)
lens : {a b : Set} -> FunList a b -> Σ Nat (\n -> Vec a n × Order n a b)
lens (Done f) = (Z , [] , f)
lens (More a l) with lens l
... | (n , as , f) = (S n , a :: as , f)
unlens : {a b : Set} -> Σ Nat (\n -> Vec a n × Order n a b) -> FunList a b
unlens (Z , [] , f) = Done f
unlens (S n , a :: as , f) = More a (unlens (n , as , f))
reverseFL : {a b : Set} -> FunList a b -> FunList a b
reverseFL fl with lens fl
... | (n , v , f) = unlens (n , reverse v , f)
|
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 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 | module FunList where
data Nat : Set where
Z : Nat
S : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO Z #-}
{-# BUILTIN SUC S #-}
infixl 60 _+_
_+_ : Nat -> Nat -> Nat
Z + n = n
S m + n = S (m + n)
{-# BUILTIN NATPLUS _+_ #-}
data FunL (a b : Set) : Set where
Done : (f : b) -> FunL a b
More : (h : a) (t : FunL a (a -> b)) -> FunL a b
infixr 55 _::_
data [_] (a : Set) : Set where
[] : [ a ]
_::_ : a -> [ a ] -> [ a ]
data _≡_ {a : Set} (x : a) : a -> Set where
refl : x ≡ x
data _T-≡_ : Set -> Set -> Set1 where
T-refl : {a : Set} -> a T-≡ a
get-b : {a b : Set} -> FunL a b -> b
get-b (Done f) = f
get-b (More h t) = get-b t h
get-as : {a b : Set} -> FunL a b -> [ a ]
get-as (Done f) = []
get-as (More h t) = h :: get-as t
Order : Nat -> Set -> Set -> Set
Order Z a b = b
Order (S n) a b = Order n a (a -> b)
Order' : Nat -> Set -> Set -> Set
Order' Z a b = b
Order' (S n) a b = a -> Order' n a b
infixr 30 _T-trans_
_T-trans_ : {a b c : Set} -> a T-≡ b -> b T-≡ c -> a T-≡ c
T-refl T-trans T-refl = T-refl
up : {b c : Set} -> (a : Set) -> b T-≡ c -> (a -> b) T-≡ (a -> c)
up a T-refl = T-refl
lemma₀ : forall n a b -> Order (S n) a b T-≡ (a -> Order n a b)
lemma₀ Z a b = T-refl
lemma₀ (S n) a b = pf₀ T-trans pf₁ T-trans pf₂
where
pf₀ : Order (S (S n)) a b T-≡ Order (S n) a (a -> b)
pf₀ = T-refl
pf₁ : Order (S n) a (a -> b) T-≡ (a -> Order n a (a -> b))
pf₁ = lemma₀ n a (a -> b)
pf₂ : (a -> Order n a (a -> b)) T-≡ (a -> Order (S n) a b)
pf₂ = T-refl
lemma₁ : forall n a b -> Order n a b T-≡ Order' n a b
lemma₁ Z a b = T-refl
lemma₁ (S n) a b = lemma₀ n a b T-trans up a (lemma₁ n a b)
⟨_⟩_ : {a b : Set} -> a T-≡ b -> a -> b
⟨ T-refl ⟩ v = v
T-resp : {a b : Set} -> (P : Set -> Set) -> a T-≡ b -> P a T-≡ P b
T-resp P T-refl = T-refl
T-symm : {a b : Set} -> a T-≡ b -> b T-≡ a
T-symm T-refl = T-refl
more : forall {n a b} -> a -> FunL a (Order (S n) a b) -> FunL a (Order n a b)
more {n} {a} {b} h t = More h t'
where
t' : FunL a (a -> Order n a b)
t' = ⟨ T-resp (FunL a) (lemma₀ n a b) ⟩ t
more∘ : forall {m n a} -> a
-> (forall b -> FunL a (Order n a b) -> FunL a (Order m a b))
-> (forall b -> FunL a (Order (S n) a b) -> FunL a (Order m a b))
more∘ {m} {n} {a} h k b t = more {m} h (k (a -> b) t)
-- This fails the termination checker, because of the coercion used in t'
-- I don't know how to structure it so that this doesn't happen.
rev : forall {m n a b}
-> (forall c -> FunL a (Order n a c) -> FunL a (Order m a c))
-> FunL a (Order n a b) -> FunL a (Order m a b)
rev {m} {n} {a} {b} acc (Done f) = acc b (Done f)
rev {m} {n} {a} {b} acc (More h t) = rev {m} {S n} (more∘ {m} {n} h acc) t'
where
t' : FunL a (Order (S n) a b)
t' = ⟨ T-resp (FunL a) (T-symm (lemma₀ n a b)) ⟩ t
reverseFun : {a b : Set} -> FunL a b -> FunL a b
reverseFun {a} = rev {0} {0} (\c f -> f)
test : FunL Nat Nat
test = More 1 (More 2 (More 3 (Done (\x y z -> x + y + z))))
-- get-as test ==> 1 :: 2 :: 3 :: []
-- get-as (reverseFun test) ==> 3 :: 2 :: 1 :: []
|
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 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 | {-# OPTIONS --sized-types #-}
module FunList where
data Nat : Set where
Z : Nat
S : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO Z #-}
{-# BUILTIN SUC S #-}
infixl 60 _+_
_+_ : Nat -> Nat -> Nat
Z + n = n
S m + n = S (m + n)
{-# BUILTIN NATPLUS _+_ #-}
data FunL (a b : Set) : Set where
Done : (f : b) -> FunL a b
More : (h : a) (t : FunL a (a -> b)) -> FunL a b
infixr 55 _::_
data [_] (a : Set) : Set where
[] : [ a ]
_::_ : a -> [ a ] -> [ a ]
data _≡_ {a : Set} (x : a) : a -> Set where
refl : x ≡ x
data _T-≡_ : Set -> Set -> Set1 where
T-refl : {a : Set} -> a T-≡ a
data T-Inspect (a : Set) : Set1 where
it : (b : Set) -> a T-≡ b -> T-Inspect a
get-b : {a b : Set} -> FunL a b -> b
get-b (Done f) = f
get-b (More h t) = get-b t h
get-as : {a b : Set} -> FunL a b -> [ a ]
get-as (Done f) = []
get-as (More h t) = h :: get-as t
Order : Nat -> Set -> Set -> Set
Order Z a b = b
Order (S n) a b = Order n a (a -> b)
Order' : Nat -> Set -> Set -> Set
Order' Z a b = b
Order' (S n) a b = a -> Order' n a b
infixr 30 _T-trans_
_T-trans_ : {a b c : Set} -> a T-≡ b -> b T-≡ c -> a T-≡ c
T-refl T-trans T-refl = T-refl
up : {b c : Set} -> (a : Set) -> b T-≡ c -> (a -> b) T-≡ (a -> c)
up a T-refl = T-refl
lemma₀ : forall n a b -> Order (S n) a b T-≡ (a -> Order n a b)
lemma₀ Z a b = T-refl
lemma₀ (S n) a b = pf₀ T-trans pf₁ T-trans pf₂
where
pf₀ : Order (S (S n)) a b T-≡ Order (S n) a (a -> b)
pf₀ = T-refl
pf₁ : Order (S n) a (a -> b) T-≡ (a -> Order n a (a -> b))
pf₁ = lemma₀ n a (a -> b)
pf₂ : (a -> Order n a (a -> b)) T-≡ (a -> Order (S n) a b)
pf₂ = T-refl
lemma₁ : forall n a b -> Order n a b T-≡ Order' n a b
lemma₁ Z a b = T-refl
lemma₁ (S n) a b = lemma₀ n a b T-trans up a (lemma₁ n a b)
⟨_⟩_ : {a b : Set} -> a T-≡ b -> a -> b
⟨ T-refl ⟩ v = v
T-resp : {a b : Set} -> (P : Set -> Set) -> a T-≡ b -> P a T-≡ P b
T-resp P T-refl = T-refl
T-symm : {a b : Set} -> a T-≡ b -> b T-≡ a
T-symm T-refl = T-refl
more : forall {n a b} -> a -> FunL a (Order (S n) a b)
-> FunL a (Order n a b)
more {n} {a} {b} h t = More h t'
where
t' : FunL a (a -> Order n a b)
t' = ⟨ T-resp (FunL a) (lemma₀ n a b) ⟩ t
more∘ : forall {m n a} -> a
-> (forall b -> FunL a (Order n a b) -> FunL a (Order m a b))
-> (forall b -> FunL a (Order (S n) a b) -> FunL a (Order m a b))
more∘ {m} {n} {a} h k b t = more {m} h (k (a -> b) t)
rev : forall {m n a b}
-> (forall c -> FunL a (Order n a c) -> FunL a (Order m a c))
-> FunL a (Order' n a b) -> FunL a (Order m a b)
rev {m} {n} {a} {b} acc (Done f) = acc b (⟨ pf ⟩ Done f)
where
pf : FunL a (Order' n a b) T-≡ FunL a (Order n a b)
pf = T-resp (FunL a) (T-symm (lemma₁ n a b))
rev {m} {n} {a} {b} acc (More h t) = rev {m} {S n} (more∘ {m} {n} h acc) t
reverseFun : {a b : Set} -> FunL a b -> FunL a b
reverseFun {a} = rev {0} {0} (\c f -> f)
test : FunL Nat Nat
test = More 1 (More 2 (More 3 (Done (\x y z -> x + y + z))))
-- get-as test ==> 1 :: 2 :: 3 :: []
-- get-as (reverseFun test) ==> 3 :: 2 :: 1 :: []
|