module Language.Haskell.Liquid.Bare.Laws ( makeInstanceLaws ) where

import qualified Data.Maybe                                 as Mb
import qualified Data.List                                  as L
import qualified Data.HashMap.Strict                        as M
import           Control.Monad ((<=<))

import qualified Language.Haskell.Liquid.Measure            as Ms
import qualified Language.Fixpoint.Types                    as F
import qualified Language.Haskell.Liquid.GHC.Misc           as GM
import           Language.Haskell.Liquid.Bare.Types         as Bare
import           Language.Haskell.Liquid.Bare.Resolve       as Bare
import           Language.Haskell.Liquid.Bare.Expand        as Bare
import           Language.Haskell.Liquid.Types
import           Liquid.GHC.API



makeInstanceLaws :: Bare.Env -> Bare.SigEnv -> [(Var,LocSpecType)]
                -> Bare.ModSpecs -> [LawInstance]
makeInstanceLaws :: Env -> SigEnv -> [(Var, LocSpecType)] -> ModSpecs -> [LawInstance]
makeInstanceLaws Env
env SigEnv
sigEnv [(Var, LocSpecType)]
sigs ModSpecs
specs
  = [Env
-> SigEnv
-> [(Var, LocSpecType)]
-> ModName
-> RILaws LocBareType
-> LawInstance
makeInstanceLaw Env
env SigEnv
sigEnv [(Var, LocSpecType)]
sigs ModName
name RILaws LocBareType
rilaw
              | (ModName
name, BareSpec
spec) <- forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs
              , RILaws LocBareType
rilaw <- forall ty bndr. Spec ty bndr -> [RILaws ty]
Ms.ilaws BareSpec
spec ]


makeInstanceLaw :: Bare.Env -> Bare.SigEnv -> [(Var,LocSpecType)] -> ModName
                -> RILaws LocBareType -> LawInstance
makeInstanceLaw :: Env
-> SigEnv
-> [(Var, LocSpecType)]
-> ModName
-> RILaws LocBareType
-> LawInstance
makeInstanceLaw Env
env SigEnv
sigEnv [(Var, LocSpecType)]
sigs ModName
name RILaws LocBareType
rilaw = LawInstance
  { lilName :: Class
lilName   = forall a. a -> Maybe a -> a
Mb.fromMaybe forall {a}. a
errmsg Maybe Class
tc
  , liSupers :: [LocSpecType]
liSupers  = LocBareType -> LocSpecType
mkTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty. RILaws ty -> [ty]
rilSupers RILaws LocBareType
rilaw
  , lilTyArgs :: [LocSpecType]
lilTyArgs = LocBareType -> LocSpecType
mkTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty. RILaws ty -> [ty]
rilTyArgs RILaws LocBareType
rilaw
  , lilEqus :: [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus   = [(LocSymbol -> VarOrLocSymbol
mkVar LocSymbol
l, LocSymbol -> (VarOrLocSymbol, Maybe LocSpecType)
mkTypedVar LocSymbol
r) | (LocSymbol
l,LocSymbol
r)<- forall ty. RILaws ty -> [(LocSymbol, LocSymbol)]
rilEqus RILaws LocBareType
rilaw ]
  , lilPos :: SrcSpan
lilPos    = SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc forall a b. (a -> b) -> a -> b
$ forall ty. RILaws ty -> Located ()
rilPos RILaws LocBareType
rilaw
  }
  where
    tc    :: Maybe Class
    tc :: Maybe Class
tc     = BTyCon -> Maybe Class
classTc (forall ty. RILaws ty -> BTyCon
rilName RILaws LocBareType
rilaw)
    errmsg :: a
errmsg = forall a. HasCallStack => [Char] -> a
error ([Char]
"Not a type class: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp Maybe Class
tc)

    classTc :: BTyCon -> Maybe Class
classTc = TyCon -> Maybe Class
tyConClass_maybe forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"makeClass" forall b c a. (b -> c) -> (a -> b) -> a -> c
. BTyCon -> LocSymbol
btc_tc)

    mkTy :: LocBareType -> LocSpecType
    mkTy :: LocBareType -> LocSpecType
mkTy = Env
-> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.GenTV
    mkVar :: LocSymbol -> VarOrLocSymbol
    mkVar :: LocSymbol -> VarOrLocSymbol
mkVar LocSymbol
x = case forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"makeInstanceLaw" LocSymbol
x of
                Just Var
v -> forall a b. a -> Either a b
Left Var
v
                Maybe Var
_      -> forall a b. b -> Either a b
Right LocSymbol
x

    mkTypedVar :: LocSymbol -> (VarOrLocSymbol, Maybe LocSpecType)
    mkTypedVar :: LocSymbol -> (VarOrLocSymbol, Maybe LocSpecType)
mkTypedVar LocSymbol
l = case LocSymbol -> VarOrLocSymbol
mkVar LocSymbol
l of
                     Left Var
x -> (forall a b. a -> Either a b
Left Var
x, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
Mb.fromMaybe (forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall r. Monoid r => Type -> RRType r
ofType forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) (forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Var
x [(Var, LocSpecType)]
sigs))
                     Right LocSymbol
x -> (forall a b. b -> Either a b
Right LocSymbol
x, forall a. Maybe a
Nothing)