git.iko.soy/Idris-dev
on master help sign in
Add ASTUtils.
bb6873cMatus Tejiscak
idris.cabal+1
compare with master
unifiedsplit
@@ -456,6 +456,7 @@ Library
456 , Idris.AbsSyntax
456 , Idris.AbsSyntax
457 , Idris.AbsSyntaxTree
457 , Idris.AbsSyntaxTree
458 , Idris.Apropos
458 , Idris.Apropos
459+ , Idris.ASTUtils
459 , Idris.CaseSplit
460 , Idris.CaseSplit
460 , Idris.Chaser
461 , Idris.Chaser
461 , Idris.Colours
462 , Idris.Colours
src/Idris/ASTUtils.hsnew file+62
@@ -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 })
src/Idris/Core/TT.hs+1
@@ -383,6 +383,7 @@ implicitable _ = False
383nsroot (NS n _) = n
383nsroot (NS n _) = n
384nsroot n = n
384nsroot n = n
385
385
386+-- this will overwrite already existing definitions
386addDef :: Name -> a -> Ctxt a -> Ctxt a
387addDef :: Name -> a -> Ctxt a -> Ctxt a
387addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
388addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
388 Nothing -> Map.insert (nsroot n)
389 Nothing -> Map.insert (nsroot n)
src/Idris/ElabDecls.hs+5−5
@@ -88,7 +88,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
88 let ty = addImpl i ty'
88 let ty = addImpl i ty'
89 inacc = inaccessibleArgs 0 ty
89 inacc = inaccessibleArgs 0 ty
90 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
90 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
91− logLvl 5 $ "Inaccessible arguments: " ++ show inacc
91+ logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc
92
92
93 ((tyT, defer, is), log) <-
93 ((tyT, defer, is), log) <-
94 tclift $ elaborate ctxt n (TType (UVal 0)) []
94 tclift $ elaborate ctxt n (TType (UVal 0)) []
@@ -182,12 +182,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
182saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
182saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()
183saveInaccArgs n is = do
183saveInaccArgs n is = do
184 ist <- getIState
184 ist <- getIState
185− case lookupCtxt n (idris_optimisation ist) of
185+ case lookupCtxtExact n (idris_optimisation ist) of
186− [oi] -> do
186+ Just oi -> do
187 putIState ist{ idris_optimisation =
187 putIState ist{ idris_optimisation =
188 addDef n oi{ inaccessible = is } (idris_optimisation ist) }
188 addDef n oi{ inaccessible = is } (idris_optimisation ist) }
189
189
190− _ -> do
190+ Nothing -> do
191 putIState ist{ idris_optimisation =
191 putIState ist{ idris_optimisation =
192 addDef n (Optimise is False) (idris_optimisation ist) }
192 addDef n (Optimise is False) (idris_optimisation ist) }
193 addIBC (IBCOpt n)
193 addIBC (IBCOpt n)
@@ -195,7 +195,7 @@ saveInaccArgs n is = do
195-- Get the list of (index, name) of inaccessible arguments from the type.
195-- Get the list of (index, name) of inaccessible arguments from the type.
196inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
196inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
197inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
197inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)
198− = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
198+ = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
199inaccessibleArgs i (PPi plicity n ty t)
199inaccessibleArgs i (PPi plicity n ty t)
200 | InaccessibleArg `elem` pargopts plicity
200 | InaccessibleArg `elem` pargopts plicity
201 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
201 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}