{-# 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
    { fget :: rec -> fld
    , fset :: fld -> rec -> rec
    }

fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
fmodify field f x = fset field (f $ fget field x) x

instance Category Field where
    id = Field id const
    Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)

fgetState :: MonadState s m => Field s a -> m a
fgetState field = gets $ fget field

fputState :: MonadState s m => Field s a -> a -> m ()
fputState field x = fmodifyState field (const x)

fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
fmodifyState field f = modify $ fmodify field 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 n = Field
    { fget = lookupCtxtExact n
    , fset = \newVal -> case newVal of
        Just x  -> addDef n x
        Nothing -> deleteDefExact n
    }

-- Maybe-lens with a default value.
maybe_default :: a -> Field (Maybe a) a
maybe_default dflt = Field (fromMaybe dflt) (const . 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 n =
      maybe_default Optimise
        { inaccessible = []
        , detaggable = False
        , forceable = []
        }
    . ctxt_lookup n
    . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

-- | two fields of the optimisation record
opt_inaccessible :: Field OptInfo [(Int, Name)]
opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })

opt_detaggable :: Field OptInfo Bool
opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

opt_forceable :: Field OptInfo [Int]
opt_forceable = Field forceable (\v opt -> opt{ forceable = v })

-- | callgraph record for the given (exact) name
ist_callgraph :: Name -> Field IState CGInfo
ist_callgraph n =
      maybe_default CGInfo
        { calls = [], allCalls = Nothing, scg = [], usedpos = []
        }
    . ctxt_lookup n
    . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

cg_usedpos :: Field CGInfo [(Int, [UsageReason])]
cg_usedpos = Field usedpos (\v cg -> cg{ usedpos = v })

-- | Commandline flags
opts_idrisCmdline :: Field IState [Opt]
opts_idrisCmdline =
      Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })
    . Field idris_options (\v ist -> 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 (definitions . tt_ctxt)
                    (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

known_interfaces :: Field IState (Ctxt InterfaceInfo)
known_interfaces = Field idris_interfaces (\v state -> state {idris_interfaces = idris_interfaces state})


-- | Names defined at the repl
repl_definitions :: Field IState [Name]
repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})

-- | Fixity declarations in an IState
idris_fixities :: Field IState [FixDecl]
idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})