git.iko.soy/Idris-dev
on master help sign in
Added records to changelog.
4373184Sune Alkærsig
CHANGELOG+2
compare with master
unifiedsplit
@@ -32,6 +32,8 @@ New in 0.9.17:
32* New REPL command ":core TM" that shows the elaborated form of TM along with
32* New REPL command ":core TM" that shows the elaborated form of TM along with
33 its elaborated type using the syntax of TT. IDE mode has a corresponding
33 its elaborated type using the syntax of TT. IDE mode has a corresponding
34 command :elaborate-term for serialized terms.
34 command :elaborate-term for serialized terms.
35+* Records has a new syntax based on fields rather than constructors.
36+* Records can now be coinductive.
35
37
36
38
37New in 0.9.16:
39New in 0.9.16:
libs/prelude/Prelude/Nat.idr+4−19
@@ -200,30 +200,15 @@ instance Cast Integer Nat where
200 cast = fromInteger
200 cast = fromInteger
201
201
202||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
202||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
203−data Multiplicative : Type where
204− getMultiplicative : Nat -> Multiplicative
205−
206−{-
207record Multiplicative where
203record Multiplicative where
208− multiplicative_n : Nat
209 constructor getMultiplicative
204 constructor getMultiplicative
210−-}
205+ multiplicative_n : Nat
211−{-
206+
212−record Multiplicative : Type where
213− getMultiplicative : Nat -> Multiplicative
214−-}
215||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
207||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
216−data Additive : Type where
217− getAdditive : Nat -> Additive
218−{-
219record Additive where
208record Additive where
220− additive_n : Nat
221 constructor getAdditive
209 constructor getAdditive
222−-}
210+ additive_n : Nat
223−{-
211+
224−record Additive : Type where
225− getAdditive : Nat -> Additive
226−-}
227instance Semigroup Multiplicative where
212instance Semigroup Multiplicative where
228 (<+>) left right = getMultiplicative $ left' * right'
213 (<+>) left right = getMultiplicative $ left' * right'
229 where
214 where
src/Idris/Elab/Record.hs+14−17
@@ -5,9 +5,7 @@ import Idris.AbsSyntax
5import Idris.Docstrings
5import Idris.Docstrings
6import Idris.Error
6import Idris.Error
7import Idris.Delaborate
7import Idris.Delaborate
8−
9−import Idris.ParseExpr -- Remove me
8+import Idris.ParseExpr
10−
11import Idris.Core.TT
9import Idris.Core.TT
12import Idris.Core.Evaluate
10import Idris.Core.Evaluate
13
11
@@ -17,10 +15,6 @@ import Data.Maybe
17import Data.List
15import Data.List
18import Control.Monad
16import Control.Monad
19
17
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−
24elabRecord :: ElabInfo ->
18elabRecord :: ElabInfo ->
25 (Docstring (Either Err PTerm)) ->
19 (Docstring (Either Err PTerm)) ->
26 SyntaxInfo ->
20 SyntaxInfo ->
@@ -42,7 +36,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
42 logLvl 4 $ "Type constructor " ++ showTmImpls tycon
36 logLvl 4 $ "Type constructor " ++ showTmImpls tycon
43
37
44 -- Data constructor
38 -- Data constructor
45− dconName <- liftM (expandNS csyn) $ generateDConName cname
39+ dconName <- generateDConName cname
46 let dcon = generateDCon params fields
40 let dcon = generateDCon params fields
47 logLvl 4 $ "Data constructor: " ++ showTmImpls dcon
41 logLvl 4 $ "Data constructor: " ++ showTmImpls dcon
48
42
@@ -60,19 +54,22 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
60
54
61 -- The arguments to the constructor
55 -- The arguments to the constructor
62 let constructorArgs = getArgTys ttCons
56 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+
63 -- The parameters for elaboration with their documentation
60 -- The parameters for elaboration with their documentation
64− paramsForElab = [((nsroot n), (param_name n), impl, t, d) | (n, t, d) <- zip' i params paramDocs]
61+ let 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.
62+
66− freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
67 -- The fields (written by the user) with their documentation.
63 -- The fields (written by the user) with their documentation.
68− userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
64+ let userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
65+
69− -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
66+ -- 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..]]
67+ let fieldsForElab = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
71
68
72 -- Build projection functions
69 -- Build projection functions
73 elabProj dconName fieldsForElab
70 elabProj dconName fieldsForElab
74 -- Build update functions
71 -- 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..]]
76 where
73 where
77 -- | Generates a type constructor.
74 -- | Generates a type constructor.
78 generateTyCon :: [(Name, Plicity, PTerm)] -> PTerm
75 generateTyCon :: [(Name, Plicity, PTerm)] -> PTerm
@@ -116,7 +113,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
116 paramNames = [nsroot n | (n, _, _) <- params]
113 paramNames = [nsroot n | (n, _, _) <- params]
117
114
118 isFieldOrParam :: Name -> Bool
115 isFieldOrParam :: Name -> Bool
119− isFieldOrParam = flip elem (fieldNames ++ paramNames)
116+ isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
120
117
121 isFieldOrParam' :: (Name, a) -> Bool
118 isFieldOrParam' :: (Name, a) -> Bool
122 isFieldOrParam' = isFieldOrParam . fst
119 isFieldOrParam' = isFieldOrParam . fst
@@ -245,7 +242,7 @@ elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames in
245 -- | The left hand side of the projection function.
242 -- | The left hand side of the projection function.
246 generateLhs :: PTerm
243 generateLhs :: PTerm
247 generateLhs = let args = lhsArgs index phArgs
244 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)]
249 where
246 where
250 lhsArgs :: Int -> [PArg] -> [PArg]
247 lhsArgs :: Int -> [PArg] -> [PArg]
251 lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
248 lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest