{-
   Copyright 2016, Dominic Orchard, Andrew Rice, Mistral Contrastin, Matthew Danish

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
-}

{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImplicitParams         #-}
{-# LANGUAGE TupleSections          #-}

module Camfort.Specification.Stencils.CheckBackend
  (
    -- * Classes
    SynToAst(..)
    -- * Errors
  , SynToAstError
  , regionNotInScope
    -- * Helpers
  , checkOffsetsAgainstSpec
  ) where

import           Algebra.Lattice (joins1)
import           Control.Arrow (second)
import           Data.Function (on)
import           Data.Int (Int64)
import           Data.List (sort)
import qualified Data.List.NonEmpty as NE
import qualified Data.Set as S

import qualified Camfort.Helpers.Vec as V
import qualified Camfort.Specification.Stencils.Consistency as C
import           Camfort.Specification.Stencils.Model
import qualified Camfort.Specification.Stencils.Parser.Types as SYN
import           Camfort.Specification.Stencils.Syntax

data SynToAstError = RegionNotInScope String
  deriving (SynToAstError -> SynToAstError -> Bool
(SynToAstError -> SynToAstError -> Bool)
-> (SynToAstError -> SynToAstError -> Bool) -> Eq SynToAstError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SynToAstError -> SynToAstError -> Bool
== :: SynToAstError -> SynToAstError -> Bool
$c/= :: SynToAstError -> SynToAstError -> Bool
/= :: SynToAstError -> SynToAstError -> Bool
Eq)

regionNotInScope :: String -> SynToAstError
regionNotInScope :: Variable -> SynToAstError
regionNotInScope = Variable -> SynToAstError
RegionNotInScope

instance Show SynToAstError where
  show :: SynToAstError -> Variable
show (RegionNotInScope Variable
r) = Variable
"Error: region " Variable -> ShowS
forall a. [a] -> [a] -> [a]
++ Variable
r Variable -> ShowS
forall a. [a] -> [a] -> [a]
++ Variable
" is not in scope."

-- Class for functions converting from Parser parse
-- syntax to the AST representation of the Syntax module
class SynToAst s t | s -> t where
  synToAst :: (?renv :: RegionEnv) => s -> Either SynToAstError t

-- Top-level conversion of declarations
instance SynToAst SYN.Specification (Either RegionDecl SpecDecl) where
  synToAst :: (?renv::RegionEnv) =>
Specification -> Either SynToAstError (Either RegionDecl SpecDecl)
synToAst (SYN.SpecDec SpecInner
spec [Variable]
vars) = do
     Specification
spec' <- SpecInner -> Either SynToAstError Specification
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst SpecInner
spec
     Either RegionDecl SpecDecl
-> Either SynToAstError (Either RegionDecl SpecDecl)
forall a. a -> Either SynToAstError a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either RegionDecl SpecDecl
 -> Either SynToAstError (Either RegionDecl SpecDecl))
-> Either RegionDecl SpecDecl
-> Either SynToAstError (Either RegionDecl SpecDecl)
forall a b. (a -> b) -> a -> b
$ SpecDecl -> Either RegionDecl SpecDecl
forall a b. b -> Either a b
Right ([Variable]
vars, Specification
spec')

  synToAst (SYN.RegionDec Variable
rvar Region
region) = do
     RegionSum
spec' <- Region -> Either SynToAstError RegionSum
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst Region
region
     Either RegionDecl SpecDecl
-> Either SynToAstError (Either RegionDecl SpecDecl)
forall a. a -> Either SynToAstError a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either RegionDecl SpecDecl
 -> Either SynToAstError (Either RegionDecl SpecDecl))
-> Either RegionDecl SpecDecl
-> Either SynToAstError (Either RegionDecl SpecDecl)
forall a b. (a -> b) -> a -> b
$ RegionDecl -> Either RegionDecl SpecDecl
forall a b. a -> Either a b
Left (Variable
rvar, RegionSum
spec')

-- Convert temporal or spatial specifications
instance SynToAst SYN.SpecInner Specification where
  synToAst :: (?renv::RegionEnv) =>
SpecInner -> Either SynToAstError Specification
synToAst (SYN.SpecInner Multiplicity (Approximation Region)
spec Bool
isStencil) = do
    Multiplicity (Approximation Spatial)
spec' <- Multiplicity (Approximation Region)
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst Multiplicity (Approximation Region)
spec
    Specification -> Either SynToAstError Specification
forall a. a -> Either SynToAstError a
forall (m :: * -> *) a. Monad m => a -> m a
return (Specification -> Either SynToAstError Specification)
-> Specification -> Either SynToAstError Specification
forall a b. (a -> b) -> a -> b
$ Multiplicity (Approximation Spatial) -> Bool -> Specification
Specification Multiplicity (Approximation Spatial)
spec' Bool
isStencil

instance SynToAst (Multiplicity (Approximation SYN.Region)) (Multiplicity (Approximation Spatial)) where
  synToAst :: (?renv::RegionEnv) =>
Multiplicity (Approximation Region)
-> Either SynToAstError (Multiplicity (Approximation Spatial))
synToAst (Once Approximation Region
a) = (Approximation Spatial -> Multiplicity (Approximation Spatial))
-> Either SynToAstError (Approximation Spatial)
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall a b.
(a -> b) -> Either SynToAstError a -> Either SynToAstError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Approximation Spatial -> Multiplicity (Approximation Spatial)
forall a. a -> Multiplicity a
Once (Either SynToAstError (Approximation Spatial)
 -> Either SynToAstError (Multiplicity (Approximation Spatial)))
-> (Approximation Region
    -> Either SynToAstError (Approximation Spatial))
-> Approximation Region
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Approximation Region
-> Either SynToAstError (Approximation Spatial)
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst (Approximation Region
 -> Either SynToAstError (Multiplicity (Approximation Spatial)))
-> Approximation Region
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall a b. (a -> b) -> a -> b
$ Approximation Region
a
  synToAst (Mult Approximation Region
a) = (Approximation Spatial -> Multiplicity (Approximation Spatial))
-> Either SynToAstError (Approximation Spatial)
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall a b.
(a -> b) -> Either SynToAstError a -> Either SynToAstError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Approximation Spatial -> Multiplicity (Approximation Spatial)
forall a. a -> Multiplicity a
Mult (Either SynToAstError (Approximation Spatial)
 -> Either SynToAstError (Multiplicity (Approximation Spatial)))
-> (Approximation Region
    -> Either SynToAstError (Approximation Spatial))
-> Approximation Region
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Approximation Region
-> Either SynToAstError (Approximation Spatial)
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst (Approximation Region
 -> Either SynToAstError (Multiplicity (Approximation Spatial)))
-> Approximation Region
-> Either SynToAstError (Multiplicity (Approximation Spatial))
forall a b. (a -> b) -> a -> b
$ Approximation Region
a

instance SynToAst (Approximation SYN.Region) (Approximation Spatial) where
  synToAst :: (?renv::RegionEnv) =>
Approximation Region
-> Either SynToAstError (Approximation Spatial)
synToAst (Exact Region
s)     = (RegionSum -> Approximation Spatial)
-> Either SynToAstError RegionSum
-> Either SynToAstError (Approximation Spatial)
forall a b.
(a -> b) -> Either SynToAstError a -> Either SynToAstError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Spatial -> Approximation Spatial
forall a. a -> Approximation a
Exact (Spatial -> Approximation Spatial)
-> (RegionSum -> Spatial) -> RegionSum -> Approximation Spatial
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegionSum -> Spatial
Spatial) (Either SynToAstError RegionSum
 -> Either SynToAstError (Approximation Spatial))
-> (Region -> Either SynToAstError RegionSum)
-> Region
-> Either SynToAstError (Approximation Spatial)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Region -> Either SynToAstError RegionSum
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst (Region -> Either SynToAstError (Approximation Spatial))
-> Region -> Either SynToAstError (Approximation Spatial)
forall a b. (a -> b) -> a -> b
$ Region
s
  synToAst (Bound Maybe Region
s1 Maybe Region
s2) = (Maybe Spatial -> Maybe Spatial -> Approximation Spatial
forall a. Maybe a -> Maybe a -> Approximation a
Bound (Maybe Spatial -> Maybe Spatial -> Approximation Spatial)
-> (Maybe RegionSum -> Maybe Spatial)
-> Maybe RegionSum
-> Maybe RegionSum
-> Approximation Spatial
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ((RegionSum -> Spatial) -> Maybe RegionSum -> Maybe Spatial
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RegionSum -> Spatial
Spatial)) (Maybe RegionSum -> Maybe RegionSum -> Approximation Spatial)
-> Either SynToAstError (Maybe RegionSum)
-> Either SynToAstError (Maybe RegionSum -> Approximation Spatial)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Region -> Either SynToAstError (Maybe RegionSum)
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst Maybe Region
s1 Either SynToAstError (Maybe RegionSum -> Approximation Spatial)
-> Either SynToAstError (Maybe RegionSum)
-> Either SynToAstError (Approximation Spatial)
forall a b.
Either SynToAstError (a -> b)
-> Either SynToAstError a -> Either SynToAstError b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Region -> Either SynToAstError (Maybe RegionSum)
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst Maybe Region
s2

instance SynToAst (Maybe SYN.Region) (Maybe RegionSum) where
  synToAst :: (?renv::RegionEnv) =>
Maybe Region -> Either SynToAstError (Maybe RegionSum)
synToAst Maybe Region
Nothing  = Maybe RegionSum -> Either SynToAstError (Maybe RegionSum)
forall a. a -> Either SynToAstError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe RegionSum
forall a. Maybe a
Nothing
  synToAst (Just Region
r) = (RegionSum -> Maybe RegionSum)
-> Either SynToAstError RegionSum
-> Either SynToAstError (Maybe RegionSum)
forall a b.
(a -> b) -> Either SynToAstError a -> Either SynToAstError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RegionSum -> Maybe RegionSum
forall a. a -> Maybe a
Just (Either SynToAstError RegionSum
 -> Either SynToAstError (Maybe RegionSum))
-> (Region -> Either SynToAstError RegionSum)
-> Region
-> Either SynToAstError (Maybe RegionSum)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Region -> Either SynToAstError RegionSum
forall s t.
(SynToAst s t, ?renv::RegionEnv) =>
s -> Either SynToAstError t
synToAst (Region -> Either SynToAstError (Maybe RegionSum))
-> Region -> Either SynToAstError (Maybe RegionSum)
forall a b. (a -> b) -> a -> b
$ Region
r

-- Convert region definitions into the DNF-form used internally
instance SynToAst SYN.Region RegionSum where
  synToAst :: (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
synToAst = (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
Region -> Either SynToAstError RegionSum
dnf

-- Convert a grammar syntax to Disjunctive Normal Form AST
dnf :: (?renv :: RegionEnv) => SYN.Region -> Either SynToAstError RegionSum

dnf :: (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
dnf (SYN.RegionConst Region
rconst) = RegionSum -> Either SynToAstError RegionSum
forall a. a -> Either SynToAstError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RegionSum -> Either SynToAstError RegionSum)
-> ([RegionProd] -> RegionSum)
-> [RegionProd]
-> Either SynToAstError RegionSum
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RegionProd] -> RegionSum
Sum ([RegionProd] -> Either SynToAstError RegionSum)
-> [RegionProd] -> Either SynToAstError RegionSum
forall a b. (a -> b) -> a -> b
$ [[Region] -> RegionProd
Product [Region
rconst]]
-- Distributive law
dnf (SYN.And Region
r1 Region
r2) = do
    RegionSum
r1' <- (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
Region -> Either SynToAstError RegionSum
dnf Region
r1
    RegionSum
r2' <- (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
Region -> Either SynToAstError RegionSum
dnf Region
r2
    RegionSum -> Either SynToAstError RegionSum
forall a. a -> Either SynToAstError a
forall (m :: * -> *) a. Monad m => a -> m a
return (RegionSum -> Either SynToAstError RegionSum)
-> RegionSum -> Either SynToAstError RegionSum
forall a b. (a -> b) -> a -> b
$ [RegionProd] -> RegionSum
Sum ([RegionProd] -> RegionSum) -> [RegionProd] -> RegionSum
forall a b. (a -> b) -> a -> b
$ RegionSum -> [RegionProd]
unSum RegionSum
r1' [RegionProd] -> (RegionProd -> [RegionProd]) -> [RegionProd]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\(Product [Region]
ps1) ->
                    RegionSum -> [RegionProd]
unSum RegionSum
r2' [RegionProd] -> (RegionProd -> [RegionProd]) -> [RegionProd]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\(Product [Region]
ps2) ->
                      RegionProd -> [RegionProd]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (RegionProd -> [RegionProd]) -> RegionProd -> [RegionProd]
