Skip to content

Commit

Permalink
Merge pull request #9 from objectionary/rule-1
Browse files Browse the repository at this point in the history
  • Loading branch information
fizruk authored Jan 13, 2024
2 parents 067dcc3 + 2494f11 commit b43f6e3
Show file tree
Hide file tree
Showing 18 changed files with 378 additions and 150 deletions.
15 changes: 12 additions & 3 deletions eo-phi-normalizer/eo-phi-normalizer.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,9 @@ library
exposed-modules:
Language.EO.Phi
Language.EO.Phi.Normalize
Language.EO.Phi.Rules.Common
Language.EO.Phi.Rules.PhiPaper
Language.EO.Phi.Syntax
Language.EO.Phi.Syntax.Abs
Language.EO.Phi.Syntax.Lex
Language.EO.Phi.Syntax.Par
Expand All @@ -42,7 +45,7 @@ library
Paths_eo_phi_normalizer
hs-source-dirs:
src
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror
build-tools:
alex >=3.2.4
, happy >=1.19.9
Expand All @@ -54,6 +57,8 @@ library
, base >=4.7 && <5
, directory
, filepath
, mtl
, string-interpolate
, yaml
default-language: Haskell2010

Expand All @@ -63,7 +68,7 @@ executable normalize-phi
Paths_eo_phi_normalizer
hs-source-dirs:
app
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -threaded -rtsopts -with-rtsopts=-N
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror -threaded -rtsopts -with-rtsopts=-N
build-tools:
alex >=3.2.4
, happy >=1.19.9
Expand All @@ -76,6 +81,8 @@ executable normalize-phi
, directory
, eo-phi-normalizer
, filepath
, mtl
, string-interpolate
, yaml
default-language: Haskell2010

Expand All @@ -88,7 +95,7 @@ test-suite eo-phi-normalizer-test
Paths_eo_phi_normalizer
hs-source-dirs:
test
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -threaded -rtsopts -with-rtsopts=-N
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror -threaded -rtsopts -with-rtsopts=-N
build-tools:
alex >=3.2.4
, happy >=1.19.9
Expand All @@ -103,5 +110,7 @@ test-suite eo-phi-normalizer-test
, filepath
, hspec
, hspec-discover
, mtl
, string-interpolate
, yaml
default-language: Haskell2010
6 changes: 3 additions & 3 deletions eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
Original file line number Diff line number Diff line change
Expand Up @@ -27,17 +27,17 @@ separator Binding "," ;
Phi. Attribute ::= "φ" ; -- decoratee object
Rho. Attribute ::= "ρ" ; -- parent object
Sigma. Attribute ::= "σ" ; -- home object
VTX. Attribute ::= "ν" ; -- ???
VTX. Attribute ::= "ν" ; -- the vertex identifier (an object that represents the unique identifier of the containing object)
Label. Attribute ::= LabelId ;
Alpha. Attribute ::= AlphaIndex ;

PeeledObject. PeeledObject ::= ObjectHead [ObjectAction] ;

HeadFormation. ObjectHead ::= "{" [Binding] "}" ;
HeadFormation. ObjectHead ::= "" [Binding] "" ;
HeadGlobal. ObjectHead ::= "Φ" ;
HeadThis. ObjectHead ::= "ξ" ;
HeadTermination. ObjectHead ::= "⊥" ;

ActionApplication. ObjectAction ::= "{" [Binding] "}" ;
ActionApplication. ObjectAction ::= "(" [Binding] ")" ;
ActionDispatch. ObjectAction ::= "." Attribute ;
separator ObjectAction "" ;
3 changes: 3 additions & 0 deletions eo-phi-normalizer/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ dependencies:
- directory
- filepath
- yaml
- mtl
- string-interpolate

ghc-options:
- -Wall
Expand All @@ -53,6 +55,7 @@ ghc-options:
- -Wpartial-fields
- -Wredundant-constraints
- -Wno-missing-export-lists
- -Werror

