8f76315 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed approach to unification

8f76315Edwin Brady14 years ago

lib/Prelude/Heap.idr+1−1

compare with master

unifiedsplit

@@ -106,7 +106,7 @@ toList (Node s l e r) = toList' (Node s l e r) refl

106 where

107 %assert_total -- relies on deleteMinimum making heap smaller

108 toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a

109− toList' heap p = findMinimum heap p :: (toList $ deleteMinimum heap p)

109+ toList' heap p = findMinimum heap p :: (toList (deleteMinimum heap p))

110

111fromList : Ord a => List a -> MaxiphobicHeap a

112fromList = foldr insert empty

lib/Prelude/Vect.idr+2−2

@@ -129,10 +129,10 @@ total or : Vect Bool m -> Bool

129or = foldr (||) False

130

131total any : (a -> Bool) -> Vect a m -> Bool

132−any p = or . map p

132+any p = Vect.or . map p

133

134total all : (a -> Bool) -> Vect a m -> Bool

135−all p = and . map p

135+all p = Vect.and . map p

136

137--------------------------------------------------------------------------------

138-- Transformations

src/Core/Elaborate.hs+45−21

@@ -15,6 +15,7 @@ import Core.ProofState

15import Core.TT

16import Core.Evaluate

17import Core.Typecheck

18+import Core.Unify

19import Control.Monad.State

20import Control.Monad.State

20import Data.Char

21import Data.Char

@@ -118,6 +119,10 @@ get_holes :: Elab' aux [Name]

118get_holes = do ES p _ _ <- get

119get_holes = do ES p _ _ <- get

119 return (holes (fst p))

120 return (holes (fst p))

120

121

122+get_probs :: Elab' aux Fails

123+get_probs = do ES p _ _ <- get

124+ return (problems (fst p))

125+

121-- get the current goal type

126-- get the current goal type

122goal :: Elab' aux Type

127goal :: Elab' aux Type

123goal = do ES p _ _ <- get

128goal = do ES p _ _ <- get

@@ -150,10 +155,6 @@ get_deferred :: Elab' aux [Name]

150get_deferred = do ES p _ _ <- get

155get_deferred = do ES p _ _ <- get

151 return (deferred (fst p))

156 return (deferred (fst p))

152

157

153−get_inj :: Elab' aux [(Term, Term, Term)]

154−get_inj = do ES p _ _ <- get

155− return (injective (fst p))

156−

157checkInjective :: (Term, Term, Term) -> Elab' aux ()

158checkInjective :: (Term, Term, Term) -> Elab' aux ()

158checkInjective (tm, l, r) = do ctxt <- get_context

159checkInjective (tm, l, r) = do ctxt <- get_context

159 if isInj ctxt tm then return ()

160 if isInj ctxt tm then return ()

@@ -296,6 +297,9 @@ deferType n ty ns = processTactic' (DeferType n ty ns)

296instanceArg :: Name -> Elab' aux ()

297instanceArg :: Name -> Elab' aux ()

297instanceArg n = processTactic' (Instance n)

298instanceArg n = processTactic' (Instance n)

298

299

300+setinj :: Name -> Elab' aux ()

301+setinj n = processTactic' (SetInjective n)

302+

299proofstate :: Elab' aux ()

303proofstate :: Elab' aux ()

300proofstate = processTactic' ProofState

304proofstate = processTactic' ProofState

301

305

@@ -375,12 +379,14 @@ apply fn imps =

375 if null imps then [] -- do all we can

379 if null imps then [] -- do all we can

376 else

380 else

377 map fst (filter (not.snd) (zip args (map fst imps)))

381 map fst (filter (not.snd) (zip args (map fst imps)))

378− let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

382+ let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

379 unified p

383 unified p

380 let unify = -- trace ("Not done " ++ show hs) $

384 let unify = -- trace ("Not done " ++ show hs) $

381− dropGiven dont hs

385+ dropGiven dont hunis hs

382 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

386 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

383 ptm <- get_term

387 ptm <- get_term

388+ g <- goal

389+-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

384 end_unify

390 end_unify

385 ptm <- get_term

391 ptm <- get_term

386 return (map (updateUnify unify) args)

392 return (map (updateUnify unify) args)

@@ -461,15 +467,20 @@ simple_app fun arg =

461 claim a RType

467 claim a RType

462 claim b RType

468 claim b RType

463 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

469 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

470+ tm <- get_term

464 start_unify s

471 start_unify s

465 claim s (Var a)

472 claim s (Var a)

466 prep_fill f [s]

473 prep_fill f [s]

467 -- try elaborating in both orders, since we might learn something useful

474 -- try elaborating in both orders, since we might learn something useful

468 -- either way

475 -- either way

469− try (do focus s; arg

476+-- try (do focus s; arg

470− focus f; fun)

477+-- focus f; fun)

471− (do focus f; fun

478+-- (do focus f; fun

472− focus s; arg)

479+-- focus s; arg)

480+ focus f; fun

481+ focus s; arg

482+ tm <- get_term

483+ ps <- get_probs

473 complete_fill

484 complete_fill

474 hs <- get_holes

485 hs <- get_holes

475 -- We don't need a and b in the hole queue any more since they were just for

486 -- We don't need a and b in the hole queue any more since they were just for

@@ -493,7 +504,8 @@ try t1 t2 = try' t1 t2 False

493try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

504try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

494try' t1 t2 proofSearch

505try' t1 t2 proofSearch

495 = do s <- get

506 = do s <- get

507+ ps <- get_probs

496− case runStateT t1 s of

508+ case prunStateT ps t1 s of

