module ADT

import StdMisc
import StdOverloaded
import StdInt
import StdString

/*
 * Algebrai típusdefiníciók segítségével lényegében tetszőleges típust meg
 * tudunk adni, amelyet aztán felhasználhatunk a programjainkban.  Ehhez az
 * alapeszközeink lényegében a következőek:
 *
 * :: Empty                           // üres
 * :: Unit       = Unit               // egység
 * :: Pair a b   = Pair a b           // szorzat
 * :: Either a b = Left a | Right b   // összeg
 * :: Fix f      = Fix (f (Fix f))    // fixpont (rekurzió)
 *
 *
 * - `Empty`: Olyan típus, amelynek nincs eleme.  (Cleanben ilyet nem lehet
 *   megadni, ezt csak az elméleti teljesség miatt tesszük most hozzá.)
 *
 * - `Unit`: Egységtípus, amelynek csak egyetlen létezik.
 *
 * - `Pair`: Szorzattípus, amely két másik típusból építi fel azok elemeinek
 *    összes lehetséges kombinációját.  Ez tulajdonképpen egy Descartes-szorzat
 *    a két típus elemei között.  Így a létrehozott típus értékeinek száma
 *    megegyezik a szorzásban résztvevő típusok értékeinek számának
 *    szorzatával.  Ennek a típusnak az elemeit csak akkor tudjuk létrehozni,
 *    ha mind a két típusból tudunk elemet megadni.
 *
 * - `Either`: Összegtípus, amely két másik típusból építi fel azok elemeinek
 *   összes lehetséges kombinációját.  Ez lényegében a típusok értékeinek
 *   halmazainak uniójának feleltethető meg, azonban ez annál szigorúbb.  Itt
 *   egy ún. diszjunkt unióról van szó, vagyis az uniózás során elemek nem
 *   vesznek el még akkor sem, ha ugyanazt a típust uniózzuk össze magával.
 *   Ezt úgy érjük el, hogy az unióban résztvevő típusokat felcímkézzük és
 *   ezzel lehetőségünk nyílik az elemek megkülönböztetésére.  Egy ilyen típusú
 *   elem létrehozásához elengedő csak valamelyik típus elemét megadni.  Az így
 *   létrehozott típus értékeinek száma megegyezik az összeadásban résztvevő
 *   típusok értékeinek számának összegével.
 *
 * - `Fix`: Előfordulhat, hogy szükségünk lehet rekurzív típusokra.  Ekkor a
 *   függvényekhez hasonlóan egy fixpontkombinátorral tudunk ilyeneket is
 *   definiálni.  (Erre a programokban nincs szükség, mert a Clean típusrendszere
 *   implicite támogatja, a megemlítésének csak elméleti jelentősége van.)
 *
 * Ezek segítségével tehát meg lehet adni akár a listákat ábrázoló `List` típust
 * is.  Ez lényegében egy rekurzív, paraméteres típus.
 *
 * Ha egy típus rendelkezik paraméterrel, akkor azt egyben magasabbrendű
 * típusnak, vagy típuskonstruktornak is hívjuk, mivel segítségével további
 * típusokat tudunk előállítani.  A `List` is ezek közé tartozik.  Ezt az
 * ún. "kind" vagy fajta fogalmával jelöljük, amely lényegében a típusok
 * típusaként adható meg.  Ekkor a típushoz is rendelhetünk egy olyan típust,
 * amelyben nem konkrét értékek, hanem csak csillagok szerepelnek.
 *
 *     T :: * -> * -> * -> *
 *
 * Ennek megfelelően lehetnek alaptípusok (top-level type), amelyek kindja
 * egyszerűen "*".  Ilyen minden olyan típus, amely nem magasabbrendű, azaz
 * nincs paramétere, például a Clean `Int` típusa:
 *
 *     Int :: *
 *
 * A `List` pedig ennek megfelelően ilyen kinddal rendelkezik, ahol a `->`
 * a függvények típusához hasonlóan egy típusok közti leképezésre utal:
 *
 *     List :: * -> *
 *
 * A kindok jelölése azért fontos, hogy tudjuk, a típusokat milyen módokon
 * lehet egymással kombinálni.  Például az `Int` paramétere nem lehet a
 * `List`, mivel a kindjaik nem illeszkednek egymáshoz.
 *
 * Most definiáljuk tehát a saját lista típusunkat, amelyen keresztül
 * megmutatjuk a különböző listafüggvények működését!  Ez talán azért is lesz
 * majd hasznos, mert így jobban látható válik, mikor végzünk a listákkal
 * mintaillesztést, illetve mikor konstruálunk új listákat.  A Clean
 * hagyományos szintaktikája szerint ugyanis a kettő nem válik külön, ezért
 * eleinte zavaró lehet.  Egy egyszerű ökölszabállyal azt mondhatjuk, hogy ha
 * lista a definiáló egyenlőség jobb oldalán jelenik meg, akkor konstrukciót
 * jelent, ha a bal oldalán, akkor mintaillesztést.
 */
