From 1408d2bcd76e3fe6c0c851575022c383ce548e71 Mon Sep 17 00:00:00 2001 From: Benjamin Summers Date: Tue, 16 Jul 2019 22:38:35 -0700 Subject: [PATCH] Moved language stuff to another branch. --- pkg/hs-conq/.gitignore | 2 - pkg/hs-conq/lib/Language/Conq.hs | 1258 --------------- pkg/hs-conq/lib/Language/Conq/Axe.hs | 138 -- pkg/hs-conq/lib/Language/Conq/Exp.hs | 130 -- pkg/hs-conq/lib/Language/Conq/ForVal.hs | 32 - pkg/hs-conq/lib/Language/Conq/Grainary.hs | 180 --- pkg/hs-conq/lib/Language/Conq/Mess.hs | 1356 ----------------- pkg/hs-conq/lib/Language/Conq/Types.hs | 157 -- pkg/hs-conq/package.yaml | 84 - pkg/hs-hoon/.gitignore | 2 - pkg/hs-hoon/lib/Language/Attila/AST/Parser.hs | 345 ----- pkg/hs-hoon/lib/Language/Attila/AST/Types.hs | 66 - pkg/hs-hoon/lib/Language/Attila/IR.hs | 359 ----- pkg/hs-hoon/lib/Language/Hoon/AST/Parser.hs | 345 ----- pkg/hs-hoon/lib/Language/Hoon/AST/Types.hs | 66 - pkg/hs-hoon/lib/Language/Hoon/Desugar.hs | 187 --- pkg/hs-hoon/lib/Language/Hoon/IR/Desugar.hs | 183 --- pkg/hs-hoon/lib/Language/Hoon/IR/Infer.hs | 213 --- pkg/hs-hoon/lib/Language/Hoon/IR/Ty.hs | 660 -------- pkg/hs-hoon/lib/Language/Hoon/IR/Wing.hs | 206 --- pkg/hs-hoon/lib/Language/Hoon/LL/Gen.hs | 80 - pkg/hs-hoon/lib/Language/Hoon/LL/Run.hs | 108 -- pkg/hs-hoon/lib/Language/Hoon/LL/Types.hs | 73 - pkg/hs-hoon/lib/Language/Hoon/Nock/Types.hs | 57 - pkg/hs-hoon/lib/Language/Hoon/SpecToBunt.hs | 7 - pkg/hs-hoon/lib/Language/Hoon/SpecToMold.hs | 9 - pkg/hs-hoon/lib/Language/Hoon/Types.hs | 285 ---- pkg/hs-hoon/package.yaml | 80 - stack.yaml | 2 - 29 files changed, 6670 deletions(-) delete mode 100644 pkg/hs-conq/.gitignore delete mode 100644 pkg/hs-conq/lib/Language/Conq.hs delete mode 100644 pkg/hs-conq/lib/Language/Conq/Axe.hs delete mode 100644 pkg/hs-conq/lib/Language/Conq/Exp.hs delete mode 100644 pkg/hs-conq/lib/Language/Conq/ForVal.hs delete mode 100644 pkg/hs-conq/lib/Language/Conq/Grainary.hs delete mode 100644 pkg/hs-conq/lib/Language/Conq/Mess.hs delete mode 100644 pkg/hs-conq/lib/Language/Conq/Types.hs delete mode 100644 pkg/hs-conq/package.yaml delete mode 100644 pkg/hs-hoon/.gitignore delete mode 100644 pkg/hs-hoon/lib/Language/Attila/AST/Parser.hs delete mode 100644 pkg/hs-hoon/lib/Language/Attila/AST/Types.hs delete mode 100644 pkg/hs-hoon/lib/Language/Attila/IR.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/AST/Parser.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/AST/Types.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/Desugar.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/IR/Desugar.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/IR/Infer.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/IR/Ty.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/IR/Wing.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/LL/Gen.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/LL/Run.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/LL/Types.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/Nock/Types.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/SpecToBunt.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/SpecToMold.hs delete mode 100644 pkg/hs-hoon/lib/Language/Hoon/Types.hs delete mode 100644 pkg/hs-hoon/package.yaml diff --git a/pkg/hs-conq/.gitignore b/pkg/hs-conq/.gitignore deleted file mode 100644 index c99ca9e136..0000000000 --- a/pkg/hs-conq/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -.stack-work -*.cabal diff --git a/pkg/hs-conq/lib/Language/Conq.hs b/pkg/hs-conq/lib/Language/Conq.hs deleted file mode 100644 index 186346e58b..0000000000 --- a/pkg/hs-conq/lib/Language/Conq.hs +++ /dev/null @@ -1,1258 +0,0 @@ -module Language.Conq 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.Bits -import Data.Vector (generate) -import Data.Monoid.Unicode ((∅)) - -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 - --------------------------------------------------------------------------------- - -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) - -data Val - = VV -- Void - | VN -- Null - | V0 !Val -- Left - | V1 !Val -- Right - | VP !Val !Val -- Pair - | VT !Val !Exp Val - | VR !SHA256 - deriving (Eq, Ord, Generic, Flat) - -instance Show Val where - show = show . valExp - -crash :: Exp -crash = EEval <> EEval <> ENull - -grainery :: IORef (HashMap SHA256 ByteString) -grainery = unsafePerformIO (newIORef grainsFromJets) - -grainsFromJets :: HashMap SHA256 ByteString -grainsFromJets = do - mapFromList $ jetReg <&> \(h,e,_) -> (h, flat (forVal e)) - -jetReg :: [(SHA256, Exp, Val -> Val)] -jetReg = - [ ( SHA256 (encodeBase58 "FWz5mTGmuVz2b4TLNa7yMjTKL7wihsEWakoUD2nzqP6q") - , ESubj - , id - ) - ] - -jets :: HashMap SHA256 (Val -> Val) -jets = mapFromList (jetReg <&> \(h,_,f) -> (h,f)) - -runTent :: SHA256 -> Exp -> Val -> Val -runTent k exp arg = - lookup k jets & \case - Nothing -> runExp arg exp - Just fn -> trace ("running jet " <> show (ETent k)) (fn arg) - -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 - -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) - -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 - -valExp :: Val -> Exp -valExp VN = ENull -valExp VV = crash -valExp v = go v <> ENull - where - go = \case - 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 _ _ v → go v - VR k → EHash <> go (getGrain k) - -hashVal :: Val -> (ByteString, SHA256) -hashVal x = (bs, SHA256 (SHA256.hash bs)) - where bs = flat x - -data TyExp - = TENil - | TESum TyExp TyExp - | TETup TyExp TyExp - | TEFor TyExp TyExp - | TEAll TyExp - | TEFix TyExp - | TERef Int - deriving (Eq, Ord, Generic, Flat) - -instance Show TyExp where - show = \case - TESum TENil TENil -> "?" - TENil -> "~" - TESum x y -> "<" <> show x <> " " <> show y <> ">" - TETup x y -> "[" <> show x <> " " <> show y <> "]" - TEFor x y -> "(" <> show x <> " " <> show y <> ")" - TEAll x -> "A" <> show x - TEFix x -> "F" <> show x - TERef x -> show x - -data Ty - = TNil - | TSum Ty Ty - | TTup Ty Ty - | TFor Ty Ty - | TVar Int - deriving (Eq, Ord) - -tBit :: TyExp -tBit = TESum TENil TENil - -tBitOp :: TyExp -tBitOp = TEFor tBit tBit - -instance Show Ty where - show = \case - TNil -> "~" - TSum x y -> "<" <> show x <> " " <> show y <> ">" - TTup x y -> "[" <> show x <> " " <> show y <> "]" - TFor x y -> "(" <> show x <> " => " <> show y <> ")" - TVar x -> show x - -tyExpTy :: TyExp -> Infer Ty -tyExpTy = go [] - where - go :: [Int] -> TyExp -> Infer Ty - go t = \case - TENil -> pure TNil - TESum x y -> TSum <$> go t x <*> go t y - TETup x y -> TTup <$> go t x <*> go t y - TEFor x y -> TFor <$> go t x <*> go t y - TEAll x -> do t' <- (:t) <$> mkTVar - go t' x - TEFix x -> do t' <- (:t) <$> mkTVar - go t' x - TERef i -> pure $ TVar (t P.!! i) - -declare :: Ty -> TyExp -> Infer Ty -declare t e = do - te <- tyExpTy e - unify t te - -checkType :: Exp -> Either Text Ty -checkType e = runInfer (infer e >>= finalize) - -type Unique = Int -type Infer a = ExceptT Text (State (Map Int Ty, Unique)) a -type Unify a = Maybe a - -mkTVar :: Infer Int -mkTVar = do - (env, n) <- get - put (env, n+1) - pure n - -forAll :: Infer Ty -forAll = TVar <$> mkTVar - -varIs :: Int -> Ty -> Infer Ty -varIs v (TVar x) | x==v = do - pure (TVar x) -varIs v t = do - (env, n) <- get - put (insertMap v t env, n) - pure t - -finalize :: Ty -> Infer Ty -finalize (TVar v) = resolve v >>= finalize' -finalize t = finalize' t - -finalize' :: Ty -> Infer Ty -finalize' = \case - TNil -> pure TNil - TVar x -> pure (TVar x) - TSum x y -> TSum <$> finalize x <*> finalize y - TTup x y -> TTup <$> finalize x <*> finalize y - TFor x y -> TFor <$> finalize x <*> finalize y - -unify :: Ty -> Ty -> Infer Ty -unify x y = do - -- traceM $ "UNIFY " <> show x <> " " <> show y - x <- case x of { TVar v -> resolve v; x -> pure x } - y <- case y of { TVar v -> resolve v; y -> pure y } - unify' x y - -unify' :: Ty -> Ty -> Infer Ty -unify' = curry \case - ( TNil, TNil ) → pure TNil - ( TSum a1 b1, TSum a2 b2 ) → TSum <$> unify a1 a2 <*> unify b1 b2 - ( TTup a1 b1, TTup a2 b2 ) → TTup <$> unify a1 a2 <*> unify b1 b2 - ( TFor a1 b1, TFor a2 b2 ) → TFor <$> unify a1 a2 <*> unify b1 b2 - ( ty, TVar x ) → varIs x ty - ( TVar x, ty ) → varIs x ty - ( x, y ) → throwE - $ "Bad unify: " <> tshow x <> " " <> tshow y - -resolve :: Int -> Infer Ty -resolve v = do - (env, _) <- get - lookup v env & \case - Nothing -> pure (TVar v) - Just (TVar x) -> resolve x - Just x -> pure x - -expectFor :: Ty -> Infer (Ty, Ty, Ty) -expectFor = \case - ty@(TFor x y) -> pure (ty, x, y) - t -> throwE ("Not a formula: " <> tshow t) - -runInfer :: Infer a -> Either Text a -runInfer = flip evalState ((∅), 0) . runExceptT - -infer :: Exp -> Infer Ty -infer = \case - ENull -> do - a <- forAll - pure (TFor a TNil) - - ESubj -> do - a <- forAll - pure (TFor a a) - - ELeft -> do - (a, b) <- (,) <$> forAll <*> forAll - pure (TFor a (TSum a b)) - - EWrit -> do - (a, b) <- (,) <$> forAll <*> forAll - pure (TFor b (TSum a b)) - - EHead -> do - (a, b) <- (,) <$> forAll <*> forAll - pure $ TFor (TTup a b) a - - ETail -> do - (a, b) <- (,) <$> forAll <*> forAll - pure $ TFor (TTup a b) b - - EDist -> do - (a, b, c) <- (,,) <$> forAll <*> forAll <*> forAll - pure $ TFor (TTup (TSum a b) c) (TSum (TTup a c) (TTup b c)) - - EEval -> do - (a, b) <- (,) <$> forAll <*> forAll - pure $ TFor (TTup a (TFor a b)) b - - EWith x y -> do - (xt, xi, xo) <- infer x >>= expectFor - (yt, yi, yo) <- infer y >>= expectFor - unify xo yi - pure (TFor xi yo) - - ECons x y -> do - (xt, xi, xo) <- infer x >>= expectFor - (yt, yi, yo) <- infer y >>= expectFor - unify xi yi - pure (TFor xi (TTup xo yo)) - - ECase p q -> do - (pt, pi, po) <- infer p >>= expectFor - (qt, qi, qo) <- infer q >>= expectFor - unify po qo - pure (TFor (TSum pi qi) po) - - EType t -> do - tt <- tyExpTy t - pure (TFor tt tt) - - EPush -> throwE "infer: EPush" -- TODO - EPull -> throwE "infer: EPull" -- TODO - EHash -> throwE "infer: EHash" -- TODO - EFall -> throwE "infer: EFall" -- TODO - ETent _ -> throwE "infer: ETent" -- TODO - -data Exp - = ESubj - | ENull - | EEval - | ELeft - | EWrit - | EHead - | ETail - | EDist - | EWith Exp Exp - | ECons Exp Exp - | ECase Exp Exp - | EType TyExp - | ETent SHA256 - | EPush - | EPull - | EHash - | EFall - deriving (Eq, Ord, Generic, Flat) - -instance Semigroup Exp where - ENull <> ESubj = ENull - x <> ESubj = x - ESubj <> y = y - x <> y = EWith y x - -instance Monoid Exp where - mempty = ESubj - -runExp :: Val -> Exp -> Val -runExp s ESubj = s -runExp s e = uncurry runExp (step s e) - --- Get a formula from a Val ---------------------------------------------------- - -{- - for = - opk = < < > - opk-alt = >> - dir = - get = <- +> - sim = <~ .> - otr = - plx = <◆ ●> - hin = < <@ <^ |>>> --} - -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 - ENull -> V1 $ V0 $ V0 $ V0 VN - ESubj -> V1 $ V0 $ V0 $ V1 VN - EPush -> V1 $ V0 $ V1 $ V0 $ V0 VN - EPull -> V1 $ V0 $ V1 $ V0 $ V1 VN - EHash -> V1 $ V0 $ V1 $ V1 $ V0 VN - EFall -> V1 $ V0 $ V1 $ V1 $ V1 VN - ETent ref -> VR ref - 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 - - -valFor :: Val -> Exp -valFor (V0 l) = valOpk l -valFor (VR r) = ETent r -valFor (V1 (VP x y)) = EWith (valOpk x) (valFor y) -valFor _ = ENull - -valOpk :: Val -> 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 _ = ENull - -valDir :: Val -> Exp -valDir (V0 VN) = ELeft -valDir (V1 VN) = EWrit -valDir _ = ENull - -valGet :: Val -> Exp -valGet (V0 VN) = EHead -valGet (V1 VN) = ETail -valGet _ = ENull - -valSim :: Val -> Exp -valSim (V0 VN) = ENull -valSim (V1 VN) = ESubj -valSim _ = ENull - -valOtr :: Val -> Exp -valOtr (V0 VN) = EEval -valOtr (V1 VN) = EDist -valOtr _ = ENull - -valPlx :: Val -> Exp -valPlx (V0 (VP x y)) = ECase (valFor x) (valFor y) -valPlx (V1 (VP x y)) = ECons (valFor x) (valFor y) -valPlx _ = ENull - -valHin :: Val -> Exp -valHin = \case - V0 (V0 VN) -> EPush - V0 (V1 VN) -> EPull - V1 (V0 VN) -> EHash - V1 (V1 VN) -> EFall - _ -> crash - --------------------------------------------------------------------------------- - --- tag :: Bool -> Val -> Val --- tag False = V0 --- tag True = V1 - --- unTag :: Val -> (Bool, Val) --- unTag (V0 x) = (False, x) --- unTag (V1 x) = (True, x) --- unTag _ = error "unTag" - --- toBits :: (Bits b, FiniteBits b) => b -> Vector Bool --- toBits b = --- generate (finiteBitSize b) (testBit b) - --- byteVal :: Word8 -> Val --- byteVal b = --- foldl' (flip tag) VN (toBits b) - --- valByte :: Val -> Word8 --- valByte v = runIdentity $ do --- (a, v) <- pure $ unTag v --- (b, v) <- pure $ unTag v --- (c, v) <- pure $ unTag v --- (d, v) <- pure $ unTag v --- (e, v) <- pure $ unTag v --- (f, v) <- pure $ unTag v --- (g, v) <- pure $ unTag v --- (h, v) <- pure $ unTag v --- let bits = [a, b, c, d, e, f, g, h] --- unless (VN == v) (error "valByte: bad byte") --- pure $ foldl' (\acc (i, x) -> if x then setBit acc (7-i) else acc) --- 0 --- (zip [0..] bits) - --- data Pair a = Pair a a --- deriving (Functor) - --- data Quad a = Quad (Pair a) (Pair a) --- deriving (Functor) - --- data Oct a = Oct (Quad a) (Quad a) --- deriving (Functor) - --- pairVal :: Pair Val -> Val --- pairVal (Pair x y) = VP x y - --- quadVal :: Quad Val -> Val --- quadVal (Quad x y) = VP (pairVal x) (pairVal y) - --- octVal :: Oct Val -> Val --- octVal (Oct x y) = VP (quadVal x) (quadVal y) - --- -- Needs to be four times as big -- This throws away data --- hashOct :: SHA256 -> Oct Word8 --- hashOct (SHA256 bs) = --- Oct (Quad (Pair a b) (Pair c d)) --- (Quad (Pair e f) (Pair g h)) --- where --- a = B.unsafeIndex bs 0 --- b = B.unsafeIndex bs 1 --- c = B.unsafeIndex bs 2 --- d = B.unsafeIndex bs 3 --- e = B.unsafeIndex bs 4 --- f = B.unsafeIndex bs 5 --- g = B.unsafeIndex bs 6 --- h = B.unsafeIndex bs 7 - --- valHash :: Val -> SHA256 --- valHash = \case --- VP (VP (VP a b) (VP c d)) (VP (VP e f) (VP g h)) -> --- SHA256 (B.pack $ valByte <$> [a, b, c, d, e, f, g, h]) --- _ -> --- SHA256 "" - --- hashToVal :: SHA256 -> Val --- hashToVal = octVal . fmap byteVal . hashOct - - --- Small-Step Interpreter ------------------------------------------------------ - -step :: Val -> Exp -> (Val, Exp) -step VV = const (VV, ESubj) -step s = \case - ENull -> (VN, ESubj) - ESubj -> (s, ESubj) - EWith ESubj y -> (s, y) - EWith x y -> case step s x of - (s', ESubj) -> (s', y) - (s', x' ) -> (s', EWith x' y) - - ETent ref -> - (runTent ref (valFor (getGrain ref)) s, ESubj) - - EEval -> - case s of - VP s' f' -> (s', valFor f') - _ -> (VV, ESubj) - - ECons ESubj ESubj -> (VP s s, ESubj) - ECons x y -> (VP (runExp s x) (runExp s y), ESubj) - ELeft -> (V0 s, ESubj) - EWrit -> (V1 s, ESubj) - EHead -> case s of - VP x _ -> (x, ESubj) - _ -> (VV, ESubj) - ETail -> case s of - VP _ y -> (y, ESubj) - _ -> (VV, ESubj) - EDist -> case s of - VP (V0 l) x -> (V0 (VP l x), ESubj) - VP (V1 r) x -> (V1 (VP r x), ESubj) - _ -> (VV, ESubj) - ECase p q -> case s of - V0 l -> (l, p) - V1 r -> (r, q) - _ -> (VV, ESubj) - EType _ -> (s, ESubj) - EPush -> case s of - VP s' f' -> let e = valFor f' - in traceShowId (VT s' e (runExp s' e), ESubj) - _ -> (VV, ESubj) - EPull -> case s of - VT _ _ x -> (x, ESubj) - _ -> (VV, ESubj) - EHash -> (putGrain s, ESubj) - EFall -> case s of - VR k -> (getGrain k, ESubj) - _ -> (VV, ESubj) - -displayExp :: Exp -> String -displayExp (EWith x y) = displayExp x <> "\n" <> displayExp y -displayExp x = "\t" <> show x - -traceRunExp :: Val -> Exp -> IO Val -traceRunExp s e = do - putStrLn (tshow (valExp s)) - putStrLn (pack $ displayExp e) - void getLine - case e of - ESubj -> do putStrLn "DONE" - pure s - _ -> uncurry traceRunExp (step s e) - -traceRun :: Conq () r -> IO Val -traceRun = traceRunExp VN . toExp - -flattenCons :: Exp -> Exp -> [Exp] -flattenCons = \x -> go [x] - where - go acc (ECons x y) = go (x:acc) y - go acc x = reverse (x:acc) - -instance Show Exp where - show = \case - ESubj -> "." - ENull -> "~" - 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 <> "}" - EPush -> "?" - EPull -> "*" - EHash -> "@" - EFall -> "^" - ETent ref -> "|" <> take 8 (unpack $ decodeBase58 $ unSHA256 ref) <> "|" - -parseSimpl :: String -> Maybe (Exp, String) -parseSimpl = \case - '.' : xs -> pure (ESubj, xs) - '~' : xs -> pure (ENull, xs) - '!' : 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 (EPush, xs) - '*' : xs -> pure (EPull, xs) - '@' : xs -> pure (EHash, xs) - '^' : xs -> pure (EFall, xs) - _ -> Nothing - -parseHash :: String -> Either String (SHA256, String) -parseHash b = do - let (h,r) = splitAt 44 b - let sha = SHA256 (encodeBase58 $ pack h) - when (length h /= 44) (P.Left "short tent") - pure (sha, r) - -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) -> (valExp (forVal e), cs) - '|':xs -> parseHash xs >>= \case - (s, '|':xs) -> pure (ETent s, xs) - (_, _ ) -> P.Left "bad tent" - _ -> P.Left "bad" - -repl :: IO () -repl = r VN - where - r sut = do - ln <- unpack <$> getLine - parseSeq '\n' ln & \case - P.Right (e,"") -> do - epl sut e - P.Right (e,cs) -> do - traceM ("ignoring trailing chars: " <> cs) - epl sut e - P.Left msg -> do - traceM msg - traceM "Try again\n" - r sut - - epl sut exp = do - sut' <- pure (runExp sut exp) - if (sut' == VV) - then do - putStrLn "Crash! Try again\n" - r sut - else do - putStrLn ("-> " <> tshow sut') - putStrLn "" - r sut' - -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) - --- Thunks are Easy ------------------------------------------------------------- - -data Thunk a = forall s. Thunk !s !(Conq s a) a - -push :: s -> Conq s a -> Thunk a -push s f = Thunk s f (run s f) - -pull :: Thunk a -> a -pull (Thunk _ _ r) = r - --- Refs need Serialization ----------------------------------------------------- - -data Ref a = Ref Int a -- TODO s/Int/Sha256/ - -hash :: a -> Ref a -hash x = Ref 0 x - -fall :: Ref a -> a -fall (Ref h x) = x - --------------------------------------------------------------------------------- - -data Conq s r where - Subj :: Conq s s - Null :: Conq s () - 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 - Hash :: Conq a (Ref a) - Fall :: Conq (Ref a) a - Push :: Conq (Tup s (Conq s a)) (Thunk a) - Pull :: Conq (Thunk a) a - -instance Category Conq where - id = Subj - (.) = flip With - -instance Show (Conq s r) where - show c = show (toExp c) - --------------------------------------------------------------------------------- - -run :: s -> Conq s r -> r -run sut = \case - Null -> () - Subj -> sut - With x y -> run (run sut x) y - Eval -> case sut of (s,f) -> run s f - Cons x y -> (run sut x, run sut y) - Left -> L sut - Writ -> R sut - Head -> fst sut - Tail -> snd sut - Dist -> case sut of (L l, x) -> L (l, x); (R r, x) -> R (r, x) - Case p q -> case sut of L l -> run l p; R r -> run r q - Push -> uncurry push sut - Pull -> pull sut - Hash -> hash sut - Fall -> fall sut - -times :: Int -> Conq s s -> Conq s s -times 0 _ = id -times 1 f = f -times n f = With f (times (n-1) f) - -runTimes :: Int -> s -> Conq s s -> s -runTimes n sut conq = go n - where - go 0 = sut - go 1 = run sut conq - go n = run (go (n-1)) conq - --------------------------------------------------------------------------------- - -toExp :: Conq s r -> Exp -toExp = \case - Subj -> ESubj - Null -> ENull - Eval -> EEval - Left -> ELeft - Writ -> EWrit - Head -> EHead - Tail -> ETail - Dist -> EDist - Cons x y -> ECons (toExp x) (toExp y) - Case l r -> ECase (toExp l) (toExp r) - With x y -> EWith (toExp x) (toExp y) - Push -> EPush - Pull -> EPull - Hash -> EHash - Fall -> EFall - --------------------------------------------------------------------------------- - -fromExp :: forall s r. (Typeable s, Typeable r) => Exp -> Maybe (Conq s r) -fromExp = \case - ESubj -> - case testEquality (typeRep @s) (typeRep @r) of - Just Refl -> Just (coerce Subj) - Nothing -> Nothing - - _ -> - Nothing - --- Axis Lookup ----------------------------------------------------------------- - -a1 :: Conq a a -a1 = Subj - -a2 :: Conq (Tup a b) a -a2 = Head - -a3 :: Conq (Tup a b) b -a3 = Tail - -a4 :: Conq (Tup (Tup a b) c) a -a4 = Head . Head - -a5 :: Conq (Tup (Tup a b) c) b -a5 = Tail . Head - -a6 :: Conq (Tup a (Tup b c)) b -a6 = Head . Tail - -a7 :: Conq (Tup a (Tup b c)) c -a7 = Tail . Tail - -a8 :: Conq (((a, b), c), d) a -a8 = Head . Head . Head - - --- Eat Operations -------------------------------------------------------------- - -nothing :: Conq s (Sum () a) -nothing = Left . Null - -just :: Conq a (Sum () a) -just = Writ - -case' :: Conq (a,s) r -> Conq (b,s) r -> Conq (Sum a b,s) r -case' x y = Case x y . Dist - -previewLeft :: Conq (Sum a b) (Sum () a) -previewLeft = Case just nothing - -previewWrit :: Conq (Sum a b) (Sum () b) -previewWrit = Case nothing just - - --- Pair Operations ------------------------------------------------------------- - -curry' :: Conq (a, b) c -> Conq s a -> Conq s b -> Conq s c -curry' f x y = With (Cons x y) f - -both :: Conq a b -> Conq (a, a) (b, b) -both x = Cons (With Head x) (With Tail x) - -dub_equal :: Conq (a, a) Bit -> Conq ((a, a), (a, a)) Bit -dub_equal cmp = With results bit_and - where - results = Cons (With (both Head) cmp) (With (both Tail) cmp) - -dub_test :: Conq a Bit -> Conq (a, a) Bit -dub_test test = curry' bit_and (With Head test) (With Tail test) - -dub_inc :: Conq a a -> Conq a Bit -> Conq (a, a) (a, a) -dub_inc inc null = With bump_low (if' low_zero bump_hig id) - where - bump_low = Cons (inc . Head) Tail - bump_hig = Cons Head (inc . Tail) - low_zero = null . Head - -type Tag a = Sum a a -- Tag with a bit: <0 1> -type Inc a = Conq a (Tag a) - -bit_incer :: Inc Bit -bit_incer = Case (Left . Writ) (Writ . Left) - -duo_incer' :: Inc Duo -duo_incer' = incer bit_incer - -duo_incer :: Inc Duo -duo_incer = Case (Left . Cons true Tail) carry . Dist - where - carry = Case (Left . Cons Left Writ) (Writ . Cons Left Left) . Tail - -incer :: forall a. Inc a -> Inc (a, a) -incer i = - Case Left hig . low - where - low, hig :: Inc (a, a) - low = Dist . Cons (i . Head) Tail - hig = Case (Left . flip') Writ . Dist . Cons (i . Tail) Head - -nyb_incer :: Inc Nyb -nyb_incer = incer duo_incer - -byt_incer :: Inc Byt -byt_incer = incer nyb_incer - -short_incer :: Inc Short -short_incer = incer byt_incer - -wide_incer :: Inc Wide -wide_incer = incer short_incer - -long_incer :: Inc Long -long_incer = incer wide_incer - -bit :: Int -> Bit -bit n = runTimes n val_bit_zero bit_inc - - --- Random Combinators ---------------------------------------------------------- - -dup :: Conq a (a, a) -dup = Cons Subj Subj - -eat :: Conq (Sum a a) a -eat = Case Subj Subj - -flip' :: Conq (a, b) (b, a) -flip' = Cons Tail Head - -if' :: Conq s Bit -> Conq s r -> Conq s r -> Conq s r -if' c t f = case' (f . Tail) (t . Tail) . Cons c Subj - -factor :: Conq (Sum (a, c) (b, c)) (Sum a b, c) -factor = Case (Cons (Left . Head) Tail) - (Cons (Writ . Head) Tail) - - --- Boolean Operations ---------------------------------------------------------- - -type Bit = Sum () () - -true :: Conq s Bit -true = Writ . Null - -false :: Conq s Bit -false = Left . Null - -bit_not :: Conq Bit Bit -bit_not = Case Writ Left - -bit_id :: Conq Bit Bit -bit_id = Case Left Writ - -bit_and :: Conq (Bit, Bit) Bit -bit_and = Case false Tail . Dist - -bit_or :: Conq (Bit, Bit) Bit -bit_or = Case Tail true . Dist - -bit_xor :: Conq (Bit, Bit) Bit -bit_xor = Case Tail (bit_not . Tail) . Dist - -bit_equal :: Conq (Bit, Bit) Bit -bit_equal = Case (bit_not . Tail) Tail . Dist - -bit_zero :: Conq s Bit -bit_zero = false - -val_bit_zero :: Bit -val_bit_zero = run () bit_zero - -bit_is_zero :: Conq Bit Bit -bit_is_zero = bit_not - -bit_inc :: Conq Bit Bit -bit_inc = bit_not - --- Duo Operations (2 bit) ------------------------------------------------------ - -type Duo = (Bit, Bit) - -duo_zero :: Conq s Duo -duo_zero = Cons bit_zero bit_zero - -duo_is_zero :: Conq Duo Bit -duo_is_zero = dub_test bit_is_zero - -duo_inc :: Conq Duo Duo -duo_inc = Case (Cons true Tail) (Cons false (bit_not . Tail)) . Dist - -duo :: Int -> Duo -duo n = runTimes n (run () duo_zero) duo_inc - -duo_equal :: Conq (Duo, Duo) Bit -duo_equal = dub_equal bit_equal - - --- Nibble Operations (4 bit) --------------------------------------------------- - -type Nyb = (Duo, Duo) - -nyb_zero :: Conq a Nyb -nyb_zero = Cons duo_zero duo_zero - -nyb_is_zero :: Conq Nyb Bit -nyb_is_zero = dub_test duo_is_zero - -nyb_inc :: Conq Nyb Nyb -nyb_inc = dub_inc duo_inc duo_is_zero - -nyb :: Int -> Nyb -nyb n = runTimes n (run () nyb_zero) nyb_inc - -nyb_equal :: Conq (Nyb, Nyb) Bit -nyb_equal = dub_equal duo_equal - - --- Byte Operations (8 bit) ----------------------------------------------------- - -type Byt = (Nyb, Nyb) - -byt_zero :: Conq a Byt -byt_zero = Cons nyb_zero nyb_zero - -byt_is_zero :: Conq Byt Bit -byt_is_zero = dub_test nyb_is_zero - -byt_inc :: Conq Byt Byt -byt_inc = dub_inc nyb_inc nyb_is_zero - -byt :: Int -> Byt -byt n = runTimes n (run () byt_zero) byt_inc - -byt_equal :: Conq (Byt, Byt) Bit -byt_equal = dub_equal nyb_equal - - --- Short Operations (16 bit) --------------------------------------------------- - -type Short = (Byt, Byt) - -short_zero :: Conq a Short -short_zero = Cons byt_zero byt_zero - -short_is_zero :: Conq Short Bit -short_is_zero = dub_test byt_is_zero - -short_inc :: Conq Short Short -short_inc = dub_inc byt_inc byt_is_zero - -short :: Int -> Short -short n = runTimes n (run () short_zero) short_inc - -short_equal :: Conq (Short, Short) Bit -short_equal = dub_equal byt_equal - - --- Wide Operations (32 bit) ---------------------------------------------------- - -type Wide = (Short, Short) - -wide_zero :: Conq a Wide -wide_zero = Cons short_zero short_zero - -wide_is_zero :: Conq Wide Bit -wide_is_zero = dub_test short_is_zero - -wide_inc :: Conq Wide Wide -wide_inc = dub_inc short_inc short_is_zero - -wide :: Int -> Wide -wide n = runTimes n (run () wide_zero) wide_inc - -wide_equal :: Conq (Wide, Wide) Bit -wide_equal = dub_equal short_equal - - --- Long Operations (64 bit) ---------------------------------------------------- - -type Long = (Wide, Wide) - -long_zero :: Conq a Long -long_zero = Cons wide_zero wide_zero - -long_is_zero :: Conq Long Bit -long_is_zero = dub_test wide_is_zero - -long_inc :: Conq Long Long -long_inc = dub_inc wide_inc wide_is_zero - -long :: Int -> Long -long n = runTimes n (run () long_zero) long_inc - -long_equal :: Conq (Long, Long) Bit -long_equal = dub_equal wide_equal - -n0 :: Conq a (Sum () a) -n0 = Left . Null - -n1 :: Conq a (Sum () (Sum () a)) -n1 = Writ . n0 - -n2 = Writ . n1 -n3 = Writ . n2 -n4 = Writ . n3 -n5 = Writ . n4 -n6 = Writ . n5 -n7 = Writ . n6 -n8 = Writ . n7 -n9 = Writ . n8 -n10 = Writ . n9 - - --------------------------------------------------------------------------------- - --- ((arg (ctx for)) fireTramp) -> %(!((arg ctx) for) (ctx for)) --- fireTramp = Payload --- fireTramp = undefined - --- [Lx y] -> R[x y] --- [R[x y] z] -> R[x (compose y z)] -compose :: Exp -compose = ECase EWrit (EWrit <> recur) <> EDist - where - recur = ECons (EHead <> EHead) - (ECons (ETail <> EHead) ETail) - --- ctx for -> (ctx for) -gate :: Val -> Exp -> Val -gate v e = VP v (forVal e) - --- `$-(a a)`: Identity -identFn :: Val -identFn = gate VN (toExp Head) - --- `$-(a b)`: Trivial-Loop -spinFn :: Val -spinFn = gate VN fire - -call :: Exp -> Exp -> Exp -call g a = fire <> ECons a g - -spin :: Exp -spin = call (valExp spinFn) ENull - --- `$-((list a) @)`: List-Length -lenFn :: Val -lenFn = gate (V0 VN) lenFnBody - -caseHead x y = ECase x y <> EDist - -hep, lus :: Exp -hep = EHead -lus = ETail -zer = ELeft -one = EWrit - -cons :: Exp -> Exp -> Exp -cons = ECons - -lenFnBody :: Exp -lenFnBody = caseHead (hep <> lus) - $ (fire <>) - $ cons (lus <> hep) - $ cons (one<>hep) lus <> lus - -swapFn :: Val -swapFn = gate VN (toExp swapFnBody) - -swapFnBody :: Conq ((a,b),x) (b,a) -swapFnBody = Cons Tail Head . Head - --- ctx lFor rFor -> (ctx (lfor rfor)) -coreTwo :: Val -> Exp -> Exp -> Val -coreTwo v l r = VP v (VP (forVal l) (forVal r)) - -evenOddCore :: Val -evenOddCore = coreTwo VN evArm odArm - -evArm, odArm :: Exp -evArm = caseHead (toExp true) fireRit -odArm = caseHead (toExp false) fireLef - --- (arg (ctx for)) -> ((arg (ctx for)) for)! -fire :: Exp -fire = EEval <> cons (∅) (lus <> lus) - --- (arg (ctx (lfor rfor))) -> ((arg (ctx (lfor rfor))) lfor)! -fireLef :: Exp -fireLef = EEval <> toExp reOrg - where - reOrg :: Conq (a,(c,(l,r))) ((a,(c,(l,r))),l) - reOrg = Cons Subj (Head . Tail . Tail) - --- (arg (ctx (lfor rfor))) -> ((arg (ctx (lfor rfor))) rfor)! -fireRit :: Exp -fireRit = EEval <> toExp reOrg - where - reOrg :: Conq (a,(c,(l,r))) ((a,(c,(l,r))),r) - reOrg = Cons Subj (Tail . Tail . Tail) - --- Demos ----------------------------------------------------------------------- - -type Payload = (Val, Exp) - -demo :: Payload -> IO Val -demo (s,f) = traceRunExp s f - -dumbLoop :: Exp -dumbLoop = EEval <> ECons (∅) (∅) - -dumbLoopP :: Payload -dumbLoopP = (forVal dumbLoop, dumbLoop) - -demo_dumb_loop :: IO Val -demo_dumb_loop = demo dumbLoopP - -demo_duo_overflow :: IO Val -demo_duo_overflow = traceRun (duo_incer . times 3 (eat . duo_incer) . duo_zero) - -demo_nat_constr :: IO Val -demo_nat_constr = traceRun n10 - --- [[-e +] +]! -fix :: Val -> Exp -> Payload -fix x e = (VP x (forVal fe), fe) - where - fe = EEval <> cons (cons (e <> hep) lus) lus - -natOverflow :: Exp -natOverflow = EEval <> cons (cons (one <> hep) lus) lus - -natOverflowPay :: Payload -natOverflowPay = fix (V0 VN) EWrit - -demo_nat_inc_loop :: IO Val -demo_nat_inc_loop = demo natOverflowPay - -duo_zero_val :: Val -duo_zero_val = VP (V0 VN) (V0 (VN)) - -short_zero_val :: Val -short_zero_val = runExp VN (toExp short_zero) - -short_inc_loop :: IO Val -short_inc_loop = demo $ fix (V0 short_zero_val) (toExp (short_incer . eat)) diff --git a/pkg/hs-conq/lib/Language/Conq/Axe.hs b/pkg/hs-conq/lib/Language/Conq/Axe.hs deleted file mode 100644 index a434bf340a..0000000000 --- a/pkg/hs-conq/lib/Language/Conq/Axe.hs +++ /dev/null @@ -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)) diff --git a/pkg/hs-conq/lib/Language/Conq/Exp.hs b/pkg/hs-conq/lib/Language/Conq/Exp.hs deleted file mode 100644 index e7d9dcfffd..0000000000 --- a/pkg/hs-conq/lib/Language/Conq/Exp.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-conq/lib/Language/Conq/ForVal.hs b/pkg/hs-conq/lib/Language/Conq/ForVal.hs deleted file mode 100644 index 5b0a071e3a..0000000000 --- a/pkg/hs-conq/lib/Language/Conq/ForVal.hs +++ /dev/null @@ -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 diff --git a/pkg/hs-conq/lib/Language/Conq/Grainary.hs b/pkg/hs-conq/lib/Language/Conq/Grainary.hs deleted file mode 100644 index 312906e430..0000000000 --- a/pkg/hs-conq/lib/Language/Conq/Grainary.hs +++ /dev/null @@ -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 diff --git a/pkg/hs-conq/lib/Language/Conq/Mess.hs b/pkg/hs-conq/lib/Language/Conq/Mess.hs deleted file mode 100644 index bc8c4e7d63..0000000000 --- a/pkg/hs-conq/lib/Language/Conq/Mess.hs +++ /dev/null @@ -1,1356 +0,0 @@ -{-# LANGUAGE StandaloneDeriving #-} - -module Language.Conq.Mess 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 - --------------------------------------------------------------------------------- - -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) - -data Val - = VV -- Void - | VN -- Null - | V0 !Val -- Left - | V1 !Val -- Right - | VP !Val !Val -- Pair - | VT !Val !Exp Val - | VR !SHA256 - deriving (Eq, Ord, Generic, Flat) - -instance Show Val where - show = show . valExp - -crash :: Exp -crash = EEval <> EEval <> (EPure VN) - -grainery :: IORef (HashMap SHA256 ByteString) -grainery = unsafePerformIO (newIORef grainsFromJets) - -grainsFromJets :: HashMap SHA256 ByteString -grainsFromJets = do - mapFromList $ jetReg <&> \(h,e,_) -> (h, flat (forVal e)) - -jetReg :: [(SHA256, Exp, Val -> Val)] -jetReg = - [ ( SHA256 (encodeBase58 "FWz5mTGmuVz2b4TLNa7yMjTKL7wihsEWakoUD2nzqP6q") - , ESubj - , id - ) - ] - -jets :: HashMap SHA256 (Val -> Val) -jets = mapFromList (jetReg <&> \(h,_,f) -> (h,f)) - -{- -runTent :: SHA256 -> Exp -> Val -> Val -runTent k exp arg = - lookup k jets & \case - Nothing -> runExp arg exp - Just fn -> trace ("running jet " <> show (ETent k)) (fn arg) --} - -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 - -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) - -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 - -valExp :: Val -> Exp --- Exp (valFor' -> Just e) = EQuot e -valExp VN = EPure VN -valExp VV = crash -valExp v = go v <> EPure VN - where - go = \case - -- lFor' → 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) - -hashVal :: Val -> (ByteString, SHA256) -hashVal x = (bs, SHA256 (SHA256.hash bs)) - where bs = flat x - -data TyExp - = TENil - | TESum TyExp TyExp - | TETup TyExp TyExp - | TEFor TyExp TyExp - | TEAll TyExp - | TEFix TyExp - | TERef Int - deriving (Eq, Ord, Generic, Flat) - -instance Show TyExp where - show = \case - TESum TENil TENil -> "?" - TENil -> "~" - TESum x y -> "<" <> show x <> " " <> show y <> ">" - TETup x y -> "[" <> show x <> " " <> show y <> "]" - TEFor x y -> "(" <> show x <> " " <> show y <> ")" - TEAll x -> "A" <> show x - TEFix x -> "F" <> show x - TERef x -> show x - -data Ty - = TNil - | TSum Ty Ty - | TTup Ty Ty - | TFor Ty Ty - | TVar Int - deriving (Eq, Ord) - -tBit :: TyExp -tBit = TESum TENil TENil - -tBitOp :: TyExp -tBitOp = TEFor tBit tBit - -instance Show Ty where - show = \case - TNil -> "~" - TSum x y -> "<" <> show x <> " " <> show y <> ">" - TTup x y -> "[" <> show x <> " " <> show y <> "]" - TFor x y -> "(" <> show x <> " => " <> show y <> ")" - TVar x -> show x - -tyExpTy :: TyExp -> Infer Ty -tyExpTy = go [] - where - go :: [Int] -> TyExp -> Infer Ty - go t = \case - TENil -> pure TNil - TESum x y -> TSum <$> go t x <*> go t y - TETup x y -> TTup <$> go t x <*> go t y - TEFor x y -> TFor <$> go t x <*> go t y - TEAll x -> do t' <- (:t) <$> mkTVar - go t' x - TEFix x -> do t' <- (:t) <$> mkTVar - go t' x - TERef i -> pure $ TVar (t P.!! i) - -declare :: Ty -> TyExp -> Infer Ty -declare t e = do - te <- tyExpTy e - unify t te - -checkType :: Exp -> Either Text Ty -checkType e = runInfer (infer e >>= finalize) - -type Unique = Int -type Infer a = ExceptT Text (State (Map Int Ty, Unique)) a -type Unify a = Maybe a - -mkTVar :: Infer Int -mkTVar = do - (env, n) <- get - put (env, n+1) - pure n - -forAll :: Infer Ty -forAll = TVar <$> mkTVar - -varIs :: Int -> Ty -> Infer Ty -varIs v (TVar x) | x==v = do - pure (TVar x) -varIs v t = do - (env, n) <- get - put (insertMap v t env, n) - pure t - -finalize :: Ty -> Infer Ty -finalize (TVar v) = resolve v >>= finalize' -finalize t = finalize' t - -finalize' :: Ty -> Infer Ty -finalize' = \case - TNil -> pure TNil - TVar x -> pure (TVar x) - TSum x y -> TSum <$> finalize x <*> finalize y - TTup x y -> TTup <$> finalize x <*> finalize y - TFor x y -> TFor <$> finalize x <*> finalize y - -unify :: Ty -> Ty -> Infer Ty -unify x y = do - -- traceM $ "UNIFY " <> show x <> " " <> show y - x <- case x of { TVar v -> resolve v; x -> pure x } - y <- case y of { TVar v -> resolve v; y -> pure y } - unify' x y - -unify' :: Ty -> Ty -> Infer Ty -unify' = curry \case - ( TNil, TNil ) → pure TNil - ( TSum a1 b1, TSum a2 b2 ) → TSum <$> unify a1 a2 <*> unify b1 b2 - ( TTup a1 b1, TTup a2 b2 ) → TTup <$> unify a1 a2 <*> unify b1 b2 - ( TFor a1 b1, TFor a2 b2 ) → TFor <$> unify a1 a2 <*> unify b1 b2 - ( ty, TVar x ) → varIs x ty - ( TVar x, ty ) → varIs x ty - ( x, y ) → throwE - $ "Bad unify: " <> tshow x <> " " <> tshow y - -resolve :: Int -> Infer Ty -resolve v = do - (env, _) <- get - lookup v env & \case - Nothing -> pure (TVar v) - Just (TVar x) -> resolve x - Just x -> pure x - -expectFor :: Ty -> Infer (Ty, Ty, Ty) -expectFor = \case - ty@(TFor x y) -> pure (ty, x, y) - t -> throwE ("Not a formula: " <> tshow t) - -runInfer :: Infer a -> Either Text a -runInfer = flip evalState ((∅), 0) . runExceptT - -infer :: Exp -> Infer Ty -infer = \case - EPure _v -> do - a <- forAll - pure (TFor a TNil) -- TODO - - ESubj -> do - a <- forAll - pure (TFor a a) - - ELeft -> do - (a, b) <- (,) <$> forAll <*> forAll - pure (TFor a (TSum a b)) - - EWrit -> do - (a, b) <- (,) <$> forAll <*> forAll - pure (TFor b (TSum a b)) - - EHead -> do - (a, b) <- (,) <$> forAll <*> forAll - pure $ TFor (TTup a b) a - - ETail -> do - (a, b) <- (,) <$> forAll <*> forAll - pure $ TFor (TTup a b) b - - EDist -> do - (a, b, c) <- (,,) <$> forAll <*> forAll <*> forAll - pure $ TFor (TTup (TSum a b) c) (TSum (TTup a c) (TTup b c)) - - EEval -> do - (a, b) <- (,) <$> forAll <*> forAll - pure $ TFor (TTup a (TFor a b)) b - - EWith x y -> do - (xt, xi, xo) <- infer x >>= expectFor - (yt, yi, yo) <- infer y >>= expectFor - unify xo yi - pure (TFor xi yo) - - ECons x y -> do - (xt, xi, xo) <- infer x >>= expectFor - (yt, yi, yo) <- infer y >>= expectFor - unify xi yi - pure (TFor xi (TTup xo yo)) - - ECase p q -> do - (pt, pi, po) <- infer p >>= expectFor - (qt, qi, qo) <- infer q >>= expectFor - unify po qo - pure (TFor (TSum pi qi) po) - - EType t -> do - tt <- tyExpTy t - pure (TFor tt tt) - - ELazy -> throwE "infer: EPush" -- TODO - EMark -> throwE "infer: EHash" -- TODO - --- An Alternate Encoding for Conq ---------------------------------------------- - -data Flag = T | F - deriving (Generic, Flat) - -data Hint = HLazy | HMark - deriving (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 (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 [] - -instance Show Axe where - show = show . axeVal - --- Convenience ----------------------------------------------------------------- - -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 --------------------------------------------------------- - -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 - -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 - -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) - EType ty -> undefined - EMark -> AHint HMark - ELazy -> AHint HMark - ETent ref -> expAxe (valFor (getGrain ref)) - EQuot e -> APure (axeVal (expAxe e)) ---EUnquot e -> undefined - - -hintVal :: Hint -> Val -hintVal HLazy = V0 VN -hintVal HMark = 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))) - --------------------------------------------------------------------------------- - -data Exp - = ESubj - | EPure Val - | EEval - | ELeft - | EWrit - | EHead - | ETail - | EDist - | EWith Exp Exp - | ECons Exp Exp - | ECase Exp Exp - - -- Hints - | EType TyExp - | EMark - | ELazy - - -- Convenience - | ETent SHA256 - | EQuot Exp --- | EUnquot Exp - deriving (Eq, Ord, Generic, Flat) - -instance Semigroup Exp where - x <> y = EWith y x - -instance Monoid Exp where - mempty = ESubj - -runExp :: Val -> Exp -> Val -runExp s ESubj = s -runExp s e = uncurry runExp (step s e) - --- Get a formula from a Val ---------------------------------------------------- - -{- - :+ <: > - :+ :+ <<- +> <~ .>> - < <◆ ▪>> - :+ <<, ●> > - <<# @> <^ |>> --} - - -{- - for = - opk = < < > - dir = - get = <- +> - sim = <~ .> - otr = - plx = <◆ ▪> - quo = <, ●> - hin = < <<# @> <^ |>>> --} - -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 --- ETent ref -> V1 $ V0 $ V1 $ V1 $ V0 VN - EMark -> V1 $ V0 $ V1 $ V1 $ V0 VN --- ETent ref -> VR ref - 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 - -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 - --------------------------------------------------------------------------------- - --- tag :: Bool -> Val -> Val --- tag False = V0 --- tag True = V1 - --- unTag :: Val -> (Bool, Val) --- unTag (V0 x) = (False, x) --- unTag (V1 x) = (True, x) --- unTag _ = error "unTag" - --- toBits :: (Bits b, FiniteBits b) => b -> Vector Bool --- toBits b = --- generate (finiteBitSize b) (testBit b) - --- byteVal :: Word8 -> Val --- byteVal b = --- foldl' (flip tag) VN (toBits b) - --- valByte :: Val -> Word8 --- valByte v = runIdentity $ do --- (a, v) <- pure $ unTag v --- (b, v) <- pure $ unTag v --- (c, v) <- pure $ unTag v --- (d, v) <- pure $ unTag v --- (e, v) <- pure $ unTag v --- (f, v) <- pure $ unTag v --- (g, v) <- pure $ unTag v --- (h, v) <- pure $ unTag v --- let bits = [a, b, c, d, e, f, g, h] --- unless (VN == v) (error "valByte: bad byte") --- pure $ foldl' (\acc (i, x) -> if x then setBit acc (7-i) else acc) --- 0 --- (zip [0..] bits) - --- data Pair a = Pair a a --- deriving (Functor) - --- data Quad a = Quad (Pair a) (Pair a) --- deriving (Functor) - --- data Oct a = Oct (Quad a) (Quad a) --- deriving (Functor) - --- pairVal :: Pair Val -> Val --- pairVal (Pair x y) = VP x y - --- quadVal :: Quad Val -> Val --- quadVal (Quad x y) = VP (pairVal x) (pairVal y) - --- octVal :: Oct Val -> Val --- octVal (Oct x y) = VP (quadVal x) (quadVal y) - --- -- Needs to be four times as big -- This throws away data --- hashOct :: SHA256 -> Oct Word8 --- hashOct (SHA256 bs) = --- Oct (Quad (Pair a b) (Pair c d)) --- (Quad (Pair e f) (Pair g h)) --- where --- a = B.unsafeIndex bs 0 --- b = B.unsafeIndex bs 1 --- c = B.unsafeIndex bs 2 --- d = B.unsafeIndex bs 3 --- e = B.unsafeIndex bs 4 --- f = B.unsafeIndex bs 5 --- g = B.unsafeIndex bs 6 --- h = B.unsafeIndex bs 7 - --- valHash :: Val -> SHA256 --- valHash = \case --- VP (VP (VP a b) (VP c d)) (VP (VP e f) (VP g h)) -> --- SHA256 (B.pack $ valByte <$> [a, b, c, d, e, f, g, h]) --- _ -> --- SHA256 "" - --- hashToVal :: SHA256 -> Val --- hashToVal = octVal . fmap byteVal . hashOct - - --- Small-Step Interpreter ------------------------------------------------------ - -step :: Val -> Exp -> (Val, Exp) -step VV = const (VV, ESubj) -step s = \case - EPure v -> (v, ESubj) - ESubj -> (s, ESubj) - EWith ESubj y -> (s, y) - EWith x y -> case step s x of - (s', ESubj) -> (s', y) - (s', x' ) -> (s', EWith x' y) - - EEval -> - case s of - VP s' f' -> (s', valFor f') - _ -> (VV, ESubj) - - ECons ESubj ESubj -> (VP s s, ESubj) - ECons x y -> (VP (runExp s x) (runExp s y), ESubj) - ELeft -> (V0 s, ESubj) - EWrit -> (V1 s, ESubj) - EHead -> case s of - VP x _ -> (x, ESubj) - _ -> (VV, ESubj) - ETail -> case s of - VP _ y -> (y, ESubj) - _ -> (VV, ESubj) - EDist -> case s of - VP (V0 l) x -> (V0 (VP l x), ESubj) - VP (V1 r) x -> (V1 (VP r x), ESubj) - _ -> (VV, ESubj) - ECase p q -> case s of - V0 l -> (l, p) - V1 r -> (r, q) - _ -> (VV, ESubj) - EType _ -> (s, ESubj) - ELazy -> case s of - VP s' f' -> let e = valFor f' - in traceShowId (VT s' e (runExp s' e), ESubj) - _ -> (VV, ESubj) - EMark -> (putGrain s, ESubj) - EQuot e -> (forVal e, ESubj) - -displayExp :: Exp -> String -displayExp (EWith x y) = displayExp x <> "\n" <> displayExp y -displayExp x = "\t" <> show x - -traceRunExp :: Val -> Exp -> IO Val -traceRunExp s e = do - putStrLn (tshow (valExp s)) - putStrLn (pack $ displayExp e) - void getLine - case e of - ESubj -> do putStrLn "DONE" - pure s - _ -> uncurry traceRunExp (step s e) - -traceRun :: Conq () r -> IO Val -traceRun = traceRunExp VN . toExp - -flattenCons :: Exp -> Exp -> [Exp] -flattenCons = \x -> go [x] - where - go acc (ECons x y) = go (x:acc) y - go acc x = reverse (x:acc) - -instance Show Exp where - show = \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 -> "?" - EMark -> "@" - EQuot x -> "(" <> show x <> ")" --- ETent ref -> "|" <> take 8 (unpack $ decodeBase58 $ unSHA256 ref) <> "|" - -parseSimpl :: String -> Maybe (Exp, String) -parseSimpl = \case - '.' : xs -> pure (ESubj, xs) ---'~' : xs -> pure (ENull, 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 - -parseHash :: String -> Either String (SHA256, String) -parseHash b = do - let (h,r) = splitAt 44 b - let sha = SHA256 (encodeBase58 $ pack h) - when (length h /= 44) (P.Left "short tent") - pure (sha, r) - -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) --- '|':xs -> parseHash xs >>= \case --- (s, '|':xs) -> pure (ETent s, xs) --- (_, _ ) -> P.Left "bad tent" - _ -> P.Left "bad" - -repl :: IO () -repl = r VN - where - r sut = do - ln <- unpack <$> getLine - parseSeq '\n' ln & \case - P.Right (e,"") -> do - epl sut e - P.Right (e,cs) -> do - traceM ("ignoring trailing chars: " <> cs) - epl sut e - P.Left msg -> do - traceM msg - traceM "Try again\n" - r sut - - epl sut exp = do - sut' <- pure (runExp sut exp) - if (sut' == VV) - then do - putStrLn "Crash! Try again\n" - r sut - else do - putStrLn ("-> " <> tshow sut') - putStrLn "" - r sut' - -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) - --------------------------------------------------------------------------------- - -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 - -instance Show (Conq s r) where - show c = show (toExp c) - --------------------------------------------------------------------------------- - -run :: s -> Conq s r -> r -run sut = \case - Pure x -> x - Subj -> sut - With x y -> run (run sut x) y - Eval -> case sut of (s,f) -> run s f - Cons x y -> (run sut x, run sut y) - Left -> L sut - Writ -> R sut - Head -> fst sut - Tail -> snd sut - Dist -> case sut of (L l, x) -> L (l, x); (R r, x) -> R (r, x) - Case p q -> case sut of L l -> run l p; R r -> run r q - Mark -> sut - Lazy -> sut - -times :: Int -> Conq s s -> Conq s s -times 0 _ = id -times 1 f = f -times n f = With f (times (n-1) f) - -runTimes :: Int -> s -> Conq s s -> s -runTimes n sut conq = go n - where - go 0 = sut - go 1 = run sut conq - go n = run (go (n-1)) conq - --------------------------------------------------------------------------------- - -toExp :: Conq s r -> Exp -toExp = \case - Subj -> ESubj - Pure _ -> EPure VN -- TODO - Eval -> EEval - Left -> ELeft - Writ -> EWrit - Head -> EHead - Tail -> ETail - Dist -> EDist - Cons x y -> ECons (toExp x) (toExp y) - Case l r -> ECase (toExp l) (toExp r) - With x y -> EWith (toExp x) (toExp y) - Lazy -> ELazy - Mark -> EMark - --------------------------------------------------------------------------------- - -fromExp :: forall s r. (Typeable s, Typeable r) => Exp -> Maybe (Conq s r) -fromExp = \case - ESubj -> - case testEquality (typeRep @s) (typeRep @r) of - Just Refl -> Just (coerce Subj) - Nothing -> Nothing - - _ -> - Nothing - --- Axis Lookup ----------------------------------------------------------------- - -a1 :: Conq a a -a1 = Subj - -a2 :: Conq (Tup a b) a -a2 = Head - -a3 :: Conq (Tup a b) b -a3 = Tail - -a4 :: Conq (Tup (Tup a b) c) a -a4 = Head . Head - -a5 :: Conq (Tup (Tup a b) c) b -a5 = Tail . Head - -a6 :: Conq (Tup a (Tup b c)) b -a6 = Head . Tail - -a7 :: Conq (Tup a (Tup b c)) c -a7 = Tail . Tail - -a8 :: Conq (((a, b), c), d) a -a8 = Head . Head . Head - - --- Eat Operations -------------------------------------------------------------- - -nothing :: Conq s (Sum () a) -nothing = Left . Pure() - -just :: Conq a (Sum () a) -just = Writ - -case' :: Conq (a,s) r -> Conq (b,s) r -> Conq (Sum a b,s) r -case' x y = Case x y . Dist - -previewLeft :: Conq (Sum a b) (Sum () a) -previewLeft = Case just nothing - -previewWrit :: Conq (Sum a b) (Sum () b) -previewWrit = Case nothing just - - --- Pair Operations ------------------------------------------------------------- - -curry' :: Conq (a, b) c -> Conq s a -> Conq s b -> Conq s c -curry' f x y = With (Cons x y) f - -both :: Conq a b -> Conq (a, a) (b, b) -both x = Cons (With Head x) (With Tail x) - -dub_equal :: Conq (a, a) Bit -> Conq ((a, a), (a, a)) Bit -dub_equal cmp = With results bit_and - where - results = Cons (With (both Head) cmp) (With (both Tail) cmp) - -dub_test :: Conq a Bit -> Conq (a, a) Bit -dub_test test = curry' bit_and (With Head test) (With Tail test) - -dub_inc :: Conq a a -> Conq a Bit -> Conq (a, a) (a, a) -dub_inc inc null = With bump_low (if' low_zero bump_hig id) - where - bump_low = Cons (inc . Head) Tail - bump_hig = Cons Head (inc . Tail) - low_zero = null . Head - -type Tag a = Sum a a -- Tag with a bit: <0 1> -type Inc a = Conq a (Tag a) - -bit_incer :: Inc Bit -bit_incer = Case (Left . Writ) (Writ . Left) - -duo_incer' :: Inc Duo -duo_incer' = incer bit_incer - -duo_incer :: Inc Duo -duo_incer = Case (Left . Cons true Tail) carry . Dist - where - carry = Case (Left . Cons Left Writ) (Writ . Cons Left Left) . Tail - -incer :: forall a. Inc a -> Inc (a, a) -incer i = - Case Left hig . low - where - low, hig :: Inc (a, a) - low = Dist . Cons (i . Head) Tail - hig = Case (Left . flip') Writ . Dist . Cons (i . Tail) Head - -nyb_incer :: Inc Nyb -nyb_incer = incer duo_incer - -byt_incer :: Inc Byt -byt_incer = incer nyb_incer - -short_incer :: Inc Short -short_incer = incer byt_incer - -wide_incer :: Inc Wide -wide_incer = incer short_incer - -long_incer :: Inc Long -long_incer = incer wide_incer - -bit :: Int -> Bit -bit n = runTimes n val_bit_zero bit_inc - - --- Random Combinators ---------------------------------------------------------- - -dup :: Conq a (a, a) -dup = Cons Subj Subj - -eat :: Conq (Sum a a) a -eat = Case Subj Subj - -flip' :: Conq (a, b) (b, a) -flip' = Cons Tail Head - -if' :: Conq s Bit -> Conq s r -> Conq s r -> Conq s r -if' c t f = case' (f . Tail) (t . Tail) . Cons c Subj - -factor :: Conq (Sum (a, c) (b, c)) (Sum a b, c) -factor = Case (Cons (Left . Head) Tail) - (Cons (Writ . Head) Tail) - - --- Boolean Operations ---------------------------------------------------------- - -type Bit = Sum () () - -true :: Conq s Bit -true = Writ . Pure() - -false :: Conq s Bit -false = Left . Pure() - -bit_not :: Conq Bit Bit -bit_not = Case Writ Left - -bit_id :: Conq Bit Bit -bit_id = Case Left Writ - -bit_and :: Conq (Bit, Bit) Bit -bit_and = Case false Tail . Dist - -bit_or :: Conq (Bit, Bit) Bit -bit_or = Case Tail true . Dist - -bit_xor :: Conq (Bit, Bit) Bit -bit_xor = Case Tail (bit_not . Tail) . Dist - -bit_equal :: Conq (Bit, Bit) Bit -bit_equal = Case (bit_not . Tail) Tail . Dist - -bit_zero :: Conq s Bit -bit_zero = false - -val_bit_zero :: Bit -val_bit_zero = run () bit_zero - -bit_is_zero :: Conq Bit Bit -bit_is_zero = bit_not - -bit_inc :: Conq Bit Bit -bit_inc = bit_not - --- Duo Operations (2 bit) ------------------------------------------------------ - -type Duo = (Bit, Bit) - -duo_zero :: Conq s Duo -duo_zero = Cons bit_zero bit_zero - -duo_is_zero :: Conq Duo Bit -duo_is_zero = dub_test bit_is_zero - -duo_inc :: Conq Duo Duo -duo_inc = Case (Cons true Tail) (Cons false (bit_not . Tail)) . Dist - -duo :: Int -> Duo -duo n = runTimes n (run () duo_zero) duo_inc - -duo_equal :: Conq (Duo, Duo) Bit -duo_equal = dub_equal bit_equal - - --- Nibble Operations (4 bit) --------------------------------------------------- - -type Nyb = (Duo, Duo) - -nyb_zero :: Conq a Nyb -nyb_zero = Cons duo_zero duo_zero - -nyb_is_zero :: Conq Nyb Bit -nyb_is_zero = dub_test duo_is_zero - -nyb_inc :: Conq Nyb Nyb -nyb_inc = dub_inc duo_inc duo_is_zero - -nyb :: Int -> Nyb -nyb n = runTimes n (run () nyb_zero) nyb_inc - -nyb_equal :: Conq (Nyb, Nyb) Bit -nyb_equal = dub_equal duo_equal - - --- Byte Operations (8 bit) ----------------------------------------------------- - -type Byt = (Nyb, Nyb) - -byt_zero :: Conq a Byt -byt_zero = Cons nyb_zero nyb_zero - -byt_is_zero :: Conq Byt Bit -byt_is_zero = dub_test nyb_is_zero - -byt_inc :: Conq Byt Byt -byt_inc = dub_inc nyb_inc nyb_is_zero - -byt :: Int -> Byt -byt n = runTimes n (run () byt_zero) byt_inc - -byt_equal :: Conq (Byt, Byt) Bit -byt_equal = dub_equal nyb_equal - - --- Short Operations (16 bit) --------------------------------------------------- - -type Short = (Byt, Byt) - -short_zero :: Conq a Short -short_zero = Cons byt_zero byt_zero - -short_is_zero :: Conq Short Bit -short_is_zero = dub_test byt_is_zero - -short_inc :: Conq Short Short -short_inc = dub_inc byt_inc byt_is_zero - -short :: Int -> Short -short n = runTimes n (run () short_zero) short_inc - -short_equal :: Conq (Short, Short) Bit -short_equal = dub_equal byt_equal - - --- Wide Operations (32 bit) ---------------------------------------------------- - -type Wide = (Short, Short) - -wide_zero :: Conq a Wide -wide_zero = Cons short_zero short_zero - -wide_is_zero :: Conq Wide Bit -wide_is_zero = dub_test short_is_zero - -wide_inc :: Conq Wide Wide -wide_inc = dub_inc short_inc short_is_zero - -wide :: Int -> Wide -wide n = runTimes n (run () wide_zero) wide_inc - -wide_equal :: Conq (Wide, Wide) Bit -wide_equal = dub_equal short_equal - - --- Long Operations (64 bit) ---------------------------------------------------- - -type Long = (Wide, Wide) - -long_zero :: Conq a Long -long_zero = Cons wide_zero wide_zero - -long_is_zero :: Conq Long Bit -long_is_zero = dub_test wide_is_zero - -long_inc :: Conq Long Long -long_inc = dub_inc wide_inc wide_is_zero - -long :: Int -> Long -long n = runTimes n (run () long_zero) long_inc - -long_equal :: Conq (Long, Long) Bit -long_equal = dub_equal wide_equal - -n0 :: Conq a (Sum () a) -n0 = Left . Pure() - -n1 :: Conq a (Sum () (Sum () a)) -n1 = Writ . n0 - -n2 = Writ . n1 -n3 = Writ . n2 -n4 = Writ . n3 -n5 = Writ . n4 -n6 = Writ . n5 -n7 = Writ . n6 -n8 = Writ . n7 -n9 = Writ . n8 -n10 = Writ . n9 - - --------------------------------------------------------------------------------- - --- ((arg (ctx for)) fireTramp) -> %(!((arg ctx) for) (ctx for)) --- fireTramp = Payload --- fireTramp = undefined - --- [Lx y] -> R[x y] --- [R[x y] z] -> R[x (compose y z)] -compose :: Exp -compose = ECase EWrit (EWrit <> recur) <> EDist - where - recur = ECons (EHead <> EHead) - (ECons (ETail <> EHead) ETail) - --- ctx for -> (ctx for) -gate :: Val -> Exp -> Val -gate v e = VP v (forVal e) - --- `$-(a a)`: Identity -identFn :: Val -identFn = gate VN (toExp Head) - --- `$-(a b)`: Trivial-Loop -spinFn :: Val -spinFn = gate VN fire - -call :: Exp -> Exp -> Exp -call g a = fire <> ECons a g - -spin :: Exp -spin = call (valExp spinFn) (EPure VN) - --- `$-((list a) @)`: List-Length -lenFn :: Val -lenFn = gate (V0 VN) lenFnBody - -caseHead x y = ECase x y <> EDist - -hep, lus :: Exp -hep = EHead -lus = ETail -zer = ELeft -one = EWrit - -cons :: Exp -> Exp -> Exp -cons = ECons - -lenFnBody :: Exp -lenFnBody = caseHead (hep <> lus) - $ (fire <>) - $ cons (lus <> hep) - $ cons (one<>hep) lus <> lus - -swapFn :: Val -swapFn = gate VN (toExp swapFnBody) - -swapFnBody :: Conq ((a,b),x) (b,a) -swapFnBody = Cons Tail Head . Head - --- ctx lFor rFor -> (ctx (lfor rfor)) -coreTwo :: Val -> Exp -> Exp -> Val -coreTwo v l r = VP v (VP (forVal l) (forVal r)) - -evenOddCore :: Val -evenOddCore = coreTwo VN evArm odArm - -evArm, odArm :: Exp -evArm = caseHead (toExp true) fireRit -odArm = caseHead (toExp false) fireLef - --- (arg (ctx for)) -> ((arg (ctx for)) for)! -fire :: Exp -fire = EEval <> cons (∅) (lus <> lus) - --- (arg (ctx (lfor rfor))) -> ((arg (ctx (lfor rfor))) lfor)! -fireLef :: Exp -fireLef = EEval <> toExp reOrg - where - reOrg :: Conq (a,(c,(l,r))) ((a,(c,(l,r))),l) - reOrg = Cons Subj (Head . Tail . Tail) - --- (arg (ctx (lfor rfor))) -> ((arg (ctx (lfor rfor))) rfor)! -fireRit :: Exp -fireRit = EEval <> toExp reOrg - where - reOrg :: Conq (a,(c,(l,r))) ((a,(c,(l,r))),r) - reOrg = Cons Subj (Tail . Tail . Tail) - --- Demos ----------------------------------------------------------------------- - -type Payload = (Val, Exp) - -demo :: Payload -> IO Val -demo (s,f) = traceRunExp s f - -dumbLoop :: Exp -dumbLoop = EEval <> ECons (∅) (∅) - -dumbLoopP :: Payload -dumbLoopP = (forVal dumbLoop, dumbLoop) - -demo_dumb_loop :: IO Val -demo_dumb_loop = demo dumbLoopP - -demo_duo_overflow :: IO Val -demo_duo_overflow = traceRun (duo_incer . times 3 (eat . duo_incer) . duo_zero) - -demo_nat_constr :: IO Val -demo_nat_constr = traceRun n10 - --- [[-e +] +]! -fix :: Val -> Exp -> Payload -fix x e = (VP x (forVal fe), fe) - where - fe = EEval <> cons (cons (e <> hep) lus) lus - -natOverflow :: Exp -natOverflow = EEval <> cons (cons (one <> hep) lus) lus - -natOverflowPay :: Payload -natOverflowPay = fix (V0 VN) EWrit - -demo_nat_inc_loop :: IO Val -demo_nat_inc_loop = demo natOverflowPay - -duo_zero_val :: Val -duo_zero_val = VP (V0 VN) (V0 (VN)) - -short_zero_val :: Val -short_zero_val = runExp VN (toExp short_zero) - -short_inc_loop :: IO Val -short_inc_loop = demo $ fix (V0 short_zero_val) (toExp (short_incer . eat)) diff --git a/pkg/hs-conq/lib/Language/Conq/Types.hs b/pkg/hs-conq/lib/Language/Conq/Types.hs deleted file mode 100644 index 0cf320220d..0000000000 --- a/pkg/hs-conq/lib/Language/Conq/Types.hs +++ /dev/null @@ -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 diff --git a/pkg/hs-conq/package.yaml b/pkg/hs-conq/package.yaml deleted file mode 100644 index 798edf1304..0000000000 --- a/pkg/hs-conq/package.yaml +++ /dev/null @@ -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 diff --git a/pkg/hs-hoon/.gitignore b/pkg/hs-hoon/.gitignore deleted file mode 100644 index c99ca9e136..0000000000 --- a/pkg/hs-hoon/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -.stack-work -*.cabal diff --git a/pkg/hs-hoon/lib/Language/Attila/AST/Parser.hs b/pkg/hs-hoon/lib/Language/Attila/AST/Parser.hs deleted file mode 100644 index f13bd7eee2..0000000000 --- a/pkg/hs-hoon/lib/Language/Attila/AST/Parser.hs +++ /dev/null @@ -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 - ] diff --git a/pkg/hs-hoon/lib/Language/Attila/AST/Types.hs b/pkg/hs-hoon/lib/Language/Attila/AST/Types.hs deleted file mode 100644 index f112790691..0000000000 --- a/pkg/hs-hoon/lib/Language/Attila/AST/Types.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-hoon/lib/Language/Attila/IR.hs b/pkg/hs-hoon/lib/Language/Attila/IR.hs deleted file mode 100644 index 3d8551099f..0000000000 --- a/pkg/hs-hoon/lib/Language/Attila/IR.hs +++ /dev/null @@ -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])) --} diff --git a/pkg/hs-hoon/lib/Language/Hoon/AST/Parser.hs b/pkg/hs-hoon/lib/Language/Hoon/AST/Parser.hs deleted file mode 100644 index 89ff3e3b42..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/AST/Parser.hs +++ /dev/null @@ -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 - ] diff --git a/pkg/hs-hoon/lib/Language/Hoon/AST/Types.hs b/pkg/hs-hoon/lib/Language/Hoon/AST/Types.hs deleted file mode 100644 index b34ded52f3..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/AST/Types.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-hoon/lib/Language/Hoon/Desugar.hs b/pkg/hs-hoon/lib/Language/Hoon/Desugar.hs deleted file mode 100644 index 9eb34ff51f..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/Desugar.hs +++ /dev/null @@ -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" - - - diff --git a/pkg/hs-hoon/lib/Language/Hoon/IR/Desugar.hs b/pkg/hs-hoon/lib/Language/Hoon/IR/Desugar.hs deleted file mode 100644 index 0b936d6631..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/IR/Desugar.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-hoon/lib/Language/Hoon/IR/Infer.hs b/pkg/hs-hoon/lib/Language/Hoon/IR/Infer.hs deleted file mode 100644 index b26a17f4f9..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/IR/Infer.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-hoon/lib/Language/Hoon/IR/Ty.hs b/pkg/hs-hoon/lib/Language/Hoon/IR/Ty.hs deleted file mode 100644 index 1ff1bdd0cb..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/IR/Ty.hs +++ /dev/null @@ -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 diff --git a/pkg/hs-hoon/lib/Language/Hoon/IR/Wing.hs b/pkg/hs-hoon/lib/Language/Hoon/IR/Wing.hs deleted file mode 100644 index 1b81e609e0..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/IR/Wing.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-hoon/lib/Language/Hoon/LL/Gen.hs b/pkg/hs-hoon/lib/Language/Hoon/LL/Gen.hs deleted file mode 100644 index 5c5acf56c0..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/LL/Gen.hs +++ /dev/null @@ -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 diff --git a/pkg/hs-hoon/lib/Language/Hoon/LL/Run.hs b/pkg/hs-hoon/lib/Language/Hoon/LL/Run.hs deleted file mode 100644 index 9ed0e312c4..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/LL/Run.hs +++ /dev/null @@ -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) diff --git a/pkg/hs-hoon/lib/Language/Hoon/LL/Types.hs b/pkg/hs-hoon/lib/Language/Hoon/LL/Types.hs deleted file mode 100644 index b49b21b1aa..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/LL/Types.hs +++ /dev/null @@ -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 diff --git a/pkg/hs-hoon/lib/Language/Hoon/Nock/Types.hs b/pkg/hs-hoon/lib/Language/Hoon/Nock/Types.hs deleted file mode 100644 index 014be2b6e7..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/Nock/Types.hs +++ /dev/null @@ -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)) diff --git a/pkg/hs-hoon/lib/Language/Hoon/SpecToBunt.hs b/pkg/hs-hoon/lib/Language/Hoon/SpecToBunt.hs deleted file mode 100644 index 3101174fc6..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/SpecToBunt.hs +++ /dev/null @@ -1,7 +0,0 @@ -module Language.Hoon.SpecToBunt (specToBunt) where - -import Prelude -import Language.Hoon.Types - -specToBunt :: Bool -> Spec -> Hoon -specToBunt = undefined diff --git a/pkg/hs-hoon/lib/Language/Hoon/SpecToMold.hs b/pkg/hs-hoon/lib/Language/Hoon/SpecToMold.hs deleted file mode 100644 index dc2ffb9b3c..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/SpecToMold.hs +++ /dev/null @@ -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" - diff --git a/pkg/hs-hoon/lib/Language/Hoon/Types.hs b/pkg/hs-hoon/lib/Language/Hoon/Types.hs deleted file mode 100644 index 1370f190b3..0000000000 --- a/pkg/hs-hoon/lib/Language/Hoon/Types.hs +++ /dev/null @@ -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 - diff --git a/pkg/hs-hoon/package.yaml b/pkg/hs-hoon/package.yaml deleted file mode 100644 index 9c8bc3dcb4..0000000000 --- a/pkg/hs-hoon/package.yaml +++ /dev/null @@ -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 diff --git a/stack.yaml b/stack.yaml index 7527acff66..5c3615502e 100644 --- a/stack.yaml +++ b/stack.yaml @@ -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