497 OK (v, s') -> do put s'

509 OK (v, s') -> do put s'

498 return v

510 return v

499 Error e1 -> if proofSearch || recoverableErr e1 then

511 Error e1 -> if proofSearch || recoverableErr e1 then

@@ -525,18 +537,30 @@ tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

525 tryAll' [res] _ [] = res

537 tryAll' [res] _ [] = res

526 tryAll' (_:_) _ [] = cantResolve

538 tryAll' (_:_) _ [] = cantResolve

527 tryAll' [] (f, _) [] = f

539 tryAll' [] (f, _) [] = f

528− tryAll' cs f (x:xs) = do s <- get

540+ tryAll' cs f (x:xs)

541+ = do s <- get

542+ ps <- get_probs

529− case runStateT x s of

543+ case prunStateT ps x s of

530− OK (v, s') -> tryAll' ((do put s'

544+ OK (v, s') -> tryAll' ((do put s'

531− return v):cs) f xs

545+ return v):cs) f xs

532− Error err -> do put s

546+ Error err -> do put s

533− if (score err) < 100

547+ if (score err) < 100

534− then

535− tryAll' cs (better err f) xs

548+ then tryAll' cs (better err f) xs

536− else

537− tryAll' [] (better err f) xs -- give up

549+ else tryAll' [] (better err f) xs -- give up

550+

538

551

539 better err (f, i) = let s = score err in

552 better err (f, i) = let s = score err in

540 if (s >= i) then (lift (tfail err), s)

553 if (s >= i) then (lift (tfail err), s)

541 else (f, i)

554 else (f, i)

542

555

556+prunStateT ps x s

557+ = case runStateT x s of

558+ OK (v, s'@(ES (p, _) _ _)) ->

559+ if (length (problems p) > length ps)

560+ then case reverse (problems p) of

561+ ((_,_,_,e):_) -> Error e

562+ else OK (v, s')

563+ Error e -> Error e

564+

565+dumpprobs [] = ""

566+dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Core/ProofState.hs+98−45

@@ -29,7 +29,7 @@ data ProofState = PS { thname :: Name,

29 unified :: (Name, [(Name, Term)]),

30 solved :: Maybe (Name, Term),

31 problems :: Fails,

32− injective :: [(Term, Term, Term)],

32+ injective :: [Name],

33 deferred :: [Name], -- names we'll need to define

34 instances :: [Name], -- instance arguments (for type classes)

35 previous :: Maybe ProofState, -- for undo

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

68 | Defer Name

69 | DeferType Name Raw [Name]

70 | Instance Name

71+ | SetInjective Name

71 | MoveLast Name

72 | MoveLast Name

72 | ProofState

73 | ProofState

73 | Undo

74 | Undo

@@ -148,15 +149,28 @@ hole _ = False

148

149

149holeName i = MN i "hole"

150holeName i = MN i "hole"

150

151

152+qshow :: Fails -> String

153+qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

154+

151unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]

155unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]

156+unify' ctxt env topx topy =

157+ do ps <- get

152−unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy

158+ (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)

153− addInj inj

159+-- trace ("Unified " ++ show (topx, topy) ++ show (injective ps) ++

160+-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

161+-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps)) $

154− case fails of

162+ case fails of

155− [] -> return u

163+-- [] -> return u

156− err ->

164+ err ->

157− do ps <- get

165+ do ps <- get

166+ let (h, ns) = unified ps

167+ let (ns', probs') = updateProblems (context ps) (u ++ ns)

168+ (err ++ problems ps)

169+ (injective ps)

170+ (holes ps)

158− put (ps { problems = err ++ problems ps })

171+ put (ps { problems = probs',

172+ unified = (h, ns') })

159− return []

173+ return u

160

174

161getName :: Monad m => String -> StateT TState m Name

175getName :: Monad m => String -> StateT TState m Name

162getName tag = do ps <- get

176getName tag = do ps <- get

@@ -194,6 +208,7 @@ goalAtFocus :: ProofState -> TC (Binder Type)

194goalAtFocus ps

208goalAtFocus ps

195 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

209 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

196 return (goalType g)

210 return (goalType g)

211+ | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)

197

212

198goal :: Hole -> Term -> TC Goal

213goal :: Hole -> Term -> TC Goal

199goal h tm = g [] tm where

214goal h tm = g [] tm where

@@ -288,6 +303,12 @@ instanceArg n ctxt env (Bind x (Hole t) sc)

288 instances = x:is })

303 instances = x:is })

289 return (Bind x (Hole t) sc)

304 return (Bind x (Hole t) sc)

290

305

306+setinj :: Name -> RunTactic

307+setinj n ctxt env (Bind x (Hole t) sc)

308+ = do action (\ps -> let is = injective ps in

309+ ps { injective = n : is })

310+ return (Bind x (Hole t) sc)

311+

291defer :: Name -> RunTactic

312defer :: Name -> RunTactic

292defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

313defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

293 do action (\ps -> let hs = holes ps in

314 do action (\ps -> let hs = holes ps in

@@ -322,10 +343,6 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

322 return sc

343 return sc

323regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"

344regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"

324

345

325−addInj :: [(Term, Term, Term)] -> StateT TState TC ()

326−addInj inj = do ps <- get

327− put (ps { injective = inj ++ injective ps })

328−

329exact :: Raw -> RunTactic

346exact :: Raw -> RunTactic

330exact guess ctxt env (Bind x (Hole ty) sc) =

347exact guess ctxt env (Bind x (Hole ty) sc) =

331 do (val, valty) <- lift $ check ctxt env guess

348 do (val, valty) <- lift $ check ctxt env guess

@@ -344,7 +361,7 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

344 ns <- unify' ctxt env valty ty

361 ns <- unify' ctxt env valty ty

345 ps <- get

362 ps <- get

346 let (uh, uns) = unified ps

363 let (uh, uns) = unified ps

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

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

348-- addLog (show (uh, uns ++ ns))

365-- addLog (show (uh, uns ++ ns))

349 return $ Bind x (Guess ty val) sc

366 return $ Bind x (Guess ty val) sc

350fill _ _ _ _ = fail "Can't fill here."

367fill _ _ _ _ = fail "Can't fill here."

@@ -362,22 +379,25 @@ complete_fill ctxt env (Bind x (Guess ty val) sc) =

362 ns <- unify' ctxt env valty ty

379 ns <- unify' ctxt env valty ty

363 ps <- get

380 ps <- get

364 let (uh, uns) = unified ps

381 let (uh, uns) = unified ps

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

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

366 return $ Bind x (Guess ty val) sc

383 return $ Bind x (Guess ty val) sc

367complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

384complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

368

385

369solve :: RunTactic

386solve :: RunTactic

370solve ctxt env (Bind x (Guess ty val) sc)

387solve ctxt env (Bind x (Guess ty val) sc)

371− | pureTerm val = do ps <- get

388+ | True = do ps <- get

372 let (uh, uns) = unified ps

389 let (uh, uns) = unified ps

373 action (\ps -> ps { holes = holes ps \\ [x],

390 action (\ps -> ps { holes = holes ps \\ [x],

374 solved = Just (x, val),

391 solved = Just (x, val),

392+-- problems = solveInProblems

393+-- x val (problems ps),

375 -- dontunify = dontunify ps \\ [x],

394 -- dontunify = dontunify ps \\ [x],

376 -- unified = (uh, uns ++ [(x, val)]),

395 -- unified = (uh, uns ++ [(x, val)]),

377 instances = instances ps \\ [x] })

396 instances = instances ps \\ [x] })

378 return $ {- Bind x (Let ty val) sc -}

397 return $ {- Bind x (Let ty val) sc -}

379 instantiate val (pToV x sc)

398 instantiate val (pToV x sc)

399+ | otherwise = do ps <- get

380− | otherwise = lift $ tfail $ IncompleteTerm val

400+ lift $ tfail $ IncompleteTerm val

381solve _ _ h = do ps <- get

401solve _ _ h = do ps <- get

382 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

402 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

383

403

@@ -396,7 +416,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

396 do ns <- unify' ctxt env s tyv

416 do ns <- unify' ctxt env s tyv

397 ps <- get

417 ps <- get

398 let (uh, uns) = unified ps

418 let (uh, uns) = unified ps

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

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

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

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

401 _ -> fail "Nothing to introduce"

421 _ -> fail "Nothing to introduce"

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

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

@@ -494,7 +514,8 @@ hnf_compute ctxt env (Bind x (Hole ty) sc) =

494 do let ty' = hnf ctxt env ty in

514 do let ty' = hnf ctxt env ty in

495-- trace ("HNF " ++ show (ty, ty')) $

515-- trace ("HNF " ++ show (ty, ty')) $

496 return $ Bind x (Hole ty') sc

516 return $ Bind x (Hole ty') sc

497−

517+hnf_compute ctxt env t = return t

518+

498check_in :: Raw -> RunTactic

519check_in :: Raw -> RunTactic

499check_in t ctxt env tm =

520check_in t ctxt env tm =

500 do (val, valty) <- lift $ check ctxt env t

521 do (val, valty) <- lift $ check ctxt env t

@@ -515,7 +536,7 @@ eval_in t ctxt env tm =

515 return tm

536 return tm

516

537

517start_unify :: Name -> RunTactic

538start_unify :: Name -> RunTactic

518−start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })

539+start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })

519 return tm

540 return tm

520

541

521tmap f (a, b, c) = (f a, b, c)

542tmap f (a, b, c) = (f a, b, c)

@@ -524,22 +545,24 @@ solve_unified :: RunTactic

524solve_unified ctxt env tm =

545solve_unified ctxt env tm =

525 do ps <- get

546 do ps <- get

526 let (_, ns) = unified ps

547 let (_, ns) = unified ps

527− let unify = dropGiven (dontunify ps) ns

548+ let unify = dropGiven (dontunify ps) ns (holes ps)

528 action (\ps -> ps { holes = holes ps \\ map fst unify })

549 action (\ps -> ps { holes = holes ps \\ map fst unify })

529 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

550 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })

530− action (\ps -> ps { injective = map (tmap (updateSolved unify)) (injective ps) })

531 return (updateSolved unify tm)

551 return (updateSolved unify tm)

532 where

552 where

533

553

534−dropGiven du [] = []

554+dropGiven du [] hs = []

535−dropGiven du ((n, P Bound t ty) : us) | n `elem` du && not (t `elem` du)

555+dropGiven du ((n, P Bound t ty) : us) hs

556+ | n `elem` du && not (t `elem` du)

557+ && n `elem` hs && t `elem` hs

536− = (t, P Bound n ty) : dropGiven du us

558+ = (t, P Bound n ty) : dropGiven du us hs

559+dropGiven du (u@(n, _) : us) hs

537−dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us

560+ | n `elem` du = dropGiven du us hs

538-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

561-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

539−dropGiven du (u : us) = u : dropGiven du us

562+dropGiven du (u : us) hs = u : dropGiven du us hs

540

563

541updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

564updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

542− updateSolved' xs x

565+ updateSolved' xs x

543updateSolved' xs (Bind n (Hole ty) t)

566updateSolved' xs (Bind n (Hole ty) t)

544 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))

567 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))

