{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures -fno-warn-orphans #-}
module WildcardSemantics where

-- import           Prelude hiding ((.),fail,Just,Nothing)

-- import qualified ConcreteSemantics as C
-- import           SharedSemantics
-- import           Soundness
-- import           Syntax hiding (Fail,TermPattern(..))
-- import           Utils

-- import           Control.Category
-- import           Control.Arrow
-- import           Control.Arrow.Deduplicate
-- import           Control.Arrow.Except
-- import           Control.Arrow.Fail
-- import           Control.Arrow.Fix
-- import           Control.Arrow.Reader
-- import           Control.Arrow.State
-- import           Control.Arrow.Transformer.Abstract.Except
-- import           Control.Arrow.Transformer.Abstract.Failure
-- import           Control.Arrow.Transformer.Abstract.Fix
-- import           Control.Arrow.Transformer.Abstract.Powerset
-- import           Control.Arrow.Transformer.Abstract.Terminating
-- import           Control.Arrow.Transformer.Reader
-- import           Control.Arrow.Transformer.State
-- import           Control.DeepSeq
-- import           Control.Monad hiding (fail)

-- import           Data.Abstract.FreeCompletion
-- import           Data.Abstract.Except
-- import           Data.Abstract.Failure
-- import           Data.Abstract.Maybe
-- import qualified Data.Abstract.Powerset as A
-- import           Data.Abstract.Map (Map)
-- import qualified Data.Abstract.Map as S
-- import qualified Data.Abstract.StackWidening as SW
-- import           Data.Abstract.Terminating (Terminating,fromTerminating)
-- import           Data.Abstract.Widening as W
-- import qualified Data.Concrete.Powerset as CP
-- import           Data.Constructor
-- import           Data.Foldable (foldr')
-- import           Data.GaloisConnection
-- import qualified Data.HashMap.Lazy as M
-- import           Data.Hashable
-- import           Data.Order
-- import           Data.Term
-- import           Data.Text (Text)
-- import           Data.Profunctor
-- import           Data.Functor.Const(Const)
-- import qualified Data.Lens as L

-- import           Test.QuickCheck hiding (Success)
-- import           Text.Printf

-- -- | Abstract terms in this semantics contain wildcards that represent
-- -- every possible concrete term.
-- data Term
--     = Cons Constructor [Term]
--     | StringLiteral Text
--     | NumberLiteral Int
--     | Wildcard
--     deriving (Eq)

-- type TermEnv = Map TermVar Term

-- -- | 
-- newtype Interp s a b =
--   Interp (
--     Fix (Strat,Term) Term
--       (ReaderT StratEnv
--         (StateT TermEnv
--           (ExceptT ()
--             (FailureT String
--               (PowT
--                 (TerminatingT
--                   (FixT s () ()
--                     (->)))))))) a b)

-- type Stack = (Const (SW.Groups ((StratVar, [Strat], [TermVar]), StratEnv) (Term, TermEnv) SW.Stack (TermEnv, (StratEnv, ((StratVar, [Strat], [TermVar]), Term)))))

-- runInterp :: Interp _ a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (A.Pow (Failure String (Except () (TermEnv,b))))
-- runInterp (Interp f) k senv0 tenv0 a =
--   runFixT stackWidening W.finite
--     (runTerminatingT
--       (runPowT
--         (runFailureT
--           (runExceptT
--             (runStateT
--               (runReaderT f))))))
--     (tenv0, (senv0, a))
--   where
--     stackWidening :: SW.StackWidening _ (TermEnv, (StratEnv, (Strat, Term)))
--     stackWidening = SW.filter' (L.second (L.second (L.first stratCall)))
--                   $ SW.groupBy (L.iso' (\(tenv,(senv,(strat,term))) -> ((strat,senv),(term,tenv))) (\((strat,senv),(term,tenv)) -> (tenv,(senv,(strat,term)))))
--                   $ SW.stack
--                   $ SW.reuseFirst
--                   $ SW.maxSize k
--                   $ SW.topOut

-- from' :: (TermEnv, (StratEnv, (Strat, Term))) -> ((Strat, StratEnv), (TermEnv, Term))
-- from' (tenv,(senv,(s,t))) = ((s,senv),(tenv,t))

-- to' :: ((Strat, StratEnv), (TermEnv, Term)) -> (TermEnv, (StratEnv, (Strat, Term)))
-- to' ((s,senv),(tenv,t)) = (tenv,(senv,(s,t)))

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

-- -- Instances -----------------------------------------------------------------------------------------
-- deriving instance Profunctor (Interp s)
-- deriving instance Category (Interp s)
-- deriving instance Arrow (Interp s)
-- deriving instance ArrowChoice (Interp s)
-- deriving instance ArrowReader StratEnv (Interp s)
-- deriving instance ArrowState TermEnv (Interp s)
-- deriving instance ArrowFail String (Interp s)
-- deriving instance ArrowFix (Strat,Term) Term (Interp Stack)
-- deriving instance ArrowExcept () (Interp s)
-- deriving instance ArrowDeduplicate Term Term (Interp s)
-- deriving instance PreOrd b => PreOrd (Interp s a b)
-- deriving instance (Complete  b, PreOrd b) => Complete (Interp s a b)

-- instance ArrowApply (Interp s) where
--   app = Interp $ (\(Interp f, b) -> (f,b)) ^>> app

-- instance HasStratEnv (Interp s) where
--   readStratEnv = Interp (const () ^>> ask)
--   localStratEnv senv f = proc a -> do
--     r <- local f -< (senv,a)
--     returnA -< r

-- instance IsTermEnv TermEnv Term (Interp s) where
--   getTermEnv = get
--   putTermEnv = put
--   lookupTermVar f g = proc (v,env,ex) ->
--     case S.lookup v env of
--       Just t -> f -< t
--       JustNothing t -> joined f g -< (t,ex)
--       Nothing -> g -< ex
--   insertTerm = arr $ \(v,t,env) -> S.insert v t env
--   deleteTermVars = arr $ \(vars,env) -> foldr' S.delete env vars
--   unionTermEnvs = arr (\(vars,e1,e2) -> S.union e1 (foldr' S.delete e2 vars))

-- instance IsTerm Term (Interp s) 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)] ])
--       (returnA -< Cons c ts'') ⊔ (throw -< ())
--     _ -> throw -< ()
  
--   matchTermAgainstString = proc (s,t) -> case t of
--     StringLiteral s'
--       | s == s' -> returnA -< t
--       | otherwise -> throw -< ()
--     Wildcard ->
--       (returnA -< StringLiteral s) ⊔ (throw -< ())
--     _ -> throw -< ()
  
--   matchTermAgainstNumber = proc (n,t) -> case t of
--     NumberLiteral n'
--       | n == n' -> returnA -< t
--       | otherwise -> throw -< ()
--     Wildcard ->
--       (returnA -< NumberLiteral n) ⊔ (throw -< ())
--     _ -> throw -< ()
  
--   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 -> throw -< ()
--       (StringLiteral s, StringLiteral s')
--           | s == s' -> success -< t1
--           | otherwise -> throw -< ()
--       (NumberLiteral n, NumberLiteral n')
--           | n == n' -> success -< t1
--           | otherwise -> throw -< ()
--       (Wildcard, t) -> (returnA -< t) ⊔ (throw -< ())
--       (t, Wildcard) -> (returnA -< t) ⊔ (throw -< ())
--       (_,_) -> throw -< ()
  
--   convertFromList = proc (c,ts) -> case (c,go ts) of
--     (StringLiteral c', Just ts'') -> returnA -< Cons (Constructor c') ts''
--     (Wildcard, Just _)            -> (returnA -< Wildcard) ⊔ (throw -< ())
--     (_,                Nothing)   -> (returnA -< Wildcard) ⊔ (throw -< ())
--     _                             -> throw -< ()
--     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
--       Wildcard -> (returnA -< Wildcard) ⊔ (throw -< ())
  
--   cons = arr (uncurry Cons)
--   numberLiteral = arr NumberLiteral
--   stringLiteral = arr StringLiteral

-- instance Soundness StratEnv (Interp Stack) where
--   sound senv xs f g = forAll (choose (0,3)) $ \i ->
--     let con :: A.Pow (Failure String (Except () (TermEnv,_)))
--         con = A.dedup $ alpha (fmap (\(x,tenv) -> C.runInterp f senv tenv x) xs)
--         abst :: A.Pow (Failure String (Except () (TermEnv,_)))
--         abst = A.dedup $ fromTerminating (error "non-terminating wildcard semantics") $ runInterp g i senv (alpha (fmap snd xs)) (alpha (fmap fst xs))
--     in counterexample (printf "%s ⊑/ %s" (show con) (show abst)) $ con ⊑ abst

-- instance UpperBounded Term where
--   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

-- instance Complete (FreeCompletion Term) where
--   Lower x ⊔ Lower y = Lower (x ⊔ y)
--   _ ⊔ _ = Top


-- instance Complete Term where
--   t1 ⊔ t2 = case (t1,t2) of
--     (Cons c ts, Cons c' ts')
--       | c == c' -> case Lower ts ⊔ Lower ts' of
--           Lower ts'' -> Cons c ts''
--           _          -> 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

-- instance Galois (CP.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 ++ if null ts then "" else 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

-- instance UpperBounded TermEnv where
--   top = S.empty

-- instance Galois (CP.Pow C.TermEnv) TermEnv where
--   alpha = lub . fmap (\(C.TermEnv e) -> S.fromList (M.toList (fmap alphaSing e)))
--   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 #-}
 
