{- LOOKMANO --no-positivity-check
  -}

module Ornament where

record One : Set where

{-
record Sig (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T}

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sig S T
s , t = record {fst = s; snd = t}

-}

data Sig (S : Set)(T : S -> Set) : Set where
  _,_ : (s : S) -> T s -> Sig S T

fst : forall {S T} -> Sig S T -> S
fst (s , t) = s

snd : forall {S T}(x : Sig S T) -> T (fst x)
snd (s , t) = t

infixr 40 _,_

_/_ : {I J : Set} -> (J -> Set) -> (I -> J) -> I -> Set
_/_ F f i = F (f i)

_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set
X -:> Y = {i : _} -> X i -> Y i

Alg : {I : Set} -> ((I -> Set) -> I -> Set) -> (I -> Set) -> Set
Alg F X = F X -:> X

infix 40 _-:>_
infixl 50 _/_

_*_ : Set -> Set -> Set
S * T = Sig S \ _ -> T

data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x

data Desc (I : Set) : Set1 where
  out : (o : I) -> Desc I
  arg : (A : Set)(D : A -> Desc I) -> Desc I
  _rec_ : (h : I)(D : Desc I) -> Desc I

[!_!] : {I : Set} -> Desc I -> (I -> Set) -> I -> Set
[! out o   !]   X i = o == i
[! arg A D !]   X i = Sig A \ a -> [! D a !] X i
[! h rec D !]  X i = X h * [! D !] X i

data Data {I : Set}(D : Desc I)(i : I) : Set where
  <_> : [! D !] (Data D) i -> Data D i

map : {I : Set}(D : Desc I){X Y : I -> Set} ->
      X -:> Y -> [! D !] X -:> [! D !] Y
map (out o)   f q  = q
map (arg A D) f (a , d) = a , map (D a) f d
map (h rec D) f (x , d) = f x , map D f d

fold :  {I : Set}{D : Desc I}{X : I -> Set} ->
        Alg [! D !] X -> Data D -:> X
fold {D = D} phi < d > = phi (map D (fold phi) d)

data Two : Set where
  tt : Two
  ff : Two

Case : {P : Two -> Set1} -> P tt -> P ff -> (b : Two) -> P b
Case t f tt = t
Case t f ff = f 

NAT : Desc One
NAT = arg Two (Case (out _) (_ rec out _))

Nat : Set
Nat = Data NAT _

zero : Nat
zero = < tt , refl >

suc : Nat -> Nat
suc n = < ff , n , refl >

_+_ : Nat -> Nat -> Nat
_+_ x y = fold palg x where
  palg : Alg [! NAT !] (\ _ -> Nat)
  palg (tt , refl)        = y
  palg (ff , x+y , refl)  = suc x+y

data _Inv_ {I J : Set}(f : J -> I) : I -> Set where
  inv : (j : J) -> f Inv (f j)

data Orn {I : Set}(J : Set)(f : J -> I) : Desc I -> Set1 where
  out : {o : I}(jq : f Inv o) -> Orn J f (out o)
  arg : (A : Set){D : A -> Desc I}
        (O : (a : A) -> Orn J f (D a)) -> Orn J f (arg A D)
  _rec_ : {h : I}{D : Desc I} ->
          (jq : f Inv h)(O : Orn J f D) -> Orn J f (h rec D)
  new : {D : Desc I}(A : Set)(O : A -> Orn J f D) -> Orn J f D

infixr 40 _rec_

oD : {I J : Set}{f : J -> I}{D : Desc I} -> Orn J f D -> Desc J
oD (out (inv j))   = out j
oD (arg A O)  = arg A \ a -> oD (O a)
oD (inv j rec O) = j rec (oD O)
oD (new A O)  = arg A \ a -> oD (O a)

oAHelp : forall {I J f}{D : Desc I}{R : I -> Set} -> (O : Orn J f D) ->
                     [! oD O !] (R / f) -:> [! D !] R / f
