{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE ScopedTypeVariables #-}

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

module Emit (emitted) where

import AST
import Control.Monad (zipWithM)
import Data.Char (isAlphaNum, isDigit, toLower, toUpper)
import Data.List (intercalate, mapAccumL, nub)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, isJust, isNothing)
import qualified Data.Set as Set
import qualified Data.Text as T
import Deps (Judgment)
import qualified Inference as In
import Matcher (Meta (..))
import Rewriter (fast)
import Rule (redex)
import Text.Printf (printf)
import qualified Yaml as Y

data Scope = Scope (Map.Map Meta String) Int

newtype Emitting a = Emitting (Scope -> Either String (a, Scope))

instance Functor Emitting where
  fmap :: forall a b. (a -> b) -> Emitting a -> Emitting b
fmap a -> b
func (Emitting Scope -> Either String (a, Scope)
walk) = (Scope -> Either String (b, Scope)) -> Emitting b
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting (((a, Scope) -> (b, Scope))
-> Either String (a, Scope) -> Either String (b, Scope)
forall a b. (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
value, Scope
scope) -> (a -> b
func a
value, Scope
scope)) (Either String (a, Scope) -> Either String (b, Scope))
-> (Scope -> Either String (a, Scope))
-> Scope
-> Either String (b, Scope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope -> Either String (a, Scope)
walk)

instance Applicative Emitting where
  pure :: forall a. a -> Emitting a
pure a
value = (Scope -> Either String (a, Scope)) -> Emitting a
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting (\Scope
scope -> (a, Scope) -> Either String (a, Scope)
forall a b. b -> Either a b
Right (a
value, Scope
scope))
  Emitting Scope -> Either String (a -> b, Scope)
left <*> :: forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
<*> Emitting Scope -> Either String (a, Scope)
right = (Scope -> Either String (b, Scope)) -> Emitting b
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting ((Scope -> Either String (b, Scope)) -> Emitting b)
-> (Scope -> Either String (b, Scope)) -> Emitting b
forall a b. (a -> b) -> a -> b
$ \Scope
scope -> do
    (a -> b
func, Scope
scope') <- Scope -> Either String (a -> b, Scope)
left Scope
scope
    (a
value, Scope
scope'') <- Scope -> Either String (a, Scope)
right Scope
scope'
    (b, Scope) -> Either String (b, Scope)
forall a b. b -> Either a b
Right (a -> b
func a
value, Scope
scope'')

instance Monad Emitting where
  Emitting Scope -> Either String (a, Scope)
walk >>= :: forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
>>= a -> Emitting b
next = (Scope -> Either String (b, Scope)) -> Emitting b
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting ((Scope -> Either String (b, Scope)) -> Emitting b)
-> (Scope -> Either String (b, Scope)) -> Emitting b
forall a b. (a -> b) -> a -> b
$ \Scope
scope -> do
    (a
value, Scope
scope') <- Scope -> Either String (a, Scope)
walk Scope
scope
    let Emitting Scope -> Either String (b, Scope)
walk' = a -> Emitting b
next a
value
    Scope -> Either String (b, Scope)
walk' Scope
scope'

data Qual
  = Gen Pat String
  | Guard String
  | Let String String

data Pat
  = PVar String
  | PCon String [Pat]
  | PPair Pat Pat
  | PCons Pat Pat
  | PNil

emitted :: [Y.Rule] -> [Y.Rule] -> [Y.ContextualizeRule] -> [Y.MorphRule] -> [Y.DataizeRule] -> [String] -> Either String String
emitted :: [Rule]
-> [Rule]
-> [ContextualizeRule]
-> [MorphRule]
-> [DataizeRule]
-> [String]
-> Either String String
emitted [Rule]
builtin [Rule]
custom [ContextualizeRule]
contextual [MorphRule]
morphs [DataizeRule]
dataizes [String]
sources = do
  let rules :: [(String, Rule)]
rules = [String] -> [Rule] -> [(String, Rule)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([String] -> [String]
named ((Rule -> String) -> [Rule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) ([Rule]
builtin [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ [Rule]
custom))) ([Rule]
builtin [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
++ [Rule]
custom)
  [String]
functions <- ((String, Rule) -> Either String String)
-> [(String, Rule)] -> Either String [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (String, Rule) -> Either String String
rewriting [(String, Rule)]
rules
  [String]
equations <- (String -> ContextualizeRule -> Either String String)
-> [String] -> [ContextualizeRule] -> Either String [String]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM String -> ContextualizeRule -> Either String String
contextualizing ([String] -> [String]
named ((ContextualizeRule -> String) -> [ContextualizeRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [ContextualizeRule]
contextual)) [ContextualizeRule]
contextual
  [String]
morphings <- (String -> MorphRule -> Either String String)
-> [String] -> [MorphRule] -> Either String [String]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM String -> MorphRule -> Either String String
morphing ([String] -> [String]
named ((MorphRule -> String) -> [MorphRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [MorphRule]
morphs)) [MorphRule]
morphs
  [String]
dataizations <- (String -> DataizeRule -> Either String String)
-> [String] -> [DataizeRule] -> Either String [String]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM String -> DataizeRule -> Either String String
dataizing ([String] -> [String]
named ((DataizeRule -> String) -> [DataizeRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [DataizeRule]
dataizes)) [DataizeRule]
dataizes
  let body :: String
body =
        [String] -> String
unlines
          ( [ String
"compiled :: Maybe En.Engine"
            , String
"compiled ="
            , String
"  Just"
            , String
"    En.Engine"
            , String
"      { En._normalization = normalization"
            , String
"      , En._matching = \\universe -> Set.fromList . matching universe"
            , String
"      , En._rules = steps"
            , String
"      , En._normal = nf"
            , String
"      , En._contextualize = \\term context -> either E.throwIO pure (contextualize term context)"
            , String
"      , En._morphing = morphings"
            , String
"      , En._dataization = dataizations"
            , String
"      , En._sources = sources"
            , String
"      }"
            , String
""
            , String
"-- The steps of the built-in rules of normalization, in the order of the rules."
            , String
"normalization :: [Ru.Step]"
            , String
"normalization = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
listed (((String, Rule) -> String) -> [(String, Rule)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"step" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> ((String, Rule) -> String) -> (String, Rule) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Rule) -> String
forall a b. (a, b) -> a
fst) (Int -> [(String, Rule)] -> [(String, Rule)]
forall a. Int -> [a] -> [a]
take ([Rule] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Rule]
builtin) [(String, Rule)]
rules))
            , String
""
            , String
"-- The steps of every rule compiled, by the text of the rule."
            , String
"steps :: Map.Map String Ru.Step"
            , String
"steps ="
            , String
"  Map.fromList " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
listed [String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%s, step%s)" (String -> String
forall a. Show a => a -> String
show (Rule -> String
forall a. Show a => a -> String
show Rule
rule)) String
name | (String
name, Rule
rule) <- [(String, Rule)]
rules]
            , String
""
            , String
"-- The rules of 𝕄, in the order of their files."
            , String
"morphings :: [In.Inference Expression]"
            , String
"morphings = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
listed ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"In.direct morphing" String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> [String]
named ((MorphRule -> String) -> [MorphRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [MorphRule]
morphs)))
            , String
""
            , String
"-- The rules of 𝔻, in the order of their files."
            , String
"dataizations :: [In.Inference Bytes]"
            , String
"dataizations = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
listed ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"In.direct dataization" String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> [String]
named ((DataizeRule -> String) -> [DataizeRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [DataizeRule]
dataizes)))
            , String
""
            , String
"-- The texts of the built-in rules of all four judgments this module is made of."
            , String
"sources :: [String]"
            , String
"sources = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
listed ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
forall a. Show a => a -> String
show [String]
sources)
            , String
""
            , String
"-- Whether the term is a normal form: no built-in rule of normalization"
            , String
"-- matches anywhere inside it."
            , String
"nf :: Expression -> Bool"
            , String
"nf = Ru.normalWith (not . null . matching Nothing)"
            , String
""
            , String
"-- The numbers of the built-in rules of normalization matching somewhere in"
            , String
"-- the term, in the order one walk over it meets them, told the world the"
            , String
"-- term stands in."
            , String
"matching :: Maybe Expression -> Expression -> [Int]"
            , String
"matching ="
            , String
"  M.hits"
            , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [String] -> String
listed' Int
4 [String -> Int -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%d, %s, rewrite%s)" Int
idx (Bool -> String
forall a. Show a => a -> String
show (Rule -> Bool
redex Rule
rule)) String
name | (Int
idx, (String
name, Rule
rule)) <- [Int] -> [(String, Rule)] -> [(Int, (String, Rule))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Int -> [(String, Rule)] -> [(String, Rule)]
forall a. Int -> [a] -> [a]
take ([Rule] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Rule]
builtin) [(String, Rule)]
rules)]
            , String
""
            , String
"-- The Contextualization function 𝒞, the conclusion of the one rule matching"
            , String
"-- the term and the context."
            , String
"contextualize :: Expression -> Expression -> Either C.ContextualizeException Expression"
            , String
"contextualize term context ="
            , String
"  C.concluded"
            , String
"    term"
            , String
"    ( concat"
            , String
"        " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [String] -> String
listed' Int
8 [String -> String -> String
forall r. PrintfType r => String -> r
printf String
"contextualize%s term context" String
name | String
name <- [String] -> [String]
named ((ContextualizeRule -> String) -> [ContextualizeRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [ContextualizeRule]
contextual)]
            , String
"    )"
            , String
""
            ]
              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
functions
              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
equations
              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
morphings
              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
dataizations
          )
  String -> Either String String
forall a b. b -> Either a b
Right (String
header String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
imports String
body String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
body)
  where
    header :: String
    header :: String
header =
      [String] -> String
unlines
        [ String
"-- The built-in rules of phino, and the rules of '--rule' it was given, as"
        , String
"-- Haskell: this module is written by 'phino compile' and a build with the"
        , String
"-- flag 'compiled' links it in (#1617). The next 'phino compile' writes it"
        , String
"-- anew, so a change belongs to the rules of YAML and not to it."
        , String
"module Compiled (compiled) where"
        , String
""
        ]
    imports :: String -> String
    imports :: String -> String
imports String
body =
      [String] -> String
unlines
        ( String
"import AST"
            String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ String
line
              | (String
qualifier, String
line) <-
                  [ (String
"B.", String
"import qualified Builder as B")
                  , (String
"C.", String
"import qualified Contextualize as C")
                  , (String
"D.", String
"import qualified Deps as D")
                  , (String
"E.", String
"import qualified Control.Exception as E")
                  , (String
"En.", String
"import qualified Engine as En")
                  , (String
"In.", String
"import qualified Inference as In")
                  , (String
"M.", String
"import qualified Matcher as M")
                  , (String
"Map.", String
"import qualified Data.Map.Strict as Map")
                  , (String
"R.", String
"import qualified Rewriter as R")
                  , (String
"Ru.", String
"import qualified Rule as Ru")
                  , (String
"Set.", String
"import qualified Data.Set as Set")
                  , (String
"T.", String
"import qualified Data.Text as T")
                  ]
              , String
qualifier String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
qualifiers String
body
              ]
        )
    qualifiers :: String -> [String]
    qualifiers :: String -> [String]
