{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes           #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TemplateHaskell       #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Dense.TH
-- Copyright   :  (c) Christopher Chalmers
-- License     :  BSD3
--
-- Maintainer  :  Christopher Chalmers
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Contains QuasiQuotes and TemplateHaskell utilities for creating dense
-- arrays, stencils and fixed length vectors.
--
-- The parser for the QuasiQuotes is still a work in progress.
-----------------------------------------------------------------------------
module Data.Dense.TH
  ( -- * Creating dense arrays
    dense

    -- * Fixed length vector
  , v

    -- * Stencils
  , stencil

    -- ** Stencils from lists
  , ShapeLift (..)
  , mkStencilTH
  , mkStencilTHBy

  ) where

import           Control.Applicative          hiding (many, empty)
import           Control.Lens
import           Control.Monad
import           Data.Char
import           Data.Foldable                as F
import           Data.Function                (on)
import qualified Data.List                    as List
import           Data.Maybe
import           Data.Monoid                  (Endo)
import qualified Data.Vector                  as Vector
import           Language.Haskell.TH
import           Language.Haskell.TH.Quote
import           Language.Haskell.TH.Syntax
import           Linear
import qualified Linear.V                     as V
import           Text.ParserCombinators.ReadP
import qualified Text.Read.Lex                as Lex

import           Data.Dense.Generic          (empty, fromListInto_)
import           Data.Dense.Index
import           Data.Dense.Stencil

tupe :: [Exp] -> Exp
#if __GLASGOW_HASKELL__ <= 808
tupe = TupE
#else
tupe :: [Exp] -> Exp
tupe = [Maybe Exp] -> Exp
TupE ([Maybe Exp] -> Exp) -> ([Exp] -> [Maybe Exp]) -> [Exp] -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exp -> Maybe Exp) -> [Exp] -> [Maybe Exp]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Maybe Exp
forall a. a -> Maybe a
Just
#endif

-- | QuasiQuoter for producing a dense arrays using a custom parser.
--   Values are space separated, while also allowing infix expressions
--   (like @5/7@). If you want to apply a function, it should be done in
--   brackets. Supports 1D, 2D and 3D arrays.
--
--   The number of rows/columns must be consistent thought out the
--   array.
--
-- === __Examples__
--
--   - 1D arrays are of the following form form. Note these can be
--     used as 'V1', 'V2' or 'V3' arrays.
--
-- @
-- ['dense'| 5 -3 1 -3 5 |] :: ('R1' f, 'Vector.Vector' v a, 'Num' a) => 'Data.Dense.Array' v f a
-- @
--
--
--   - 2D arrays are of the following form. Note these can be used as
--     'V2' or 'V3' arrays.
--
-- @
-- chars :: 'Data.Dense.UArray' 'V2' 'Char'
-- chars :: ['dense'|
--   \'a\' \'b\' \'c\'
--   \'d\' \'e\' \'f\'
--   \'g\' \'h\' \'i\'
-- |]
-- @
--
--   - 3D arrays are of the following form. Note the order in which
--     'dense' formats the array. The array @a@ is such that @a ! 'V3'
--     x y z = "xyz"@
--
-- @
-- a :: 'Data.Dense.BArray' 'V3' 'String'
-- a = ['dense'|
--   "000" "100" "200"
--   "010" "110" "210"
--   "020" "120" "220"
--
--   "001" "101" "201"
--   "011" "111" "211"
--   "021" "121" "221"
--
--   "002" "102" "202"
--   "012" "112" "212"
--   "022" "122" "222"
-- |]
-- @
--
dense :: QuasiQuoter
dense :: QuasiQuoter
dense = QuasiQuoter :: (String -> Q Exp)
-> (String -> Q Pat)
-> (String -> Q Type)
-> (String -> Q [Dec])
-> QuasiQuoter
QuasiQuoter
  { quoteExp :: String -> Q Exp
quoteExp  = String -> Q Exp
parseDense
  , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"dense can't be used in pattern"
  , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"dense can't be used in type"
  , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"dense can't be used in dec"
  }

-- | List of expressions forming a stencil. To be either turned into
--   either a real list or an unfolded stencil.
parseDense :: String -> Q Exp
parseDense :: String -> Q Exp
parseDense String
str =
  case ([String] -> Either String [[Exp]])
-> [[String]] -> Either String [[[Exp]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String -> Either String [Exp])
-> [String] -> Either String [[Exp]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Either String [Exp]
parseLine) ((String -> [String]) -> [String] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map String -> [String]
lines [String]
ps) of
    Left String
err      -> String -> Q Exp
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right []      -> [| empty |]
    Right [[[Exp]
as]]  -> (Layout V1 -> [Exp] -> Q Exp) -> (Layout V1, [Exp]) -> Q Exp
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Layout V1 -> [Exp] -> Q Exp
forall (f :: * -> *). ShapeLift f => Layout f -> [Exp] -> Q Exp
mkArray ((Layout V1, [Exp]) -> Q Exp) -> (Layout V1, [Exp]) -> Q Exp
forall a b. (a -> b) -> a -> b
$ [Exp] -> (Layout V1, [Exp])
forall a. [a] -> (Layout V1, [a])
parse1D [Exp]
as
    Right [[[Exp]]
ass]   -> (Layout V2 -> [Exp] -> Q Exp) -> (Layout V2, [Exp]) -> Q Exp
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Layout V2 -> [Exp] -> Q Exp
forall (f :: * -> *). ShapeLift f => Layout f -> [Exp] -> Q Exp
mkArray ((Layout V2, [Exp]) -> Q Exp) -> (Layout V2, [Exp]) -> Q Exp
forall a b. (a -> b) -> a -> b
$ [[Exp]] -> (Layout V2, [Exp])
forall a. [[a]] -> (Layout V2, [a])
parse2D [[Exp]]
ass
    Right [[[Exp]]]
asss    -> (Layout V3 -> [Exp] -> Q Exp) -> (Layout V3, [Exp]) -> Q Exp
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Layout V3 -> [Exp] -> Q Exp
forall (f :: * -> *). ShapeLift f => Layout f -> [Exp] -> Q Exp
mkArray ((Layout V3, [Exp]) -> Q Exp) -> (Layout V3, [Exp]) -> Q Exp
forall a b. (a -> b) -> a -> b
$ [[[Exp]]] -> (Layout V3, [Exp])
forall a. [[[a]]] -> (Layout V3, [a])
parse3D [[[Exp]]]
asss
  where ps :: [String]
ps = String -> [String]
paragraphs String
str

-- | Split a string up into paragraphs separated by a new line. Extra
--   newlines inbetween paragraphs are stripped.
paragraphs :: String -> [String]
paragraphs :: String -> [String]
paragraphs = String -> String -> [String]
go [] (String -> [String]) -> (String -> String) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
strip where
  go :: String -> String -> [String]
go String
ps (Char
'\n':Char
'\n':String
xs) = [String -> String
forall a. [a] -> [a]
reverse String
ps] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> String -> [String]
go [] (String -> String
strip String
xs)
  go String
ps (Char
x:String
xs)         = String -> String -> [String]
go (Char
xChar -> String -> String
forall a. a -> [a] -> [a]
:String
ps) String
xs
  go [] []             = []
  go String
ps []             = [String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
strip String
ps]

  strip :: String -> String
strip = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\Char
x -> Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n' Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ')

