{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}

module Language.Haskell.Liquid.Synthesize.Termination (
    decrType
  ) where

import           Language.Haskell.Liquid.Types
import qualified Language.Haskell.Liquid.Types.RefType
                                               as R
import qualified Language.Fixpoint.Types       as F
import           Var

decrType :: Var -> SpecType -> [Var] -> [(F.Symbol, SpecType)] -> SpecType
decrType :: Var -> SpecType -> [Var] -> [(Symbol, SpecType)] -> SpecType
decrType Var
_x SpecType
ti [Var]
xs [(Symbol, SpecType)]
_xts =
  [Var] -> SpecType -> SpecType
forall a. Symbolic a => [a] -> SpecType -> SpecType
go [Var]
xs SpecType
ti 
  where
    go :: [a] -> SpecType -> SpecType
go (a
v:[a]
_) (RFun Symbol
x SpecType
tx SpecType
t RReft
r) 
      | HashSet TyCon -> [RTyVar] -> SpecType -> Bool
isDecreasing HashSet TyCon
forall a. Monoid a => a
mempty [RTyVar]
forall a. Monoid a => a
mempty SpecType
tx  = let Left (Symbol
x', SpecType
tx') = HashSet TyCon
-> [(a, (Symbol, SpecType))] -> Either (Symbol, SpecType) String
forall a t.
Symbolic a =>
HashSet TyCon
-> [(a, (Symbol, RType RTyCon t RReft))]
-> Either (Symbol, RType RTyCon t RReft) String
R.makeDecrType HashSet TyCon
forall a. Monoid a => a
mempty [(a
v,(Symbol
x,SpecType
tx))] 
                                         in  Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' SpecType
tx' SpecType
t RReft
r 
    go (a
_:[a]
vs) (RFun Symbol
x SpecType
tx SpecType
t RReft
r) = Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x SpecType
tx ([a] -> SpecType -> SpecType
go [a]
vs SpecType
t) RReft
r
    go [a]
vs (RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
x) = RTVU RTyCon RTyVar -> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
a ([a] -> SpecType -> SpecType
go [a]
vs SpecType
t) RReft
x
    go [a]
_     SpecType
t = SpecType
t