{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module Dataize (morph, dataize, dataize', DataizeContext (..), defaultDataizeContext) where

import Ast
import Builder (contextualize)
import Condition (isNF)
import Control.Exception (throwIO)
import Data.List (partition)
import Misc
import Rewriter (RewriteContext (RewriteContext), rewrite')
import Text.Printf (printf)
import XMIR (XmirContext (XmirContext))
import Yaml (normalizationRules)

data DataizeContext = DataizeContext
  { DataizeContext -> Program
program :: Program,
    DataizeContext -> Integer
maxDepth :: Integer
  }

defaultDataizeContext :: Program -> DataizeContext
defaultDataizeContext :: Program -> DataizeContext
defaultDataizeContext Program
prog = Program -> Integer -> DataizeContext
DataizeContext Program
prog Integer
25

switchContext :: DataizeContext -> RewriteContext
switchContext :: DataizeContext -> RewriteContext
switchContext DataizeContext {Integer
Program
program :: DataizeContext -> Program
maxDepth :: DataizeContext -> Integer
program :: Program
maxDepth :: Integer
..} = Program -> Integer -> RewriteContext
RewriteContext Program
program Integer
maxDepth

maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])
maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])
maybeBinding Binding -> Bool
_ [] = (Maybe Binding
forall a. Maybe a
Nothing, [])
maybeBinding Binding -> Bool
func [Binding]
bds =
  let ([Binding]
found, [Binding]
rest) = (Binding -> Bool) -> [Binding] -> ([Binding], [Binding])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Binding -> Bool
func [Binding]
bds
   in case [Binding]
found of
        [Binding
bd] -> (Binding -> Maybe Binding
forall a. a -> Maybe a
Just Binding
bd, [Binding]
rest)
        [Binding]
_ -> (Maybe Binding
forall a. Maybe a
Nothing, [Binding]
bds)

maybeLambda :: [Binding] -> (Maybe Binding, [Binding])
maybeLambda :: [Binding] -> (Maybe Binding, [Binding])
maybeLambda = (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])
maybeBinding (\case BiLambda String
_ -> Bool
True; Binding
_ -> Bool
False)

maybeDelta :: [Binding] -> (Maybe Binding, [Binding])
maybeDelta :: [Binding] -> (Maybe Binding, [Binding])
maybeDelta = (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])
maybeBinding (\case BiDelta String
_ -> Bool
True; Binding
_ -> Bool
False)

maybePhi :: [Binding] -> (Maybe Binding, [Binding])
maybePhi :: [Binding] -> (Maybe Binding, [Binding])
maybePhi = (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])
maybeBinding (\case (BiTau Attribute
AtPhi Expression
_) -> Bool
True; Binding
_ -> Bool
False)

formation :: [Binding] -> DataizeContext -> IO (Maybe Expression)
formation :: [Binding] -> DataizeContext -> IO (Maybe Expression)
formation [Binding]
bds DataizeContext
ctx = do
  let (Maybe Binding
lambda, [Binding]
bds') = [Binding] -> (Maybe Binding, [Binding])
maybeLambda [Binding]
bds
  case Maybe Binding
lambda of
    Just (BiLambda String
func) -> do
      Maybe Expression
obj' <- String -> Expression -> DataizeContext -> IO (Maybe Expression)
atom String
func ([Binding] -> Expression
ExFormation [Binding]
bds') DataizeContext
ctx
      case Maybe Expression
obj' of
        Just Expression
obj -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
obj)
        Maybe Expression
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
    Maybe Binding
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing

phiDispatch :: String -> Expression -> Maybe Expression
phiDispatch :: String -> Expression -> Maybe Expression
phiDispatch String
attr Expression
expr = case Expression
expr of
  ExFormation [Binding]
bds -> [Binding] -> Maybe Expression
boundExpr [Binding]
bds
  Expression
_ -> Maybe Expression
forall a. Maybe a
Nothing
  where
    boundExpr :: [Binding] -> Maybe Expression
    boundExpr :: [Binding] -> Maybe Expression
boundExpr [] = Maybe Expression
forall a. Maybe a
Nothing
    boundExpr (Binding
bd : [Binding]
bds) = case Binding
bd of
      BiTau (AtLabel String
attr') Expression
expr' -> if String
attr' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
attr then Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
expr' else [Binding] -> Maybe Expression
boundExpr [Binding]
bds
      Binding
_ -> [Binding] -> Maybe Expression
boundExpr [Binding]
bds

withTail :: Expression -> DataizeContext -> IO (Maybe Expression)
withTail :: Expression -> DataizeContext -> IO (Maybe Expression)
withTail (ExApplication (ExFormation [Binding]
_) Binding
_) DataizeContext
_ = Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
withTail (ExApplication (ExDispatch Expression
ExGlobal Attribute
_) Binding
_) DataizeContext
_ = Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
withTail (ExApplication Expression
expr Binding
tau) DataizeContext
ctx = do
  Maybe Expression
exp' <- Expression -> DataizeContext -> IO (Maybe Expression)
withTail Expression
expr DataizeContext
ctx
  case Maybe Expression
exp' of
    Just Expression
exp -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Binding -> Expression
ExApplication Expression
exp Binding
tau))
    Maybe Expression
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
withTail (ExDispatch (ExFormation [Binding]
bds) Attribute
attr) DataizeContext
ctx = do
  Maybe Expression
