content: {-# LANGUAGE Arrows #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PartialTypeSignatures #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-orphans -fsimpl-tick-factor=400 #-}
  module AbstractInterpreter where
  
  import           Prelude as Prelude hiding ((.),fail,id,iterate)
  
  import           SortContext (Context)
  import           Syntax hiding (Fail,TermPattern(..),id)
  import           Abstract.TermEnvironment as TEnv
  
  import           Control.Category
  import           Control.Arrow.Fix as Fix
  import           Control.Arrow.Fix.Stack(reuseFirst)
  import           Control.Arrow.Trans
  import           Control.Arrow.Transformer.Value
  import           Control.Arrow.Transformer.Const
  import qualified Control.Arrow.Transformer.Abstract.Environment as SEnv
  import           Control.Arrow.Transformer.Abstract.Completion
  import           Control.Arrow.Transformer.Abstract.Except
  import           Control.Arrow.Transformer.Abstract.Error
  import           Control.Arrow.Transformer.Abstract.Terminating
  import           Control.Arrow.Transformer.Abstract.Fix
  import           Control.Arrow.Fix.Chaotic
  import           Control.Arrow.Transformer.Abstract.Fix.Stack
  import           Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable
  import           Control.Arrow.Transformer.Abstract.Fix.Component as Comp
  
  import qualified Data.HashMap.Lazy as M
  import qualified Data.Abstract.Environment.Flat as Flat
  import           Data.Abstract.Closure (Closure)
  import qualified Data.Abstract.Closure as Cl
  import           Data.Abstract.FreeCompletion hiding (Top)
  import qualified Data.Abstract.FreeCompletion as Free
  import           Data.Abstract.Except as E
  import           Data.Abstract.Error as F
  import           Data.Abstract.DiscretePowerset(Pow)
  import qualified Data.Abstract.DiscretePowerset as P
  import qualified Data.Abstract.Map as S
  import           Data.Abstract.Terminating (Terminating)
  import qualified Data.Abstract.Terminating as T
  import           Data.Abstract.Stable
  import           Data.Abstract.Widening as W
  import           Data.Order
  
  import           Data.Identifiable
  -- import           Data.Hashable(hash)
  -- import           GHC.Exts(toList)
  
  import           Prettyprinter
  
  
  type TypeError = Pow String
  type SEnv = Flat.Env StratVar (Closure Strategy)
  
  type Dom t = ((Strat, SEnv), (t, TermEnv t))
  type Cod t = Terminating (FreeCompletion (Error (Pow String) (Except () (TermEnv t,t))))
  type Interp t =
     ValueT t
      (ConstT Context
       (SEnv.EnvT SEnv
        (TEnv.EnvT t
         --NoInlineT
          (ExceptT ()
           (ErrorT TypeError
            (CompletionT
             (TerminatingT
              (FixT
               -- TraceT
                (ComponentT Comp.Component (Dom t)
                 (StackT Stack (Dom t)
                  (CacheT (Group Cache) (Dom t) (Cod t)
                   (->))))))))))))
  
  runInterp :: forall t x y. (Pretty t, Show t, Complete t, Identifiable t)
            => (FixpointAlgorithm (Fix (Interp t (Strat,t) t)) -> Interp t x y)
            -> W.Widening t
            -> StratEnv
            -> Context
            -> TermEnv t
            -> x
            -> Terminating (FreeCompletion (Error (Pow String) (Except () (TermEnv t,y))))
  runInterp f termWidening senv0 ctx0 tenv0 a0 =
    -- let ?contextWidening = termWidening W.** S.widening termWidening in
    let ?cacheWidening = T.widening (Free.widening (F.widening P.widening (E.widening (\_ _ -> (Stable,())) (S.widening termWidening W.** termWidening)))) in
    let algorithm =
          Fix.fixpointAlgorithm $
          Fix.filterPrism stratApply
          (
            reuseFirst .
  
            -- Fix.trace (\((strat,senv),(term,tenv)) ->
            --              vsep [ "STRAT" <+> align (pretty strat <> "@" <> pretty (hash strat))
            --                   , "TERM " <+> align (pretty term <> "@" <> pretty (hash term))
            --                   , "TENV " <+> align (pretty tenv <> "@" <> pretty (hash tenv))
            --                   , "SENV " <+> align (pretty (hash senv))
            --                   ])
            --            (\ret -> pretty ret <> "@" <> pretty (hash ret)) .
  
            -- Fix.traceCache (\(cache :: Group Cache (Dom t) (Cod t)) ->
            --                   show $ vsep [ vsep [pretty strat <+> pretty (hash strat),
            --                                       pretty term <+> pretty (hash term),
            --                                       pretty tenv <+> pretty (hash tenv),
            --                                       pretty (hash senv), -- pretty senv <+> pretty (hash senv),
            --                                       pretty ret <+> pretty (hash ret),
            --                                       pretty stable]
            --                               | ((strat,senv),cache')    <- toList cache,
            --                                 ((term,tenv),ret,stable) <- toList cache']) .
              outermost
          )
    in snd (run (f algorithm) ctx0 (tenv0, (senvInit, a0)))
    where
      senvInit = Flat.fromList [ (var,Cl.closure strat ())| (var,strat) <- M.toList senv0]
  {-# INLINE runInterp #-}
  