@@ -0,0 +1,62 @@
1+module Idris.ASTUtils where
2+
3+-- This implements just a few basic lens-like concepts to ease state updates.
4+-- Similar to fclabels in approach, just without the extra dependency.
5+--
6+-- We don't include an explicit export list
7+-- because everything here is meant to be exported.
8+
9+import Control.Category
10+import Control.Applicative
11+import Control.Monad.State.Class
12+import Data.Maybe
13+import Prelude hiding (id, (.))
14+
15+import Idris.Core.TT
16+import Idris.AbsSyntaxTree
17+
18+data Field rec fld = Field
19+ { fget :: rec -> fld
20+ , fset :: fld -> rec -> rec
21+ }
22+
23+fmodify :: Field rec fld -> (fld -> fld) -> rec -> rec
24+fmodify field f x = fset field (f $ fget field x) x
25+
26+instance Category Field where
27+ id = Field id const
28+ Field g2 s2 . Field g1 s1 = Field (g2 . g1) (\v2 x1 -> s1 (s2 v2 $ g1 x1) x1)
29+
30+fgetState :: MonadState s m => Field s a -> m a
31+fgetState field = gets $ fget field
32+
33+fputState :: MonadState s m => Field s a -> a -> m ()
34+fputState field x = fmodifyState field (const x)
35+
36+fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
37+fmodifyState field f = modify $ fmodify field f
38+
39+class InitialValue a where
40+ initialValue :: a
41+
42+ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
43+ctxt_lookupExact n = Field
44+ { fget = fromMaybe initialValue . lookupCtxtExact n
45+ , fset = addDef n
46+ }
47+
48+-----------------------------------
49+-- Individual records and fields --
50+-----------------------------------
51+
52+instance InitialValue OptInfo where
53+ initialValue = Optimise [] False
54+
55+ist_optimisation :: Field IState (Ctxt OptInfo)
56+ist_optimisation = Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
57+
58+opt_inaccessible :: Field OptInfo [(Int, Name)]
59+opt_inaccessible = Field inaccessible (\v opt -> opt{ inaccessible = v })
60+
61+opt_detaggable :: Field OptInfo Bool
62+opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })