Model.hs

{-
   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.
-}

{-

This files gives an executable implementation of the model for
abstract stencil specifications. This model is used to drive both
the specification checking and program synthesis features.

-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}

module Camfort.Specification.Stencils.Model where

import Camfort.Specification.Stencils.Syntax
import Data.Set hiding (map,foldl',(\\))
import qualified Data.Set as Set
import Data.List
import qualified Data.List as DL
import qualified Data.Map as DM

{-| This function maps inner representation to a set of vectors of length
-   given by `dim`. This is the mathematical representation of the
-   specification. |-}
model :: Multiplicity (Approximation Spatial)
      -> Int
      -> Multiplicity (Approximation (Set [Int]))
model s dims =
    let ?globalDimensionality = dims
    in mkModel s

consistent :: Multiplicity [[Int]]
           -> Multiplicity (Approximation Spatial)
           -> Bool
-- If the specification says "readOnce" but there are duplicates among
-- offsets, then there is no consistency.
--
-- Note that if the spec omits "readOnce" and the offsets happen to be
-- unique that is allowed as "readOnce" is an extra qualifier.
consistent (Multiple _) (Single _) = False
consistent mult1 spec =
    consistent' (model spec dimensionality)
  where
    dimensionality = length . head $ accesses
    consistent' m2 =
      case fromMult m2 of
        Exact unifiers ->
          consistent' (Multiple (Bound Nothing (Just unifiers))) &&
          consistent' (Multiple (Bound (Just unifiers) Nothing))
        Bound lus@Just{} uus@Just{} ->
          consistent' (Multiple (Bound lus Nothing)) &&
          consistent' (Multiple (Bound Nothing uus))
        Bound Nothing (Just unifiers) ->
          all (\access -> any (access `accepts`) unifiers) accesses
        Bound (Just unifiers) Nothing ->
          all (\unifier -> any (`accepts` unifier) accesses) unifiers

    accesses = fromMult mult1

    access `accepts` unifier =
      all (\(u,v) -> v == absoluteRep || u == v) (zip access unifier)

-- Recursive `Model` class implemented for all parts of the spec.
class Model spec where
   type Domain spec

   -- generate model for the specification, where the implicit
   -- parameter ?globalDimensionality is the global dimensionality
   -- for the spec (not just the local maximum dimensionality)
   mkModel :: (?globalDimensionality :: Int) => spec -> Domain spec

   -- Return the maximum dimension specified in the spec
   -- giving the dimensionality for that specification
   dimensionality :: spec -> Int
   dimensionality = maximum . dimensions
   -- Return all the dimensions specified for in this spec
   dimensions :: spec -> [Int]

-- Set representation where multiplicities are (-1) modulo 2
-- that is, False = multiplicity 1, True = multiplicity > 1
instance Model Specification where
   type Domain Specification = Multiplicity (Approximation (Set [Int]))

   mkModel (Specification s) = mkModel s

   dimensionality (Specification s) = dimensionality s

   dimensions (Specification s) = dimensions s

instance Model (Multiplicity (Approximation Spatial)) where
   type Domain (Multiplicity (Approximation Spatial)) =
     Multiplicity (Approximation (Set [Int]))

   mkModel (Multiple s) = Multiple (mkModel s)
   mkModel (Single s) = Single (mkModel s)

   dimensionality mult = dimensionality $ fromMult mult

   dimensions mult = dimensions $ fromMult mult

instance Model (Approximation Spatial) where
  type Domain (Approximation Spatial) = Approximation (Set [Int])

  mkModel = fmap mkModel
  dimensionality (Exact s) = dimensionality s
  dimensionality (Bound l u) = dimensionality l `max` dimensionality u

  dimensions (Exact s) = dimensions s
  dimensions (Bound l u) = dimensions l ++ dimensions u

-- Lifting of model to Maybe type
instance Model a => Model (Maybe a) where
  type Domain (Maybe a) = Maybe (Domain a)

  mkModel Nothing = Nothing
  mkModel (Just x) = Just (mkModel x)

  dimensions Nothing = [0]
  dimensions (Just x) = dimensions x

-- Core part of the model
instance Model Spatial where
    type Domain Spatial = Set [Int]

    mkModel (Spatial s) = mkModel s

    dimensionality (Spatial s) = dimensionality s

    dimensions (Spatial s)     = dimensions s


instance Model RegionSum where
   type Domain RegionSum = Set [Int]
   mkModel (Sum ss) = unions (map mkModel ss)
   dimensionality (Sum ss) =
     maximum1 (map dimensionality ss)

   dimensions (Sum ss) = concatMap dimensions ss


instance Model Region where
   type Domain Region = Set [Int]

   mkModel (Forward dep dim reflx) = fromList
     [mkSingleEntryNeg i dim ?globalDimensionality | i <- [i0..dep]]
       where i0 = if reflx then 0 else 1

   mkModel (Backward dep dim reflx) = fromList
     [mkSingleEntryNeg i dim ?globalDimensionality | i <- [(-dep)..i0]]
       where i0 = if reflx then 0 else 1

   mkModel (Centered dep dim reflx) = fromList
     [mkSingleEntryNeg i dim ?globalDimensionality | i <- [(-dep)..dep] \\ i0]
       where i0 = if reflx then [] else [0]

   dimensionality (Forward  _ d _) = d
   dimensionality (Backward _ d _) = d
   dimensionality (Centered _ d _) = d

   dimensions (Forward _ d _)  = [d]
   dimensions (Backward _ d _) = [d]
   dimensions (Centered _ d _) = [d]

mkSingleEntryNeg :: Int -> Int -> Int -> [Int]
mkSingleEntryNeg i 0 ds = error "Dimensions are 1-indexed"
mkSingleEntryNeg i 1 ds = i : replicate (ds - 1) absoluteRep
mkSingleEntryNeg i d ds = absoluteRep : mkSingleEntryNeg i (d - 1) (ds - 1)

instance Model RegionProd where
   type Domain RegionProd = Set [Int]

   mkModel (Product [])  = Set.empty
   mkModel (Product [s])  = mkModel s
   mkModel p@(Product ss)  = cleanedProduct
     where
       cleanedProduct = fromList $ DL.filter keepPred product
       product = cprodVs $ map (toList . mkModel) ss
       dims = dimensions p
       keepPred el = DL.foldr (\pr acc -> nonProdP pr && acc) True (zip [(1::Int)..] el)
       nonProdP (i,el) = i `notElem` dims || el /= absoluteRep

   dimensionality (Product ss) =
      maximum1 (map dimensionality ss)
   dimensions (Product ss) =
      nub $ concatMap dimensions ss

tensor n s t = cleanedProduct
   where
       cleanedProduct = fromList $ DL.filter keepPred product
       product = cprodV s t
       keepPred el = DL.foldr (\pr acc -> nonProdP pr && acc) True (zip [(1::Int)..] el)
       nonProdP (i,el) = i `notElem` [1..n] || el /= absoluteRep

-- Cartesian product on list of vectors4
cprodVs :: [[[Int]]] -> [[Int]]
cprodVs = foldr1 cprodV

cprodV :: [[Int]] -> [[Int]] -> [[Int]]
cprodV xss yss = xss >>= (\xs -> yss >>= pairwisePerm xs)

pairwisePerm :: [Int] -> [Int] -> [[Int]]
pairwisePerm x y = sequence . transpose $ [x, y]

maximum1 [] = 0
maximum1 xs = maximum xs