library:
source-dirs: src
Expand Down
83 changes: 2 additions & 81 deletions eo-phi-normalizer/src/Language/EO/Phi.hs
Original file line number Diff line number Diff line change
@@ -1,23 +1,18 @@
{-# LANGUAGE LambdaCase #-}

module Language.EO.Phi (
defaultMain,
normalize,
parseProgram,
unsafeParseProgram,
printTree,
module Language.EO.Phi.Syntax.Abs,
module Language.EO.Phi.Syntax,
) where

import Data.Char (isSpace)
import System.Exit (exitFailure)

import Language.EO.Phi.Syntax.Abs
import qualified Language.EO.Phi.Syntax.Abs as Phi
import qualified Language.EO.Phi.Syntax.Par as Phi
import qualified Language.EO.Phi.Syntax.Print as Phi

import Language.EO.Phi.Normalize
import Language.EO.Phi.Syntax

-- | Parse a 'Program' or return a parsing error.
parseProgram :: String -> Either String Phi.Program
Expand Down Expand Up @@ -46,77 +41,3 @@ defaultMain = do
exitFailure
Right program -> do
putStrLn (printTree (normalize program))

-- * Overriding generated pretty-printer

-- | Like 'Phi.printTree', but without spaces around dots and no indentation for curly braces.
printTree :: (Phi.Print a) => a -> String
printTree = shrinkDots . render . Phi.prt 0

-- | Remove spaces around dots.
--
-- >>> putStrLn (shrinkDots "a ↦ ξ . a")
-- a ↦ ξ.a
shrinkDots :: String -> String
shrinkDots [] = []
shrinkDots (' ' : '.' : ' ' : cs) = '.' : shrinkDots cs
shrinkDots (c : cs) = c : shrinkDots cs

-- | Copy of 'Phi.render', except no indentation is made for curly braces.
render :: Phi.Doc -> String
render d = rend 0 False (map ($ "") $ d []) ""
where
rend ::
Int ->
-- \^ Indentation level.
Bool ->
-- \^ Pending indentation to be output before next character?
[String] ->
ShowS
rend i p = \case
"[" : ts -> char '[' . rend i False ts
"(" : ts -> char '(' . rend i False ts
-- "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts
-- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
-- "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts
[";"] -> char ';'
";" : ts -> char ';' . new i ts
t : ts@(s : _)
| closingOrPunctuation s ->
pending . showString t . rend i False ts
t : ts -> pending . space t . rend i False ts
[] -> id
where
-- Output character after pending indentation.
char :: Char -> ShowS
char c = pending . showChar c

-- Output pending indentation.
pending :: ShowS
pending = if p then indent i else id

-- Indentation (spaces) for given indentation level.
indent :: Int -> ShowS
indent i = Phi.replicateS (2 * i) (showChar ' ')

-- Continue rendering in new line with new indentation.
new :: Int -> [String] -> ShowS
new j ts = showChar '\n' . rend j True ts

-- Separate given string from following text by a space (if needed).
space :: String -> ShowS
space t s =
case (all isSpace t, null spc, null rest) of
(True, _, True) -> [] -- remove trailing space
(False, _, True) -> t -- remove trailing space
(False, True, False) -> t ++ ' ' : s -- add space if none
_ -> t ++ s
where
(spc, rest) = span isSpace s

closingOrPunctuation :: String -> Bool
closingOrPunctuation [c] = c `elem` closerOrPunct
closingOrPunctuation _ = False

closerOrPunct :: String
closerOrPunct = ")],;"
79 changes: 61 additions & 18 deletions eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
Original file line number Diff line number Diff line change
@@ -1,44 +1,87 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}

module Language.EO.Phi.Normalize where
module Language.EO.Phi.Normalize (
normalizeObject,
normalize,
peelObject,
unpeelObject,
) where

import Control.Monad.State
import Data.Maybe (fromMaybe)
import Numeric (showHex)

import Control.Monad (forM)
import Language.EO.Phi.Syntax.Abs
import Language.EO.Phi.Rules.Common (lookupBinding)

data Context = Context
{ globalObject :: [Binding]
, thisObject :: [Binding]
, totalNuCount :: Int
}

lookupBinding :: Attribute -> [Binding] -> Maybe Object
lookupBinding _ [] = Nothing
lookupBinding a (AlphaBinding a' object : bindings)
| a == a' = Just object
| otherwise = lookupBinding a bindings
lookupBinding _ _ = Nothing
isNu :: Binding -> Bool
isNu (AlphaBinding VTX _) = True
isNu (EmptyBinding VTX) = True
isNu _ = False

-- | Normalize an input 𝜑-program.
normalize :: Program -> Program
normalize (Program bindings) = Program (map (normalizeBindingWith context) bindings)
normalize (Program bindings) = evalState (Program . objectBindings <$> normalizeObject (Formation bindings)) context
where
context =
Context
{ globalObject = bindings
, thisObject = bindings
, totalNuCount = nuCount bindings
}
nuCount binds = count isNu binds + sum (map (sum . map (nuCount . objectBindings) . values) binds)
count = (length .) . filter
values (AlphaBinding _ obj) = [obj]
values _ = []
objectBindings (Formation bs) = bs
objectBindings _ = []

normalizeBindingWith :: Context -> Binding -> Binding
normalizeBindingWith context = \case
AlphaBinding a object -> AlphaBinding a (normalizeObjectWith context object)
binding -> binding
rule1 :: Object -> State Context Object
rule1 (Formation bindings) = do
normalizedBindings <- forM bindings $ \case
AlphaBinding a object
| a /= VTX ->
do
object' <- rule1 object
pure (AlphaBinding a object')
b -> pure b
finalBindings <-
if not $ any isNu normalizedBindings
then do
nus <- gets totalNuCount
modify (\c -> c{totalNuCount = totalNuCount c + 1})
let pad s = (if even (length s) then "" else "0") ++ s
let insertDashes s
| length s <= 2 = s ++ "-"
| otherwise =
let go = \case
[] -> []
[x] -> [x]
[x, y] -> [x, y, '-']
(x : y : xs) -> x : y : '-' : go xs
in go s
let dataObject = Formation [DeltaBinding $ Bytes $ insertDashes $ pad $ showHex nus ""]
pure (AlphaBinding VTX dataObject : normalizedBindings)
else do
pure normalizedBindings
pure (Formation finalBindings)
rule1 object = pure object

normalizeObjectWith :: Context -> Object -> Object
normalizeObjectWith Context{..} object =
normalizeObject :: Object -> State Context Object
normalizeObject object = do
this <- gets thisObject
case object of
ThisDispatch a ->
fromMaybe object (lookupBinding a thisObject)
_ -> object
-- Rule 1
obj@(Formation _) -> rule1 obj
ThisDispatch a -> pure $ fromMaybe object (lookupBinding a this)
_ -> pure object

-- | Split compound object into its head and applications/dispatch actions.
peelObject :: Object -> PeeledObject
Expand Down
88 changes: 88 additions & 0 deletions eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
module Language.EO.Phi.Rules.Common where

import Language.EO.Phi.Syntax.Abs
import Control.Applicative (asum, Alternative ((<|>)))

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import Language.EO.Phi.Syntax

data Context = Context
{ allRules :: [Rule]
}

-- | A rule tries to apply a transformation to the root object, if possible.
type Rule = Context -> Object -> Maybe Object

applyOneRuleAtRoot :: Context -> Object -> [Object]
applyOneRuleAtRoot ctx@Context{..} obj =
[ obj'
| rule <- allRules
, Just obj' <- [rule ctx obj]
]

withSubObject :: (Object -> [Object]) -> Object -> [Object]
withSubObject f root = f root <|>
case root of
Formation bindings ->
Formation <$> withSubObjectBindings f bindings
Application obj bindings -> asum
[ Application <$> withSubObject f obj <*> pure bindings
, Application obj <$> withSubObjectBindings f bindings
]
ObjectDispatch obj a -> ObjectDispatch <$> withSubObject f obj <*> pure a
GlobalDispatch{} -> []
ThisDispatch{} -> []
Termination -> []

withSubObjectBindings :: (Object -> [Object]) -> [Binding] -> [[Binding]]
withSubObjectBindings _ [] = []
withSubObjectBindings f (b:bs) = asum
[ [ b' : bs | b' <- withSubObjectBinding f b ]
, [ b : bs' | bs' <- withSubObjectBindings f bs ]
]

withSubObjectBinding :: (Object -> [Object]) -> Binding -> [Binding]
withSubObjectBinding f = \case
AlphaBinding a obj -> AlphaBinding a <$> withSubObject f obj
EmptyBinding{} -> []
DeltaBinding{} -> []
LambdaBinding{} -> []

applyOneRule :: Context -> Object -> [Object]
applyOneRule = withSubObject . applyOneRuleAtRoot

isNF :: Context -> Object -> Bool
isNF ctx = null . applyOneRule ctx

-- | Apply rules until we get a normal form.
--
-- >>> mapM_ (putStrLn . Language.EO.Phi.printTree) (applyRules (Context [rule6]) "⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧.b ⟧.a")
-- ⟦ ⟧ (ρ ↦ ⟦ ⟧) (ρ ↦ ⟦ ⟧)
applyRules :: Context -> Object -> [Object]
applyRules ctx obj
| isNF ctx obj = [obj]
| otherwise =
[ obj''
| obj' <- applyOneRule ctx obj
, obj'' <- applyRules ctx obj' ]

applyRulesChain :: Context -> Object -> [[Object]]
applyRulesChain ctx obj
| isNF ctx obj = [[obj]]
| otherwise =
[ obj : chain
| obj' <- applyOneRule ctx obj
, chain <- applyRulesChain ctx obj' ]

-- * Helpers

-- | Lookup a binding by the attribute name.
lookupBinding :: Attribute -> [Binding] -> Maybe Object
lookupBinding _ [] = Nothing
lookupBinding a (AlphaBinding a' object : bindings)
| a == a' = Just object
| otherwise = lookupBinding a bindings
lookupBinding _ _ = Nothing
Loading

0 comments on commit b43f6e3

Please sign in to comment.