qualifiers String
body = [(Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.') String
word String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." | String
word <- String -> [String]
words ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
spaced String
body), Char
'.' Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
word, String -> Bool
isUpperStart String
word]
    spaced :: Char -> Char
    spaced :: Char -> Char
spaced Char
char
      | Char -> Bool
isAlphaNum Char
char Bool -> Bool -> Bool
|| Char
char Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.' Bool -> Bool -> Bool
|| Char
char Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' = Char
char
      | Bool
otherwise = Char
' '
    isUpperStart :: String -> Bool
    isUpperStart :: String -> Bool
isUpperStart (Char
first : String
_) = Char
first Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'A' .. Char
'Z']
    isUpperStart [] = Bool
False

named :: [String] -> [String]
named :: [String] -> [String]
named [String]
names = (Set String, [String]) -> [String]
forall a b. (a, b) -> b
snd ((Set String -> (Int, String) -> (Set String, String))
-> Set String -> [(Int, String)] -> (Set String, [String])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL Set String -> (Int, String) -> (Set String, String)
unique ([String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList [String]
stems) ([Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [String]
stems))
  where
    stems :: [String]
    stems :: [String]
stems = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
camel [String]
names
    unique :: Set.Set String -> (Int, String) -> (Set.Set String, String)
    unique :: Set String -> (Int, String) -> (Set String, String)
unique Set String
taken (Int
idx, String
name)
      | [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
name) [String]
stems) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 =
          let chosen :: String
chosen = String -> String
available (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
idx)
           in (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
chosen Set String
taken, String
chosen)
      | Bool
otherwise = (Set String
taken, String
name)
      where
        available :: String -> String
        available :: String -> String
available String
candidate
          | String
candidate String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
taken = String -> String
available (String
candidate String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_")
          | Bool
otherwise = String
candidate
    camel :: String -> String
    camel :: String -> String
camel String
name = case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter Char -> Bool
isAlphaNum ((String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> String
upper (String -> [String]
words ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\Char
char -> if Char -> Bool
isAlphaNum Char
char then Char
char else Char
' ') String
name))) of
      [] -> String
"Rule"
      word :: String
word@(Char
first : String
_)
        | Char -> Bool
isDigit Char
first -> String
"Rule" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
word
        | Bool
otherwise -> String
word
    upper :: String -> String
    upper :: String -> String
upper (Char
first : String
rest) = Char -> Char
toUpper Char
first Char -> String -> String
forall a. a -> [a] -> [a]
: String
rest
    upper [] = []

rewriting :: (String, Y.Rule) -> Either String String
rewriting :: (String, Rule) -> Either String String
rewriting (String
name, Rule
rule) = do
  Either String ()
refused
  ([Qual]
quals, String
result) <- Emitting ([Qual], String) -> Either String ([Qual], String)
forall a. Emitting a -> Either String a
walked (Emitting ([Qual], String) -> Either String ([Qual], String))
-> Emitting ([Qual], String) -> Either String ([Qual], String)
forall a b. (a -> b) -> a -> b
$ do
    [Qual]
pattern' <- Expression -> String -> Emitting [Qual]
matching Rule
rule.pattern String
"term"
    [Qual]
when' <- Emitting [Qual]
-> (Condition -> Emitting [Qual])
-> Maybe Condition
-> Emitting [Qual]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) ((String -> [Qual]) -> Emitting String -> Emitting [Qual]
forall a b. (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Qual -> [Qual]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Qual -> [Qual]) -> (String -> Qual) -> String -> [Qual]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Qual
Guard) (Emitting String -> Emitting [Qual])
-> (Condition -> Emitting String) -> Condition -> Emitting [Qual]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Condition -> Emitting String
condition) Rule
rule.when
    [Qual]
absolute <- (Meta -> Emitting Qual) -> [Meta] -> Emitting [Qual]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((String -> Qual) -> Emitting String -> Emitting Qual
forall a b. (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\String
var -> String -> Qual
Guard (String
"Ru.xiFree " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var)) (Emitting String -> Emitting Qual)
-> (Meta -> Emitting String) -> Meta -> Emitting Qual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Meta -> Emitting String
held) (String -> Expression -> [Meta]
prefixed String
"k" Rule
rule.pattern)
    [Qual]
normal <- (Meta -> Emitting Qual) -> [Meta] -> Emitting [Qual]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((String -> Qual) -> Emitting String -> Emitting Qual
forall a b. (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\String
var -> String -> Qual
Guard (String
"Ru.normalHeld nf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var)) (Emitting String -> Emitting Qual)
-> (Meta -> Emitting String) -> Meta -> Emitting Qual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Meta -> Emitting String
held) (String -> Expression -> [Meta]
prefixed String
"n" Rule
rule.pattern [Meta] -> [Meta] -> [Meta]
forall a. [a] -> [a] -> [a]
++ String -> Expression -> [Meta]
prefixed String
"k" Rule
rule.pattern)
    [Qual]
extras <- [[Qual]] -> [Qual]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Qual]] -> [Qual]) -> Emitting [[Qual]] -> Emitting [Qual]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Extra -> Emitting [Qual]) -> [Extra] -> Emitting [[Qual]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Extra -> Emitting [Qual]
extended ([Extra] -> Maybe [Extra] -> [Extra]
forall a. a -> Maybe a -> a
fromMaybe [] Rule
rule.where_)
    String
result <- Bool -> Expression -> Emitting (Maybe String)
built Bool
True Rule
rule.result Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"its result names a meta its pattern does not bind") String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ([Qual], String) -> Emitting ([Qual], String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Qual]
pattern' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
when' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
absolute [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
normal [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
extras, String
result)
  let body :: String
body = [Qual] -> String -> String
comprehension [Qual]
quals String
result
      universe :: String
universe = if String
"universe" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
tokens String
body then String
"universe" else String
"_"
  String -> Either String String
forall a b. b -> Either a b
Right
    ( [String] -> String
unlines
        [ String -> String -> String
forall r. PrintfType r => String -> r
printf String
"-- The rule '%s'." ([String] -> String
unwords (String -> [String]
lines Rule
rule.name))
        , String -> String -> String
forall r. PrintfType r => String -> r
printf String
"step%s :: Ru.Step" String
name
        , String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"step%s = R.direct %s %s rewrite%s" String
name (String -> String
forall a. Show a => a -> String
show Rule
rule.name) (Bool -> String
forall a. Show a => a -> String
show (Rule -> Bool
redex Rule
rule)) String
name
        , String
""
        , String -> String -> String
forall r. PrintfType r => String -> r
printf String
"rewrite%s :: Maybe Expression -> Expression -> [Expression]" String
name
        , String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"rewrite%s %s %s =" String
name String
universe (if String
"term" String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
tokens String
body then String
"term" else String
"_")
        , String
body
        ]
    )
  where
    refused :: Either String ()
    refused :: Either String ()
refused
      | Maybe Condition -> Bool
forall a. Maybe a -> Bool
isJust Rule
rule.having = String -> Either String ()
forall a b. a -> Either a b
Left (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The rule '%s' cannot be compiled, since it has a 'having' condition" Rule
rule.name)
      | Maybe Condition -> Bool
forall a. Maybe a -> Bool
isNothing Rule
rule.when Bool -> Bool -> Bool
&& Expression -> Expression -> Bool
fast Rule
rule.pattern Rule
rule.result = String -> Either String ()
forall a b. a -> Either a b
Left (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The rule '%s' cannot be compiled, since it rewrites a formation into a formation the fast way" Rule
rule.name)
      | Expression -> Bool
rooted Rule
rule.pattern = String -> Either String ()
forall a b. a -> Either a b
Left (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The rule '%s' cannot be compiled, since its pattern applies Φ to a ρ" Rule
rule.name)
      | Bool
otherwise = () -> Either String ()
forall a b. b -> Either a b
Right ()
    walked :: Emitting a -> Either String a
    walked :: forall a. Emitting a -> Either String a
walked (Emitting Scope -> Either String (a, Scope)
walk) = (String -> Either String a)
-> ((a, Scope) -> Either String a)
-> Either String (a, Scope)
-> Either String a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a)
-> (String -> String) -> String -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The rule '%s' cannot be compiled, since %s" Rule
rule.name) (a -> Either String a
forall a b. b -> Either a b
Right (a -> Either String a)
-> ((a, Scope) -> a) -> (a, Scope) -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Scope) -> a
forall a b. (a, b) -> a
fst) (Scope -> Either String (a, Scope)
walk (Map Meta String -> Int -> Scope
Scope Map Meta String
forall k a. Map k a
Map.empty Int
1))
    extended :: Y.Extra -> Emitting [Qual]
    extended :: Extra -> Emitting [Qual]
