{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

-- |
-- Module      :  Disco.Syntax.Prims
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- Concrete syntax for the prims (i.e. built-in constants) supported
-- by the language.
module Disco.Syntax.Prims (
  Prim (..),
  PrimInfo (..),
  primTable,
  toPrim,
  primMap,
) where

import GHC.Generics (Generic)
import Unbound.Generics.LocallyNameless

import Data.Map (Map)
import qualified Data.Map as M

import Data.Data (Data)
import Disco.Syntax.Operators

------------------------------------------------------------
-- Prims
------------------------------------------------------------

-- | Primitives, /i.e./ built-in constants.
data Prim where
  PrimUOp ::
    UOp ->
    -- | Unary operator
    Prim
  PrimBOp ::
    BOp ->
    -- | Binary operator
    Prim
  PrimLeft ::
    -- | Left injection into a sum type.
    Prim
  PrimRight ::
    -- | Right injection into a sum type.
    Prim
  PrimSqrt ::
    -- | Integer square root (@sqrt@)
    Prim
  PrimFloor ::
    -- | Floor of fractional type (@floor@)
    Prim
  PrimCeil ::
    -- | Ceiling of fractional type (@ceiling@)
    Prim
  PrimAbs ::
    -- | Absolute value (@abs@)
    Prim
  PrimPower ::
    -- | Power set (XXX or bag?)
    Prim
  PrimList ::
    -- | Container -> list conversion
    Prim
  PrimBag ::
    -- | Container -> bag conversion
    Prim
  PrimSet ::
    -- | Container -> set conversion
    Prim
  PrimB2C ::
    -- | bag -> set of counts conversion
    Prim
  PrimC2B ::
    -- | set of counts -> bag conversion
    Prim
  PrimUC2B ::
    -- | unsafe set of counts -> bag conversion
    --   that assumes all distinct
    Prim
  PrimMapToSet ::
    -- | Map k v -> Set (k × v)
    Prim
  PrimSetToMap ::
    -- | Set (k × v) -> Map k v
    Prim
  PrimSummary ::
    -- | Get Adjacency list of Graph
    Prim
  PrimVertex ::
    -- | Construct a graph Vertex
    Prim
  PrimEmptyGraph ::
    -- | Empty graph
    Prim
  PrimOverlay ::
    -- | Overlay two Graphs
    Prim
  PrimConnect ::
    -- | Connect Graph to another with directed edges
    Prim
  PrimInsert ::
    -- | Insert into map
    Prim
  PrimLookup ::
    -- | Get value associated with key in map
    Prim
  PrimEach ::
    -- | Each operation for containers
    Prim
  PrimReduce ::
    -- | Reduce operation for containers
    Prim
  PrimFilter ::
    -- | Filter operation for containers
    Prim
  PrimJoin ::
    -- | Monadic join for containers
    Prim
  PrimMerge ::
    -- | Generic merge operation for bags/sets
    Prim
  PrimIsPrime ::
    -- | Efficient primality test
    Prim
  PrimFactor ::
    -- | Factorization
    Prim
  PrimFrac ::
    -- | Turn a rational into a pair (num, denom)
    Prim
  PrimCrash ::
    -- | Crash
    Prim
  PrimUntil ::
    -- | @[x, y, z .. e]@
    Prim
  PrimHolds ::
    -- | Test whether a proposition holds
    Prim
  PrimLookupSeq ::
    -- | Lookup OEIS sequence
    Prim
  PrimExtendSeq ::
    -- | Extend OEIS sequence
    Prim
  deriving (Int -> Prim -> ShowS
[Prim] -> ShowS
Prim -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prim] -> ShowS
$cshowList :: [Prim] -> ShowS
show :: Prim -> String
$cshow :: Prim -> String
showsPrec :: Int -> Prim -> ShowS
$cshowsPrec :: Int -> Prim -> ShowS
Show, ReadPrec [Prim]
ReadPrec Prim
Int -> ReadS Prim
ReadS [Prim]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Prim]
$creadListPrec :: ReadPrec [Prim]
readPrec :: ReadPrec Prim
$creadPrec :: ReadPrec Prim
readList :: ReadS [Prim]
$creadList :: ReadS [Prim]
readsPrec :: Int -> ReadS Prim
$creadsPrec :: Int -> ReadS Prim
Read, Prim -> Prim -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prim -> Prim -> Bool
$c/= :: Prim -> Prim -> Bool
== :: Prim -> Prim -> Bool
$c== :: Prim -> Prim -> Bool
Eq, Eq Prim
Prim -> Prim -> Bool
Prim -> Prim -> Ordering
Prim -> Prim -> Prim
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Prim -> Prim -> Prim
$cmin :: Prim -> Prim -> Prim
max :: Prim -> Prim -> Prim
$cmax :: Prim -> Prim -> Prim
>= :: Prim -> Prim -> Bool
$c>= :: Prim -> Prim -> Bool
> :: Prim -> Prim -> Bool
$c> :: Prim -> Prim -> Bool
<= :: Prim -> Prim -> Bool
$c<= :: Prim -> Prim -> Bool
< :: Prim -> Prim -> Bool
$c< :: Prim -> Prim -> Bool
compare :: Prim -> Prim -> Ordering
$ccompare :: Prim -> Prim -> Ordering
Ord, forall x. Rep Prim x -> Prim
forall x. Prim -> Rep Prim x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Prim x -> Prim
$cfrom :: forall x. Prim -> Rep Prim x
Generic, Show Prim
AlphaCtx -> NthPatFind -> Prim -> Prim
AlphaCtx -> NamePatFind -> Prim -> Prim
AlphaCtx -> Perm AnyName -> Prim -> Prim
AlphaCtx -> Prim -> Prim -> Bool
AlphaCtx -> Prim -> Prim -> Ordering
Prim -> Bool
Prim -> All
Prim -> DisjointSet AnyName
Prim -> NthPatFind
Prim -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Prim -> f Prim
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Prim -> m (Prim, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Prim -> (Prim -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Prim -> Prim -> Ordering
$cacompare' :: AlphaCtx -> Prim -> Prim -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Prim -> m (Prim, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Prim -> m (Prim, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Prim -> (Prim -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Prim -> (Prim -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Prim -> Prim
$cswaps' :: AlphaCtx -> Perm AnyName -> Prim -> Prim
namePatFind :: Prim -> NamePatFind
$cnamePatFind :: Prim -> NamePatFind
nthPatFind :: Prim -> NthPatFind
$cnthPatFind :: Prim -> NthPatFind
isEmbed :: Prim -> Bool
$cisEmbed :: Prim -> Bool
isTerm :: Prim -> All
$cisTerm :: Prim -> All
isPat :: Prim -> DisjointSet AnyName
$cisPat :: Prim -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Prim -> Prim
$copen :: AlphaCtx -> NthPatFind -> Prim -> Prim
close :: AlphaCtx -> NamePatFind -> Prim -> Prim
$cclose :: AlphaCtx -> NamePatFind -> Prim -> Prim
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Prim -> f Prim
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Prim -> f Prim
aeq' :: AlphaCtx -> Prim -> Prim -> Bool
$caeq' :: AlphaCtx -> Prim -> Prim -> Bool
Alpha, Subst t, Typeable Prim
Prim -> DataType
Prim -> Constr
(forall b. Data b => b -> b) -> Prim -> Prim
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Prim -> u
forall u. (forall d. Data d => d -> u) -> Prim -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Prim -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Prim -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Prim
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Prim -> c Prim
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Prim)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Prim)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Prim -> m Prim
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Prim -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Prim -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Prim -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Prim -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Prim -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Prim -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Prim -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Prim -> r
gmapT :: (forall b. Data b => b -> b) -> Prim -> Prim
$cgmapT :: (forall b. Data b => b -> b) -> Prim -> Prim
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Prim)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Prim)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Prim)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Prim)
dataTypeOf :: Prim -> DataType
$cdataTypeOf :: Prim -> DataType
toConstr :: Prim -> Constr
$ctoConstr :: Prim -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Prim
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Prim
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Prim -> c Prim
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Prim -> c Prim
Data)

------------------------------------------------------------
-- Concrete syntax for prims
------------------------------------------------------------

-- | An info record for a single primitive name, containing the
--   primitive itself, its concrete syntax, and whether it is
--   "exposed", /i.e./ available to be used in the surface syntax of
--   the basic language.  Unexposed prims can only be referenced by
--   enabling the Primitives language extension and prefixing their
--   name by @$@.
data PrimInfo = PrimInfo
  { PrimInfo -> Prim
thePrim :: Prim
  , PrimInfo -> String
primSyntax :: String
  , PrimInfo -> Bool
primExposed :: Bool
  -- Is the prim available in the normal syntax of the language?
  --
  --   primExposed = True means that the bare primSyntax can be used
  --   in the surface syntax, and the prim will be pretty-printed as
  --   the primSyntax.
  --
  --   primExposed = False means that the only way to enter it is to
  --   enable the Primitives language extension and write a $
  --   followed by the primSyntax.  The prim will be pretty-printed with a $
  --   prefix.
  --
  --   In no case is a prim a reserved word.
  }

-- | A table containing a 'PrimInfo' record for every non-operator
--   'Prim' recognized by the language.
primTable :: [PrimInfo]
primTable :: [PrimInfo]
primTable =
  [ Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimLeft String
"left" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimRight String
"right" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo (UOp -> Prim
PrimUOp UOp
Not) String
"not" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimSqrt String
"sqrt" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimFloor String
"floor" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimCeil String
"ceiling" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimAbs String
"abs" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimPower String
"power" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimList String
"list" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimBag String
"bag" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimSet String
"set" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimB2C String
"bagCounts" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimC2B String
"bagFromCounts" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimUC2B String
"unsafeBagFromCounts" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimMapToSet String
"mapToSet" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimSetToMap String
"map" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimSummary String
"summary" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimVertex String
"vertex" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimEmptyGraph String
"emptyGraph" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimOverlay String
"overlay" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimConnect String
"connect" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimInsert String
"insert" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimLookup String
"lookup" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimEach String
"each" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimReduce String
"reduce" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimFilter String
"filter" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimJoin String
"join" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimMerge String
"merge" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimIsPrime String
"isPrime" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimFactor String
"factor" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimFrac String
"frac" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimCrash String
"crash" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimUntil String
"until" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimHolds String
"holds" Bool
True
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimLookupSeq String
"lookupSequence" Bool
False
  , Prim -> String -> Bool -> PrimInfo
PrimInfo Prim
PrimExtendSeq String
"extendSequence" Bool
False
  ]

-- | Find any exposed prims with the given name.
toPrim :: String -> [Prim]
toPrim :: String -> [Prim]
toPrim String
x = [Prim
p | PrimInfo Prim
p String
syn Bool
True <- [PrimInfo]
primTable, String
syn forall a. Eq a => a -> a -> Bool
== String
x]

-- | A convenient map from each 'Prim' to its info record.
primMap :: Map Prim PrimInfo
primMap :: Map Prim PrimInfo
primMap =
  forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
    [(Prim
p, PrimInfo
pinfo) | pinfo :: PrimInfo
pinfo@(PrimInfo Prim
p String
_ Bool
_) <- [PrimInfo]
primTable]