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