66bcd8c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix library compilation errors and improve name resolution in patterns

66bcd8cEdwin Brady15 years ago

lib/checkall.idr+1

compare with master

unifiedsplit

@@ -8,6 +8,7 @@ import prelude

8import io

9import system

11+import prelude.algebra

11import prelude.cast

12import prelude.cast

12import prelude.nat

13import prelude.nat

13import prelude.fin

14import prelude.fin

lib/prelude/vect.idr+2−2

@@ -44,13 +44,13 @@ reverse xs = revAcc [] xs where

45revAcc_lemma_2 = proof {

46 intros;

47− rewrite sym (plusn_Sm n k);

47+ rewrite plusSuccRightSucc n k;

48 exact value;

49}

51revAcc_lemma_1 = proof {

52 intros;

53− rewrite sym (plusnO n);

53+ rewrite sym (plusZeroRightNeutral n);

54 exact value;

55}

src/Idris/ElabTerm.hs+39−30

@@ -62,7 +62,7 @@ buildTC ist info pattern tcgen fn tm

62elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

63 ElabD ()

64elab ist info pattern tcgen fn tm

65− = do elabE False tm

65+ = do elabE (False, False) tm -- (in argument, guarded)

66 when pattern -- convert remaining holes to pattern vars

67 mkPat

68 inj <- get_inj

@@ -108,9 +108,10 @@ elab ist info pattern tcgen fn tm

108 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

109 pimp (MN 0 "b") Placeholder,

110 pexp l, pexp r])

111+ elab' ina@(_, a) (PPair fc l r)

111− elab' ina (PPair fc l r) = try (elabE True (PApp fc (PRef fc pairTy)

112+ = try (elabE (True, a) (PApp fc (PRef fc pairTy)

112 [pexp l,pexp r]))

113 [pexp l,pexp r]))

113− (elabE True (PApp fc (PRef fc pairCon)

114+ (elabE (True, a) (PApp fc (PRef fc pairCon)

114 [pimp (MN 0 "A") Placeholder,

115 [pimp (MN 0 "A") Placeholder,

115 pimp (MN 0 "B") Placeholder,

116 pimp (MN 0 "B") Placeholder,

116 pexp l, pexp r]))

117 pexp l, pexp r]))

@@ -135,31 +136,37 @@ elab ist info pattern tcgen fn tm

135 (tryAll (zip (map (elab' ina) as) (map showHd as)))

136 (tryAll (zip (map (elab' ina) as) (map showHd as)))

136 where showHd (PApp _ h _) = show h

137 where showHd (PApp _ h _) = show h

137 showHd x = show x

138 showHd x = show x

138− elab' ina (PRef fc n) | pattern && not (inparamBlock n)

139+ elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

139 = do ctxt <- get_context

140 = do ctxt <- get_context

140 let iscon = isConName Nothing n ctxt

141 let iscon = isConName Nothing n ctxt

142+ let defined = case lookupTy Nothing n ctxt of

143+ [] -> False

144+ _ -> True

145+ -- this is to stop us resolve type classes recursively

141− if (not iscon && ina) then erun fc $ patvar n

146+ if (tcname n && ina) then erun fc $ patvar n

147+ else if (defined && not guarded)

148+ then do apply (Var n) []; solve

142− else try (do apply (Var n) []; solve)

149+ else try (do apply (Var n) []; solve)

143− (patvar n)

150+ (patvar n)

144 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

151 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

145 [] -> False

152 [] -> False

146 _ -> True

153 _ -> True

147 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

154 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

148− elab' ina (PLam n Placeholder sc)

155+ elab' ina@(_, a) (PLam n Placeholder sc)

149− = do attack; intro (Just n); elabE True sc; solve

156+ = do attack; intro (Just n); elabE (True, a) sc; solve

150− elab' ina (PLam n ty sc)

157+ elab' ina@(_, a) (PLam n ty sc)

151 = do tyn <- unique_hole (MN 0 "lamty")

158 = do tyn <- unique_hole (MN 0 "lamty")

152 claim tyn RSet

159 claim tyn RSet

153 attack

160 attack

154 introTy (Var tyn) (Just n)

161 introTy (Var tyn) (Just n)

155 -- end_unify

162 -- end_unify

156 focus tyn

163 focus tyn

157− elabE True ty

164+ elabE (True, a) ty

158− elabE True sc

165+ elabE (True, a) sc

159 solve

166 solve

160− elab' ina (PPi _ n Placeholder sc)

167+ elab' ina@(_,a) (PPi _ n Placeholder sc)

161− = do attack; arg n (MN 0 "ty"); elabE True sc; solve

168+ = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve

162− elab' ina (PPi _ n ty sc)

169+ elab' ina@(_,a) (PPi _ n ty sc)

163 = do attack; tyn <- unique_hole (MN 0 "ty")

170 = do attack; tyn <- unique_hole (MN 0 "ty")

164 claim tyn RSet

171 claim tyn RSet

165 n' <- case n of

172 n' <- case n of

@@ -167,10 +174,10 @@ elab ist info pattern tcgen fn tm

167 _ -> return n

174 _ -> return n

168 forall n' (Var tyn)

175 forall n' (Var tyn)

169 focus tyn

176 focus tyn

170− elabE True ty

177+ elabE (True, a) ty

171− elabE True sc

178+ elabE (True, a) sc

172 solve

179 solve

173− elab' ina (PLet n ty val sc)

180+ elab' ina@(_,a) (PLet n ty val sc)

174 = do attack;

181 = do attack;

175 tyn <- unique_hole (MN 0 "letty")

182 tyn <- unique_hole (MN 0 "letty")

176 claim tyn RSet

183 claim tyn RSet

@@ -180,10 +187,10 @@ elab ist info pattern tcgen fn tm

180 case ty of

187 case ty of

181 Placeholder -> return ()

188 Placeholder -> return ()

182 _ -> do focus tyn

189 _ -> do focus tyn

183− elabE True ty

190+ elabE (True, a) ty

184 focus valn

191 focus valn

185− elabE True val

192+ elabE (True, a) val

186− elabE True sc

193+ elabE (True, a) sc

187 solve

194 solve

188-- elab' ina (PTyped val ty)

195-- elab' ina (PTyped val ty)

189-- = do tyn <- unique_hole (MN 0 "castty")

196-- = do tyn <- unique_hole (MN 0 "castty")

@@ -198,27 +205,29 @@ elab ist info pattern tcgen fn tm

198-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)

205-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)

199-- = let dsl' = expandDo d (getTm arg) in

206-- = let dsl' = expandDo d (getTm arg) in

200-- trace (show dsl') $ elab' ina dsl'

207-- trace (show dsl') $ elab' ina dsl'

201− elab' ina (PApp fc (PRef _ f) args')

208+ elab' (ina, g) (PApp fc (PRef _ f) args')

202 = do let args = {- case lookupCtxt f (inblock info) of

209 = do let args = {- case lookupCtxt f (inblock info) of

203 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

210 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

204 _ ->-} args'

211 _ ->-} args'

205 ivs <- get_instances

212 ivs <- get_instances

206 -- HACK: we shouldn't resolve type classes if we're defining an instance

213 -- HACK: we shouldn't resolve type classes if we're defining an instance

207− -- function or default defition.

214+ -- function or default definition.

208 let isinf = f == inferCon || tcname f

215 let isinf = f == inferCon || tcname f

216+ ctxt <- get_context

217+ let guarded = isConName Nothing f ctxt

209 try (do ns <- apply (Var f) (map isph args)

218 try (do ns <- apply (Var f) (map isph args)

210 solve

219 solve

211 let (ns', eargs)

220 let (ns', eargs)

212 = unzip $

221 = unzip $

213 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

222 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

214 (zip ns args)

223 (zip ns args)

215− try (elabArgs (ina || not isinf)

224+ try (elabArgs (ina || not isinf, guarded)

216 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

225 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

217− (elabArgs (ina || not isinf)

226+ (elabArgs (ina || not isinf, guarded)

218 [] False (reverse ns')

227 [] False (reverse ns')

219 (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))

228 (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))

220-- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args))

229-- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args))

221− (do apply_elab f (map (toElab (ina || not isinf)) args)

230+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

222 solve)

231 solve)

223 ivs' <- get_instances

232 ivs' <- get_instances

224 when (not pattern || (ina && not tcgen)) $

233 when (not pattern || (ina && not tcgen)) $

@@ -233,9 +242,9 @@ elab ist info pattern tcgen fn tm

233 where tcArg (n, PConstraint _ _ Placeholder) = True

242 where tcArg (n, PConstraint _ _ Placeholder) = True

234 tcArg _ = False

243 tcArg _ = False

235

244

236− elab' a (PApp fc f [arg])

245+ elab' ina@(_, a) (PApp fc f [arg])

237 = erun fc $

246 = erun fc $

238− do simple_app (elabE a f) (elabE True (getTm arg))

247+ do simple_app (elabE ina f) (elabE (True, a) (getTm arg))

239 solve

248 solve

240 elab' ina Placeholder = do (h : hs) <- get_holes

249 elab' ina Placeholder = do (h : hs) <- get_holes

241 movelast h

250 movelast h

@@ -250,7 +259,7 @@ elab ist info pattern tcgen fn tm

250 | not pattern = do mapM_ (runTac False ist) ts

259 | not pattern = do mapM_ (runTac False ist) ts

251 | otherwise = elab' ina Placeholder

260 | otherwise = elab' ina Placeholder

252 elab' ina (PElabError e) = fail e

261 elab' ina (PElabError e) = fail e

253− elab' ina c@(PCase fc scr opts)

262+ elab' ina@(_, a) c@(PCase fc scr opts)

254 = do attack

263 = do attack

255 tyn <- unique_hole (MN 0 "scty")

264 tyn <- unique_hole (MN 0 "scty")

256 claim tyn RSet

265 claim tyn RSet

@@ -259,7 +268,7 @@ elab ist info pattern tcgen fn tm

259 claim valn (Var tyn)

268 claim valn (Var tyn)

260 letbind scvn (Var tyn) (Var valn)

269 letbind scvn (Var tyn) (Var valn)

261 focus valn

270 focus valn

262− elabE True scr

271+ elabE (True, a) scr

263 args <- get_env

272 args <- get_env

264 cname <- unique_hole (mkCaseName fn)

273 cname <- unique_hole (mkCaseName fn)

265 elab' ina (PMetavar cname)

274 elab' ina (PMetavar cname)

test/test006/test006.idr+2−2

@@ -25,14 +25,14 @@ main = do print (natToBin 42)

25main.parity_lemma_2 = proof {

26 intro;

27 intro;

28− rewrite plusn_Sm j j;

28+ rewrite sym (plusSuccRightSucc j j);

29 trivial;

30};

32main.parity_lemma_1 = proof {

33 intro j;

34 intro;

35− rewrite plusn_Sm j j;

35+ rewrite sym (plusSuccRightSucc j j);

36 trivial;

37};