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
   "false = t\n \ 
  \ true = t t\n \
  \ _ = t\n \
  \ k = t t\n \
  \ i = t (t k) t\n \
  \ s = t (t (k t)) t\n \
  \ m = s i i\n \
  \ b = s (k s) k\n \
  \ c = s (s (k s) (s (k k) s)) (k k)\n \
  \ iC = (\\a b c : s a (k c) b)\n \
  \ iD = b (b iC) iC\n \
  \ iE = b (b iD) iC\n \
  \ yi = (\\i : b m (c b (i m)))\n \
  \ y = yi iC\n \
  \ yC = yi iD\n \
  \ yD = yi iE\n \
  \ id = (\\a : a)\n \
  \ triage = (\\a b c : t (t a b) c)\n \
  \ pair = t\n \
  \ matchBool = (\\ot of : triage of (\\_ : ot) (\\_ _ : ot))\n \
  \ matchList = (\\oe oc : triage oe _ oc)\n \
  \ matchPair = (\\op : triage _ _ op)\n \
  \ and = matchBool id (\\z : false)\n \
  \ if = (\\cond then else : t (t else (t t then)) t cond)\n \
  \ test = triage \"leaf\" (\\z : \"stem\") (\\a b : \"fork\")\n \
  \ emptyList = matchList true (\\y z : false)\n \
  \ nonEmptyList = matchList false (\\y z : true)\n \
  \ head = matchList t (\\hd tl : hd)\n \
  \ tail = matchList t (\\hd tl : tl)\n \
  \ isLeaf = (\\_ : triage true false false)\n \
  \ listConcat = y (\\self : matchList (\\k : k) (\\h r k : pair h (self r k)))\n \
  \ lAnd = triage (\\x : false) (\\_ x : x) (\\_ _ x : x)\n \
  \ lOr = triage (\\x : x) (\\_ _ : true) (\\_ _ x : true)\n \
  \ hmap = y (\\self : matchList (\\f : t) (\\hd tl f : pair (f hd) (self tl f)))\n \
  \ map = (\\f l : hmap l f) \n \
  \ 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))))"