content: {-# 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 #-}
   
  