Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions core/avaleryar.cabal
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
cabal-version: 1.12

-- This file has been generated from package.yaml by hpack version 0.33.0.
-- This file has been generated from package.yaml by hpack version 0.34.4.
--
-- see: https://github.com/sol/hpack
--
-- hash: 30fac0c3b148d219353f8644d0c0934b9b681991e4892964c8bbf9aba9738fc7
-- hash: 98d84695e2ed9bf9a29be1f53517d51095cc126033cfa4bcfa0d713cee5f65d5

name: avaleryar
version: 0.0.1.1
Expand Down Expand Up @@ -39,6 +39,7 @@ library
, qq-literals
, template-haskell
, text
, vector
, wl-pprint-text
default-language: Haskell2010

Expand Down Expand Up @@ -67,6 +68,7 @@ test-suite avaleryar-tests
, hspec
, hspec-core
, text
, vector
default-language: Haskell2010

benchmark avaleryar-benchmarks
Expand All @@ -81,5 +83,6 @@ benchmark avaleryar-benchmarks
, base
, criterion
, text
, vector
, wl-pprint-text
default-language: Haskell2010
4 changes: 3 additions & 1 deletion core/bench/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,14 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE OverloadedLists #-}

module Main where

import Criterion.Main
import Data.Bool
import Data.Text (pack)
import qualified Data.Vector as Vector
import Text.PrettyPrint.Leijen.Text (displayTStrict, renderPretty, vcat, Pretty(..))

import Language.Avaleryar
Expand Down Expand Up @@ -135,7 +137,7 @@ tight n = do
-- @
parse :: Int -> Benchmark
parse n = go txt
where rule x = Rule (lit (rn x) vars) [Says (ARTerm (val $ T "application")) (lit (rn x <> "-body") vars) | _ <- [1..5]]
where rule x = Rule (lit (rn x) vars) (Vector.fromList [Says (ARTerm (val $ T "application")) (lit (rn x <> "-body") vars) | _ <- [1..5]])
rn x = pack ("rule-" <> show x)
vars = Var <$> [pack "x", "y", "z", "w"]
rs = [rule x | x <- [1..n]]
Expand Down
3 changes: 3 additions & 0 deletions core/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ library:
- qq-literals
- template-haskell
- text
- vector
- wl-pprint-text

tests:
Expand All @@ -36,6 +37,7 @@ tests:
- directory
- filepath
- text
- vector

benchmarks:
avaleryar-benchmarks:
Expand All @@ -48,3 +50,4 @@ benchmarks:
- criterion
- wl-pprint-text
- text
- vector
3 changes: 2 additions & 1 deletion core/src/Language/Avaleryar/ModeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import Data.Foldable
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Text (Text, pack)
import qualified Data.Vector as Vector
import Text.Megaparsec (sourcePosPretty)
import Text.PrettyPrint.Leijen.Text (Pretty(..), colon, squotes)

Expand Down Expand Up @@ -73,7 +74,7 @@ modeCheckRule :: Monad m => Rule RawVar -> ModeCheck m ()
modeCheckRule (Rule hd body) = traverse_ modeCheckBody body >> modeCheckHead hd
where modeCheckBody (ARNative assn `Says` Lit p bas) = do
Lit _ mas <- getNativeMode assn p
zipWithM_ modeCheckArg mas bas
Vector.zipWithM_ modeCheckArg mas bas
modeCheckBody (ARTerm aref `Says` Lit _ bas) = do
case aref of
Var v -> grounded v >>= bool (throwError $ FVInAssertionPosition v) (pure ())
Expand Down
15 changes: 10 additions & 5 deletions core/src/Language/Avaleryar/PDP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ import Data.List (stripPrefix)
import Data.Map (Map)
import Data.Text (Text, pack)
import qualified Data.Text as T
import Data.Vector (Vector)
import qualified Data.Vector as Vector
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import System.FilePath (stripExtension)
Expand Down Expand Up @@ -140,26 +142,29 @@ retractAssertion = modifyRulesDb . retractRuleAssertion

