<commit_before>module Main where

import Data.Char
import SIL


just_abort = Anno (Lam (CI Zero)) (Pair Zero Zero)

message_then_abort = Anno (Lam (CI (ITE (Var Zero) Zero (Pair (s2g "Test message") Zero)))) (Pair Zero Zero)

quit_to_exit =
  let check_input = ITE (App (App list_equality (CI . PLeft $ Var Zero)) (CI $ s2g "quit"))
                    Zero
                    (Pair (s2g "type quit to exit") (i2g 1))
  in Anno (Lam (CI check_input)) (Pair Zero Zero)

three_succ = App (App (Anno (toChurch 3) (Pair (Pair Zero Zero) (Pair Zero Zero)))
                  (Lam (CI (Pair (Var Zero) Zero))))
             (CI Zero)

church_type = Pair (Pair Zero Zero) (Pair Zero Zero)

c2d = Anno (Lam (CI (App (App (Var Zero) (Lam (CI (Pair (Var Zero) Zero)))) (CI Zero))))
  (Pair church_type Zero)

h2c i =
  let layer recurf i churchf churchbase =
        if i > 0
        then churchf $ recurf (i - 1) churchf churchbase
        -- App v1 (App (App (App v3 (PLeft v2)) v1) v0)
        else churchbase
      stopf i churchf churchbase = churchbase
  in \cf cb -> layer (layer (layer (layer stopf))) i cf cb


{-
h_zipWith a b f =
  let layer recurf zipf a b =
        if a > 0
        then if b > 0
             then Pair (zipf (PLeft a) (PLeft b)) (recurf zipf (PRight a) (PRight b))
             else Zero
        else Zero
      stopf _ _ _ = Zero
  in layer (layer (layer (layer stopf))) a b f

foldr_h =
  let layer recurf f accum l =
        if not $ nil l
        then recurf f (f (PLeft l) accum) (PRight l)
        else accum
-}

fixl l base layer layerType  =
  let inner 0 = Var Zero
      inner x = App (Var $ i2g 1) (CI $ inner (x - 1))
      nested = Lam (Lam (CI $ inner l))
      fixType = Pair (Pair layerType layerType) (Pair layerType layerType)
  in App (App (Anno nested fixType) layer) base

map_ =
  -- layer recurf f l = Pair (f (PLeft l)) (recurf f (PRight l))
  let layer = Lam (Lam (Lam (CI
                            (ITE (Var Zero)
                            (Pair
                             (App (Var $ i2g 1) (CI . PLeft $ Var Zero))
                             (App (App (Var $ i2g 2) (CI . Var $ i2g 1))
                              (CI . PRight $ Var Zero)))
                            Zero
                            ))))
      layerType = Pair (Pair Zero Zero) (Pair Zero Zero)
      base = Lam (Lam (CI Zero))
  in fixl 255 base layer layerType

foldr_ =
  let layer = Lam (Lam (Lam (Lam (CI
                                 (ITE (Var $ i2g 0)
                                 (App (App (App (Var $ i2g 3) (CI . Var $ i2g 2))

                                       (CI (App (App (Var $ i2g 2) (CI . PLeft . Var $ i2g 0))
                                            (CI . Var $ i2g 1))))
                                  (CI . PRight . Var $ i2g 0))
                                 (Var $ i2g 1)
                                 )
                                 ))))
      layerType = Pair (Pair Zero (Pair Zero Zero)) (Pair Zero (Pair Zero Zero))
      base = Lam (Lam (Lam (CI Zero))) -- var 0?
  in fixl 255 base layer layerType

zipWith_ =
  let layer = Lam (Lam (Lam (Lam (CI
                                  (ITE (Var $ i2g 1)
                                   (ITE (Var $ i2g 0)
                                    (Pair
                                     (App (App (Var $ i2g 2) (CI . PLeft . Var $ i2g 1))
                                      (CI . PLeft . Var $ i2g 0))
                                     (App (App (App (Var $ i2g 3) (CI . Var $ i2g 2))
                                           (CI . PRight . Var $ i2g 1))
                                      (CI . PRight . Var $ i2g 0))
                                    )
                                    Zero)
                                   Zero)
                                 ))))
      base = Lam (Lam (Lam (CI Zero)))
      layerType = Pair (Pair Zero (Pair Zero Zero)) (Pair Zero (Pair Zero Zero))
  in fixl 255 base layer layerType

-- layer recurf i churchf churchbase
-- layer :: (Zero -> baseType) -> Zero -> (baseType -> baseType) -> baseType
--           -> baseType
-- converts plain data type number (0-255) to church numeral
d2c baseType =
  let layer = Lam (Lam (Lam (Lam (CI (ITE
                             (Var $ i2g 2)
                             (App (Var $ i2g 1)
                              (CI (App (App (App (Var $ i2g 3)
                                   (CI . PLeft . Var $ i2g 2))
                                   (CI . Var $ i2g 1))
                                   (CI . Var $ Zero)
                                  )))
                             (Var Zero)
                            )))))
      base = Lam (Lam (Lam (CI (Var Zero))))
      layerType = Pair Zero (Pair (Pair baseType baseType) (Pair baseType baseType))
  in fixl 255 base layer layerType

-- d_equality_h iexpr = (\d -> if d > 0
--                                then \x -> d_equals_one ((d2c (pleft d) pleft) x)
--                                else \x -> if x == 0 then 1 else 0
--                         )<commit_msg>removed redundant fixl<commit_after>module Main where

import Data.Char
import SIL


just_abort = Anno (Lam (CI Zero)) (Pair Zero Zero)

message_then_abort = Anno (Lam (CI (ITE (Var Zero) Zero (Pair (s2g "Test message") Zero)))) (Pair Zero Zero)

quit_to_exit =
  let check_input = ITE (App (App list_equality (CI . PLeft $ Var Zero)) (CI $ s2g "quit"))
                    Zero
                    (Pair (s2g "type quit to exit") (i2g 1))
  in Anno (Lam (CI check_input)) (Pair Zero Zero)

three_succ = App (App (Anno (toChurch 3) (Pair (Pair Zero Zero) (Pair Zero Zero)))
                  (Lam (CI (Pair (Var Zero) Zero))))
             (CI Zero)

church_type = Pair (Pair Zero Zero) (Pair Zero Zero)

c2d = Anno (Lam (CI (App (App (Var Zero) (Lam (CI (Pair (Var Zero) Zero)))) (CI Zero))))
  (Pair church_type Zero)

h2c i =
  let layer recurf i churchf churchbase =
        if i > 0
        then churchf $ recurf (i - 1) churchf churchbase
        -- App v1 (App (App (App v3 (PLeft v2)) v1) v0)
        else churchbase
      stopf i churchf churchbase = churchbase
  in \cf cb -> layer (layer (layer (layer stopf))) i cf cb


{-
h_zipWith a b f =
  let layer recurf zipf a b =
        if a > 0
        then if b > 0
             then Pair (zipf (PLeft a) (PLeft b)) (recurf zipf (PRight a) (PRight b))
             else Zero
        else Zero
      stopf _ _ _ = Zero
  in layer (layer (layer (layer stopf))) a b f

foldr_h =
  let layer recurf f accum l =
        if not $ nil l
        then recurf f (f (PLeft l) accum) (PRight l)
        else accum
-}

map_ =
  -- layer recurf f l = Pair (f (PLeft l)) (recurf f (PRight l))
  let layer = Lam (Lam (Lam (CI
                            (ITE (Var Zero)
                            (Pair
                             (App (Var $ i2g 1) (CI . PLeft $ Var Zero))
                             (App (App (Var $ i2g 2) (CI . Var $ i2g 1))
                              (CI . PRight $ Var Zero)))
                            Zero
                            ))))
      layerType = Pair (Pair Zero Zero) (Pair Zero Zero)
      fixType = Pair (Pair layerType layerType) (Pair layerType layerType)
      base = Lam (Lam (CI Zero))
  in App (App (Anno (toChurch 255) fixType) layer) base

foldr_ =
  let layer = Lam (Lam (Lam (Lam (CI
                                 (ITE (Var $ i2g 0)
                                 (App (App (App (Var $ i2g 3) (CI . Var $ i2g 2))

                                       (CI (App (App (Var $ i2g 2) (CI . PLeft . Var $ i2g 0))
                                            (CI . Var $ i2g 1))))
                                  (CI . PRight . Var $ i2g 0))
                                 (Var $ i2g 1)
                                 )
                                 ))))
      layerType = Pair (Pair Zero (Pair Zero Zero)) (Pair Zero (Pair Zero Zero))
      fixType = Pair (Pair layerType layerType) (Pair layerType layerType)
      base = Lam (Lam (Lam (CI Zero))) -- var 0?
  in App (App (Anno (toChurch 255) fixType) layer) base

zipWith_ =
  let layer = Lam (Lam (Lam (Lam (CI
                                  (ITE (Var $ i2g 1)
                                   (ITE (Var $ i2g 0)
                                    (Pair
                                     (App (App (Var $ i2g 2) (CI . PLeft . Var $ i2g 1))
                                      (CI . PLeft . Var $ i2g 0))
                                     (App (App (App (Var $ i2g 3) (CI . Var $ i2g 2))
                                           (CI . PRight . Var $ i2g 1))
                                      (CI . PRight . Var $ i2g 0))
                                    )
                                    Zero)
                                   Zero)
                                 ))))
      base = Lam (Lam (Lam (CI Zero)))
      layerType = Pair (Pair Zero (Pair Zero Zero)) (Pair Zero (Pair Zero Zero))
      fixType = Pair (Pair layerType layerType) (Pair layerType layerType)
  in App (App (Anno (toChurch 255) fixType) layer) base

-- layer recurf i churchf churchbase
-- layer :: (Zero -> baseType) -> Zero -> (baseType -> baseType) -> baseType
--           -> baseType
-- converts plain data type number (0-255) to church numeral
d2c baseType =
  let layer = Lam (Lam (Lam (Lam (CI (ITE
                             (Var $ i2g 2)
                             (App (Var $ i2g 1)
                              (CI (App (App (App (Var $ i2g 3)
                                   (CI . PLeft . Var $ i2g 2))
                                   (CI . Var $ i2g 1))
                                   (CI . Var $ Zero)
                                  )))
                             (Var Zero)
                            )))))
      base = Lam (Lam (Lam (CI (Var Zero))))
      layerType = Pair Zero (Pair (Pair baseType baseType) (Pair baseType baseType))
      fixType = Pair (Pair layerType layerType) (Pair layerType layerType)
  in App (App (Anno (toChurch 255) fixType) layer) base

-- d_equality_h iexpr = (\d -> if d > 0
--                                then \x -> d_equals_one ((d2c (pleft d) pleft) x)
--                                else \x -> if x == 0 then 1 else 0
--                         )
{'fraction_non_alphanumeric': 0.10462168486739469, 'fraction_numerical': 0.01794071762870515, 'mean_word_length': 1.1382113821138211, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 76, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4754693', 'n_tokens_mistral': 3228, 'n_tokens_neox': 2989, 'n_words': 1172}