e7c9256 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow inference of Sets at REPL

e7c9256Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -390,7 +390,7 @@ infP = P (TCon 6 0) inferTy (Set (UVal 0))

390getInferTerm, getInferType :: Term -> Term

391getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc

392getInferTerm (App (App _ _) tm) = tm

393−getInferTerm tm = error ("getInferTerm " ++ show tm)

393+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

394

395getInferType (Bind n b sc) = Bind n b $ getInferType sc

396getInferType (App (App _ ty) _) = ty

src/Idris/ElabDecls.hs+13−4

@@ -417,8 +417,16 @@ elabVal info aspat tm_in

417 i <- get

418 let tm = addImpl i tm_in

419 logLvl 10 (showImp True tm)

420+ -- try:

421+ -- * ordinary elaboration

422+ -- * elaboration as a Set

423+ -- * elaboration as a function a -> b

424+

425+ ((tm', defer, is), _) <-

426+ tctry (elaborate ctxt (MN 0 "val") (Set (UVal 0)) []

427+ (build i info aspat (MN 0 "val") tm))

420− ((tm', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "val") infP []

428+ (elaborate ctxt (MN 0 "val") infP []

421− (build i info aspat (MN 0 "val") (infTerm tm))

429+ (build i info aspat (MN 0 "val") (infTerm tm)))

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

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

423 let vtm = getInferTerm tm'

431 let vtm = getInferTerm tm'

424 logLvl 2 (show vtm)

432 logLvl 2 (show vtm)

@@ -533,8 +541,9 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

533 i <- get

541 i <- get

534 let lhs = addImpl i lhs_in

542 let lhs = addImpl i lhs_in

535 logLvl 5 ("LHS: " ++ showImp True lhs)

543 logLvl 5 ("LHS: " ++ showImp True lhs)

544+ ((lhs', dlhs, []), _) <-

536− ((lhs', dlhs, []), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP []

545+ tclift $ elaborate ctxt (MN 0 "patLHS") infP []

537− (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

546+ (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

538 let lhs_tm = orderPats (getInferTerm lhs')

547 let lhs_tm = orderPats (getInferTerm lhs')

539 let lhs_ty = getInferType lhs'

548 let lhs_ty = getInferType lhs'

540 let ret_ty = getRetTy lhs_ty

549 let ret_ty = getRetTy lhs_ty

src/Idris/Error.hs+6

@@ -58,6 +58,12 @@ tclift tc = case tc of

58 _ -> return ()

59 throwIO (IErr $ pshow i err)

61+tctry :: TC a -> TC a -> Idris a

62+tctry tc1 tc2

63+ = case tc1 of

64+ OK v -> return v

65+ Error err -> tclift tc2

66+

61getErrLine str

67getErrLine str

62 = case span (/=':') str of

68 = case span (/=':') str of

63 (_, ':':rest) -> case span isDigit rest of

69 (_, ':':rest) -> case span isDigit rest of