hpastetwo

New Revision

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 :: []

author title

language channel