@@ -5,9 +5,7 @@ import Idris.AbsSyntax
55import Idris.Docstrings
66import Idris.Error
77import Idris.Delaborate
8−
9−import Idris.ParseExpr -- Remove me
10−
8+import Idris.ParseExpr
119import Idris.Core.TT
1210import Idris.Core.Evaluate
1311
@@ -17,10 +15,6 @@ import Data.Maybe
1715import Data.List
1816import Control.Monad
1917
20−-- TODO:
21−-- Consider what to do about type parameters in projection that do not occur as a parameter.
22−-- I.e. set_bar : Foo n -> Vect n a
23−
2418elabRecord :: ElabInfo ->
2519 (Docstring (Either Err PTerm)) ->
2620 SyntaxInfo ->
@@ -42,7 +36,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
4236 logLvl 4 $ "Type constructor " ++ showTmImpls tycon
4337
4438 -- Data constructor
45− dconName <- liftM (expandNS csyn) $ generateDConName cname
39+ dconName <- generateDConName cname
4640 let dcon = generateDCon params fields
4741 logLvl 4 $ "Data constructor: " ++ showTmImpls dcon
4842
@@ -60,19 +54,22 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
6054
6155 -- The arguments to the constructor
6256 let constructorArgs = getArgTys ttCons
57+ -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
58+ let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
59+
6360 -- The parameters for elaboration with their documentation
64− paramsForElab = [((nsroot n), (param_name n), impl, t, d) | (n, t, d) <- zip' i params paramDocs]
65− -- If elaborating the constructor has resulted in some new implicit fields we make a projeciton functions for them.
66− freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
61+ let paramsForElab = [((nsroot n), (param_name n), impl, t, d) | (n, t, d) <- zip' i params paramDocs]
62+
6763 -- The fields (written by the user) with their documentation.
68− userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
69− -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
70− fieldsForElab = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
64+ let userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
65+
66+ -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
67+ let fieldsForElab = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
7168
7269 -- Build projection functions
7370 elabProj dconName fieldsForElab
7471 -- Build update functions
75− elabUp dconName fieldsForElab -- [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
72+ elabUp dconName [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
7673 where
7774 -- | Generates a type constructor.
7875 generateTyCon :: [(Name, Plicity, PTerm)] -> PTerm
@@ -116,7 +113,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
116113 paramNames = [nsroot n | (n, _, _) <- params]
117114
118115 isFieldOrParam :: Name -> Bool
119− isFieldOrParam = flip elem (fieldNames ++ paramNames)
116+ isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
120117
121118 isFieldOrParam' :: (Name, a) -> Bool
122119 isFieldOrParam' = isFieldOrParam . fst
@@ -245,7 +242,7 @@ elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames in
245242 -- | The left hand side of the projection function.
246243 generateLhs :: PTerm
247244 generateLhs = let args = lhsArgs index phArgs
248− in PApp fc (PRef fc pname) [pexp (PApp fc (PRef fc cn) args)]
245+ in PApp fc (PRef fc pname) [pexp (PApp fc (PRef fc cn) args)]
249246 where
250247 lhsArgs :: Int -> [PArg] -> [PArg]
251248 lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest