86bcbbc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allowed unnamed fields.

86bcbbcSune Alkærsig12 years ago

libs/base/Data/Buffer.idr+3−3

compare with master

unifiedsplit

@@ -50,13 +50,13 @@ bitsFromFin (FS k) = 1 + bitsFromFin k

50||| approximate ultimate size of the Buffer is known. Users can assume

51||| the new Buffer is word-aligned.

52public

53−allocate : ( hint : Nat) -> Buffer Z

53+allocate : ( hint : Nat ) -> Buffer Z

54−allocate = MkBuffer Z . prim__allocate . bitsFromNat

54+allocate = MkBuffer Z . prim__allocate . bitsFromNat

56||| Append count repetitions of a Buffer to another Buffer

57%assert_total

58public

59−appendBuffer : {n : Nat} -> {m : Nat} -> Buffer n ->

59+appendBuffer : Buffer n ->

60 ( count : Nat ) ->

61 Buffer m ->

62 Buffer ( n + count * m )

libs/prelude/Prelude/Nat.idr+6−4

@@ -200,15 +200,17 @@ instance Cast Integer Nat where

200 cast = fromInteger

201

202||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

203+--record Multiplicative : Type where

204+-- getMultiplicative : Nat -> Multiplicative

203record Multiplicative where

205record Multiplicative where

204 constructor getMultiplicative

206 constructor getMultiplicative

205− multiplicative_n : Nat

207+ _ : Nat

206

208

207||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

209||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

208record Additive where

210record Additive where

209− constructor getAdditive

211+ constructor getAdditive

210− additive_n : Nat

212+ _ : Nat

211−

213+

212instance Semigroup Multiplicative where

214instance Semigroup Multiplicative where

213 (<+>) left right = getMultiplicative $ left' * right'

215 (<+>) left right = getMultiplicative $ left' * right'

214 where

216 where

src/Idris/AbsSyntax.hs+3−4

@@ -1076,10 +1076,9 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

1076 econ (doc, argDocs, n, t, fc, fs)

1077 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1078expandParamsD rhs ist dec ps ns (PRecord doc syn fc opts n prs pdocs fls fdocs cn cdoc csyn)

1079− = PRecord doc syn fc opts (dec n) (map (mapTrd $ expandParams dec ps ns []) prs) pdocs

1079+ = PRecord doc syn fc opts n prs pdocs

1080− (map (mapTrd $ expandParams dec ps ns []) fls) fdocs

1080+ fls fdocs

1081− (liftM dec cn) cdoc csyn

1081+ cn cdoc csyn

1082− where mapTrd f (x, y, z) = (x, y, f z)

1083

1082

1084expandParamsD rhs ist dec ps ns (PParams f params pds)

1083expandParamsD rhs ist dec ps ns (PParams f params pds)

1085 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

1084 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

src/Idris/Elab/Record.hs+20−21

@@ -50,7 +50,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

50 ttConsTy <-

51 case lookupTyExact dconName (tt_ctxt i) of

52 Just as -> return as

53− Nothing -> tclift $ tfail $ At fc (Elaborating "record" tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

53+ Nothing -> tclift $ tfail $ At fc (Elaborating "record " tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))

55 -- The arguments to the constructor

56 let constructorArgs = getArgTys ttConsTy

@@ -69,6 +69,10 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

69 -- Build and elaborate projection functions

70 elabProj dconName projectors

72+ logLvl 1 $ "Dependencies: " ++ show fieldDependencies

73+

74+ logLvl 1 $ "Depended on: " ++ show dependedOn

75+

72 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.

76 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.

73 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]

77 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]

74 -- Build and elaborate update functions

78 -- Build and elaborate update functions

@@ -170,14 +174,6 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

170 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i

174 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i

171 in mapM_ elab fs

175 in mapM_ elab fs

172

176

173− projectInType :: [(Name, Name)] -> PTerm -> PTerm

174− projectInType xs = mapPT st

175− where

176− st :: PTerm -> PTerm

177− st (PRef fc n)

178− | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]

179− st t = t

180−

181 -- | Elaborate the update functions.

177 -- | Elaborate the update functions.

182 elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

