e7c9256 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow inference of Sets at REPL

commite7c92569cf2e2a183de1becd921fcd40c7ea418a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 26 Nov 2012, 15:39 (14 years ago) parent50d93dc

3 files changed+20−5

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabDecls.hs+13−4 src/Idris/Error.hs+6

src/Idris/AbsSyntax.hs+1−1

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

390390getInferTerm, getInferType :: Term -> Term

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

392392getInferTerm (App (App _ _) tm) = tm

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

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

394394

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

396396getInferType (App (App _ ty) _) = ty

src/Idris/ElabDecls.hs+13−4

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

417417 i <- get

418418 let tm = addImpl i tm_in

419419 logLvl 10 (showImp True tm)

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

421− (build i info aspat (MN 0 "val") (infTerm 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))

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

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

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

423431 let vtm = getInferTerm tm'

424432 logLvl 2 (show vtm)

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

533541 i <- get

534542 let lhs = addImpl i lhs_in

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

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

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

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

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

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

538547 let lhs_tm = orderPats (getInferTerm lhs')

539548 let lhs_ty = getInferType lhs'

540549 let ret_ty = getRetTy lhs_ty

src/Idris/Error.hs+6

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

5858 _ -> return ()

5959 throwIO (IErr $ pshow i err)

6060

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+

6167getErrLine str

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

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