{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC
  -Wno-partial-type-signatures
  -Wno-orphans
  -fspecialise-aggressively
  -fexpose-all-unfoldings
  -funfolding-use-threshold=10000
  -flate-specialise
  -flate-dmd-anal
  -fsimpl-tick-factor=50000
  -fmax-simplifier-iterations=10
#-}
module SortSemantics where

import           Prelude hiding ((.),fail)

import           GenericInterpreter as Generic
import           AbstractInterpreter
import           Abstract.TermEnvironment
import           Sort
import           SortContext (Context,Signature(..))
import qualified SortContext as Ctx
import           Syntax (Strat,LStrat,LStratEnv,Strategy)
import           Utils

import           Control.Category
import           Control.Arrow
import           Control.Arrow.Closure
import           Control.Arrow.Trans
import           Control.Arrow.Const
import           Control.Arrow.Except
import           Control.Arrow.Fail as Fail
import           Control.Arrow.Order
import           Control.Arrow.Transformer.Value
import           Control.DeepSeq

import           Data.Abstract.Closure(Closure)
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.Terminating (Terminating)
import           Data.Abstract.Widening as W
import           Data.Hashable
import           Data.Order hiding (LowerBounded(..))
import           Data.Profunctor
import           Data.Label

import           Text.Printf
import           Prettyprinter
import           GHC.Exts(IsString(..))

data Term = Term { sort :: Sort, context :: Context }

-- {-# SPECIALIZE Generic.eval :: (?fixpointAlgorithm :: FixpointAlgorithm (Fix (Interp Term (Strat,Term) Term)))
--                             => Strat -> Interp Term Term Term #-}

eval :: Int -> LStrat -> LStratEnv -> Context -> TermEnv Term -> Term -> Terminating (FreeCompletion (Error TypeError (Except () (TermEnv Term,Term))))
eval j lstrat lsenv ctx =
  let (strat,senv) = generate $ (,) <$> lstrat <*> lsenv
  in runInterp (\algo -> let ?fixpointAlgorithm = algo in
                   (Generic.eval :: Strat -> Interp Term Term Term) strat) termWidening senv ctx
  where
    termWidening :: Widening Term
    termWidening (Term s _) (Term s' _) = let ~(st,s'') = Ctx.widening ctx j s s' in (st,Term s'' ctx)

-- Instances -----------------------------------------------------------------------------------------
instance (ArrowChoice c, ArrowApply c, ArrowComplete Term c, ArrowConst Context c, ArrowLowerBounded Term c, ArrowFail e c, ArrowExcept () c, IsString e, Fail.Join Term c)
    => IsTerm Term (ValueT Term c) where
  matchCons matchSubterms = proc (c,ps,t@(Term s ctx)) ->
    case (c,ps,s) of
      (_,_,Bottom) -> do
          ss' <- matchSubterms -< (ps,[t | _ <- ps])
          buildCons -< (c,ss')
      ("Cons",[_,_],_) | isList t -> (do
           let t' = Term (List Top) ctx ⊓ t
           ss <- matchSubterms -< (ps,[getListElem t', t'])
           buildCons -< ("Cons",ss))
           <⊔>
           (throw -< ())
      ("Cons",_,_) -> typeMismatch -< ("List",show s)
      ("Nil",[],_) | isList t -> (returnA -< Term (List Bottom) ctx) <⊔> (throw -< ())
      ("Nil",_,_) -> throw -< ()
      ("",_,Tuple ss)
        | eqLength ss ps -> do
          ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
          buildCons -< (c,ss')
        | otherwise -> throw -< ()
      ("",_,Top) -> (do
           ss <- matchSubterms -< (ps,[Term Top ctx | _ <- ps ])
           buildCons -< ("",ss))
           <⊔>
           (throw -< ())
      (_,_,Top) -> do
         (| joinList (typeError -< printf "cannot find constructor %s in context" (show c))
                     (\(Signature ss _) ->
                       if eqLength ss ps
                       then do
                         ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
                         buildCons -< (c,ss')
                       else throw -< ()) |)
            (Ctx.lookupCons ctx c)
          <⊔>
          do throw -< ()
      _ -> do
        (| joinList (bottom -< ()) -- printf "cannot find constructors of %s in context" (show s)
                    (\(c',Signature ss _) ->
                       if c == c' && eqLength ss ps
                       then do
                         ss' <- matchSubterms -< (ps,sortsToTerms ss ctx)
                         buildCons -< (c',ss')
                       else throw -< ()) |)
           (Ctx.lookupSort ctx s)

  matchString = proc (_,t) ->
    if isLexical t
      then (returnA -< t) <⊔> (throw -< ())
      else throw -< ()

  matchNum = proc (_,t) ->
    if isNumeric t
      then (returnA -< t) <⊔> (throw -< ())
      else throw -< ()

  matchExplode matchCons' matchSubterms = proc t -> case t of
    _ | isLexical t -> do
        matchSubterms -< convertToList [] (context t)
        returnA -< t
      | isNumeric t -> do
        matchSubterms -< convertToList [] (context t)
        returnA -< t
    Term (Tuple ss) ctx -> do
        matchCons' -< Term Lexical ctx
        matchSubterms -< Term (List $ foldr (Ctx.lub ctx) Bottom ss) ctx
        returnA -< t
    Term _ ctx -> do
      matchCons' -< Term Lexical ctx
      matchSubterms -< Term (List Top) ctx
      returnA -< t

  buildExplode = proc (t,ts) ->
    if isLexical t && isList ts
      then (returnA -< Term Top (context t)) <⊔> (throw -< ()) -- cannot deduct target sort from sort Lexical
      else throw -< ()

  buildCons = askConst $ \ctx -> proc (c, ss) -> case c of
    "Cons" -> case ss of
      [Term a _,Term s _] ->
        if isList (Term s ctx)
          then returnA -< Term (List a) ctx ⊔ Term s ctx
          else typeMismatch -< ("List(_)",show s)
      _ -> typeMismatch -< ("a * List(b)",show ss)
    "Nil" -> case ss of
      [] -> returnA -< Term (List Bottom) ctx
      _ -> typeMismatch -< ("List(a)",show ss)
    "" -> returnA -< Term (Tuple (map sort ss)) ctx
    _ -> let t = glb1 (Term Top ctx : [ Term s ctx | Signature ss' s <- Ctx.lookupCons ctx c, ss ⊑ sortsToTerms ss' ctx ])
         in if t == Term Bottom ctx
            then typeError -< printf "Could not construct term %s. Could not find the constructor %s in the context." (show (c,ss)) (show c)
            else returnA   -< t

  buildNum = askConst $ \ctx -> proc _ -> do
    returnA -< Term Numerical ctx

  buildString = askConst $ \ctx -> proc _ -> do
    returnA -< Term Lexical ctx

  equal = proc (t1,t2) -> case t1 ⊓ t2 of
    t | sort t == Bottom -> throw -< ()
      | isSingleton t1 && isSingleton t2 -> returnA -< t
      | otherwise -> (returnA -< t) <⊔> (throw -< ())

  mapSubterms f = askConst $ \ctx -> proc s -> do
    case sort s of
      Top ->
        typeError -< "generic traversal over top is not supported."
      s' ->
        (| joinList
          (typeError -< printf "Sort %s not found in context." (show s))
          (\(c,ts) -> do
            ts' <- f -< ts
            buildCons -< (c,ts')) |)
          ([ (c',sortsToTerms ss ctx) | (c',Signature ss _) <- Ctx.lookupSort ctx s'])

  {-# INLINE matchCons #-}
  {-# INLINE matchString #-}
  {-# INLINE matchNum #-}
  {-# INLINE matchExplode #-}
  {-# INLINE buildCons #-}
  {-# INLINE buildString #-}
  {-# INLINE buildNum #-}
  {-# INLINE buildExplode #-}
  {-# INLINE equal #-}
  {-# INLINE mapSubterms #-}

-- instance ArrowConst Context c => ArrowTop Term (EnvironmentT Term c) where
--   topA = proc () -> do
--     ctx <- askConst -< ()
--     returnA -< Term Top ctx

deriving instance ArrowComplete Term c => ArrowComplete Term (ValueT Term c)
deriving instance ArrowLowerBounded Term c => ArrowLowerBounded Term (ValueT Term c)
deriving instance ArrowClosure Strategy (Closure Strategy SEnv) c => ArrowClosure Strategy (Closure Strategy SEnv) (ValueT Term c)

instance ArrowTrans (ValueT Term) where
  lift' = ValueT
  {-# INLINE lift' #-}

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

instance Show Term where
  show (Term s _) = show s

instance Pretty Term where
  pretty = viaShow

instance Eq Term where
  Term t1 _ == Term t2 _ = t1 == t2

instance Hashable Term where
  hashWithSalt salt (Term s _) = salt `hashWithSalt` s

instance NFData Term where
  rnf = rnf . sort

instance PreOrd Term where
  Term s1 ctx ⊑ Term s2 _ = Ctx.subtype ctx s1 s2

instance Complete Term where
  Term t1 ctx ⊔ Term t2 _ = Term (Ctx.lub ctx t1 t2) ctx

instance CoComplete Term where
  Term t1 ctx ⊓ Term t2 _ = Term (Ctx.glb ctx t1 t2) ctx

instance UpperBounded Term where
  top = Term Top Ctx.empty

convertToList :: [Term] -> Context -> Term
convertToList [] ctx = Term (List Bottom) ctx
convertToList ts ctx = Term (List (sort $ lub ts)) ctx

isLexical :: Term -> Bool
isLexical (Term s ctx) = Ctx.isLexical ctx s

isNumeric :: Term -> Bool
isNumeric (Term s ctx) = Ctx.isNumerical ctx s

isList :: Term -> Bool
isList (Term s ctx) = Ctx.isList ctx s

getListElem :: Term -> Term
getListElem (Term s ctx) = Term (Ctx.getListElem ctx s) ctx

isTuple :: Term -> Int -> Bool
isTuple (Term s ctx) i = Ctx.isTuple ctx i s

isSingleton :: Term -> Bool
isSingleton (Term s ctx) = Ctx.isSingleton ctx s

sortsToTerms :: [Sort] -> Context -> [Term]
sortsToTerms ss ctx = map (`Term` ctx) ss

typeMismatch :: (ArrowFail e c, Fail.Join a c, IsString e) => c (String,String) a
typeMismatch = lmap (\(expected,actual) -> printf "expected type %s but got type %s" (show expected) (show actual)) typeError

typeError :: (ArrowFail e c, Fail.Join a c, IsString e) => c String a
typeError = lmap fromString fail

-- alphaTerm :: Context -> C.Pow C.Term -> Term
-- alphaTerm ctx = lub . fmap (toSort ctx)

-- alphaEnv :: Context -> C.Pow C.TermEnv -> TermEnv
-- alphaEnv ctx = lub . fmap (\(C.TermEnv e) -> S.fromList (M.toList (fmap (toSort ctx) e)))

-- alphaErr :: (Complete e', Complete x') => (e -> e') -> (x -> x') -> C.Pow (CF.Failure String (CE.Error e x)) -> Failure String (Error e' x')
-- alphaErr f g = lub . fmap (\er -> case er of
--   CF.Fail msg -> F.Fail msg
--   CF.Success (CE.Fail x) -> F.Success (E.Fail (f x))
--   CF.Success (CE.Success x) -> F.Success (E.Success (g x)))

-- instance Soundness (StratEnv,Context) (Interp (SW.Categories (Strat,StratEnv) (TermEnv,Term) SW.Stack)) where
--  sound (senv,ctx) xs f g = forAll (choose (0,3)) $ \i -> forAll (choose (3,5)) $ \j -> 
--    let con :: Terminating (FreeCompletion (Failure String (Error () (TermEnv,_))))
--        con = Terminating (Lower (
--                  alphaErr P.id ((alphaEnv ctx . return) *** alphaSing) (fmap (\(x,tenv) -> C.runInterp f senv tenv x) xs)))
--        abst :: Terminating (FreeCompletion (Failure String (Error () (TermEnv,_))))
--        abst = runInterp g i j senv ctx (alphaEnv ctx (fmap snd xs)) (alpha (fmap fst xs))
--    in counterexample (printf "%s ⊑/ %s" (show con) (show abst)) $ con ⊑ abst