178 elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

183 elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

179 elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]

@@ -186,14 +182,14 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo

186

182

187 -- | Decides whether a setter should be generated for a field or not.

183 -- | Decides whether a setter should be generated for a field or not.

188 optionalSetter :: Name -> Bool

184 optionalSetter :: Name -> Bool

189− optionalSetter n = n `notElem` dependentFields && n `notElem` dependedOn

185+ optionalSetter n = n `elem` dependedOn

190

186

191 -- | A map from a field name to the other fields it depends on.

187 -- | A map from a field name to the other fields it depends on.

192 fieldDependencies :: [(Name, [Name])]

188 fieldDependencies :: [(Name, [Name])]

193 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]

189 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]

194 where

190 where

195 fieldDep :: Name -> PTerm -> (Name, [Name])

191 fieldDep :: Name -> PTerm -> (Name, [Name])

196− fieldDep n t = ((nsroot n), fieldNames `intersect` allNamesIn t)

192+ fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

197

193

198 -- | A list of fields depending on another field.

194 -- | A list of fields depending on another field.

199 dependentFields :: [Name]

195 dependentFields :: [Name]

@@ -223,7 +219,7 @@ elabProjection :: ElabInfo ->

223 [Name] -> -- ^ All Field Names

219 [Name] -> -- ^ All Field Names

224 Int -> -- ^ Argument Index

220 Int -> -- ^ Argument Index

225 Idris ()

221 Idris ()

226−elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames index

222+elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

227 = do logLvl 1 $ "Generating Projection for " ++ show pname

223 = do logLvl 1 $ "Generating Projection for " ++ show pname

228

224

229 let ty = generateTy

225 let ty = generateTy

@@ -241,13 +237,7 @@ elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames in

241 where

237 where

242 -- | The type of the projection function.

238 -- | The type of the projection function.

243 generateTy :: PDecl

239 generateTy :: PDecl

244− generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName tty (mapPT applyProjs pty)

240+ generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName targetTy projTy

245−

246− -- | Applies all fields to "rec".

247− applyProjs :: PTerm -> PTerm

248− applyProjs t@(PRef fc name)

249− | (nsroot name) `elem` fnames = PApp fc t [pexp recRef]

250− applyProjs t = t

251

241

252 -- | The left hand side of the projection function.

242 -- | The left hand side of the projection function.

253 generateLhs :: PTerm

243 generateLhs :: PTerm

@@ -303,9 +293,10 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

303

293

304 idrisCatch (do rec_elabDecl info EAll info ty

294 idrisCatch (do rec_elabDecl info EAll info ty

305 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])

295 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])

296+ (\err -> logLvl 1 $ "Could not generate update function for " ++ show pname)

306− (\err -> if optional

297+ {-if optional

307 then logLvl 1 $ "Could not generate update function for " ++ show pname

298 then logLvl 1 $ "Could not generate update function for " ++ show pname

308− else tclift $ tfail $ At fc (Elaborating "record update function" pname err))

299+ else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}

309 where

300 where

310 -- | The type of the udpate function.

301 -- | The type of the udpate function.

311 generateTy :: PDecl

302 generateTy :: PDecl

@@ -364,3 +355,11 @@ recName :: Name

364recName = sMN 0 "rec"

355recName = sMN 0 "rec"

365

356

366recRef = PRef emptyFC recName

357recRef = PRef emptyFC recName

358+

359+projectInType :: [(Name, Name)] -> PTerm -> PTerm

360+projectInType xs = mapPT st

361+ where

362+ st :: PTerm -> PTerm

363+ st (PRef fc n)

364+ | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]

365+ st t = t

src/Idris/ParseData.hs+1−1

@@ -98,7 +98,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

98 field :: SyntaxInfo -> IdrisParser (Name, PTerm, Plicity, Docstring ())

99 field syn = do (doc, _) <- option noDocs docComment

100 c <- optional $ lchar '{'

101− n <- fnName

101+ n <- fnName <|> do symbol "_"; return $ sUN "__pi_arg"

102 lchar ':'

103 t <- typeExpr (allowImp syn)

104 p <- endPlicity c