03d7d5e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow type labels on lambdas

03d7d5eEdwin Brady15 years ago

src/Core/Elaborate.hs+3

compare with master

unifiedsplit

@@ -185,6 +185,9 @@ check_in t = processTactic' (CheckIn t)

185intro :: Maybe Name -> Elab ()

186intro n = processTactic' (Intro n)

187

188+introTy :: Raw -> Maybe Name -> Elab ()

189+introTy ty n = processTactic' (IntroTy ty n)

190+

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

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

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

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

190

193

src/Core/ProofState.hs+41−20

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

49 | EvalIn Raw

50 | CheckIn Raw

51 | Intro (Maybe Name)

52+ | IntroTy Raw (Maybe Name)

52 | Forall Name Raw

53 | Forall Name Raw

53 | LetBind Name Raw Raw

54 | LetBind Name Raw Raw

54 | Rewrite Raw

55 | Rewrite Raw

@@ -264,6 +265,24 @@ solve ctxt env (Bind x (Guess ty val) sc)

264 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

265 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

265solve _ _ h = fail $ "Not a guess " ++ show h

266solve _ _ h = fail $ "Not a guess " ++ show h

266

267

268+introTy :: Raw -> Maybe Name -> RunTactic

269+introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

270+ do let n = case mn of

271+ Just name -> name

272+ Nothing -> x

273+ let t' = normalise ctxt env t

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

275+-- ns <- lift $ unify ctxt env tyv t'

276+ case t' of

277+ Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

278+ do ns <- lift $ unify ctxt env s tyv

279+ ps <- get

280+ let (uh, uns) = unified ps

281+ put (ps { unified = (uh, uns ++ ns) })

282+ return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

283+ _ -> fail "Nothing to introduce"

284+introTy ty n ctxt env _ = fail "Can't introduce here."

285+

267intro :: Maybe Name -> RunTactic

286intro :: Maybe Name -> RunTactic

268intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

287intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

269 do let n = case mn of

288 do let n = case mn of

@@ -406,25 +425,27 @@ process EndUnify _

406 let (h, _) = unified ps

425 let (h, _) = unified ps

407 tactic (Just h) solve_unified

426 tactic (Just h) solve_unified

408process t h = tactic (Just h) (mktac t)

427process t h = tactic (Just h) (mktac t)

409− where mktac Attack = attack

428+ where mktac Attack = attack

410− mktac (Claim n r) = claim n r

429+ mktac (Claim n r) = claim n r

411− mktac (Exact r) = exact r

430+ mktac (Exact r) = exact r

412− mktac (Fill r) = fill r

431+ mktac (Fill r) = fill r

413 mktac (PrepFill n ns) = prep_fill n ns

432 mktac (PrepFill n ns) = prep_fill n ns

414− mktac CompleteFill = complete_fill

433+ mktac CompleteFill = complete_fill

415− mktac Regret = regret

434+ mktac Regret = regret

416− mktac Solve = solve

435+ mktac Solve = solve

417− mktac (StartUnify n) = start_unify n

436+ mktac (StartUnify n) = start_unify n

418− mktac Compute = compute

437+ mktac Compute = compute

419− mktac (Intro n) = intro n

438+ mktac (Intro n) = intro n

439+ mktac (IntroTy ty n) = introTy ty n

420− mktac (Forall n t) = forall n t

440+ mktac (Forall n t) = forall n t

421 mktac (LetBind n t v) = letbind n t v

441 mktac (LetBind n t v) = letbind n t v

422− mktac (Rewrite t) = rewrite t

442+ mktac (Rewrite t) = rewrite t

423− mktac (PatVar n) = patvar n

443+ mktac (PatVar n) = patvar n

424− mktac (PatBind n) = patbind n

444+ mktac (PatBind n) = patbind n

425− mktac (CheckIn r) = check_in r

445+ mktac (CheckIn r) = check_in r

426− mktac (EvalIn r) = eval_in r

446+ mktac (EvalIn r) = eval_in r

427− mktac (Focus n) = focus n

447+ mktac (Focus n) = focus n

428− mktac (Defer n) = defer n

448+ mktac (Defer n) = defer n

429− mktac (Instance n) = instanceArg n

449+ mktac (Instance n) = instanceArg n

430− mktac (MoveLast n) = movelast n

450+ mktac (MoveLast n) = movelast n

451+

src/Idris/ElabDecls.hs+10

@@ -557,6 +557,16 @@ elab ist info pattern tm

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

558 elab' (PLam n Placeholder sc)

559 = do attack; intro (Just n); elabE sc; solve

560+ elab' (PLam n ty sc)

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

562+ claim tyn (RSet 0)

563+ attack

564+ introTy (Var tyn) (Just n)

565+ -- end_unify

566+ focus tyn

567+ elabE ty

568+ elabE sc

569+ solve

560 elab' (PPi _ n Placeholder sc)

570 elab' (PPi _ n Placeholder sc)

561 = do attack; arg n (MN 0 "ty"); elabE sc; solve

571 = do attack; arg n (MN 0 "ty"); elabE sc; solve

562 elab' (PPi _ n ty sc)

572 elab' (PPi _ n ty sc)

src/Idris/Parser.hs+3−1

@@ -529,7 +529,9 @@ tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

529 t <- pTSig syn

530 return (map (\x -> (x, t)) ns)

531

532−tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)

532+tyOptDeclList syn = sepBy1 (do x <- pfName;

533+ t <- option Placeholder (do lchar ':'

534+ pExpr syn)

533 return (x,t))

535 return (x,t))

534 (lchar ',')

536 (lchar ',')

535

537