forall a b. (a -> b) -> a -> b
$ [Region] -> RegionProd
Product ([Region] -> RegionProd) -> [Region] -> RegionProd
forall a b. (a -> b) -> a -> b
$ [Region]
ps1 [Region] -> [Region] -> [Region]
forall a. [a] -> [a] -> [a]
++ [Region]
ps2))
-- Coalesce sums
dnf (SYN.Or Region
r1 Region
r2) = do
    RegionSum
r1' <- (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
Region -> Either SynToAstError RegionSum
dnf Region
r1
    RegionSum
r2' <- (?renv::RegionEnv) => Region -> Either SynToAstError RegionSum
Region -> Either SynToAstError RegionSum
dnf Region
r2
    RegionSum -> Either SynToAstError RegionSum
forall a. a -> Either SynToAstError a
forall (m :: * -> *) a. Monad m => a -> m a
return (RegionSum -> Either SynToAstError RegionSum)
-> RegionSum -> Either SynToAstError RegionSum
forall a b. (a -> b) -> a -> b
$ [RegionProd] -> RegionSum
Sum ([RegionProd] -> RegionSum) -> [RegionProd] -> RegionSum
forall a b. (a -> b) -> a -> b
$ RegionSum -> [RegionProd]
unSum RegionSum
r1' [RegionProd] -> [RegionProd] -> [RegionProd]
forall a. [a] -> [a] -> [a]
++ RegionSum -> [RegionProd]
unSum RegionSum
r2'
-- Region conversion
dnf (SYN.Var Variable
v)              =
    case Variable -> RegionEnv -> Maybe RegionSum
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Variable
v ?renv::RegionEnv
RegionEnv
?renv of
      Maybe RegionSum