extended Extra
extra = case (Extra
extra.meta, Extra
extra.function, Extra
extra.args) of
      (Y.ArgExpression (ExMeta Text
meta), String
"contextualize", [Y.ArgExpression Expression
expr, Y.ArgExpression Expression
context]) -> do
        String
expr' <- Expression -> Emitting String
argument Expression
expr
        String
context' <- Expression -> Emitting String
argument Expression
context
        Text -> String -> Emitting [Qual]
into Text
meta (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"either E.throw id (contextualize %s %s)" String
expr' String
context')
      (Y.ArgExpression (ExMeta Text
meta), String
"named", [Y.ArgExpression Expression
expr]) -> do
        String
expr' <- Expression -> Emitting String
argument Expression
expr
        Text -> String -> Emitting [Qual]
into Text
meta (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"B.nameIn universe %s" String
expr')
      (ExtraArgument
_, String
func, [ExtraArgument]
_) -> String -> Emitting [Qual]
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"its 'where' calls the function '%s', which only 'contextualize' and 'named' can be" String
func)
    argument :: Expression -> Emitting String
    argument :: Expression -> Emitting String
argument Expression
expr = Bool -> Expression -> Emitting (Maybe String)
built Bool
True Expression
expr Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"its 'where' names a meta its pattern does not bind") (String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Emitting String)
-> (String -> String) -> String -> Emitting String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens)
    into :: T.Text -> String -> Emitting [Qual]
    into :: Text -> String -> Emitting [Qual]
into Text
meta String
value =
      Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta) Emitting (Maybe String)
-> (Maybe String -> Emitting [Qual]) -> Emitting [Qual]
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just String
var -> [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [String -> Qual
Guard (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s == %s" String
var (String -> String
parens String
value))]
        Maybe String
Nothing -> do
          let var :: String
var = Meta -> String
variable (Text -> Meta
Named Text
meta)
          Meta -> String -> Emitting ()
bind (Text -> Meta
Named Text
meta) String
var
          [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [String -> String -> Qual
Let String
var String
value]

contextualizing :: String -> Y.ContextualizeRule -> Either String String
contextualizing :: String -> ContextualizeRule -> Either String String
contextualizing String
name ContextualizeRule
rule = do
  ([Qual]
quals, String
result) <- Emitting ([Qual], String) -> Either String ([Qual], String)
forall a. Emitting a -> Either String a
walked (Emitting ([Qual], String) -> Either String ([Qual], String))
-> Emitting ([Qual], String) -> Either String ([Qual], String)
forall a b. (a -> b) -> a -> b
$ do
    [Qual]
term <- Expression -> String -> Emitting [Qual]
matching ContextualizeRule
rule.match String
"term"
    [Qual]
context <- Expression -> String -> Emitting [Qual]
matching ContextualizeRule
rule.cmatch String
"context"
    [(String, String)]
premises <- (Premise -> Emitting (String, String))
-> [Premise] -> Emitting [(String, String)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Premise -> Emitting (String, String)
premised ContextualizeRule
rule.premises
    String
result <- Bool -> Expression -> Emitting (Maybe String)
built Bool
True ContextualizeRule
rule.cresult Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"its conclusion names a meta nothing binds") String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ([Qual], String) -> Emitting ([Qual], String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Qual]
term [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
context, [(String, String)] -> String -> String
conclusion [(String, String)]
premises String
result)
  let body :: String
body = [Qual] -> String -> String
comprehension [Qual]
quals String
result
      arg :: String -> String
arg String
var = if String
var String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
tokens String
body then String
var else String
"_"
  String -> Either String String
forall a b. b -> Either a b
Right
    ( [String] -> String
unlines
        [ String -> String -> String
forall r. PrintfType r => String -> r
printf String
"-- The contextualization rule '%s'." ([String] -> String
unwords (String -> [String]
lines ContextualizeRule
rule.name))
        , String -> String -> String
forall r. PrintfType r => String -> r
printf String
"contextualize%s :: Expression -> Expression -> [(String, Either C.ContextualizeException Expression)]" String
name
        , String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"contextualize%s %s %s =" String
name (String -> String
arg String
"term") (String -> String
arg String
"context")
        , String
body
        ]
    )
  where
    walked :: Emitting a -> Either String a
    walked :: forall a. Emitting a -> Either String a
walked (Emitting Scope -> Either String (a, Scope)
walk) = (String -> Either String a)
-> ((a, Scope) -> Either String a)
-> Either String (a, Scope)
-> Either String a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a)
-> (String -> String) -> String -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The contextualization rule '%s' cannot be compiled, since %s" ContextualizeRule
rule.name) (a -> Either String a
forall a b. b -> Either a b
Right (a -> Either String a)
-> ((a, Scope) -> a) -> (a, Scope) -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Scope) -> a
forall a b. (a, b) -> a
fst) (Scope -> Either String (a, Scope)
walk (Map Meta String -> Int -> Scope
Scope Map Meta String
forall k a. Map k a
Map.empty Int
1))
    premised :: Y.Premise -> Emitting (String, String)
    premised :: Premise -> Emitting (String, String)
premised (Y.Premise Text
result (Y.OpContextualize Expression
inner Expression
outer)) = do
      String
inner' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
True Expression
inner Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"a premise names a meta nothing binds") (String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Emitting String)
-> (String -> String) -> String -> Emitting String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens)
      String
outer' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
True Expression
outer Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"a premise names a meta nothing binds") (String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Emitting String)
-> (String -> String) -> String -> Emitting String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens)
      String
var <- Text -> Emitting String
introduced Text
result
      (String, String) -> Emitting (String, String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
var, String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"contextualize %s %s" String
inner' String
outer')
    premised Premise
premise = String -> Emitting (String, String)
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"its premise '%s' is not a contextualization" (Text -> String
T.unpack Premise
premise.result))
    conclusion :: [(String, String)] -> String -> String
    conclusion :: [(String, String)] -> String -> String
conclusion [] String
result = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%s, Right %s)" (String -> String
forall a. Show a => a -> String
show ContextualizeRule
rule.name) (String -> String
parens String
result)
    conclusion [(String, String)]
premises String
result =
      String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf
        String
"(%s, do { %s; pure %s })"
        (String -> String
forall a. Show a => a -> String
show ContextualizeRule
rule.name)
        (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"; " [String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s <- %s" String
var String
call | (String
var, String
call) <- [(String, String)]
premises])
        (String -> String
parens String
result)

morphing :: String -> Y.MorphRule -> Either String String
morphing :: String -> MorphRule -> Either String String
morphing String
name MorphRule
rule = String
-> (String, String)
-> Rule
-> Expression
-> (Expression -> Emitting (Maybe String))
-> Either String ([Premise], Conclusion Expression)
-> Either String String
forall value.
String
-> (String, String)
-> Rule
-> Expression
-> (value -> Emitting (Maybe String))
-> Either String ([Premise], Conclusion value)
-> Either String String
inferring String
"morphing" (String
"morphing" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name, String
"Expression") (String
-> Maybe String
-> Maybe String
-> Expression
-> Expression
-> Maybe Condition
-> Maybe [Extra]
-> Maybe Condition
-> Rule
Y.Rule MorphRule
rule.name Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing MorphRule
rule.match Expression
ExRoot MorphRule
rule.when Maybe [Extra]
forall a. Maybe a
Nothing Maybe Condition
forall a. Maybe a
Nothing) MorphRule
rule.ematch (Bool -> Expression -> Emitting (Maybe String)
built Bool
True) (MorphRule -> Either String ([Premise], Conclusion Expression)
In.morphingSpine MorphRule
rule)

dataizing :: String -> Y.DataizeRule -> Either String String
dataizing :: String -> DataizeRule -> Either String String
dataizing String
name DataizeRule
rule = String
-> (String, String)
-> Rule
-> Expression
-> (Bytes -> Emitting (Maybe String))
-> Either String ([Premise], Conclusion Bytes)
-> Either String String
forall value.
String
-> (String, String)
-> Rule
-> Expression
-> (value -> Emitting (Maybe String))
-> Either String ([Premise], Conclusion value)
-> Either String String
inferring String
"dataization" (String
"dataization" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name, String
"Bytes") (String
-> Maybe String
-> Maybe String
-> Expression
-> Expression
-> Maybe Condition
-> Maybe [Extra]
-> Maybe Condition
-> Rule
Y.Rule DataizeRule
rule.name Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing DataizeRule
rule.match Expression
ExRoot DataizeRule
rule.when Maybe [Extra]
forall a. Maybe a
Nothing Maybe Condition
forall a. Maybe a
Nothing) DataizeRule
rule.ematch Bytes -> Emitting (Maybe String)
builtBytes (DataizeRule -> Either String ([Premise], Conclusion Bytes)
In.dataizationSpine DataizeRule
rule)