runDetailedQuery :: [Fact] -> Text -> [Term TextVar] -> PDP DetailedQueryResults
runDetailedQuery facts p args = do
answers <- runDetailedWith (insertApplicationAssertion facts) $ compileQuery "system" p args
answers <- runDetailedWith (insertApplicationAssertion facts) $ compileQuery "system" p (Vector.fromList args)
flip traverse answers $ \l -> do
traverse (throwError . VarInQueryResults . unEVar) l

runQuery :: [Fact] -> Text -> [Term TextVar] -> PDP QueryResults
runQuery facts p args = do
runQueryVector :: [Fact] -> Text -> Vector (Term TextVar) -> PDP QueryResults
runQueryVector facts p args = do
answers <- runAvaWith (insertApplicationAssertion facts) $ compileQuery "system" p args
flip traverse answers $ \l -> do
traverse (throwError . VarInQueryResults . unEVar) l

runQuery :: [Fact] -> Text -> [Term TextVar] -> PDP QueryResults
runQuery facts p args = runQueryVector facts p (Vector.fromList args)

runQuery' :: [Fact] -> Query -> PDP QueryResults
runQuery' facts (Lit (Pred p _) as) = runQuery facts p as
runQuery' facts (Lit (Pred p _) as) = runQueryVector facts p as

queryPretty :: [Fact] -> Text -> [Term TextVar] -> PDP ()
queryPretty facts p args = do
answers <- runQuery facts p args
liftIO $ mapM_ (putDoc . pretty . factToRule @TextVar) answers

testQuery :: [Fact] -> Query -> PDP ()
testQuery facts (Lit (Pred p _) as) = queryPretty facts p as
testQuery facts (Lit (Pred p _) as) = queryPretty facts p (Vector.toList as)

-- | Insert an @application@ assertion into a 'RulesDb' providing the given facts.
insertApplicationAssertion :: [Fact] -> RulesDb -> RulesDb
Expand Down
18 changes: 11 additions & 7 deletions core/src/Language/Avaleryar/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ import Data.Either (partitionEithers)
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
import Data.Vector (Vector)
import qualified Data.Vector as Vector
import Data.Void
import Language.Haskell.TH.Quote (QuasiQuoter)
import QQLiterals
Expand Down Expand Up @@ -67,7 +69,7 @@ value :: Parser Value
value = I <$> L.signed (pure ()) L.decimal
<|> T <$> stringLiteral
<|> T <$> sym -- unquoted symbols
<|> B <$> (string "#t" *> pure True <|> string "#f" *> pure False)
<|> B <$> (string "#t" *> pure True <|> string "#f" *> pure False)

ident :: Parser Text
ident = sym <?> "identifer"
Expand All @@ -84,7 +86,8 @@ lit :: Parser (Lit RawVar)
lit = label "literal" $ do
ftor <- ident
args <- concat <$> optional (parens (term `sepBy` comma))
pure $ Lit (Pred ftor (length args)) args
let argsVector = Vector.fromList args
pure $ Lit (Pred ftor (Vector.length argsVector)) argsVector

-- | A specialized version of 'lit' that fails faster for facts. Like 'rule' and unlike 'lit',
-- parses a trailing 'dot'.
Expand All @@ -93,14 +96,16 @@ fact = label "fact" $ do
ftor <- ident
args <- fmap Val <$> parens (value `sepBy` comma)
dot
pure $ Lit (Pred ftor (length args)) args
let argsVector = Vector.fromList args
pure $ Lit (Pred ftor (Vector.length argsVector)) argsVector

-- | Like 'fact', but without the trailing 'dot'. FIXME: Suck less.
fact' :: Parser Fact
fact' = label "fact" $ do
ftor <- ident
args <- fmap Val <$> parens (value `sepBy` comma)
pure $ Lit (Pred ftor (length args)) args
let argsVector = Vector.fromList args
pure $ Lit (Pred ftor (Vector.length argsVector)) argsVector

aref :: Parser (ARef RawVar)
aref = colon *> (ARNative <$> sym) <|> ARTerm <$> term
Expand All @@ -112,9 +117,9 @@ bodyLit :: Parser (BodyLit RawVar)
bodyLit = Says <$> (try (aref <* symbol "says") <|> currentAssertion) <*> lit

rule :: Parser (Rule RawVar)
rule = Rule <$> lit <*> (body <|> dot *> pure [])
rule = Rule <$> lit <*> (body <|> dot *> pure mempty)
where -- bodyLits = ( (try (term val *> symbol "says") *> lit val) <|> lit val) `sepBy1` comma
bodyLits = bodyLit `sepBy1` comma
bodyLits = Vector.fromList <$> bodyLit `sepBy1` comma
body = symbol ":-" *> label "rule body" bodyLits <* dot

directive :: Parser Directive
Expand Down Expand Up @@ -183,4 +188,3 @@ qry = qqLiteral queryQQParser 'queryQQParser

fct :: QuasiQuoter
fct = qqLiteral factQQParser 'factQQParser

33 changes: 19 additions & 14 deletions core/src/Language/Avaleryar/Semantics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
Expand Down Expand Up @@ -74,6 +75,8 @@ import Data.Map (Map)
import qualified Data.Map as Map
import Data.String
import Data.Text (Text, pack)
import Data.Vector (Vector, (!?))
import qualified Data.Vector as Vector
import Data.Void (vacuous)
import GHC.Clock (getMonotonicTime)
import GHC.Generics (Generic)
Expand Down Expand Up @@ -253,13 +256,12 @@ resolve (assn `Says` l@(Lit p as)) = do
resolver l
Lit p <$> traverse subst as


-- | A slightly safer version of @'zipWithM_' 'unifyTerm'@ that ensures its argument lists are the
-- same length.
unifyArgs :: [Term EVar] -> [Term EVar] -> Avaleryar ()
unifyArgs [] [] = pure ()
unifyArgs (x:xs) (y:ys) = unifyTerm x y >> unifyArgs xs ys
unifyArgs _ _ = empty
unifyArgs :: Vector (Term EVar) -> Vector (Term EVar) -> Avaleryar ()
unifyArgs ts1 ts2 = do
guard (Vector.length ts1 == Vector.length ts2)
Vector.zipWithM_ unifyTerm ts1 ts2

-- | NB: 'compilePred' doesn't look at the 'Pred' for any of the given rules, it assumes it was
-- given a query that applies, and that the rules it was handed are all for the same predicate.
Expand Down Expand Up @@ -288,7 +290,7 @@ emplaceCurrentAssertion assn (Rule l b) = Rule l (go <$> b)
where go (ARCurrent `Says` bl) = (ARTerm $ val assn) `Says` bl
go bl = bl

compileQuery :: String -> Text -> [Term TextVar] -> Avaleryar (Lit EVar)
compileQuery :: String -> Text -> Vector (Term TextVar) -> Avaleryar (Lit EVar)
compileQuery assn p args = resolve $ assn' `Says` (Lit (Pred p (length args)) (fmap (fmap (EVar (-1))) args))
where assn' = case assn of
(':':_) -> ARNative (pack assn)
Expand Down Expand Up @@ -320,7 +322,7 @@ class ToNative a where
-- list of 'Term's given. Usually, the list will only have one value in it, but it can have more
-- or fewer in the case of e.g., tuples. Implementations /must/ ground-out every variable in the
-- list, or the mode-checker will become unsound.
toNative :: a -> [Term EVar] -> Avaleryar ()
toNative :: a -> Vector (Term EVar) -> Avaleryar ()

