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 (join)

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           Language.Haskell.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) <- ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs
              , RILaws LocBareType
rilaw <- BareSpec -> [RILaws LocBareType]
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 :: Class
-> [LocSpecType]
-> [LocSpecType]
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
-> SrcSpan
-> LawInstance
LawInstance
  { lilName :: Class
lilName   = Class -> Maybe Class -> Class
forall a. a -> Maybe a -> a
Mb.fromMaybe Class
forall a. a
errmsg Maybe Class
tc
  , liSupers :: [LocSpecType]
liSupers  = LocBareType -> LocSpecType
mkTy (LocBareType -> LocSpecType) -> [LocBareType] -> [LocSpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RILaws LocBareType -> [LocBareType]
forall ty. RILaws ty -> [ty]
rilSupers RILaws LocBareType
rilaw 
  , lilTyArgs :: [LocSpecType]
lilTyArgs = LocBareType -> LocSpecType
mkTy (LocBareType -> LocSpecType) -> [LocBareType] -> [LocSpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RILaws LocBareType -> [LocBareType]
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)<- RILaws LocBareType -> [(LocSymbol, LocSymbol)]
forall ty. RILaws ty -> [(LocSymbol, LocSymbol)]
rilEqus RILaws LocBareType
rilaw ]  
  , lilPos :: SrcSpan
lilPos    = SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located () -> SourcePos
forall a. Located a -> SourcePos
loc (Located () -> SourcePos) -> Located () -> SourcePos
forall a b. (a -> b) -> a -> b
$ RILaws LocBareType -> Located ()
forall ty. RILaws ty -> Located ()
rilPos RILaws LocBareType
rilaw
  } 
  where
    tc    :: Maybe Class 
    tc :: Maybe Class
tc     = BTyCon -> Maybe Class
classTc (RILaws LocBareType -> BTyCon
forall ty. RILaws ty -> BTyCon
rilName RILaws LocBareType
rilaw)
    errmsg :: a
errmsg = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"Not a type class: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe Class -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Maybe Class
tc)

    classTc :: BTyCon -> Maybe Class
classTc = Maybe (Maybe Class) -> Maybe Class
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe Class) -> Maybe Class)
-> (BTyCon -> Maybe (Maybe Class)) -> BTyCon -> Maybe Class
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Maybe Class) -> Maybe TyCon -> Maybe (Maybe Class)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCon -> Maybe Class
tyConClass_maybe (Maybe TyCon -> Maybe (Maybe Class))
-> (BTyCon -> Maybe TyCon) -> BTyCon -> Maybe (Maybe Class)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> [Char] -> LocSymbol -> Maybe TyCon
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"makeClass" (LocSymbol -> Maybe TyCon)
-> (BTyCon -> LocSymbol) -> BTyCon -> Maybe TyCon
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 PlugTV Var
forall v. PlugTV v
Bare.GenTV 
    mkVar :: LocSymbol -> VarOrLocSymbol 
    mkVar :: LocSymbol -> VarOrLocSymbol
mkVar LocSymbol
x = case Env -> ModName -> [Char] -> LocSymbol -> Maybe Var
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"makeInstanceLaw" LocSymbol
x of 
                Just Var
v -> Var -> VarOrLocSymbol
forall a b. a -> Either a b
Left Var
v 
                Maybe Var
_      -> LocSymbol -> VarOrLocSymbol
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 -> (Var -> VarOrLocSymbol
forall a b. a -> Either a b
Left Var
x, LocSpecType -> Maybe LocSpecType
forall a. a -> Maybe a
Just (LocSpecType -> Maybe LocSpecType)
-> LocSpecType -> Maybe LocSpecType
forall a b. (a -> b) -> a -> b
$ LocSpecType -> Maybe LocSpecType -> LocSpecType
forall a. a -> Maybe a -> a
Mb.fromMaybe (RRType RReft -> LocSpecType
forall a. a -> Located a
dummyLoc (RRType RReft -> LocSpecType) -> RRType RReft -> LocSpecType
forall a b. (a -> b) -> a -> b
$ Type -> RRType RReft
forall r. Monoid r => Type -> RRType r
ofType (Type -> RRType RReft) -> Type -> RRType RReft
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) (Var -> [(Var, LocSpecType)] -> Maybe LocSpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Var
x [(Var, LocSpecType)]
sigs))
                     Right LocSymbol
x -> (LocSymbol -> VarOrLocSymbol
forall a b. b -> Either a b
Right LocSymbol
x, Maybe LocSpecType
forall a. Maybe a
Nothing)