obj' <- [Binding] -> DataizeContext -> IO (Maybe Expression)
formation [Binding]
bds DataizeContext
ctx
  case Maybe Expression
obj' of
    Just Expression
obj -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Attribute -> Expression
ExDispatch Expression
obj Attribute
attr))
    Maybe Expression
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
withTail (ExFormation [Binding]
bds) DataizeContext
ctx = [Binding] -> DataizeContext -> IO (Maybe Expression)
formation [Binding]
bds DataizeContext
ctx
withTail (ExDispatch (ExDispatch Expression
ExGlobal (AtLabel String
label)) Attribute
attr) (DataizeContext {program :: DataizeContext -> Program
program = Program Expression
expr}) = case String -> Expression -> Maybe Expression
phiDispatch String
label Expression
expr of
  Just Expression
obj -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Attribute -> Expression
ExDispatch Expression
obj Attribute
attr))
  Maybe Expression
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
withTail (ExDispatch Expression
ExGlobal (AtLabel String
label)) (DataizeContext {program :: DataizeContext -> Program
program = Program Expression
expr}) = Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Expression -> Maybe Expression
phiDispatch String
label Expression
expr)
withTail (ExDispatch Expression
expr Attribute
attr) DataizeContext
ctx = do
  Maybe Expression
exp' <- Expression -> DataizeContext -> IO (Maybe Expression)
withTail Expression
expr DataizeContext
ctx
  case Maybe Expression
exp' of
    Just Expression
exp -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Attribute -> Expression
ExDispatch Expression
exp Attribute
attr))
    Maybe Expression
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
withTail Expression
_ DataizeContext
_ = Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing

-- The Morphing function M:<B,S> -> <P,S> maps objects to
-- primitives, possibly modifying the state of evaluation.
-- Terminology:
-- P(e) - is e Primitive, which is either formation without λ binding or termination ⊥
-- N(e) - normalize e
-- NF(e) - is e in normal form (can't be normalized anymore)
--
-- PRIM:   M(e) -> e                              if P(e)
-- NMZ:    M(e1) -> M(e2)                         if e2 := N(e1) and e1 != e2
-- LAMBDA: M([B1, λ -> F, B2] * t) -> M(e2 * t)   if e3 := [B1,B2] and e2 := F(e3)
-- PHI:    M(Q.tau * t) -> M(e * t)               if Q -> [B1, tau -> e, B2], t is tail started with dispatch
--         M(e) -> nothing                        otherwise
morph :: Expression -> DataizeContext -> IO (Maybe Expression)
morph :: Expression -> DataizeContext -> IO (Maybe Expression)
morph Expression
ExTermination DataizeContext
_ = Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
ExTermination) -- PRIM
morph (ExFormation [Binding]
bds) DataizeContext
ctx = do
  Maybe Expression
resolved <- Expression -> DataizeContext -> IO (Maybe Expression)
withTail ([Binding] -> Expression
ExFormation [Binding]
bds) DataizeContext
ctx
  case Maybe Expression
resolved of
    Just Expression
obj -> Expression -> DataizeContext -> IO (Maybe Expression)
morph Expression
obj DataizeContext
ctx -- LAMBDA or PHI
    Maybe Expression
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just ([Binding] -> Expression
ExFormation [Binding]
bds)) -- PRIM
morph Expression
expr DataizeContext
ctx = do
  Maybe Expression
resolved <- Expression -> DataizeContext -> IO (Maybe Expression)
withTail Expression
expr DataizeContext
ctx
  case Maybe Expression
resolved of
    Just Expression
obj -> Expression -> DataizeContext -> IO (Maybe Expression)
morph Expression
obj DataizeContext
ctx
    Maybe Expression
_ ->
      if Expression -> Bool
isNF Expression
expr
        then Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
        else do
          (Program Expression
expr') <- Program -> [Rule] -> RewriteContext -> IO Program
rewrite' (Expression -> Program
Program Expression
expr) [Rule]
normalizationRules (DataizeContext -> RewriteContext
switchContext DataizeContext
ctx) -- NMZ
          Expression -> DataizeContext -> IO (Maybe Expression)
morph Expression
expr' DataizeContext
ctx

-- The goal of 'dataize' function is retrieve bytes from given expression.
--
-- DELTA: D(e) -> data                          if e = [B1, Δ -> data, B2]
-- BOX:   D([B1, 𝜑 -> e, B2]) -> D(С(e))        if [B1,B2] has no delta/lambda, where С(e) - contextualization
-- NORM:  D(e1) -> D(e2)                        if e2 := M(e1) and e1 is not primitive
--        nothing                               otherwise
dataize :: Program -> DataizeContext -> IO (Maybe String)
dataize :: Program -> DataizeContext -> IO (Maybe String)
dataize (Program Expression
expr) = Expression -> DataizeContext -> IO (Maybe String)
dataize' Expression
expr

dataize' :: Expression -> DataizeContext -> IO (Maybe String)
dataize' :: Expression -> DataizeContext -> IO (Maybe String)
dataize' Expression
ExTermination DataizeContext
_ = Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
dataize' (ExFormation [Binding]
bds) DataizeContext
ctx = case [Binding] -> (Maybe Binding, [Binding])
maybeDelta [Binding]
bds of
  (Just (BiDelta String
bytes), [Binding]
_) -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
bytes)
  (Maybe Binding
Nothing, [Binding]
_) -> case [Binding] -> (Maybe Binding, [Binding])
maybePhi [Binding]
bds of
    (Just (BiTau Attribute
AtPhi Expression
expr), [Binding]
bds') -> case [Binding] -> (Maybe Binding, [Binding])
maybeLambda [Binding]
bds' of
      (Just (BiLambda String
_), [Binding]
_) -> IOError -> IO (Maybe String)
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"The 𝜑 and λ can't be present in formation at the same time")
      (Maybe Binding
_, [Binding]
_) ->
        let expr' :: Expression
expr' = Expression -> Expression -> Program -> Expression
contextualize Expression
expr ([Binding] -> Expression
ExFormation [Binding]
bds) (DataizeContext -> Program
program DataizeContext
ctx)
         in Expression -> DataizeContext -> IO (Maybe String)
dataize' Expression
expr' DataizeContext
ctx
    (Maybe Binding
Nothing, [Binding]
_) -> case [Binding] -> (Maybe Binding, [Binding])
maybeLambda [Binding]
bds of
      (Just (BiLambda String
_), [Binding]
_) -> do
        Maybe Expression
morphed' <- Expression -> DataizeContext -> IO (Maybe Expression)
morph ([Binding] -> Expression
ExFormation [Binding]
bds) DataizeContext
ctx
        case Maybe Expression
morphed' of
          Just Expression
morphed -> Expression -> DataizeContext -> IO (Maybe String)
dataize' Expression
morphed DataizeContext
ctx
          Maybe Expression
_ -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
      (Maybe Binding
Nothing, [Binding]
_) -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
dataize' Expression
expr DataizeContext
prog = do
  Maybe Expression
morphed' <- Expression -> DataizeContext -> IO (Maybe Expression)
morph Expression
expr DataizeContext
prog
  case Maybe Expression
morphed' of
    Just Expression
morphed -> Expression -> DataizeContext -> IO (Maybe String)
dataize' Expression
morphed DataizeContext
prog
    Maybe Expression
_ -> Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing

toDouble :: Integer -> Double
toDouble :: Integer -> Double
toDouble = Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral

atom :: String -> Expression -> DataizeContext -> IO (Maybe Expression)
atom :: String -> Expression -> DataizeContext -> IO (Maybe Expression)
atom String
"L_org_eolang_number_plus" Expression
self DataizeContext
ctx = do
  Maybe String
left <- Expression -> DataizeContext -> IO (Maybe String)
dataize' (Expression -> Attribute -> Expression
ExDispatch Expression
self (String -> Attribute
AtLabel String
"x")) DataizeContext
ctx
  Maybe String
right <- Expression -> DataizeContext -> IO (Maybe String)
dataize' (Expression -> Attribute -> Expression
ExDispatch Expression
self Attribute
AtRho) DataizeContext
ctx
  case (Maybe String
left, Maybe String
right) of
    (Just String
left', Just String
right') -> do
      let first :: Double
first = (Integer -> Double)
-> (Double -> Double) -> Either Integer Double -> Double
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Integer -> Double
toDouble Double -> Double
forall a. a -> a
id (String -> Either Integer Double
hexToNum String
left')
          second :: Double
second = (Integer -> Double)
-> (Double -> Double) -> Either Integer Double -> Double
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Integer -> Double
toDouble Double -> Double
forall a. a -> a
id (String -> Either Integer Double
hexToNum String
right')
          sum :: Double
sum = Double
first Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
second
      Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (String -> String -> Expression
DataObject String
"number" (Double -> String
numToHex Double
sum)))
    (Maybe String, Maybe String)
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
atom String
"L_org_eolang_number_times" Expression
self DataizeContext
ctx = do
  Maybe String
left <- Expression -> DataizeContext -> IO (Maybe String)
dataize' (Expression -> Attribute -> Expression
ExDispatch Expression
self (String -> Attribute
AtLabel String
"x")) DataizeContext
ctx
  Maybe String
right <- Expression -> DataizeContext -> IO (Maybe String)
dataize' (Expression -> Attribute -> Expression
ExDispatch Expression
self Attribute
AtRho) DataizeContext
ctx
  case (Maybe String
left, Maybe String
right) of
    (Just String
left', Just String
right') -> do
      let first :: Double
first = (Integer -> Double)
-> (Double -> Double) -> Either Integer Double -> Double
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Integer -> Double
toDouble Double -> Double
forall a. a -> a
id (String -> Either Integer Double
hexToNum String
left')
          second :: Double
second = (Integer -> Double)
-> (Double -> Double) -> Either Integer Double -> Double
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Integer -> Double
toDouble Double -> Double
forall a. a -> a
id (String -> Either Integer Double
hexToNum String
right')
          sum :: Double
sum = Double
first Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
second
      Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (String -> String -> Expression
DataObject String
"number" (Double -> String
numToHex Double
sum)))
    (Maybe String, Maybe String)
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
atom String
"L_org_eolang_number_eq" Expression
self DataizeContext
ctx = do
  Maybe String
x <- Expression -> DataizeContext -> IO (Maybe String)
dataize' (Expression -> Attribute -> Expression
ExDispatch Expression
self (String -> Attribute
AtLabel String
"x")) DataizeContext
ctx
  Maybe String
rho <- Expression -> DataizeContext -> IO (Maybe String)
dataize' (Expression -> Attribute -> Expression
ExDispatch Expression
self Attribute
AtRho) DataizeContext
ctx
  case (Maybe String
x, Maybe String
rho) of
    (Just String
x', Just String
rho') -> do
      let self' :: Double
self' = (Integer -> Double)
-> (Double -> Double) -> Either Integer Double -> Double
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Integer -> Double
toDouble Double -> Double
forall a. a -> a
id (String -> Either Integer Double
hexToNum String
rho')
          first :: Double
first = (Integer -> Double)
-> (Double -> Double) -> Either Integer Double -> Double
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Integer -> Double
toDouble Double -> Double
forall a. a -> a
id (String -> Either Integer Double
hexToNum String
x')
      if Double
self' Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
first
        then Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (String -> String -> Expression
DataObject String
"number" (Double -> String
numToHex Double
first)))
        else Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> Maybe Expression
forall a. a -> Maybe a
Just (Expression -> Attribute -> Expression
ExDispatch Expression
self (String -> Attribute
AtLabel String
"y")))
    (Maybe String, Maybe String)
_ -> Maybe Expression -> IO (Maybe Expression)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expression
forall a. Maybe a
Nothing
atom String
func Expression
_ DataizeContext
_ = IOError -> IO (Maybe Expression)
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Atom '%s' does not exist" String
func))