:: List a = Nil | Cons a (List a)

/*
 * Vegyük észre, hogy a definícióban lényegében a következő függvényeket, ún.
 * adatkonstruktorokat hoztuk létre:
 *
 *     Nil  :: List a                  -- üres lista, []
 *     Cons :: a (List a) -> List a    -- a (:) operátor
 *
 * A listák felépítéséhez készítünk egy saját infix operátort, amellyel egy
 * értéket tudunk egy lista elejére építeni.
 */
(@) infixr 5 :: a (List a) -> List a
(@) x xs = Cons x xs

/*
 * A `@` művelet lesz egyben a nagyobb listák létrehozásának módja, mivel
 * egymás után többször, rekurzívan alkalmazva fel tudunk így építeni listákat,
 * az üres listától kiindulva.  A jobbasszociativitás (`infixr`) miatt a
 * zárójeleket ilyenkor nem is kell kitenni.
 *
 * Ekkor egy jobbra torzult bináris fa jön létre:
 *
 *                 @
 *                / \
 *               5   @
 *                  / \
 *                 4   @
 *                    / \
 *                   3   @
 *                      / \
 *                     2   @
 *                        / \
 *                       1  Nil
 *
 */
sampleIntList = 5 @ 4 @ 3 @ 2 @ 1 @ Nil

/*
 * Továbbá, a `List` `Cons` konstruktorának felhasználásával meg tudjuk adni a
 * listák két alapvető műveletét: az első elem kivétele, valamint a lista
 * törzsének, vagyis az első elem kívül az összes visszaadása.  Az előbbit a
 * régi hagyományok szerint "head" vagy fejelemnek is nevezik, az utóbbit pedig
 * "tail" vagy farok-, ill. maradékrésznek.
 *
 * Látható, hogy az így megszerkesztett listák egy lineáris szervezést írnak
 * le, ahol lényegében mindig csak első elemet tudjuk elérni közvetlenül.
 * Minden további elem eléréséhez lentebb kell mennünk a listába a törzsön
 * keresztül, majd azoknak venni az első elemeit.
 *
 * Ezek a függvények parciálisak, vagyis mivel csak a `Cons` konstruktort
 * kezeltük le, üres lista esetén nem adnak vissza értéket.  Pontosabban hibát,
 * kivételt váltanak ki.
 */
hd :: (List a) -> a
hd (Cons x _) = x
hd _          = abort "hd: empty list"

tl :: (List a) -> List a
tl (Cons _ xs) = xs
tl _           = abort "tl: empty list"

/*
 * A listák sok helyen használhatóak, több különféle műveletet érhetőek el
 * hozzájuk általában.  Ezeket többnyire a lista szerkezete szerinti
 * rekurzíóval lehet megadni:
 *
 *   - `sum`: számokat tartalmazó lista elemeinek összeadása, hasonló
 *            függvény még a `product`, amely összeszorozza az elemeket,
 */
sum :: (List Int) -> Int
sum Nil         = 0
sum (Cons x xs) = x + sum xs

