cc4eb28 · Idris-dev · git.iko.soy

lib/vect.idr+5−1

compare with master

unifiedsplit

@@ -13,4 +13,8 @@ data Vect : Set -> Nat -> Set where

13vlookup : (i : Fin n) -> Vect a n -> a;

14vlookup fO (x :: xs) = x;

15vlookup (fS k) (x :: xs) = vlookup k xs;

16−

16+

17+vapp : Vect a n -> Vect a m -> Vect a (plus n m);

18+vapp VNil ys = ys;

19+vapp (x :: xs) ys = x :: vapp xs ys;

20+

src/Core/Elaborate.hs+4−1

@@ -163,6 +163,9 @@ intro n = processTactic' (Intro n)

163forall :: Name -> Raw -> Elab ()

164forall n t = processTactic' (Forall n t)

165

166+letbind :: Name -> Raw -> Raw -> Elab ()

167+letbind n t v = processTactic' (LetBind n t v)

168+

166patvar :: Name -> Elab ()

169patvar :: Name -> Elab ()

167patvar n = processTactic' (PatVar n)

170patvar n = processTactic' (PatVar n)

168

171

@@ -272,8 +275,8 @@ simple_app fun arg =

272 start_unify s

275 start_unify s

273 claim s (Var a)

276 claim s (Var a)

274 prep_fill f [s]

277 prep_fill f [s]

278+ focus s; arg -- need to work out the type of the arg, so do it first

275 focus f; fun

279 focus f; fun

276− focus s; arg

277 complete_fill

280 complete_fill

278 end_unify

281 end_unify

279

282

src/Core/ProofState.hs+10

@@ -49,6 +49,7 @@ data Tactic = Attack

49 | CheckIn Raw

50 | Intro Name

51 | Forall Name Raw

52+ | LetBind Name Raw Raw

52 | PatVar Name

53 | PatVar Name

53 | PatBind Name

54 | PatBind Name

54 | Focus Name

55 | Focus Name

@@ -270,6 +271,14 @@ patvar n ctxt env (Bind x (Hole t) sc) =

270 do action (\ps -> ps { holes = holes ps \\ [x] })

271 do action (\ps -> ps { holes = holes ps \\ [x] })

271 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

272 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

272

273

274+letbind :: Name -> Raw -> Raw -> RunTactic

275+letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

276+ do (tyv, tyt) <- lift $ check ctxt env ty

277+ (valv, valt) <- lift $ check ctxt env val

278+ lift $ isSet ctxt env tyt

279+ return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

280+letbind n ty val ctxt env _ = fail "Can't let bind here"

281+

273patbind :: Name -> RunTactic

282patbind :: Name -> RunTactic

274patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

283patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

275 do let t' = normalise ctxt env t

284 do let t' = normalise ctxt env t

@@ -379,6 +388,7 @@ process t h = tactic (Just h) (mktac t)

379 mktac Compute = compute

388 mktac Compute = compute

380 mktac (Intro n) = intro n

389 mktac (Intro n) = intro n

381 mktac (Forall n t) = forall n t

390 mktac (Forall n t) = forall n t

391+ mktac (LetBind n t v) = letbind n t v

382 mktac (PatVar n) = patvar n

392 mktac (PatVar n) = patvar n

383 mktac (PatBind n) = patbind n

393 mktac (PatBind n) = patbind n

384 mktac (CheckIn r) = check_in r

394 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntax.hs+7

@@ -263,6 +263,8 @@ showImp impl tm = se 10 tm where

263 se p (PQuote r) = "![" ++ show r ++ "]"

264 se p (PRef _ n) = show n

265 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

266+ se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

267+ " in " ++ se 10 sc

266 se p (PPi Exp n ty sc)

268 se p (PPi Exp n ty sc)

267 | n `elem` allNamesIn sc = bracket p 2 $

269 | n `elem` allNamesIn sc = bracket p 2 $

268 "(" ++ show n ++ " : " ++ se 10 ty ++

270 "(" ++ show n ++ " : " ++ se 10 ty ++

@@ -433,6 +435,11 @@ addImpl ist ptm = ai [] ptm

433 ai env (PLam n ty sc) = let ty' = ai env ty

435 ai env (PLam n ty sc) = let ty' = ai env ty

434 sc' = ai (n:env) sc in

436 sc' = ai (n:env) sc in

435 PLam n ty' sc'

437 PLam n ty' sc'

438+ ai env (PLet n ty val sc)

439+ = let ty' = ai env ty

440+ val' = ai env val

441+ sc' = ai (n:env) sc in

442+ PLet n ty' val' sc'

436 ai env (PPi p n ty sc) = let ty' = ai env ty

443 ai env (PPi p n ty sc) = let ty' = ai env ty

437 sc' = ai (n:env) sc in

444 sc' = ai (n:env) sc in

438 PPi p n ty' sc'

445 PPi p n ty' sc'