-- Creating arrays -----------------------------------------------------

mkArray :: ShapeLift f => Layout f -> [Exp] -> Q Exp
mkArray :: Layout f -> [Exp] -> Q Exp
mkArray Layout f
l [Exp]
as = do
  Exp
lE <- Layout f -> Q Exp
forall (f :: * -> *) a. (ShapeLift f, Lift a) => f a -> Q Exp
liftShape' Layout f
l
  let fromListE :: Exp
fromListE = Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fromListInto_) Exp
lE
  Exp -> Q Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE Exp
fromListE ([Exp] -> Exp
ListE [Exp]
as)

------------------------------------------------------------------------
-- V n a
------------------------------------------------------------------------

-- | Type safe 'QuasiQuoter' for fixed length vectors 'V.V'. Values are
--   space separated. Can be used as expressions or patterns.
--
-- @
-- [v| x y z w q r |] :: 'V.V' 6 a
-- @
--
--   Note this requires @DataKinds@. Also requires @ViewPatterns@ if 'v'
--   is used as a pattern.
--
-- === __Examples__
--
-- @
-- >>> let a = [v| 1 2 3 4 5 |]
-- >>> :t a
-- a :: Num a => V 5 a
-- >>> a
-- V {toVector = [1,2,3,4,5]}
-- >>> let f [v| a b c d e |] = (a,b,c,d,e)
-- >>> :t f
-- f :: V 5 t -> (t, t, t, t, t)
-- >>> f a
-- (1,2,3,4,5)
-- @
--
-- Variables and infix expressions are also allowed. Negative values can
-- be expressed by a leading @-@ with a space before but no space
-- after.
--
-- @
-- >>> let b x = [v| 1\/x 2 \/ x (succ x)**2 x-2 x - 3 -x |]
-- >>> b Debug.SimpleReflect.a
-- V {toVector = [1 \/ a,2 \/ a,succ a**2,a - 2,a - 3,negate a]}
-- @
v :: QuasiQuoter
v :: QuasiQuoter
v = QuasiQuoter :: (String -> Q Exp)
-> (String -> Q Pat)
-> (String -> Q Type)
-> (String -> Q [Dec])
-> QuasiQuoter
QuasiQuoter
  { quoteExp :: String -> Q Exp
quoteExp  = String -> Q Exp
parseV
  , quotePat :: String -> Q Pat
quotePat  = String -> Q Pat
patternV
  , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"v can't be used as type"
  , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"v can't be used as dec"
  }

parseV :: String -> Q Exp
parseV :: String -> Q Exp
parseV String
s = case String -> Either String [Exp]
parseLine String
s of
  Right [Exp]
as ->
    let e :: Q Exp
e = Exp -> Q Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ [Exp] -> Exp
ListE [Exp]
as
        n :: Q Type
n = Type -> Q Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Q Type) -> (TyLit -> Type) -> TyLit -> Q Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyLit -> Type
LitT (TyLit -> Q Type) -> TyLit -> Q Type
forall a b. (a -> b) -> a -> b
$ Integer -> TyLit
NumTyLit (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ [Exp] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp]
as)
    in  [| (V.V :: Vector.Vector a -> V.V $n a) (Vector.fromList $e) |]
  Left String
err -> String -> Q Exp
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ String
"v: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err

------------------------------------------------------------------------
-- Stencils
------------------------------------------------------------------------

parseStencilLine :: String -> Either String [Maybe Exp]
parseStencilLine :: String -> Either String [Maybe Exp]
parseStencilLine String
s =
  case (([Maybe Exp], String) -> ([Maybe Exp], String) -> Ordering)
-> [([Maybe Exp], String)] -> [([Maybe Exp], String)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (([Maybe Exp], String) -> Int)
-> ([Maybe Exp], String)
-> ([Maybe Exp], String)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> (([Maybe Exp], String) -> String)
-> ([Maybe Exp], String)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Maybe Exp], String) -> String
forall a b. (a, b) -> b
snd)) [([Maybe Exp], String)]
rs of
    ([Maybe Exp]
xs,String
"") : [([Maybe Exp], String)]
_ -> [Maybe Exp] -> Either String [Maybe Exp]
forall a b. b -> Either a b
Right [Maybe Exp]
xs
    ([Maybe Exp]
_ , String
x) : [([Maybe Exp], String)]
_ -> String -> Either String [Maybe Exp]
forall a b. a -> Either a b
Left (String -> Either String [Maybe Exp])
-> String -> Either String [Maybe Exp]
forall a b. (a -> b) -> a -> b
$ String
"parse error on input " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. [a] -> a
head (String -> [String]
words String
x)
    [([Maybe Exp], String)]
_           -> String -> Either String [Maybe Exp]
forall a b. a -> Either a b
Left String
"no parse"
  where
    rs :: [([Maybe Exp], String)]
rs = ReadP [Maybe Exp] -> ReadS [Maybe Exp]
forall a. ReadP a -> ReadS a
readP_to_S (ReadP (Maybe Exp) -> ReadP [Maybe Exp]
forall a. ReadP a -> ReadP [a]
many (ReadP (Maybe Exp) -> ReadP [Maybe Exp])
-> ReadP (Maybe Exp) -> ReadP [Maybe Exp]
forall a b. (a -> b) -> a -> b
$ ReadP (Maybe Exp)
mExp ReadP (Maybe Exp) -> ReadP () -> ReadP (Maybe Exp)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces) String
s
    mExp :: ReadP (Maybe Exp)