/*
 * Mindezek mellett létrehozhatóak ún. felsorolásos típusok is.  Ekkor
 * egységtípusok összegeként közvetlenül felsoroljuk a típus lehetséges
 * értékeit mint adatkonstruktorkat.
 *
 * Erre példa a logikai értékeket ábrázoló `Bool` típus, ahol pontosan
 * két elem létezik, amelyek a `True` és `False` literálok.
 */
:: Bool = True | False

(||) infixr 3 :: Bool Bool -> Bool
(||) False False = False
(||) _     _     = True

sampleBoolList = True @ False @ True @ False @ Nil

/*
 *   - `or`: logikai értékeket tartalmazó lista elemeinek diszjunkciója,
 *           hasonló függvény az `and`, amely konjunkciót számol,
 */
or :: (List Bool) -> Bool
or Nil         = False
or (Cons x xs) = x || (or xs)

/*
 *   - `++`: két lista összefűzése, pontosabban a második lista hozzáfűzése
 *           az első végéhez, ezért ennek futása annak hosszával arányos,
 */
(++) infixr 5 :: (List a) (List a) -> List a
(++) Nil         ys = ys
(++) (Cons x xs) ys = x @ (xs ++ ys)

/*
 *   - `flatten`: listák összefűzése, lényegében a `++` művelet kiterjesztése
 *                listákra,
 */
flatten :: (List (List a)) -> List a
flatten Nil         = Nil
flatten (Cons x xs) = x ++ (flatten xs)

/*
 *   - `length`: listában levő elemek meghatározása, a hossz lemérése,
 */
listLength :: (List a) -> Int
listLength Nil         = 0
listLength (Cons _ xs) = 1 + listLength xs

/*
 * Észrevehetjük azonban, hogy a fentebb megadott függvénydefiníciók
 * hasonlítanak egymásra, felírhatóak a következő sémával:
 *
 *     f Nil         = z
 *     f (Cons x xs) = g x (f xs)
 *
 * ahol `z` a `Nil` esethez rendelt érték, `g` pedig a fej és a törzsre
 * (rekurzívan) kiszámított függvényérték kombinációja.  A `g` lényegében egy
 * jobbasszociatív bináris művelet.
 *
 * Vizuálisan úgy képzelhetjük el például a `sum` függvény esetén, hogy a
 * listát záró `Nil` értéket kicseréljük a `0` konstansra, a listaelemeket
 * elválasztó `@` operátorokat a `+` műveletére:
 *
 *     5 @ 4 @ 3 @ 2 @ 1 @ Nil
 *       |   |   |   |   |  |
 *       ˇ   ˇ   ˇ   ˇ   ˇ  ˇ
 *     5 + 4 + 3 + 2 + 1 +  0
 *
 * Ezt a sémát fogja meg a `foldr` avagy "fold right" függvény.  Ez lefordítva
 * azt jelenti, hogy "hajtogatás jobbra".  Ez arra utal, hogy a lista elemeit
 * balról jobbra lépésenként összekombináljuk egy jobbasszociatív binér
 * művelettel és ebből képzünk egy teljesen új értéket.  Erre utal a típusban a
 * `b` típusváltozó.  A binér függvényünk azért mindig egy ugyanilyen, `b`
 * típusú értéket fog gyártani, végighajtogatni a lista feldolgozása közben.
 */
foldr :: (a b -> b) b (List a) -> b
foldr f z Nil         = z
foldr f z (Cons x xs) = f x (foldr f z xs)

/*
 * A `foldr` alkalmazásával az eddigi függvényeinket így tudjuk megadni:
 *
 *     sum xs     = foldr (+) 0 xs
 *     or xs      = foldr (||) False xs
 *     (++) xs ys = foldr (@) ys xs
 *     flatten xs = foldr (++) Nil xs
 *     length xs  = foldr (\_ n -> 1 + n) 0 xs
 */

/*
 * Ha készítünk egy olyan függvényt, amely szövegként ábrázolja a binér művelet
 * egy alkalmazását, a `#` karakterrel jelölve az operátort infix formában,
 * látható is a `foldr` működése.  A függvény lépésenkénti kiértékelését az
 * alábbi oldalon megnézhetjük (Haskell nyelven, de a lényege ugyanaz):
 *
 *     https://stevekrouse.github.io/hs.js/
 */