545updateSolved' xs (Bind n b t)

568updateSolved' xs (Bind n b t)

@@ -549,11 +572,30 @@ updateSolved' xs (P _ n _)

549 | Just v <- lookup n xs = v

572 | Just v <- lookup n xs = v

550updateSolved' xs t = t

573updateSolved' xs t = t

551

574

575+updateEnv ns [] = []

576+updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env

577+

578+updateError ns (CantUnify b l r e xs sc)

579+ = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc

580+updateError ns e = e

581+

582+solveInProblems x val [] = []

583+solveInProblems x val ((l, r, env, err) : ps)

584+ = ((instantiate val (pToV x l), instantiate val (pToV x r),

585+ updateEnv [(x, val)] env, err) : solveInProblems x val ps)

586+

552−updateProblems ns [] = []

587+updateProblems ctxt ns ps inj holes = up ns ps where

588+ up ns [] = (ns, [])

553−updateProblems ns ((x, y, env, err) : ps) =

589+ up ns ((x, y, env, err) : ps) =

554 let x' = updateSolved ns x

590 let x' = updateSolved ns x

555− y' = updateSolved ns y in

591+ y' = updateSolved ns y

592+ err' = updateError ns err

593+ env' = updateEnv ns env in

594+ case unify ctxt env' x' y' inj holes of

595+ OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

596+ up (ns ++ v) ps

597+ _ -> let (ns', ps') = up ns ps in

556− (x',y',env,err) : updateProblems ns ps

598+ (ns', (x',y',env',err') : ps')

557

599

558processTactic :: Tactic -> ProofState -> TC (ProofState, String)

600processTactic :: Tactic -> ProofState -> TC (ProofState, String)

559processTactic QED ps = case holes ps of

601processTactic QED ps = case holes ps of

@@ -568,18 +610,16 @@ processTactic Undo ps = case previous ps of

568 Just pold -> return (pold, "")

610 Just pold -> return (pold, "")

569processTactic EndUnify ps

611processTactic EndUnify ps

570 = let (h, ns_in) = unified ps

612 = let (h, ns_in) = unified ps

571− ns = dropGiven (dontunify ps) ns_in

613+ ns = dropGiven (dontunify ps) ns_in (holes ps)

572 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

614 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

615+ (ns'', probs') = updateProblems (context ps) ns' (problems ps)

616+ (injective ps) (holes ps)

573− tm' = -- trace ("Updating " ++ show ns') $ -- ++ " in " ++ show (pterm ps)) $

617+ tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $

574− updateSolved ns' (pterm ps)

618+ updateSolved ns'' (pterm ps) in

575− probs' = updateProblems ns' (problems ps) in

576− case probs' of

577− [] -> return (ps { pterm = tm',

619+ return (ps { pterm = tm',

578− unified = (h, []),

620+ unified = (h, []),

579− injective = map (tmap (updateSolved ns'))

621+ problems = probs',

580− (injective ps),

581− holes = holes ps \\ map fst ns' }, "")

622+ holes = holes ps \\ map fst ns'' }, "")

582− errs@((_,_,_,err):_) -> tfail err

583processTactic (Reorder n) ps

623processTactic (Reorder n) ps

584 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

624 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

585 return (ps' { previous = Just ps, plog = "" }, plog ps')

625 return (ps' { previous = Just ps, plog = "" }, plog ps')

@@ -590,9 +630,21 @@ processTactic t ps

590 let pterm' = case solved ps' of

630 let pterm' = case solved ps' of

591 Just s -> updateSolved [s] (pterm ps')

631 Just s -> updateSolved [s] (pterm ps')

592 _ -> pterm ps'

632 _ -> pterm ps'

633+ let (ns', probs')

634+ = case solved ps' of

635+ Just s -> updateProblems (context ps')

636+ [s] (problems ps')

637+ (injective ps')

638+ (holes ps')

639+ _ -> ([], problems ps')

640+ -- rechecking problems may find more solutions, so

641+ -- apply them here

642+ let pterm'' = updateSolved ns' pterm'

593− return (ps' { pterm = pterm',

643+ return (ps' { pterm = pterm'',

594 solved = Nothing,

644 solved = Nothing,

645+ problems = probs',

595− previous = Just ps, plog = "" }, plog ps')

646+ previous = Just ps, plog = "",

647+ holes = holes ps' \\ (map fst ns')}, plog ps')

596

648

597process :: Tactic -> Name -> StateT TState TC ()

649process :: Tactic -> Name -> StateT TState TC ()

598process EndUnify _

650process EndUnify _

@@ -624,5 +676,6 @@ process t h = tactic (Just h) (mktac t)

624 mktac (Defer n) = defer n

676 mktac (Defer n) = defer n

625 mktac (DeferType n t a) = deferType n t a

677 mktac (DeferType n t a) = deferType n t a

626 mktac (Instance n) = instanceArg n

678 mktac (Instance n) = instanceArg n

679+ mktac (SetInjective n) = setinj n

627 mktac (MoveLast n) = movelast n

680 mktac (MoveLast n) = movelast n

628

681

src/Core/TT.hs+7−3

@@ -480,7 +480,7 @@ data Datatype n = Data { d_typename :: n,

480 deriving (Show, Functor, Eq)

481

482instance Eq n => Eq (TT n) where

483− (==) (P xt x _) (P yt y _) = xt == yt && x == y

483+ (==) (P xt x _) (P yt y _) = x == y

484 (==) (V x) (V y) = x == y

485 (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys

486 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

@@ -788,13 +788,17 @@ showEnv' env t dbg = se 10 env t where

788

789-- Check whether a term has any holes in it - impure if so

790

791−pureTerm :: TT n -> Bool

791+pureTerm :: TT Name -> Bool

792pureTerm (App f a) = pureTerm f && pureTerm a

793−pureTerm (Bind n b sc) = pureBinder b && pureTerm sc where

793+pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

794 pureBinder (Hole _) = False

795 pureBinder (Guess _ _) = False

796 pureBinder (Let t v) = pureTerm t && pureTerm v

797 pureBinder t = pureTerm (binderTy t)

798+

799+ notClassName (MN _ "class") = False

800+ notClassName _ = True

801+

798pureTerm _ = True

802pureTerm _ = True

799

803

800-- weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)

804-- weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)

src/Core/Unify.hs+108−43

@@ -20,25 +20,29 @@ import Debug.Trace

20type Injs = [(TT Name, TT Name, TT Name)]

21type Fails = [(TT Name, TT Name, Env, Err)]

23−data UInfo = UI Int Injs Fails

23+data UInfo = UI Int Fails

24 deriving Show

26+data UResult a = UOK a

27+ | UPartOK a

28+ | UFail Err

29+

26−unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

30+unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

27− Injs, Fails)

31+ TC ([(Name, TT Name)], Fails)

28−unify ctxt env topx topy =

32+unify ctxt env topx topy injtc holes =

29−-- trace ("Unifying " ++ show (topx, topy)) $

33+-- trace ("Unifying " ++ show (topx, topy)) $

30 -- don't bother if topx and topy are different at the head

34 -- don't bother if topx and topy are different at the head

31− case runStateT (un False [] topx topy) (UI 0 [] []) of

35+ case runStateT (un False [] topx topy) (UI 0 []) of

32− OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

36+ OK (v, UI _ []) -> return (filter notTrivial v, [])

33−-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

34 res ->

37 res ->

35 let topxn = normalise ctxt env topx

38 let topxn = normalise ctxt env topx

36 topyn = normalise ctxt env topy in

39 topyn = normalise ctxt env topy in

37-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

40-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n" ++ show res ++ "\n\n") $

38 case runStateT (un False [] topxn topyn)

41 case runStateT (un False [] topxn topyn)

39− (UI 0 [] []) of

42+ (UI 0 []) of

40− OK (v, UI _ inj fails) ->

43+ OK (v, UI _ fails) ->

41− return (filter notTrivial v, inj, reverse fails)

44+ return (filter notTrivial v, reverse fails)

45+-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

42 Error e -> tfail e

46 Error e -> tfail e

43 where

47 where

44 notTrivial (x, P _ x' _) = x /= x'

48 notTrivial (x, P _ x' _) = x /= x'

@@ -50,21 +54,22 @@ unify ctxt env topx topy =

51 injective (P (DCon _ _) _ _) = True

55 injective (P (DCon _ _) _ _) = True

52 injective (P (TCon _ _) _ _) = True

56 injective (P (TCon _ _) _ _) = True

57+ injective (P _ n _) = n `elem` injtc

53 injective (App f a) = injective f

58 injective (App f a) = injective f

54 injective _ = False

59 injective _ = False

56 notP (P _ _ _) = False

61 notP (P _ _ _) = False

57 notP _ = True

62 notP _ = True

59− sc i = do UI s x f <- get

64+ sc i = do UI s f <- get

60− put (UI (s+i) x f)

65+ put (UI (s+i) f)

62− uplus u1 u2 = do UI s i f <- get

67+ uplus u1 u2 = do UI s f <- get

63 r <- u1

68 r <- u1

64− UI s _ f' <- get

69+ UI s f' <- get

65 if (length f == length f')

70 if (length f == length f')

66 then return r

71 then return r

67− else do put (UI s i f); u2

72+ else do put (UI s f); u2

69 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

74 un :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->

70 StateT UInfo

75 StateT UInfo

@@ -89,34 +94,53 @@ unify ctxt env topx topy =

89 = unifyFail topx topy

94 = unifyFail topx topy

90 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

95 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

91 = unifyFail topx topy

96 = unifyFail topx topy

92− un' fn bnames (P Bound x _) (P Bound y _)

97+ un' fn bnames tx@(P _ x _) ty@(P _ y _)

93− | (x,y) `elem` bnames = do sc 1; return []

98+ | (x,y) `elem` bnames || x == y = do sc 1; return []

99+ | injective tx && not (holeIn env y || y `elem` holes)

100+ = unifyFail tx ty

101+ | injective ty && not (holeIn env x || x `elem` holes)

102+ = unifyFail tx ty

94− un' fn bnames (P Bound x _) tm

103+ un' fn bnames xtm@(P _ x _) tm

104+ | holeIn env x || x `elem` holes

95− | holeIn env x = do UI s i f <- get

105+ = do UI s f <- get

96 -- injectivity check

106 -- injectivity check

97− when (notP tm && fn) $

107+ if (notP tm && fn)

98-- trace (show (x, tm, normalise ctxt env tm)) $

108-- trace (show (x, tm, normalise ctxt env tm)) $

99− put (UI s ((tm, topx, topy) : i) f)

109+-- put (UI s ((tm, topx, topy) : i) f)

110+ then unifyTmpFail xtm tm

100− sc 1

111+ else do sc 1

101− checkCycle (x, tm)

112+ checkCycle (x, tm)

113+ | not (injective xtm) && injective tm = unifyFail xtm tm

102− un' fn bnames tm (P Bound y _)

114+ un' fn bnames tm ytm@(P _ y _)

115+ | holeIn env y || y `elem` holes

103− | holeIn env y = do UI s i f <- get

116+ = do UI s f <- get

104 -- injectivity check

117 -- injectivity check

105− when (notP tm && fn) $

118+ if (notP tm && fn)

106-- trace (show (y, tm, normalise ctxt env tm)) $

119-- trace (show (y, tm, normalise ctxt env tm)) $

107− put (UI s ((tm, topx, topy) : i) f)

120+-- put (UI s ((tm, topx, topy) : i) f)

121+ then unifyTmpFail tm ytm

108− sc 1

122+ else do sc 1

109− checkCycle (y, tm)

123+ checkCycle (y, tm)

124+ | not (injective ytm) && injective tm = unifyFail ytm tm

110− un' fn bnames (V i) (P Bound x _)

125+ un' fn bnames (V i) (P _ x _)

111 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

126 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

112− un' fn bnames (P Bound x _) (V i)

127+ un' fn bnames (P _ x _) (V i)

113 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

128 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

114

129

115− un' fn bnames appx@(App fx ax) appy@(App fy ay)

130+ un' fn bnames appx@(App fx ax) appy@(App fy ay)

131+ | injective fx && metavarApp appy

132+ || injective fy && metavarApp appx

133+ || injective fx && injective fy

134+ || fx == fy

116− = do let (headx, _) = unApply fx

135+ = do let (headx, _) = unApply fx

117− let (heady, _) = unApply fy

136+ let (heady, _) = unApply fy

137+ -- fail quickly if the heads are disjoint

118− checkHeads headx heady

138+ checkHeads headx heady

119− uplus -- do the second one if the first adds any errors

139+-- if True then -- (injective fx || injective fy || fx == fy) then

140+-- if (injective fx && metavarApp appy) ||

141+-- (injective fy && metavarApp appx) ||

142+-- (injective fx && injective fy) || fx == fy

143+ uplus

120 (do hf <- un' True bnames fx fy

144 (do hf <- un' True bnames fx fy

121 let ax' = hnormalise hf ctxt env (substNames hf ax)

145 let ax' = hnormalise hf ctxt env (substNames hf ax)

122 let ay' = hnormalise hf ctxt env (substNames hf ay)

146 let ay' = hnormalise hf ctxt env (substNames hf ay)

@@ -129,6 +153,15 @@ unify ctxt env topx topy =

129 hf <- un' False bnames fx' fy'

153 hf <- un' False bnames fx' fy'

130 sc 1

154 sc 1

131 combine bnames hf ha)

155 combine bnames hf ha)

156+ | otherwise

157+ = do let (headx, argsx) = unApply appx

158+ let (heady, argsy) = unApply appy

159+ if (length argsx == length argsy &&

160+ ((headx == heady) || (argsx == argsy) ||

161+ (notFn headx && notFn heady))) then

162+ do uf <- un' True bnames headx heady

163+ unArgs uf argsx argsy

164+ else unifyTmpFail appx appy

132 where hnormalise [] _ _ t = t

165 where hnormalise [] _ _ t = t

133 hnormalise ns ctxt env t = normalise ctxt env t

166 hnormalise ns ctxt env t = normalise ctxt env t

134 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

167 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

@@ -141,6 +174,25 @@ unify ctxt env topx topy =

141 = unifyFail appx appy

174 = unifyFail appx appy

142 checkHeads _ _ = return []

175 checkHeads _ _ = return []

143

176

177+ unArgs as [] [] = return as

178+ unArgs as (x : xs) (y : ys)

179+ = do let x' = hnormalise as ctxt env (substNames as x)

180+ let y' = hnormalise as ctxt env (substNames as y)

181+ as' <- un' False bnames x' y'

182+ vs <- combine bnames as as'

183+ unArgs vs xs ys

184+

185+ metavarApp tm = let (f, args) = unApply tm in

186+ all metavar (f : args)

187+ metavar t = case t of

188+ P _ x _ -> x `elem` holes || holeIn env x

189+ _ -> False

190+ inenv t = case t of

191+ P _ x _ -> x `elem` (map fst env)

192+ _ -> False

193+

194+ notFn t = injective t || metavar t || inenv t

195+

144 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

196 un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _)))

145 | n == n' = un' False bnames x y

197 | n == n' = un' False bnames x y

146 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

198 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

@@ -155,20 +207,28 @@ unify ctxt env topx topy =

155 combine bnames h1 h2

207 combine bnames h1 h2

156 un' fn bnames x y

208 un' fn bnames x y

157 | OK True <- convEq' ctxt x y = do sc 1; return []

209 | OK True <- convEq' ctxt x y = do sc 1; return []

158− | otherwise = do UI s i f <- get

210+ | otherwise = do UI s f <- get

159 let r = recoverable x y

211 let r = recoverable x y

160 let err = CantUnify r

212 let err = CantUnify r

161 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

213 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

162 if (not r) then lift $ tfail err

214 if (not r) then lift $ tfail err

163− else do put (UI s i ((x, y, env, err) : f))

215+ else do put (UI s ((x, y, env, err) : f))

164 return [] -- lift $ tfail err

216 return [] -- lift $ tfail err

165

217

218+ unifyTmpFail x y

219+ = do UI s f <- get

220+ let r = recoverable x y

221+ let err = CantUnify r

222+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

223+ put (UI s ((x, y, env, err) : f))

224+ return []

225+

166 -- shortcut failure, if we *know* nothing can fix it

226 -- shortcut failure, if we *know* nothing can fix it

167− unifyFail x y = do UI s i f <- get

227+ unifyFail x y = do UI s f <- get

168 let r = recoverable x y

228 let r = recoverable x y

169 let err = CantUnify r

229 let err = CantUnify r

170 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

230 topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

171− put (UI s i ((x, y, env, err) : f))

231+ put (UI s ((x, y, env, err) : f))

172 lift $ tfail err

232 lift $ tfail err

173

233

174

234

@@ -186,12 +246,12 @@ unify ctxt env topx topy =

186 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty

246 uB bnames (Pi tx) (Pi ty) = do sc 1; un' False bnames tx ty

187 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

247 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

188 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

248 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

189− uB bnames x y = do UI s i f <- get

249+ uB bnames x y = do UI s f <- get

190 let r = recoverable (binderTy x) (binderTy y)

250 let r = recoverable (binderTy x) (binderTy y)

191 let err = CantUnify r topx topy

251 let err = CantUnify r topx topy

192 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)

252 (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)

193 (errEnv env) s

253 (errEnv env) s

194− put (UI s i ((binderTy x, binderTy y, env, err) : f))

254+ put (UI s ((binderTy x, binderTy y, env, err) : f))

195 return [] -- lift $ tfail err

255 return [] -- lift $ tfail err

196

256

197 checkCycle p@(x, P _ _ _) = return [p]

257 checkCycle p@(x, P _ _ _) = return [p]

@@ -199,6 +259,11 @@ unify ctxt env topx topy =

199 | not (x `elem` freeNames tm) = return [(x, tm)]

259 | not (x `elem` freeNames tm) = return [(x, tm)]

200 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

260 | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

201

261

262+ combineArgs bnames args = ca [] args where

263+ ca acc [] = return acc

264+ ca acc (x : xs) = do x' <- combine bnames acc x

265+ ca x' xs

266+

202 combine bnames as [] = return as

267 combine bnames as [] = return as

203 combine bnames as ((n, t) : bs)

268 combine bnames as ((n, t) : bs)

204 = case lookup n as of

269 = case lookup n as of

src/Idris/ElabDecls.hs+8−6

@@ -514,6 +514,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

514 let lhs_tm = orderPats (getInferTerm lhs')

515 let lhs_ty = getInferType lhs'

516 logLvl 3 ("Elaborated: " ++ show lhs_tm)

517+ logLvl 3 ("Elaborated type: " ++ show lhs_ty)

517 (clhs, clhsty) <- recheckC fc [] lhs_tm

518 (clhs, clhsty) <- recheckC fc [] lhs_tm

518 logLvl 5 ("Checked " ++ show clhs)

519 logLvl 5 ("Checked " ++ show clhs)

519 -- Elaborate where block

520 -- Elaborate where block

@@ -673,7 +674,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

673 (map (pexp . (PRef fc) . fst) bargs_pre ++

674 (map (pexp . (PRef fc) . fst) bargs_pre ++

674 pexp wval :

675 pexp wval :

675 (map (pexp . (PRef fc) . fst) bargs_post))

676 (map (pexp . (PRef fc) . fst) bargs_post))

676− logLvl 1 ("New RHS " ++ show rhs)

677+ logLvl 5 ("New RHS " ++ showImp True rhs)

677 ctxt <- getContext -- New context with block added

678 ctxt <- getContext -- New context with block added

678 i <- get

679 i <- get

679 ((rhs', defer, is), _) <-

680 ((rhs', defer, is), _) <-

@@ -686,6 +687,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

686 def' <- checkDef fc defer

687 def' <- checkDef fc defer

687 addDeferred def'

688 addDeferred def'

688 mapM_ (elabCaseBlock info) is

689 mapM_ (elabCaseBlock info) is

690+ logLvl 5 ("Checked RHS " ++ show rhs')

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

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

690 return $ Right (clhs, crhs)

692 return $ Right (clhs, crhs)

691 where

693 where

@@ -765,6 +767,8 @@ elabClass info syn doc fc constraints tn ps ds

765 (filter clause ds)

767 (filter clause ds)

766 let (methods, imethods)

768 let (methods, imethods)

767 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

769 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

770+ let defaults = map (\ (x, (y, z)) -> (x,y)) defs

771+ addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])

768 -- build instance constructor type

772 -- build instance constructor type

769 -- decorate names of functions to ensure they can't be referred

773 -- decorate names of functions to ensure they can't be referred

770 -- to elsewhere in the class declaration

774 -- to elsewhere in the class declaration

@@ -786,8 +790,6 @@ elabClass info syn doc fc constraints tn ps ds

786 -- add the default definitions

790 -- add the default definitions

787 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

791 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

788 i <- get

792 i <- get

789− let defaults = map (\ (x, (y, z)) -> (x,y)) defs

790− addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])

791 addIBC (IBCClass tn)

793 addIBC (IBCClass tn)

792 where

794 where

793 nodoc (n, (_, o, t)) = (n, (o, t))

795 nodoc (n, (_, o, t)) = (n, (o, t))

@@ -800,7 +802,7 @@ elabClass info syn doc fc constraints tn ps ds

800

802

801 impbind [] x = x

803 impbind [] x = x

802 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

804 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

803− conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

805+ conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

804 conbind [] x = x

806 conbind [] x = x

805

807

806 getMName (PTy _ _ _ _ n _) = nsroot n

808 getMName (PTy _ _ _ _ n _) = nsroot n

@@ -888,7 +890,7 @@ elabClass info syn doc fc constraints tn ps ds

888

890

889 insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

891 insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

890 = PPi p n ty (insertConstraint c sc)

892 = PPi p n ty (insertConstraint c sc)

891− insertConstraint c sc = PPi constraint (MN 0 "c") c sc

893+ insertConstraint c sc = PPi constraint (MN 0 "class") c sc

892

894

893 -- make arguments explicit and don't bind class parameters

895 -- make arguments explicit and don't bind class parameters

894 toExp ns e (PPi (Imp l s _) n ty sc)

896 toExp ns e (PPi (Imp l s _) n ty sc)

@@ -1010,7 +1012,7 @@ elabInstance info syn fc cs n ps t expn ds

1010

1012

1011 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

1013 mkTyDecl (n, op, t, _) = PTy "" syn fc op n t

1012

1014

1013− conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x)

1015+ conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

1014 conbind [] x = x

1016 conbind [] x = x

1015

1017

1016 coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

1018 coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

src/Idris/ElabTerm.hs+132−39

@@ -39,6 +39,27 @@ build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

39 ElabD (Term, [(Name, Type)], [PDecl])

40build ist info pattern fn tm

41 = do elab ist info pattern False fn tm

42+ ivs <- get_instances

43+ hs <- get_holes

44+ ptm <- get_term

45+ -- Resolve remaining type classes. Two passes - first to get the

46+ -- default Num instances, second to clean up the rest

47+ when (not pattern) $

48+ mapM_ (\n -> when (n `elem` hs) $

49+ do focus n

50+ try (resolveTC 7 fn ist)

51+ (movelast n)) ivs

52+ ivs <- get_instances

53+ hs <- get_holes

54+ when (not pattern) $

55+ mapM_ (\n -> when (n `elem` hs) $

56+ do focus n

57+ resolveTC 7 fn ist) ivs

58+ probs <- get_probs

59+ tm <- get_term

60+ case probs of

61+ [] -> return ()

62+ ((_,_,_,e):es) -> lift (Error e)

42 is <- getAux

63 is <- getAux

43 tt <- get_term

64 tt <- get_term

44 let (tm, ds) = runState (collectDeferred tt) []

65 let (tm, ds) = runState (collectDeferred tt) []

@@ -54,6 +75,11 @@ buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

54 ElabD (Term, [(Name, Type)], [PDecl])

75 ElabD (Term, [(Name, Type)], [PDecl])

55buildTC ist info pattern tcgen fn tm

76buildTC ist info pattern tcgen fn tm

56 = do elab ist info pattern tcgen fn tm

77 = do elab ist info pattern tcgen fn tm

78+ probs <- get_probs

79+ tm <- get_term

80+ case probs of

81+ [] -> return ()

82+ ((_,_,_,e):es) -> lift (Error e)

57 is <- getAux

83 is <- getAux

58 tt <- get_term

84 tt <- get_term

59 let (tm, ds) = runState (collectDeferred tt) []

85 let (tm, ds) = runState (collectDeferred tt) []

@@ -72,8 +98,6 @@ elab ist info pattern tcgen fn tm

72 (do update_term orderPats

98 (do update_term orderPats

73-- tm <- get_term

99-- tm <- get_term

74 mkPat)

100 mkPat)

75− inj <- get_inj

76− mapM_ checkInjective inj

77 where

101 where

78 isph arg = case getTm arg of

102 isph arg = case getTm arg of

79 Placeholder -> (True, priority arg)

103 Placeholder -> (True, priority arg)

@@ -110,11 +134,11 @@ elab ist info pattern tcgen fn tm

110 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

134 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

111 = resolveTC 5 fn ist

135 = resolveTC 5 fn ist

112 elab' ina (PResolveTC fc)

136 elab' ina (PResolveTC fc)

113− | pattern = do c <- unique_hole (MN 0 "c")

137+ | True = do c <- unique_hole (MN 0 "class")

114− instanceArg c

138+ instanceArg c

115 | otherwise = do g <- goal

139 | otherwise = do g <- goal

116 try (resolveTC 2 fn ist)

140 try (resolveTC 2 fn ist)

117− (do c <- unique_hole (MN 0 "c")

141+ (do c <- unique_hole (MN 0 "class")

118 instanceArg c)

142 instanceArg c)

119 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

143 elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

120 pimp (MN 0 "x") t])

144 pimp (MN 0 "x") t])

@@ -122,15 +146,23 @@ elab ist info pattern tcgen fn tm

122 pimp (MN 0 "b") Placeholder,

146 pimp (MN 0 "b") Placeholder,

123 pexp l, pexp r])

147 pexp l, pexp r])

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

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

149+ = do hnf_compute

150+ g <- goal

151+ case g of

125− = try (elabE (True, a) (PApp fc (PRef fc pairTy)

152+ TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)

126− [pexp l,pexp r]))

153+ [pexp l,pexp r])

