ASTUtils.hs

module Idris.ASTUtils where

-- 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.

import Control.Category
import Control.Applicative
import Control.Monad.State.Class
import Data.Maybe
import Prelude hiding (id, (.))

import Idris.Core.TT
import Idris.AbsSyntaxTree

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
        }
    . 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 })


-- CGInfo
---------

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

-- some fields of the CGInfo record
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 })