Nothing -> SynToAstError -> Either SynToAstError RegionSum
forall a b. a -> Either a b
Left (Variable -> SynToAstError
RegionNotInScope Variable
v)
      Just RegionSum
rs -> RegionSum -> Either SynToAstError RegionSum
forall a. a -> Either SynToAstError a
forall (m :: * -> *) a. Monad m => a -> m a
return RegionSum
rs

-- *** Other Helpers

checkOffsetsAgainstSpec :: [(Variable, Multiplicity [[Int]])]
                        -> [(Variable, Specification)]
                        -> Bool
checkOffsetsAgainstSpec :: [(Variable, Multiplicity [[Int]])]
-> [(Variable, Specification)] -> Bool
checkOffsetsAgainstSpec [(Variable, Multiplicity [[Int]])]
offsetMaps [(Variable, Specification)]
specMaps =
  Bool
variablesConsistent Bool -> Bool -> Bool
&& ((Specification, Multiplicity (VecList Int64)) -> Bool)
-> [(Specification, Multiplicity (VecList Int64))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Specification, Multiplicity (VecList Int64)) -> Bool
specConsistent [(Specification, Multiplicity (VecList Int64))]
specToVecList
  where
    variablesConsistent :: Bool
variablesConsistent =
      let vs1 :: [Variable]