127− (elabE (True, a) (PApp fc (PRef fc pairCon)

154+ _ -> elabE (True, a) (PApp fc (PRef fc pairCon)

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

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

129 pimp (MN 0 "B") Placeholder,

156 pimp (MN 0 "B") Placeholder,

130− pexp l, pexp r]))

157+ pexp l, pexp r])

131 elab' ina (PDPair fc l@(PRef _ n) t r)

158 elab' ina (PDPair fc l@(PRef _ n) t r)

132 = case t of

159 = case t of

133− Placeholder -> try asType asValue

160+ Placeholder ->

161+ do hnf_compute

162+ g <- goal

163+ case g of

164+ TType _ -> asType

165+ _ -> asValue

134 _ -> asType

166 _ -> asType

135 where asType = elab' ina (PApp fc (PRef fc sigmaTy)

167 where asType = elab' ina (PApp fc (PRef fc sigmaTy)

136 [pexp t,

168 [pexp t,

@@ -144,10 +176,14 @@ elab ist info pattern tcgen fn tm

144 pimp (MN 0 "P") Placeholder,

176 pimp (MN 0 "P") Placeholder,

145 pexp l, pexp r])

177 pexp l, pexp r])

146 elab' ina (PAlternative True as)

178 elab' ina (PAlternative True as)

