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

git.iko.soy/Idris-dev

Elaborator tweak, dealing better with values that are inferred automatically

commit3af0ae0ffcdf59270acdbc02bea067b688403fb3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 9 Jan 2012, 01:19 (15 years ago) parent22b2879

7 files changed+63−21

compare with master

unifiedsplit

lib/builtins.idr+1−1 lib/prelude/either.idr+3 lib/prelude/nat.idr+4−3 src/Core/Elaborate.hs+26−6 src/Idris/Delaborate.hs+6−2 src/Idris/ElabDecls.hs+3 src/Idris/ElabTerm.hs+20−9

lib/builtins.idr+1−1

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

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

1616replace refl prf = prf

1717

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

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

1919sym refl = refl

2020

2121lazy : a -> a

lib/prelude/either.idr+3

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

88choose True = Left oh

99choose False = Right oh

1010

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)

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

6464

6565plus_commutes_Sk = proof {

66− intro k,m,ih;

66+ intros;

6767 refine sym;

68− rewrite (sym ih);

69− refine plusn_Sm;

68+ rewrite sym ih;

69+ rewrite plusn_Sm m k;

70+ trivial;

7071}

7172

7273plus_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

253253undo :: Elab' aux ()

254254undo = processTactic' Undo

255255

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

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

257257prepare_apply fn imps =

258258 do ty <- get_type fn

259259 ctxt <- get_context

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

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

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

264264 -- 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)

266266 let (h : hs) = holes p

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

268268-- case claims of

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

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

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

277277 claim n (forget t)

278− when (fst i) (movelast n)

278+ when i (movelast n)

279279 mkClaims sc' is (n : claims)

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

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

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

289289

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

291291apply fn imps =

292− do args <- prepare_apply fn imps

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

293293 fill (raw_apply fn (map Var args))

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

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

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

297297 -- so do nothing

298298 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)))

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

301301 let (n, hs) = unified p

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

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

304304 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

306326

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

308328apply_elab n args =

src/Idris/Delaborate.hs+6−2

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

1111import Debug.Trace

1212

1313delab :: IState -> Term -> PTerm

14−delab ist tm = de [] tm

14+delab i tm = delab' i tm False

15+

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

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

1518 where

1619 un = FC "(val)" 0

1720

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

3033 de env (Constant i) = PConstant i

3134 de env (Set i) = PSet

3235

36+ dens x | fullname = x

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

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

3539 _ -> ns

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

5660pshow i (Msg s) = s

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

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

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

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

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

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

6266 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)

196196 ctxt <- getContext

197197 logLvl 5 $ "Rechecking"

198198 (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

199202 return $ Just (clhs, crhs)

200203 where

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

src/Idris/ElabTerm.hs+20−9

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

7373 Placeholder -> Nothing

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

7575

76+ toElab' ina arg = case getTm arg of

77+ Placeholder -> Nothing

78+ v -> Just (elabE ina v)

79+

7680 mkPat = do hs <- get_holes

7781 case hs of

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

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

190194 solve

191195 let (ns', eargs)

192196 = unzip $

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

194− (zip ns args)

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

198+ (zip ns args)

195199 elabArgs (ina || not isinf)

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

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

198− solve)

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

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

203+ solve)

199204 ivs' <- get_instances

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

201206 mapM_ (\n -> do focus n

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

269274 [pimp (UN "a") Placeholder,

270275 pexp t]);

271276 | otherwise = elabArg n t

272− where elabArg n t = if r

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

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

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

276−

277+ where elabArg n t

278+ = do hs <- get_holes

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

280+ True ->

281+ if r

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

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

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

285+ False -> return failed

286+ elabArgs ina failed r ns args

287+

277288pruneAlt :: [PTerm] -> [PTerm]

278289pruneAlt xs = map prune xs

279290 where