3af0ae0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Elaborator tweak, dealing better with values that are inferred automatically

3af0ae0Edwin Brady15 years ago

lib/builtins.idr+1−1

compare with master

unifiedsplit

@@ -15,7 +15,7 @@ FalseElim : _|_ -> a

15replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y

16replace refl prf = prf

18−sym : {x:a} -> {y:a} -> x = y -> y = x

18+sym : {l:a} -> {r:a} -> l = r -> r = l

19sym refl = refl

21lazy : a -> a

lib/prelude/either.idr+3

@@ -8,3 +8,6 @@ choose : (b : Bool) -> Either (so b) (so (not b))

8choose True = Left oh

9choose False = Right oh

11+either : Either a b -> (a -> c) -> (b -> c) -> c

12+either (Left x) l r = l x

13+either (Right x) l r = r x

lib/prelude/nat.idr+4−3

@@ -63,10 +63,11 @@ plus_commutes O m = sym (plusnO m)

63plus_commutes (S k) m = let ih = plus_commutes k m in ?plus_commutes_Sk

65plus_commutes_Sk = proof {

66− intro k,m,ih;

66+ intros;

67 refine sym;

68− rewrite (sym ih);

68+ rewrite sym ih;

69− refine plusn_Sm;

69+ rewrite plusn_Sm m k;

70+ trivial;

70}

71}

72plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p

73plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p

src/Core/Elaborate.hs+26−6

@@ -253,7 +253,7 @@ qed = do processTactic' QED

253undo :: Elab' aux ()

254undo = processTactic' Undo

255

256−prepare_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

256+prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]

257prepare_apply fn imps =

258 do ty <- get_type fn

259 ctxt <- get_context

@@ -262,7 +262,7 @@ prepare_apply fn imps =

262 claims <- mkClaims (normalise ctxt env ty) imps []

263 ES (p, a) s prev <- get

264 -- reverse the claims we made so that args go left to right

265− let n = length (filter not (map fst imps))

265+ let n = length (filter not imps)

266 let (h : hs) = holes p

267 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)

268-- case claims of

@@ -275,7 +275,7 @@ prepare_apply fn imps =

275-- when (null claims) (start_unify n)

276 let sc' = instantiate (P Bound n t) sc

277 claim n (forget t)

278− when (fst i) (movelast n)

278+ when i (movelast n)

279 mkClaims sc' is (n : claims)

280 mkClaims t [] claims = return (reverse claims)

281 mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn

@@ -289,20 +289,40 @@ prepare_apply fn imps =

289

290apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

291apply fn imps =

292− do args <- prepare_apply fn imps

292+ do args <- prepare_apply fn (map fst imps)

293 fill (raw_apply fn (map Var args))

294 -- *Don't* solve the arguments we're specifying by hand.

295 -- (remove from unified list before calling end_unify)

296 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

297 -- so do nothing

298 ptm <- get_term

299− let dontunify = [] -- map fst (filter (not.snd) (zip args imps))

299+ let dontunify = [] -- map fst (filter (not.snd) (zip args (map fst imps)))

300 ES (p, a) s prev <- get

301 let (n, hs) = unified p

302 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)

303 put (ES (p { unified = unify }, a) s prev)

304 end_unify

305− return args

305+ return (map (updateUnify hs) args)

306+ where updateUnify hs n = case lookup n hs of

307+ Just (P _ t _) -> t

308+ _ -> n

309+

310+apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

311+apply2 fn elabs =

312+ do args <- prepare_apply fn (map isJust elabs)

313+ fill (raw_apply fn (map Var args))

314+ elabArgs args elabs

315+ ES (p, a) s prev <- get

316+ let (n, hs) = unified p

317+ end_unify

318+ solve

319+ where elabArgs [] [] = return ()

320+ elabArgs (n:ns) (Just e:es) = do focus n; e

321+ elabArgs ns es

322+ elabArgs (n:ns) (_:es) = elabArgs ns es

323+

324+ isJust (Just _) = False

325+ isJust _ = True

306

326

307apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()

327apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()

308apply_elab n args =

328apply_elab n args =

src/Idris/Delaborate.hs+6−2

@@ -11,7 +11,10 @@ import Core.TT

11import Debug.Trace

13delab :: IState -> Term -> PTerm

