module Library where

import Eval
import Parser
import Research

import qualified Data.Map as Map

library :: Map.Map String T
library = evalSapling Map.empty $ parseSapling $ unlines 
  [ "false = t" 
  , "true = t t"
  , "_ = t"
  , "k = t t"
  , "i = t (t k) t"
  , "s = t (t (k t)) t"
  , "m = s i i"
  , "b = s (k s) k"
  , "c = s (s (k s) (s (k k) s)) (k k)"
  , "iC = (\\a b c : s a (k c) b)"
  , "iD = b (b iC) iC"
  , "iE = b (b iD) iC"
  , "yi = (\\i : b m (c b (i m)))"
  , "y = yi iC"
  , "yC = yi iD"
  , "yD = yi iE"
  , "id = (\\a : a)"
  , "triage = (\\a b c : t (t a b) c)"
  , "pair = t"
  , "matchBool = (\\ot of : triage of (\\_ : ot) (\\_ _ : ot))"
  , "matchList = (\\oe oc : triage oe _ oc)"
  , "matchPair = (\\op : triage _ _ op)"
  , "and = matchBool id (\\z : false)"
  , "if = (\\cond then else : t (t else (t t then)) t cond)"
  , "test = triage \"leaf\" (\\z : \"stem\") (\\a b : \"fork\")"
  , "emptyList = matchList true (\\y z : false)"
  , "nonEmptyList = matchList false (\\y z : true)"
  , "head = matchList t (\\hd tl : hd)"
  , "tail = matchList t (\\hd tl : tl)"
  , "isLeaf = (\\_ : triage true false false)"
  , "listConcat = y (\\self : matchList (\\k : k) (\\h r k : pair h (self r k)))"
  , "lAnd = triage (\\x : false) (\\_ x : x) (\\_ _ x : x)"
  , "lOr = triage (\\x : x) (\\_ _ : true) (\\_ _ x : true)"
  , "hmap = y (\\self : matchList (\\f : t) (\\hd tl f : pair (f hd) (self tl f)))"
  , "map = (\\f l : hmap l f)"
  , "equal = y (\\self : triage (triage true (\\z : false) (\\y z : false)) (\\ax : triage false (self ax) (\\y z : false)) (\\ax ay : triage false (\\z : false) (\\bx by : lAnd (self ax bx) (self ay by))))" 
  ]