<commit_before>import Modal
import Data.Map hiding (map)
import Data.Maybe (fromJust)
import Data.List (find)

type ModalProgram v a = a -> ModalFormula v
data ProgFrag v a = ProgFrag (ModalProgram v a -> ModalProgram v a)

enumerate :: Enum a => [a]
enumerate = enumFrom (toEnum 0)

progToList :: Enum a => ModalProgram v a -> [ModalFormula v]
progToList f = map f enumerate

modalProgram :: (Enum a,Eq a) => a -> ProgFrag v a -> ModalProgram v a
modalProgram dflt (ProgFrag f) = f $ \a -> Val (a == dflt)


mReturn :: Eq a => a -> ProgFrag v a
mReturn a = ProgFrag $ const $ \a' -> Val (a == a')

mPass :: ProgFrag v a
mPass = ProgFrag id

mIf' :: ModalFormula v -> ProgFrag v a -> ProgFrag v a -> ProgFrag v a
mIf' cond (ProgFrag t) (ProgFrag e) = ProgFrag $ \prog a ->
  And (Imp cond       (t prog a))
      (Imp (Neg cond) (e prog a))

mIf :: ModalFormula v -> ProgFrag v a -> ProgFrag v a
mIf cond t = mIf' cond t mPass

(>->) :: ProgFrag v a -> ProgFrag v a -> ProgFrag v a
ProgFrag f >-> ProgFrag g = ProgFrag (f . g)

mFor' :: [c] -> (c -> ProgFrag v a) -> ProgFrag v a
mFor' []     _ = mPass
mFor' (c:cs) f = f c >-> mFor' cs f

mFor :: Enum c => (c -> ProgFrag v a) -> ProgFrag v a
mFor = mFor' enumerate


evalProgram :: (Ord a,Show a,Read a,Enum a) => ModalProgram a a -> a
evalProgram prog = fst $ fromJust $ find snd $ Data.Map.toList $
  findGeneralGLFixpoint $ Data.Map.fromList $
    flip map enumerate $ \a -> (a, prog a)


udt :: (Enum a,Ord b,Show b,Enum b)
    => Int -> ModalProgram b a -> b -> ModalProgram b b
udt level univ dflt = modalProgram dflt $
  mFor $ \a ->
    mFor $ \b ->
      mIf (boxk level (Var b %> univ a)) (mReturn b)

evalUDT :: (Enum a,Ord b,Show b,Read b,Enum b)
        => Int -> ModalProgram b a -> b -> b
evalUDT level univ dflt = evalProgram $ udt level univ dflt


data FiveOrTen = Ten | Five deriving (Eq,Ord,Show,Read,Enum)

fiveAndTen :: ModalProgram FiveOrTen FiveOrTen
fiveAndTen Five = Var Five
fiveAndTen Ten = Var Ten


data NewcombAction = OneBox | TwoBox deriving (Eq,Ord,Show,Read,Enum)
data NewcombOutcome = MillionThousand | Million | Thousand | Naught
  deriving (Eq,Ord,Show,Read,Enum)

onebox = Var OneBox
twobox = Neg onebox

newcomb :: Int -> ModalProgram NewcombAction NewcombOutcome
newcomb k MillionThousand = twobox %^      boxk k onebox
newcomb k Million         = onebox %^      boxk k onebox
newcomb k Thousand        = twobox %^ Neg (boxk k onebox)
newcomb k Naught          = onebox %^ Neg (boxk k onebox)


main = do
  print $ evalUDT 0 fiveAndTen Five
  print $ evalUDT 0 (newcomb 0) OneBox
  print $ udt 0 (newcomb 0) OneBox OneBox
<commit_msg>add some explanatory text in the output<commit_after>import Modal
import Data.Map hiding (map)
import Data.Maybe (fromJust)
import Data.List (find)

type ModalProgram v a = a -> ModalFormula v
data ProgFrag v a = ProgFrag (ModalProgram v a -> ModalProgram v a)

enumerate :: Enum a => [a]
enumerate = enumFrom (toEnum 0)

