{-# OPTIONS -fglasgow-exts #-}

module Expr where

import Data.Maybe

import Base
import Representations
import Zipper

-- --------------------------------------
-- Types and conversion
-- --------------------------------------
infixl 7 :*:
infixl 6 :+:

data Expr = Const Int | Expr :+: Expr | Expr :*: Expr deriving Show

instance PFView Expr where
  type PF Expr = Sum (Con (K Int)) (Sum (Con (Prod Id Id)) (Con (Prod Id Id)))

  from (Const n)   = Inl (Con "Const" (K n))
  from (e1 :+: e2) = Inr (Inl (Con "(:+:)" $ Prod (Id e1) (Id e2)))
  from (e1 :*: e2) = Inr (Inr (Con "(:*:)" $ Prod (Id e1) (Id e2)))

  to (Inl (Con _ (K n)))                        = Const n
  to (Inr (Inl (Con _ (Prod (Id r1) (Id r2))))) = r1 :+: r2
  to (Inr (Inr (Con _ (Prod (Id r1) (Id r2))))) = r1 :*: r2

-- Example
-- initial zipper
zipE = toZipper (Const 1 :+: Const 2)
-- go down
zipE' = fromJust (down zipE)
expr1 = getZipper zipE'
-- go further right
zipE'' = fromJust (next zipE')
expr2 = getZipper zipE''