{-# LANGUAGE MultiParamTypeClasses #-}
{-|
Module      : Idris.ASTUtils
Description : This implements just a few basic lens-like concepts to ease state updates. Similar to fclabels in approach, just without the extra dependency.

License     : BSD3
Maintainer  : The Idris Community.

This implements just a few basic lens-like concepts to ease state updates.
Similar to fclabels in approach, just without the extra dependency.

We don't include an explicit export list
because everything here is meant to be exported.

Short synopsis:
---------------
@
f :: Idris ()
f = do
     -- these two steps:
     detaggable <- fgetState (opt_detaggable . ist_optimisation typeName)
     fputState (opt_detaggable . ist_optimisation typeName) (not detaggable)

     -- are equivalent to:
     fmodifyState (opt_detaggable . ist_optimisation typeName) not

     -- of course, the long accessor can be put in a variable;
     -- everything is first-class
     let detag n = opt_detaggable . ist_optimisation n
     fputState (detag n1) True
     fputState (detag n2) False

     -- Note that all these operations handle missing items consistently
     -- and transparently, as prescribed by the default values included
     -- in the definitions of the ist_* functions.
     --
     -- Especially, it's no longer necessary to have initial values of
     -- data structures copied (possibly inconsistently) all over the compiler.
@
-}
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

-- | Exact-name context lookup; uses Nothing for deleted values
-- (read+write!).
--
-- Reading a non-existing value yields Nothing,
-- writing Nothing deletes the value (if it existed).
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-lens with a default value.
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)


-----------------------------------
-- Individual records and fields --
-----------------------------------
--
-- These could probably be generated; let's use lazy addition for now.
--


-- OptInfo
----------

-- | the optimisation record for the given (exact) name
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 })

-- | two fields of the optimisation record
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 })

-- | callgraph record for the given (exact) name
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 })

-- | Commandline flags
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 })

-- | TT Context
--
-- This has a terrible name, but I'm not sure of a better one that
-- isn't confusingly close to tt_ctxt
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})


-- | Names defined at the repl
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})

-- | Fixity declarations in an IState
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})