vizualize x y = "(" +++ toString x +++ " # " +++ toString y +++ ")"

vizualizeFoldr = foldr vizualize "X" sampleIntList

/*
 * Ha viszont olyan függvényt akarunk készíteni, amely megfordítja ez lista
 * elemeinek sorrendjét, akkor a "fold right" séma alkalmazása nem feltétlenül
 * lesz hatékony.  Ilyenkor ugyanis az elemeket nem jó sorrendben kapnánk, így
 * csak úgy tudnánk megadni a definíciót, ha a beérkező elemeket mindig a
 * hajtogatás eredményeként készülő listához fűznénk.
 *
 * Helyette egy gyorsabb megoldást választunk, ahol egy segédfüggvénnyel azt
 * valósítjuk meg, hogy a listából kivett elemeket egy másik lista elejére
 * építjük be.  Néhány lépést ábrázolva:
 *
 *     1 @ 2 @ 3 @ Nil       Nil
 *     2 @ 3 @ Nil      -->  1 @ Nil
 *     3 @ Nil          -->  2 @ 1 @ Nil
 *     Nil              -->  3 @ 2 @ 1 @ Nil
 *
 * Érdemes megjegyezni, hogy a listák ábrázolása miatt ilyenkor az elemeket
 * magukat nem másoljuk le, hanem egy másik vázat szerkesztünk a listához.  Ezt
 * nevezik "boxed" ábrázolásnak, amikor az elemek nem a vázban helyezkednek el,
 * hanem azon kívül.
 */
reverse :: (List a) -> List a
reverse xs = f xs Nil
  where
    f Nil         ys = ys
    f (Cons x xs) ys = f xs (x @ ys)

/*
 * Viszont nem kell feladnunk a hajtogatáshoz megismert sémát, mivel lehet
 * definiálni egy "fold left", avagy `foldl` műveletet is.  Itt egy
 * balasszociatív művelet segítségével hajtogatjuk jobbról balra a listát.
 */
foldl :: (b a -> b) b (List a) -> b
foldl f z Nil         = z
foldl f z (Cons x xs) = foldl f (f z x) xs

/*
 * A `reverse` így adható meg a `foldl` alkalmazásával:
 *
 *     reverse xs = foldl (\xs x -> x @ xs) Nil xs
 */

/*
 * A viselkedését a korábban megadott `vizualize` függvény segítségével tudjuk
 * ábrázolni.
 */
vizualizeFoldl = foldl vizualize "X" sampleIntList

/*
 * A "fold left" azonban nem tud végtelen listákkal lustán dolgozni, mivel
 * ahhoz, hogy el tudja végezni a hajtogatást, először lényegében a lista
 * végére kell tudnia mennie.
 *
 * Ezt a legegyszerűbben úgy lehet szemléltetni, készítünk egy végtelen
 * listát, például az `iterate` segítségével.  Az `iterate` egy végtelen
 * rekurziót valósít meg, ahol a függvény segítségével egy kezdőelemből
 * indulva, azt folyamatosan változtatja.
 */
iterate :: (a -> a) a -> (List a)
iterate f x = x @ iterate f (f x)

/*
 * Például így lehet az `iterate` segítségével természetesen számok nullától
 * induló végtelen sorozatát előállítani.
 */
infiniteIntList = iterate inc 0
  where inc x = x + 1

foldrExample = (foldr (\x xs -> (x + 1) @ xs) Nil infiniteIntList)

/*
 * Bizonyos esetekben hasznos lehet még, ha megköveteljük, hogy legalább egy
 * eleme legyen a listánknak.  Például ilyen a lista legkisebb elemét megkereső
 * `minimum` függvény definíciója:
 */
minimum :: (List a) -> a | < a
minimum Nil          = abort "minimum: empty list"
minimum (Cons x Nil) = x
minimum (Cons x xs)  = min x (minimum xs)
  where
    min a b
      | a < b     = a
      | otherwise = b