vs1 = [Variable] -> [Variable]
forall a. Ord a => [a] -> [a]
sort ([Variable] -> [Variable])
-> ([(Variable, Multiplicity [[Int]])] -> [Variable])
-> [(Variable, Multiplicity [[Int]])]
-> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Variable, Multiplicity [[Int]]) -> Variable)
-> [(Variable, Multiplicity [[Int]])] -> [Variable]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable, Multiplicity [[Int]]) -> Variable
forall a b. (a, b) -> a
fst ([(Variable, Multiplicity [[Int]])] -> [Variable])
-> [(Variable, Multiplicity [[Int]])] -> [Variable]
forall a b. (a -> b) -> a -> b
$ [(Variable, Multiplicity [[Int]])]
offsetMaps
          vs2 :: [Variable]
vs2 = [Variable] -> [Variable]
forall a. Ord a => [a] -> [a]
sort ([Variable] -> [Variable])
-> ([(Variable, Specification)] -> [Variable])
-> [(Variable, Specification)]
-> [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Variable, Specification) -> Variable)
-> [(Variable, Specification)] -> [Variable]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable, Specification) -> Variable
forall a b. (a, b) -> a
fst ([(Variable, Specification)] -> [Variable])
-> [(Variable, Specification)] -> [Variable]
forall a b. (a -> b) -> a -> b
$ [(Variable, Specification)]
specMaps
      in [Variable]
