mirror of
https://github.com/urbit/shrub.git
synced 2024-12-01 06:35:32 +03:00
Moved language stuff to another branch.
This commit is contained in:
Benjamin Summers
parent
91561f10cd
commit
1408d2bcd7
2
pkg/hs-conq/.gitignore
vendored
2
pkg/hs-conq/.gitignore
vendored
@ -1,2 +0,0 @@
|
||||
.stack-work
|
||||
*.cabal
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,138 +0,0 @@
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
|
||||
module Language.Conq.Axe where
|
||||
|
||||
import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
|
||||
|
||||
import Language.Conq.Types
|
||||
import Language.Conq.Exp
|
||||
|
||||
import Data.Type.Equality
|
||||
import Type.Reflection
|
||||
import Data.Coerce
|
||||
import GHC.Natural
|
||||
import Control.Category
|
||||
import Data.Flat
|
||||
import Data.Flat.Bits
|
||||
import Data.Bits
|
||||
import Data.Vector (generate)
|
||||
import Data.Monoid.Unicode ((∅))
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Control.Lens ((&))
|
||||
import Control.Monad.Except (ExceptT, runExceptT)
|
||||
import Control.Monad.State (State, get, put, evalState, runState)
|
||||
import Control.Monad.Trans.Except (throwE)
|
||||
import Data.Bits ((.|.), shiftL, shiftR)
|
||||
import System.IO.Unsafe (unsafePerformIO)
|
||||
import Text.Show (showString, showParen)
|
||||
|
||||
import qualified Prelude as P
|
||||
import qualified Crypto.Hash.SHA256 as SHA256
|
||||
import qualified Data.ByteString.Base58 as Base58
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.ByteString.Unsafe as B
|
||||
|
||||
|
||||
-- Utils -----------------------------------------------------------------------
|
||||
|
||||
lef = ATong (singleton F)
|
||||
rit = ATong (singleton T)
|
||||
|
||||
sut = AAxis []
|
||||
hed = AAxis [F]
|
||||
tel = AAxis [T]
|
||||
|
||||
showFlatAxe :: Axe -> IO ()
|
||||
showFlatAxe a = putStrLn $ pack
|
||||
$ filter (\x -> x=='0' || x=='1')
|
||||
$ show
|
||||
$ fmap (\x -> if x then 1 else 0)
|
||||
$ toList (bits a)
|
||||
|
||||
|
||||
-- Encode Axes to Vals ---------------------------------------------------------
|
||||
|
||||
intVal :: Int -> Val
|
||||
intVal n | n <= 0 = V0 VN
|
||||
intVal n = V1 (intVal (n-1))
|
||||
|
||||
typeVal :: TyExp -> Val
|
||||
typeVal = \case
|
||||
TENil -> V0 $ V0 $ V0 $ VN
|
||||
TESum x y -> V0 $ V0 $ V1 $ VP (typeVal x) (typeVal y)
|
||||
TETup x y -> V0 $ V1 $ V0 $ VP (typeVal x) (typeVal y)
|
||||
TEFor x y -> V0 $ V1 $ V1 $ VP (typeVal x) (typeVal y)
|
||||
TEAll x -> V1 $ V0 $ V0 $ typeVal x
|
||||
TEFix x -> V1 $ V0 $ V1 $ typeVal x
|
||||
TERef i -> V1 $ V1 $ V0 $ intVal i
|
||||
|
||||
axeVal :: Axe -> Val
|
||||
axeVal = \case
|
||||
AAxis ds -> V0 $ V0 $ V0 $ flagsVal ds
|
||||
APure v -> V0 $ V0 $ V1 $ v
|
||||
AEval -> V0 $ V1 $ V0 $ VN
|
||||
ATong ts -> V0 $ V1 $ V1 $ flagsValNE ts
|
||||
ACons x y -> V1 $ V0 $ V0 $ VP (axeVal x) (axeVal y)
|
||||
ACase x y -> V1 $ V0 $ V1 $ VP (axeVal x) (axeVal y)
|
||||
AWith x y -> V1 $ V1 $ V0 $ VP (axeVal x) (axeVal y)
|
||||
AHint h -> V1 $ V1 $ V1 $ hintVal h
|
||||
where
|
||||
hintVal :: Hint -> Val
|
||||
hintVal HLazy = V0 $ V0 VN
|
||||
hintVal HMark = V0 $ V1 VN
|
||||
hintVal (HType t) = V1 $ V0 (typeVal t)
|
||||
hintVal HFast = V1 $ V1 VN
|
||||
|
||||
flagsVal :: [Flag] -> Val
|
||||
flagsVal [] = V0 VN
|
||||
flagsVal (F:bs) = V1 (VP (V0 VN) (flagsVal bs))
|
||||
flagsVal (T:bs) = V1 (VP (V1 VN) (flagsVal bs))
|
||||
|
||||
flagsValNE :: NonEmpty Flag -> Val
|
||||
flagsValNE (F :| []) = V0 (V0 VN)
|
||||
flagsValNE (T :| []) = V0 (V1 VN)
|
||||
flagsValNE (F :| b:bs) = V1 (VP (V0 VN) (flagsValNE (b :| bs)))
|
||||
flagsValNE (T :| b:bs) = V1 (VP (V1 VN) (flagsValNE (b :| bs)))
|
||||
|
||||
axeExp :: Axe -> Exp
|
||||
axeExp = \case
|
||||
AAxis [] -> ESubj
|
||||
AAxis [F] -> EHead
|
||||
AAxis [T] -> ETail
|
||||
AAxis (F:ds) -> axeExp (AAxis ds) <> EHead
|
||||
AAxis (T:ds) -> axeExp (AAxis ds) <> ETail
|
||||
APure VN -> EPure VN
|
||||
APure v -> valExp v
|
||||
AEval -> EEval
|
||||
ATong (F :| []) -> ELeft
|
||||
ATong (T :| []) -> EWrit
|
||||
ATong (F :| t:ts) -> axeExp (ATong (t :| ts)) <> ELeft
|
||||
ATong (T :| t:ts) -> axeExp (ATong (t :| ts)) <> EWrit
|
||||
ACons x y -> ECons (axeExp x) (axeExp y)
|
||||
ACase x y -> ECase (axeExp x) (axeExp y)
|
||||
AWith x y -> axeExp y <> axeExp x
|
||||
AHint HLazy -> ELazy
|
||||
AHint HMark -> EMark
|
||||
AHint (HType ty) -> EType ty
|
||||
AHint HFast -> EFast
|
||||
|
||||
expAxe :: Exp -> Axe
|
||||
expAxe = \case
|
||||
ESubj -> AAxis []
|
||||
EPure v -> APure v
|
||||
EEval -> AEval
|
||||
ELeft -> ATong (singleton F)
|
||||
EWrit -> ATong (singleton T)
|
||||
EHead -> AAxis (singleton F)
|
||||
ETail -> AAxis (singleton T)
|
||||
EDist -> ACase (expAxe ELeft) (expAxe EWrit)
|
||||
EWith x y -> AWith (expAxe x) (expAxe y)
|
||||
ECons x y -> ACons (expAxe x) (expAxe y)
|
||||
ECase x y -> ACase (expAxe x) (expAxe y) -- TODO Wrong
|
||||
EType ty -> AHint (HType ty)
|
||||
EMark -> AHint HMark
|
||||
ELazy -> AHint HMark -- TODO
|
||||
EFast -> AHint HFast
|
||||
EQuot e -> APure (axeVal (expAxe e)) -- TODO Unquoting
|
||||
ETape e -> expAxe (EQuot (ETape e))
|
||||
@ -1,130 +0,0 @@
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
|
||||
module Language.Conq.Exp where
|
||||
|
||||
import Language.Conq.Types
|
||||
import Language.Conq.Grainary
|
||||
|
||||
import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
|
||||
import Data.Type.Equality
|
||||
import Type.Reflection
|
||||
import Data.Coerce
|
||||
import GHC.Natural
|
||||
import Control.Category
|
||||
import Data.Flat
|
||||
import Data.Flat.Bits
|
||||
import Data.Bits
|
||||
import Data.Vector (generate)
|
||||
import Data.Monoid.Unicode ((∅))
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Control.Lens ((&))
|
||||
import Control.Monad.Except (ExceptT, runExceptT)
|
||||
import Control.Monad.State (State, get, put, evalState, runState)
|
||||
import Control.Monad.Trans.Except (throwE)
|
||||
import Data.Bits ((.|.), shiftL, shiftR)
|
||||
import System.IO.Unsafe (unsafePerformIO)
|
||||
import Text.Show (showString, showParen)
|
||||
|
||||
import qualified Prelude as P
|
||||
import qualified Crypto.Hash.SHA256 as SHA256
|
||||
import qualified Data.ByteString.Base58 as Base58
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.ByteString.Unsafe as B
|
||||
|
||||
|
||||
-- Unparsing -------------------------------------------------------------------
|
||||
|
||||
dispExp :: Exp -> String
|
||||
dispExp = \case
|
||||
ESubj -> "."
|
||||
EPure VN -> "~"
|
||||
EPure v -> show (valExp v)
|
||||
EEval -> "!"
|
||||
ELeft -> "0"
|
||||
EWrit -> "1"
|
||||
EHead -> "-"
|
||||
ETail -> "+"
|
||||
EDist -> "%"
|
||||
EWith x y -> show y <> show x
|
||||
ECons x y -> "[" <> show x <> " " <> show y <> "]"
|
||||
ECase x y -> "<" <> show x <> " " <> show y <> ">"
|
||||
EType t -> "{" <> show t <> "}"
|
||||
ELazy -> "?"
|
||||
EFast -> "_"
|
||||
ETape e -> "$(" <> dispExp e <> ")"
|
||||
EMark -> "@"
|
||||
EQuot x -> "(" <> show x <> ")"
|
||||
|
||||
valExp :: Val -> Exp
|
||||
valExp (valFor' -> Just e) = EQuot e
|
||||
valExp VN = EPure VN
|
||||
valExp VV = crash
|
||||
valExp v = go v <> EPure VN
|
||||
where
|
||||
go = \case
|
||||
(valFor' → Just e) → EQuot e
|
||||
VV → crash
|
||||
VN → ESubj
|
||||
V0 VN → ELeft
|
||||
V1 VN → EWrit
|
||||
V0 l → ELeft <> go l
|
||||
V1 r → EWrit <> go r
|
||||
VP x y → ECons (go x) (go y)
|
||||
VT x y _r → ECons (go x) y
|
||||
VR k → EMark <> go (getGrain k)
|
||||
|
||||
crash :: Exp
|
||||
crash = EEval <> EEval <> (EPure VN)
|
||||
|
||||
|
||||
-- Parsing ---------------------------------------------------------------------
|
||||
|
||||
parseSimpl :: String -> Maybe (Exp, String)
|
||||
parseSimpl = \case
|
||||
'.' : xs -> pure (ESubj, xs)
|
||||
'~' : xs -> pure (EPure VN, xs) -- TODO EPure
|
||||
'!' : xs -> pure (EEval, xs)
|
||||
'0' : xs -> pure (ELeft, xs)
|
||||
'1' : xs -> pure (EWrit, xs)
|
||||
'-' : xs -> pure (EHead, xs)
|
||||
'+' : xs -> pure (ETail, xs)
|
||||
'%' : xs -> pure (EDist, xs)
|
||||
'?' : xs -> pure (ELazy, xs)
|
||||
'@' : xs -> pure (EMark, xs)
|
||||
_ -> Nothing
|
||||
|
||||
parseExp :: String -> Either String (Exp, String)
|
||||
parseExp str = do
|
||||
case parseSimpl str of
|
||||
Just (e, xs) -> pure (e, xs)
|
||||
Nothing ->
|
||||
case str of
|
||||
'[':xs -> parseTwo ECons ']' xs
|
||||
'<':xs -> parseTwo ECase '>' xs
|
||||
'(':xs -> parseSeq ')' xs <&> \case
|
||||
(e,cs) -> (EQuot e, cs)
|
||||
_ -> P.Left "bad"
|
||||
|
||||
parseSeq :: Char -> String -> Either String (Exp, String)
|
||||
parseSeq end = go >=> \case
|
||||
(Just x, buf) -> pure (x, buf)
|
||||
(Nothing, buf) -> P.Left "empty sequence"
|
||||
where
|
||||
go :: String -> Either String (Maybe Exp, String)
|
||||
go = \case
|
||||
[] -> pure (Nothing, [])
|
||||
c : cd | c == end -> pure (Nothing, cd)
|
||||
cs -> do
|
||||
(x, buf) <- parseExp cs
|
||||
(y, buf) <- go buf
|
||||
case y of
|
||||
Nothing -> pure (Just x, buf)
|
||||
Just y -> pure (Just (x <> y), buf)
|
||||
|
||||
parseTwo :: (Exp -> Exp -> Exp) -> Char -> String
|
||||
-> Either String (Exp, String)
|
||||
parseTwo cntr end buf = do
|
||||
(xs, buf) <- parseSeq ' ' buf
|
||||
(ys, buf) <- parseSeq end buf
|
||||
pure (cntr xs ys, buf)
|
||||
@ -1,32 +0,0 @@
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
|
||||
module Language.Conq.ForVal where
|
||||
|
||||
import Language.Conq.Types
|
||||
|
||||
import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
|
||||
import Data.Type.Equality
|
||||
import Type.Reflection
|
||||
import Data.Coerce
|
||||
import GHC.Natural
|
||||
import Control.Category
|
||||
import Data.Flat
|
||||
import Data.Flat.Bits
|
||||
import Data.Bits
|
||||
import Data.Vector (generate)
|
||||
import Data.Monoid.Unicode ((∅))
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Control.Lens ((&))
|
||||
import Control.Monad.Except (ExceptT, runExceptT)
|
||||
import Control.Monad.State (State, get, put, evalState, runState)
|
||||
import Control.Monad.Trans.Except (throwE)
|
||||
import Data.Bits ((.|.), shiftL, shiftR)
|
||||
import System.IO.Unsafe (unsafePerformIO)
|
||||
import Text.Show (showString, showParen)
|
||||
|
||||
import qualified Prelude as P
|
||||
import qualified Crypto.Hash.SHA256 as SHA256
|
||||
import qualified Data.ByteString.Base58 as Base58
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.ByteString.Unsafe as B
|
||||
@ -1,180 +0,0 @@
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
|
||||
module Language.Conq.Grainary where
|
||||
|
||||
import Language.Conq.Types
|
||||
import Language.Conq.ForVal
|
||||
|
||||
import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
|
||||
import Data.Type.Equality
|
||||
import Type.Reflection
|
||||
import Data.Coerce
|
||||
import GHC.Natural
|
||||
import Control.Category
|
||||
import Data.Flat
|
||||
import Data.Flat.Bits
|
||||
import Data.Bits
|
||||
import Data.Vector (generate)
|
||||
import Data.Monoid.Unicode ((∅))
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Control.Lens ((&))
|
||||
import Control.Monad.Except (ExceptT, runExceptT)
|
||||
import Control.Monad.State (State, get, put, evalState, runState)
|
||||
import Control.Monad.Trans.Except (throwE)
|
||||
import Data.Bits ((.|.), shiftL, shiftR)
|
||||
import System.IO.Unsafe (unsafePerformIO)
|
||||
import Text.Show (showString, showParen)
|
||||
|
||||
import qualified Prelude as P
|
||||
import qualified Crypto.Hash.SHA256 as SHA256
|
||||
import qualified Data.ByteString.Base58 as Base58
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.ByteString.Unsafe as B
|
||||
|
||||
|
||||
-- Jets ------------------------------------------------------------------------
|
||||
|
||||
jetReg :: [(SHA256, Exp, Val -> Val)]
|
||||
jetReg =
|
||||
[ ( SHA256 (encodeBase58 "FWz5mTGmuVz2b4TLNa7yMjTKL7wihsEWakoUD2nzqP6q")
|
||||
, ESubj
|
||||
, id
|
||||
)
|
||||
]
|
||||
|
||||
jets :: HashMap SHA256 (Val -> Val)
|
||||
jets = mapFromList (jetReg <&> \(h,_,f) -> (h,f))
|
||||
|
||||
grainsFromJets :: HashMap SHA256 ByteString
|
||||
grainsFromJets = do
|
||||
mapFromList $ jetReg <&> \(h,e,_) -> (h, flat (forVal e))
|
||||
|
||||
-- The Grainary ----------------------------------------------------------------
|
||||
|
||||
grainery :: IORef (HashMap SHA256 ByteString)
|
||||
grainery = unsafePerformIO (newIORef grainsFromJets)
|
||||
|
||||
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
||||
decodeBase58 :: ByteString -> Text
|
||||
decodeBase58 = decodeUtf8 . Base58.encodeBase58 Base58.bitcoinAlphabet
|
||||
|
||||
fromJust (Just x) = x
|
||||
fromJust _ = error "fromJust: Nothing"
|
||||
|
||||
encodeBase58 :: Text -> ByteString
|
||||
encodeBase58 = fromJust
|
||||
. Base58.decodeBase58 Base58.bitcoinAlphabet
|
||||
. encodeUtf8
|
||||
|
||||
|
||||
-- Create Grains ---------------------------------------------------------------
|
||||
|
||||
putGrain :: Val -> Val
|
||||
putGrain v = unsafePerformIO $ do
|
||||
(bs, k) <- evaluate $ force (hashVal v)
|
||||
traceM ("Putting Grain: " <> unpack (decodeBase58 $ unSHA256 k))
|
||||
atomicModifyIORef' grainery (\t -> (insertMap k bs t, ()))
|
||||
evaluate (VR k)
|
||||
where
|
||||
hashVal :: Val -> (ByteString, SHA256)
|
||||
hashVal x = (bs, SHA256 (SHA256.hash bs))
|
||||
where bs = flat x
|
||||
|
||||
|
||||
-- Read Grains -----------------------------------------------------------------
|
||||
|
||||
getGrain :: SHA256 -> Val
|
||||
getGrain k = unsafePerformIO $ do
|
||||
traceM ("Getting Grain: " <> unpack (decodeBase58 $ unSHA256 k))
|
||||
|
||||
t <- readIORef grainery
|
||||
|
||||
Just (P.Right v) <- pure (unflat <$> lookup k t)
|
||||
|
||||
pure v
|
||||
|
||||
|
||||
-- Encode/Decode Formulas ------------------------------------------------------
|
||||
|
||||
flattenExp :: Exp -> Exp
|
||||
flattenExp = go
|
||||
where
|
||||
go (EWith (EWith x y) z) = go (EWith x (EWith y z))
|
||||
go (EWith x y) = EWith x (go y)
|
||||
go x = x
|
||||
|
||||
forVal :: Exp -> Val
|
||||
forVal = \e ->
|
||||
case flattenExp e of
|
||||
EWith x y -> V1 $ VP (opkVal x) (forVal y)
|
||||
x -> V0 (opkVal x)
|
||||
where
|
||||
opkVal :: Exp -> Val
|
||||
opkVal = \case
|
||||
EWith _ _ -> error "forVal: broken invariant"
|
||||
ELeft -> V0 $ V0 $ V0 VN
|
||||
EWrit -> V0 $ V0 $ V1 VN
|
||||
EHead -> V0 $ V1 $ V0 VN
|
||||
ETail -> V0 $ V1 $ V1 VN
|
||||
EPure v -> V1 $ V0 $ V0 $ V0 v
|
||||
ESubj -> V1 $ V0 $ V0 $ V1 VN
|
||||
ELazy -> V1 $ V0 $ V1 $ V0 $ V0 VN
|
||||
EMark -> V1 $ V0 $ V1 $ V1 $ V0 VN
|
||||
EEval -> V1 $ V1 $ V0 $ V0 VN
|
||||
EDist -> V1 $ V1 $ V0 $ V1 VN
|
||||
ECase x y -> V1 $ V1 $ V1 $ V0 $ VP (forVal x) (forVal y)
|
||||
ECons x y -> V1 $ V1 $ V1 $ V1 $ VP (forVal x) (forVal y)
|
||||
EType _ -> opkVal ESubj
|
||||
_ -> undefined
|
||||
|
||||
valFor' :: Val -> Maybe Exp
|
||||
valFor' (V0 l) = valOpk l
|
||||
valFor' (VR r) = valFor' (getGrain r)
|
||||
valFor' (V1 (VP x y)) = (<>) <$> valFor' y <*> valOpk x
|
||||
valFor' _ = Nothing
|
||||
|
||||
valFor :: Val -> Exp
|
||||
valFor = maybe (EPure VN) id . valFor'
|
||||
|
||||
valOpk :: Val -> Maybe Exp
|
||||
valOpk (V0 (V0 x)) = valDir x
|
||||
valOpk (V0 (V1 x)) = valGet x
|
||||
valOpk (V1 (V0 (V0 x))) = valSim x
|
||||
valOpk (V1 (V0 (V1 x))) = valHin x
|
||||
valOpk (V1 (V1 (V0 x))) = valOtr x
|
||||
valOpk (V1 (V1 (V1 x))) = valPlx x
|
||||
valOpk _ = Nothing
|
||||
|
||||
valDir :: Val -> Maybe Exp
|
||||
valDir (V0 VN) = pure ELeft
|
||||
valDir (V1 VN) = pure EWrit
|
||||
valDir _ = Nothing
|
||||
|
||||
valGet :: Val -> Maybe Exp
|
||||
valGet (V0 VN) = pure EHead
|
||||
valGet (V1 VN) = pure ETail
|
||||
valGet _ = Nothing
|
||||
|
||||
valSim :: Val -> Maybe Exp
|
||||
valSim (V0 v) = pure (EPure v)
|
||||
valSim (V1 VN) = pure ESubj
|
||||
valSim _ = Nothing
|
||||
|
||||
valOtr :: Val -> Maybe Exp
|
||||
valOtr (V0 VN) = pure EEval
|
||||
valOtr (V1 VN) = pure EDist
|
||||
valOtr _ = Nothing
|
||||
|
||||
valPlx :: Val -> Maybe Exp
|
||||
valPlx (V0 (VP x y)) = pure $ ECase (valFor x) (valFor y)
|
||||
valPlx (V1 (VP x y)) = pure $ ECons (valFor x) (valFor y)
|
||||
valPlx _ = Nothing
|
||||
|
||||
valHin :: Val -> Maybe Exp
|
||||
valHin = \case
|
||||
V0 (V0 VN) -> pure ELazy
|
||||
V1 (V0 VN) -> pure EMark
|
||||
_ -> Nothing
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,157 +0,0 @@
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
|
||||
module Language.Conq.Types where
|
||||
|
||||
import ClassyPrelude hiding ((<.>), Left, Right, hash, cons)
|
||||
import Data.Type.Equality
|
||||
import Type.Reflection
|
||||
import Data.Coerce
|
||||
import GHC.Natural
|
||||
import Control.Category
|
||||
import Data.Flat
|
||||
import Data.Flat.Bits
|
||||
import Data.Bits
|
||||
import Data.Vector (generate)
|
||||
import Data.Monoid.Unicode ((∅))
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Control.Lens ((&))
|
||||
import Control.Monad.Except (ExceptT, runExceptT)
|
||||
import Control.Monad.State (State, get, put, evalState, runState)
|
||||
import Control.Monad.Trans.Except (throwE)
|
||||
import Data.Bits ((.|.), shiftL, shiftR)
|
||||
import System.IO.Unsafe (unsafePerformIO)
|
||||
import Text.Show (showString, showParen)
|
||||
|
||||
import qualified Prelude as P
|
||||
import qualified Crypto.Hash.SHA256 as SHA256
|
||||
import qualified Data.ByteString.Base58 as Base58
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.ByteString.Unsafe as B
|
||||
|
||||
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
||||
type Tup a b = (a, b)
|
||||
|
||||
data Sum a b = L a | R b
|
||||
deriving (Eq, Ord)
|
||||
|
||||
-- SHA256
|
||||
newtype SHA256 = SHA256 { unSHA256 :: ByteString }
|
||||
deriving newtype (Eq, Ord, Flat, Show, Hashable, NFData)
|
||||
|
||||
|
||||
-- RTS Values ------------------------------------------------------------------
|
||||
|
||||
data Val
|
||||
= VV -- Void
|
||||
| VN -- Null
|
||||
| V0 !Val -- Left
|
||||
| V1 !Val -- Right
|
||||
| VP !Val !Val -- Pair
|
||||
| VT !Val !Exp Val -- Thunk
|
||||
| VR !SHA256 -- Grain
|
||||
deriving (Eq, Ord, Show, Generic, Flat)
|
||||
|
||||
|
||||
-- Types -----------------------------------------------------------------------
|
||||
|
||||
data TyExp
|
||||
= TENil
|
||||
| TESum TyExp TyExp
|
||||
| TETup TyExp TyExp
|
||||
| TEFor TyExp TyExp
|
||||
| TEAll TyExp
|
||||
| TEFix TyExp
|
||||
| TERef Int
|
||||
deriving (Eq, Ord, Show, Generic, Flat)
|
||||
|
||||
data Ty
|
||||
= TNil
|
||||
| TSum Ty Ty
|
||||
| TTup Ty Ty
|
||||
| TFor Ty Ty
|
||||
| TVar Int
|
||||
deriving (Eq, Show, Ord)
|
||||
|
||||
|
||||
-- Axe -- Conq Encoding --------------------------------------------------------
|
||||
|
||||
data Flag = T | F
|
||||
deriving (Eq, Ord, Show, Generic, Flat)
|
||||
|
||||
data Hint = HLazy | HMark | HType TyExp | HFast
|
||||
deriving (Eq, Ord, Show, Generic, Flat)
|
||||
|
||||
deriving instance Flat a => Flat (NonEmpty a)
|
||||
|
||||
data Axe
|
||||
= AAxis [Flag]
|
||||
| APure Val
|
||||
| AEval
|
||||
| ATong (NonEmpty Flag)
|
||||
| ACons Axe Axe
|
||||
| ACase Axe Axe
|
||||
| AWith Axe Axe
|
||||
| AHint Hint
|
||||
deriving (Eq, Ord, Show, Generic, Flat)
|
||||
|
||||
instance Semigroup Axe where
|
||||
AAxis xs <> AAxis ys = AAxis (ys <> xs)
|
||||
ATong xs <> ATong ys = ATong (ys <> xs)
|
||||
x <> y = y `AWith` x
|
||||
|
||||
instance Monoid Axe where
|
||||
mempty = AAxis []
|
||||
|
||||
|
||||
-- Exp -- Conq ASTs ------------------------------------------------------------
|
||||
|
||||
data Exp
|
||||
= ESubj
|
||||
| EPure Val
|
||||
| EEval
|
||||
| ELeft
|
||||
| EWrit
|
||||
| EHead
|
||||
| ETail
|
||||
| EDist
|
||||
| EWith Exp Exp
|
||||
| ECons Exp Exp
|
||||
| ECase Exp Exp
|
||||
| EType TyExp
|
||||
| EMark
|
||||
| ELazy
|
||||
| EFast
|
||||
| EQuot Exp
|
||||
| ETape Exp -- Unquote
|
||||
deriving (Eq, Ord, Show, Generic, Flat)
|
||||
|
||||
instance Semigroup Exp where
|
||||
x <> y = EWith y x
|
||||
|
||||
instance Monoid Exp where
|
||||
mempty = ESubj
|
||||
|
||||
|
||||
-- Conq -- Typed-Embedding -----------------------------------------------------
|
||||
|
||||
data Conq s r where
|
||||
Subj :: Conq s s
|
||||
Pure :: v -> Conq s v
|
||||
Left :: Conq a (Sum a b)
|
||||
Writ :: Conq b (Sum a b)
|
||||
Head :: Conq (Tup a b) a
|
||||
Tail :: Conq (Tup a b) b
|
||||
Cons :: Conq s a -> Conq s b -> Conq s (Tup a b)
|
||||
Case :: Conq a r -> Conq b r -> Conq (Sum a b) r
|
||||
Dist :: Conq (Tup (Sum a b) s) (Sum (Tup a s) (Tup b s))
|
||||
With :: (Conq s a) -> ((Conq a r) -> (Conq s r))
|
||||
Eval :: Conq (Tup a (Conq a r)) r
|
||||
Mark :: Conq a a
|
||||
Lazy :: Conq (Tup s (Conq s a)) (Tup s (Conq s a))
|
||||
|
||||
instance Category Conq where
|
||||
id = Subj
|
||||
(.) = flip With
|
||||
@ -1,84 +0,0 @@
|
||||
name: language-conq
|
||||
version: 0.1.0
|
||||
license: AGPL-3.0-only
|
||||
|
||||
library:
|
||||
source-dirs: lib
|
||||
ghc-options:
|
||||
- -fwarn-incomplete-patterns
|
||||
- -O2
|
||||
|
||||
dependencies:
|
||||
- async
|
||||
- base
|
||||
- base58-bytestring
|
||||
- base-unicode-symbols
|
||||
- bytestring
|
||||
- case-insensitive
|
||||
- chunked-data
|
||||
- classy-prelude
|
||||
- containers
|
||||
- cryptohash
|
||||
- data-fix
|
||||
- extra
|
||||
- flat
|
||||
- ghc-prim
|
||||
- http-client
|
||||
- http-types
|
||||
- integer-gmp
|
||||
- largeword
|
||||
- lens
|
||||
- megaparsec
|
||||
- mtl
|
||||
- multimap
|
||||
- para
|
||||
- pretty-show
|
||||
- QuickCheck
|
||||
- semigroups
|
||||
- smallcheck
|
||||
- stm
|
||||
- stm-chans
|
||||
- tasty
|
||||
- tasty-quickcheck
|
||||
- tasty-th
|
||||
- text
|
||||
- these
|
||||
- time
|
||||
- transformers
|
||||
- unordered-containers
|
||||
- vector
|
||||
|
||||
default-extensions:
|
||||
- ApplicativeDo
|
||||
- BangPatterns
|
||||
- BlockArguments
|
||||
- DeriveAnyClass
|
||||
- DeriveDataTypeable
|
||||
- DeriveFoldable
|
||||
- DeriveGeneric
|
||||
- DeriveTraversable
|
||||
- DerivingStrategies
|
||||
- EmptyDataDecls
|
||||
- FlexibleContexts
|
||||
- FlexibleInstances
|
||||
- FunctionalDependencies
|
||||
- GADTs
|
||||
- GeneralizedNewtypeDeriving
|
||||
- LambdaCase
|
||||
- MultiParamTypeClasses
|
||||
- NamedFieldPuns
|
||||
- NoImplicitPrelude
|
||||
- NumericUnderscores
|
||||
- OverloadedStrings
|
||||
- PartialTypeSignatures
|
||||
- QuasiQuotes
|
||||
- Rank2Types
|
||||
- RankNTypes
|
||||
- RecordWildCards
|
||||
- ScopedTypeVariables
|
||||
- TemplateHaskell
|
||||
- TupleSections
|
||||
- TypeApplications
|
||||
- TypeFamilies
|
||||
- UnicodeSyntax
|
||||
- ViewPatterns
|
||||
2
pkg/hs-hoon/.gitignore
vendored
2
pkg/hs-hoon/.gitignore
vendored
@ -1,2 +0,0 @@
|
||||
.stack-work
|
||||
*.cabal
|
||||
@ -1,345 +0,0 @@
|
||||
-- TODO Handle comments
|
||||
|
||||
module Language.Attila.AST.Parser where
|
||||
|
||||
import Language.Hoon.AST.Types
|
||||
import ClassyPrelude hiding (head, many, some, try)
|
||||
import Control.Lens
|
||||
import Text.Megaparsec
|
||||
import Text.Megaparsec.Char
|
||||
import Control.Monad.State.Lazy
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Data.Void (Void)
|
||||
import Prelude (head)
|
||||
import Text.Format.Para (formatParas)
|
||||
|
||||
import qualified Data.MultiMap as MM
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.Lazy as LT
|
||||
import qualified Data.Text.Lazy.IO as LT
|
||||
import qualified Prelude
|
||||
|
||||
|
||||
-- Parser Monad ----------------------------------------------------------------
|
||||
|
||||
data Mode = Wide | Tall
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
type Parser = StateT Mode (Parsec Void Text)
|
||||
|
||||
withLocalState :: Monad m => s -> StateT s m a -> StateT s m a
|
||||
withLocalState val x = do { old <- get; put val; x <* put old }
|
||||
|
||||
inWideMode :: Parser a -> Parser a
|
||||
inWideMode = withLocalState Wide
|
||||
|
||||
|
||||
-- Simple Lexers ---------------------------------------------------------------
|
||||
|
||||
ace, pal, par ∷ Parser ()
|
||||
ace = void (char ' ')
|
||||
pal = void (char '(')
|
||||
par = void (char ')')
|
||||
|
||||
gap ∷ Parser ()
|
||||
gap = choice [ char ' ' >> void (some spaceChar)
|
||||
, newline >> void (many spaceChar)
|
||||
]
|
||||
|
||||
whitespace ∷ Parser ()
|
||||
whitespace = ace <|> void gap
|
||||
|
||||
|
||||
-- Literals --------------------------------------------------------------------
|
||||
|
||||
alpha ∷ Parser Char
|
||||
alpha = oneOf (['a'..'z'] ++ ['A'..'Z'])
|
||||
|
||||
sym ∷ Parser Sym
|
||||
sym = bucSym <|> some alpha
|
||||
where bucSym = char '$' *> pure ""
|
||||
|
||||
atom ∷ Parser Nat
|
||||
atom = do
|
||||
init ← some digitChar
|
||||
rest ← many (char '.' *> some digitChar)
|
||||
guard True -- TODO Validate '.'s
|
||||
pure (Prelude.read $ concat $ init:rest)
|
||||
|
||||
nat ∷ Parser Nat
|
||||
nat = Prelude.read <$> some digitChar
|
||||
|
||||
limb ∷ Parser (Either Nat Sym)
|
||||
limb = (Right <$> sym) <|> (char '+' >> Left <$> nat)
|
||||
|
||||
wing ∷ Parser Wing
|
||||
wing =
|
||||
subjt <|> limbs
|
||||
where
|
||||
subjt ∷ Parser Wing
|
||||
subjt = pure [] <* char '.'
|
||||
limbs ∷ Parser Wing
|
||||
limbs = do s ← limb
|
||||
ss ← many (char '.' >> limb)
|
||||
pure (s:ss)
|
||||
|
||||
tape ∷ Parser Text
|
||||
tape = do
|
||||
between (char '"') (char '"') $
|
||||
pack <$> many (label "tape char" (anySingleBut '"'))
|
||||
|
||||
cord ∷ Parser Text
|
||||
cord = do
|
||||
between (char '\'') (char '\'') $
|
||||
pack <$> many (label "cord char" (anySingleBut '\''))
|
||||
|
||||
literal ∷ Parser Hoon
|
||||
literal = choice
|
||||
[ Atom <$> atom
|
||||
, Wing <$> wing
|
||||
, pure Yes <* string "%.y"
|
||||
, pure No <* string "%.n"
|
||||
, pure Pam <* char '&'
|
||||
, pure Bar <* char '|'
|
||||
, pure Sig <* char '~'
|
||||
, pure Lus <* char '+'
|
||||
, pure Hep <* char '-'
|
||||
, Cord <$> cord
|
||||
, Tape <$> tape
|
||||
]
|
||||
|
||||
-- Rune Helpers ----------------------------------------------------------------
|
||||
|
||||
{-
|
||||
- If the parser is in `Wide` mode, only accept the `wide` form.
|
||||
- If the parser is in `Tall` mode, either
|
||||
- accept the `tall` form or:
|
||||
- swich to `Wide` mode and then accept the wide form.
|
||||
-}
|
||||
parseRune ∷ Parser a → Parser a → Parser a
|
||||
parseRune tall wide = get >>= \case
|
||||
Wide → wide
|
||||
Tall → tall <|> inWideMode wide
|
||||
|
||||
rune1 ∷ (a→b) → Parser a → Parser b
|
||||
rune1 node x = parseRune tall wide
|
||||
where tall = do gap; p←x; pure (node p)
|
||||
wide = do pal; p←x; par; pure (node p)
|
||||
|
||||
rune2 ∷ (a→b→c) → Parser a → Parser b → Parser c
|
||||
rune2 node x y = parseRune tall wide
|
||||
where tall = do gap; p←x; gap; q←y; pure (node p q)
|
||||
wide = do pal; p←x; ace; q←y; par; pure (node p q)
|
||||
|
||||
rune3 ∷ (a→b→c→d) → Parser a → Parser b → Parser c → Parser d
|
||||
rune3 node x y z = parseRune tall wide
|
||||
where tall = do gap; p←x; gap; q←y; gap; r←z; pure (node p q r)
|
||||
wide = do pal; p←x; ace; q←y; ace; r←z; par; pure (node p q r)
|
||||
|
||||
rune4 ∷ (a→b→c→d→e) → Parser a → Parser b → Parser c → Parser d → Parser e
|
||||
rune4 node x y z g = parseRune tall wide
|
||||
where tall = do gap; p←x; gap; q←y; gap; r←z; gap; s←g; pure (node p q r s)
|
||||
wide = do pal; p←x; ace; q←y; ace; r←z; ace; s←g; pure (node p q r s)
|
||||
|
||||
runeN ∷ ([a]→b) → Parser a → Parser b
|
||||
runeN node elem = node <$> parseRune tall wide
|
||||
where tall = gap >> elems
|
||||
where elems = term <|> elemAnd
|
||||
elemAnd = do x ← elem; gap; xs ← elems; pure (x:xs)
|
||||
term = string "==" *> pure []
|
||||
wide = pal *> option [] elems <* par
|
||||
where elems = (:) <$> elem <*> many (ace >> elem)
|
||||
|
||||
runeNE ∷ (NonEmpty a → b) → Parser a → Parser b
|
||||
runeNE node elem = node <$> parseRune tall wide
|
||||
where tall = do
|
||||
let elems = term <|> elemAnd
|
||||
elemAnd = do x ← elem; gap; xs ← elems; pure (x:xs)
|
||||
term = string "==" *> pure []
|
||||
fst <- gap *> elem
|
||||
rst <- gap *> elems
|
||||
pure (fst :| rst)
|
||||
wide = mzero -- No wide form for cores
|
||||
|
||||
-- Irregular Syntax ------------------------------------------------------------
|
||||
|
||||
inc ∷ Parser Hoon -- +(3)
|
||||
inc = do
|
||||
string "+("
|
||||
h ← hoon
|
||||
char ')'
|
||||
pure h
|
||||
|
||||
equals ∷ Parser (Hoon, Hoon) -- =(3 4)
|
||||
equals = do
|
||||
string "=("
|
||||
x ← hoon
|
||||
ace
|
||||
y ← hoon
|
||||
char ')'
|
||||
pure (x, y)
|
||||
|
||||
tuple ∷ ∀a. Parser a → Parser [a]
|
||||
tuple p = char '[' >> elems
|
||||
where
|
||||
xs ∷ Parser [a]
|
||||
xs = do { x ← p; (x:) <$> tail }
|
||||
|
||||
tail ∷ Parser [a]
|
||||
tail = (pure [] <* char ']')
|
||||
<|> (ace >> elems)
|
||||
|
||||
elems ∷ Parser [a]
|
||||
elems = (pure [] <* char ']') <|> xs
|
||||
|
||||
irregular ∷ Parser Hoon
|
||||
irregular =
|
||||
inWideMode $
|
||||
choice [ Tupl <$> tuple hoon
|
||||
, IncrIrr <$> inc
|
||||
, uncurry IsEqIrr <$> equals
|
||||
]
|
||||
|
||||
-- Runes -----------------------------------------------------------------------
|
||||
|
||||
cRune ∷ (Map Sym Hoon → a) → Parser a
|
||||
cRune f = do
|
||||
mode ← get
|
||||
guard (mode == Tall)
|
||||
gap
|
||||
f . mapFromList <$> arms -- TODO Complain about duplicated arms
|
||||
where
|
||||
arms :: Parser [(Sym, Hoon)]
|
||||
arms = many arm <* string "--"
|
||||
|
||||
arm :: Parser (Sym, Hoon)
|
||||
arm = do
|
||||
string "++"
|
||||
gap
|
||||
s ← sym
|
||||
gap
|
||||
h ← hoon
|
||||
gap
|
||||
pure (s, h)
|
||||
|
||||
data Skin
|
||||
|
||||
rune ∷ Parser Hoon
|
||||
rune = runeSwitch [ ("|=", rune2 BarTis hoon hoon)
|
||||
, ("|-", rune1 BarHep hoon)
|
||||
, (":-", rune2 ColHep hoon hoon)
|
||||
, (":+", rune3 ColLus hoon hoon hoon)
|
||||
, (":^", rune4 ColKet hoon hoon hoon hoon)
|
||||
, (":*", runeN ColTar hoon)
|
||||
, (":~", runeN ColSig hoon)
|
||||
, ("^-", rune2 KetHep spec hoon)
|
||||
, ("=<", rune2 TisGal hoon hoon)
|
||||
, ("=>", rune2 TisGar hoon hoon)
|
||||
, ("?:", rune3 WutCol hoon hoon hoon)
|
||||
, ("?=", rune2 WutTis spec hoon)
|
||||
, ("?@", rune3 WutPat hoon hoon hoon)
|
||||
, ("?^", rune3 WutKet hoon hoon hoon)
|
||||
, (".+", rune1 Incr hoon)
|
||||
, (".=", rune2 IsEq hoon hoon)
|
||||
, ("^=", rune2 KetTis sym hoon)
|
||||
, ("=.", rune3 TisDot wing hoon hoon)
|
||||
, ("|%", cRune BarCen)
|
||||
]
|
||||
|
||||
runeSwitch ∷ [(Text, Parser a)] → Parser a
|
||||
runeSwitch = choice . fmap (\(s, p) → string s *> p)
|
||||
|
||||
-- runeSwitch ∷ [(String, Parser a)] → Parser a
|
||||
-- runeSwitch = parseBasedOnRune
|
||||
-- . fmap (\([x,y], p) → (x, (y,p)))
|
||||
-- where
|
||||
-- parseBasedOnRune ∷ [(Char, (Char, Parser a))] → Parser a
|
||||
-- parseBasedOnRune = combine . restructure
|
||||
-- where combine = lexThen . overSnd lexThen
|
||||
-- overSnd f = fmap (\(x,y) → (x,f y))
|
||||
-- lexThen = choice . fmap (\(x,y) → char x *> y)
|
||||
-- restructure = MM.assocs
|
||||
-- . MM.fromList
|
||||
|
||||
-- Infix Syntax ----------------------------------------------------------------
|
||||
|
||||
colInfix ∷ Parser Hoon
|
||||
colInfix = do
|
||||
x ← try (hoonNoInfix <* char ':')
|
||||
y ← hoon
|
||||
pure (ColOp x y)
|
||||
|
||||
faceOp ∷ Parser Hoon
|
||||
faceOp = FaceOp <$> try (sym <* char '=')
|
||||
<*> hoon
|
||||
|
||||
infixOp ∷ Parser Hoon
|
||||
infixOp = do
|
||||
inWideMode (colInfix <|> faceOp)
|
||||
|
||||
-- Hoon Parser -----------------------------------------------------------------
|
||||
|
||||
hoonNoInfix ∷ Parser Hoon
|
||||
hoonNoInfix = irregular <|> rune <|> literal
|
||||
|
||||
hoon ∷ Parser Hoon
|
||||
hoon = infixOp <|> hoonNoInfix
|
||||
|
||||
-- Entry Point -----------------------------------------------------------------
|
||||
|
||||
hoonFile = do
|
||||
option () whitespace
|
||||
h ← hoon
|
||||
option () whitespace
|
||||
eof
|
||||
pure h
|
||||
|
||||
parse :: Text -> Either Text Hoon
|
||||
parse txt =
|
||||
runParser (evalStateT hoonFile Tall) "stdin" txt & \case
|
||||
Left e -> Left (pack $ errorBundlePretty e)
|
||||
Right x -> pure x
|
||||
|
||||
parseHoonTest ∷ Text → IO ()
|
||||
parseHoonTest = parseTest (evalStateT hoonFile Tall)
|
||||
|
||||
main ∷ IO ()
|
||||
main = (head <$> getArgs) >>= parseHoonTest
|
||||
|
||||
|
||||
-- Parse Spec ------------------------------------------------------------------
|
||||
|
||||
base :: Parser Base
|
||||
base = choice [ BVoid <$ char '!'
|
||||
, BNull <$ char '~'
|
||||
, BFlag <$ char '?'
|
||||
, BNoun <$ char '*'
|
||||
, BCell <$ char '^'
|
||||
, BAtom <$ char '@'
|
||||
]
|
||||
|
||||
specTuple ∷ Parser Spec
|
||||
specTuple = tuple spec >>= \case
|
||||
[] -> mzero
|
||||
x:xs -> pure (STuple (x :| xs))
|
||||
|
||||
specFace ∷ Parser Spec
|
||||
specFace = SFaceOp <$> try (sym <* char '=') <*> spec
|
||||
|
||||
specIrregular ∷ Parser Spec
|
||||
specIrregular = inWideMode (specTuple <|> specFace)
|
||||
|
||||
spec :: Parser Spec
|
||||
spec = specIrregular <|> specRune <|> fmap SBase base
|
||||
|
||||
specRune ∷ Parser Spec
|
||||
specRune = choice
|
||||
[ string "$:" >> runeNE SBucCol spec
|
||||
, string "$-" >> rune2 SBucHep spec spec
|
||||
, string "$=" >> rune2 SBucTis sym spec
|
||||
, string "$?" >> runeNE SBucWut spec
|
||||
, string "$@" >> rune2 SBucPat spec spec
|
||||
, string "$^" >> rune2 SBucKet spec spec
|
||||
, string "$%" >> runeNE SBucCen spec
|
||||
]
|
||||
@ -1,66 +0,0 @@
|
||||
-- TODO Handle comments
|
||||
|
||||
module Language.Attila.AST.Types where
|
||||
|
||||
import ClassyPrelude
|
||||
import Data.List.NonEmpty (NonEmpty)
|
||||
|
||||
-- AST Types -------------------------------------------------------------------
|
||||
|
||||
type Nat = Int
|
||||
type Sym = String
|
||||
type Wing = [Either Nat Sym]
|
||||
|
||||
data Base = BVoid | BNull | BFlag | BNoun | BCell | BAtom
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Spec
|
||||
= SBase Base -- ^, ?
|
||||
| SFaceOp Sym Spec -- x=@
|
||||
| SBucCol (NonEmpty Spec) -- $:
|
||||
| SBucHep Spec Spec -- $-, function core
|
||||
| SBucTis Sym Spec -- $=, name
|
||||
| SBucWut (NonEmpty Spec) -- $?, full pick
|
||||
| SBucPat Spec Spec -- $@, atom pick
|
||||
| SBucKet Spec Spec -- $^, cons pick
|
||||
| SBucCen (NonEmpty Spec) -- $%, head pick
|
||||
| STuple (NonEmpty Spec) -- [@ @]
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Hoon
|
||||
= WutCol Hoon Hoon Hoon -- ?:(c t f)
|
||||
| WutTis Spec Hoon -- ?=(@ 0)
|
||||
| WutPat Hoon Hoon Hoon -- ?@(c t f)
|
||||
| WutKet Hoon Hoon Hoon -- ?^(c t f)
|
||||
| KetTis Sym Hoon -- ^=(x 3)
|
||||
| ColHep Hoon Hoon -- :-(a b)
|
||||
| ColLus Hoon Hoon Hoon -- :+(a b c)
|
||||
| ColKet Hoon Hoon Hoon Hoon -- :^(a b c d)
|
||||
| ColTar [Hoon] -- :*(a as ...)
|
||||
| ColSig [Hoon] -- :~(a as ...)
|
||||
| KetHep Spec Hoon -- ^-(s h)
|
||||
| TisGal Hoon Hoon -- =<(a b)
|
||||
| TisGar Hoon Hoon -- =>(a b)
|
||||
| BarTis Hoon Hoon -- |=(s h)
|
||||
| BarHep Hoon -- |-(a)
|
||||
| TisDot Wing Hoon Hoon -- =.(a 3 a)
|
||||
| BarCen (Map Sym Hoon) -- |% ++ a 3 --
|
||||
| ColOp Hoon Hoon -- [+ -]:[3 4]
|
||||
| Tupl [Hoon] -- [a b]
|
||||
| FaceOp Sym Hoon -- x=y
|
||||
| Wing Wing -- ., a, a.b
|
||||
| Atom Nat -- 3
|
||||
| Cord Text -- 'cord'
|
||||
| Tape Text -- "tape"
|
||||
| Incr Hoon -- .+(3)
|
||||
| IncrIrr Hoon -- +(3)
|
||||
| IsEq Hoon Hoon -- .=(3 4)
|
||||
| IsEqIrr Hoon Hoon -- =(3 4)
|
||||
| Lus -- +
|
||||
| Hep -- -
|
||||
| Pam -- &
|
||||
| Bar -- |
|
||||
| Yes -- %.y
|
||||
| No -- %.n
|
||||
| Sig -- ~
|
||||
deriving (Eq, Ord, Show)
|
||||
@ -1,359 +0,0 @@
|
||||
{-# LANGUAGE OverloadedLists #-}
|
||||
|
||||
module Language.Attila.IR where
|
||||
|
||||
import ClassyPrelude hiding (fail, try)
|
||||
import GHC.Natural
|
||||
import Control.Lens
|
||||
import Data.Vector (Vector, (!), (!?))
|
||||
import Control.Monad.Fail
|
||||
import Control.Arrow ((>>>))
|
||||
import Data.ChunkedZip (Zip)
|
||||
import Language.Hoon.Nock.Types
|
||||
import Text.Show.Pretty (ppShow)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
type Nat = Natural
|
||||
type Vec = Vector
|
||||
|
||||
data Ty
|
||||
= Nat
|
||||
| Sum (Vec Ty)
|
||||
| Mul (Vec Ty)
|
||||
| Nok Ty Ty
|
||||
| Fix Ty
|
||||
| All Ty
|
||||
| Ref Nat
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
{-
|
||||
An IR Expression
|
||||
|
||||
Formulas and subject manipulation:
|
||||
|
||||
- Sub -- Reference the current subject.
|
||||
- Lam -- A formula (with the type for its subject)
|
||||
- Wit -- Run an expression against a new subject.
|
||||
- Eva -- Eval a formula against a subject.
|
||||
- Fir -- Fire an arm of a core.
|
||||
|
||||
Atoms:
|
||||
|
||||
- Lit -- An atom literal.
|
||||
- Inc -- Increment an atom.
|
||||
- Eke -- Atom equality.
|
||||
|
||||
Product Types:
|
||||
|
||||
- Tup -- Construct a product type.
|
||||
- Get -- Get a field out of a product.
|
||||
- Mod -- Update a field of a product.
|
||||
|
||||
Sum Types:
|
||||
|
||||
- Cho -- Construct a (branch of a) sum type.
|
||||
- Eat -- Pattern match (switch) on a sum type.
|
||||
-}
|
||||
data Exp
|
||||
= Sub
|
||||
| Lam Ty Exp
|
||||
| Wit Ty Exp Exp
|
||||
| Eva Exp Exp
|
||||
| Fir Nat (Ty, Vec Ty) Exp
|
||||
| Lit Nat
|
||||
| Inc Exp
|
||||
| Eke Exp Exp
|
||||
| Tup (Vec Exp)
|
||||
| Get Nat (Vec Ty) Exp
|
||||
| Cho (Vec Ty) Nat Exp
|
||||
| Eat (Vec Ty) Exp (Vec Exp)
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
zipWithM :: (Monad m, Traversable seq, Zip seq)
|
||||
=> (a -> b -> m c) -> seq a -> seq b -> m (seq c)
|
||||
zipWithM f xs ys = sequence (zipWith f xs ys)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
newtype Infer a = Infer { runInfer :: Either Text a }
|
||||
deriving newtype (Eq, Ord, Show, Functor, Applicative, Monad)
|
||||
|
||||
instance MonadFail Infer where
|
||||
fail = Infer . Left . pack
|
||||
|
||||
guardInfer :: String -> Bool -> Infer ()
|
||||
guardInfer _ True = pure ()
|
||||
guardInfer msg False = fail msg
|
||||
|
||||
unify2 :: Ty -> Ty -> Infer Ty
|
||||
unify2 x y = do
|
||||
let err = "(bad_unify " <> show x <> " ## " <> show y <> ")"
|
||||
guardInfer err (x == y)
|
||||
pure x
|
||||
|
||||
unify :: Vec Ty -> Infer Ty
|
||||
unify = go . toList
|
||||
where
|
||||
go :: [Ty] -> Infer Ty
|
||||
go [] = pure tVoid
|
||||
go [x] = pure x
|
||||
go (x:y:zs) = unify2 x y >> go (y:zs)
|
||||
|
||||
unifyVec :: Vec Ty -> Vec Ty -> Infer (Vec Ty)
|
||||
unifyVec xs ys = do
|
||||
let lenMsg = "unify-bad-len: " <> show (xs, ys)
|
||||
guardInfer lenMsg (length xs == length ys)
|
||||
zipWithM (\x y -> unify [x,y]) xs ys
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
battery :: Ty -> Infer (Vec Ty)
|
||||
battery (Mul [Mul arms, _ctx]) = pure arms
|
||||
battery ty = fail ("battery-not-core: " <> show ty)
|
||||
|
||||
arm :: Nat -> Ty -> Vec Ty -> Infer (Nat, Ty, Ty)
|
||||
arm n cor arms = do
|
||||
let len = fromIntegral (length arms)
|
||||
arms !? fromIntegral n & \case
|
||||
Nothing ->
|
||||
fail ("arm-bad-idx: " <> show (n, arms))
|
||||
Just (Nok nokSut nokRes) -> do
|
||||
unify [cor, nokSut]
|
||||
pure (armAxis n len, nokSut, nokRes)
|
||||
Just armTy ->
|
||||
fail ("arm-not-nok: " <> show armTy)
|
||||
|
||||
nokResTy :: Ty -> Ty -> Infer Ty
|
||||
nokResTy sut (Nok nSut nRes) = unify [sut, nSut] $> nRes
|
||||
nokResTy _ ty = fail ("not-nok: " <> show ty)
|
||||
|
||||
infer :: Ty -> Exp -> Infer Ty
|
||||
infer sut = \case
|
||||
Sub -> do
|
||||
pure sut
|
||||
Lam lub b -> do
|
||||
Nok lub <$> infer lub b
|
||||
Wit ty new bod -> do
|
||||
newSut <- infer sut new
|
||||
unify [ty, newSut]
|
||||
infer ty bod
|
||||
Eva new bod -> do
|
||||
sut' <- infer sut new
|
||||
nokTy <- infer sut bod
|
||||
nokResTy sut' nokTy
|
||||
Fir n (corTy, armTys) cor -> do
|
||||
corTy' <- infer sut cor
|
||||
armTys' <- battery corTy
|
||||
unify [corTy, corTy']
|
||||
unifyVec armTys armTys'
|
||||
view _3 <$> arm n corTy armTys
|
||||
Lit _ -> do
|
||||
pure Nat
|
||||
Inc exp -> do
|
||||
eTy <- infer sut exp
|
||||
unify [eTy, Nat]
|
||||
Eke ex1 ex2 -> do
|
||||
ty1 <- infer sut ex1
|
||||
ty2 <- infer sut ex2
|
||||
unify [Nat, ty1, ty2]
|
||||
Tup exps -> do
|
||||
Mul <$> traverse (infer sut) exps
|
||||
Get n tys tup -> do
|
||||
tupTy <- infer sut tup
|
||||
unify [Mul tys, tupTy]
|
||||
maybe (fail "mul-bad-index") pure (tys !? fromIntegral n)
|
||||
Cho tys n exp -> do
|
||||
ty <- infer sut exp
|
||||
tu <- maybe (fail "cho-bad-index") pure (tys !? fromIntegral n)
|
||||
unify [tu, ty]
|
||||
pure (Sum tys)
|
||||
Eat tys exp bods -> do
|
||||
expTy <- infer sut exp
|
||||
unify [expTy, Sum tys]
|
||||
guardInfer "eat-bad-len" (length tys == length bods)
|
||||
let checkBranch br exp = infer (tPair (tPair Nat br) sut) exp
|
||||
unify =<< zipWithM checkBranch tys bods
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
tPair :: Ty -> Ty -> Ty
|
||||
tPair x y = Mul [x,y]
|
||||
|
||||
tSum :: Ty -> Ty -> Ty
|
||||
tSum x y = Sum [x, y]
|
||||
|
||||
tUnit, tBox, tVoid, tAtom, tNoun, tOpt, tEith, tBool, tOrd, tTop :: Ty
|
||||
tUnit = Mul []
|
||||
tBox = All $ Mul [Ref 0]
|
||||
tVoid = Sum []
|
||||
tAtom = Nat
|
||||
tNoun = Fix $ tSum Nat (tSum (Ref 0) (Ref 0))
|
||||
tOpt = All $ tSum tUnit (Ref 0)
|
||||
tEith = All $ All $ tSum (Ref 1) (Ref 0)
|
||||
tBool = tSum tUnit tUnit
|
||||
tOrd = Sum [tUnit, tUnit, tUnit]
|
||||
tTop = All $ Ref 0
|
||||
|
||||
|
||||
-- Expression Examples ---------------------------------------------------------
|
||||
|
||||
tup2 :: Exp -> Exp -> Exp
|
||||
tup2 x y = Tup [x, y]
|
||||
|
||||
choEx, tupEx, witEx, eatEx :: Exp
|
||||
choEx = Cho [Nat, Nat] 0 (Lit 0)
|
||||
witEx = Wit Nat (Lit 3) Sub
|
||||
tupEx = Get 0 [Nat, Nat]
|
||||
$ Get 1 [Nat, Mul [Nat, Nat]]
|
||||
$ tup2 (Lit 3) (tup2 (Lit 4) (Lit 5))
|
||||
|
||||
eatEx = Eat [Nat, Nat]
|
||||
choEx
|
||||
[ Get 1 [Nat, Nat]
|
||||
(Get 0 [Mul [Nat, Nat], tTop] Sub)
|
||||
, Inc (Lit 0)
|
||||
]
|
||||
|
||||
lamEx :: Exp
|
||||
lamEx = Lam Nat (tup2 (Inc Sub) Sub)
|
||||
|
||||
evaEx :: Exp
|
||||
evaEx = Eva (Lit 0) lamEx
|
||||
|
||||
armExTy, batExTy, corExTy :: Ty
|
||||
armExTy = Nok corExTy Nat
|
||||
batExTy = Mul [armExTy]
|
||||
corExTy = Fix $ Mul [Mul [Nok (Ref 0) Nat], Nat]
|
||||
|
||||
armEx :: Exp
|
||||
armEx = Lam corExTy (Get 1 [batExTy, Nat] Sub)
|
||||
|
||||
batEx :: Exp
|
||||
batEx = Tup [armEx]
|
||||
|
||||
corEx :: Exp
|
||||
corEx = Tup [batEx, Lit 0]
|
||||
|
||||
firEx :: Exp
|
||||
firEx = Fir 0 (corExTy, [armExTy]) corEx
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
indent :: String -> String
|
||||
indent = unlines . fmap (" " <>) . lines
|
||||
|
||||
try :: Text -> Exp -> IO ()
|
||||
try m e = do
|
||||
putStrLn (m <> ":")
|
||||
putStrLn " exp:"
|
||||
putStr (pack $ indent (ppShow e))
|
||||
putStrLn " type:"
|
||||
putStr (pack $ indent (ppShow (runInfer (infer tTop e))))
|
||||
putStrLn " nock:"
|
||||
putStr (pack $ indent (ppShow (compile tTop e)))
|
||||
|
||||
tryAll :: IO ()
|
||||
tryAll = do
|
||||
try "tup" tupEx
|
||||
try "wit" witEx
|
||||
try "cho" choEx
|
||||
try "eat" eatEx
|
||||
try "lam" lamEx
|
||||
try "eva" evaEx
|
||||
try "arm" armEx
|
||||
try "bat" batEx
|
||||
try "cor" corEx
|
||||
try "fir" firEx
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
{-
|
||||
- TODO Record layout (tree instead of list).
|
||||
- TODO Sum layout (use all of atom, atom-head, and cell-head).
|
||||
-}
|
||||
compile :: Ty -> Exp -> Either Text Nock
|
||||
compile sut = \case
|
||||
Sub ->
|
||||
pure (NZeroAxis 1)
|
||||
Lit n ->
|
||||
pure (NOneConst (Atom $ fromIntegral n))
|
||||
Inc x -> do
|
||||
nock <- compile sut x
|
||||
pure (NFourSucc nock)
|
||||
Cho tys n exp -> do
|
||||
nock <- compile sut exp
|
||||
pure (NCons (NOneConst (Atom (fromIntegral n))) nock)
|
||||
Get n tys exp -> do
|
||||
vecNock <- compile sut exp
|
||||
axis <- pure (tupAxis n (fromIntegral $ length tys))
|
||||
pure (NSevenThen vecNock (NZeroAxis $ fromIntegral axis))
|
||||
Tup xs -> do
|
||||
nock <- genCons sut (toList xs)
|
||||
pure nock
|
||||
Eat tys exp brs -> do
|
||||
nock <- compile sut exp
|
||||
newSubjTys <- pure (tys <&> (\x -> tPair (tPair Nat x) sut))
|
||||
nocks <- zipWithM compile newSubjTys brs
|
||||
pure (NEightPush nock (cases (toList nocks)))
|
||||
Eke x y -> do
|
||||
nock1 <- compile sut x
|
||||
nock2 <- compile sut y
|
||||
pure (NFiveEq nock1 nock2)
|
||||
Wit sut' ex1 ex2 -> do
|
||||
nock1 <- compile sut ex1
|
||||
nock2 <- compile sut' ex2
|
||||
pure (NSevenThen nock1 nock2)
|
||||
Lam ty exp -> do
|
||||
NOneConst . nockToNoun <$> compile ty exp
|
||||
Eva sub for -> do
|
||||
subNock <- compile sut sub
|
||||
forNock <- compile sut for
|
||||
pure (NTwoCompose subNock forNock)
|
||||
Fir n (corTy, armTys) cor -> do
|
||||
getCore <- compile sut cor
|
||||
(a,_,_) <- runInfer (arm n corTy armTys)
|
||||
pure (NNineInvoke (fromIntegral a) getCore)
|
||||
|
||||
zapZap :: Nock
|
||||
zapZap = NZeroAxis 0
|
||||
|
||||
genCons :: Ty -> [Exp] -> Either Text Nock
|
||||
genCons sut [] = compile sut (Lit 0)
|
||||
genCons sut [x] = compile sut x
|
||||
genCons sut (x:xs) = do n <- compile sut x
|
||||
ns <- compile sut (Tup (fromList xs))
|
||||
pure (NCons n ns)
|
||||
|
||||
cases :: [Nock] -> Nock
|
||||
cases = go 0
|
||||
where
|
||||
go tag [] = zapZap
|
||||
go tag (nock:nocks) = NSixIf (NFiveEq (NOneConst (Atom (fromIntegral tag)))
|
||||
(NZeroAxis 4))
|
||||
nock
|
||||
(go (tag+1) nocks)
|
||||
|
||||
tupAxis :: Nat -> Nat -> Nat
|
||||
tupAxis 0 1 = 1
|
||||
tupAxis 0 len = 2
|
||||
tupAxis i len | i+1 == len = 1 + tupAxis (i-1) len
|
||||
tupAxis i len = 2 * (1 + tupAxis (i-1) len)
|
||||
|
||||
armAxis :: Nat -> Nat -> Nat
|
||||
armAxis 0 1 = 2
|
||||
armAxis 0 len = 4
|
||||
armAxis i len | i+1 == len = 1 + armAxis (i-1) len
|
||||
armAxis i len = 2 * (1 + armAxis (i-1) len)
|
||||
|
||||
-- Credits: Morgan, Ted, Benjamin
|
||||
|
||||
{-
|
||||
Fix (Mul [Mul [Nok (Ref 0) Nat],Nat])
|
||||
Fix (Mul [Mul [Nok (Ref 0) Nat],Nat])
|
||||
|
||||
1: (Fix (Mul [Mul [Nok (Ref 0) Nat],Nat]))
|
||||
2: (Fix (Mul [Mul [Nok (Ref 0) Nat],Nat]))
|
||||
-}
|
||||
@ -1,345 +0,0 @@
|
||||
-- TODO Handle comments
|
||||
|
||||
module Language.Hoon.AST.Parser where
|
||||
|
||||
import Language.Hoon.AST.Types
|
||||
import ClassyPrelude hiding (head, many, some, try)
|
||||
import Control.Lens
|
||||
import Text.Megaparsec
|
||||
import Text.Megaparsec.Char
|
||||
import Control.Monad.State.Lazy
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
|
||||
import Data.Void (Void)
|
||||
import Prelude (head)
|
||||
import Text.Format.Para (formatParas)
|
||||
|
||||
import qualified Data.MultiMap as MM
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.Lazy as LT
|
||||
import qualified Data.Text.Lazy.IO as LT
|
||||
import qualified Prelude
|
||||
|
||||
|
||||
-- Parser Monad ------------------------------------------------------------------------------------
|
||||
|
||||
data Mode = Wide | Tall
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
type Parser = StateT Mode (Parsec Void Text)
|
||||
|
||||
withLocalState :: Monad m => s -> StateT s m a -> StateT s m a
|
||||
withLocalState val x = do { old <- get; put val; x <* put old }
|
||||
|
||||
inWideMode :: Parser a -> Parser a
|
||||
inWideMode = withLocalState Wide
|
||||
|
||||
|
||||
-- Simple Lexers ---------------------------------------------------------------
|
||||
|
||||
ace, pal, par ∷ Parser ()
|
||||
ace = void (char ' ')
|
||||
pal = void (char '(')
|
||||
par = void (char ')')
|
||||
|
||||
gap ∷ Parser ()
|
||||
gap = choice [ char ' ' >> void (some spaceChar)
|
||||
, newline >> void (many spaceChar)
|
||||
]
|
||||
|
||||
whitespace ∷ Parser ()
|
||||
whitespace = ace <|> void gap
|
||||
|
||||
|
||||
-- Literals --------------------------------------------------------------------
|
||||
|
||||
alpha ∷ Parser Char
|
||||
alpha = oneOf (['a'..'z'] ++ ['A'..'Z'])
|
||||
|
||||
sym ∷ Parser Sym
|
||||
sym = bucSym <|> some alpha
|
||||
where bucSym = char '$' *> pure ""
|
||||
|
||||
atom ∷ Parser Nat
|
||||
atom = do
|
||||
init ← some digitChar
|
||||
rest ← many (char '.' *> some digitChar)
|
||||
guard True -- TODO Validate '.'s
|
||||
pure (Prelude.read $ concat $ init:rest)
|
||||
|
||||
nat ∷ Parser Nat
|
||||
nat = Prelude.read <$> some digitChar
|
||||
|
||||
limb ∷ Parser (Either Nat Sym)
|
||||
limb = (Right <$> sym) <|> (char '+' >> Left <$> nat)
|
||||
|
||||
wing ∷ Parser Wing
|
||||
wing =
|
||||
subjt <|> limbs
|
||||
where
|
||||
subjt ∷ Parser Wing
|
||||
subjt = pure [] <* char '.'
|
||||
limbs ∷ Parser Wing
|
||||
limbs = do s ← limb
|
||||
ss ← many (char '.' >> limb)
|
||||
pure (s:ss)
|
||||
|
||||
tape ∷ Parser Text
|
||||
tape = do
|
||||
between (char '"') (char '"') $
|
||||
pack <$> many (label "tape char" (anySingleBut '"'))
|
||||
|
||||
cord ∷ Parser Text
|
||||
cord = do
|
||||
between (char '\'') (char '\'') $
|
||||
pack <$> many (label "cord char" (anySingleBut '\''))
|
||||
|
||||
literal ∷ Parser Hoon
|
||||
literal = choice
|
||||
[ Atom <$> atom
|
||||
, Wing <$> wing
|
||||
, pure Yes <* string "%.y"
|
||||
, pure No <* string "%.n"
|
||||
, pure Pam <* char '&'
|
||||
, pure Bar <* char '|'
|
||||
, pure Sig <* char '~'
|
||||
, pure Lus <* char '+'
|
||||
, pure Hep <* char '-'
|
||||
, Cord <$> cord
|
||||
, Tape <$> tape
|
||||
]
|
||||
|
||||
-- Rune Helpers ------------------------------------------------------------------------------------
|
||||
|
||||
{-
|
||||
- If the parser is in `Wide` mode, only accept the `wide` form.
|
||||
- If the parser is in `Tall` mode, either
|
||||
- accept the `tall` form or:
|
||||
- swich to `Wide` mode and then accept the wide form.
|
||||
-}
|
||||
parseRune ∷ Parser a → Parser a → Parser a
|
||||
parseRune tall wide = get >>= \case
|
||||
Wide → wide
|
||||
Tall → tall <|> inWideMode wide
|
||||
|
||||
rune1 ∷ (a→b) → Parser a → Parser b
|
||||
rune1 node x = parseRune tall wide
|
||||
where tall = do gap; p←x; pure (node p)
|
||||
wide = do pal; p←x; par; pure (node p)
|
||||
|
||||
rune2 ∷ (a→b→c) → Parser a → Parser b → Parser c
|
||||
rune2 node x y = parseRune tall wide
|
||||
where tall = do gap; p←x; gap; q←y; pure (node p q)
|
||||
wide = do pal; p←x; ace; q←y; par; pure (node p q)
|
||||
|
||||
rune3 ∷ (a→b→c→d) → Parser a → Parser b → Parser c → Parser d
|
||||
rune3 node x y z = parseRune tall wide
|
||||
where tall = do gap; p←x; gap; q←y; gap; r←z; pure (node p q r)
|
||||
wide = do pal; p←x; ace; q←y; ace; r←z; par; pure (node p q r)
|
||||
|
||||
rune4 ∷ (a→b→c→d→e) → Parser a → Parser b → Parser c → Parser d → Parser e
|
||||
rune4 node x y z g = parseRune tall wide
|
||||
where tall = do gap; p←x; gap; q←y; gap; r←z; gap; s←g; pure (node p q r s)
|
||||
wide = do pal; p←x; ace; q←y; ace; r←z; ace; s←g; pure (node p q r s)
|
||||
|
||||
runeN ∷ ([a]→b) → Parser a → Parser b
|
||||
runeN node elem = node <$> parseRune tall wide
|
||||
where tall = gap >> elems
|
||||
where elems = term <|> elemAnd
|
||||
elemAnd = do x ← elem; gap; xs ← elems; pure (x:xs)
|
||||
term = string "==" *> pure []
|
||||
wide = pal *> option [] elems <* par
|
||||
where elems = (:) <$> elem <*> many (ace >> elem)
|
||||
|
||||
runeNE ∷ (NonEmpty a → b) → Parser a → Parser b
|
||||
runeNE node elem = node <$> parseRune tall wide
|
||||
where tall = do
|
||||
let elems = term <|> elemAnd
|
||||
elemAnd = do x ← elem; gap; xs ← elems; pure (x:xs)
|
||||
term = string "==" *> pure []
|
||||
fst <- gap *> elem
|
||||
rst <- gap *> elems
|
||||
pure (fst :| rst)
|
||||
wide = mzero -- No wide form for cores
|
||||
|
||||
-- Irregular Syntax --------------------------------------------------------------------------------
|
||||
|
||||
inc ∷ Parser Hoon -- +(3)
|
||||
inc = do
|
||||
string "+("
|
||||
h ← hoon
|
||||
char ')'
|
||||
pure h
|
||||
|
||||
equals ∷ Parser (Hoon, Hoon) -- =(3 4)
|
||||
equals = do
|
||||
string "=("
|
||||
x ← hoon
|
||||
ace
|
||||
y ← hoon
|
||||
char ')'
|
||||
pure (x, y)
|
||||
|
||||
tuple ∷ ∀a. Parser a → Parser [a]
|
||||
tuple p = char '[' >> elems
|
||||
where
|
||||
xs ∷ Parser [a]
|
||||
xs = do { x ← p; (x:) <$> tail }
|
||||
|
||||
tail ∷ Parser [a]
|
||||
tail = (pure [] <* char ']')
|
||||
<|> (ace >> elems)
|
||||
|
||||
elems ∷ Parser [a]
|
||||
elems = (pure [] <* char ']') <|> xs
|
||||
|
||||
irregular ∷ Parser Hoon
|
||||
irregular =
|
||||
inWideMode $
|
||||
choice [ Tupl <$> tuple hoon
|
||||
, IncrIrr <$> inc
|
||||
, uncurry IsEqIrr <$> equals
|
||||
]
|
||||
|
||||
-- Runes -------------------------------------------------------------------------------------------
|
||||
|
||||
cRune ∷ (Map Sym Hoon → a) → Parser a
|
||||
cRune f = do
|
||||
mode ← get
|
||||
guard (mode == Tall)
|
||||
gap
|
||||
f . mapFromList <$> arms -- TODO Complain about duplicated arms
|
||||
where
|
||||
arms :: Parser [(Sym, Hoon)]
|
||||
arms = many arm <* string "--"
|
||||
|
||||
arm :: Parser (Sym, Hoon)
|
||||
arm = do
|
||||
string "++"
|
||||
gap
|
||||
s ← sym
|
||||
gap
|
||||
h ← hoon
|
||||
gap
|
||||
pure (s, h)
|
||||
|
||||
data Skin
|
||||
|
||||
rune ∷ Parser Hoon
|
||||
rune = runeSwitch [ ("|=", rune2 BarTis hoon hoon)
|
||||
, ("|-", rune1 BarHep hoon)
|
||||
, (":-", rune2 ColHep hoon hoon)
|
||||
, (":+", rune3 ColLus hoon hoon hoon)
|
||||
, (":^", rune4 ColKet hoon hoon hoon hoon)
|
||||
, (":*", runeN ColTar hoon)
|
||||
, (":~", runeN ColSig hoon)
|
||||
, ("^-", rune2 KetHep spec hoon)
|
||||
, ("=<", rune2 TisGal hoon hoon)
|
||||
, ("=>", rune2 TisGar hoon hoon)
|
||||
, ("?:", rune3 WutCol hoon hoon hoon)
|
||||
, ("?=", rune2 WutTis spec hoon)
|
||||
, ("?@", rune3 WutPat hoon hoon hoon)
|
||||
, ("?^", rune3 WutKet hoon hoon hoon)
|
||||
, (".+", rune1 Incr hoon)
|
||||
, (".=", rune2 IsEq hoon hoon)
|
||||
, ("^=", rune2 KetTis sym hoon)
|
||||
, ("=.", rune3 TisDot wing hoon hoon)
|
||||
, ("|%", cRune BarCen)
|
||||
]
|
||||
|
||||
runeSwitch ∷ [(Text, Parser a)] → Parser a
|
||||
runeSwitch = choice . fmap (\(s, p) → string s *> p)
|
||||
|
||||
-- runeSwitch ∷ [(String, Parser a)] → Parser a
|
||||
-- runeSwitch = parseBasedOnRune
|
||||
-- . fmap (\([x,y], p) → (x, (y,p)))
|
||||
-- where
|
||||
-- parseBasedOnRune ∷ [(Char, (Char, Parser a))] → Parser a
|
||||
-- parseBasedOnRune = combine . restructure
|
||||
-- where combine = lexThen . overSnd lexThen
|
||||
-- overSnd f = fmap (\(x,y) → (x,f y))
|
||||
-- lexThen = choice . fmap (\(x,y) → char x *> y)
|
||||
-- restructure = MM.assocs
|
||||
-- . MM.fromList
|
||||
|
||||
-- Infix Syntax ------------------------------------------------------------------------------------
|
||||
|
||||
colInfix ∷ Parser Hoon
|
||||
colInfix = do
|
||||
x ← try (hoonNoInfix <* char ':')
|
||||
y ← hoon
|
||||
pure (ColOp x y)
|
||||
|
||||
faceOp ∷ Parser Hoon
|
||||
faceOp = FaceOp <$> try (sym <* char '=')
|
||||
<*> hoon
|
||||
|
||||
infixOp ∷ Parser Hoon
|
||||
infixOp = do
|
||||
inWideMode (colInfix <|> faceOp)
|
||||
|
||||
-- Hoon Parser -------------------------------------------------------------------------------------
|
||||
|
||||
hoonNoInfix ∷ Parser Hoon
|
||||
hoonNoInfix = irregular <|> rune <|> literal
|
||||
|
||||
hoon ∷ Parser Hoon
|
||||
hoon = infixOp <|> hoonNoInfix
|
||||
|
||||
-- Entry Point -------------------------------------------------------------------------------------
|
||||
|
||||
hoonFile = do
|
||||
option () whitespace
|
||||
h ← hoon
|
||||
option () whitespace
|
||||
eof
|
||||
pure h
|
||||
|
||||
parse :: Text -> Either Text Hoon
|
||||
parse txt =
|
||||
runParser (evalStateT hoonFile Tall) "stdin" txt & \case
|
||||
Left e -> Left (pack $ errorBundlePretty e)
|
||||
Right x -> pure x
|
||||
|
||||
parseHoonTest ∷ Text → IO ()
|
||||
parseHoonTest = parseTest (evalStateT hoonFile Tall)
|
||||
|
||||
main ∷ IO ()
|
||||
main = (head <$> getArgs) >>= parseHoonTest
|
||||
|
||||
|
||||
-- Parse Spec ------------------------------------------------------------------
|
||||
|
||||
base :: Parser Base
|
||||
base = choice [ BVoid <$ char '!'
|
||||
, BNull <$ char '~'
|
||||
, BFlag <$ char '?'
|
||||
, BNoun <$ char '*'
|
||||
, BCell <$ char '^'
|
||||
, BAtom <$ char '@'
|
||||
]
|
||||
|
||||
specTuple ∷ Parser Spec
|
||||
specTuple = tuple spec >>= \case
|
||||
[] -> mzero
|
||||
x:xs -> pure (STuple (x :| xs))
|
||||
|
||||
specFace ∷ Parser Spec
|
||||
specFace = SFaceOp <$> try (sym <* char '=') <*> spec
|
||||
|
||||
specIrregular ∷ Parser Spec
|
||||
specIrregular = inWideMode (specTuple <|> specFace)
|
||||
|
||||
spec :: Parser Spec
|
||||
spec = specIrregular <|> specRune <|> fmap SBase base
|
||||
|
||||
specRune ∷ Parser Spec
|
||||
specRune = choice
|
||||
[ string "$:" >> runeNE SBucCol spec
|
||||
, string "$-" >> rune2 SBucHep spec spec
|
||||
, string "$=" >> rune2 SBucTis sym spec
|
||||
, string "$?" >> runeNE SBucWut spec
|
||||
, string "$@" >> rune2 SBucPat spec spec
|
||||
, string "$^" >> rune2 SBucKet spec spec
|
||||
, string "$%" >> runeNE SBucCen spec
|
||||
]
|
||||
@ -1,66 +0,0 @@
|
||||
-- TODO Handle comments
|
||||
|
||||
module Language.Hoon.AST.Types where
|
||||
|
||||
import ClassyPrelude
|
||||
import Data.List.NonEmpty (NonEmpty)
|
||||
|
||||
-- AST Types -------------------------------------------------------------------
|
||||
|
||||
type Nat = Int
|
||||
type Sym = String
|
||||
type Wing = [Either Nat Sym]
|
||||
|
||||
data Base = BVoid | BNull | BFlag | BNoun | BCell | BAtom
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Spec
|
||||
= SBase Base -- ^, ?
|
||||
| SFaceOp Sym Spec -- x=@
|
||||
| SBucCol (NonEmpty Spec) -- $:
|
||||
| SBucHep Spec Spec -- $-, function core
|
||||
| SBucTis Sym Spec -- $=, name
|
||||
| SBucWut (NonEmpty Spec) -- $?, full pick
|
||||
| SBucPat Spec Spec -- $@, atom pick
|
||||
| SBucKet Spec Spec -- $^, cons pick
|
||||
| SBucCen (NonEmpty Spec) -- $%, head pick
|
||||
| STuple (NonEmpty Spec) -- [@ @]
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Hoon
|
||||
= WutCol Hoon Hoon Hoon -- ?:(c t f)
|
||||
| WutTis Spec Hoon -- ?=(@ 0)
|
||||
| WutPat Hoon Hoon Hoon -- ?@(c t f)
|
||||
| WutKet Hoon Hoon Hoon -- ?^(c t f)
|
||||
| KetTis Sym Hoon -- ^=(x 3)
|
||||
| ColHep Hoon Hoon -- :-(a b)
|
||||
| ColLus Hoon Hoon Hoon -- :+(a b c)
|
||||
| ColKet Hoon Hoon Hoon Hoon -- :^(a b c d)
|
||||
| ColTar [Hoon] -- :*(a as ...)
|
||||
| ColSig [Hoon] -- :~(a as ...)
|
||||
| KetHep Spec Hoon -- ^-(s h)
|
||||
| TisGal Hoon Hoon -- =<(a b)
|
||||
| TisGar Hoon Hoon -- =>(a b)
|
||||
| BarTis Hoon Hoon -- |=(s h)
|
||||
| BarHep Hoon -- |-(a)
|
||||
| TisDot Wing Hoon Hoon -- =.(a 3 a)
|
||||
| BarCen (Map Sym Hoon) -- |% ++ a 3 --
|
||||
| ColOp Hoon Hoon -- [+ -]:[3 4]
|
||||
| Tupl [Hoon] -- [a b]
|
||||
| FaceOp Sym Hoon -- x=y
|
||||
| Wing Wing -- ., a, a.b
|
||||
| Atom Nat -- 3
|
||||
| Cord Text -- 'cord'
|
||||
| Tape Text -- "tape"
|
||||
| Incr Hoon -- .+(3)
|
||||
| IncrIrr Hoon -- +(3)
|
||||
| IsEq Hoon Hoon -- .=(3 4)
|
||||
| IsEqIrr Hoon Hoon -- =(3 4)
|
||||
| Lus -- +
|
||||
| Hep -- -
|
||||
| Pam -- &
|
||||
| Bar -- |
|
||||
| Yes -- %.y
|
||||
| No -- %.n
|
||||
| Sig -- ~
|
||||
deriving (Eq, Ord, Show)
|
||||
@ -1,187 +0,0 @@
|
||||
module Language.Hoon.Desugar (desugar) where
|
||||
|
||||
import Prelude
|
||||
|
||||
import Data.List.NonEmpty (NonEmpty((:|)))
|
||||
import qualified Data.Map as Map
|
||||
|
||||
import Language.Hoon.Nock.Types
|
||||
import Language.Hoon.Types
|
||||
import Language.Hoon.SpecToMold
|
||||
import Language.Hoon.SpecToBunt
|
||||
|
||||
-- open:ap
|
||||
desugar :: Bool -> Hoon -> BHoon
|
||||
desugar fab = go
|
||||
where
|
||||
-- things that are already desugared
|
||||
go (HAutocons hs) = BAutocons (map go hs)
|
||||
go (HDebug s h) = BDebug s (go h)
|
||||
go (Hand t nk) = BHand t nk
|
||||
-- but open:ap also strips note
|
||||
go (Note note h) = BNote note (go h)
|
||||
go (Fits h w) = BFits (go h) w
|
||||
go (Sand n nou) = BSand n nou
|
||||
go (Rock n nou) = BRock n nou
|
||||
go (Tune t) = BTune t
|
||||
go (Lost h) = BLost (go h)
|
||||
--
|
||||
go (BarCen n b) = BBarCen n (Map.map (Map.map (\(w, h) -> (w, go h))) b)
|
||||
go (BarPat n b) = BBarPat n (Map.map (Map.map (\(w, h) -> (w, go h))) b)
|
||||
--
|
||||
go (CenTis w cs) = BCenTis w (map (\(w, h) -> (w, go h)) cs)
|
||||
--
|
||||
go (DotKet s h) = BDotKet s (go h)
|
||||
go (DotLus h) = BDotLus (go h)
|
||||
go (DotTar h j) = BDotTar (go h) (go j)
|
||||
go (DotTis h j) = BDotTis (go h) (go j)
|
||||
go (DotWut h) = BDotWut (go h)
|
||||
--
|
||||
go (KetBar h) = BKetBar (go h)
|
||||
go (KetCen h) = BKetCen (go h)
|
||||
go (KetLus h j) = BKetLus (go h) (go j)
|
||||
go (KetPam h) = BKetPam (go h)
|
||||
go (KetSig h) = BKetSig (go h)
|
||||
go (KetWut h) = BKetWut (go h)
|
||||
--
|
||||
go (SigGar hint mh j) = BSigGar hint (fmap go mh) (go j)
|
||||
go (SigZap h j) = BSigZap (go h) (go j)
|
||||
--
|
||||
go (TisGar h j) = BTisGar (go h) (go j)
|
||||
go (TisCom h j) = BTisCom (go h) (go j)
|
||||
--
|
||||
go (WutCol h j k) = BWutCol (go h) (go j) (go k)
|
||||
go (WutHax s w) = BWutHax s w
|
||||
--
|
||||
go (ZapCom h j) = BZapCom (go h) (go j)
|
||||
go (ZapMic h j) = BZapMic (go h) (go j)
|
||||
go (ZapTis h) = BZapTis (go h)
|
||||
go (ZapPat ws h j) = BZapPat ws (go h) (go j)
|
||||
go ZapZap = BZapZap
|
||||
|
||||
|
||||
go (H_ axis) = (BCenTis [AxisLimb axis] [])
|
||||
--
|
||||
go (HBase basetype) = go (specToMold fab (SBase basetype))
|
||||
go (Bust basetype) = go (specToBunt fab (SBase basetype))
|
||||
go (KetCol spec) = go (specToMold fab spec)
|
||||
-- writen into open:ap even though mint:ut uses handles debug case directly
|
||||
-- go (Debug h) = go h
|
||||
go (Error msg) = error ("%slog.[0 leaf/" ++ msg ++ "]")
|
||||
--
|
||||
go (Knit woofs) = error "TODO: implement %knit desugar"
|
||||
--
|
||||
go (HLeaf name atom) = go (specToMold fab (SLeaf name atom))
|
||||
go (Limb name) = (BCenTis [NameLimb name] [])
|
||||
go (Wing wing) = (BCenTis wing [])
|
||||
go (Tell hs) = go (CenCol (Limb "noah") [ZapGar (ColTar hs)])
|
||||
go (Yell hs) = go (CenCol (Limb "cain") [ZapGar (ColTar hs)])
|
||||
go (Xray _) = error "TODO: %xray not implemented"
|
||||
--
|
||||
-- TODO implement bars
|
||||
--
|
||||
go (ColKet h1 h2 h3 h4) = BAutocons (map go [h1, h2, h3, h4])
|
||||
go (ColLus h1 h2 h3) = BAutocons (map go [h1, h2, h3])
|
||||
go (ColCab h1 h2) = BAutocons (map go [h2, h1])
|
||||
go (ColHep h1 h2) = BAutocons (map go [h1, h2])
|
||||
go (ColSig hs) = BAutocons (map go hs ++ [BRock "n" (Atom 0)])
|
||||
go (ColTar (h :| hs)) = BAutocons (go h : map go hs)
|
||||
--
|
||||
go (KetTar spec) = BKetSig (go (specToBunt fab spec))
|
||||
--
|
||||
-- CenTis, but the product is cast to the type of the old value
|
||||
go (CenCab wing changes) = BKetLus (go (Wing wing))
|
||||
(BCenTis wing (desugarChanges changes))
|
||||
go (CenDot h1 h2) = go (CenCol h2 [h1])
|
||||
go (CenKet h1 h2 h3 h4) = go (CenCol h1 [h2, h3, h4])
|
||||
go (CenLus h1 h2 h3) = go (CenCol h1 [h2, h3])
|
||||
go (CenHep h1 h2) = go (CenCol h1 [h2])
|
||||
-- the implementation that "probably should work, but doesn't"
|
||||
go (CenCol h hs)
|
||||
= go (CenTar [NameLimb ""] h [([AxisLimb 6], HAutocons hs)])
|
||||
-- in lieu of the "electroplating" implementation
|
||||
go (CenSig wing h hs) = go (CenTar wing h [([AxisLimb 6], HAutocons hs)])
|
||||
go (CenTar wing h changes)
|
||||
| null changes = BTisGar (go (Wing wing)) (go h)
|
||||
| otherwise = go (TisLus h (CenTis (wing ++ [AxisLimb 2]) changes))
|
||||
--
|
||||
go (KetDot h j) = BKetLus (go (CenCol h [j])) (go j)
|
||||
go (KetHep spec h) = BKetLus (go (specToBunt fab spec)) (go h)
|
||||
go (KetTis skin h) = go (grip skin h)
|
||||
--
|
||||
go (SigBar h j) = BSigGar "mean" (Just (hint h)) (go j)
|
||||
where
|
||||
hint (Sand "tas" x) = (BRock "tas" x)
|
||||
hint (HDebug _ h) = hint h
|
||||
hint h = go (BarDot (CenCol (Limb "cain") [ZapGar (TisGar (H_ 3) h)]))
|
||||
go (SigCab h j) = BSigGar "mean" (Just (go (BarDot h))) (go j)
|
||||
go (SigCen chum h tyre j) = error "desugar: TODO ~% not supported"
|
||||
go (SigFas chum h) = error "desugar: TODO ~/ not supported"
|
||||
go (SigLed n mh j) = BTisGar (go j) (BSigGar n (fmap go mh) (go (H_ 1)))
|
||||
go (SigBuc name h)
|
||||
= BSigGar "live" (Just (BRock "" (nameToAtom name))) (go h)
|
||||
go (SigLus atom h) = BSigGar "memo" (Just (BRock "" (Atom atom))) (go h)
|
||||
go (SigPam atom h j)
|
||||
= BSigGar
|
||||
"slog"
|
||||
(Just (BAutocons [BSand "" (Atom atom)
|
||||
, go (CenCol (Limb "cain") [ZapGar j])]))
|
||||
(go j)
|
||||
go (SigTis h j) = BSigGar "germ" (Just (go h)) (go j)
|
||||
go (SigWut atom h j k)
|
||||
= go (TisLus
|
||||
(WutDot j (Bust SNull) (HAutocons [Bust SNull, k]))
|
||||
(WutSig
|
||||
[AxisLimb 2]
|
||||
(TisGar (H_ 3) k)
|
||||
(SigPam atom (H_ 5) (TisGar (H_ 3) k))))
|
||||
--
|
||||
-- TODO mic runes
|
||||
--
|
||||
go (TisBar h j) = go (TisLus (specToBunt fab h) j)
|
||||
--go (TisTar name Nothing h j) = BTisGar (BTune Tone) j
|
||||
--go (TisTar name (Just spec) h j) = undefined
|
||||
go (TisCol chs h) = BTisGar (go (CenCab [AxisLimb 1] chs)) (go h)
|
||||
go (TisFas skin h j) = go (TisLus (KetTis skin h) j)
|
||||
go (TisDot w h j) = BTisGar (go (CenCab [AxisLimb 1] [(w, h)])) (go j)
|
||||
go (TisWut w h j k) = go (TisDot w (WutCol h j (Wing w)) k)
|
||||
--go (TisKet skin wing h j)
|
||||
-- = BTisGar
|
||||
-- (go (KetTis
|
||||
go (TisLed h j) = BTisGar (go j) (go h)
|
||||
go (TisLus h j) = BTisGar (go (HAutocons [h, (H_ 1)])) (go j)
|
||||
go (TisHep h j) = go (TisLus j h)
|
||||
go (TisSig hs) = foldr BTisGar (go (H_ 1)) (map go hs)
|
||||
--
|
||||
go (WutBar hs)
|
||||
= foldr
|
||||
(\h r -> BWutCol (go h) (BRock "f" (Atom 0)) r)
|
||||
(BRock "f" (Atom 1))
|
||||
hs
|
||||
go (WutPam hs)
|
||||
= foldr
|
||||
(\h r -> BWutCol (go h) r (BRock"f" (Atom 1)))
|
||||
(BRock "f" (Atom 0))
|
||||
hs
|
||||
go (WutDot h j k) = BWutCol (go h) (go k) (go j)
|
||||
go (WutLed h j) = BWutCol (go h) BZapZap (go j)
|
||||
go (WutGar h j) = BWutCol (go h) (go j) BZapZap
|
||||
go (WutKet wing h j)
|
||||
= BWutCol (go (WutTis (SBase (SAtom "")) wing)) (go h) (go j)
|
||||
|
||||
--go (WutKet
|
||||
--
|
||||
go (ZapWut (Left vers) h)
|
||||
| vers >= hoonVersion = go h
|
||||
| otherwise = error "hoon-version"
|
||||
go (ZapWut (Right (lower, upper)) h)
|
||||
| lower <= hoonVersion && hoonVersion <= upper = go h
|
||||
| otherwise = error "hoon-version"
|
||||
|
||||
desugarChanges = map (\(w, h) -> (w, go h))
|
||||
|
||||
grip :: Skin -> Hoon -> Hoon
|
||||
grip = error "grip not implemented"
|
||||
|
||||
|
||||
|
||||
@ -1,183 +0,0 @@
|
||||
module Language.Hoon.IR.Desugar where
|
||||
|
||||
import ClassyPrelude hiding (union)
|
||||
|
||||
import Language.Hoon.IR.Ty
|
||||
import Control.Lens
|
||||
|
||||
import Data.Foldable (foldr1)
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
import Data.Char (ord)
|
||||
import Text.Show.Pretty (pPrint)
|
||||
|
||||
import qualified Language.Hoon.AST.Parser as AST
|
||||
import qualified Language.Hoon.AST.Types as AST
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Language.Hoon.IR.Infer as IR
|
||||
import qualified Language.Hoon.IR.Ty as IR
|
||||
import qualified Language.Hoon.LL.Run as LL
|
||||
import qualified Language.Hoon.LL.Types as LL
|
||||
import qualified Prelude
|
||||
import qualified System.Exit as Sys
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
list :: [IR.Hoon] -> IR.Hoon
|
||||
list [] = HAtom 0
|
||||
list (x:xs) = HCons x (list xs)
|
||||
|
||||
tuple :: NonEmpty IR.Hoon -> IR.Hoon
|
||||
tuple (x :| []) = x
|
||||
tuple (x :| y : zs) = HCons x (tuple (y :| zs))
|
||||
|
||||
baseToTy :: AST.Base -> Ty
|
||||
baseToTy = \case
|
||||
AST.BVoid -> bot
|
||||
AST.BNull -> tyNull
|
||||
AST.BFlag -> tyBool
|
||||
AST.BNoun -> top
|
||||
AST.BCell -> tyAnyCell `union` tyAnyCore
|
||||
AST.BAtom -> tyAnyAtom
|
||||
|
||||
gateTy :: Ty -> Ty -> Ty -> Ty
|
||||
gateTy ctx arg result = tyCore batt ctx
|
||||
where
|
||||
batt = mapFromList [("", result)]
|
||||
ctx = tyCell arg ctx
|
||||
|
||||
specToTy :: AST.Spec -> Ty
|
||||
specToTy = \case
|
||||
AST.SBase b -> baseToTy b
|
||||
AST.SFaceOp f s -> specToTy (AST.SBucTis f s)
|
||||
AST.STuple specs -> specToTy (AST.SBucCol specs)
|
||||
AST.SBucCol specs -> foldr1 tyCell (specToTy <$> specs)
|
||||
AST.SBucHep a r -> gateTy top (specToTy a) (specToTy r) -- TODO Ctx type
|
||||
AST.SBucTis s y -> let y' = specToTy y
|
||||
in y' { tFace = Set.insert s (tFace y') }
|
||||
AST.SBucWut specs -> foldr1 union (specToTy <$> specs)
|
||||
AST.SBucPat x y -> specToTy x `union` specToTy x
|
||||
AST.SBucKet x y -> specToTy x `union` specToTy y
|
||||
AST.SBucCen specs -> foldr1 union (specToTy <$> specs)
|
||||
|
||||
armNm "" = "$"
|
||||
armNm nm = nm
|
||||
|
||||
arm :: Sym -> AST.Hoon -> Either String (Ty, AST.Hoon)
|
||||
arm _ (AST.KetHep s h) = pure (specToTy s, h)
|
||||
arm nm _ = Left msg
|
||||
where msg = mconcat [ "Arm ", armNm nm, " needs a type declaration" ]
|
||||
|
||||
axisPath :: Nat -> Maybe TreePath
|
||||
axisPath 0 = Nothing
|
||||
axisPath 1 = Just []
|
||||
axisPath 2 = Just [False]
|
||||
axisPath 3 = Just [True]
|
||||
axisPath n
|
||||
| 0==(n `rem` 2) = (++) <$> axisPath (n `quot` 2) <*> axisPath 2
|
||||
| otherwise = (++) <$> axisPath (n `quot` 2) <*> axisPath 3
|
||||
|
||||
mbErr :: String -> Maybe a -> Either String a
|
||||
mbErr err = \case Nothing -> Left err
|
||||
Just a -> pure a
|
||||
|
||||
wing :: AST.Wing -> Either String Wing
|
||||
wing = traverse \case
|
||||
Left a -> WAxis <$> mbErr "+0 is not valid" (axisPath a)
|
||||
Right n -> Right (WName n)
|
||||
|
||||
core :: Map Sym AST.Hoon -> Either String (Map Sym (Ty, AST.Hoon))
|
||||
core = Map.traverseWithKey arm
|
||||
|
||||
desugar :: AST.Hoon -> Either String IR.Hoon
|
||||
desugar = \case
|
||||
AST.Sig -> pure (HAtom 0)
|
||||
AST.No -> pure (HAtom 1)
|
||||
AST.Yes -> pure (HAtom 0)
|
||||
AST.Bar -> pure (HAtom 1)
|
||||
AST.Pam -> pure (HAtom 0)
|
||||
AST.Hep -> pure (HRef [WAxis [False]])
|
||||
AST.Lus -> pure (HRef [WAxis [True]])
|
||||
AST.IsEqIrr x y -> desugar (AST.IsEq x y)
|
||||
AST.IsEq x y -> HEq <$> desugar x <*> desugar y
|
||||
AST.IncrIrr x -> desugar (AST.Incr x)
|
||||
AST.Incr x -> HSucc <$> desugar x
|
||||
AST.Tape t -> pure (list (HAtom . ord <$> unpack t))
|
||||
AST.Cord _ -> pure (HAtom 1337)
|
||||
AST.Atom a -> pure (HAtom a)
|
||||
AST.Wing ss -> HRef <$> wing ss
|
||||
AST.FaceOp n h -> desugar (AST.KetTis n h)
|
||||
AST.KetTis n h -> HFace n <$> desugar h
|
||||
AST.Tupl xs -> desugar (AST.ColTar xs)
|
||||
AST.ColOp x y -> desugar (AST.TisGal x y)
|
||||
AST.BarCen arms -> do bat <- core arms >>= traverse (traverseOf _2 desugar)
|
||||
pure (HCore bat)
|
||||
AST.TisDot w x y -> do x <- desugar x
|
||||
y <- desugar y
|
||||
w <- wing w
|
||||
pure (HWith
|
||||
(HEdit w
|
||||
(HLike (HRef w) x)
|
||||
(HRef []))
|
||||
y)
|
||||
AST.BarTis s h -> desugar (AST.TisGar
|
||||
(AST.Tupl [s, AST.Wing []])
|
||||
(AST.BarCen (mapFromList [("", h)])))
|
||||
AST.BarHep x -> do (t, x') <- arm "" x
|
||||
x'' <- desugar x'
|
||||
pure (HWith
|
||||
(HCore (mapFromList [("", (t, x''))]))
|
||||
(HRef [WName ""]))
|
||||
AST.TisGal x y -> desugar (AST.TisGar y x)
|
||||
AST.TisGar x y -> HWith <$> desugar x <*> desugar y
|
||||
AST.KetHep s x -> HCast (specToTy s) <$> desugar x
|
||||
AST.ColSig xs -> list <$> traverse desugar xs
|
||||
AST.ColTar [] -> Left "empty tuple"
|
||||
AST.ColTar (x:xs) -> tuple <$> traverse desugar (x :| xs)
|
||||
AST.ColHep x y -> desugar (AST.ColTar [x, y])
|
||||
AST.ColLus x y z -> desugar (AST.ColTar [x, y, z])
|
||||
AST.ColKet x y z a -> desugar (AST.ColTar [x, y, z, a])
|
||||
AST.WutTis s h -> do h <- desugar h
|
||||
pure (HNest (Pat $ specToTy s) h)
|
||||
AST.WutKet x y z -> desugar (AST.WutPat x z y)
|
||||
AST.WutPat x y z -> do x <- desugar x
|
||||
y <- desugar y
|
||||
z <- desugar z
|
||||
pure (HIf (HNest (Pat tyAnyAtom) x) y z)
|
||||
AST.WutCol x y z -> HIf <$> desugar x <*> desugar y <*> desugar z
|
||||
|
||||
getRightAndShow :: Show r => (l -> Text) -> Either l r -> IO r
|
||||
getRightAndShow err = \case
|
||||
Left e -> putStrLn (err e) >> Sys.exitFailure
|
||||
Right x -> pPrint x >> putStrLn "" >> pure x
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
ex <- Prelude.head <$> getArgs
|
||||
putStrLn "== Parsing =="
|
||||
ast <- getRightAndShow id (AST.parse ex)
|
||||
putStrLn "== Desugaring =="
|
||||
ir <- getRightAndShow pack (desugar ast)
|
||||
putStrLn "== Type Inferring =="
|
||||
ty <- getRightAndShow pack (IR.infer tyNull ir)
|
||||
putStrLn "== Compiling =="
|
||||
ll <- getRightAndShow pack (IR.down tyNull ir)
|
||||
putStrLn "== Result Type =="
|
||||
_ <- getRightAndShow pack (Right (ll ^. LL.llTy))
|
||||
putStrLn "== Result =="
|
||||
res <- getRightAndShow pack (LL.runLL (LL.VAtom 0) ll)
|
||||
pure ()
|
||||
|
||||
sugar :: LL.LL a -> AST.Hoon
|
||||
sugar = \case
|
||||
LL.LWith _ x y -> AST.ColOp (sugar y) (sugar x)
|
||||
LL.LAxis _ p -> undefined
|
||||
LL.LEdit _ p x y -> AST.TisDot undefined undefined undefined
|
||||
LL.LFire _ s _ -> AST.Wing [Right s]
|
||||
LL.LAtom _ n -> AST.Atom n
|
||||
LL.LPair _ x y -> AST.Tupl [sugar x, sugar y]
|
||||
LL.LCore _ _bat -> undefined
|
||||
LL.LSucc _ x -> AST.IncrIrr (sugar x)
|
||||
LL.LTest _ x y z -> AST.WutCol (sugar x) (sugar y) (sugar z)
|
||||
LL.LCelQ _ x -> AST.WutKet (sugar x) (AST.Atom 0) (AST.Atom 1)
|
||||
LL.LEqlQ _ x y -> AST.IsEqIrr (sugar x) (sugar y)
|
||||
@ -1,213 +0,0 @@
|
||||
module Language.Hoon.IR.Infer where
|
||||
|
||||
import ClassyPrelude hiding (union, intersect, subtract, negate)
|
||||
import Control.Monad.Fix
|
||||
import Data.Void
|
||||
import Language.Hoon.IR.Ty
|
||||
|
||||
import Data.List.NonEmpty
|
||||
import Language.Hoon.LL.Types hiding (L, R, Ctx)
|
||||
import Control.Category ((>>>))
|
||||
import Control.Lens
|
||||
import Data.Function ((&))
|
||||
import Data.Maybe (fromJust)
|
||||
|
||||
import qualified Language.Hoon.LL.Types as LL
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Language.Hoon.IR.Wing as Wing
|
||||
import qualified Prelude
|
||||
|
||||
|
||||
-- Code Inference --------------------------------------------------------------
|
||||
|
||||
infer :: Ty -> Hoon -> Either String Ty
|
||||
infer sut h = view llTy <$> down sut h
|
||||
|
||||
splitPattern :: Ty -> Ty -> (Ty, Ty)
|
||||
splitPattern pat sut = (pat `intersect` sut, pat `diff` sut)
|
||||
|
||||
traversePair :: Applicative f => (f a, f b) -> f (a, b)
|
||||
traversePair (mx, my) = (,) <$> mx <*> my
|
||||
|
||||
refine :: Wing -> Ty -> Ty -> Either String (Ty, Ty)
|
||||
refine w pat sut = do
|
||||
(_,oldTy) <- Wing.resolve w sut
|
||||
|
||||
let matchBr = pat `intersect` oldTy
|
||||
elseBr = pat `diff` oldTy
|
||||
update = \t -> snd <$> Wing.edit w t sut
|
||||
|
||||
traversePair (update matchBr, update elseBr)
|
||||
|
||||
extractRefinement :: Ty -> Hoon -> Either String (Ty, Ty)
|
||||
extractRefinement sut (HNest (Pat p) h@(HRef w)) = refine w p sut
|
||||
extractRefinement sut _ = pure (sut, sut)
|
||||
|
||||
|
||||
-- Resolve Names and Infer Types -----------------------------------------------
|
||||
|
||||
splitHoonPath :: HoonPath -> Either HoonPath (HoonPath, Sym, Core Ty)
|
||||
splitHoonPath pp = pp ^? _Snoc & \case
|
||||
Just (xs, Arm n c) -> Right (xs, n, c)
|
||||
_ -> Left pp
|
||||
|
||||
fromHoonPath :: HoonPath -> LLPath
|
||||
fromHoonPath = catMaybes . fmap \case
|
||||
Dot -> Nothing
|
||||
Arm _ _ -> Nothing
|
||||
L -> pure LL.L
|
||||
R -> pure LL.R
|
||||
Ctx -> pure LL.Ctx
|
||||
|
||||
resolve :: Ty -> Wing -> Either String LLTy
|
||||
resolve sut w = do
|
||||
(hoonPath, resTy) <- Wing.resolve w sut
|
||||
pure $ splitHoonPath hoonPath & \case
|
||||
Left p -> LAxis resTy (fromHoonPath p)
|
||||
Right (p, arm, core) -> lFire resTy (fromHoonPath p) arm core
|
||||
|
||||
where
|
||||
lFire :: Ty -> LLPath -> Sym -> Core Ty -> LLTy
|
||||
lFire ty [] arm (Core bat ctx) = LFire ty arm bat
|
||||
lFire ty axis arm (Core bat ctx) = LWith ty (LFire ty arm bat)
|
||||
(LAxis (tyCore bat ctx) axis)
|
||||
|
||||
-- TODO Should we produce an LFire if we edit an arm?
|
||||
mkEdit :: Ty -> Wing -> LLTy -> LLTy -> Either String LLTy
|
||||
mkEdit sut w v x = do
|
||||
(p,ty) <- Wing.edit w (x ^. llTy) (v ^. llTy)
|
||||
p <- pure (fromHoonPath p)
|
||||
pure (LEdit ty p v x)
|
||||
|
||||
disjoin, conjoin :: LLTy -> LLTy -> LLTy
|
||||
disjoin x y = LTest tyBool x llYes y
|
||||
conjoin x y = LTest tyBool x y llNo
|
||||
|
||||
negate :: LLTy -> LLTy
|
||||
negate x = LTest tyBool x llNo llYes
|
||||
|
||||
reduce1 :: (a -> a -> a) -> a -> [a] -> a
|
||||
reduce1 f z [] = z
|
||||
reduce1 f z (x:xs) = foldl' f x xs
|
||||
|
||||
disjoinAll, conjoinAll :: [LLTy] -> LLTy
|
||||
disjoinAll = reduce1 disjoin llYes
|
||||
conjoinAll = reduce1 conjoin llNo
|
||||
|
||||
fishAtom :: (LLPath, Ty) -> Nat -> Either String LLTy
|
||||
fishAtom (p, t) n = pure (LEqlQ tyBool (LAxis t p) (LAtom (tyConst n) n))
|
||||
|
||||
-- TODO maybe this is wrong?
|
||||
fishCell :: (LLPath, Ty) -> Cell Ty -> Either String LLTy
|
||||
fishCell (p, sut) (Cell l r) =
|
||||
let cellSut = bot { tCell = tCell sut }
|
||||
in if cellSut == bot then pure llNo else do
|
||||
lef <- Wing.getPath [L] cellSut
|
||||
rit <- Wing.getPath [R] cellSut
|
||||
left <- fishTy (p ++ [LL.L], lef) l
|
||||
right <- fishTy (p ++ [LL.R], rit) r
|
||||
pure (conjoin left right)
|
||||
|
||||
fishCore :: (LLPath, Ty) -> Core Ty -> Either String LLTy
|
||||
fishCore _ _ = Left "Can't fish using core type."
|
||||
|
||||
fishHappy :: Ord a
|
||||
=> ((LLPath, Ty) -> a -> Either String LLTy)
|
||||
-> (LLPath, Ty)
|
||||
-> Happy a
|
||||
-> Either String LLTy
|
||||
fishHappy f p (Fork (setToList -> xs)) = disjoinAll <$> traverse (f p) xs
|
||||
fishHappy f p (Isnt (setToList -> xs)) = conjoinAll <$> traverse (fmap negate . (f p)) xs
|
||||
|
||||
fishFork :: Ord a
|
||||
=> ((LLPath, Ty) -> a -> Either String LLTy)
|
||||
-> (LLPath, Ty)
|
||||
-> Fork a
|
||||
-> Either String LLTy
|
||||
fishFork f _ Top = pure llYes
|
||||
fishFork f p (FFork (setToList -> xs)) = disjoinAll <$> traverse (f p) xs
|
||||
|
||||
fishTy :: (LLPath, Ty) -> Ty -> Either String LLTy
|
||||
fishTy (p, sut) t@Ty{..} = do
|
||||
atomic <- fishHappy fishAtom (p, sut) tAtom
|
||||
core <- fishHappy fishCore (p, sut) tCore
|
||||
cellular <- fishFork fishCell (p, sut) tCell
|
||||
let atomic' = conjoin (negate (LCelQ tyBool (LAxis sut p))) atomic
|
||||
cellular' = conjoin (LCelQ tyBool (LAxis sut p)) cellular
|
||||
pure (disjoinAll [atomic, core, cellular])
|
||||
|
||||
doesNest :: LLTy -> Pat -> Either String LLTy
|
||||
doesNest (LAxis t p) (Pat ref) = fishTy (p, t) ref
|
||||
doesNest h (Pat ref) = do
|
||||
j <- fishTy ([], (h ^. llTy)) ref
|
||||
pure (LWith tyBool h (simplify j))
|
||||
|
||||
simplify :: LLTy -> LLTy
|
||||
simplify = \case
|
||||
LTest t c x y -> simplify c & \case
|
||||
LAtom _ 0 -> simplify x
|
||||
LAtom _ 1 -> simplify y
|
||||
c' -> LTest t c' (simplify x) (simplify y)
|
||||
LWith t x y -> LWith t (simplify x) (simplify y)
|
||||
LEdit t p x y -> LEdit t p (simplify x) (simplify y)
|
||||
LPair t x y -> LPair t (simplify x) (simplify y)
|
||||
LCore t b -> LCore t (simplify <$> b)
|
||||
LSucc t x -> LSucc t (simplify x)
|
||||
LCelQ t x -> LCelQ t (simplify x)
|
||||
LEqlQ t x y -> LEqlQ t (simplify x) (simplify y)
|
||||
ll -> ll
|
||||
|
||||
mbErr :: String -> Maybe a -> Either String a
|
||||
mbErr err = \case Nothing -> Left err
|
||||
Just a -> pure a
|
||||
|
||||
down :: Ty -> Hoon -> Either String LLTy
|
||||
down sut = \case
|
||||
HRef w -> resolve sut w
|
||||
HCast t h -> do h <- down sut h
|
||||
let nestFail = mconcat [ show (h ^. llTy)
|
||||
, " does not nest in "
|
||||
, show t
|
||||
]
|
||||
mbErr nestFail $ guard (view llTy h `nest` t)
|
||||
pure (h & set llTy t)
|
||||
HFace f h -> over llTy (addFace f) <$> down sut h
|
||||
HLike x y -> do x <- down sut x
|
||||
down sut (HCast (view llTy x) y)
|
||||
HEdit w v x -> do v <- down sut v
|
||||
x <- down sut x
|
||||
mkEdit sut w v x
|
||||
HEq h j -> do h <- down sut h
|
||||
j <- down sut j
|
||||
let (ht, jt) = (h ^. llTy, j ^. llTy)
|
||||
let nestFail = mconcat [ "type mismatch: "
|
||||
, show ht
|
||||
, " vs "
|
||||
, show jt
|
||||
]
|
||||
mbErr nestFail $ guard (nest ht jt || nest jt ht)
|
||||
pure (LEqlQ tyBool h j)
|
||||
HAtom a -> pure (LAtom (tyConst a) a)
|
||||
HCons h j -> do h <- down sut h
|
||||
j <- down sut j
|
||||
let ty = tyCell (h ^. llTy) (j ^. llTy)
|
||||
pure (LPair ty h j)
|
||||
HSucc h -> LSucc tyAnyAtom <$> down sut (HCast tyAnyAtom h)
|
||||
HIf c l r -> do (lSut, rSut) <- extractRefinement sut c
|
||||
c <- down sut c
|
||||
l <- down lSut l
|
||||
r <- down rSut r
|
||||
let nestFail = show c <> " is not a boolean value"
|
||||
mbErr nestFail $ guard (nest (c ^. llTy) tyBool)
|
||||
let res = view llTy l `union` view llTy r
|
||||
pure (LTest res c l r)
|
||||
HWith h j -> do h <- down sut h
|
||||
j <- down (h ^. llTy) j
|
||||
pure (LWith (j ^. llTy) h j)
|
||||
HNest p h -> do h <- down sut h
|
||||
doesNest h p
|
||||
HCore arms -> do let coreTy = tyCore (fst <$> arms) sut
|
||||
let go decl arm = down coreTy (HCast decl arm)
|
||||
arms <- traverse (uncurry go) arms
|
||||
pure (LCore coreTy arms)
|
||||
@ -1,660 +0,0 @@
|
||||
module Language.Hoon.IR.Ty where
|
||||
|
||||
import ClassyPrelude hiding (union, intersect)
|
||||
import Control.Lens
|
||||
import Control.Lens.TH
|
||||
import Control.Monad.Fix
|
||||
import Data.Void
|
||||
|
||||
import Control.Category ((>>>))
|
||||
import Data.Function ((&))
|
||||
import Data.Maybe (fromJust)
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Prelude
|
||||
|
||||
import Test.Tasty
|
||||
import Test.Tasty.TH
|
||||
import Test.Tasty.QuickCheck as QC
|
||||
import Test.QuickCheck
|
||||
|
||||
|
||||
-- Happy and Fork --------------------------------------------------------------
|
||||
|
||||
data Fork a = Top | FFork (Set a)
|
||||
deriving (Eq, Ord)
|
||||
|
||||
showHappy :: (Show a, Ord a) => String -> Set a -> String
|
||||
showHappy i xs = intercalate i (show <$> setToList xs)
|
||||
|
||||
instance (Ord a, Show a) => Show (Fork a)
|
||||
where
|
||||
show Top = "Top"
|
||||
show (FFork alts) | null alts = "Bot"
|
||||
show (FFork (setToList -> [x])) = show x
|
||||
show (FFork alts) =
|
||||
"(" <> showHappy " ∪ " alts <> ")"
|
||||
|
||||
data Happy a = Fork (Set a) | Isnt (Set a)
|
||||
deriving (Eq, Ord)
|
||||
|
||||
instance (Ord a, Show a) => Show (Happy a)
|
||||
where
|
||||
show (Isnt alts) | null alts = "Top"
|
||||
show (Fork alts) | null alts = "Bot"
|
||||
show (Fork (setToList -> [x])) = show x
|
||||
show (Isnt (setToList -> [x])) = "not:" <> show x
|
||||
show (Fork alts) = showHappy " ∪ " alts
|
||||
show (Isnt alts) = "not:" <> showHappy " ∩ " alts
|
||||
|
||||
_HappyFork :: Ord a => Prism' (Happy a) (Fork a)
|
||||
_HappyFork = prism' mk get
|
||||
where
|
||||
mk Top = Isnt mempty
|
||||
mk (FFork f) = Fork f
|
||||
get (Isnt i) = if null i then pure Top else Nothing
|
||||
get (Fork h) = pure (FFork h)
|
||||
|
||||
_Singleton :: Ord a => Prism' (Fork a) a
|
||||
_Singleton = prism' mk get
|
||||
where
|
||||
mk a = FFork (Set.singleton a)
|
||||
get = \case FFork (setToList -> [x]) -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
nullHappy :: Ord a => Happy a -> Bool
|
||||
nullHappy (Fork f) = null f
|
||||
nullHappy (Isnt i) = False
|
||||
|
||||
nullFork :: Ord a => Fork a -> Bool
|
||||
nullFork = nullHappy . review _HappyFork
|
||||
|
||||
traverseSet :: (Applicative f, Ord a, Ord b) => (a -> f b) -> Set a -> f (Set b)
|
||||
traverseSet f = fmap setFromList . traverse f . setToList
|
||||
|
||||
mapFork :: Ord b => Fork b -> (a -> b) -> Fork a -> Fork b
|
||||
mapFork top _ Top = top
|
||||
mapFork _ f (FFork k) = FFork (Set.map f k)
|
||||
|
||||
traverseFork :: (Applicative f, Ord a, Ord b)
|
||||
=> f (Fork b) -> (a -> f b) -> Fork a -> f (Fork b)
|
||||
traverseFork top f = \case
|
||||
Top -> top
|
||||
FFork k -> FFork <$> traverseSet f k
|
||||
|
||||
traverseHappyFork :: (Applicative f, Ord a)
|
||||
=> (a -> f a) -> Happy a -> f (Happy a)
|
||||
traverseHappyFork f = \case
|
||||
Isnt k -> pure (Isnt k)
|
||||
Fork k -> Fork <$> traverseSet f k
|
||||
|
||||
-- Type Types ------------------------------------------------------------------
|
||||
|
||||
type Sym = String
|
||||
type Nat = Int
|
||||
|
||||
data Cell t = Cell t t
|
||||
deriving (Eq, Ord)
|
||||
|
||||
instance Show t => Show (Cell t) where
|
||||
show (Cell l r) = mconcat [ "["
|
||||
, filter (/= '"') (show l)
|
||||
, " "
|
||||
, filter (/= '"') (show r)
|
||||
, "]"
|
||||
]
|
||||
|
||||
data Core t = Core (Map Sym t) t
|
||||
deriving (Eq, Ord)
|
||||
|
||||
instance Show t => Show (Core t) where
|
||||
show (Core batt ctx) = mconcat [ "%:("
|
||||
, filter (/= '"') (show ctx)
|
||||
, " → "
|
||||
, filter (/= '"') (show $ mapToList batt)
|
||||
, ")"
|
||||
]
|
||||
|
||||
data Func t = Func t t
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Ty = Ty { tFace :: Set Sym
|
||||
, tAtom :: Happy Nat
|
||||
, tCore :: Happy (Core Ty)
|
||||
, tCell :: Fork (Cell Ty)
|
||||
-- , tFunc :: Func Ty
|
||||
}
|
||||
deriving (Eq, Ord)
|
||||
|
||||
instance Show Ty
|
||||
where
|
||||
show t = "\"" <> showTy t <> "\""
|
||||
|
||||
showTy :: Ty -> String
|
||||
showTy t@Ty{..} = faces <> niceTy
|
||||
where
|
||||
niceTy = let tyNoFace = t { tFace = mempty } in
|
||||
if top == tyNoFace then "*" else
|
||||
if tyBool == tyNoFace then "?" else
|
||||
t ^? _Discrim & \case
|
||||
Just d -> show d
|
||||
Nothing -> let alts = catMaybes [ atoms, cores, cells ]
|
||||
in "(" <> intercalate " ∪ " alts <> ")"
|
||||
faces = if null tFace then "" else unpack (intercalate "," tFace <> "=")
|
||||
atoms = if tAtom == bot then Nothing
|
||||
else if tAtom == top then Just "@"
|
||||
else Just (show tAtom)
|
||||
cores = if tCore == bot then Nothing
|
||||
else if tCore == top then Just "%"
|
||||
else Just (show tCore)
|
||||
cells = if tCell == bot then Nothing
|
||||
else if tCell == top then Just "^"
|
||||
else Just (show tCell)
|
||||
|
||||
-- IR Types --------------------------------------------------------------------
|
||||
|
||||
type TreePath = [Bool]
|
||||
|
||||
data Limb
|
||||
= WName Sym
|
||||
| WAxis TreePath
|
||||
| WDot
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
type Wing = [Limb]
|
||||
|
||||
newtype Pat = Pat Ty
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data Hoon
|
||||
= HRef Wing
|
||||
| HNest Pat Hoon
|
||||
| HSucc Hoon
|
||||
| HEq Hoon Hoon
|
||||
| HIf Hoon Hoon Hoon
|
||||
| HAtom Nat
|
||||
| HCons Hoon Hoon
|
||||
| HEdit Wing Hoon Hoon
|
||||
| HWith Hoon Hoon
|
||||
| HFace Sym Hoon
|
||||
| HCore (Map Sym (Ty, Hoon))
|
||||
| HCast Ty Hoon
|
||||
| HLike Hoon Hoon
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
|
||||
-- Path Types ------------------------------------------------------------------
|
||||
|
||||
data HoonDir = Dot | L | R | Ctx | Arm Sym (Core Ty)
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
type HoonPath = [HoonDir]
|
||||
|
||||
|
||||
-- Type Discrimination ---------------------------------------------------------
|
||||
|
||||
data Discrim
|
||||
= DAtom (Fork Nat)
|
||||
| DCore (Fork (Core Ty)) -- TODO: Should this be Core Discrim
|
||||
| DCell (Fork (Cell Ty))
|
||||
| DCoreAndCell (Fork (Core Ty)) (Fork (Cell Ty))
|
||||
deriving (Eq, Ord)
|
||||
|
||||
instance Show Discrim where
|
||||
show = \case
|
||||
DAtom Top -> "@"
|
||||
DCore Top -> "%"
|
||||
DCell Top -> "^"
|
||||
|
||||
DAtom (FFork (setToList -> [])) -> "!"
|
||||
DCell (FFork (setToList -> [])) -> "!"
|
||||
DCore (FFork (setToList -> [])) -> "!"
|
||||
|
||||
DAtom (FFork (setToList -> [x])) -> show x
|
||||
DCell (FFork (setToList -> [x])) -> show x
|
||||
DCore (FFork (setToList -> [x])) -> show x
|
||||
|
||||
DAtom (FFork xs) -> showHappy " ∪ " xs
|
||||
DCell (FFork xs) -> showHappy " ∪ " xs
|
||||
DCore (FFork xs) -> showHappy " ∪ " xs
|
||||
DCoreAndCell k p -> showHappy " ∪ " (setFromList [DCore k, DCell p])
|
||||
|
||||
|
||||
-- Boolean algebras ------------------------------------------------------------
|
||||
|
||||
class BoolAlg a where
|
||||
top :: a
|
||||
bot :: a
|
||||
complement :: a -> a
|
||||
union :: a -> a -> a
|
||||
intersect :: a -> a -> a
|
||||
nest :: a -> a -> Bool
|
||||
|
||||
diff :: a -> a -> a
|
||||
diff x y = intersect x (complement y)
|
||||
|
||||
|
||||
-- Ur Elements -----------------------------------------------------------------
|
||||
|
||||
class Ord a => Ur a
|
||||
|
||||
instance Ur Nat
|
||||
instance (Ord t) => Ur (Core t)
|
||||
|
||||
|
||||
-- Happy BoolAlg ---------------------------------------------------------------
|
||||
|
||||
instance Ur a => BoolAlg (Happy a) where
|
||||
bot = Fork Set.empty
|
||||
top = Isnt Set.empty
|
||||
|
||||
complement (Fork x) = Isnt x
|
||||
complement (Isnt x) = Fork x
|
||||
|
||||
union (Fork x) (Fork y) = Fork (Set.union x y)
|
||||
union (Isnt x) (Isnt y) = Isnt (Set.intersection x y)
|
||||
union (Isnt x) (Fork y) = Isnt (Set.difference x y)
|
||||
union (Fork x) (Isnt y) = Isnt (Set.difference y x)
|
||||
|
||||
intersect (Fork x) (Fork y) = Fork (Set.intersection x y)
|
||||
intersect (Isnt x) (Isnt y) = Isnt (Set.union x y)
|
||||
intersect (Isnt x) (Fork y) = Fork (Set.difference y x)
|
||||
intersect (Fork x) (Isnt y) = Fork (Set.difference x y)
|
||||
|
||||
nest (Fork xs) (Fork ys) = xs `Set.isSubsetOf` ys
|
||||
nest (Isnt xs) (Isnt ys) = ys `Set.isSubsetOf` xs
|
||||
nest (Fork xs) (Isnt ys) = Set.null (ys `Set.intersection` xs)
|
||||
nest (Isnt xs) (Fork ys) = False
|
||||
|
||||
|
||||
-- (Fork Cell) BoolAlg ---------------------------------------------------------
|
||||
|
||||
instance (Ord t, BoolAlg t) => BoolAlg (Fork (Cell t)) where
|
||||
bot = FFork mempty
|
||||
top = Top
|
||||
|
||||
complement Top = bot
|
||||
complement (FFork cs) = FFork $ Set.fromList do
|
||||
(Cell x y) <- toList cs
|
||||
id [ Cell (complement x) y
|
||||
, Cell x (complement y)
|
||||
, Cell (complement x) (complement y)
|
||||
]
|
||||
|
||||
union Top _ = Top
|
||||
union _ Top = Top
|
||||
union (FFork xs) (FFork ys) = FFork (Set.union xs ys)
|
||||
|
||||
nest _ Top = True
|
||||
nest Top _ = False
|
||||
nest (FFork xs) (FFork ys) = all (\x -> any (cellNest x) ys) xs
|
||||
where
|
||||
cellNest (Cell x1 y1) (Cell x2 y2) = nest x1 x2 && nest y1 y2
|
||||
|
||||
intersect Top f = f
|
||||
intersect f Top = f
|
||||
intersect (FFork xs) (FFork ys) = FFork $ Set.fromList do
|
||||
(Cell x1 x2) <- toList xs
|
||||
(Cell y1 y2) <- toList ys
|
||||
let z1 = (intersect x1 y1)
|
||||
z2 = (intersect x2 y2)
|
||||
guard (z1 /= bot && z2 /= bot)
|
||||
pure (Cell z1 z2)
|
||||
|
||||
|
||||
-- Func BoolAlg ----------------------------------------------------------------
|
||||
|
||||
instance BoolAlg t => BoolAlg (Func t) where
|
||||
bot = Func top bot
|
||||
top = Func bot top
|
||||
|
||||
complement (Func x y) = Func (complement x) (complement y)
|
||||
|
||||
union (Func x1 y1) (Func x2 y2) = Func (intersect x1 x2) (union y1 y2)
|
||||
intersect (Func x1 y1) (Func x2 y2) = Func (union x1 x2) (union y1 y2)
|
||||
|
||||
nest (Func x1 y1) (Func x2 y2) = nest x2 x1 && nest y1 y2
|
||||
|
||||
-- Ty BoolAlg ------------------------------------------------------------------
|
||||
|
||||
instance BoolAlg Ty where
|
||||
bot = Ty mempty bot bot bot
|
||||
top = Ty mempty top top top
|
||||
|
||||
complement = \case
|
||||
Ty{tFace,tAtom,tCore,tCell} ->
|
||||
Ty { tFace = mempty
|
||||
, tAtom = complement tAtom
|
||||
, tCore = complement tCore
|
||||
, tCell = complement tCell
|
||||
}
|
||||
|
||||
union p q =
|
||||
Ty { tFace = tFace p `Set.intersection` tFace q
|
||||
, tAtom = tAtom p `union` tAtom q
|
||||
, tCore = tCore p `union` tCore q
|
||||
, tCell = tCell p `union` tCell q
|
||||
}
|
||||
|
||||
intersect p q =
|
||||
Ty { tFace = Set.union (tFace p) (tFace q)
|
||||
, tAtom = tAtom p `intersect` tAtom q
|
||||
, tCore = tCore p `intersect` tCore q
|
||||
, tCell = tCell p `intersect` tCell q
|
||||
}
|
||||
|
||||
nest p q =
|
||||
and [ nest (tAtom p) (tAtom q)
|
||||
, nest (tCell p) (tCell q)
|
||||
, nest (tCore p) (tCore q)
|
||||
]
|
||||
|
||||
diff p q =
|
||||
Ty { tFace = Set.union (tFace p) (tFace q)
|
||||
, tAtom = tAtom p `diff` tAtom q
|
||||
, tCore = tCore p `diff` tCore q
|
||||
, tCell = tCell p `diff` tCell q
|
||||
}
|
||||
|
||||
|
||||
-- Basic Types -----------------------------------------------------------------
|
||||
|
||||
tyAnyCell, tyAnyAtom, tyAnyCore :: Ty
|
||||
tyAnyAtom = bot { tAtom = top }
|
||||
tyAnyCell = bot { tCell = top }
|
||||
tyAnyCore = bot { tCore = top }
|
||||
|
||||
tyConst :: Nat -> Ty
|
||||
tyConst x = bot { tAtom = Fork (singleton x) }
|
||||
|
||||
tyCell :: Ty -> Ty -> Ty
|
||||
tyCell x y = bot { tCell = _Singleton # Cell x y }
|
||||
|
||||
tyCore :: Map Sym Ty -> Ty -> Ty
|
||||
tyCore arms ctx = bot { tCore = Fork (singleton (Core arms ctx)) }
|
||||
|
||||
tyNull, tyYes, tyNo, tyBool :: Ty
|
||||
tyNull = tyConst 0
|
||||
tyYes = tyConst 0
|
||||
tyNo = tyConst 1
|
||||
tyBool = tyYes `union` tyNo
|
||||
|
||||
addFace :: Sym -> Ty -> Ty
|
||||
addFace fc t = t { tFace = Set.insert fc (tFace t) }
|
||||
|
||||
|
||||
-- Lenses ----------------------------------------------------------------------
|
||||
|
||||
{-
|
||||
TODO The review case is not quite right. If we do
|
||||
`DAtom nullFork # _HappyFork`, we will get `tyNull`. So
|
||||
this law is broken:
|
||||
|
||||
Just f == (f # _HappyFork) ^? _HappyFork
|
||||
-}
|
||||
_Discrim :: Prism' Ty Discrim
|
||||
_Discrim = prism' mk get
|
||||
where
|
||||
mk = \case
|
||||
DAtom f -> bot { tAtom = _HappyFork # f }
|
||||
DCore f -> bot { tCore = _HappyFork # f }
|
||||
DCell f -> bot { tCell = f }
|
||||
|
||||
DCoreAndCell core cell ->
|
||||
bot { tCell = cell, tCore = _HappyFork # core }
|
||||
|
||||
get Ty{..} =
|
||||
(nullHappy tCore, nullFork tCell, nullHappy tAtom) & \case
|
||||
( False, True, True ) -> DCore <$> tCore ^? _HappyFork
|
||||
( True, False, True ) -> DCell <$> pure tCell
|
||||
( True, True, False ) -> DAtom <$> tAtom ^? _HappyFork
|
||||
( False, False, True ) -> DCoreAndCell <$> tCore ^? _HappyFork
|
||||
<*> pure tCell
|
||||
_ -> Nothing
|
||||
|
||||
makePrisms ''HoonDir
|
||||
makePrisms ''Discrim
|
||||
|
||||
_Cell :: Prism' Ty (Fork (Cell Ty))
|
||||
_Cell = _Discrim . _DCell
|
||||
|
||||
_Core :: Prism' Ty (Fork (Core Ty))
|
||||
_Core = _Discrim . _DCore
|
||||
|
||||
_Atom :: Prism' Ty (Fork Nat)
|
||||
_Atom = _Discrim . _DAtom
|
||||
|
||||
_CoreAndCell :: Prism' Ty (Fork (Core Ty), Fork (Cell Ty))
|
||||
_CoreAndCell = _Discrim . _DCoreAndCell
|
||||
|
||||
|
||||
-- Cast cores to cells. --------------------------------------------------------
|
||||
|
||||
castCoreToCell :: (BoolAlg t) => Core t -> Cell t
|
||||
castCoreToCell (Core _ c) = Cell top c
|
||||
|
||||
castTyToCell :: Ty -> Maybe Ty
|
||||
castTyToCell = fmap (review _Cell . cast) . preview _CoreAndCell
|
||||
where
|
||||
cast (cores, cells) = union cells (mapFork Top castCoreToCell cores)
|
||||
|
||||
|
||||
-- Testing: Generators ---------------------------------------------------------
|
||||
|
||||
-- prop_example :: Int -> Int -> Bool
|
||||
-- prop_example a b = a + b == b + a
|
||||
|
||||
-- tests :: TestTree
|
||||
-- tests = $(testGroupGenerator)
|
||||
|
||||
|
||||
perms :: forall a. Show a => [a] -> [[a]]
|
||||
perms as = do
|
||||
ii <- iis (length as)
|
||||
pure (foldr f [] (zip ii as))
|
||||
where
|
||||
f (True, x) xs = x:xs
|
||||
f (False, x) xs = xs
|
||||
|
||||
iis :: Int -> [[Bool]]
|
||||
iis 0 = pure [True, False]
|
||||
iis n = do
|
||||
x <- iis (n - 1)
|
||||
b <- [True, False]
|
||||
pure (b:x)
|
||||
|
||||
genFace :: Gen (Set Sym)
|
||||
genFace = do
|
||||
xs <- oneof (pure <$> perms ["p", "q"])
|
||||
pure (setFromList xs)
|
||||
|
||||
instance Arbitrary Ty where
|
||||
arbitrary = do
|
||||
getSize >>= \case
|
||||
0 -> oneof [pure top, pure bot]
|
||||
1 -> resize 0 (Ty <$> genFace <*> arbitrary <*> arbitrary <*> arbitrary)
|
||||
n -> Ty <$> genFace <*> arbitrary <*> arbitrary <*> resize 1 arbitrary
|
||||
|
||||
instance (Arbitrary t, Ord t) => Arbitrary (Happy (Core t)) where
|
||||
-- TODO
|
||||
arbitrary = oneof [ pure (Fork mempty), pure (Isnt mempty) ]
|
||||
|
||||
instance (Arbitrary t, Ord t) => Arbitrary (Fork t) where
|
||||
arbitrary = oneof [ pure Top, FFork <$> setFromList <$> listOf arbitrary ]
|
||||
|
||||
instance Arbitrary t => Arbitrary (Cell t) where
|
||||
arbitrary = Cell <$> arbitrary <*> arbitrary
|
||||
|
||||
instance Arbitrary (Happy Nat) where
|
||||
arbitrary = do
|
||||
xs <- oneof (pure <$> perms [0, 1])
|
||||
b <- arbitrary
|
||||
pure case b of
|
||||
True -> Fork (setFromList xs)
|
||||
False -> Isnt (setFromList xs)
|
||||
|
||||
instance Arbitrary t => Arbitrary (Func t) where
|
||||
arbitrary = Func <$> arbitrary <*> arbitrary
|
||||
|
||||
-- can we make this ==?
|
||||
equiv :: (BoolAlg a) => a -> a -> Bool
|
||||
equiv x y = nest x y && nest y x
|
||||
|
||||
nestRefl :: (Arbitrary a, BoolAlg a) => a -> Bool
|
||||
nestRefl x = nest x x
|
||||
|
||||
subGivesBot :: (Arbitrary a, Eq a, BoolAlg a) => a -> Bool
|
||||
subGivesBot x = bot == diff x x
|
||||
|
||||
nestTrans :: (Arbitrary a, BoolAlg a) => a -> a -> a -> Property
|
||||
nestTrans a b c = (nest a b && nest b c) ==> nest a c
|
||||
|
||||
nestUnion :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
nestUnion x y = nest x u && nest y u
|
||||
where u = x `union` y
|
||||
|
||||
nestIntersect :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
nestIntersect x y = nest u x && nest u y
|
||||
where u = x `intersect` y
|
||||
|
||||
unionId :: (Arbitrary a, BoolAlg a) => a -> Bool
|
||||
unionId x = union x bot `equiv` x
|
||||
|
||||
intersectId :: (Arbitrary a, BoolAlg a) => a -> Bool
|
||||
intersectId x = intersect x top `equiv` x
|
||||
|
||||
unionAbsorbs :: (Arbitrary a, BoolAlg a) => a -> Bool
|
||||
unionAbsorbs x = union x top `equiv` top
|
||||
|
||||
intersectAbsorbs :: (Arbitrary a, BoolAlg a) => a -> Bool
|
||||
intersectAbsorbs x = intersect x bot `equiv` bot
|
||||
|
||||
unionCommutes :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
unionCommutes x y = union x y `equiv` union y x
|
||||
|
||||
intersectCommutes :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
intersectCommutes x y = intersect x y `equiv` intersect y x
|
||||
|
||||
unionAssociates :: (Arbitrary a, BoolAlg a) => a -> a -> a -> Bool
|
||||
unionAssociates x y z = union x (union y z) `equiv` union (union x y) z
|
||||
|
||||
intersectAssociates :: (Arbitrary a, BoolAlg a) => a -> a -> a -> Bool
|
||||
intersectAssociates x y z = intersect x (intersect y z)
|
||||
`equiv` intersect (intersect x y) z
|
||||
|
||||
unionDistributes :: (Arbitrary a, BoolAlg a) => a -> a -> a -> Bool
|
||||
unionDistributes x y z = union x (intersect y z)
|
||||
`equiv` intersect (union x y) (union x z)
|
||||
|
||||
intersectDistributes :: (Arbitrary a, BoolAlg a) => a -> a -> a -> Bool
|
||||
intersectDistributes x y z = intersect x (union y z)
|
||||
`equiv` union (intersect x y) (intersect x z)
|
||||
|
||||
doubleCompl :: (Arbitrary a, BoolAlg a) => a -> Bool
|
||||
doubleCompl x = equiv x (complement (complement x))
|
||||
|
||||
complSub :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
complSub x y = diff x y `equiv` intersect x (complement y)
|
||||
|
||||
deMorganUnion :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
deMorganUnion x y = complement (union x y) `equiv` intersect (complement x) (complement y)
|
||||
|
||||
deMorganIntersect :: (Arbitrary a, BoolAlg a) => a -> a -> Bool
|
||||
deMorganIntersect x y = complement (intersect x y) `equiv` union (complement x) (complement y)
|
||||
|
||||
|
||||
prop_nestReflAtom = nestRefl @(Happy Nat)
|
||||
prop_nestTransAtom = nestTrans @(Happy Nat)
|
||||
prop_nestUnionAtom = nestUnion @(Happy Nat)
|
||||
prop_nestIntersectAtom = nestIntersect @(Happy Nat)
|
||||
prop_unionIdAtom = unionId @(Happy Nat)
|
||||
prop_intersectIdAtom = intersectId @(Happy Nat)
|
||||
prop_unionAbsorbsAtom = unionAbsorbs @(Happy Nat)
|
||||
prop_intersectAbsorbsAtom = intersectAbsorbs @(Happy Nat)
|
||||
prop_unionCommutesAtom = unionCommutes @(Happy Nat)
|
||||
prop_intersectCommutesAtom = intersectCommutes @(Happy Nat)
|
||||
prop_unionAssociatesAtom = unionAssociates @(Happy Nat)
|
||||
prop_intersectAssociatesAtom = intersectAssociates @(Happy Nat)
|
||||
prop_unionDistributesAtom = unionDistributes @(Happy Nat)
|
||||
prop_intersectDistributesAtom = intersectDistributes @(Happy Nat)
|
||||
prop_doubleComplAtom = doubleCompl @(Happy Nat)
|
||||
prop_complSubAtom = complSub @(Happy Nat)
|
||||
prop_deMorganUnionAtom = deMorganUnion @(Happy Nat)
|
||||
prop_deMorganIntersectAtom = deMorganIntersect @(Happy Nat)
|
||||
|
||||
prop_nestReflCore = nestRefl @(Happy (Core (Happy Nat)))
|
||||
prop_nestTransCore = nestTrans @(Happy (Core (Happy Nat)))
|
||||
prop_nestUnionCore = nestUnion @(Happy (Core (Happy Nat)))
|
||||
prop_nestIntersectCore = nestIntersect @(Happy (Core (Happy Nat)))
|
||||
prop_unionIdCore = unionId @(Happy (Core (Happy Nat)))
|
||||
prop_intersectIdCore = intersectId @(Happy (Core (Happy Nat)))
|
||||
prop_unionAbsorbsCore = unionAbsorbs @(Happy (Core (Happy Nat)))
|
||||
prop_intersectAbsorbsCore = intersectAbsorbs @(Happy (Core (Happy Nat)))
|
||||
prop_unionCommutesCore = unionCommutes @(Happy (Core (Happy Nat)))
|
||||
prop_intersectCommutesCore = intersectCommutes @(Happy (Core (Happy Nat)))
|
||||
prop_unionAssociatesCore = unionAssociates @(Happy (Core (Happy Nat)))
|
||||
prop_intersectAssociatesCore = intersectAssociates @(Happy (Core (Happy Nat)))
|
||||
prop_unionDistributesCore = unionDistributes @(Happy (Core (Happy Nat)))
|
||||
prop_intersectDistributesCore = intersectDistributes @(Happy (Core (Happy Nat)))
|
||||
prop_doubleComplCore = doubleCompl @(Happy (Core (Happy Nat)))
|
||||
prop_complSubCore = complSub @(Happy (Core (Happy Nat)))
|
||||
prop_deMorganUnionCore = deMorganUnion @(Happy (Core (Happy Nat)))
|
||||
prop_deMorganIntersectCore = deMorganIntersect @(Happy (Core (Happy Nat)))
|
||||
|
||||
prop_nestReflCell = nestRefl @(Fork (Cell (Happy Nat)))
|
||||
prop_nestTransCell = nestTrans @(Fork (Cell (Happy Nat)))
|
||||
prop_nestUnionCell = nestUnion @(Fork (Cell (Happy Nat)))
|
||||
prop_nestIntersectCell = nestIntersect @(Fork (Cell (Happy Nat)))
|
||||
prop_unionIdCell = unionId @(Fork (Cell (Happy Nat)))
|
||||
prop_intersectIdCell = intersectId @(Fork (Cell (Happy Nat)))
|
||||
prop_unionAbsorbsCell = unionAbsorbs @(Fork (Cell (Happy Nat)))
|
||||
prop_intersectAbsorbsCell = intersectAbsorbs @(Fork (Cell (Happy Nat)))
|
||||
prop_unionCommutesCell = unionCommutes @(Fork (Cell (Happy Nat)))
|
||||
prop_intersectCommutesCell = intersectCommutes @(Fork (Cell (Happy Nat)))
|
||||
prop_unionAssociatesCell = unionAssociates @(Fork (Cell (Happy Nat)))
|
||||
prop_intersectAssociatesCell = intersectAssociates @(Fork (Cell (Happy Nat)))
|
||||
prop_unionDistributesCell = unionDistributes @(Fork (Cell (Happy Nat)))
|
||||
prop_intersectDistributesCell = intersectDistributes @(Fork (Cell (Happy Nat)))
|
||||
prop_doubleComplCell = doubleCompl @(Fork (Cell (Happy Nat)))
|
||||
prop_complSubCell = complSub @(Fork (Cell (Happy Nat)))
|
||||
prop_deMorganUnionCell = deMorganUnion @(Fork (Cell (Happy Nat)))
|
||||
prop_deMorganIntersectCell = deMorganIntersect @(Fork (Cell (Happy Nat)))
|
||||
|
||||
prop_nestReflFunc = nestRefl @(Func (Happy Nat))
|
||||
prop_nestTransFunc = nestTrans @(Func (Happy Nat))
|
||||
prop_nestUnionFunc = nestUnion @(Func (Happy Nat))
|
||||
prop_nestIntersectFunc = nestIntersect @(Func (Happy Nat))
|
||||
prop_unionIdFunc = unionId @(Func (Happy Nat))
|
||||
prop_intersectIdFunc = intersectId @(Func (Happy Nat))
|
||||
prop_unionAbsorbsFunc = unionAbsorbs @(Func (Happy Nat))
|
||||
prop_intersectAbsorbsFunc = intersectAbsorbs @(Func (Happy Nat))
|
||||
prop_unionCommutesFunc = unionCommutes @(Func (Happy Nat))
|
||||
prop_intersectCommutesFunc = intersectCommutes @(Func (Happy Nat))
|
||||
prop_unionAssociatesFunc = unionAssociates @(Func (Happy Nat))
|
||||
prop_intersectAssociatesFunc = intersectAssociates @(Func (Happy Nat))
|
||||
prop_unionDistributesFunc = unionDistributes @(Func (Happy Nat))
|
||||
prop_intersectDistributesFunc = intersectDistributes @(Func (Happy Nat))
|
||||
prop_doubleComplFunc = doubleCompl @(Func (Happy Nat))
|
||||
prop_complSubFunc = complSub @(Func (Happy Nat))
|
||||
prop_deMorganUnionFunc = deMorganUnion @(Func (Happy Nat))
|
||||
prop_deMorganIntersectFunc = deMorganIntersect @(Func (Happy Nat))
|
||||
|
||||
prop_nestReflTy = nestRefl @Ty
|
||||
prop_nestTransTy = nestTrans @Ty
|
||||
prop_nestUnionTy = nestUnion @Ty
|
||||
prop_nestIntersectTy = nestIntersect @Ty
|
||||
prop_unionIdTy = unionId @Ty
|
||||
prop_intersectIdTy = intersectId @Ty
|
||||
prop_unionAbsorbsTy = unionAbsorbs @Ty
|
||||
prop_intersectAbsorbsTy = intersectAbsorbs @Ty
|
||||
prop_unionCommutesTy = unionCommutes @Ty
|
||||
prop_intersectCommutesTy = intersectCommutes @Ty
|
||||
prop_unionAssociatesTy = unionAssociates @Ty
|
||||
prop_intersectAssociatesTy = intersectAssociates @Ty
|
||||
prop_unionDistributesTy = unionDistributes @Ty
|
||||
prop_intersectDistributesTy = intersectDistributes @Ty
|
||||
prop_doubleComplTy = doubleCompl @Ty
|
||||
prop_complSubTy = complSub @Ty
|
||||
prop_deMorganUnionTy = deMorganUnion @Ty
|
||||
prop_deMorganIntersectTy = deMorganIntersect @Ty
|
||||
@ -1,206 +0,0 @@
|
||||
module Language.Hoon.IR.Wing where
|
||||
|
||||
import ClassyPrelude hiding (union)
|
||||
import Control.Lens hiding (union)
|
||||
import Language.Hoon.IR.Ty
|
||||
|
||||
import Control.Category ((>>>))
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Map as Map
|
||||
|
||||
import Data.Foldable (foldrM)
|
||||
|
||||
|
||||
-- Search Forks ----------------------------------------------------------------
|
||||
|
||||
{-
|
||||
Search all the branches of a fork, and merge the results.
|
||||
|
||||
If the fork is `Top`, return `top`, otherwise `search` all the branches
|
||||
of the fork and `merge` the results. This succeeds if all of the
|
||||
searches succeed and all of the merges succeed.
|
||||
-}
|
||||
searchFork :: Ord a
|
||||
=> Either String b
|
||||
-> (b -> b -> Either String b)
|
||||
-> (a -> Either String b)
|
||||
-> Fork a
|
||||
-> Either String b
|
||||
searchFork top merge search = \case
|
||||
Top -> top
|
||||
FFork alts -> do
|
||||
results <- traverse search (setToList alts)
|
||||
case results of
|
||||
[] -> Left "searchFork: no matches"
|
||||
r:rs -> foldrM merge r rs
|
||||
|
||||
|
||||
|
||||
-- Traversals ------------------------------------------------------------------
|
||||
|
||||
atDir :: HoonDir -> Traversal' Ty Ty
|
||||
atDir dd f t = dd & \case
|
||||
Dot -> f t
|
||||
Ctx -> walk _Core topCtx ctx
|
||||
Arm s c -> walk _Core (topArm s) (arm s)
|
||||
L -> walk _Cell topLeft left
|
||||
R -> walk _Cell topRight right
|
||||
where
|
||||
sing :: Ord a => a -> Fork a
|
||||
sing = review _Singleton
|
||||
|
||||
topRight = sing <$> right (Cell top top)
|
||||
topLeft = sing <$> left (Cell top top)
|
||||
topCtx = sing <$> ctx (Core mempty top)
|
||||
topArm s = sing <$> ctx (Core mempty top)
|
||||
|
||||
right (Cell l r) = Cell <$> pure l <*> f r
|
||||
left (Cell l r) = Cell <$> f l <*> pure r
|
||||
ctx (Core a c) = Core a <$> f c
|
||||
|
||||
arm s k@(Core a c) =
|
||||
Map.lookup s a & \case
|
||||
Nothing -> pure k
|
||||
Just at -> do at' <- f at
|
||||
pure (Core (Map.insert s at' a) c)
|
||||
|
||||
walk :: (Ord a, Applicative f)
|
||||
=> Prism' Ty (Fork a) -> f (Fork a) -> (a -> f a) -> f Ty
|
||||
walk p top get =
|
||||
(t ^? p) & \case
|
||||
Nothing -> pure t
|
||||
Just fk -> review p <$> traverseFork top get fk
|
||||
|
||||
atPath :: HoonPath -> Traversal' Ty Ty
|
||||
atPath [] f t = f t
|
||||
atPath (d:ds) f t = (atDir d . atPath ds) f t
|
||||
|
||||
getPath :: HoonPath -> Ty -> Either String Ty
|
||||
getPath d t = t ^.. atPath d & \case
|
||||
[] -> Left ("No values found at path " <> show d)
|
||||
(d:ds) -> pure (foldr union d ds)
|
||||
|
||||
|
||||
-- Name Resolution -------------------------------------------------------------
|
||||
|
||||
mbErr :: String -> Maybe a -> Either String a
|
||||
mbErr err = \case Nothing -> Left err
|
||||
Just a -> pure a
|
||||
|
||||
getName :: Sym -> Ty -> Either String (HoonPath, Ty)
|
||||
getName nm = fmap (over _1 reverse) . go []
|
||||
where
|
||||
go :: HoonPath -> Ty -> Either String (HoonPath, Ty)
|
||||
go acc t | member nm (tFace t) = pure (acc, t)
|
||||
go acc t =
|
||||
mbErr "getName: Can't discriminate type" (t ^? _Discrim) >>= \case
|
||||
DCore k -> searchFork top merge (goCore acc) k
|
||||
DCell p -> searchFork top merge (goCell acc) p
|
||||
DCoreAndCell _ _ -> Left "getName: Might be core or cell"
|
||||
DAtom _ -> Left "getName: Search ended at atom"
|
||||
|
||||
top :: Either String (HoonPath, Ty)
|
||||
top = Left "Trying to search through top type"
|
||||
|
||||
merge :: (HoonPath, Ty) -> (HoonPath, Ty) -> Either String (HoonPath, Ty)
|
||||
merge (i,x) (j,y) = do
|
||||
mbErr "face matches at differing locations" $ guard (i == j)
|
||||
pure (i, union x y)
|
||||
|
||||
goCore :: HoonPath -> Core Ty -> Either String (HoonPath, Ty)
|
||||
goCore acc c@(Core arms ctx) = isArm <|> inCtx
|
||||
where
|
||||
isArm = ((Arm nm c:acc),) <$>
|
||||
mbErr "no such arm" (Map.lookup nm arms)
|
||||
inCtx = go (Ctx:acc) ctx
|
||||
|
||||
goCell :: HoonPath -> Cell Ty -> Either String (HoonPath, Ty)
|
||||
goCell acc (Cell l r) = go (L:acc) l <|> go (R:acc) r
|
||||
|
||||
-- Simple Getters and Setters --------------------------------------------------
|
||||
|
||||
previewErr :: String -> Prism' a b -> a -> Either String b
|
||||
previewErr err p a = mbErr err (a ^? p)
|
||||
|
||||
getDir' :: HoonDir -> Ty -> Either String Ty
|
||||
getDir' = \case
|
||||
Dot -> pure
|
||||
L -> previewErr notCell _Cell >=>
|
||||
searchFork ptop merge (\(Cell l _) -> pure l)
|
||||
R -> previewErr notCell _Cell >=>
|
||||
searchFork ptop merge (\(Cell _ r) -> pure r)
|
||||
Ctx -> previewErr notCore _Core >=>
|
||||
searchFork ptop merge (\(Core _ c) -> pure c)
|
||||
Arm s c -> \t -> do c' <- mbErr "getDir': can't discern core type" $
|
||||
t ^? _Core . _Singleton
|
||||
mbErr "arm signature doesn't match core type" $
|
||||
guard (c == c')
|
||||
pure (_Core . _Singleton # c)
|
||||
where
|
||||
notCell = "Trying to use cell-indexing into non-cell value"
|
||||
notCore = "Trying to get context of non-core value"
|
||||
merge = \x y -> pure (union x y)
|
||||
ptop = pure top
|
||||
|
||||
getPath' :: HoonPath -> Ty -> Either String Ty
|
||||
getPath' [] t = pure t
|
||||
getPath' (d:ds) t = getDir' d t >>= getPath' ds
|
||||
|
||||
setDir' :: HoonDir -> Ty -> Ty -> Either String Ty
|
||||
setDir' dd newTy t = dd & \case
|
||||
Dot -> pure newTy
|
||||
Ctx -> Left "Can't edit context type"
|
||||
Arm s c -> Left "Can't edit arms"
|
||||
L -> review _Cell . mapFork topLeft setLeft <$> asCell
|
||||
R -> review _Cell . mapFork topRight setRight <$> asCell
|
||||
where
|
||||
asCell = mbErr "Can't get axis of non-cell value" (t ^? _Cell)
|
||||
topRight = _Singleton # Cell top newTy
|
||||
setRight (Cell l _) = Cell l newTy
|
||||
topLeft = _Singleton # Cell newTy top
|
||||
setLeft (Cell _ r) = Cell newTy r
|
||||
|
||||
|
||||
-- Get and Edit Wings ----------------------------------------------------------
|
||||
|
||||
getAxis :: TreePath -> Ty -> Either String (HoonPath, Ty)
|
||||
getAxis axis = fmap (path,) . getPath path
|
||||
where
|
||||
path = axis <&> \case { False -> L; True -> R }
|
||||
|
||||
getLimb :: Limb -> Ty -> Either String (HoonPath, Ty)
|
||||
getLimb (WAxis a) = getAxis a
|
||||
getLimb (WName n) = getName n
|
||||
getLimb WDot = \t -> pure ([Dot], t)
|
||||
|
||||
{-
|
||||
In Hoon, only the last arm name actually resolves to an arm,
|
||||
everything else just refers to the core of that arm. `muck` handles
|
||||
this transformation.
|
||||
-}
|
||||
resolve :: Wing -> Ty -> Either String (HoonPath, Ty)
|
||||
resolve (reverse -> ww) tt = over _1 muck <$> go ww tt
|
||||
where
|
||||
go [] t = pure ([], t)
|
||||
go (l:ls) t = do (p,t') <- getLimb l t
|
||||
over _1 (p <>) <$> go ls t'
|
||||
|
||||
muck = reverse . r . reverse
|
||||
where
|
||||
r [] = []
|
||||
r (d:ds) = d : filter (not . isWeird) ds
|
||||
isWeird (Arm _ _) = True
|
||||
isWeird Dot = True
|
||||
isWeird _ = False
|
||||
|
||||
edit :: Wing -> Ty -> Ty -> Either String (HoonPath, Ty)
|
||||
edit w newTy ty = do
|
||||
(path, oldTy) <- resolve w ty
|
||||
|
||||
guard (all (isn't _Arm) path)
|
||||
|
||||
result <- any (has _Ctx) path & \case
|
||||
True -> ty <$ guard (nest newTy oldTy)
|
||||
False -> pure (set (atPath path) newTy ty)
|
||||
|
||||
pure (path, result)
|
||||
@ -1,80 +0,0 @@
|
||||
module Language.Hoon.LL.Gen where
|
||||
|
||||
import ClassyPrelude hiding (union)
|
||||
import Data.Bits (shift, finiteBitSize, countLeadingZeros)
|
||||
|
||||
import Language.Hoon.IR.Ty (Sym, Nat)
|
||||
import Language.Hoon.LL.Types
|
||||
import Language.Hoon.Nock.Types
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Vector as Vector
|
||||
|
||||
axis :: LLPath -> Atom
|
||||
axis = go . reverse
|
||||
where
|
||||
go [] = 1
|
||||
go (L:ds) = 2 * go ds
|
||||
go (R:ds) = 2 * go ds + 1
|
||||
go (Ctx:ds) = 2 * go ds + 1
|
||||
|
||||
log2 :: Int -> Int
|
||||
log2 x = finiteBitSize x - 1 - countLeadingZeros x
|
||||
|
||||
-- | The greatest power of two less than the argument
|
||||
scale :: Int -> Int
|
||||
scale x = shift (log2 x) 1
|
||||
|
||||
layoutPath :: Nat -> Nat -> LLPath
|
||||
layoutPath 0 1 = []
|
||||
layoutPath _ 1 = error "axis-fell"
|
||||
layoutPath idx sz =
|
||||
let midpoint = sz `quot` 2
|
||||
in if idx <= midpoint
|
||||
then L : layoutPath idx midpoint
|
||||
else R : layoutPath (idx - midpoint) (sz - midpoint)
|
||||
|
||||
-- | The axis of an arm, as laid out in a battery
|
||||
coreAxis :: Sym -> (Map Sym t) -> Maybe Atom
|
||||
coreAxis a bat = do
|
||||
i <- Map.lookupIndex a bat
|
||||
let batPath = layoutPath i (Map.size bat)
|
||||
pure (axis (L : batPath))
|
||||
|
||||
layOut :: Vector Noun -> Noun
|
||||
layOut ns
|
||||
| null ns = Atom 0
|
||||
| length ns == 1 = Vector.head ns
|
||||
| otherwise = Cell (layOut as) (layOut bs)
|
||||
where (as, bs) = splitAt (length ns `quot` 2) ns
|
||||
|
||||
battery :: (Map Sym a) -> (a -> Maybe Noun) -> Maybe Noun
|
||||
battery bat conv = layOut <$> Vector.fromList <$> Map.elems <$> traverse conv bat
|
||||
|
||||
generate :: LLTy -> Maybe Nock
|
||||
generate = \case
|
||||
LWith _ x (LFire _ s bat) -> do
|
||||
ax <- coreAxis s bat
|
||||
x' <- generate x
|
||||
-- FIXME icky
|
||||
pure (NNineInvoke ax x')
|
||||
LWith _ x y -> NSevenThen <$> generate x <*> generate y
|
||||
LAxis _ a -> pure (NZeroAxis (axis a))
|
||||
LEdit _ a r x -> do
|
||||
r' <- generate r
|
||||
x' <- generate x
|
||||
pure (NTenEdit (axis a, r') x')
|
||||
LFire _ s bat -> do
|
||||
ax <- coreAxis s bat
|
||||
-- FIXME icky
|
||||
pure (NNineInvoke ax (NZeroAxis 1))
|
||||
LAtom _ n -> pure (NOneConst (Atom n))
|
||||
LPair _ x y -> NCons <$> generate x <*> generate y
|
||||
LCore _ arms -> do
|
||||
b <- battery arms (fmap nockToNoun . generate)
|
||||
pure (NCons (NOneConst b) (NZeroAxis 1))
|
||||
LSucc _ x -> NFourSucc <$> generate x
|
||||
LTest _ x y z -> NSixIf <$> generate x <*> generate y <*> generate z
|
||||
LCelQ _ x -> NThreeIsCell <$> generate x
|
||||
LEqlQ _ x y -> NFiveEq <$> generate x <*> generate y
|
||||
@ -1,108 +0,0 @@
|
||||
module Language.Hoon.LL.Run where
|
||||
|
||||
import ClassyPrelude hiding (succ, union, intersect)
|
||||
import Control.Lens
|
||||
import Control.Lens.TH
|
||||
import Control.Monad.Fix
|
||||
import Data.Void
|
||||
import Language.Hoon.IR.Ty (Ty, Nat, Sym, Hoon, HoonPath)
|
||||
import Language.Hoon.LL.Types
|
||||
|
||||
import Control.Category ((>>>))
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Language.Hoon.IR.Wing as Wing
|
||||
import qualified Prelude
|
||||
|
||||
|
||||
-- Types -----------------------------------------------------------------------
|
||||
|
||||
type Battery a = Map Sym (LL a)
|
||||
|
||||
data Val a
|
||||
= VAtom !Nat
|
||||
| VCell !(Val a) !(Val a)
|
||||
| VCore !(Battery a) !(Val a)
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
|
||||
-- Lenses ----------------------------------------------------------------------
|
||||
|
||||
makePrisms ''Val
|
||||
|
||||
_VBool :: Prism' (Val a) Bool
|
||||
_VBool = prism' mk get
|
||||
where
|
||||
mk True = VAtom 0
|
||||
mk False = VAtom 1
|
||||
|
||||
get (VAtom 1) = pure False
|
||||
get (VAtom 0) = pure True
|
||||
get _ = Nothing
|
||||
|
||||
|
||||
-- Value Manipulation ----------------------------------------------------------
|
||||
|
||||
succ :: Val a -> Either String (Val a)
|
||||
succ = fmap (review _VAtom . (+1)) . mbErr notAtom . preview _VAtom
|
||||
where notAtom = "Can't increment non-atom value."
|
||||
|
||||
isCell :: Val a -> Bool
|
||||
isCell = \case
|
||||
VAtom _ -> False
|
||||
VCell _ _ -> True
|
||||
VCore _ _ -> True -- bah
|
||||
|
||||
get :: LLPath -> Val a -> Either String (Val a)
|
||||
get = go
|
||||
where
|
||||
go [] val = pure val
|
||||
go (L:ds) (VCell l _) = go ds l
|
||||
go (R:ds) (VCell _ r) = go ds r
|
||||
go (Ctx:ds) (VCore _ c) = go ds c
|
||||
go _ _ = Left "Failed to lookup LLPath in value"
|
||||
|
||||
edit :: LLPath -> Val a -> Val a -> Either String (Val a)
|
||||
edit = go
|
||||
where
|
||||
go [] x v = pure x
|
||||
go (L:ds) x (VCell l r) = VCell <$> edit ds l x <*> pure r
|
||||
go (R:ds) x (VCell l r) = VCell <$> pure l <*> edit ds r x
|
||||
go (Ctx:ds) x (VCore arms ctx) = VCore <$> pure arms <*> edit ds ctx x
|
||||
go _ x _ = Left "LL.Run.edit: Bullshit edit"
|
||||
|
||||
|
||||
-- Interpreter -----------------------------------------------------------------
|
||||
|
||||
mbErr :: String -> Maybe a -> Either String a
|
||||
mbErr err = \case Nothing -> Left err
|
||||
Just a -> pure a
|
||||
|
||||
fire :: (Eq a, Show a) => Sym -> Val a -> Either String (Val a)
|
||||
fire nm = \case
|
||||
k@(VCore batt ctx) -> mbErr noArm (Map.lookup nm batt) >>= runLL k
|
||||
_ -> Left "Attempting to fire arm in non-core value"
|
||||
where
|
||||
noArm = unpack ("LL.Run.fire: Can't find arm " <> nm)
|
||||
|
||||
toBool :: Show a => Val a -> Either String Bool
|
||||
toBool v = mbErr notBool (v ^? _VBool)
|
||||
where
|
||||
notBool = "Expected a bool, but got " <> show v
|
||||
|
||||
runLL :: (Eq a, Show a) => Val a -> LL a -> Either String (Val a)
|
||||
runLL sut = r
|
||||
where
|
||||
r = \case
|
||||
LAxis _ p -> get p sut
|
||||
LFire _ a bat -> fire a sut -- TODO do we test whether bat is correct?
|
||||
LSucc _ h -> r h >>= succ
|
||||
LPair _ x y -> VCell <$> r x <*> r y
|
||||
LAtom _ n -> pure (VAtom n)
|
||||
LEdit _ w x y -> join (edit w <$> r x <*> r y)
|
||||
LWith _ x y -> r x >>= flip runLL y
|
||||
LCore _ b -> pure (VCore b sut)
|
||||
LTest _ v t f -> r v >>= toBool >>= bool (r t) (r f)
|
||||
LCelQ _ v -> review _VBool . isCell <$> r v
|
||||
LEqlQ _ x y -> review _VBool <$> ((==) <$> r x <*> r y)
|
||||
@ -1,73 +0,0 @@
|
||||
module Language.Hoon.LL.Types where
|
||||
|
||||
import ClassyPrelude hiding (union, intersect)
|
||||
import Language.Hoon.IR.Ty
|
||||
import Control.Lens
|
||||
import Control.Lens.TH
|
||||
import Control.Monad.Fix
|
||||
import Data.Void
|
||||
|
||||
import Control.Category ((>>>))
|
||||
import Data.Function ((&))
|
||||
import Data.Maybe (fromJust)
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Prelude
|
||||
|
||||
|
||||
-- Low-Level Representation ----------------------------------------------------
|
||||
|
||||
data LLDir = L | R | Ctx
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
type LLPath = [LLDir]
|
||||
|
||||
data LL t
|
||||
= LWith t (LL t) (LL t)
|
||||
| LAxis t LLPath
|
||||
| LEdit t LLPath (LL t) (LL t)
|
||||
| LFire t Sym (Map Sym t)
|
||||
| LAtom t Nat
|
||||
| LPair t (LL t) (LL t)
|
||||
| LCore t (Map Sym (LL t))
|
||||
| LSucc t (LL t)
|
||||
| LTest t (LL t) (LL t) (LL t)
|
||||
| LCelQ t (LL t)
|
||||
| LEqlQ t (LL t) (LL t)
|
||||
deriving (Eq, Ord, Show, Functor)
|
||||
|
||||
type LLTy = LL Ty
|
||||
|
||||
llYes, llNo :: LLTy
|
||||
llYes = LAtom tyBool 0
|
||||
llNo = LAtom tyBool 1
|
||||
|
||||
llTy :: Lens (LL a) (LL a) a a
|
||||
llTy = lens get set
|
||||
where
|
||||
get = \case
|
||||
LWith t _ _ -> t
|
||||
LAxis t _ -> t
|
||||
LEdit t _ _ _ -> t
|
||||
LFire t _ _ -> t
|
||||
LAtom t _ -> t
|
||||
LPair t _ _ -> t
|
||||
LCore t _ -> t
|
||||
LSucc t _ -> t
|
||||
LTest t _ _ _ -> t
|
||||
LCelQ t _ -> t
|
||||
LEqlQ t _ _ -> t
|
||||
|
||||
set ty t = ty & \case
|
||||
LWith _ x y -> LWith t x y
|
||||
LAxis _ x -> LAxis t x
|
||||
LEdit _ x y z -> LEdit t x y z
|
||||
LFire _ x bat -> LFire t x bat
|
||||
LAtom _ x -> LAtom t x
|
||||
LPair _ x y -> LPair t x y
|
||||
LCore _ x -> LCore t x
|
||||
LSucc _ x -> LSucc t x
|
||||
LTest _ x y z -> LTest t x y z
|
||||
LCelQ _ x -> LCelQ t x
|
||||
LEqlQ _ x y -> LEqlQ t x y
|
||||
@ -1,57 +0,0 @@
|
||||
module Language.Hoon.Nock.Types where
|
||||
|
||||
import ClassyPrelude
|
||||
|
||||
type Atom = Int
|
||||
|
||||
data Noun = Atom !Atom
|
||||
| Cell !Noun !Noun
|
||||
deriving (Eq, Ord, Read, Show)
|
||||
|
||||
yes, no :: Noun
|
||||
yes = Atom 0
|
||||
no = Atom 1
|
||||
|
||||
-- | Tree address
|
||||
type Axis = Atom
|
||||
|
||||
data Nock = NCons Nock Nock -- ^ autocons
|
||||
| NZeroAxis Axis -- ^ 0: tree addressing
|
||||
| NOneConst Noun
|
||||
| NTwoCompose Nock Nock
|
||||
| NThreeIsCell Nock
|
||||
| NFourSucc Nock
|
||||
| NFiveEq Nock Nock
|
||||
| NSixIf Nock Nock Nock
|
||||
| NSevenThen Nock Nock
|
||||
| NEightPush Nock Nock
|
||||
| NNineInvoke Axis Nock
|
||||
| NTenEdit (Axis, Nock) Nock
|
||||
| NElevenHint Hint Nock
|
||||
| NTwelveScry Nock Nock
|
||||
deriving (Eq, Ord, Read, Show)
|
||||
|
||||
data Hint = Tag Atom
|
||||
| Assoc Atom Nock
|
||||
deriving (Eq, Ord, Read, Show)
|
||||
|
||||
nockToNoun :: Nock -> Noun
|
||||
nockToNoun = go
|
||||
where
|
||||
go (NCons n m) = (Cell (go n) (go m))
|
||||
go (NZeroAxis a) = (Cell (Atom 0) (Atom a))
|
||||
go (NOneConst c) = (Cell (Atom 1) c)
|
||||
go (NTwoCompose n m) = (Cell (Atom 2) (Cell (go n) (go m)))
|
||||
go (NThreeIsCell n) = (Cell (Atom 3) (go n))
|
||||
go (NFourSucc n) = (Cell (Atom 4) (go n))
|
||||
go (NFiveEq n m) = (Cell (Atom 5) (Cell (go n) (go m)))
|
||||
go (NSixIf n m o) = (Cell (Atom 6) (Cell (go n) (Cell (go m) (go o))))
|
||||
go (NSevenThen n m) = (Cell (Atom 7) (Cell (go n) (go m)))
|
||||
go (NEightPush n m) = (Cell (Atom 8) (Cell (go n) (go m)))
|
||||
go (NNineInvoke a n) = (Cell (Atom 9) (Cell (Atom a) (go n)))
|
||||
go (NTenEdit (a, n) m) = (Cell (Atom 10) (Cell (Cell (Atom a) (go n)) (go m)))
|
||||
go (NElevenHint h n) = (Cell (Atom 11) (Cell (ho h) (go n)))
|
||||
go (NTwelveScry n m) = (Cell (Atom 12) (Cell (go n) (go m)))
|
||||
|
||||
ho (Tag x) = (Atom x)
|
||||
ho (Assoc x n) = (Cell (Atom x) (go n))
|
||||
@ -1,7 +0,0 @@
|
||||
module Language.Hoon.SpecToBunt (specToBunt) where
|
||||
|
||||
import Prelude
|
||||
import Language.Hoon.Types
|
||||
|
||||
specToBunt :: Bool -> Spec -> Hoon
|
||||
specToBunt = undefined
|
||||
@ -1,9 +0,0 @@
|
||||
module Language.Hoon.SpecToMold (specToMold) where
|
||||
|
||||
import Prelude
|
||||
import Language.Hoon.Types
|
||||
|
||||
-- | factory:ax. Given a spec and a boolean (?) produces a normalizing gate.
|
||||
specToMold :: Bool -> Spec -> Hoon
|
||||
specToMold fab spec = error "TODO specToMold"
|
||||
|
||||
@ -1,285 +0,0 @@
|
||||
module Language.Hoon.Types where
|
||||
|
||||
import Prelude
|
||||
|
||||
import Language.Hoon.Nock.Types
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
|
||||
import Data.Map (Map)
|
||||
import Data.Set (Set)
|
||||
import Data.List.NonEmpty (NonEmpty)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
hoonVersion :: Atom
|
||||
hoonVersion = 141
|
||||
|
||||
type Name = String -- "term"
|
||||
type Aura = Name
|
||||
type Tape = String
|
||||
type AtomUD = Atom
|
||||
|
||||
nameToAtom = error "TODO nameToAtom"
|
||||
|
||||
data Type = Void
|
||||
| Noun
|
||||
| Atomic Name (Maybe Atom)
|
||||
| Cell Type Type
|
||||
| Core Type -- TODO
|
||||
| Face Name Type -- TODO name or "tune"
|
||||
| Fork (Set Type)
|
||||
-- TODO %hint
|
||||
| Hold Type Hoon
|
||||
|
||||
data Polarity = Wet | Dry
|
||||
deriving (Eq, Ord, Read, Show)
|
||||
|
||||
data Variance = Invariant -- "gold"
|
||||
| Contravariant -- "iron"
|
||||
| Bivariant -- "lead"
|
||||
| Covariant -- "zinc"
|
||||
deriving (Eq, Ord, Read, Show)
|
||||
|
||||
type Claims = Map Name Spec
|
||||
|
||||
data Base
|
||||
= SVoid -- Empty Set
|
||||
| SNull -- ~
|
||||
| SFlag -- Bool
|
||||
| SNoun -- *
|
||||
| SCell -- ^
|
||||
| SAtom Aura
|
||||
|
||||
data Spec
|
||||
= SBase Base
|
||||
| SDebug Spot Spec
|
||||
| SLeaf Name Atom
|
||||
| Like (NonEmpty Wing)
|
||||
| Loop Name
|
||||
| Made (NonEmpty Name) Spec
|
||||
| Make Hoon [Spec]
|
||||
| Name Name Spec
|
||||
| Over Wing Spec
|
||||
--
|
||||
| BucGar Spec Spec -- ^ $> filter: require
|
||||
| BucBuc Spec Claims -- ^ $$ recursion
|
||||
| BucBar Spec Hoon -- ^ $$ recursion
|
||||
| BucCab Hoon -- $_
|
||||
| BucCol (NonEmpty Spec) -- $:
|
||||
| BucCen (NonEmpty Spec) -- $%, head pick
|
||||
| BucDot Spec Claims -- $., read-write core
|
||||
| BucLed Spec Spec -- $<, filter: exclude
|
||||
| BucHep Spec Spec -- $-, function core
|
||||
| BucKet Spec Spec -- $^, cons pick
|
||||
| BucLus Stud Spec -- $+, standard
|
||||
| BucFas Spec Claims -- $/, write-only core
|
||||
| BucMic Hoon -- $;, manual
|
||||
| BucPad Spec Hoon -- $&, repair
|
||||
| BucSig Hoon Spec -- $~, default
|
||||
| BucTic Spec Claims -- $`, read-only core
|
||||
| BucTis Skin Spec -- $=, name
|
||||
| BucPat Spec Spec -- $@, atom pick
|
||||
| BucWut (NonEmpty Spec) -- $?, full pick
|
||||
| BucZap Spec Claims -- $!, opaque core
|
||||
|
||||
type Bindings hoon = Map Name (Map Name (BindingHelp, hoon))
|
||||
data BindingHelp -- "what"
|
||||
data Tome
|
||||
|
||||
data Hoon
|
||||
= HAutocons [Hoon]
|
||||
| H_ Axis -- shorthand which should have been a function
|
||||
| HBase Base -- base type mold
|
||||
| Bust Base -- base type bunt
|
||||
| HDebug Spot Hoon
|
||||
| Error Tape
|
||||
| Hand Type Nock
|
||||
| Note Note Hoon
|
||||
| Fits Hoon Wing
|
||||
| Knit [Woof]
|
||||
| HLeaf Name Atom
|
||||
| Limb Name
|
||||
| Lost Hoon
|
||||
| Rock Name Noun
|
||||
| Sand Name Noun
|
||||
| Tell (NonEmpty Hoon)
|
||||
| Tune (Either Name Tune)
|
||||
| Wing Wing
|
||||
| Yell (NonEmpty Hoon)
|
||||
| Xray ManxHoot
|
||||
-- Cores
|
||||
| BarCab Spec Alas (Bindings Hoon)
|
||||
| BarCol Hoon Hoon
|
||||
| BarCen (Maybe Name) (Bindings Hoon)
|
||||
| BarDot Hoon
|
||||
| BarKet Hoon (Bindings Hoon)
|
||||
| BarHep Hoon
|
||||
| BarSig Spec Hoon
|
||||
| BarTar Spec Hoon
|
||||
| BarTis Spec Hoon
|
||||
| BarPat (Maybe Name) (Bindings Hoon)
|
||||
| BarWut Hoon
|
||||
-- Tuples
|
||||
| ColCab Hoon Hoon
|
||||
| ColKet Hoon Hoon Hoon Hoon
|
||||
| ColHep Hoon Hoon
|
||||
| ColLus Hoon Hoon Hoon
|
||||
| ColSig [Hoon]
|
||||
| ColTar (NonEmpty Hoon) -- was ordinary list
|
||||
-- Invocations
|
||||
| CenCab Wing [(Wing, Hoon)]
|
||||
| CenDot Hoon Hoon
|
||||
| CenHep Hoon Hoon
|
||||
| CenCol Hoon [Hoon]
|
||||
| CenTar Wing Hoon [(Wing, Hoon)]
|
||||
| CenKet Hoon Hoon Hoon Hoon
|
||||
| CenLus Hoon Hoon Hoon
|
||||
| CenSig Wing Hoon [Hoon]
|
||||
| CenTis Wing [(Wing, Hoon)]
|
||||
-- Nock
|
||||
| DotKet Spec Hoon
|
||||
| DotLus Hoon
|
||||
| DotTar Hoon Hoon
|
||||
| DotTis Hoon Hoon
|
||||
| DotWut Hoon
|
||||
-- Type conversions
|
||||
| KetBar Hoon
|
||||
| KetCen Hoon
|
||||
| KetDot Hoon Hoon
|
||||
| KetLus Hoon Hoon
|
||||
| KetHep Spec Hoon
|
||||
| KetPam Hoon
|
||||
| KetSig Hoon
|
||||
| KetTis Skin Hoon
|
||||
| KetWut Hoon
|
||||
| KetTar Spec
|
||||
| KetCol Spec
|
||||
-- Hints
|
||||
| SigBar Hoon Hoon
|
||||
| SigCab Hoon Hoon
|
||||
| SigCen Chum Hoon Tyre Hoon
|
||||
| SigFas Chum Hoon
|
||||
| SigLed Name (Maybe Hoon) Hoon
|
||||
| SigGar Name (Maybe Hoon) Hoon
|
||||
| SigBuc Name Hoon
|
||||
| SigLus Atom Hoon
|
||||
| SigPam AtomUD Hoon Hoon
|
||||
| SigTis Hoon Hoon
|
||||
| SigWut AtomUD Hoon Hoon Hoon
|
||||
| SigZap Hoon Hoon
|
||||
-- Miscellaneous
|
||||
| MicTis MarlHoot
|
||||
| MicCol Hoon [Hoon]
|
||||
| MicNet Hoon
|
||||
| MicSig Hoon [Hoon]
|
||||
| MicMic Hoon Hoon
|
||||
-- Compositions
|
||||
| TisBar Spec Hoon
|
||||
| TisCol [(Wing, Hoon)] Hoon
|
||||
| TisFas Skin Hoon Hoon
|
||||
| TisMic Skin Hoon Hoon
|
||||
| TisDot Wing Hoon Hoon
|
||||
| TisWut Wing Hoon Hoon Hoon
|
||||
| TisLed Hoon Hoon
|
||||
| TisHep Hoon Hoon
|
||||
| TisGar Hoon Hoon
|
||||
| TisKet Skin Wing Hoon Hoon
|
||||
| TisLus Hoon Hoon
|
||||
| TisSig [Hoon]
|
||||
| TisTar Name (Maybe Spec) Hoon Hoon
|
||||
| TisCom Hoon Hoon
|
||||
-- Conditionals
|
||||
| WutBar [Hoon]
|
||||
| WutHep Wing [(Spec,Hoon)]
|
||||
| WutCol Hoon Hoon Hoon
|
||||
| WutDot Hoon Hoon Hoon
|
||||
| WutKet Wing Hoon Hoon
|
||||
| WutLed Hoon Hoon
|
||||
| WutGar Hoon Hoon
|
||||
| WutLus Wing Hoon [(Spec, Hoon)]
|
||||
| WutPam [Hoon]
|
||||
| WutPat Wing Hoon Hoon
|
||||
| WutSig Wing Hoon Hoon
|
||||
| WutHax Skin Wing
|
||||
| WutTis Spec Wing
|
||||
| WutZap Hoon
|
||||
-- Special
|
||||
| ZapCom Hoon Hoon
|
||||
| ZapGar Hoon
|
||||
| ZapMic Hoon Hoon
|
||||
| ZapTis Hoon
|
||||
| ZapPat [Wing] Hoon Hoon
|
||||
| ZapWut (Either Atom (Atom, Atom)) Hoon
|
||||
| ZapZap
|
||||
|
||||
type Wing = [Limb]
|
||||
data Limb
|
||||
= NameLimb Name
|
||||
| AxisLimb Axis -- ^ %& tag
|
||||
| ByNameLimb Atom (Maybe Name) -- ^ ??? %| tag
|
||||
|
||||
data Tune
|
||||
= Tone
|
||||
{ aliases :: (Map Name (Maybe Hoon))
|
||||
, bridges :: [Hoon]
|
||||
}
|
||||
|
||||
-- TODO
|
||||
data Alas
|
||||
data Spot
|
||||
data Woof
|
||||
data ManxHoot
|
||||
data MarlHoot
|
||||
data Note
|
||||
data Chum
|
||||
data Tyre
|
||||
data Stud
|
||||
data Skin
|
||||
|
||||
-- | Basic hoon: totally desugared
|
||||
data BHoon
|
||||
= BAutocons [BHoon]
|
||||
| BDebug Spot BHoon
|
||||
| BHand Type Nock
|
||||
| BNote Note BHoon
|
||||
| BFits BHoon Wing
|
||||
| BSand Name Noun
|
||||
| BRock Name Noun
|
||||
| BTune (Either Name Tune)
|
||||
| BLost BHoon
|
||||
--
|
||||
| BBarCen (Maybe Name) (Bindings BHoon)
|
||||
| BBarPat (Maybe Name) (Bindings BHoon)
|
||||
--
|
||||
| BCenTis Wing [(Wing, BHoon)]
|
||||
--
|
||||
| BDotKet Spec BHoon
|
||||
| BDotLus BHoon
|
||||
| BDotTar BHoon BHoon
|
||||
| BDotTis BHoon BHoon
|
||||
| BDotWut BHoon
|
||||
--
|
||||
| BKetBar BHoon
|
||||
| BKetCen BHoon
|
||||
| BKetLus BHoon BHoon
|
||||
| BKetPam BHoon
|
||||
| BKetSig BHoon
|
||||
| BKetWut BHoon
|
||||
--
|
||||
| BSigGar Name (Maybe BHoon) BHoon
|
||||
| BSigZap BHoon BHoon
|
||||
--
|
||||
| BTisGar BHoon BHoon
|
||||
| BTisCom BHoon BHoon
|
||||
--
|
||||
| BWutCol BHoon BHoon BHoon
|
||||
| BWutHax Skin Wing
|
||||
--
|
||||
| BZapCom BHoon BHoon
|
||||
| BZapMic BHoon BHoon
|
||||
| BZapTis BHoon
|
||||
| BZapPat [Wing] BHoon BHoon
|
||||
| BZapZap
|
||||
|
||||
@ -1,80 +0,0 @@
|
||||
name: language-hoon
|
||||
version: 0.1.0
|
||||
license: AGPL-3.0-only
|
||||
|
||||
library:
|
||||
source-dirs: lib
|
||||
ghc-options:
|
||||
- -fwarn-incomplete-patterns
|
||||
- -O2
|
||||
|
||||
dependencies:
|
||||
- async
|
||||
- base
|
||||
- case-insensitive
|
||||
- chunked-data
|
||||
- classy-prelude
|
||||
- containers
|
||||
- data-fix
|
||||
- extra
|
||||
- flat
|
||||
- ghc-prim
|
||||
- http-client
|
||||
- http-types
|
||||
- integer-gmp
|
||||
- largeword
|
||||
- lens
|
||||
- megaparsec
|
||||
- mtl
|
||||
- multimap
|
||||
- para
|
||||
- pretty-show
|
||||
- QuickCheck
|
||||
- semigroups
|
||||
- smallcheck
|
||||
- stm
|
||||
- stm-chans
|
||||
- tasty
|
||||
- tasty-quickcheck
|
||||
- tasty-th
|
||||
- text
|
||||
- these
|
||||
- time
|
||||
- transformers
|
||||
- unordered-containers
|
||||
- vector
|
||||
|
||||
default-extensions:
|
||||
- ApplicativeDo
|
||||
- BangPatterns
|
||||
- BlockArguments
|
||||
- DeriveAnyClass
|
||||
- DeriveDataTypeable
|
||||
- DeriveFoldable
|
||||
- DeriveGeneric
|
||||
- DeriveTraversable
|
||||
- DerivingStrategies
|
||||
- EmptyDataDecls
|
||||
- FlexibleContexts
|
||||
- FlexibleInstances
|
||||
- FunctionalDependencies
|
||||
- GADTs
|
||||
- GeneralizedNewtypeDeriving
|
||||
- LambdaCase
|
||||
- MultiParamTypeClasses
|
||||
- NamedFieldPuns
|
||||
- NoImplicitPrelude
|
||||
- NumericUnderscores
|
||||
- OverloadedStrings
|
||||
- PartialTypeSignatures
|
||||
- QuasiQuotes
|
||||
- Rank2Types
|
||||
- RankNTypes
|
||||
- RecordWildCards
|
||||
- ScopedTypeVariables
|
||||
- TemplateHaskell
|
||||
- TupleSections
|
||||
- TypeApplications
|
||||
- TypeFamilies
|
||||
- UnicodeSyntax
|
||||
- ViewPatterns
|
||||
@ -3,8 +3,6 @@ resolver: lts-13.10
|
||||
packages:
|
||||
- pkg/hs-urbit
|
||||
- pkg/hs-vere
|
||||
- pkg/hs-hoon
|
||||
- pkg/hs-conq
|
||||
|
||||
extra-deps:
|
||||
- para-1.1@sha256:a90eebb063ad70271e6e2a7f00a93e8e8f8b77273f100f39852fbf8301926f81
|
||||
|
||||
Loading…
Reference in New Issue
Block a user