{-# 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 = forall rec fld. Field rec fld -> fld -> rec -> rec
fset Field rec fld
field (fld -> fld
f forall a b. (a -> b) -> a -> b
$ 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 = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id 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 = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field (b -> c
g2 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 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 = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ 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 = forall s (m :: * -> *) a.
MonadState s m =>
Field s a -> (a -> a) -> m ()
fmodifyState Field s a
field (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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ 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 = 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 -> forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n a
x
Maybe a
Nothing -> 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 = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field (forall a. a -> Maybe a -> a
fromMaybe a
dflt) (forall a b. a -> b -> a
const forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. a -> Maybe a
Just)
ist_optimisation :: Name -> Field IState OptInfo
ist_optimisation :: Name -> Field IState OptInfo
ist_optimisation Name
n =
forall a. a -> Field (Maybe a) a
maybe_default Optimise
{ inaccessible :: [(Int, Name)]
inaccessible = []
, detaggable :: Bool
detaggable = Bool
False
, forceable :: [Int]
forceable = []
}
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 :: Ctxt OptInfo
idris_optimisation = Ctxt OptInfo
v })
opt_inaccessible :: Field OptInfo [(Int, Name)]
opt_inaccessible :: Field OptInfo [(Int, Name)]
opt_inaccessible = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field OptInfo -> [(Int, Name)]
inaccessible (\[(Int, Name)]
v OptInfo
opt -> OptInfo
opt{ inaccessible :: [(Int, Name)]
inaccessible = [(Int, Name)]
v })
opt_detaggable :: Field OptInfo Bool
opt_detaggable :: Field OptInfo Bool
opt_detaggable = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field OptInfo -> Bool
detaggable (\Bool
v OptInfo
opt -> OptInfo
opt{ detaggable :: Bool
detaggable = Bool
v })
opt_forceable :: Field OptInfo [Int]
opt_forceable :: Field OptInfo [Int]
opt_forceable = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field OptInfo -> [Int]
forceable (\[Int]
v OptInfo
opt -> OptInfo
opt{ forceable :: [Int]
forceable = [Int]
v })
ist_callgraph :: Name -> Field IState CGInfo
ist_callgraph :: Name -> Field IState CGInfo
ist_callgraph Name
n =
forall a. a -> Field (Maybe a) a
maybe_default CGInfo
{ calls :: [Name]
calls = [], allCalls :: Maybe [Name]
allCalls = forall a. Maybe a
Nothing, scg :: [SCGEntry]
scg = [], usedpos :: [(Int, [UsageReason])]
usedpos = []
}
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. Name -> Field (Ctxt a) (Maybe a)
ctxt_lookup Name
n
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 :: Ctxt CGInfo
idris_callgraph = Ctxt CGInfo
v })
cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
cg_usedpos = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field CGInfo -> [(Int, [UsageReason])]
usedpos (\[(Int, [UsageReason])]
v CGInfo
cg -> CGInfo
cg{ usedpos :: [(Int, [UsageReason])]
usedpos = [(Int, [UsageReason])]
v })
opts_idrisCmdline :: Field IState [Opt]
opts_idrisCmdline :: Field IState [Opt]
opts_idrisCmdline =
forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IOption -> [Opt]
opt_cmdline (\[Opt]
v IOption
opts -> IOption
opts{ opt_cmdline :: [Opt]
opt_cmdline = [Opt]
v })
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> IOption
idris_options (\IOption
v IState
ist -> IState
ist{ idris_options :: IOption
idris_options = IOption
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 = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field (Context
-> Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
definitions 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 :: Context
tt_ctxt = (IState -> Context
tt_ctxt IState
state) {definitions :: Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
definitions = Ctxt
(Def, RigCount, Bool, Accessibility, Totality, MetaInformation)
v}})
known_interfaces :: Field IState (Ctxt InterfaceInfo)
known_interfaces :: Field IState (Ctxt InterfaceInfo)
known_interfaces = 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 :: Ctxt InterfaceInfo
idris_interfaces = IState -> Ctxt InterfaceInfo
idris_interfaces IState
state})
repl_definitions :: Field IState [Name]
repl_definitions :: Field IState [Name]
repl_definitions = 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 :: [Name]
idris_repl_defs = [Name]
v})
idris_fixities :: Field IState [FixDecl]
idris_fixities :: Field IState [FixDecl]
idris_fixities = forall rec fld.
(rec -> fld) -> (fld -> rec -> rec) -> Field rec fld
Field IState -> [FixDecl]
idris_infixes (\[FixDecl]
v IState
state -> IState
state {idris_infixes :: [FixDecl]
idris_infixes = [FixDecl]
v})