vs1 [Variable] -> [Variable] -> Bool
forall a. Eq a => a -> a -> Bool
== [Variable]
vs2
    specConsistent :: (Specification, Multiplicity (VecList Int64)) -> Bool
specConsistent (Specification, Multiplicity (VecList Int64))
spec =
      case (Specification, Multiplicity (VecList Int64))
spec of
        (Specification
spec', Once (V.VL [Vec n Int64]
vs)) -> Specification
spec' Specification
-> Multiplicity (UnionNF n Offsets) -> ConsistencyResult
forall (n :: Nat).
Specification
-> Multiplicity (UnionNF n Offsets) -> ConsistencyResult
`C.consistent` (UnionNF n Offsets -> Multiplicity (UnionNF n Offsets)
forall a. a -> Multiplicity a
Once (UnionNF n Offsets -> Multiplicity (UnionNF n Offsets))
-> ([Vec n Int64] -> UnionNF n Offsets)
-> [Vec n Int64]
-> Multiplicity (UnionNF n Offsets)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n Int64] -> UnionNF n Offsets
forall (n :: Nat). [Vec n Int64] -> UnionNF n Offsets
toUNF) [Vec n Int64]
vs ConsistencyResult -> ConsistencyResult -> Bool
forall a. Eq a => a -> a -> Bool
== ConsistencyResult
C.Consistent
        (Specification
spec', Mult (V.VL [Vec n Int64]
vs)) -> Specification
spec' Specification
-> Multiplicity (UnionNF n Offsets) -> ConsistencyResult
forall (n :: Nat).
Specification
-> Multiplicity (UnionNF n Offsets) -> ConsistencyResult
`C.consistent` (UnionNF n Offsets -> Multiplicity (UnionNF n Offsets)
forall a. a -> Multiplicity a
Mult (UnionNF n Offsets -> Multiplicity (UnionNF n Offsets))
-> ([Vec n Int64] -> UnionNF n Offsets)
-> [Vec n Int64]
-> Multiplicity (UnionNF n Offsets)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Vec n Int64] -> UnionNF n Offsets
forall (n :: Nat). [Vec n Int64] -> UnionNF n Offsets
toUNF) [Vec n Int64]
vs ConsistencyResult -> ConsistencyResult -> Bool
forall a. Eq a => a -> a -> Bool
== ConsistencyResult
C.Consistent
    toUNF :: [ V.Vec n Int64 ] -> UnionNF n Offsets
    toUNF :: forall (n :: Nat). [Vec n Int64] -> UnionNF n Offsets
toUNF = NonEmpty (UnionNF n Offsets) -> UnionNF n Offsets
forall a (f :: * -> *). (Lattice a, Foldable1 f) => f a -> a
joins1 (NonEmpty (UnionNF n Offsets) -> UnionNF n Offsets)
-> ([Vec n Int64] -> NonEmpty (UnionNF n Offsets))
-> [Vec n Int64]
-> UnionNF n Offsets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UnionNF n Offsets] -> NonEmpty (UnionNF n Offsets)
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([UnionNF n Offsets] -> NonEmpty (UnionNF n Offsets))
-> ([Vec n Int64] -> [UnionNF n Offsets])
-> [Vec n Int64]
-> NonEmpty (UnionNF n Offsets)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vec n Int64 -> UnionNF n Offsets)
-> [Vec n Int64] -> [UnionNF n Offsets]
forall a b. (a -> b) -> [a] -> [b]
map (Vec n Offsets -> UnionNF n Offsets
forall a. a -> NonEmpty a
forall (m :: * -> *) a. Monad m => a -> m a
return (Vec n Offsets -> UnionNF n Offsets)
-> (Vec n Int64 -> Vec n Offsets)
-> Vec n Int64
-> UnionNF n Offsets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int64 -> Offsets) -> Vec n Int64 -> Vec n Offsets
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int64 -> Offsets
intToSubscript)

    -- This function generates the special offsets subspace, subscript,
    -- that either had one element or is the whole set.
    intToSubscript :: Int64 -> Offsets
    intToSubscript :: Int64 -> Offsets
intToSubscript Int64
i
      | Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
absoluteRep = Offsets
SetOfIntegers
      | Bool
otherwise = Set Int64 -> Offsets
Offsets (Set Int64 -> Offsets) -> (Int64 -> Set Int64) -> Int64 -> Offsets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Set Int64
forall a. a -> Set a
S.singleton (Int64 -> Offsets) -> Int64 -> Offsets
forall a b. (a -> b) -> a -> b
$ Int64
i

    -- Convert list of list of indices into vectors and wrap them around
    -- existential so that we don't have to prove they are all of the same
    -- size.
    specToVecList :: [ (Specification, Multiplicity (V.VecList Int64)) ]
    specToVecList :: [(Specification, Multiplicity (VecList Int64))]
specToVecList = ((Specification, Multiplicity [[Int64]])
 -> (Specification, Multiplicity (VecList Int64)))
-> [(Specification, Multiplicity [[Int64]])]
-> [(Specification, Multiplicity (VecList Int64))]
forall a b. (a -> b) -> [a] -> [b]
map ((Multiplicity [[Int64]] -> Multiplicity (VecList Int64))
-> (Specification, Multiplicity [[Int64]])
-> (Specification, Multiplicity (VecList Int64))
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (([[Int64]] -> VecList Int64)
-> Multiplicity [[Int64]] -> Multiplicity (VecList Int64)
forall a b. (a -> b) -> Multiplicity a -> Multiplicity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Int64]] -> VecList Int64
forall a. [[a]] -> VecList a
V.fromLists)) [(Specification, Multiplicity [[Int64]])]
specToIxs

    specToIxs :: [ (Specification, Multiplicity [ [ Int64 ] ]) ]
    specToIxs :: [(Specification, Multiplicity [[Int64]])]
specToIxs = [(Variable, Specification)]
-> [(Variable, Multiplicity [[Int64]])]
-> [(Specification, Multiplicity [[Int64]])]
forall a b c. Eq a => [(a, b)] -> [(a, c)] -> [(b, c)]
pairWithFst [(Variable, Specification)]
specMaps (((Variable, Multiplicity [[Int]])
 -> (Variable, Multiplicity [[Int64]]))
-> [(Variable, Multiplicity [[Int]])]
-> [(Variable, Multiplicity [[Int64]])]
forall a b. (a -> b) -> [a] -> [b]
map ((Multiplicity [[Int]] -> Multiplicity [[Int64]])
-> (Variable, Multiplicity [[Int]])
-> (Variable, Multiplicity [[Int64]])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Multiplicity [[Int]] -> Multiplicity [[Int64]]
toInt64) [(Variable, Multiplicity [[Int]])]
offsetMaps)

    toInt64 :: Multiplicity [ [ Int ] ] -> Multiplicity [ [ Int64 ] ]
    toInt64 :: Multiplicity [[Int]] -> Multiplicity [[Int64]]
toInt64 = ([[Int]] -> [[Int64]])
-> Multiplicity [[Int]] -> Multiplicity [[Int64]]
forall a b. (a -> b) -> Multiplicity a -> Multiplicity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Int] -> [Int64]) -> [[Int]] -> [[Int64]]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int64) -> [Int] -> [Int64]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral))

    -- Given two maps for each key in the first map generate a set of
    -- tuples matching the (val,val') where val and val' are corresponding
    -- values from each set.
    pairWithFst :: Eq a => [ (a, b) ] -> [ (a, c) ] -> [ (b, c) ]
    pairWithFst :: forall a b c. Eq a => [(a, b)] -> [(a, c)] -> [(b, c)]
pairWithFst [] [(a, c)]
_ = []
    pairWithFst ((a
key, b
val):[(a, b)]
xs) [(a, c)]
ys =
      ((a, c) -> (b, c)) -> [(a, c)] -> [(b, c)]
forall a b. (a -> b) -> [a] -> [b]
map ((b
val,) (c -> (b, c)) -> ((a, c) -> c) -> (a, c) -> (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, c) -> c
forall a b. (a, b) -> b
snd) (((a, c) -> Bool) -> [(a, c)] -> [(a, c)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((a
key a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==) (a -> Bool) -> ((a, c) -> a) -> (a, c) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, c) -> a
forall a b. (a, b) -> a
fst) [(a, c)]
ys) [(b, c)] -> [(b, c)] -> [(b, c)]
forall a. [a] -> [a] -> [a]
++ [(a, b)] -> [(a, c)] -> [(b, c)]
forall a b c. Eq a => [(a, b)] -> [(a, c)] -> [(b, c)]
pairWithFst [(a, b)]
xs [(a, c)]
ys

-- Local variables:
-- mode: haskell
-- haskell-program-name: "cabal repl"
-- End: