git.iko.soy/Idris-dev
on master help sign in
Don't project record parameters

They're already in the right form (guaranteed by the types of the other projections), and relying on projecting them means that they must be in canonical form to get things to type check. Without record eta rules, this is somewhat onerous.

commit37ebed39bf77d2cc8f3d7d1058077f4e03c64a24 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 5 May 2015, 21:16 (11 years ago) parent274b6b1
2 files changed+7−9
compare with master
unifiedsplit
libs/base/Control/Monad/State.idr+3−7 src/Idris/Elab/Record.hs+4−2
libs/base/Control/Monad/State.idr+3−7
@@ -15,10 +15,7 @@ class Monad m => MonadState s (m : Type -> Type) | m where
1515||| The transformer on which the State monad is based
1616record StateT (s : Type) (m : Type -> Type) (a : Type) where
1717 constructor ST
18− runStateT' : s -> m (a, s)
19−
20−runStateT : StateT s m a -> s -> m (a, s)
21−runStateT (ST run) = run
18+ runStateT : s -> m (a, s)
2219
2320instance Functor f => Functor (StateT s f) where
2421 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
@@ -60,9 +57,8 @@ State : Type -> Type -> Type
6057State s a = StateT s Identity a
6158
6259||| Unwrap a State monad computation.
63−runState : StateT s Identity a -> s -> (a,s)
64−runState (ST fun) init = case fun init of
65− Id x => x
60+runState : StateT s Identity a -> s -> (a, s)
61+runState act = runIdentity . runStateT act
6662
6763||| Unwrap a State monad computation, but discard the final state.
6864evalState : State s a -> s -> a
src/Idris/Elab/Record.hs+4−2
@@ -241,14 +241,16 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
241241 paramName (UN n) = sUN ("param_" ++ str n)
242242 paramName (MN i n) = sMN i ("param_" ++ str n)
243243 paramName (NS n s) = NS (paramName n) s
244− paramName n = n
244+ paramName n = n
245245
246246 -- | Elaborate the projection functions.
247247 elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
248248 elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]
249249 elab = \(n, n', p, t, doc, i) ->
250250 -- Use projections in types
251− do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs] t
251+ do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs
252+ -- Parameters are already in scope, so just use them
253+ , not (m `elem` paramNames)] t
252254 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i
253255 in mapM_ elab fs
254256