WildcardSemantics.hs 12.1 KB
Newer Older
Sven Keidel's avatar
Sven Keidel committed
1 2 3 4 5 6 7 8 9 10
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures -fno-warn-orphans #-}
module WildcardSemantics where

Jente Hidskes's avatar
Jente Hidskes committed
11
import           Prelude hiding ((.),uncurry)
Sven Keidel's avatar
Sven Keidel committed
12 13

import qualified ConcreteSemantics as C
14
import           SharedSemantics
Sven Keidel's avatar
Sven Keidel committed
15
import           Soundness
16 17
import           Syntax hiding (Fail,TermPattern(..))
import           Utils
Sven Keidel's avatar
Sven Keidel committed
18 19 20 21 22
    
import           Control.Arrow
import           Control.Arrow.Apply
import           Control.Arrow.Try
import           Control.Arrow.Fix
23
import           Control.Arrow.Fail
Sven Keidel's avatar
Sven Keidel committed
24
import           Control.Arrow.Deduplicate
25
import           Control.Arrow.Utils (failA')
Sven Keidel's avatar
Sven Keidel committed
26 27
import           Control.Category
import           Control.DeepSeq
Jente Hidskes's avatar
Jente Hidskes committed
28
import           Control.Monad.Reader
Sven Keidel's avatar
Sven Keidel committed
29
import           Control.Monad.Result
Jente Hidskes's avatar
Jente Hidskes committed
30
import           Control.Monad.State
Sven Keidel's avatar
Sven Keidel committed
31 32

import           Data.Constructor
33
import           Data.Error
Sven Keidel's avatar
Sven Keidel committed
34 35 36 37 38 39
import           Data.Foldable (foldr')
import           Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import           Data.Hashable
import           Data.Order
import           Data.GaloisConnection
40
import           Data.FreeCompletion
Sven Keidel's avatar
Sven Keidel committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
import           Data.Powerset hiding (size)
import qualified Data.Powerset as P
import qualified Data.AbstractPowerset as A
import           Data.Term
import           Data.TermEnv
import           Data.Text (Text)
import           Data.Result

import           Test.QuickCheck hiding (Result(..))
import           Text.Printf

data Term
    = Cons Constructor [Term]
    | StringLiteral Text
    | NumberLiteral Int
    | Wildcard
    deriving (Eq)

newtype TermEnv = TermEnv (HashMap TermVar Term) deriving (Show,Eq,Hashable)
newtype Interp a b = Interp (Kleisli (ReaderT (StratEnv,Int) (StateT TermEnv (ResultT A.Pow))) a b)
61
  deriving (Category,Arrow,ArrowChoice,ArrowApply,ArrowTry,ArrowZero,ArrowPlus,ArrowDeduplicate,PreOrd,Complete)
Sven Keidel's avatar
Sven Keidel committed
62 63 64 65 66 67 68 69 70 71 72 73 74 75

runInterp :: Interp a b -> Int -> StratEnv -> TermEnv -> a -> A.Pow (Result (b,TermEnv))
runInterp (Interp f) i senv tenv a = runResultT (runStateT (runReaderT (runKleisli f a) (senv,i)) tenv)

eval :: Int -> Strat -> StratEnv -> TermEnv -> Term -> A.Pow (Result (Term,TermEnv))
eval i s = runInterp (eval' s) i

liftK :: (a -> _ b) -> Interp a b
liftK f = Interp (Kleisli f)

emptyEnv :: TermEnv
emptyEnv = TermEnv M.empty

-- Instances -----------------------------------------------------------------------------------------
76 77 78
instance ArrowFail () Interp where
  failA = Interp failA

Sven Keidel's avatar
Sven Keidel committed
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
instance HasStratEnv Interp where
  readStratEnv = liftK (const (fst <$> ask))
  localStratEnv senv (Interp (Kleisli f)) = liftK (local (first (const senv)) . f)

instance IsTermEnv TermEnv Term Interp where
  getTermEnv = liftK (const get)
  putTermEnv = liftK (modify . const)
  lookupTermVar f g = proc (v,TermEnv env) ->
    case M.lookup v env of
      Just t -> f -< t
      Nothing ->
        (proc () -> do
          putTermEnv -< TermEnv (M.insert v Wildcard env)
          f -< Wildcard)
         g
        -<< ()
  insertTerm = arr $ \(v,t,TermEnv env) -> TermEnv (M.insert v t env)
  deleteTermVars = arr $ \(vars,TermEnv env) -> TermEnv (foldr' M.delete env vars)
  unionTermEnvs = arr (\(vars,TermEnv e1,TermEnv e2) -> TermEnv (M.union e1 (foldr' M.delete e2 vars)))

instance IsTerm Term Interp where
  matchTermAgainstConstructor matchSubterms = proc (c,ts,t) -> case t of
    Cons c' ts' | c == c' && eqLength ts ts' -> do
      ts'' <- matchSubterms -< (ts,ts')
      returnA -< Cons c ts''
    Wildcard -> do
      ts'' <- matchSubterms -< (ts,[ Wildcard | _ <- [1..(length ts)] ])
106
      returnA  failA' -< Cons c ts''
Sven Keidel's avatar
Sven Keidel committed
107 108 109 110 111 112 113
    _ -> failA -< ()
  
  matchTermAgainstString = proc (s,t) -> case t of
    StringLiteral s'
      | s == s' -> returnA -< t
      | otherwise -> failA -< ()
    Wildcard ->
114 115
      returnA  failA' -< StringLiteral s
    _ -> failA' -< ()
Sven Keidel's avatar
Sven Keidel committed
116 117 118 119 120 121
  
  matchTermAgainstNumber = proc (n,t) -> case t of
    NumberLiteral n'
      | n == n' -> returnA -< t
      | otherwise -> failA -< ()
    Wildcard ->
122 123
      success  failA' -< NumberLiteral n
    _ -> failA' -< ()
Sven Keidel's avatar
Sven Keidel committed
124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
  
  matchTermAgainstExplode matchCons matchSubterms = proc t -> case t of
      Cons (Constructor c) ts -> do
        matchCons -< StringLiteral c
        matchSubterms -< convertToList ts
        returnA -< t
      StringLiteral _ -> do
        matchSubterms -< convertToList []
        returnA -< t
      NumberLiteral _ -> do
        matchSubterms -< convertToList []
        returnA -< t
      Wildcard ->
        (proc t -> do
           matchCons -< Wildcard
           matchSubterms -< Wildcard
           returnA -< t)
        
        (proc t -> do
           matchSubterms -< convertToList []
           returnA -< t)
        -< t
  
  equal = proc (t1,t2) ->
    case (t1,t2) of
      (Cons c ts, Cons c' ts')
          | c == c' && eqLength ts ts' -> do
          ts'' <- zipWithA equal -< (ts,ts')
          returnA -< Cons c ts''
          | otherwise -> failA -< ()
      (StringLiteral s, StringLiteral s')
          | s == s' -> success -< t1
          | otherwise -> failA -< ()
      (NumberLiteral n, NumberLiteral n')
          | n == n' -> success -< t1
          | otherwise -> failA -< ()
160 161 162
      (Wildcard, t) -> failA'  success -< t
      (t, Wildcard) -> failA'  success -< t
      (_,_) -> failA' -< ()
Sven Keidel's avatar
Sven Keidel committed
163 164 165
  
  convertFromList = proc (c,ts) -> case (c,go ts) of
    (StringLiteral c', Just ts'') -> returnA -< Cons (Constructor c') ts''
166 167 168
    (Wildcard, Just _)            -> failA'  success -< Wildcard
    (_,                Nothing)   -> failA'  success -< Wildcard
    _                             -> failA' -< ()
Sven Keidel's avatar
Sven Keidel committed
169 170 171 172 173 174 175 176 177 178 179 180 181 182
    where
      go t = case t of
        Cons "Cons" [x,tl] -> (x:) <$> go tl
        Cons "Nil" [] -> Just []
        Wildcard -> Nothing 
        _ -> Nothing
  
  mapSubterms f = proc t ->
    case t of
      Cons c ts -> do
        ts' <- f -< ts
        returnA -< Cons c ts'
      StringLiteral _ -> returnA -< t
      NumberLiteral _ -> returnA -< t
183
      Wildcard -> failA'  success -< Wildcard
Sven Keidel's avatar
Sven Keidel committed
184 185 186 187 188 189
  
  
  cons = arr (uncurry Cons)
  numberLiteral = arr NumberLiteral
  stringLiteral = arr StringLiteral

190
instance UpperBounded (Interp () Term) where
191
  top = proc () -> success  failA' -< Wildcard
Sven Keidel's avatar
Sven Keidel committed
192

193 194
instance ArrowFix' Interp Term where
  fixA' f z = proc x -> do
Sven Keidel's avatar
Sven Keidel committed
195 196 197
    i <- getFuel -< ()
    if i <= 0
    then top -< ()
198
    else localFuel (f (fixA' f) z) -< (i-1,x)
Sven Keidel's avatar
Sven Keidel committed
199 200 201 202 203 204 205
    where
      getFuel = liftK (const (snd <$> ask))
      localFuel (Interp (Kleisli g)) = liftK $ \(i,a) -> local (second (const i)) (g a)

instance Soundness Interp where
  sound senv xs f g = forAll (choose (0,3)) $ \i ->
    let con :: A.Pow (Result (_,TermEnv))
Jente Hidskes's avatar
Jente Hidskes committed
206
        con = A.dedup $ alpha (fmap (\(x,tenv) -> C.runInterp f senv tenv x) xs)
Sven Keidel's avatar
Sven Keidel committed
207
        abst :: A.Pow (Result (_,TermEnv))
Jente Hidskes's avatar
Jente Hidskes committed
208
        abst = A.dedup $ runInterp g i senv (alpha (fmap snd xs)) (alpha (fmap fst xs))
Sven Keidel's avatar
Sven Keidel committed
209 210
    in counterexample (printf "%s ⊑/ %s" (show con) (show abst)) $ con  abst

211
instance UpperBounded Term where
Sven Keidel's avatar
Sven Keidel committed
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
  top = Wildcard

instance TermUtils Term where
  convertToList ts = case ts of
    (x:xs) -> Cons "Cons" [x,convertToList xs]
    []     -> Cons "Nil" []
    
  size (Cons _ ts) = sum (size <$> ts) + 1
  size (StringLiteral _) = 1
  size (NumberLiteral _) = 1
  size Wildcard = 1

  height (Cons _ []) = 1
  height (Cons _ ts) = maximum (height <$> ts) + 1
  height (StringLiteral _) = 1
  height (NumberLiteral _) = 1
  height Wildcard = 1

instance PreOrd Term where
  t1  t2 = case (t1,t2) of
    (_,Wildcard) -> True
    (Cons c ts,Cons c' ts') -> c == c' && (ts  ts')
    (StringLiteral s, StringLiteral s') -> s == s'
    (NumberLiteral n, NumberLiteral n') -> n == n'
    (_, _) -> False

238
instance Complete Term where
Sven Keidel's avatar
Sven Keidel committed
239 240
  t1  t2 = case (t1,t2) of
    (Cons c ts, Cons c' ts')
241 242
      | c == c' -> case Lower ts  Lower ts' of
        Lower ts'' -> Cons c ts''
Sven Keidel's avatar
Sven Keidel committed
243 244 245 246 247 248 249 250 251 252 253 254
        _             -> Wildcard
      | otherwise -> Wildcard
    (StringLiteral s, StringLiteral s')
      | s == s' -> StringLiteral s
      | otherwise -> Wildcard
    (NumberLiteral n, NumberLiteral n')
      | n == n' -> NumberLiteral n
      | otherwise -> Wildcard
    (Wildcard, _) -> Wildcard
    (_, Wildcard) -> Wildcard
    (_, _) -> Wildcard

255 256 257 258 259 260
instance LowerBounded Term where
  bottom = undefined

instance LowerBounded TermEnv where
  bottom = emptyEnv

Sven Keidel's avatar
Sven Keidel committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
instance Galois (P.Pow C.Term) Term where
  alpha = lub . fmap go
    where
      go (C.Cons c ts) = Cons c (fmap go ts)
      go (C.StringLiteral s) = StringLiteral s
      go (C.NumberLiteral s) = NumberLiteral s
  gamma = error "Infinite"

instance Show Term where
  show (Cons c ts) = show c ++ show ts
  show (StringLiteral s) = show s
  show (NumberLiteral n) = show n
  show Wildcard = "_"

instance Num Term where
  t1 + t2 = Cons "Add" [t1,t2]
  t1 - t2 = Cons "Sub" [t1,t2]
  t1 * t2 = Cons "Mul" [t1,t2]
  abs t = Cons "Abs" [t]
  signum t = Cons "Signum" [t]
  fromInteger = NumberLiteral . fromIntegral

instance Hashable Term where
  hashWithSalt s (Cons c ts) = s `hashWithSalt` (0::Int) `hashWithSalt` c `hashWithSalt` ts
  hashWithSalt s (StringLiteral t) = s `hashWithSalt` (1::Int) `hashWithSalt` t
  hashWithSalt s (NumberLiteral n) = s `hashWithSalt` (2::Int) `hashWithSalt` n
  hashWithSalt s Wildcard = s `hashWithSalt` (3::Int)

instance NFData Term where
  rnf t = case t of
    Cons c ts -> rnf c `seq` rnf ts
    StringLiteral s -> rnf s
    NumberLiteral n -> rnf n
    Wildcard -> ()

instance Arbitrary Term where
  arbitrary = do
    he <- choose (0,7)
    wi <- choose (0,4)
    arbitraryTerm he wi

arbitraryTerm :: Int -> Int -> Gen Term
arbitraryTerm 0 _ =
  oneof
    [ Cons <$> arbitrary <*> pure []
    , StringLiteral <$> arbitraryLetter
    , NumberLiteral <$> choose (0,9)
    , pure Wildcard
    ]
arbitraryTerm h w = do
  w' <- choose (0,w)
  c <- arbitrary
  fmap (Cons c) $ vectorOf w' $ join $
    arbitraryTerm <$> choose (0,h-1) <*> pure w

internal :: Arrow c => c (HashMap TermVar Term) (HashMap TermVar Term) -> c TermEnv TermEnv
internal f = arr TermEnv . f . arr (\(TermEnv e) -> e)

map :: ArrowChoice c => c Term Term -> c TermEnv TermEnv
map f = internal (arr M.fromList . mapA (second f) . arr M.toList)

dom :: HashMap TermVar t -> [TermVar]
dom = M.keys

instance PreOrd TermEnv where
  TermEnv env1  TermEnv env2 =
327
    Prelude.all (\v -> fromMaybe (M.lookup v env1)  fromMaybe (M.lookup v env2)) (dom env2)
Sven Keidel's avatar
Sven Keidel committed
328

329
instance Complete TermEnv where
Sven Keidel's avatar
Sven Keidel committed
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
  TermEnv env1'  TermEnv env2' = go (dom env1') env1' env2' M.empty
    where
      go vars env1 env2 env3 = case vars of
        (v:vs) -> case (M.lookup v env1,M.lookup v env2) of
          (Just t1,Just t2) -> go vs env1 env2 (M.insert v (t1t2) env3)
          _                 -> go vs env1 env2 env3
        [] -> TermEnv env3

instance Galois (Pow C.TermEnv) TermEnv where
  alpha = lub . fmap (\(C.TermEnv e) -> TermEnv (fmap alphaSing e))
  gamma = undefined

instance (Eq x, Hashable x, Eq x', Hashable x', Galois (Pow x) x') => Galois (Pow (Result x)) (A.Pow (Result x')) where
  alpha = P.fromFoldable . fmap (fmap alphaSing)
  gamma = undefined

-- prim :: (ArrowTry p, ArrowAppend p, IsTerm t p, IsTermEnv (AbstractTermEnv t) t p)
--      => StratVar -> [TermVar] -> p a t
-- prim f ps = undefined
  -- proc _ -> case f of
  --   "SSL_strcat" -> do
  --     args <- lookupTermArgs -< ps
  --     case args of
  --       [T.StringLiteral t1, T.StringLiteral t2] -> stringLiteral -< t1 `append` t2
  --       [T.Wildcard, _] -> wildcard -< ()
  --       [_, T.Wildcard] -> wildcard -< ()
  --       _ -> fail -< ()
  --   "SSL_newname" -> do
  --     args <- lookupTermArgs -< ps
  --     case args of
  --       [T.StringLiteral _] -> wildcard -< ()
  --       [T.Wildcard] -> wildcard -< ()
  --       _ -> fail -< ()
  --   _ -> error ("unrecognized primitive function: " ++ show f) -< ()
  -- where
  --   lookupTermArgs = undefined
      -- proc args -> do
      -- tenv <- getTermEnv -< ()
      -- case mapM (`M.lookup` tenv) args of
      --   Just t -> mapA matchTerm -< t
      --   Nothing -> fail <+> success -< [T.Wildcard | _ <- args]
-- {-# SPECIALISE prim :: StratVar -> [TermVar] -> Interp StratEnv TermEnv PowersetResult Term Term #-}