inferring :: forall value. String -> (String, String) -> Y.Rule -> Expression -> (value -> Emitting (Maybe String)) -> Either String ([Y.Premise], In.Conclusion value) -> Either String String
inferring :: forall value.
String
-> (String, String)
-> Rule
-> Expression
-> (value -> Emitting (Maybe String))
-> Either String ([Premise], Conclusion value)
-> Either String String
inferring String
kind (String
name, String
answer) Rule
rule Expression
ematch value -> Emitting (Maybe String)
builder Either String ([Premise], Conclusion value)
spine = do
  ([Premise]
sides, Conclusion value
conclusion) <- (String -> Either String ([Premise], Conclusion value))
-> (([Premise], Conclusion value)
    -> Either String ([Premise], Conclusion value))
-> Either String ([Premise], Conclusion value)
-> Either String ([Premise], Conclusion value)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Either String ([Premise], Conclusion value)
forall a b. a -> Either a b
Left (String -> Either String ([Premise], Conclusion value))
-> (String -> String)
-> String
-> Either String ([Premise], Conclusion value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
refusal) ([Premise], Conclusion value)
-> Either String ([Premise], Conclusion value)
forall a b. b -> Either a b
Right Either String ([Premise], Conclusion value)
spine
  ([Qual]
quals, String
result) <- Emitting ([Qual], String) -> Either String ([Qual], String)
forall a. Emitting a -> Either String a
walked (Emitting ([Qual], String) -> Either String ([Qual], String))
-> Emitting ([Qual], String) -> Either String ([Qual], String)
forall a b. (a -> b) -> a -> b
$ do
    [Qual]
universe <- Expression -> String -> Emitting [Qual]
matching Expression
ematch String
"universe"
    [Qual]
term <- Expression -> String -> Emitting [Qual]
matching Rule
rule.pattern String
"term"
    [Qual]
when' <- Emitting [Qual]
-> (Condition -> Emitting [Qual])
-> Maybe Condition
-> Emitting [Qual]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) ((String -> [Qual]) -> Emitting String -> Emitting [Qual]
forall a b. (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Qual -> [Qual]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Qual -> [Qual]) -> (String -> Qual) -> String -> [Qual]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Qual
Guard) (Emitting String -> Emitting [Qual])
-> (Condition -> Emitting String) -> Condition -> Emitting [Qual]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Condition -> Emitting String
condition) Rule
rule.when
    [Qual]
absolute <- (Meta -> Emitting Qual) -> [Meta] -> Emitting [Qual]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((String -> Qual) -> Emitting String -> Emitting Qual
forall a b. (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\String
var -> String -> Qual
Guard (String
"Ru.xiFree " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var)) (Emitting String -> Emitting Qual)
-> (Meta -> Emitting String) -> Meta -> Emitting Qual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Meta -> Emitting String
held) (String -> Expression -> [Meta]
prefixed String
"k" Rule
rule.pattern)
    [Qual]
normal <- (Meta -> Emitting Qual) -> [Meta] -> Emitting [Qual]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((String -> Qual) -> Emitting String -> Emitting Qual
forall a b. (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\String
var -> String -> Qual
Guard (String
"Ru.normalHeld nf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var)) (Emitting String -> Emitting Qual)
-> (Meta -> Emitting String) -> Meta -> Emitting Qual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Meta -> Emitting String
held) (String -> Expression -> [Meta]
prefixed String
"n" Rule
rule.pattern [Meta] -> [Meta] -> [Meta]
forall a. [a] -> [a] -> [a]
++ String -> Expression -> [Meta]
prefixed String
"k" Rule
rule.pattern)
    String
result <- [Premise] -> Conclusion value -> Emitting String
premised [Premise]
sides Conclusion value
conclusion
    ([Qual], String) -> Emitting ([Qual], String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Qual]
universe [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
term [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
when' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
absolute [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
normal, String
result)
  let body :: String
body = [Qual] -> String -> String
comprehension [Qual]
quals String
result
      arg :: String -> String
arg String
var = if String
var String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
tokens String
body then String
var else String
"_"
  String -> Either String String
forall a b. b -> Either a b
Right
    ( [String] -> String
unlines
        [ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"-- The %s rule '%s'." String
kind ([String] -> String
unwords (String -> [String]
lines Rule
rule.name))
        , String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s :: Expression -> Expression -> [In.Premises %s]" String
name String
answer
        , String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s %s =" String
name (String -> String
arg String
"term") (String -> String
arg String
"universe")
        , String
body
        ]
    )
  where
    refusal :: String -> String
    refusal :: String -> String
refusal = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The %s rule '%s' cannot be compiled, since %s" String
kind Rule
rule.name
    walked :: Emitting a -> Either String a
    walked :: forall a. Emitting a -> Either String a
walked (Emitting Scope -> Either String (a, Scope)
walk) = (String -> Either String a)
-> ((a, Scope) -> Either String a)
-> Either String (a, Scope)
-> Either String a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Either String a
forall a b. a -> Either a b
Left (String -> Either String a)
-> (String -> String) -> String -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
refusal) (a -> Either String a
forall a b. b -> Either a b
Right (a -> Either String a)
-> ((a, Scope) -> a) -> (a, Scope) -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Scope) -> a
forall a b. (a, b) -> a
fst) (Scope -> Either String (a, Scope)
walk (Map Meta String -> Int -> Scope
Scope Map Meta String
forall k a. Map k a
Map.empty Int
1))
    premised :: [Y.Premise] -> In.Conclusion value -> Emitting String
    premised :: [Premise] -> Conclusion value -> Emitting String
premised [] Conclusion value
conclusion = (String
"In.Concludes " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens (String -> String) -> Emitting String -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Conclusion value -> Emitting String
concluded Conclusion value
conclusion
    premised (Premise
premise : [Premise]
rest) Conclusion value
conclusion = do
      (String
constructor, String
first, String
second) <- case Premise
premise.operation of
        Y.OpMorph Expression
expr Expression
world -> (,,) String
"In.Morphs" (String -> String -> (String, String, String))
-> Emitting String -> Emitting (String -> (String, String, String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Expression -> Emitting String
argued String
"a premise" Expression
expr Emitting (String -> (String, String, String))
-> Emitting String -> Emitting (String, String, String)
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Expression -> Emitting String
argued String
"a premise" Expression
world
        Y.OpEvaluate Expression
expr Expression
world -> (,,) String
"In.Evaluates" (String -> String -> (String, String, String))
-> Emitting String -> Emitting (String -> (String, String, String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Expression -> Emitting String
argued String
"a premise" Expression
expr Emitting (String -> (String, String, String))
-> Emitting String -> Emitting (String, String, String)
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Expression -> Emitting String
argued String
"a premise" Expression
world
        Y.OpContextualize Expression
expr Expression
context -> (,,) String
"In.Contextualizes" (String -> String -> (String, String, String))
-> Emitting String -> Emitting (String -> (String, String, String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Expression -> Emitting String
argued String
"a premise" Expression
expr Emitting (String -> (String, String, String))
-> Emitting String -> Emitting (String, String, String)
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Expression -> Emitting String
argued String
"a premise" Expression
context
        Operation
_ -> String -> Emitting (String, String, String)
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"its premise '%s' runs beside the spine, which only a 'morph', an 'evaluate' or a 'contextualize' can" (Text -> String
T.unpack Premise
premise.result))
      String
var <- Text -> Emitting String
introduced Premise
premise.result
      String
next <- [Premise] -> Conclusion value -> Emitting String
premised [Premise]
rest Conclusion value
conclusion
      String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s %s (\\%s -> pure %s)" String
constructor String
first String
second (if String
var String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String -> [String]
tokens String
next then String
var else String
"_") (String -> String
parens String
next))
    concluded :: In.Conclusion value -> Emitting String
    concluded :: Conclusion value -> Emitting String
concluded (In.Answered (Judgment, String)
step value
value) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"In.Answered %s %s" ((Judgment, String) -> String
stepped (Judgment, String)
step) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens (String -> String) -> Emitting String -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (value -> Emitting (Maybe String)
builder value
value Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"its conclusion names a meta nothing binds") String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
    concluded (In.Onward Way
way Expression
expr Expression
world) = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"In.Onward %s %s %s" (String -> String -> String -> String)
-> Emitting String -> Emitting (String -> String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> String
parens (String -> String) -> Emitting String -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Way -> Emitting String
wayOf Way
way) Emitting (String -> String -> String)
-> Emitting String -> Emitting (String -> String)
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Expression -> Emitting String
argued String
"its conclusion" Expression
expr Emitting (String -> String) -> Emitting String -> Emitting String
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Expression -> Emitting String
argued String
"its conclusion" Expression
world
    wayOf :: In.Way -> Emitting String
    wayOf :: Way -> Emitting String
wayOf (In.Taken (Judgment, String)
step) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In.Taken " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Judgment, String) -> String
stepped (Judgment, String)
step)
    wayOf (In.Normalized (Judgment, String)
step) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In.Normalized " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Judgment, String) -> String
stepped (Judgment, String)
step)
    wayOf (In.Named (Judgment, String)
step) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"In.Named " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Judgment, String) -> String
stepped (Judgment, String)
step)
    wayOf (In.Staged Expression
stage) = (String
"In.Staged " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> Emitting String -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Expression -> Emitting String
argued String
"its conclusion" Expression
stage
    argued :: String -> Expression -> Emitting String
    argued :: String -> Expression -> Emitting String
argued String
place Expression
expr = Bool -> Expression -> Emitting (Maybe String)
built Bool
True Expression
expr Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s names a meta nothing binds" String
place)) (String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Emitting String)
-> (String -> String) -> String -> Emitting String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens)
    stepped :: (Judgment, String) -> String
    stepped :: (Judgment, String) -> String
stepped (Judgment
judgment, String
verb) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(D.%s, %s)" (Judgment -> String
forall a. Show a => a -> String
show Judgment
judgment) (String -> String
forall a. Show a => a -> String
show String
verb)

