{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-- Modeling of an extensible, recursive sum datatype (recursive open union)
--    data List a = Nil | Cons a (List a)
-- which is later extended with two more variants,
--    ... | Unit a | App (List a) (List a)
-- 
-- Our goals:
--   - any function that accepts the extended data list
--     must also accept the unextended list.
--   - it should be possible to `extend' the function that operates
--     on plain lists to operate on extended list. We should be able
--     to reuse as much of the old code as possible.
-- It seems, we have achieved our goals.

-- Method: duality rules! Curry-Howard correspondence and logic 
-- give the wonderful guidance. In particular, we take advantage
-- of the fact that the deMorgan law
--  	NOT (A | B) -> (NOT A & NOT B)
-- holds both in classical, and, more importantly, intuitionistic
-- logics. Our encoding of sums is the straightforward Curry-Howard
-- image of the law.

-- Note, the code below has no type classes, no type-level programming
-- or any other type hacking. In fact, there are no type annotations,
-- type declarations, or any other mentioning of types, except in the comments

module VariantP where

import CommonMain
import GhcSyntax
import Label1


-- Declare labels for extensible records -- or, dually, for
-- extensible variants
-- We used the simplest field labels. They are a bit
-- ungainly to use -- but let us avoid overlapping instance extension.
-- See OOHaskell for the use of more advanced labels.

l_nil   = firstLabel
l_cons  = nextLabel l_nil

nil consumer = consumer .!. l_nil

cons a l consumer = (consumer .!. l_cons) a (l consumer)

tl1 c = cons 'a' (cons 'b' (cons 'c' nil)) c
tl2 c = cons 10 (cons 1 (cons 2 (cons 3 nil))) c

{-
  The inferred type of tl1 is

*Variants> :t tl1
tl1 :: (HasField (Label (HSucc HZero)) r (Char -> v -> v),
	HasField (Label HZero) r v) =>
       r -> v

which basically says that tl1 accepts any consumer that has at least
fields l_nil and l_cons with appropriate types. The consumer
may have more fields
-}


-- First polymorphic function: provide a regular list "view" of our list

to_list () =     l_nil  .=. []
	     .*. l_cons .=. (:) 
	     .*. emptyRecord

-- I wish GHC supported unicode in identifiers
tekiyou consumer lst = lst (consumer ())

test1 = tekiyou to_list tl1
test2 = tekiyou to_list tl2

-- another function, length

lengthL () =  l_nil  .=. 0
	  .*. l_cons .=. (\x a -> a + 1)
	  .*. emptyRecord

test_lL1 = tekiyou lengthL tl1
test_lL2 = tekiyou lengthL tl2


-- Now, add extension to our record -- and, dually, extend our variant

l_unit = nextLabel l_cons
l_app  = nextLabel l_unit

unit a c = (c .!. l_unit) a

app l1 l2 c = (c .!. l_app) (l1 c) (l2 c)

tl3 c = cons 1 (unit 2) c
tl4 c = cons 10 (app tl3 tl2) c

sumA () =  l_nil  .=. 0
       .*. l_cons .=. (+)
       .*. l_unit .=. id
       .*. l_app  .=. (+)
       .*. emptyRecord

-- we can apply sum to an original (unextended) list
test_sum1 = tekiyou sumA tl2

-- now, we can apply sum to an extended list
test_sum2 = tekiyou sumA tl4


-- we can't pass extended lists tl3 and tl4 to a regular lenghtL
-- The error message says that the field l_unit is missing
-- test_lL3 = tekiyou lengthL tl3


-- now we can attempt to extend lengthL, reusing as much of previous
-- functionality as possible

lengthA () =  l_unit .=. const 1
	  .*. l_app  .=. (+)
	  .*. (lengthL ())

test_lL4 = tekiyou lengthA tl3
test_lL5 = tekiyou lengthA tl4


-- A few methods to show that our extensible lists indeed act
-- as regular lists (that is, support the regular list API).

-- check if the (extensible list) is null:
el_null l = l (l_nil .=. True .*. l_cons .=. (\x a -> False) 
	       .*. emptyRecord)

el_head l = l (l_nil .=. undefined .*. l_cons .=. (\x a -> x)
	       .*. emptyRecord)

el_tail l = l (    l_nil .=. (\f -> if f then undefined else nil) 
	       .*. l_cons .=. (\x a f -> if f then a False else
			       cons x (a False))
	       .*. emptyRecord) True

test_ell = (el_null tl1, el_head tl1, tekiyou to_list $ el_tail tl1)


-- convert from the regular list
from_list l = foldr cons nil l

test_ft1 = tekiyou to_list $ from_list "abcd"


-- Binary methods.
-- Hmm, doing it directly is complicated. OTH, we can use the list view
-- (to_list) and solve the problem this way...
-- Laziness helps...

eqL l1 l2 = tekiyou to_list l1 == tekiyou to_list l2
test_eq1 = eqL tl1 tl1
test_eq2 = eqL tl1 (cons 'a' nil)
test_eq3 = eqL tl1 nil

-- we can extend to_list as usual

to_listA () =  l_unit .=. (:[])
	   .*. l_app  .=. (++)
	   .*. (to_list ())

-- And we can arbitrary mix old and extended lists
eqA l1 l2 = tekiyou to_listA l1 == tekiyou to_listA l2
test_eq4 = eqA tl1 tl1
test_eq5 = eqA tl2 tl3
test_eq6 = eqA tl3 tl4