progToList :: Enum a => ModalProgram v a -> [ModalFormula v]
progToList f = map f enumerate

modalProgram :: (Enum a,Eq a) => a -> ProgFrag v a -> ModalProgram v a
modalProgram dflt (ProgFrag f) = f $ \a -> Val (a == dflt)


mReturn :: Eq a => a -> ProgFrag v a
mReturn a = ProgFrag $ const $ \a' -> Val (a == a')

mPass :: ProgFrag v a
mPass = ProgFrag id

mIf' :: ModalFormula v -> ProgFrag v a -> ProgFrag v a -> ProgFrag v a
mIf' cond (ProgFrag t) (ProgFrag e) = ProgFrag $ \prog a ->
  And (Imp cond       (t prog a))
      (Imp (Neg cond) (e prog a))

mIf :: ModalFormula v -> ProgFrag v a -> ProgFrag v a
mIf cond t = mIf' cond t mPass

(>->) :: ProgFrag v a -> ProgFrag v a -> ProgFrag v a
ProgFrag f >-> ProgFrag g = ProgFrag (f . g)

mFor' :: [c] -> (c -> ProgFrag v a) -> ProgFrag v a
mFor' []     _ = mPass
mFor' (c:cs) f = f c >-> mFor' cs f

mFor :: Enum c => (c -> ProgFrag v a) -> ProgFrag v a
mFor = mFor' enumerate


evalProgram :: (Ord a,Show a,Read a,Enum a) => ModalProgram a a -> a
evalProgram prog = fst $ fromJust $ find snd $ Data.Map.toList $
  findGeneralGLFixpoint $ Data.Map.fromList $
    flip map enumerate $ \a -> (a, prog a)


udt :: (Enum a,Ord b,Show b,Enum b)
    => Int -> ModalProgram b a -> b -> ModalProgram b b
udt level univ dflt = modalProgram dflt $
  mFor $ \a ->
    mFor $ \b ->
      mIf (boxk level (Var b %> univ a)) (mReturn b)

evalUDT :: (Enum a,Ord b,Show b,Read b,Enum b)
        => Int -> ModalProgram b a -> b -> b
evalUDT level univ dflt = evalProgram $ udt level univ dflt


data FiveOrTen = Ten | Five deriving (Eq,Ord,Show,Read,Enum)

fiveAndTen :: ModalProgram FiveOrTen FiveOrTen
fiveAndTen Five = Var Five
fiveAndTen Ten = Var Ten


data NewcombAction = OneBox | TwoBox deriving (Eq,Ord,Show,Read,Enum)
data NewcombOutcome = MillionThousand | Million | Thousand | Naught
  deriving (Eq,Ord,Show,Read,Enum)

onebox = Var OneBox
twobox = Neg onebox

newcomb :: Int -> ModalProgram NewcombAction NewcombOutcome
newcomb k MillionThousand = twobox %^      boxk k onebox
newcomb k Million         = onebox %^      boxk k onebox
newcomb k Thousand        = twobox %^ Neg (boxk k onebox)
newcomb k Naught          = onebox %^ Neg (boxk k onebox)


main = do
  putStrLn "UDT takes 5 in the 5-and-10 problem:"
  print $ evalUDT 0 fiveAndTen Five
  putStrLn ""
  putStrLn "In Newcomb's problem, if the predictor uses a box to predict"
  putStrLn "the agent's action, UDT takes whatever its default action was:"
  print $ evalUDT 0 (newcomb 0) OneBox
  print $ evalUDT 0 (newcomb 0) TwoBox
  putStrLn ""
  putStrLn "This is the modal formula that's true if UDT one-boxes:"
  print $ udt 0 (newcomb 0) OneBox OneBox

{'fraction_non_alphanumeric': 0.11645299145299146, 'fraction_numerical': 0.003205128205128205, 'mean_word_length': 3.0910415149308084, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 97, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6829236', 'n_tokens_mistral': 2189, 'n_tokens_neox': 2110, 'n_words': 784}