14+delab i tm = delab' i tm False

15+

16+delab' :: IState -> Term -> Bool -> PTerm

14−delab ist tm = de [] tm

17+delab' ist tm fullname = de [] tm

15 where

18 where

16 un = FC "(val)" 0

19 un = FC "(val)" 0

@@ -30,6 +33,7 @@ delab ist tm = de [] tm

30 de env (Constant i) = PConstant i

33 de env (Constant i) = PConstant i

31 de env (Set i) = PSet

34 de env (Set i) = PSet

36+ dens x | fullname = x

33 dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of

37 dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of

34 [_] -> n -- just one thing

38 [_] -> n -- just one thing

35 _ -> ns

39 _ -> ns

@@ -56,7 +60,7 @@ pshow :: IState -> Err -> String

56pshow i (Msg s) = s

60pshow i (Msg s) = s

57pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

61pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

58 ++ " with " ++ show (delab i y)

62 ++ " with " ++ show (delab i y)

59−-- ++ "\n\t(" ++ pshow i e ++ ")"

63+-- ++ "\n\t(" ++ pshow i e ++ ")"

60pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

64pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

61 " when unifying " ++ show (delab i x) ++ " and " ++

65 " when unifying " ++ show (delab i x) ++ " and " ++

62 show (delab i y)

66 show (delab i y)

src/Idris/ElabDecls.hs+3

@@ -196,6 +196,9 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

196 ctxt <- getContext

197 logLvl 5 $ "Rechecking"

198 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

199+ i <- get

200+ logLvl 6 $ "Checked to\n" ++ showImp True (delab' i crhs True) ++ "\n" ++

201+ showImp True rhs

199 return $ Just (clhs, crhs)

202 return $ Just (clhs, crhs)

200 where

203 where

201 decorate x = UN (show fname ++ "#" ++ show x)

204 decorate x = UN (show fname ++ "#" ++ show x)

src/Idris/ElabTerm.hs+20−9

@@ -73,6 +73,10 @@ elab ist info pattern tcgen fn tm

73 Placeholder -> Nothing

74 v -> Just (priority arg, elabE ina v)

76+ toElab' ina arg = case getTm arg of

77+ Placeholder -> Nothing

78+ v -> Just (elabE ina v)

79+

76 mkPat = do hs <- get_holes

80 mkPat = do hs <- get_holes

77 case hs of

81 case hs of

78 (h: hs) -> do patvar h; mkPat

82 (h: hs) -> do patvar h; mkPat

@@ -190,12 +194,13 @@ elab ist info pattern tcgen fn tm

190 solve

194 solve

191 let (ns', eargs)

195 let (ns', eargs)

192 = unzip $

196 = unzip $

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

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

194− (zip ns args)

198+ (zip ns args)

195 elabArgs (ina || not isinf)

199 elabArgs (ina || not isinf)

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

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

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

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

202+ (do apply_elab f (map (toElab (ina || not isinf)) args)

198− solve)

203+ solve)

199 ivs' <- get_instances

204 ivs' <- get_instances

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

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

201 mapM_ (\n -> do focus n

206 mapM_ (\n -> do focus n

@@ -269,11 +274,17 @@ elab ist info pattern tcgen fn tm

269 [pimp (UN "a") Placeholder,

274 [pimp (UN "a") Placeholder,

270 pexp t]);

275 pexp t]);

271 | otherwise = elabArg n t

276 | otherwise = elabArg n t

272− where elabArg n t = if r

277+ where elabArg n t

278+ = do hs <- get_holes

279+ failed' <- case n `elem` hs of

280+ True ->

281+ if r

273− then try (do focus n; elabE ina t; elabArgs ina failed r ns args)

282+ then try (do focus n; elabE ina t; return failed)

274− (elabArgs ina ((n,(lazy, t)):failed) r ns args)

283+ (return ((n,(lazy, t)):failed))

284+ else do focus n; elabE ina t; return failed

285+ False -> return failed

275− else do focus n; elabE ina t; elabArgs ina failed r ns args

286+ elabArgs ina failed r ns args

276−

287+

277pruneAlt :: [PTerm] -> [PTerm]

288pruneAlt :: [PTerm] -> [PTerm]

278pruneAlt xs = map prune xs

289pruneAlt xs = map prune xs

279 where

290 where