mExp = (Exp -> Maybe Exp) -> ReadP Exp -> ReadP (Maybe Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Exp -> Maybe Exp
forall a. a -> Maybe a
Just ReadP Exp
noAppExpression ReadP (Maybe Exp) -> ReadP (Maybe Exp) -> ReadP (Maybe Exp)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReadP (Maybe Exp)
forall a. ReadP (Maybe a)
skip
    skip :: ReadP (Maybe a)
skip = do
      Lex.Ident String
"_" <- ReadP Lexeme
Lex.lex
      Maybe a -> ReadP (Maybe a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing

-- | List of expressions forming a stencil. To be either turned into
--   either a real list or an unfolded stencil.
parseStencil :: String -> Q Exp
parseStencil :: String -> Q Exp
parseStencil String
str =
  case ([String] -> Either String [[Maybe Exp]])
-> [[String]] -> Either String [[[Maybe Exp]]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String -> Either String [Maybe Exp])
-> [String] -> Either String [[Maybe Exp]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Either String [Maybe Exp]
parseStencilLine) ((String -> [String]) -> [String] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map String -> [String]
lines [String]
ps) of
    Left String
err      -> String -> Q Exp
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right []      -> [| mkStencil [] |]
    Right [[[Maybe Exp]
as]]  -> (Layout V1 -> [Maybe Exp] -> Q Exp)
-> (Layout V1, [Maybe Exp]) -> Q Exp
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Layout V1 -> [Maybe Exp] -> Q Exp
forall (f :: * -> *).
ShapeLift f =>
Layout f -> [Maybe Exp] -> Q Exp
mkStencilE ((Layout V1, [Maybe Exp]) -> Q Exp)
-> (Layout V1, [Maybe Exp]) -> Q Exp
forall a b. (a -> b) -> a -> b
$ [Maybe Exp] -> (Layout V1, [Maybe Exp])
forall a. [a] -> (Layout V1, [a])
parse1D [Maybe Exp]
as
    Right [[[Maybe Exp]]
ass]   -> (Layout V2 -> [Maybe Exp] -> Q Exp)
-> (Layout V2, [Maybe Exp]) -> Q Exp
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Layout V2 -> [Maybe Exp] -> Q Exp
forall (f :: * -> *).
ShapeLift f =>
Layout f -> [Maybe Exp] -> Q Exp
mkStencilE ((Layout V2, [Maybe Exp]) -> Q Exp)
-> (Layout V2, [Maybe Exp]) -> Q Exp
forall a b. (a -> b) -> a -> b
$ [[Maybe Exp]] -> (Layout V2, [Maybe Exp])
forall a. [[a]] -> (Layout V2, [a])
parse2D [[Maybe Exp]]
ass
    Right [[[Maybe Exp]]]
asss    -> (Layout V3 -> [Maybe Exp] -> Q Exp)
-> (Layout V3, [Maybe Exp]) -> Q Exp
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Layout V3 -> [Maybe Exp] -> Q Exp
forall (f :: * -> *).
ShapeLift f =>
Layout f -> [Maybe Exp] -> Q Exp
mkStencilE ((Layout V3, [Maybe Exp]) -> Q Exp)
-> (Layout V3, [Maybe Exp]) -> Q Exp
forall a b. (a -> b) -> a -> b
$ [[[Maybe Exp]]] -> (Layout V3, [Maybe Exp])
forall a. [[[a]]] -> (Layout V3, [a])
parse3D [[[Maybe Exp]]]
asss
  where ps :: [String]
ps = String -> [String]
paragraphs String
str

mkStencilE :: ShapeLift f => Layout f -> [Maybe Exp] -> Q Exp
mkStencilE :: Layout f -> [Maybe Exp] -> Q Exp
mkStencilE Layout f
l [Maybe Exp]
as = do
  Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Int -> Bool) -> Layout f -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
F.any Int -> Bool
forall a. Integral a => a -> Bool
even Layout f
l) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ String -> Q ()
reportWarning
    String
"stencil has an even size in some dimension, the centre element may be incorrect"

  let ixes :: [Layout f]
ixes = (Layout f -> Layout f) -> [Layout f] -> [Layout f]
forall a b. (a -> b) -> [a] -> [b]
map (Layout f -> Layout f -> Layout f
forall (f :: * -> *) a. (Additive f, Num a) => f a -> f a -> f a
^-^ (Int -> Int) -> Layout f -> Layout f
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Layout f
l) (Getting (Endo [Layout f]) (Layout f) (Layout f)
-> Layout f -> [Layout f]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Layout f]) (Layout f) (Layout f)
forall (f :: * -> *).
Shape f =>
IndexedFold Int (Layout f) (Layout f)
shapeIndexes Layout f
l)
      -- indexes zipped with expressions, discarding 'Nothing's
      xs :: [(Layout f, Exp)]
xs = ((Layout f, Maybe Exp) -> Maybe (Layout f, Exp))
-> [(Layout f, Maybe Exp)] -> [(Layout f, Exp)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (LensLike
  (WrappedMonad Maybe)
  (Layout f, Maybe Exp)
  (Layout f, Exp)
  (Maybe Exp)
  Exp
-> (Layout f, Maybe Exp) -> Maybe (Layout f, Exp)
forall (m :: * -> *) s t b.
LensLike (WrappedMonad m) s t (m b) b -> s -> m t
sequenceOf LensLike
  (WrappedMonad Maybe)
  (Layout f, Maybe Exp)
  (Layout f, Exp)
  (Maybe Exp)
  Exp
forall s t a b. Field2 s t a b => Lens s t a b
_2) ([Layout f] -> [Maybe Exp] -> [(Layout f, Maybe Exp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Layout f]
ixes [Maybe Exp]
as)

  (Exp -> Q Exp) -> [(Layout f, Exp)] -> Q Exp
forall (f :: * -> *) a.
ShapeLift f =>
(a -> Q Exp) -> [(f Int, a)] -> Q Exp
mkStencilTHBy Exp -> Q Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Layout f, Exp)]
xs

-- | QuasiQuoter for producing a static stencil definition. This is a
--   versatile parser for 1D, 2D and 3D stencils. The parsing is similar
--   to 'dense' but 'stencil' also supports @_@, which means ignore this
--   element. Also, stencils should have an odd length in all dimensions
--   so there is always a center element (which is used as 'zero').
--
-- === __Examples__
--
--     - 1D stencils are of the form
--
-- @
-- ['stencil'| 5 -3 1 -3 5 |] :: 'Num' a => 'Stencil' 'V1' a
-- @
--
--     - 2D stencils are of the form
--
-- @
-- myStencil2 :: 'Num' a => 'Stencil' 'V2' a
-- myStencil2 = ['stencil'|
--   0 1 0
--   1 0 1
--   0 1 0
-- |]
-- @
--
--     - 3D stencils have gaps between planes.
--
-- @
-- myStencil3 :: 'Fractional' a => 'Stencil' 'V3' a
-- myStencil3 :: ['stencil'|
--   1\/20 3\/10 1\/20
--   3\/10  1   3\/10
--   1\/20 3\/10 1\/20
--
--   3\/10  1   3\/10
--    1    _    1
--   3\/10  1   3\/10
--
--   1\/20 3\/10 1\/20
--   3\/10  1   3\/10
--   1\/20 3\/10 1\/20
-- |]
-- @
--
--  Variables can also be used
--
-- @
-- myStencil2' :: a -> a -> a -> 'Stencil' 'V2' a
-- myStencil2' a b c = ['stencil'|
--   c b c
--   b a b
--   c b c
-- |]
-- @
--
--
stencil :: QuasiQuoter
stencil :: QuasiQuoter
stencil = QuasiQuoter :: (String -> Q Exp)
-> (String -> Q Pat)
-> (String -> Q Type)
-> (String -> Q [Dec])
-> QuasiQuoter
QuasiQuoter
  { quoteExp :: String -> Q Exp
quoteExp  = String -> Q Exp
parseStencil
  , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall a. HasCallStack => String -> a
error String
"stencil can't be used in pattern"
  , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall a. HasCallStack => String -> a
error String
"stencil can't be used in type"
  , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error String
"stencil can't be used in dec"
  }

-- | Construct a 'Stencil' by unrolling the list at compile time. For
--   example
--
-- @
-- 'ifoldr' f b $('mkStencilTH' [('V1' (-1), 5), ('V1' 0, 3), ('V1' 1, 5)])
-- @
--
--   will be get turned into
--
-- @
-- f ('V1' (-1)) 5 (f ('V1' 0) 3 (f ('V1' 1) 5 b))
-- @
--
--   at compile time. Since there are no loops and all target indexes
--   are known at compile time, this can lead to more optimisations and
--   faster execution times. This can lead to around a 2x speed up
--   compared to folding over unboxed vectors.
--
-- @
-- myStencil = $('mkStencilTH' (as :: [(f 'Int', a)])) :: 'Stencil' f a
-- @
mkStencilTH :: (ShapeLift f, Lift a) => [(f Int, a)] -> Q Exp
mkStencilTH :: [(f Int, a)] -> Q Exp
mkStencilTH = (a -> Q Exp) -> [(f Int, a)] -> Q Exp
forall (f :: * -> *) a.
ShapeLift f =>
(a -> Q Exp) -> [(f Int, a)] -> Q Exp
mkStencilTHBy a -> Q Exp
forall t. Lift t => t -> Q Exp
lift

-- | 'mkStencilTH' with a custom 'lift' function for @a@.
mkStencilTHBy :: ShapeLift f => (a -> Q Exp) -> [(f Int, a)] -> Q Exp
mkStencilTHBy :: (a -> Q Exp) -> [(f Int, a)] -> Q Exp
mkStencilTHBy a -> Q Exp
aLift [(f Int, a)]
as = do
  -- See Note [mkName-capturing]
  Name
f <- String -> Q Name
newName String
"mkStencilTHBy_f"
  Name
b <- String -> Q Name
newName String
"mkStencilTHBy_b"
  let appF :: (f a, a) -> Exp -> Q Exp
appF (f a
i,a
a) Exp
e = do
        Exp
iE <- f a -> Q Exp
forall (f :: * -> *) a. (ShapeLift f, Lift a) => f a -> Q Exp
liftShape' f a
i
        Exp
aE <- a -> Q Exp
aLift a
a
        Exp -> Q Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
f) Exp
iE) Exp
aE) Exp
e

  Exp
e <- ((f Int, a) -> Exp -> Q Exp) -> Exp -> [(f Int, a)] -> Q Exp
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (f Int, a) -> Exp -> Q Exp
forall (f :: * -> *) a.
(ShapeLift f, Lift a) =>
(f a, a) -> Exp -> Q Exp
appF (Name -> Exp
VarE Name
b) [(f Int, a)]
as
  Exp -> Q Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'Stencil) ([Pat] -> Exp -> Exp
LamE [Name -> Pat
VarP Name
f,Name -> Pat
VarP Name
b] Exp
e)

{-
~~~~ Note [mkName-capturing]

Since 'newName' will capture any other names below it with the same
name. So if we simply used @newName "b"@, [stencil| a b c |] where
a=1; b=2; c=3 would convert @b@ to @b_a5y0@ (or w/e the top level b
is) and fail. To prevent this I've used a name that's unlikely
conflict.

Another solution would be to use lookupValueName on all variables.
But this would either require traversing over all 'Name's in every
'Exp' (shown below) or parse in the Q monad.

-- | Lookup and replace all names made with 'mkName' using
--   'lookupValueName'; failing if not in scope.
replaceMkName :: Exp -> Q Exp
replaceMkName = template f where
  f (Name (OccName s) NameS) =
    lookupValueName s >>= \case
      Just nm -> pure nm
      -- Sometimes a variable may not be in scope yet because it's
      -- generated in a TH splice that hasn't been run yet.
      Nothing -> fail $ "Not in scope: ‘" ++ s ++ "’"
  f nm = pure nm

-}

------------------------------------------------------------------------
-- Parsing expressions
------------------------------------------------------------------------

parseLine :: String -> Either String [Exp]
parseLine :: String -> Either String [Exp]
parseLine String
s =
  case (([Exp], String) -> ([Exp], String) -> Ordering)
-> [([Exp], String)] -> [([Exp], String)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (([Exp], String) -> Int)
-> ([Exp], String)
-> ([Exp], String)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> (([Exp], String) -> String) -> ([Exp], String) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Exp], String) -> String
forall a b. (a, b) -> b
snd)) [([Exp], String)]
rs of
    ([Exp]
xs,String
"") : [([Exp], String)]
_ -> [Exp] -> Either String [Exp]
forall a b. b -> Either a b
Right [Exp]
xs
    ([Exp]
_ , String
x) : [([Exp], String)]
_ -> String -> Either String [Exp]
forall a b. a -> Either a b
Left (String -> Either String [Exp]) -> String -> Either String [Exp]
forall a b. (a -> b) -> a -> b
$ String
"parse error on input " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. [a] -> a
head (String -> [String]
words String
x)
    [([Exp], String)]
_           -> String -> Either String [Exp]
forall a b. a -> Either a b
Left String
"no parse"
  where
    rs :: [([Exp], String)]
rs = ReadP [Exp] -> ReadS [Exp]
forall a. ReadP a -> ReadS a
readP_to_S (ReadP Exp -> ReadP [Exp]
forall a. ReadP a -> ReadP [a]
many ReadP Exp
noAppExpression ReadP [Exp] -> ReadP () -> ReadP [Exp]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces) String
s

-- | Fail the parser if the next non-space is a @-@ directly followed by
--   a non-space.
closeNegateFail :: ReadP ()
closeNegateFail :: ReadP ()
closeNegateFail = do
  String
s <- ReadP String
look
  case String
s of
    Char
' ' : String
s' -> case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
s' of
                  Char
'-' : Char
c : String
_ -> if Char -> Bool
isSpace Char
c then () -> ReadP ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () else ReadP ()
forall a. ReadP a
pfail
                  String
_           -> () -> ReadP ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    String
_        -> () -> ReadP ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | If there is a space before but not after a @-@, it is treated as a
--   separate expression.
--
-- @
-- "1 2 -3 4"        -> [1, 2, -3, 4]
-- "1 2 - 3 4"       -> [1, -1, 4]
-- "1 2-3 4"         -> [1, -1, 4]
-- "11 -3/2  -3/2 4" -> [1, -1, 4]
-- "1 -3/2 4"        -> [1.0,-1.5,4.0]
-- @
noAppExpression :: ReadP Exp
noAppExpression :: ReadP Exp
noAppExpression = do
  Exp
aE <- Bool -> ReadP Exp
anExpr Bool
True

  Exp -> ReadP Exp -> ReadP Exp
forall a. a -> ReadP a -> ReadP a
option Exp
aE (ReadP Exp -> ReadP Exp) -> ReadP Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ do
    ReadP ()
closeNegateFail
    Exp
i  <- ReadP Exp
infixExp
    Exp
bE <- ReadP Exp
noAppExpression
    Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp -> Exp
UInfixE Exp
aE Exp
i Exp
bE

-- | Parse an express without any top level application. Infix functions
--   are still permitted.
--
--   This is only a small subset of the full haskell syntax. The
--   following syntax is supported:
--
--     - Variables/constructors: @a@, @'Just'@ etc.
--     - Numbers: @3@, @-6@, @7.8@, @1e-6@, @0x583fa@
--     - Parenthesis/tuples: @()@ @(f a)@, @(a,b)@
--     - Lists
--     - Strings
--     - Function application
--     - Infix operators: symbols (@+@, @/@ etc.) and blackticked (like @`mod`@)
--
--   More advanced haskell syntax are not yet supported:
--
--     - let bindings
--     - lambdas
--     - partial infix application (+) (1+) (+2)
--     - type signatures
--     - comments
--
--   This could be replaced by haskell-src-meta but since I want a
--   custom parser for 'noAppExpression' it doesn't seem worth the extra
--   dependencies.
expression :: ReadP Exp
expression :: ReadP Exp
expression = do
  Exp
f    <- Bool -> ReadP Exp
anExpr Bool
True
  [Exp]
args <- ReadP Exp -> ReadP [Exp]
forall a. ReadP a -> ReadP [a]
many (Bool -> ReadP Exp
anExpr Bool
False)
  let aE :: Exp
aE = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl Exp -> Exp -> Exp
AppE Exp
f [Exp]
args

  Exp -> ReadP Exp -> ReadP Exp
forall a. a -> ReadP a -> ReadP a
option Exp
aE (ReadP Exp -> ReadP Exp) -> ReadP Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ do
    -- if the next lex isn't a symbol, we move on to the next statement
    Exp
i  <- ReadP Exp
infixExp
    Exp
bE <- ReadP Exp
expression
    Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp -> Exp
UInfixE Exp
aE Exp
i Exp
bE

-- | Parse an infix expression. Either a symbol or a name wrapped in @`@.
infixExp :: ReadP Exp
infixExp :: ReadP Exp
infixExp = do
  Lexeme
a <- ReadP Lexeme
Lex.lex
  case Lexeme
a of
    Lex.Symbol String
s -> Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ String -> Exp
symbol String
s
    Lex.Punc String
"`" -> do
      Lex.Ident String
x  <- ReadP Lexeme
Lex.lex
      Lex.Punc String
"`" <- ReadP Lexeme
Lex.lex
      String -> ReadP Exp
ident String
x
    Lexeme
_            -> ReadP Exp
forall a. ReadP a
pfail

-- Lexing --------------------------------------------------------------

-- | Parse a single expression.
anExpr
  :: Bool      -- ^ Allow a leading @-@ to mean 'negate'
  -> ReadP Exp
anExpr :: Bool -> ReadP Exp
anExpr Bool
new = do
  Lexeme
a <- ReadP Lexeme
Lex.lex
  case Lexeme
a of
    Lex.Char Char
c   -> Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Lit -> Exp
LitE (Char -> Lit
CharL Char
c)
    Lex.String String
s -> Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Lit -> Exp
LitE (String -> Lit
StringL String
s)
    Lex.Punc String
s   -> String -> ReadP Exp
punc String
s
    Lex.Ident String
s  -> String -> ReadP Exp
ident String
s
    Lex.Symbol String
s -> if Bool
new then String -> ReadP Exp
prefix String
s else ReadP Exp
forall a. ReadP a
pfail
    Lex.Number Number
n -> Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Lit -> Exp
LitE (Number -> Lit
number Number
n)
    Lexeme
Lex.EOF      -> ReadP Exp
forall a. ReadP a
pfail

-- | Convert a name to an expression.
ident :: String -> ReadP Exp
ident :: String -> ReadP Exp
ident String
"_"                 = ReadP Exp
forall a. ReadP a
pfail
ident s :: String
s@(Char
x:String
_) | Char -> Bool
isUpper Char
x = Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
ConE (String -> Name
mkName String
s)
ident String
s                   = Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
VarE (String -> Name
mkName String
s)

-- | Convert a symbol to an expression.
symbol :: String -> Exp
symbol :: String -> Exp
symbol s :: String
s@(Char
':':String
_) = Name -> Exp
ConE (String -> Name
mkName String
s)
symbol String
s         = Name -> Exp
VarE (String -> Name
mkName String
s)

-- | Parse from some punctuation.
punc :: String -> ReadP Exp
punc :: String -> ReadP Exp
punc = \case
  -- parenthesis / tuples
  String
"(" -> do [Exp]
as           <- ReadP Exp
expression ReadP Exp -> ReadP () -> ReadP [Exp]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
`sepBy` ReadP ()
comma
            Lex.Punc String
")" <- ReadP Lexeme
Lex.lex
            Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ [Exp] -> Exp
tupe [Exp]
as
  -- lists
  String
"[" -> do [Exp]
as           <- ReadP Exp
expression ReadP Exp -> ReadP () -> ReadP [Exp]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
`sepBy` ReadP ()
comma
            Lex.Punc String
"]" <- ReadP Lexeme
Lex.lex
            Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ [Exp] -> Exp
ListE [Exp]
as
  String
_   -> ReadP Exp
forall a. ReadP a
pfail

prefix :: String -> ReadP Exp
prefix :: String -> ReadP Exp
prefix String
"-" = do
  Exp
e <- Bool -> ReadP Exp
anExpr Bool
False
  Exp -> ReadP Exp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> ReadP Exp) -> Exp -> ReadP Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'negate) Exp
e
prefix String
_   = ReadP Exp
forall a. ReadP a
pfail

comma :: ReadP ()
comma :: ReadP ()
comma = do
  Lex.Punc String
"," <- ReadP Lexeme
Lex.lex
  () -> ReadP ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Turn a 'Number' into a literal 'Integer' if possible, otherwise
--   make a literal `Rational`.
number :: Lex.Number -> Lit
number :: Number -> Lit
number Number
n =
  Lit -> (Integer -> Lit) -> Maybe Integer -> Lit
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Rational -> Lit
RationalL (Rational -> Lit) -> Rational -> Lit
forall a b. (a -> b) -> a -> b
$ Number -> Rational
Lex.numberToRational Number
n)
        Integer -> Lit
IntegerL
        (Number -> Maybe Integer
Lex.numberToInteger Number
n)

------------------------------------------------------------------------
-- Parsing patterns
------------------------------------------------------------------------

patternV :: String -> Q Pat
patternV :: String -> Q Pat
patternV String
s = do
  case String -> Either String [Pat]
parsePattern String
s of
    Left String
err -> String -> Q Pat
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err
    Right [Pat]
pats -> do
      Exp
fE <- Int -> Q Exp
vTuple ([Pat] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pat]
pats)
      Pat -> Q Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> Q Pat) -> Pat -> Q Pat
forall a b. (a -> b) -> a -> b
$ Exp -> Pat -> Pat
ViewP Exp
fE ([Pat] -> Pat
TupP [Pat]
pats)

parsePattern :: String -> Either String [Pat]
parsePattern :: String -> Either String [Pat]
parsePattern String
s =
  case (([Pat], String) -> ([Pat], String) -> Ordering)
-> [([Pat], String)] -> [([Pat], String)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (([Pat], String) -> Int)
-> ([Pat], String)
-> ([Pat], String)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> (([Pat], String) -> String) -> ([Pat], String) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Pat], String) -> String
forall a b. (a, b) -> b
snd)) [([Pat], String)]
rs of
    ([Pat]
xs,String
"") : [([Pat], String)]
_ -> [Pat] -> Either String [Pat]
forall a b. b -> Either a b
Right [Pat]
xs
    ([Pat]
_ , String
x) : [([Pat], String)]
_ -> String -> Either String [Pat]
forall a b. a -> Either a b
Left (String -> Either String [Pat]) -> String -> Either String [Pat]
forall a b. (a -> b) -> a -> b
$ String
"parse error on input " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. [a] -> a
head (String -> [String]
words String
x)
    [([Pat], String)]
_           -> String -> Either String [Pat]
forall a b. a -> Either a b
Left String
"no parse"
  where rs :: [([Pat], String)]
rs = ReadP [Pat] -> ReadS [Pat]
forall a. ReadP a -> ReadS a
readP_to_S (ReadP Pat -> ReadP [Pat]
forall a. ReadP a -> ReadP [a]
many ReadP Pat
pattern ReadP [Pat] -> ReadP () -> ReadP [Pat]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReadP ()
skipSpaces) String
s

pattern :: ReadP Pat
pattern :: ReadP Pat
pattern = do
  Lexeme
a <- ReadP Lexeme
Lex.lex
  case Lexeme
a of
    Lex.Char Char
c   -> Pat -> ReadP Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> ReadP Pat) -> Pat -> ReadP Pat
forall a b. (a -> b) -> a -> b
$ Lit -> Pat
LitP (Char -> Lit
CharL Char
c)
    Lex.String String
s -> Pat -> ReadP Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> ReadP Pat) -> Pat -> ReadP Pat
forall a b. (a -> b) -> a -> b
$ Lit -> Pat
LitP (String -> Lit
StringL String
s)
    Lex.Punc String
s   -> String -> ReadP Pat
puncP String
s
    Lex.Ident String
n  -> Pat -> ReadP Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> ReadP Pat) -> Pat -> ReadP Pat
forall a b. (a -> b) -> a -> b
$ String -> Pat
identP String
n
    Lex.Symbol String
s -> String -> ReadP Pat
prefixP String
s
    Lex.Number Number
n -> Pat -> ReadP Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> ReadP Pat) -> Pat -> ReadP Pat
forall a b. (a -> b) -> a -> b
$ Lit -> Pat
LitP (Number -> Lit
number Number
n)
    Lexeme
Lex.EOF      -> ReadP Pat
forall a. ReadP a
pfail

-- | Convert a name to an expression.
identP :: String -> Pat
identP :: String -> Pat
identP String
"_"                 = Pat
WildP
identP s :: String
s@(Char
x:String
_) | Char -> Bool
isUpper Char
x = Name -> [Pat] -> Pat
ConP (String -> Name
mkName String
s) []
identP String
s                   = Name -> Pat
VarP (String -> Name
mkName String
s)

-- | Parse from some punctuation.
puncP :: String -> ReadP Pat
puncP :: String -> ReadP Pat
puncP = \case
  String
"~" -> Pat -> Pat
TildeP (Pat -> Pat) -> ReadP Pat -> ReadP Pat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Pat
pattern

  String
"(" -> do [Pat]
as           <- ReadP Pat
pattern ReadP Pat -> ReadP () -> ReadP [Pat]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
`sepBy` ReadP ()
comma
            Lex.Punc String
")" <- ReadP Lexeme
Lex.lex
            Pat -> ReadP Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> ReadP Pat) -> Pat -> ReadP Pat
forall a b. (a -> b) -> a -> b
$ [Pat] -> Pat
TupP [Pat]
as

  String
"[" -> do [Pat]
as           <- ReadP Pat
pattern ReadP Pat -> ReadP () -> ReadP [Pat]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
`sepBy` ReadP ()
comma
            Lex.Punc String
"]" <- ReadP Lexeme
Lex.lex
            Pat -> ReadP Pat
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> ReadP Pat) -> Pat -> ReadP Pat
forall a b. (a -> b) -> a -> b
$ [Pat] -> Pat
ListP [Pat]
as
  String
_   -> ReadP Pat
forall a. ReadP a
pfail

prefixP :: String -> ReadP Pat
prefixP :: String -> ReadP Pat
prefixP String
"!" = do
  Char
c:String
_ <- ReadP String
look
  Bool -> ReadP () -> ReadP ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Char -> Bool
isSpace Char
c) ReadP ()
forall a. ReadP a
pfail
  Pat -> Pat
BangP (Pat -> Pat) -> ReadP Pat -> ReadP Pat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Pat
pattern
prefixP String
"~" = Pat -> Pat
TildeP (Pat -> Pat) -> ReadP Pat -> ReadP Pat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Pat
pattern
prefixP String
_   = ReadP Pat
forall a. ReadP a
pfail

-- | Create an expression for converting a (V n a) to an n-tuple.
vTuple :: Int -> Q Exp
vTuple :: Int -> Q Exp
vTuple Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
62 = String -> Q Exp
forall a. HasCallStack => String -> a
error String
"max supported length is 62 for v pattern"
  | Bool
otherwise = do
      Name
vN <- String -> Q Name
newName String
"v"
      let idx :: Int -> Exp
idx Int
i = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'Vector.unsafeIndex) (Name -> Exp
VarE Name
vN)) (Int -> Exp
intE Int
i)
      let xs :: Exp
xs = [Exp] -> Exp
tupe ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ (Int -> Exp) -> [Int] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Exp
idx [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
      Name
a <- String -> Q Name
newName String
"a"
      let tup :: Type
tup = (Type -> Type) -> Type -> [Type]
forall a. (a -> a) -> a -> [a]
iterate (\Type
x -> Type -> Type -> Type
AppT Type
x (Name -> Type
VarT Name
a)) (Int -> Type
TupleT Int
n) [Type] -> Int -> Type
forall a. [a] -> Int -> a
!! Int
n
          typ :: Type
typ = [TyVarBndr] -> [Type] -> Type -> Type
ForallT [Name -> TyVarBndr
PlainTV Name
a] []
                  (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT Type
ArrowT (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT (Name -> Type
ConT ''V.V) (Int -> Type
intT Int
n)) (Name -> Type
VarT Name
a))) Type
tup)

      [| (\(V.V $(pure $ VarP vN)) -> $(pure xs)) :: $(pure typ) |]
  where
    intE :: Int -> Exp
intE = Lit -> Exp
LitE (Lit -> Exp) -> (Int -> Lit) -> Int -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Lit
IntegerL (Integer -> Lit) -> (Int -> Integer) -> Int -> Lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
    intT :: Int -> Type
intT = TyLit -> Type
LitT (TyLit -> Type) -> (Int -> TyLit) -> Int -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> TyLit
NumTyLit (Integer -> TyLit) -> (Int -> Integer) -> Int -> TyLit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger

-- Parsing specific dimensions -----------------------------------------

-- | Parse a 1D list. If the system is not valid, return a string
--   with error message.
parse1D :: [a] -> (V1 Int, [a])
parse1D :: [a] -> (Layout V1, [a])
parse1D [a]
as = (Int -> Layout V1
forall a. a -> V1 a
V1 Int
x, [a]
as) where
  x :: Int
x = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as

-- | Parse a 2D list of lists. If the system is not valid, returns an
--   error
parse2D :: [[a]] -> (V2 Int, [a])
parse2D :: [[a]] -> (Layout V2, [a])
parse2D [[a]]
as
  | Just (Int, Int)
e <- Maybe (Int, Int)
badX = String -> (Layout V2, [a])
forall a. HasCallStack => String -> a
error (String
"parse2D: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a a. (Show a, Show a) => (a, a) -> String
errMsg (Int, Int)
e)
  | Bool
otherwise      = (Int -> Int -> Layout V2
forall a. a -> a -> V2 a
V2 Int
x Int
y, [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
F.concat ([[a]] -> [a]) -> [[a]] -> [a]
forall a b. (a -> b) -> a -> b
$ [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
List.transpose [[a]]
as)
  where
    x :: Int
x  = [Int] -> Int
forall a. [a] -> a
head [Int]
xs
    y :: Int
y  = [[a]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
as
    xs :: [Int]
xs = ([a] -> Int) -> [[a]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[a]]
as

    badX :: Maybe (Int, Int)
badX         = (Int -> Int -> Bool) -> [Int] -> Maybe (Int, Int)
forall i (f :: * -> *) a.
FoldableWithIndex i f =>
(i -> a -> Bool) -> f a -> Maybe (i, a)
ifind ((Int -> Bool) -> Int -> Int -> Bool
forall a b. a -> b -> a
const (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
x)) [Int]
xs
    errMsg :: (a, a) -> String
errMsg (a
i,a
j) =
      String
"row " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" columns but the first"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" row has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" columns"

-- | Parse a 3D list of list of lists. If the system is not valid,
--  return a string with error message.
--
--   The element are reordered in the appropriate way for the array:
--
-- @
-- >>> parse3D [["abc","def","ghi"],["jkl","mno","pqr"],["stu","vwx","yz!"]]
-- ((V3 3 3 3), "ajsdmvgpybktenwhqzclufoxir!")
-- @
--
parse3D :: [[[a]]] -> (V3 Int, [a])
parse3D :: [[[a]]] -> (Layout V3, [a])
parse3D [[[a]]]
as
  | Getting All [[[a]]] a -> [[[a]]] -> Bool
forall s a. Getting All s a -> s -> Bool
nullOf (([[a]] -> Const All [[a]]) -> [[[a]]] -> Const All [[[a]]]
forall s t a b. Each s t a b => Traversal s t a b
each(([[a]] -> Const All [[a]]) -> [[[a]]] -> Const All [[[a]]])
-> ((a -> Const All a) -> [[a]] -> Const All [[a]])
-> Getting All [[[a]]] a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.([a] -> Const All [a]) -> [[a]] -> Const All [[a]]
forall s t a b. Each s t a b => Traversal s t a b
each(([a] -> Const All [a]) -> [[a]] -> Const All [[a]])
-> ((a -> Const All a) -> [a] -> Const All [a])
-> (a -> Const All a)
-> [[a]]
-> Const All [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(a -> Const All a) -> [a] -> Const All [a]
forall s t a b. Each s t a b => Traversal s t a b
each) [[[a]]]
as = (Layout V3
forall (f :: * -> *) a. (Additive f, Num a) => f a
zero, [])
  | Just ((Int, Int), Int)
e <- Maybe ((Int, Int), Int)
badX = String -> (Layout V3, [a])
forall a. HasCallStack => String -> a
error (String -> (Layout V3, [a])) -> String -> (Layout V3, [a])
forall a b. (a -> b) -> a -> b
$ ((Int, Int), Int) -> String
forall a a a. (Show a, Show a, Show a) => ((a, a), a) -> String
errorCol ((Int, Int), Int)
e
  | Just (Int, Int)
e <- Maybe (Int, Int)
badY = String -> (Layout V3, [a])
forall a. HasCallStack => String -> a
error (String -> (Layout V3, [a])) -> String -> (Layout V3, [a])
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> String
forall a a. (Show a, Show a) => (a, a) -> String
errorRow (Int, Int)
e
  | Bool
otherwise      = (Int -> Int -> Int -> Layout V3
forall a. a -> a -> a -> V3 a
V3 Int
x Int
y Int
z, [a]
as')
  where
    z :: Int
z  = [[[a]]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
as
    y :: Int
y  = [[a]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[[a]]] -> [[a]]
forall a. [a] -> a
head [[[a]]]
as)
    x :: Int
x  = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[a]] -> [a]
forall a. [a] -> a
head ([[[a]]] -> [[a]]
forall a. [a] -> a
head [[[a]]]
as))

    -- reorder and concatenate so it's the correct order for the array
    as' :: [a]
as' = ([[a]] -> [a]) -> [[[a]]] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
F.concatMap [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
F.concat ([[[a]]] -> [[[a]]]
forall a. [[a]] -> [[a]]
List.transpose ([[[a]]] -> [[[a]]]) -> [[[a]]] -> [[[a]]]
forall a b. (a -> b) -> a -> b
$ ([[a]] -> [[a]]) -> [[[a]]] -> [[[a]]]
forall a b. (a -> b) -> [a] -> [b]
map [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
List.transpose ([[[a]]] -> [[[a]]]) -> [[[a]]] -> [[[a]]]
forall a b. (a -> b) -> a -> b
$ [[[a]]] -> [[[a]]]
forall a. [[a]] -> [[a]]
List.transpose [[[a]]]
as)

    -- check for inconsistencies
    badY :: Maybe (Int, Int)
badY = (Int -> Int -> Bool) -> [Int] -> Maybe (Int, Int)
forall i (f :: * -> *) a.
FoldableWithIndex i f =>
(i -> a -> Bool) -> f a -> Maybe (i, a)
ifind ((Int -> Bool) -> Int -> Int -> Bool
forall a b. a -> b -> a
const (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
y)) (([[a]] -> Int) -> [[[a]]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [[a]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
as)
    badX :: Maybe ((Int, Int), Int)
badX = IndexedGetting
  (Int, Int) (Endo (Maybe ((Int, Int), Int))) [[[a]]] Int
-> ((Int, Int) -> Int -> Bool)
-> [[[a]]]
-> Maybe ((Int, Int), Int)
forall i a s.
IndexedGetting i (Endo (Maybe (i, a))) s a
-> (i -> a -> Bool) -> s -> Maybe (i, a)
ifindOf' (Indexed Int [[a]] (Const (Endo (Maybe ((Int, Int), Int))) [[a]])
-> [[[a]]] -> Const (Endo (Maybe ((Int, Int), Int))) [[[a]]]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
traversed (Indexed Int [[a]] (Const (Endo (Maybe ((Int, Int), Int))) [[a]])
 -> [[[a]]] -> Const (Endo (Maybe ((Int, Int), Int))) [[[a]]])
-> (Indexed Int Int (Const (Endo (Maybe ((Int, Int), Int))) Int)
    -> [[a]] -> Const (Endo (Maybe ((Int, Int), Int))) [[a]])
-> IndexedGetting
     (Int, Int) (Endo (Maybe ((Int, Int), Int))) [[[a]]] Int
forall i j (p :: * -> * -> *) s t r a b.
Indexable (i, j) p =>
(Indexed i s t -> r) -> (Indexed j a b -> s -> t) -> p a b -> r
<.> Indexed Int [a] (Const (Endo (Maybe ((Int, Int), Int))) [a])
-> [[a]] -> Const (Endo (Maybe ((Int, Int), Int))) [[a]]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
traversed (Indexed Int [a] (Const (Endo (Maybe ((Int, Int), Int))) [a])
 -> [[a]] -> Const (Endo (Maybe ((Int, Int), Int))) [[a]])
-> ((Int -> Const (Endo (Maybe ((Int, Int), Int))) Int)
    -> [a] -> Const (Endo (Maybe ((Int, Int), Int))) [a])
-> Indexed Int Int (Const (Endo (Maybe ((Int, Int), Int))) Int)
-> [[a]]
-> Const (Endo (Maybe ((Int, Int), Int))) [[a]]
forall i (p :: * -> * -> *) s t r a b.
Indexable i p =>
(Indexed i s t -> r) -> ((a -> b) -> s -> t) -> p a b -> r
<. ([a] -> Int)
-> (Int -> Const (Endo (Maybe ((Int, Int), Int))) Int)
-> [a]
-> Const (Endo (Maybe ((Int, Int), Int))) [a]
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ((Int -> Bool) -> (Int, Int) -> Int -> Bool
forall a b. a -> b -> a
const (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
x)) [[[a]]]
as

    -- error messages for inconsistent rows/columns
    errorCol :: ((a, a), a) -> String
errorCol ((a
k,a
j),a
i) =
      String
"plane " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", row " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
" columns" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", but the first row has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" columns"
    errorRow :: (a, a) -> String
errorRow (a
k,a
j) =
      String
"plane " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" rows but the first"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" plane has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" rows"

-- | Version of ifindOf which is consistent with ifind (in that it also returns the index).
ifindOf' :: IndexedGetting i (Endo (Maybe (i, a))) s a -> (i -> a -> Bool) -> s -> Maybe (i, a)
ifindOf' :: IndexedGetting i (Endo (Maybe (i, a))) s a
-> (i -> a -> Bool) -> s -> Maybe (i, a)
ifindOf' IndexedGetting i (Endo (Maybe (i, a))) s a
l i -> a -> Bool
p = IndexedGetting i (Endo (Maybe (i, a))) s a
-> (i -> a -> Maybe (i, a) -> Maybe (i, a))
-> Maybe (i, a)
-> s
-> Maybe (i, a)
forall i r s a.
IndexedGetting i (Endo r) s a -> (i -> a -> r -> r) -> r -> s -> r
ifoldrOf IndexedGetting i (Endo (Maybe (i, a))) s a
l (\i
i a
a Maybe (i, a)
y -> if i -> a -> Bool
p i
i a
a then (i, a) -> Maybe (i, a)
forall a. a -> Maybe a
Just (i
i, a
a) else Maybe (i, a)
y) Maybe (i, a)
forall a. Maybe a
Nothing
{-# INLINE ifindOf' #-}

-- Shape lift class ----------------------------------------------------

-- | Class of shapes that can be 'lift'ed.
--
--   This is to prevent orphans for the 'Lift' class.
class Shape f => ShapeLift f where
  -- | 'lift' for 'Shape's.
  liftShape :: Lift a => f a -> Q Exp

  -- | Polymorphic 'lift' for a 'Shape's.
  liftShape' :: Lift a => f a -> Q Exp

instance ShapeLift V1 where
  liftShape :: V1 a -> Q Exp
liftShape (V1 a
x) = [| V1 x |]
  liftShape' :: V1 a -> Q Exp
liftShape' (V1 a
x) = [| v1 x |]

instance ShapeLift V2 where
  liftShape :: V2 a -> Q Exp
liftShape (V2 a
x a
y) = [| V2 x y |]
  liftShape' :: V2 a -> Q Exp
liftShape' (V2 a
x a
y) = [| v2 x y |]

instance ShapeLift V3 where
  liftShape :: V3 a -> Q Exp
liftShape (V3 a
x a
y a
z) = [| V3 x y z |]
  liftShape' :: V3 a -> Q Exp
liftShape' (V3 a
x a
y a
z) = [| v3 x y z |]

instance ShapeLift V4 where
  liftShape :: V4 a -> Q Exp
liftShape (V4 a
x a
y a
z a
w) = [| V4 x y z w |]
  liftShape' :: V4 a -> Q Exp
liftShape' (V4 a
x a
y a
z a
w) = [| v4 x y z w |]

v1 :: (R1 f, Shape f, Num a) => a -> f a
v1 :: a -> f a
v1 a
x = ASetter (f a) (f a) a a -> a -> f a -> f a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (f a) (f a) a a
forall (t :: * -> *) a. R1 t => Lens' (t a) a
_x a
x f a
forall (f :: * -> *) a. (Shape f, Num a) => f a
one
{-# INLINE [0] v1 #-}

v2 :: (R2 f, Shape f, Num a) => a -> a -> f a
v2 :: a -> a -> f a
v2 a
x a
y = ASetter (f a) (f a) (V2 a) (V2 a) -> V2 a -> f a -> f a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (f a) (f a) (V2 a) (V2 a)
forall (t :: * -> *) a. R2 t => Lens' (t a) (V2 a)
_xy (a -> a -> V2 a
forall a. a -> a -> V2 a
V2 a
x a
y) f a
forall (f :: * -> *) a. (Shape f, Num a) => f a
one
{-# INLINE [0] v2 #-}

v3 :: (R3 f, Shape f, Num a) => a -> a -> a -> f a
v3 :: a -> a -> a -> f a
v3 a
x a
y a
z = ASetter (f a) (f a) (V3 a) (V3 a) -> V3 a -> f a -> f a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (f a) (f a) (V3 a) (V3 a)
forall (t :: * -> *) a. R3 t => Lens' (t a) (V3 a)
_xyz (a -> a -> a -> V3 a
forall a. a -> a -> a -> V3 a
V3 a
x a
y a
z) f a
forall (f :: * -> *) a. (Shape f, Num a) => f a
one
{-# INLINE [0] v3 #-}

v4 :: (R4 f, Shape f, Num a) => a -> a -> a -> a -> f a
v4 :: a -> a -> a -> a -> f a
v4 a
x a
y a
z a
w = ASetter (f a) (f a) (V4 a) (V4 a) -> V4 a -> f a -> f a
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter (f a) (f a) (V4 a) (V4 a)
forall (t :: * -> *) a. R4 t => Lens' (t a) (V4 a)
_xyzw (a -> a -> a -> a -> V4 a
forall a. a -> a -> a -> a -> V4 a
V4 a
x a
y a
z a
w) f a
forall (f :: * -> *) a. (Shape f, Num a) => f a
one
{-# INLINE [0] v4 #-}

one :: (Shape f, Num a) => f a
one :: f a
one = a
1 a -> f Int -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (forall (f :: * -> *). Additive f => f Int
forall (f :: * -> *) a. (Additive f, Num a) => f a
zero :: Additive f => f Int)

-- are these nessesary?
{-# RULES
 "v1/V1" v1 = V1;
 "v1/V2" forall a. v1 a = V2 a 1;
 "v1/V3" forall a. v1 a = V3 a 1 1;
 "v2/V2" v2 = V2;
 "v2/V3" forall a b. v2 a b = V3 a b 1;
 "v3/V3" v3 = V3;
 "v4/V4" v4 = V4
  #-}