179+ = do hnf_compute

147− = do ty <- goal

180+ ty <- goal

148 ctxt <- get_context

181 ctxt <- get_context

149 let (tc, _) = unApply ty

182 let (tc, _) = unApply ty

150 let as' = pruneByType tc ctxt as

183 let as' = pruneByType tc ctxt as

184+-- case as' of

185+-- [a] -> elab' ina a

186+-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

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

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

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

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

153 showHd x = show x

189 showHd x = show x

@@ -181,6 +217,7 @@ elab ist info pattern tcgen fn tm

181 = do -- n' <- unique_hole n

217 = do -- n' <- unique_hole n

182 -- let sc' = mapPT (repN n n') sc

218 -- let sc' = mapPT (repN n n') sc

183 ptm <- get_term

219 ptm <- get_term

220+ g <- goal

184 attack; intro (Just n);

221 attack; intro (Just n);

185 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

222 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

186 elabE (True, a) sc; solve

223 elabE (True, a) sc; solve

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

231 focus valn

268 focus valn

232 elabE (True, a) val

269 elabE (True, a) val

233 elabE (True, a) sc

270 elabE (True, a) sc

271+ ptm <- get_term

234 solve

272 solve

235 elab' ina tm@(PApp fc (PInferRef _ f) args) = do

273 elab' ina tm@(PApp fc (PInferRef _ f) args) = do

236 rty <- goal

274 rty <- goal

@@ -283,37 +321,58 @@ elab ist info pattern tcgen fn tm

283 _ ->-} args'

321 _ ->-} args'

284-- newtm <- mkSpecialised ist fc f (map getTm args') tm

322-- newtm <- mkSpecialised ist fc f (map getTm args') tm

285 ivs <- get_instances

323 ivs <- get_instances

324+ ps <- get_probs

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

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

287 -- function or default definition.

326 -- function or default definition.

288 let isinf = f == inferCon || tcname f

327 let isinf = f == inferCon || tcname f

328+ -- if f is a type class, we need to know its arguments so that

329+ -- we can unify with them

330+ case lookupCtxt Nothing f (idris_classes ist) of

331+ [] -> return ()

332+ _ -> mapM_ setInjective (map getTm args')

289 ctxt <- get_context

333 ctxt <- get_context

290 let guarded = isConName Nothing f ctxt

334 let guarded = isConName Nothing f ctxt

291-- when True

335-- when True

292− tryWhen True

336+ (ns, committed) <- tryWhen False

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

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

338+ return (ns, True))

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

340+ mkSpecialised ist fc f (map getTm args') tm

341+ solve

342+ return ([], False))

343+ when committed $

294− ptm <- get_term

344+ do ptm <- get_term

345+ g <- goal

295 let (ns', eargs) = unzip $

346 let (ns', eargs) = unzip $

296 sortBy (\(_,x) (_,y) ->

347 sortBy (\(_,x) (_,y) ->

297 compare (priority x) (priority y))

348 compare (priority x) (priority y))

298 (zip ns args)

349 (zip ns args)

299− tryWhen True

350+ tryWhen False

300 (elabArgs (ina || not isinf, guarded)

351 (elabArgs (ina || not isinf, guarded)

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

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

302 (elabArgs (ina || not isinf, guarded)

353 (elabArgs (ina || not isinf, guarded)

303 [] False (reverse ns')

354 [] False (reverse ns')

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

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

305 mkSpecialised ist fc f (map getTm args') tm

356 mkSpecialised ist fc f (map getTm args') tm

306− solve)

357+ solve

307− (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

308− mkSpecialised ist fc f (map getTm args') tm

309− solve)

310−-- ptm <- get_term

358+ ptm <- get_term

311-- elog (show ptm)

359-- elog (show ptm)

312 ivs' <- get_instances

360 ivs' <- get_instances

361+ ps' <- get_probs

362+ -- Attempt to resolve any type classes which have 'complete' types,

363+ -- i.e. no holes in them

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

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

314 mapM_ (\n -> do focus n

365 mapM_ (\n -> do focus n

366+ g <- goal

367+ env <- get_env

368+ hs <- get_holes

369+ if all (\n -> not (n `elem` hs)) (freeNames g)

315 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

370 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

316− resolveTC 7 fn ist) (ivs' \\ ivs)

371+ then try (resolveTC 7 fn ist)

372+ (movelast n)

373+ else movelast n)

374+ (ivs' \\ ivs)

375+-- ivs'

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

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

318 tcArg _ = False

377 tcArg _ = False

319

378

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

321 tacTm (PProof _) = True

380 tacTm (PProof _) = True

322 tacTm _ = False

381 tacTm _ = False

323

382

383+ setInjective (PRef _ n) = setinj n

384+ setInjective (PApp _ (PRef _ n) _) = setinj n

385+ setInjective _ = return ()

386+

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

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

325 = erun fc $

388 = erun fc $

326 do ptm <- get_term

389 do ptm <- get_term

@@ -436,22 +499,29 @@ pruneAlt xs = map prune xs

436

499

437-- Rule out alternatives that don't return the same type as the head of the goal

500-- Rule out alternatives that don't return the same type as the head of the goal

438-- (If there are none left as a result, do nothing)

501-- (If there are none left as a result, do nothing)

439−

440pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

502pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

441pruneByType (P _ n _) c as

503pruneByType (P _ n _) c as

504+-- if the goal type is polymorphic, keep e

505+ | [] <- lookupTy Nothing n c = as

506+ | otherwise

507+ = let asV = filter (headIs True n) as

442− = let as' = filter (headIs n) as in

508+ as' = filter (headIs False n) as in

443− case as' of

509+ case as' of

510+ [] -> case asV of

444− [] -> as

511+ [] -> as

512+ _ -> asV

445− _ -> as'

513+ _ -> as'

446 where

514 where

447− headIs f (PApp _ (PRef _ f') _) = typeHead f f'

515+ headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

448− headIs f (PApp _ f' _) = headIs f f'

516+ headIs var f (PApp _ f' _) = headIs var f f'

449− headIs f (PPi _ _ _ sc) = headIs f sc

517+ headIs var f (PPi _ _ _ sc) = headIs var f sc

450− headIs _ _ = True -- keep if it's not an application

518+ headIs _ _ _ = True -- keep if it's not an application

451

519

520+ typeHead var f f'

452− typeHead f f' = case lookupTy Nothing f' c of

521+ = case lookupTy Nothing f' c of

453 [ty] -> case unApply (getRetTy ty) of

522 [ty] -> case unApply (getRetTy ty) of

454 (P _ ftyn _, _) -> ftyn == f

523 (P _ ftyn _, _) -> ftyn == f

524+ (V _, _) -> var -- keep, variable

455 _ -> False

525 _ -> False

456 _ -> False

526 _ -> False

457

527

@@ -462,13 +532,20 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

462 (PRefl (FC "prf" 0) Placeholder)

532 (PRefl (FC "prf" 0) Placeholder)

463 return ())

533 return ())

464 (do env <- get_env

534 (do env <- get_env

535+ g <- goal

465− tryAll (map fst env)

536+ tryAll env

466 return ()) True

537 return ()) True

467 where

538 where

468 tryAll [] = fail "No trivial solution"

539 tryAll [] = fail "No trivial solution"

540+ tryAll ((x, b):xs)

541+ = do -- if type of x has any holes in it, move on

542+ hs <- get_holes

543+ g <- goal

544+ if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))

469− tryAll (x:xs) = try' (elab ist toplevel False False

545+ then try' (elab ist toplevel False False

470 (MN 0 "tac") (PRef (FC "prf" 0) x))

546 (MN 0 "tac") (PRef (FC "prf" 0) x))

471 (tryAll xs) True

547 (tryAll xs) True

548+ else tryAll xs

472

549

473findInstances :: IState -> Term -> [Name]

550findInstances :: IState -> Term -> [Name]

474findInstances ist t

551findInstances ist t

@@ -483,7 +560,11 @@ resolveTC 0 fn ist = fail $ "Can't resolve type class"

483resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True

560resolveTC 1 fn ist = try' (trivial ist) (resolveTC 0 fn ist) True

484resolveTC depth fn ist

561resolveTC depth fn ist

485 = do hnf_compute

562 = do hnf_compute

563+ g <- goal

564+ ptm <- get_term

565+ hs <- get_holes

566+ if True -- all (\n -> not (n `elem` hs)) (freeNames g)

486− try' (trivial ist)

567+ then try' (trivial ist)

487 (do t <- goal

568 (do t <- goal

488 let insts = findInstances ist t

569 let insts = findInstances ist t

489 let (tc, ttypes) = unApply t

570 let (tc, ttypes) = unApply t

@@ -491,17 +572,23 @@ resolveTC depth fn ist

491 tm <- get_term

572 tm <- get_term

492-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

573-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $

493-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

574-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

575+-- if scopeOnly then fail "Can't resolve" else

494 let depth' = if scopeOnly then 2 else depth

576 let depth' = if scopeOnly then 2 else depth

495 blunderbuss t depth' insts) True

577 blunderbuss t depth' insts) True

578+ else do try' (trivial ist)

579+ (do g <- goal

580+ fail $ "Can't resolve " ++ show g) True

581+-- tm <- get_term

582+-- fail $ "Can't resolve yet in " ++ show tm

496 where

583 where

497 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

584 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

498 | otherwise = (fail "Can't resolve", show n)

585 | otherwise = (fail "Can't resolve", show n)

499

586

500−-- needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]

587+ needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]

501−-- = do focus a

588+ = do focus a

502−-- fill (RConstant IType) -- default Int

589+ fill (RConstant IType) -- default Int

503−-- solve

590+ solve

504−-- return False

591+ return False

505 needsDefault t f as

592 needsDefault t f as

506 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

593 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

507 needsDefault t f a = return False -- trace (show t) $ return ()

594 needsDefault t f a = return False -- trace (show t) $ return ()

@@ -509,7 +596,9 @@ resolveTC depth fn ist

509 boundVar (P Bound _ _) = True

596 boundVar (P Bound _ _) = True

510 boundVar _ = False

597 boundVar _ = False

511

598

599+ blunderbuss t d [] = do -- c <- get_env

600+ -- ps <- get_probs

512− blunderbuss t d [] = lift $ tfail $ CantResolve t

601+ lift $ tfail $ CantResolve t

513 blunderbuss t d (n:ns)

602 blunderbuss t d (n:ns)

514 | n /= fn && tcname n = try' (resolve n d)

603 | n /= fn && tcname n = try' (resolve n d)

515 (blunderbuss t d ns) True

604 (blunderbuss t d ns) True

@@ -526,7 +615,10 @@ resolveTC depth fn ist

526 let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

615 let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

527 [] -> []

616 [] -> []

528 [args] -> map isImp (snd args) -- won't be overloaded!

617 [args] -> map isImp (snd args) -- won't be overloaded!

618+ ps <- get_probs

529 args <- apply (Var n) imps

619 args <- apply (Var n) imps

620+ ps' <- get_probs

621+ when (length ps < length ps') $ fail "Can't apply type class"

530 -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

622 -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

531 mapM_ (\ (_,n) -> do focus n

623 mapM_ (\ (_,n) -> do focus n

532 t' <- goal

624 t' <- goal

@@ -535,6 +627,7 @@ resolveTC depth fn ist

535 resolveTC depth' fn ist)

627 resolveTC depth' fn ist)

536 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

628 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

537 -- if there's any arguments left, we've failed to resolve

629 -- if there's any arguments left, we've failed to resolve

630+ hs <- get_holes

538 solve

631 solve

539 where isImp (PImp p _ _ _ _) = (True, p)

632 where isImp (PImp p _ _ _ _) = (True, p)

540 isImp arg = (False, priority arg)

633 isImp arg = (False, priority arg)

test/reg002/reg002.idr+2−2

@@ -13,10 +13,10 @@ S Infinity = Infinity

13Sn_notzero : Main.S n = Co 0 -> _|_

14Sn_notzero = believe_me

16−S_Co_not_Inf : S (Co n) = Infinity -> _|_

16+S_Co_not_Inf : Main.S (Co n) = Infinity -> _|_

17S_Co_not_Inf = believe_me

19−S_inj : (n : CoNat) -> (m : CoNat) -> S n = S m -> n = m

19+S_inj : (n : CoNat) -> (m : CoNat) -> Main.S n = Main.S m -> n = m

20S_inj (Co n) (Co _) refl = refl

21S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)

22S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))

test/reg005/reg005.idr+1−1

@@ -18,7 +18,7 @@ eq x y = if x == y then Just ?eqCharOK else Nothing

18rle : (xs : Vect Char n) -> RLE xs

19rle [] = REnd

20rle (x :: xs) with (rle xs)

21− rle (x :: []) | REnd = RChar O x REnd

21+ rle (x :: Vect.Nil) | REnd = RChar O x REnd

22 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

23 rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p

24 = RChar (S n) x rs

test/reg008/reg008.idr+1−1

@@ -8,7 +8,7 @@ data Cmp : Nat -> Nat -> Type where

8total cmp : (x, y : Nat) -> Cmp x y

9cmp O O = cmpEQ

10cmp O (S k) = cmpLT _

11−cmp (S k) O = cmpGT _

11+cmp (S k) O = cmpGT _

12cmp (S x) (S y) with (cmp x y)

13 cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k

14 cmp (S x) (S x) | cmpEQ = cmpEQ

test/reg009/reg009.lidr+1−1

@@ -7,7 +7,7 @@

7> (as : Vect alpha n) ->

8> so (isAnyBy p (n ** as)) ->

9> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O)))

10−> filterTagP p (a :: as) q with (p a)

10+> filterTagP {n = S m} p (a :: as) q with (p a)

11> | True = (_

12> **

13> ((a ** believe_me oh)

test/test005/test005.idr+6−7

@@ -7,10 +7,9 @@ tlist : List Int

7tlist = [1, 2, 3, 4, 5]

9main : IO ()

10−main = do { print (abs (-8))

10+main = do print (abs (-8))

11− print (abs (S O))

11+ print (abs (S O))

12− print (span isAlpha tstr)

12+ print (span isAlpha tstr)

13− print (break isDigit tstr)

13+ print (break isDigit tstr)

14− print (span (\x => x < 3) tlist)

14+ print (span (\x => x < 3) tlist)

15− print (break (\x => x > 2) tlist)

15+ print (break (\x => x > 2) tlist)

16− }

test/test006/test006.idr+4−4

@@ -8,14 +8,14 @@ parity : (n:Nat) -> Parity n

8parity O = even {n=O}

9parity (S O) = odd {n=O}

10parity (S (S k)) with (parity k)

11− parity (S (S (j + j))) | even ?= even {n=S j}

11+ parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j}

12− parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

12+ parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j}

14natToBin : Nat -> List Bool

15natToBin O = Nil

16natToBin k with (parity k)

17− natToBin (j + j) | even = False :: natToBin j

17+ natToBin (j + j) | even {n = j} = False :: natToBin j

18− natToBin (S (j + j)) | odd = True :: natToBin j

18+ natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

20main : IO ()

21main = do print (natToBin 42)

test/test007/test007.idr+1−2

@@ -35,8 +35,7 @@ runEval env e with (eval e) {

35}

37main : IO ()

38−main = do print [| (*2) (Just 4) |]

38+main = do print [| (\x => x *2) (Just 4) |]

39 print [| plus (Just 4) (Just 5) |]

40 print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))))

41 print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))))

42−

test/test014/Resimp.idr+2

@@ -109,6 +109,8 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

109 (>>=) : Res gam gam' (R a) -> (a -> Res gam' gam'' (R t)) ->