src/Idris/Delaborate.hs+2−1

@@ -16,7 +16,8 @@ delab ist tm = de [] tm

16 un = FC "(val)" 0

17

18 de env (App f a) = deFn env f [a]

19− de env (V i) = PRef un (env!!i)

19+ de env (V i) | i < length env = PRef un (env!!i)

20+ | otherwise = PRef un (UN ["v" ++ show i ++ ""])

20 de env (P _ n _) | n == unitTy = PTrue un

21 de env (P _ n _) | n == unitTy = PTrue un

21 | n == unitCon = PTrue un

22 | n == unitCon = PTrue un

22 | n == falseTy = PFalse un

23 | n == falseTy = PFalse un

src/Idris/ElabDecls.hs+19−7

@@ -90,7 +90,7 @@ elabVal info tm

90 = do ctxt <- getContext

91 logLvl 10 (showImp True tm)

92 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

93− (build info False (infTerm tm))

93+ (build info True (infTerm tm))

94 logLvl 3 ("Value: " ++ show tm')

95 let vtm = getInferTerm tm'

96 logLvl 2 (show vtm)

@@ -241,18 +241,30 @@ elab info pattern tm = do elab' tm

241 elab' ty

242 elab' sc

243 solve

244+ elab' (PLet n Placeholder val sc)

245+ = do attack; -- (h:_) <- get_holes

246+ tyn <- unique_hole (MN 0 "letty")

247+ -- start_unify h

248+ claim tyn (RSet 0)

249+ valn <- unique_hole (MN 0 "letval")

250+ claim valn (Var tyn)

251+ letbind n (Var tyn) (Var valn)

252+ focus valn

253+ elab' val

254+ elab' sc

255+ -- end_unify

256+ solve

244 elab' (PApp fc (PRef _ f) args)

257 elab' (PApp fc (PRef _ f) args)

245 | Just ps <- lookupCtxt f (inblock info)

258 | Just ps <- lookupCtxt f (inblock info)

246 = erun fc $

259 = erun fc $

247 elabApp (liftname info f) (map (PExp . (PRef fc)) ps ++ args)

260 elabApp (liftname info f) (map (PExp . (PRef fc)) ps ++ args)

248 | otherwise = erun fc $ elabApp f args

261 | otherwise = erun fc $ elabApp f args

249 where elabApp f args

262 where elabApp f args

250− = -- erun (FC "FOO" 42) $

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

263+ = try (do ns <- apply (Var f) (map isph args)

252− solve

264+ solve

253− elabArgs ns (map getTm args))

265+ elabArgs ns (map getTm args))

254− (do apply_elab f (map toElab args)

266+ (do apply_elab f (map toElab args)

255− solve)

267+ solve)

256 elab' (PApp fc f [arg])

268 elab' (PApp fc f [arg])

257 = erun fc $

269 = erun fc $

258 do simple_app (elab' f) (elab' (getTm arg))

270 do simple_app (elab' f) (elab' (getTm arg))

src/Idris/Parser.hs+5

@@ -258,6 +258,7 @@ pNoExtExpr syn =

258 try (pApp syn)

259 <|> pSimpleExpr syn

260 <|> try (pLambda syn)

261+ <|> try (pLet syn)

261 <|> try (pPi syn)

262 <|> try (pPi syn)

262 <|> try (pDoBlock syn)

263 <|> try (pDoBlock syn)

263

264

@@ -354,6 +355,10 @@ pLambda syn = do lchar '\\';

354 sc <- pExpr syn

355 sc <- pExpr syn

355 return (bindList PLam xt sc)

356 return (bindList PLam xt sc)

356

357

358+pLet syn = do reserved "let"; n <- pName; lchar '='; v <- pExpr syn

359+ reserved "in"; sc <- pExpr syn

360+ return (PLet n Placeholder v sc)

361+

357pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'

362pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'

358 symbol "->"

363 symbol "->"

359 sc <- pExpr syn

364 sc <- pExpr syn

src/Main.hs+3−2

@@ -41,13 +41,14 @@ main = do xs <- getArgs

41runIdris :: [Opt] -> Idris ()

42runIdris opts =

43 do let inputs = opt getFile opts

44+ let runrepl = not (NoREPL `elem` opts)

44 mapM_ makeOption opts

45 mapM_ makeOption opts

45 elabPrims

46 elabPrims

46 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

47 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

47 return ()

48 return ()

49+ when runrepl $ iputStrLn banner

48 mods <- mapM loadModule inputs

50 mods <- mapM loadModule inputs

49− when (not (NoREPL `elem` opts)) $ do iputStrLn banner

50− repl (mkPrompt mods)

51+ when runrepl $ repl (mkPrompt mods)

51 where

52 where

52 makeOption (OLogging i) = setLogLevel i

53 makeOption (OLogging i) = setLogLevel i

53 makeOption _ = return ()

54 makeOption _ = return ()