comprehension :: [Qual] -> String -> String
comprehension :: [Qual] -> String -> String
comprehension [Qual]
quals String
result = case ([String], Set String) -> [String]
forall a b. (a, b) -> a
fst ((Qual -> ([String], Set String) -> ([String], Set String))
-> ([String], Set String) -> [Qual] -> ([String], Set String)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Qual -> ([String], Set String) -> ([String], Set String)
written ([], [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList (String -> [String]
tokens String
result)) [Qual]
quals) of
  [] -> String
"  [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
result String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
  String
first : [String]
rest -> String
"  [ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
result String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  | " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
first String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String
"\n  , " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
rest String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n  ]"
  where
    written :: Qual -> ([String], Set.Set String) -> ([String], Set.Set String)
    written :: Qual -> ([String], Set String) -> ([String], Set String)
written (Gen Pat
pat String
source) ([String]
lines', Set String
used) = ((Set String -> Pat -> String
pattern' Set String
used Pat
pat String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" <- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
source) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
lines', String -> Set String -> Set String
grown String
source Set String
used)
    written (Guard String
guard) ([String]
lines', Set String
used) = (String
guard String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
lines', String -> Set String -> Set String
grown String
guard Set String
used)
    written (Let String
var String
value) ([String]
lines', Set String
used)
      | String
var String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
used = ((String
"let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
value) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
lines', String -> Set String -> Set String
grown String
value Set String
used)
      | Bool
otherwise = ([String]
lines', Set String
used)
    grown :: String -> Set.Set String -> Set.Set String
    grown :: String -> Set String -> Set String
grown String
text Set String
used = (String -> Set String -> Set String)
-> Set String -> [String] -> Set String
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert Set String
used (String -> [String]
tokens String
text)
    pattern' :: Set.Set String -> Pat -> String
    pattern' :: Set String -> Pat -> String
pattern' Set String
used (PVar String
var)
      | String
var String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
used = String
var
      | Bool
otherwise = String
"_"
    pattern' Set String
_ (PCon String
con []) = String
con
    pattern' Set String
used (PCon String
con [Pat]
pats) = String
con String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Pat -> String) -> [Pat] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Set String -> Pat -> String
atomic Set String
used) [Pat]
pats)
    pattern' Set String
used (PPair Pat
left Pat
right) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set String -> Pat -> String
pattern' Set String
used Pat
left String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set String -> Pat -> String
pattern' Set String
used Pat
right String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    pattern' Set String
used (PCons Pat
first Pat
rest) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set String -> Pat -> String
pattern' Set String
used Pat
first String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set String -> Pat -> String
pattern' Set String
used Pat
rest String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    pattern' Set String
_ Pat
PNil = String
"[]"
    atomic :: Set.Set String -> Pat -> String
    atomic :: Set String -> Pat -> String
atomic Set String
used pat :: Pat
pat@(PCon String
_ (Pat
_ : [Pat]
_)) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set String -> Pat -> String
pattern' Set String
used Pat
pat String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    atomic Set String
used Pat
pat = Set String -> Pat -> String
pattern' Set String
used Pat
pat

tokens :: String -> [String]
tokens :: String -> [String]
tokens = String -> [String]
words (String -> [String]) -> (String -> String) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\Char
char -> if Char -> Bool
isAlphaNum Char
char Bool -> Bool -> Bool
|| Char
char Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
char Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\'' then Char
char else Char
' ')

matching :: Expression -> String -> Emitting [Qual]
matching :: Expression -> String -> Emitting [Qual]
matching (ExMeta Text
meta) String
var = Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
var
matching (ExAny Slot
slot) String
var = Meta -> String -> Emitting [Qual]
meta' (Slot -> Meta
Anon Slot
slot) String
var
matching Expression
ExXi String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExXi" []) (String -> String
single String
var)]
matching Expression
ExRoot String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExRoot" []) (String -> String
single String
var)]
matching Expression
ExTermination String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExTermination" []) (String -> String
single String
var)]
matching (ExFormation [Binding]
bds) String
var = do
  String
inner <- Emitting String
fresh
  [Qual]
rest <- [Binding] -> String -> Emitting [Qual]
bindings [Binding]
bds String
inner
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExFormation" [String -> Pat
PVar String
inner]) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
rest)
matching (ExDispatch Expression
expr Attribute
attr) String
var = do
  String
head' <- Emitting String
fresh
  String
attr' <- Emitting String
fresh
  [Qual]
attribute' <- Attribute -> String -> Emitting [Qual]
attribute Attribute
attr String
attr'
  [Qual]
expression <- Expression -> String -> Emitting [Qual]
matching Expression
expr String
head'
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExDispatch" [String -> Pat
PVar String
head', String -> Pat
PVar String
attr']) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
attribute' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
expression)
matching (ExApplication Expression
expr (ArTau Attribute
attr Expression
arg)) String
var = do
  String
head' <- Emitting String
fresh
  String
attr' <- Emitting String
fresh
  String
arg' <- Emitting String
fresh
  [Qual]
attribute' <- Attribute -> String -> Emitting [Qual]
attribute Attribute
attr String
attr'
  [Qual]
expression <- Expression -> String -> Emitting [Qual]
matching Expression
expr String
head'
  [Qual]
argument <- Expression -> String -> Emitting [Qual]
matching Expression
arg String
arg'
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExApplication" [String -> Pat
PVar String
head', String -> [Pat] -> Pat
PCon String
"ArTau" [String -> Pat
PVar String
attr', String -> Pat
PVar String
arg']]) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
attribute' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
expression [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
argument)
matching (ExApplication Expression
expr (ArAlpha Alpha
alpha Expression
arg)) String
var = do
  String
head' <- Emitting String
fresh
  String
alpha' <- Emitting String
fresh
  String
arg' <- Emitting String
fresh
  [Qual]
expression <- Expression -> String -> Emitting [Qual]
matching Expression
expr String
head'
  [Qual]
index <- Alpha -> String -> Emitting [Qual]
indexed Alpha
alpha String
alpha'
  [Qual]
argument <- Expression -> String -> Emitting [Qual]
matching Expression
arg String
arg'
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"ExApplication" [String -> Pat
PVar String
head', String -> [Pat] -> Pat
PCon String
"ArAlpha" [String -> Pat
PVar String
alpha', String -> Pat
PVar String
arg']]) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
expression [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
index [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
argument)
matching Expression
expr String
_ = String -> Emitting [Qual]
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"its pattern holds the term '%s', which only a rule of YAML can match" (Expression -> String
forall a. Show a => a -> String
show Expression
expr))

bindings :: [Binding] -> String -> Emitting [Qual]
bindings :: [Binding] -> String -> Emitting [Qual]
bindings [] String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen Pat
PNil (String -> String
single String
var)]
bindings [BiMeta Text
meta] String
var = Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
var
bindings [BiAny Slot
_] String
_ = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
bindings (BiMeta Text
meta : [Binding]
rest) String
var = do
  String
before <- Emitting String
fresh
  String
after <- Emitting String
fresh
  [Qual]
bound <- Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
before
  [Qual]
others <- [Binding] -> String -> Emitting [Qual]
bindings [Binding]
rest String
after
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (Pat -> Pat -> Pat
PPair (String -> Pat
PVar String
before) (String -> Pat
PVar String
after)) (String
"M.splits " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
bound [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
others)
bindings (BiAny Slot
_ : [Binding]
rest) String
var = do
  String
after <- Emitting String
fresh
  [Qual]
others <- [Binding] -> String -> Emitting [Qual]
bindings [Binding]
rest String
after
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (Pat -> Pat -> Pat
PPair (String -> Pat
PVar String
"_") (String -> Pat
PVar String
after)) (String
"M.splits " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
others)
bindings (Binding
bd : [Binding]
rest) String
var = do
  String
first <- Emitting String
fresh
  String
after <- Emitting String
fresh
  [Qual]
binding' <- Binding -> String -> Emitting [Qual]
binding Binding
bd String
first
  [Qual]
others <- [Binding] -> String -> Emitting [Qual]
bindings [Binding]
rest String
after
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (Pat -> Pat -> Pat
PCons (String -> Pat
PVar String
first) (String -> Pat
PVar String
after)) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
binding' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
others)

binding :: Binding -> String -> Emitting [Qual]
binding :: Binding -> String -> Emitting [Qual]
binding (BiVoid Attribute
attr) String
var = do
  String
attr' <- Emitting String
fresh
  [Qual]
attribute' <- Attribute -> String -> Emitting [Qual]
attribute Attribute
attr String
attr'
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiVoid" [String -> Pat
PVar String
attr']) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
attribute')
binding (BiTau Attribute
attr Expression
expr) String
var = do
  String
attr' <- Emitting String
fresh
  String
expr' <- Emitting String
fresh
  [Qual]
attribute' <- Attribute -> String -> Emitting [Qual]
attribute Attribute
attr String
attr'
  [Qual]
expression <- Expression -> String -> Emitting [Qual]
matching Expression
expr String
expr'
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiTau" [String -> Pat
PVar String
attr', String -> Pat
PVar String
expr']) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
attribute' [Qual] -> [Qual] -> [Qual]
forall a. [a] -> [a] -> [a]
++ [Qual]
expression)
binding (BiDelta (BtMeta Text
meta)) String
var = do
  String
data' <- Emitting String
fresh
  [Qual]
bound <- Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
data'
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiDelta" [String -> Pat
PVar String
data']) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
bound)
binding (BiDelta (BtAny Slot
_)) String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiDelta" [String -> Pat
PVar String
"_"]) (String -> String
single String
var)]
binding (BiDelta Bytes
bts) String
var = do
  String
data' <- Emitting String
fresh
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiDelta" [String -> Pat
PVar String
data']) (String -> String
single String
var), String -> Qual
Guard (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s == %s" String
data' (String -> String
parens (Bytes -> String
forall a. Show a => a -> String
show Bytes
bts)))]
binding (BiLambda (FnMeta Text
meta)) String
var = do
  String
func <- Emitting String
fresh
  [Qual]
bound <- Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
func
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiLambda" [String -> Pat
PVar String
func]) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: String -> Qual
Guard (String
"M.named " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
func) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
bound)
binding (BiLambda (FnAny Slot
_)) String
var = do
  String
func <- Emitting String
fresh
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiLambda" [String -> Pat
PVar String
func]) (String -> String
single String
var), String -> Qual
Guard (String
"M.named " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
func)]
binding (BiLambda (FnFresh Slot
_)) String
_ = String -> Emitting [Qual]
forall a. String -> Emitting a
refuse String
"its pattern asks for a fresh symbol"
binding (BiLambda Function
func) String
var = do
  String
func' <- Emitting String
fresh
  String
literal <- Function -> Emitting String
function Function
func
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"BiLambda" [String -> Pat
PVar String
func']) (String -> String
single String
var), String -> Qual
Guard (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s == %s" String
func' String
literal)]
binding Binding
bd String
_ = String -> Emitting [Qual]
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"its pattern holds the binding '%s' where a single binding stands" (Binding -> String
forall a. Show a => a -> String
show Binding
bd))

attribute :: Attribute -> String -> Emitting [Qual]
attribute :: Attribute -> String -> Emitting [Qual]
attribute (AtMeta Text
meta) String
var = Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
var
attribute (AtAny Slot
_) String
_ = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
attribute Attribute
attr String
var = (\String
literal -> [String -> Qual
Guard (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s == %s" String
var String
literal)]) (String -> [Qual]) -> Emitting String -> Emitting [Qual]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Emitting String
attributed Attribute
attr

indexed :: Alpha -> String -> Emitting [Qual]
indexed :: Alpha -> String -> Emitting [Qual]
indexed (AlMeta Text
meta) String
var = do
  String
index <- Emitting String
fresh
  [Qual]
bound <- Meta -> String -> Emitting [Qual]
meta' (Text -> Meta
Named Text
meta) String
index
  [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"Alpha" [String -> Pat
PVar String
index]) (String -> String
single String
var) Qual -> [Qual] -> [Qual]
forall a. a -> [a] -> [a]
: [Qual]
bound)
indexed (AlAny Slot
_) String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Pat -> String -> Qual
Gen (String -> [Pat] -> Pat
PCon String
"Alpha" [String -> Pat
PVar String
"_"]) (String -> String
single String
var)]
indexed (Alpha Int
idx) String
var = [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [String -> Qual
Guard (String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%s == Alpha %d" String
var Int
idx)]

meta' :: Meta -> String -> Emitting [Qual]
meta' :: Meta -> String -> Emitting [Qual]
meta' Meta
key String
var =
  Meta -> Emitting (Maybe String)
known Meta
key Emitting (Maybe String)
-> (Maybe String -> Emitting [Qual]) -> Emitting [Qual]
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just String
bound -> [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [String -> Qual
Guard (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s == %s" String
bound String
var)]
    Maybe String
Nothing -> Meta -> String -> Emitting ()
bind Meta
key String
var Emitting () -> Emitting [Qual] -> Emitting [Qual]
forall a b. Emitting a -> Emitting b -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Qual] -> Emitting [Qual]
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

prefixed :: String -> Expression -> [Meta]
prefixed :: String -> Expression -> [Meta]
prefixed String
prefix = [Meta] -> [Meta]
forall a. Eq a => [a] -> [a]
nub ([Meta] -> [Meta])
-> (Expression -> [Meta]) -> Expression -> [Meta]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> [Meta]
go
  where
    go :: Expression -> [Meta]
    go :: Expression -> [Meta]
go (ExMeta Text
meta)
      | String -> Text
T.pack String
prefix Text -> Text -> Bool
`T.isPrefixOf` Text
meta = [Text -> Meta
Named Text
meta]
    go (ExAny slot :: Slot
slot@(Slot Text
kind Int
_))
      | String -> Text
T.pack String
prefix Text -> Text -> Bool
`T.isPrefixOf` Text
kind = [Slot -> Meta
Anon Slot
slot]
    go (ExFormation [Binding]
bds) = [[Meta]] -> [Meta]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Expression -> [Meta]
go Expression
expr | BiTau Attribute
_ Expression
expr <- [Binding]
bds]
    go (ExApplication Expression
expr (ArTau Attribute
_ Expression
arg)) = Expression -> [Meta]
go Expression
expr [Meta] -> [Meta] -> [Meta]
forall a. [a] -> [a] -> [a]
++ Expression -> [Meta]
go Expression
arg
    go (ExApplication Expression
expr (ArAlpha Alpha
_ Expression
arg)) = Expression -> [Meta]
go Expression
expr [Meta] -> [Meta] -> [Meta]
forall a. [a] -> [a] -> [a]
++ Expression -> [Meta]
go Expression
arg
    go (ExDispatch Expression
expr Attribute
_) = Expression -> [Meta]
go Expression
expr
    go Expression
_ = []

condition :: Y.Condition -> Emitting String
condition :: Condition -> Emitting String
condition (Y.And [Condition]
conds) = String -> String
parens (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" && " ([String] -> String) -> Emitting [String] -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Condition -> Emitting String) -> [Condition] -> Emitting [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Condition -> Emitting String
condition [Condition]
conds
condition (Y.Or [Condition]
conds) = String -> String
parens (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" || " ([String] -> String) -> Emitting [String] -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Condition -> Emitting String) -> [Condition] -> Emitting [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Condition -> Emitting String
condition [Condition]
conds
condition (Y.Not Condition
cond) = (String
"not " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens (String -> String) -> Emitting String -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Condition -> Emitting String
condition Condition
cond
condition (Y.In [Attribute]
attrs [Binding]
bds) = Bool -> [Attribute] -> [Binding] -> Emitting String
present Bool
True [Attribute]
attrs [Binding]
bds
condition (Y.Disjoint [Attribute]
attrs [Binding]
bds) = Bool -> [Attribute] -> [Binding] -> Emitting String
present Bool
False [Attribute]
attrs [Binding]
bds
condition (Y.Eq (Y.CmpNum Number
left) (Y.CmpNum Number
right)) = String -> Maybe String -> Maybe String -> String
compared String
"==" (Maybe String -> Maybe String -> String)
-> Emitting (Maybe String) -> Emitting (Maybe String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Number -> Emitting (Maybe String)
number Number
left Emitting (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Number -> Emitting (Maybe String)
number Number
right
condition (Y.Gt (Y.CmpNum Number
left) (Y.CmpNum Number
right)) = String -> Maybe String -> Maybe String -> String
compared String
">" (Maybe String -> Maybe String -> String)
-> Emitting (Maybe String) -> Emitting (Maybe String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Number -> Emitting (Maybe String)
number Number
left Emitting (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Number -> Emitting (Maybe String)
number Number
right
condition (Y.Eq (Y.CmpAttr Attribute
left) (Y.CmpAttr Attribute
right)) = String -> Maybe String -> Maybe String -> String
compared String
"==" (Maybe String -> Maybe String -> String)
-> Emitting (Maybe String) -> Emitting (Maybe String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Emitting (Maybe String)
attr' Attribute
left Emitting (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Attribute -> Emitting (Maybe String)
attr' Attribute
right
  where
    attr' :: Attribute -> Emitting (Maybe String)
    attr' :: Attribute -> Emitting (Maybe String)
attr' (AtMeta Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
    attr' (AtAny Slot
_) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
    attr' Attribute
attr = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> Emitting String -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Emitting String
attributed Attribute
attr
condition (Y.Eq (Y.CmpExpr Expression
left) (Y.CmpExpr Expression
right)) = String -> Maybe String -> Maybe String -> String
compared String
"==" (Maybe String -> Maybe String -> String)
-> Emitting (Maybe String) -> Emitting (Maybe String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Expression -> Emitting (Maybe String)
built Bool
False Expression
left Emitting (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall a b. Emitting (a -> b) -> Emitting a -> Emitting b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> Expression -> Emitting (Maybe String)
built Bool
False Expression
right
condition (Y.Eq Comparable
_ Comparable
_) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"False"
condition (Y.Gt Comparable
_ Comparable
_) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"False"
condition (Y.NF Expression
expr) = String -> Expression -> Emitting String
asked String
"Ru.normalHeld nf" Expression
expr
condition (Y.Absolute Expression
expr) = String -> Expression -> Emitting String
asked String
"Ru.xiFree" Expression
expr
condition (Y.IsFormation (ExMeta Text
meta)) = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"False" (String
"Ru.isFormation " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
condition (Y.IsFormation (ExFormation [Binding]
_)) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"True"
condition (Y.IsFormation Expression
_) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"False"
condition (Y.Matches String
_ Expression
_) = String -> Emitting String
forall a. String -> Emitting a
refuse String
"its condition 'matches' needs a run of dataization"
condition (Y.PartOf Expression
_ Binding
_) = String -> Emitting String
forall a. String -> Emitting a
refuse String
"its condition 'part-of' is not compiled yet"

present :: Bool -> [Attribute] -> [Binding] -> Emitting String
present :: Bool -> [Attribute] -> [Binding] -> Emitting String
present Bool
every [Attribute]
attrs [Binding]
bds = do
  [Maybe String]
attrs' <- (Attribute -> Emitting (Maybe String))
-> [Attribute] -> Emitting [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Attribute -> Emitting (Maybe String)
attr' [Attribute]
attrs
  [Maybe String]
bds' <- (Binding -> Emitting (Maybe String))
-> [Binding] -> Emitting [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Binding -> Emitting (Maybe String)
bindingsOf [Binding]
bds
  String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Emitting String) -> String -> Emitting String
forall a b. (a -> b) -> a -> b
$
    if (Maybe String -> Bool) -> [Maybe String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe String -> Bool
forall a. Maybe a -> Bool
isJust [Maybe String]
attrs' Bool -> Bool -> Bool
&& (Maybe String -> Bool) -> [Maybe String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe String -> Bool
forall a. Maybe a -> Bool
isJust [Maybe String]
bds'
      then (if Bool
every then String -> String
forall a. a -> a
id else (String
"not " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens) (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s (`Ru.presentIn` concat %s) %s" (if Bool
every then String
"all" else String
"any") ([String] -> String
listed ((Maybe String -> String) -> [Maybe String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"") [Maybe String]
bds')) ([String] -> String
listed ((Maybe String -> String) -> [Maybe String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"") [Maybe String]
attrs')))
      else String
"False"
  where
    attr' :: Attribute -> Emitting (Maybe String)
    attr' :: Attribute -> Emitting (Maybe String)
attr' (AtMeta Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
    attr' (AtAny Slot
_) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
    attr' Attribute
attr = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> Emitting String -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Emitting String
attributed Attribute
attr
    bindingsOf :: Binding -> Emitting (Maybe String)
    bindingsOf :: Binding -> Emitting (Maybe String)
bindingsOf (BiMeta Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
    bindingsOf (BiAny Slot
_) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
    bindingsOf Binding
bd = ([String] -> String) -> Maybe [String] -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [String] -> String
listed (Maybe [String] -> Maybe String)
-> ([Maybe String] -> Maybe [String])
-> [Maybe String]
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe String] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Maybe String] -> Maybe String)
-> Emitting [Maybe String] -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding -> Emitting (Maybe String))
-> [Binding] -> Emitting [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Binding -> Emitting (Maybe String)
builtBinding Bool
False) [Binding
bd]

asked :: String -> Expression -> Emitting String
asked :: String -> Expression -> Emitting String
asked String
question (ExMeta Text
meta) = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"False" ((String
question String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ") String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
asked String
question (ExAny Slot
slot) = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"False" ((String
question String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ") String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> String)
-> Emitting (Maybe String) -> Emitting String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Slot -> Meta
Anon Slot
slot)
asked String
_ Expression
_ = String -> Emitting String
forall a. String -> Emitting a
refuse String
"its condition asks about a term that is no meta"

compared :: String -> Maybe String -> Maybe String -> String
compared :: String -> Maybe String -> Maybe String -> String
compared String
operator (Just String
left) (Just String
right) = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s %s" (String -> String
parens String
left) String
operator (String -> String
parens String
right)
compared String
_ Maybe String
_ Maybe String
_ = String
"False"

number :: Y.Number -> Emitting (Maybe String)
number :: Number -> Emitting (Maybe String)
number (Y.MetaIndex Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
number (Y.Length (BiMeta Text
meta)) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"length " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
number (Y.Domain (BiMeta Text
meta)) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"Ru.domainOf " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
number (Y.Literal Int
num) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just (Int -> String
forall a. Show a => a -> String
show Int
num))
number Number
_ = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing

built :: Bool -> Expression -> Emitting (Maybe String)
built :: Bool -> Expression -> Emitting (Maybe String)
built Bool
_ (ExMeta Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
built Bool
_ Expression
ExXi = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
"ExXi")
built Bool
_ Expression
ExRoot = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
"ExRoot")
built Bool
_ Expression
ExTermination = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just String
"ExTermination")
built Bool
checked (ExApplication Expression
ExRoot (ArTau Attribute
AtRho Expression
expr)) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> String -> String
forall a b. a -> b -> a
const String
"ExRoot") (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
expr
built Bool
checked (ExFormation [Binding]
bds) = do
  [Maybe (Either String String)]
parts <- (Binding -> Emitting (Maybe (Either String String)))
-> [Binding] -> Emitting [Maybe (Either String String)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Binding -> Emitting (Maybe (Either String String))
part [Binding]
bds
  Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Either String String] -> String
formation ([Either String String] -> String)
-> Maybe [Either String String] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe (Either String String)] -> Maybe [Either String String]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Maybe (Either String String)]
parts)
  where
    part :: Binding -> Emitting (Maybe (Either String String))
    part :: Binding -> Emitting (Maybe (Either String String))
part (BiMeta Text
meta) = (String -> Either String String)
-> Maybe String -> Maybe (Either String String)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Either String String
forall a b. a -> Either a b
Left (Maybe String -> Maybe (Either String String))
-> Emitting (Maybe String)
-> Emitting (Maybe (Either String String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
    part Binding
bd = (String -> Either String String)
-> Maybe String -> Maybe (Either String String)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Either String String
forall a b. b -> Either a b
Right (Maybe String -> Maybe (Either String String))
-> Emitting (Maybe String)
-> Emitting (Maybe (Either String String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Binding -> Emitting (Maybe String)
builtBinding Bool
checked Binding
bd
    formation :: [Either String String] -> String
    formation :: [Either String String] -> String
formation [Left String
var] = String
constructor String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var
    formation [Either String String]
parts = String
constructor String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens ([Either String String] -> String
joined [Either String String]
parts)
    joined :: [Either String String] -> String
    joined :: [Either String String] -> String
joined [Either String String]
parts
      | (Either String String -> Bool) -> [Either String String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Either String String -> Bool
isRight [Either String String]
parts = [String] -> String
listed [String
bd | Right String
bd <- [Either String String]
parts]
      | Bool
otherwise = String
"concat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
listed ((Either String String -> String)
-> [Either String String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> String)
-> (String -> String) -> Either String String -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> String
forall a. a -> a
id (\String
bd -> String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bd String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]")) [Either String String]
parts)
    isRight :: Either String String -> Bool
    isRight :: Either String String -> Bool
isRight (Right String
_) = Bool
True
    isRight (Left String
_) = Bool
False
    constructor :: String
    constructor :: String
constructor = if Bool
checked then String
"B.formed" else String
"ExFormation"
built Bool
checked (ExDispatch Expression
expr Attribute
attr) = do
  Maybe String
expr' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
expr
  Maybe String
attr' <- Attribute -> Emitting (Maybe String)
builtAttribute Attribute
attr
  Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"ExDispatch %s %s" (String -> String -> String)
-> Maybe String -> Maybe (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
expr' Maybe (String -> String) -> Maybe String -> Maybe String
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
attr')
built Bool
checked (ExApplication Expression
expr (ArTau Attribute
attr Expression
arg)) = do
  Maybe String
expr' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
expr
  Maybe String
attr' <- Attribute -> Emitting (Maybe String)
builtAttribute Attribute
attr
  Maybe String
arg' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
arg
  Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"ExApplication %s (ArTau %s %s)" (String -> String -> String -> String)
-> Maybe String -> Maybe (String -> String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
expr' Maybe (String -> String -> String)
-> Maybe String -> Maybe (String -> String)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
attr' Maybe (String -> String) -> Maybe String -> Maybe String
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
arg')
built Bool
checked (ExApplication Expression
expr (ArAlpha Alpha
alpha Expression
arg)) = do
  Maybe String
expr' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
expr
  Maybe String
alpha' <- Alpha -> Emitting (Maybe String)
builtAlpha Alpha
alpha
  Maybe String
arg' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
arg
  Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"ExApplication %s (ArAlpha %s %s)" (String -> String -> String -> String)
-> Maybe String -> Maybe (String -> String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
expr' Maybe (String -> String -> String)
-> Maybe String -> Maybe (String -> String)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
alpha' Maybe (String -> String) -> Maybe String -> Maybe String
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
arg')
built Bool
_ Expression
expr = String -> Emitting (Maybe String)
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"it builds the term '%s', which only a rule of YAML can build" (Expression -> String
forall a. Show a => a -> String
show Expression
expr))

builtBinding :: Bool -> Binding -> Emitting (Maybe String)
builtBinding :: Bool -> Binding -> Emitting (Maybe String)
builtBinding Bool
checked (BiTau Attribute
attr Expression
expr) = do
  Maybe String
attr' <- Attribute -> Emitting (Maybe String)
builtAttribute Attribute
attr
  Maybe String
expr' <- Bool -> Expression -> Emitting (Maybe String)
built Bool
checked Expression
expr
  Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"BiTau %s %s" (String -> String -> String)
-> Maybe String -> Maybe (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
attr' Maybe (String -> String) -> Maybe String -> Maybe String
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> String
parens Maybe String
expr')
builtBinding Bool
_ (BiVoid Attribute
attr) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String
"BiVoid " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens) (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Emitting (Maybe String)
builtAttribute Attribute
attr
builtBinding Bool
_ (BiDelta (BtMeta Text
meta)) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"BiDelta " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
builtBinding Bool
_ (BiDelta (BtAny Slot
_)) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
builtBinding Bool
_ (BiDelta Bytes
bts) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just (String
"BiDelta " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
parens (Bytes -> String
forall a. Show a => a -> String
show Bytes
bts)))
builtBinding Bool
_ (BiLambda (FnMeta Text
meta)) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"BiLambda " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
builtBinding Bool
_ (BiLambda (FnAny Slot
_)) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
builtBinding Bool
_ (BiLambda (FnFresh Slot
_)) = String -> Emitting (Maybe String)
forall a. String -> Emitting a
refuse String
"it builds a fresh symbol"
builtBinding Bool
_ (BiLambda Function
func) = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> (String -> String) -> String -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"BiLambda " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
parens (String -> Maybe String)
-> Emitting String -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Function -> Emitting String
function Function
func
builtBinding Bool
_ Binding
bd = String -> Emitting (Maybe String)
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"it builds the binding '%s'" (Binding -> String
forall a. Show a => a -> String
show Binding
bd))

builtBytes :: Bytes -> Emitting (Maybe String)
builtBytes :: Bytes -> Emitting (Maybe String)
builtBytes (BtMeta Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
builtBytes (BtAny Slot
slot) = Meta -> Emitting (Maybe String)
known (Slot -> Meta
Anon Slot
slot)
builtBytes Bytes
bts = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just (String -> String
parens (Bytes -> String
forall a. Show a => a -> String
show Bytes
bts)))

builtAttribute :: Attribute -> Emitting (Maybe String)
builtAttribute :: Attribute -> Emitting (Maybe String)
builtAttribute (AtMeta Text
meta) = Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
builtAttribute (AtAny Slot
_) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
builtAttribute Attribute
attr = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> Emitting String -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Attribute -> Emitting String
attributed Attribute
attr

builtAlpha :: Alpha -> Emitting (Maybe String)
builtAlpha :: Alpha -> Emitting (Maybe String)
builtAlpha (AlMeta Text
meta) = (String -> String) -> Maybe String -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
"Alpha " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (Maybe String -> Maybe String)
-> Emitting (Maybe String) -> Emitting (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
meta)
builtAlpha (AlAny Slot
_) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
builtAlpha (Alpha Int
idx) = Maybe String -> Emitting (Maybe String)
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"Alpha %d" Int
idx))

attributed :: Attribute -> Emitting String
attributed :: Attribute -> Emitting String
attributed (AtLabel Text
label) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"AtLabel (%s)" (Text -> String
texted Text
label))
attributed Attribute
AtPhi = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"AtPhi"
attributed Attribute
AtRho = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"AtRho"
attributed Attribute
AtLambda = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"AtLambda"
attributed Attribute
AtDelta = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"AtDelta"
attributed Attribute
attr = String -> Emitting String
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"it holds the attribute '%s' where a literal one stands" (Attribute -> String
forall a. Show a => a -> String
show Attribute
attr))

function :: Function -> Emitting String
function :: Function -> Emitting String
function (Function Text
name) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Function (%s)" (Text -> String
texted Text
name))
function (FnSymbol Int
idx) = String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"FnSymbol %d" Int
idx)
function Function
func = String -> Emitting String
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"it holds the λ function '%s' where a literal one stands" (Function -> String
forall a. Show a => a -> String
show Function
func))

texted :: T.Text -> String
texted :: Text -> String
texted Text
text = String
"T.pack " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Text -> String
T.unpack Text
text)

rooted :: Expression -> Bool
rooted :: Expression -> Bool
rooted (ExApplication Expression
ExRoot (ArTau Attribute
AtRho Expression
_)) = Bool
True
rooted (ExApplication Expression
expr (ArTau Attribute
_ Expression
arg)) = Expression -> Bool
rooted Expression
expr Bool -> Bool -> Bool
|| Expression -> Bool
rooted Expression
arg
rooted (ExApplication Expression
expr (ArAlpha Alpha
_ Expression
arg)) = Expression -> Bool
rooted Expression
expr Bool -> Bool -> Bool
|| Expression -> Bool
rooted Expression
arg
rooted (ExDispatch Expression
expr Attribute
_) = Expression -> Bool
rooted Expression
expr
rooted (ExFormation [Binding]
bds) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Expression -> Bool
rooted Expression
expr | BiTau Attribute
_ Expression
expr <- [Binding]
bds]
rooted Expression
_ = Bool
False

known :: Meta -> Emitting (Maybe String)
known :: Meta -> Emitting (Maybe String)
known Meta
key = (Scope -> Either String (Maybe String, Scope))
-> Emitting (Maybe String)
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting (\scope :: Scope
scope@(Scope Map Meta String
bound Int
_) -> (Maybe String, Scope) -> Either String (Maybe String, Scope)
forall a b. b -> Either a b
Right (Meta -> Map Meta String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Meta
key Map Meta String
bound, Scope
scope))

held :: Meta -> Emitting String
held :: Meta -> Emitting String
held Meta
key = Meta -> Emitting (Maybe String)
known Meta
key Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Emitting String
-> (String -> Emitting String) -> Maybe String -> Emitting String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Emitting String
forall a. String -> Emitting a
refuse String
"it asks a normal form of a meta its pattern does not bind") String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

bind :: Meta -> String -> Emitting ()
bind :: Meta -> String -> Emitting ()
bind Meta
key String
var = (Scope -> Either String ((), Scope)) -> Emitting ()
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting (\(Scope Map Meta String
bound Int
next) -> ((), Scope) -> Either String ((), Scope)
forall a b. b -> Either a b
Right ((), Map Meta String -> Int -> Scope
Scope (Meta -> String -> Map Meta String -> Map Meta String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Meta
key String
var Map Meta String
bound) Int
next))

fresh :: Emitting String
fresh :: Emitting String
fresh = (Scope -> Either String (String, Scope)) -> Emitting String
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting (\(Scope Map Meta String
bound Int
next) -> (String, Scope) -> Either String (String, Scope)
forall a b. b -> Either a b
Right (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
next, Map Meta String -> Int -> Scope
Scope Map Meta String
bound (Int
next Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)))

introduced :: T.Text -> Emitting String
introduced :: Text -> Emitting String
introduced Text
result =
  Meta -> Emitting (Maybe String)
known (Text -> Meta
Named Text
result) Emitting (Maybe String)
-> (Maybe String -> Emitting String) -> Emitting String
forall a b. Emitting a -> (a -> Emitting b) -> Emitting b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just String
_ -> String -> Emitting String
forall a. String -> Emitting a
refuse (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"its premise '%s' binds a meta bound already" (Text -> String
T.unpack Text
result))
    Maybe String
Nothing -> do
      let var :: String
var = Meta -> String
variable (Text -> Meta
Named Text
result)
      Meta -> String -> Emitting ()
bind (Text -> Meta
Named Text
result) String
var
      String -> Emitting String
forall a. a -> Emitting a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
var

refuse :: String -> Emitting a
refuse :: forall a. String -> Emitting a
refuse String
reason = (Scope -> Either String (a, Scope)) -> Emitting a
forall a. (Scope -> Either String (a, Scope)) -> Emitting a
Emitting (Either String (a, Scope) -> Scope -> Either String (a, Scope)
forall a b. a -> b -> a
const (String -> Either String (a, Scope)
forall a b. a -> Either a b
Left String
reason))

variable :: Meta -> String
variable :: Meta -> String
variable (Named Text
meta) = case Text -> String
T.unpack Text
meta of
  Char
first : String
rest | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
rest -> Char -> Char
toLower Char
first Char -> String -> String
forall a. a -> [a] -> [a]
: String
rest
  String
name -> String
"m_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\Char
char -> if Char -> Bool
isAlphaNum Char
char then Char
char else Char
'_') String
name
variable (Anon (Slot Text
kind Int
offset)) = String -> String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"a_%s%d" (Text -> String
T.unpack Text
kind) Int
offset

single :: String -> String
single :: String -> String
single String
var = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"

listed :: [String] -> String
listed :: [String] -> String
listed [String]
items = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
items String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"

listed' :: Int -> [String] -> String
listed' :: Int -> [String] -> String
listed' Int
_ [] = String
"[]"
listed' Int
indent [String]
items = String
"[ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", ") [String]
items String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"

parens :: String -> String
parens :: String -> String
parens String
text
  | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Char
char -> Char -> Bool
isAlphaNum Char
char Bool -> Bool -> Bool
|| Char
char Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
char Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\'') String
text = String
text
  | Bool
otherwise = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
text String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"