oAHelp (out (inv j)) refl = refl
oAHelp (arg A O) (a , o) = a , oAHelp (O a) o
oAHelp (inv j' rec O) (x , o) = x , oAHelp O o
oAHelp (new A O) (a , o) = oAHelp (O a) o

ornAlg : {I J : Set}{f : J -> I}{D : Desc I}(O : Orn J f D) ->
         Alg [! oD O !] (Data D / f)
ornAlg {I} {J} {f} {D} O d = < oAHelp O d >

NAT-LIST : Set -> Orn One _ NAT
NAT-LIST X = arg Two (Case
               (out (inv _) )
               (new X \ _ -> inv _ rec out (inv _)))

LIST : Set -> Desc One
LIST X = oD (NAT-LIST X)

List : Set -> Set
List X = Data (LIST X) _

[l] : {X : Set} -> List X
[l] = < tt , refl >

_:l:_ : {X : Set} -> X -> List X -> List X
x :l: xs = < ff , x , xs , refl >

algOrn : {I : Set}{J : I -> Set}(D : Desc I) ->
         Alg [! D !] J -> Orn (Sig I J) fst D
algOrn (out o) phi = out (inv (o , phi refl)) 
algOrn (arg A D) phi = arg A \ a -> algOrn (D a) \ d -> phi (a , d) 
algOrn {J = J} (h rec D) phi =
  new (J h) \ j ->
  inv (h , j) rec algOrn D \ d -> phi (j , d)

LIST-VEC : (X : Set) -> Orn (One * Nat) _ (LIST X)
LIST-VEC X = algOrn (LIST X) (ornAlg (NAT-LIST X))

VEC : Set -> Desc (One * Nat)
VEC X = oD (LIST-VEC X)

Vec : Nat -> Set -> Set
Vec n X = Data (VEC X) (_ , n)

[] : {X : Set} -> Vec zero X
[] = < tt , refl >

_::_ : {n : Nat}{X : Set} -> X -> Vec n X -> Vec (suc n) X
x :: xs = < ff , x , _ , xs , refl >

All : {I : Set}(D : Desc I){R : I -> Set}(P : {i : I} -> R i -> Set)
      {i : I} -> [! D !] R i -> Set
All (out o) P x = One 
All (arg A D) P (a , d) = All (D a) P d
All (h rec D) P (x , d) = P x * All D P d

everywhere : {I : Set}(D : Desc I){R : I -> Set}
             (P : {i : I} -> R i -> Set) ->
             ({i : I}(x : R i) -> P x) ->
             {i : I}(d : [! D !] R i) -> All D P d
everywhere (out o) P p d = _ 
everywhere (arg A D) P p (a , d) = everywhere (D a) P p d
everywhere (h rec D) P p (x , d) = p x , everywhere D P p d

induction : {I : Set}(D : Desc I)(P : {i : I} -> Data D i -> Set) ->
            ({i : I}(d : [! D !] (Data D) i) -> All D P d -> P < d >) ->
            {i : I}(x : Data D i) -> P x
induction D P p < d > = p d (everywhere D P (induction D P p) d)


AOOAHelp : {I : Set}{J R : I -> Set}{Y : Sig I J -> Set}
           (g : R -:> J)
           (f : Y -:> R / fst)
           (D : Desc I)(phi : Alg [! D !] J) ->
           let Dphi = algOrn D phi in
           {ij : Sig I J}(d : [! oD Dphi !] Y ij) ->
           All (oD Dphi) (\ {ij} y -> g (f y) == snd ij) d ->
           phi (map D g (oAHelp Dphi (map (oD Dphi) f d))) == snd ij
AOOAHelp g f (out o) phi refl H = refl 
AOOAHelp g f (arg A D) phi (a , d) H =
   AOOAHelp g f (D a) (\ d -> phi (a , d)) d H 
AOOAHelp g f (h rec D) phi (j , y , d) (q , H) with g (f y)
AOOAHelp g f (h rec D) phi (j , y , d) (refl , H) | .j =
   AOOAHelp g f D (\ d -> phi (j , d)) d H 
           
AOOAThm : {I : Set}(D : Desc I){J : I -> Set}(phi : Alg [! D !] J) ->
          let Dphi = algOrn D phi in
          {ij : Sig I J}(x : Data (oD Dphi) ij) ->
          fold phi (fold (ornAlg Dphi) x)
            == snd ij
AOOAThm {I} D {J} phi = let Dphi = algOrn D phi in
  induction  (oD Dphi)
  (\ {ij} x ->  fold phi (fold (ornAlg Dphi) x) == snd ij)
  (AOOAHelp {R = Data D} (fold phi) (fold (ornAlg (algOrn D phi))) D phi)

data HOp : Set where
  PUSH : HOp
  SEQ  : HOp
  ADD  : HOp

HCode : Desc (Nat * Nat)
HCode = arg HOp args where
  args : HOp -> Desc (Nat * Nat)
  args PUSH = arg Nat \ _ -> arg Nat \ i -> out (i , suc i) 
  args SEQ = arg Nat \ k -> arg Nat \ l -> arg Nat \ m ->
              (k , l) rec (l , m) rec out (k , m) 
  args ADD = arg Nat \ i -> out (suc (suc i) , suc i) 

HSem : Nat * Nat -> Set
HSem ij = Vec (fst ij) Nat -> Vec (snd ij) Nat

HAlg : Alg [! HCode !] HSem
HAlg (PUSH , n , i , refl) ns = n :: ns
HAlg (SEQ , k , l , m , f , g , refl) ns = g (f ns)
HAlg (ADD , i , refl)
     < ff , x , .(suc i) , < ff , y , .i , stk , refl > , refl >
     = (y + x) :: stk
HAlg (ADD , i , refl) < ff , _ , ._ , < tt , () > , refl >
HAlg (ADD , i , refl) < tt , () >

HCodeSem : Desc (Sig (Nat * Nat) HSem)
HCodeSem = oD (algOrn HCode HAlg)

HExp : Desc One
HExp = arg Two (Case (arg Nat \ _ -> out _) (_ rec _ rec out _ ))

hEval : Data HExp _ -> Nat
hEval = fold evAlg where
  evAlg : Alg [! HExp !] (\ _ -> Nat)
  evAlg ( tt , n , refl )     = n
  evAlg ( ff , a , b , refl ) = a + b

hCompileSem : (e : Data HExp _) ->
           {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval e))
hCompileSem = induction HExp
   (\e ->  {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval e)))
   help where
   help : (d : [! HExp !] (Data HExp) _) ->
          All HExp (\ e ->
           {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval e))) d ->
          {i : Nat} -> Data HCodeSem ((i , suc i) , _::_ (hEval < d >))
   help ( tt , n , refl ) H = < PUSH , n , _ , refl > 
   help ( ff , a , b , refl ) ( ca , cb , _ )
     = < SEQ , _ , _ , _ , _ , ca , _ ,
        < SEQ , _ , _ , _ , _ , cb , _ ,
         < ADD , _ , refl >
        , refl >
       , refl > 

hCompile : Data HExp _ -> {i : Nat} -> Data HCode (i , suc i)
hCompile e = fold (ornAlg (algOrn HCode HAlg)) (hCompileSem e)

hTheorem : (e : Data HExp _){i : Nat} ->
           fold HAlg (hCompile e {i}) == _::_ (hEval e)
hTheorem e = AOOAThm HCode HAlg (hCompileSem e)