{-# LANGUAGE MultiParamTypeClasses #-}
module Idris.ASTUtils(
Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState
, fputState, idris_fixities, ist_callgraph, ist_optimisation
, known_interfaces, known_terms, opt_detaggable, opt_inaccessible
, opt_forceable, opts_idrisCmdline, repl_definitions
) where
import Idris.AbsSyntaxTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Options
import Prelude hiding (id, (.))
import Control.Category
import Control.Monad.State.Class
import Data.Maybe
data Field rec fld = Field
{ forall rec fld. Field rec fld -> rec -> fld
fget :: rec -> fld
, forall rec fld. Field rec fld -> fld -> rec -> rec
fset :: fld -> rec -> rec
}
fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
fmodify :: forall rec fld. Field rec fld -> (fld -> fld) -> rec -> rec
fmodify Field rec fld
field fld -> fld
f rec
x = Field rec fld -> fld -> rec -> rec
forall rec fld. Field rec fld -> fld -> rec -> rec
fset Field rec fld
field (fld -> fld
f (fld -> fld) -> fld -> fld
forall a b. (a -> b) -> a -> b
$ Field rec fld -> rec -> fld
forall rec fld. Field rec fld -> rec -> fld
fget Field rec fld
field rec
x) rec
x
instance Category Field where
id :: forall a. Field a a
id = (a -> a) -> (a -> a -> a) -> Field a a
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field a -> a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id a -> a -> a
forall a b. a -> b -> a
const
Field b -> c
g2 c -> b -> b
s2 . :: forall b c a. Field b c -> Field a b -> Field a c
. Field a -> b
g1 b -> a -> a
s1 = (a -> c) -> (c -> a -> a) -> Field a c
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field (b -> c
g2 (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> b
g1) (\c
v2 a
x1 -> b -> a -> a
s1 (c -> b -> b
s2 c
v2 (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ a -> b
g1 a
x1) a
x1)
fgetState :: MonadState s m => Field s a -> m a
fgetState :: forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState Field s a
field = (s -> a) -> m a
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((s -> a) -> m a) -> (s -> a) -> m a
forall a b. (a -> b) -> a -> b
$ Field s a -> s -> a
forall rec fld. Field rec fld -> rec -> fld
fget Field s a
field
fputState :: MonadState s m => Field s a -> a -> m ()
fputState :: forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState Field s a
field a
x = Field s a -> (a -> a) -> m ()
forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field s a
field (a -> a -> a
forall a b. a -> b -> a
const a
x)
fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
fmodifyState :: forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field s a
field a -> a
f = (s -> s) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((s -> s) -> m ()) -> (s -> s) -> m ()
forall a b. (a -> b) -> a -> b
$ Field s a -> (a -> a) -> s -> s
forall rec fld. Field rec fld -> (fld -> fld) -> rec -> rec
fmodify Field s a
field a -> a
f
ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup :: forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n = Field
{ fget :: Ctxt a -> Maybe a
fget = Name -> Ctxt a -> Maybe a
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n
, fset :: Maybe a -> Ctxt a -> Ctxt a
fset = \Maybe a
newVal -> case Maybe a
newVal of
Just a
x -> Name -> a -> Ctxt a -> Ctxt a
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n a
x
Maybe a
Nothing -> Name -> Ctxt a -> Ctxt a
forall a. Name -> Ctxt a -> Ctxt a
deleteDefExact Name
n
}
maybe_default :: a -> Field (Maybe a) a
maybe_default :: forall a. a -> Field (Maybe a) a
maybe_default a
dflt = (Maybe a -> a) -> (a -> Maybe a -> Maybe a) -> Field (Maybe a) a
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
dflt) (Maybe a -> Maybe a -> Maybe a
forall a b. a -> b -> a
const (Maybe a -> Maybe a -> Maybe a)
-> (a -> Maybe a) -> a -> Maybe a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Maybe a
forall a. a -> Maybe a
Just)
ist_optimisation :: Name -> Field IState OptInfo
ist_optimisation :: Name -> Field IState OptInfo
ist_optimisation Name
n =
OptInfo -> Field (Maybe OptInfo) OptInfo
forall a. a -> Field (Maybe a) a
maybe_default Optimise
{ inaccessible :: [(Int, Name)]
inaccessible = []
, detaggable :: Bool
detaggable = Bool
False
, forceable :: [Int]
forceable = []
}
Field (Maybe OptInfo) OptInfo
-> Field IState (Maybe OptInfo) -> Field IState OptInfo
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field (Ctxt OptInfo) (Maybe OptInfo)
forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n
Field (Ctxt OptInfo) (Maybe OptInfo)
-> Field IState (Ctxt OptInfo) -> Field IState (Maybe OptInfo)
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> Ctxt OptInfo)
-> (Ctxt OptInfo -> IState -> IState)
-> Field IState (Ctxt OptInfo)
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> Ctxt OptInfo
idris_optimisation (\Ctxt OptInfo
v IState
ist -> IState
ist{ idris_optimisation = v })
opt_inaccessible :: Field OptInfo [(Int, Name)]
opt_inaccessible :: Field OptInfo [(Int, Name)]
opt_inaccessible = (OptInfo -> [(Int, Name)])
-> ([(Int, Name)] -> OptInfo -> OptInfo)
-> Field OptInfo [(Int, Name)]
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field OptInfo -> [(Int, Name)]
inaccessible (\[(Int, Name)]
v OptInfo
opt -> OptInfo
opt{ inaccessible = v })
opt_detaggable :: Field OptInfo Bool
opt_detaggable :: Field OptInfo Bool
opt_detaggable = (OptInfo -> Bool)
-> (Bool -> OptInfo -> OptInfo) -> Field OptInfo Bool
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field OptInfo -> Bool
detaggable (\Bool
v OptInfo
opt -> OptInfo
opt{ detaggable = v })
opt_forceable :: Field OptInfo [Int]
opt_forceable :: Field OptInfo [Int]
opt_forceable = (OptInfo -> [Int])
-> ([Int] -> OptInfo -> OptInfo) -> Field OptInfo [Int]
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field OptInfo -> [Int]
forceable (\[Int]
v OptInfo
opt -> OptInfo
opt{ forceable = v })
ist_callgraph :: Name -> Field IState CGInfo
ist_callgraph :: Name -> Field IState CGInfo
ist_callgraph Name
n =
CGInfo -> Field (Maybe CGInfo) CGInfo
forall a. a -> Field (Maybe a) a
maybe_default CGInfo
{ calls :: [Name]
calls = [], allCalls :: Maybe [Name]
allCalls = Maybe [Name]
forall a. Maybe a
Nothing, scg :: [SCGEntry]
scg = [], usedpos :: [(Int, [UsageReason])]
usedpos = []
}
Field (Maybe CGInfo) CGInfo
-> Field IState (Maybe CGInfo) -> Field IState CGInfo
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field (Ctxt CGInfo) (Maybe CGInfo)
forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n
Field (Ctxt CGInfo) (Maybe CGInfo)
-> Field IState (Ctxt CGInfo) -> Field IState (Maybe CGInfo)
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> Ctxt CGInfo)
-> (Ctxt CGInfo -> IState -> IState) -> Field IState (Ctxt CGInfo)
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> Ctxt CGInfo
idris_callgraph (\Ctxt CGInfo
v IState
ist -> IState
ist{ idris_callgraph = v })
cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
cg_usedpos = (CGInfo -> [(Int, [UsageReason])])
-> ([(Int, [UsageReason])] -> CGInfo -> CGInfo)
-> Field CGInfo [(Int, [UsageReason])]
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field CGInfo -> [(Int, [UsageReason])]
usedpos (\[(Int, [UsageReason])]
v CGInfo
cg -> CGInfo
cg{ usedpos = v })
opts_idrisCmdline :: Field IState [Opt]
opts_idrisCmdline :: Field IState [Opt]
opts_idrisCmdline =
(IOption -> [Opt])
-> ([Opt] -> IOption -> IOption) -> Field IOption [Opt]
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IOption -> [Opt]
opt_cmdline (\[Opt]
v IOption
opts -> IOption
opts{ opt_cmdline = v })
Field IOption [Opt] -> Field IState IOption -> Field IState [Opt]
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (IState -> IOption)
-> (IOption -> IState -> IState) -> Field IState IOption
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> IOption
idris_options (\IOption
v IState
ist -> IState
ist{ idris_options = v })
known_terms :: Field IState (Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))
known_terms :: Field
IState
(Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
known_terms = (IState
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> (Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
-> IState -> IState)
-> Field
IState
(Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field (Context
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
definitions (Context
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation))
-> (IState -> Context)
-> IState
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Context
tt_ctxt)
(\Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
v IState
state -> IState
state {tt_ctxt = (tt_ctxt state) {definitions = v}})
known_interfaces :: Field IState (Ctxt InterfaceInfo)
known_interfaces :: Field IState (Ctxt InterfaceInfo)
known_interfaces = (IState -> Ctxt InterfaceInfo)
-> (Ctxt InterfaceInfo -> IState -> IState)
-> Field IState (Ctxt InterfaceInfo)
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> Ctxt InterfaceInfo
idris_interfaces (\Ctxt InterfaceInfo
v IState
state -> IState
state {idris_interfaces = idris_interfaces state})
repl_definitions :: Field IState [Name]
repl_definitions :: Field IState [Name]
repl_definitions = (IState -> [Name])
-> ([Name] -> IState -> IState) -> Field IState [Name]
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> [Name]
idris_repl_defs (\[Name]
v IState
state -> IState
state {idris_repl_defs = v})
idris_fixities :: Field IState [FixDecl]
idris_fixities :: Field IState [FixDecl]
idris_fixities = (IState -> [FixDecl])
-> ([FixDecl] -> IState -> IState) -> Field IState [FixDecl]
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> [FixDecl]
idris_infixes (\[FixDecl]
v IState
state -> IState
state {idris_infixes = v})