-- | Probably this should be 'outMode' for each argument expected in the list of 'Term's in
-- 'toNative'.
Expand Down Expand Up @@ -388,12 +390,15 @@ instance (Valuable a, Valuable b, Valuable c, Valuable d, Valuable e, Valuable f
-- here to ensure that we actually get a value from the substitution so that 'fromValue' might
-- conceivably work.
instance (Valuable a, ToNative b) => ToNative (a -> b) where
toNative f (x:xs) = do
Val x' <- subst x -- mode checking should make this safe (because of the 'inMode' below)
case fromValue x' of
Just a -> toNative (f a) xs
Nothing -> empty
toNative _ _ = empty
toNative f xs =
case xs !? 0 of
Just x -> do
let rest = Vector.drop 1 xs
Val x' <- subst x -- mode checking should make this safe (because of the 'inMode' below)
case fromValue x' of
Just a -> toNative (f a) rest
Nothing -> empty
_ -> empty
inferMode = inMode : inferMode @b

-- | Executes the IO action and produces the result.
Expand All @@ -412,7 +417,7 @@ mkNativePred :: forall a. (ToNative a) => Text -> a -> NativePred
mkNativePred pn f = NativePred np moded
where np (Lit _ args) = toNative f args
modes = inferMode @a
moded = Lit (Pred pn $ length modes) (Var <$> modes)
moded = Lit (Pred pn $ length modes) (Vector.fromList (Var <$> modes))

-- TODO: Feels like I should be able to do this less manually, maybe?
mkNativeFact :: (Factual a) => a -> NativePred
Expand Down
26 changes: 16 additions & 10 deletions core/src/Language/Avaleryar/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,13 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ViewPatterns #-}

{-|

Expand Down Expand Up @@ -54,12 +56,17 @@ import Data.Map (Map)
import Data.String
import Data.Text (Text)
import qualified Data.Text as T
import Data.Vector (Vector)
import qualified Data.Vector as Vector
import Data.Void
import GHC.Generics (Generic)
import Text.Megaparsec (SourcePos(..), pos1, unPos)
import Text.PrettyPrint.Leijen.Text
(Doc, Pretty(..), brackets, colon, dot, empty, group, hsep, line, nest, parens, punctuate, space, vsep)

instance (Hashable a) => Hashable (Vector a) where
hashWithSalt salt = hashWithSalt salt . Vector.toList

data Value
= I Int
| T Text
Expand Down Expand Up @@ -103,17 +110,17 @@ instance Pretty v => Pretty (Term v) where

-- | A literal is identified by a 'Pred' and a list of 'Term's, where the arity in the 'Pred' is the
-- same as the length of the list of 'Term's in the argument list.
data Lit v = Lit Pred [Term v] deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)
data Lit v = Lit Pred (Vector (Term v)) deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (Lit v)
instance Hashable v => Hashable (Lit v)

instance Pretty v => Pretty (Lit v) where
pretty (Lit (Pred p _) as) = pretty p <> parens (hsep . punctuate "," $ fmap pretty as)
pretty (Lit (Pred p _) as) = pretty p <> parens (hsep . punctuate "," $ fmap pretty (Vector.toList as))

-- | Convenience constructor for 'Lit's.
lit :: Text -> [Term v] -> Lit v
lit pn as = Lit (Pred pn (length as)) as
lit pn as = Lit (Pred pn (length as)) (Vector.fromList as)

-- | A reference to an assertion may either statically denote a native assertion or appear as a
-- 'Term'.
Expand Down Expand Up @@ -145,17 +152,17 @@ instance Pretty v => Pretty (BodyLit v) where
pretty (aref `Says` l) = pretty aref <> space <> "says" <> space <> pretty l

-- | A rule has a head and a body made of 'BodyLit's.
data Rule v = Rule (Lit v) [BodyLit v]
data Rule v = Rule (Lit v) (Vector (BodyLit v))
deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (Rule v)
instance Hashable v => Hashable (Rule v)

instance Pretty v => Pretty (Rule v) where
pretty (Rule hd body) = pretty hd <> bodyDoc body <> dot <> line
where bodyDoc [] = empty
bodyDoc _ = space <> ":-"
<> group (nest 2 (line <> (vsep . punctuate "," $ fmap pretty body)))
pretty (Rule hd body) = pretty hd <> bodyDoc (Vector.toList body) <> dot <> line
where bodyDoc [] = empty
bodyDoc bodys = space <> ":-"
<> group (nest 2 (line <> (vsep . punctuate "," $ fmap pretty bodys)))

-- | Facts can be thought of as rules with no variables in the head and no body. Instead, we
-- represent them as 'Lit's with variables of type 'Void' to ensure they are facts by construction.
Expand All @@ -168,7 +175,7 @@ fact pn = lit pn . fmap val

-- | 'Fact's are vacuously 'Rule's.
factToRule :: Fact -> Rule v
factToRule fct = Rule (vacuous fct) []
factToRule fct = Rule (vacuous fct) mempty

-- | 'Directive's provide a side-channel for metadata to pass from assertion authors into an
-- implementation. They're intended to be extracted at parse time, and are /never/ considered
Expand Down Expand Up @@ -267,7 +274,6 @@ instance Valuable Value where
instance Valuable Text where
toValue = T
fromValue (T a) = Just a
fromValue _ = Nothing

instance Valuable Int where
toValue = I
Expand Down
Loading