110 Res gam gam'' (R t)

111

112+ ioret : a -> IO a

113+ ioret = return

112

114

113 interp : Env gam -> {static} Res gam gam' t ->

115 interp : Env gam -> {static} Res gam gam' t ->

114 (Env gam' -> interpTy t -> IO u) -> IO u

116 (Env gam' -> interpTy t -> IO u) -> IO u

test/test018/test018a.idr+2−2

@@ -13,8 +13,8 @@ ping main proc

14pong : Process String ()

15pong = do -- lift (putStrLn "Waiting for message")

16− (sender, msg) <- recvWithSender

16+ (sender, m) <- recvWithSender

17− lift $ putStrLn ("Received " ++ msg)

17+ lift $ putStrLn ("Received " ++ m)

18 send sender ("Hello back!")

20mainProc : Process String ()

tutorial/examples/interp.idr+3

@@ -44,6 +44,9 @@ using (G : Vect Ty n)

45 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

46 eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))

47+

48+ eEq : Expr G (TyFun TyInt (TyFun TyInt TyBool))

49+ eEq = Lam (Lam (Op (==) (Var stop) (Var (pop stop))))

48 eDouble : Expr G (TyFun TyInt TyInt)

51 eDouble : Expr G (TyFun TyInt TyInt)

49 eDouble = Lam (App (App eAdd (Var stop)) (Var stop))

52 eDouble = Lam (App (App eAdd (Var stop)) (Var stop))