/*
 * Ilyenkor a hajtogató függvényeknek megadható egy olyan változata, amely a
 * hajtogatást a lista első elemével inicializálja.  Ennek egy következménye,
 * hogy az elemek közti binér művelet ilyenkor mindig csak azonos típusú
 * operandusokkal dolgozhat, illetve a nekik megfelelő értéket állíthatja elő.
 */
foldr1 :: (a a -> a) (List a) -> a
foldr1 f (Cons x xs) = foldr f x xs
foldr1 _ _           = abort "foldr: empty list"

/*
 * A `minimum` így adható meg a `foldr1` alkalmazásával:
 *
 *     minimum xs = foldr1 (\x y -> if (x < y) x y) xs
 */

minimumExample = (minimum sampleIntList)

/*
 * Érdemes megjegyezni, hogy a hajtogatás művelete kiterjeszhető akár más
 * rekurzív adattípusokra is, mint például a bináris fákat ábrázoló `Tree`
 * típusra:
 *
 *     Tree :: * -> *
 */
:: Tree a = Leaf | Node a (Tree a) (Tree a)

sampleTree = Node 1 (Node 2 Leaf (Node 3 Leaf Leaf)) (Node 4 Leaf Leaf)

foldTree :: (a b b -> b) b (Tree a) -> b
foldTree f z Leaf         = z
foldTree f z (Node x l r) = f x (foldTree f z l) (foldTree f z r)

/*
 * Így megadható a fákra vonatkozó hosszmérés, a fa méretének meghatározása.
 */
treeSize :: (Tree a) -> Int
treeSize t = foldTree (\_ s1 s2 -> 1 + s1 + s2) 0 t

treeSizeExample = treeSize sampleTree

/*
 * Hajtogatások segítségével kulcs-érték párok listájában végzett lineáris
 * keresést is le tudunk írni.  A párokat a `Pair` szorzattípussal tudjuk
 * ábrázolni:
 *
 *     Pair :: * -> * -> *
 */
:: Pair a b = Pair a b

/*
 * Hasonlóan a listákhoz, itt is készíthetünk egy operátort, amellyel listákat
 * tudunk létrehozni.
 */
($) infixr 9 :: a b -> Pair a b
($) x y = Pair x y

/*
 * Valamint be tudjuk vezetni a párok két jellemző műveletét: az `fst`
 * segítségével a pár első elemét lehet kivenni, az `snd` segítségével pedig
 * a második elemét.
 */
fst :: (Pair a b) -> a
fst (Pair x _) = x

snd :: (Pair a b) -> b
snd (Pair _ y) = y

/*
 * A kulcs-érték párok létrehozásához definiáljuk még a `zip2` függvényt, amely
 * két listából készít egy párokból álló listát.  Ezt nevezik cipzározásnak,
 * mivel ilyenkor a két listát egyszerre járjuk be, és az azonos indexeken levő
 * értékekből építünk párokat.
 *
 *     x_1     x_2     x_3     x_4 ...     x_k
 *     |       |       |       |           |
 *     ˇ       ˇ       ˇ       ˇ           ˇ
 *     x_1,y_1 x_2,y_2 x_3,y_3 x_4,y_4     x_k,y_k
 *         ^       ^       ^       ^           ^
 *         |       |       |       |           |
 *         y_1     y_2     y_3     y_4 ...     y_k y_(k + 1)
 *
 * Ennek egyik következménye, hogy ha az egyik listából már elfogytak az elemek,
 * akkor több párt nem tudunk létrehozni, ezért a cipzározás befejeződik.  Így
 * akár végtelen listákkal is cipzározhatunk az egyik pozícióban.
 */
zip2 :: (List a) (List b) -> List (Pair a b)
zip2 (Cons x xs) (Cons y ys) = (x $ y) @ zip2 xs ys
zip2 _           _           = Nil

keyValueList = zip2 infiniteIntList ('a' @ 'b' @ 'c' @ 'd' @ Nil)

/*
 * Végül magát a keresést a `lookup` függvény segítségével implementáljuk,
 * amely a `Maybe` típusra építkezik.  Ezzel fejezzük ki azt is, amikor a
 * keresett nem találjuk a sorozatban.
 *
 * A `Maybe` egy olyan paraméteres típus, amely egy már meglevő típust
 * egészít ki olyan elemmel, amely már nem tagja annak.
 *
 * .--------------------.
 * | Maybe a            |
 * |.-------.   Nothing |
 * ||   a   |    (+ 1)  |
 * |'-------'           |
 * '--------------------'
 *
 * Ez így tulajdonképpen egy séma, ezért alkalmazunk típusváltozót, ahol
 * mindig beírhatjuk azt a típust, amelyik ki akarjuk egészíteni:
 *
 * Maybe Char ~= Just Char | Nothing
 * Maybe Int  ~= Just Int  | Nothing
 * és így tovább...
 *
 * Az értékhalmazok pedig ennek megfelelően alakulnak:
 *
 * Maybe Int  = { Nothing, Just 0, Just (-1), Just 1, Just (-2), Just 2, ... }
 * Maybe Char = { Nothing, Just 'a', Just 'b', Just 'c', ... }
 *
 * Ennek egy következménye, hogy a `Nothing` így tulajdonképpen egy polimorf
 * literál lesz, mivel több, a `Maybe` segítségével képzett típusnak is az
 * eleme lesz.  Ebben a tekintetben hasonlóan viselkedik az üres listához.
 */
:: Maybe a = Just a | Nothing

lookup :: a (List (Pair a b)) -> Maybe b | == a
lookup e xs = foldr (\p r -> if (e == (fst p)) (Just (snd p)) r) Nothing xs

maybeExample = (keyValueList, lookup 3 keyValueList)

/*
 * Paraméter nélküli rekurzív típusra a `Nat` lehet egy példa.  Ennek
 * segítségével természetes számokat ábrázolunk a Peano-axiómák szerint.
 * Láthatjuk, hogy a következő konstruktoraink vannak:
 *
 *   Zero :: Nat          // literál, 0
 *   Succ :: Nat -> Nat   // függvény, S
 */
:: Nat = Zero | Succ Nat

/*
 * Érdemes megjegyezni, hogy a típus leírása felfogható egy generatív
 * nyelvtannak is, ahol az értékek szabályos összeállításának módját,
 * vagyis lényegében szintaktikáját adjuk meg.
 *
 *   N -> '0'
 *   N -> 'S'N
 *
 * Ezáltal az értékek alábbi nyelvét generáljuk:
 *
 * Nat = { Zero, Succ Zero, Succ (Succ Zero), Succ (Succ (Succ Zero)), ... }
 */
aNat :: Nat
aNat = Succ (Succ (Succ Zero))  //  S (S (S 0))

/*
 * Ezeket az értékeket adatkonstruktorokkal hoztuk létre.  Ezek elsőre olyanok,
 * mint a függvények: rendelkeznek adott típussal és azok helyes
 * felparaméterezésével létrehozzuk a végeredmény típusának megfelelő értéket.
 * Ekkor viszont hasznos látni, hogy redukálás nem történik, vagyis ekkor
 * már eleve normálformában levő értékeket (literálokat) készítünk.
 *
 * Ennek egy következménye, hogy az így létrehozott értékeket viszont
 * interpretálni kell ahhoz, hogy valóban számként tudjanak funkcionálni.
 * Tehát készíteni kell egy olyan rekurzív függvényt, amely megadja, hogy az
 * adott szintaktikával rendelkező érték milyen számnak felel meg a
 * rendszerünkben.  Ez lesz a szintaktikához tartozó szemantika, pontosabban
 * annak denotációs szemantikája.
 *
 * Ezzel kapcsolatban meg lehet figyelni azt is, hogy az ilyenkor megírandó
 * függvény szerkezete szorosan követi a típus definícióját.  Lényegében
 * minden egyes konstruktorra mintaillesztést végzünk és annak megfelelő
 * leírjuk, milyen értéket társítunk hozzá.  Ha rekurzív a típus, akkor a
 * függvény is rekurzív lesz azokon a pontokon.
 */
fromNat :: Nat -> Int
fromNat Zero     = 0
fromNat (Succ n) = 1 + fromNat n

natTest = fromNat aNat

Start = 42