6d54cb3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Disallow explicit types on LHS

6d54cb3Edwin Brady12 years ago

src/Idris/CaseSplit.hs+3−1

compare with master

unifiedsplit

@@ -57,7 +57,9 @@ split n t'

57 = do ist <- getIState

58 -- Make sure all the names in the term are accessible

59 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')

60+ -- ETyDecl rather then ELHS because there'll be explicit type

61+ -- matching

60− (tm, ty, pats) <- elabValBind recinfo ELHS True (addImplPat ist t')

62+ (tm, ty, pats) <- elabValBind recinfo ETyDecl True (addImplPat ist t')

61 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

63 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

62 -- need to do anything special to find out what family each argument

64 -- need to do anything special to find out what family each argument

63 -- is in

65 -- is in

src/Idris/Core/CaseTree.hs+2−5

@@ -374,11 +374,8 @@ toPat reflect tc = map $ toPat' []

374

375 toPat' [] (P Bound n ty) = PV n ty

376 toPat' args (App f a) = toPat' (a : args) f

377− toPat' [] (Constant (AType _)) = PTyPat

377+ toPat' [] (Constant x) | isTypeConst x = PTyPat

378− toPat' [] (Constant StrType) = PTyPat

378+ | otherwise = PConst x

379− toPat' [] (Constant PtrType) = PTyPat

380− toPat' [] (Constant VoidType) = PTyPat

381− toPat' [] (Constant x) = PConst x

382

379

383 toPat' [] (Bind n (Pi t _) sc)

380 toPat' [] (Bind n (Pi t _) sc)

384 | reflect && noOccurrence n sc

381 | reflect && noOccurrence n sc

src/Idris/Core/ProofState.hs+24−24

@@ -876,13 +876,13 @@ processTactic EndUnify ps

876 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

877 (ns'', probs') = updateProblems ps ns' (problems ps)

878 tm' = updateSolved ns'' (pterm ps) in

879− traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

879+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

880− return (ps { pterm = tm',

880+ return (ps { pterm = tm',

881− unified = (h, []),

881+ unified = (h, []),

882− problems = probs',

882+ problems = probs',

883− notunified = updateNotunified ns'' (notunified ps),

883+ notunified = updateNotunified ns'' (notunified ps),

884− recents = recents ps ++ map fst ns'',

884+ recents = recents ps ++ map fst ns'',

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

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

886processTactic UnifyAll ps

887 = let tm' = updateSolved (notunified ps) (pterm ps) in

888 return (ps { pterm = tm',

@@ -897,24 +897,24 @@ processTactic (ComputeLet n) ps

897 computeLet (context ps) n

898 (getProofTerm (pterm ps)) }, "")

899processTactic UnifyProblems ps

900− = let (ns', probs') = updateProblems ps [] (problems ps)

900+ = do let (ns', probs') = updateProblems ps [] (problems ps)

901− pterm' = updateSolved ns' (pterm ps) in

901+ pterm' = updateSolved ns' (pterm ps)

902− traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

902+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $

903− return (ps { pterm = pterm', solved = Nothing, problems = probs',

903+ return (ps { pterm = pterm', solved = Nothing, problems = probs',

904− previous = Just ps, plog = "",

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

905− notunified = updateNotunified ns' (notunified ps),

905+ notunified = updateNotunified ns' (notunified ps),

906− recents = recents ps ++ map fst ns',

906+ recents = recents ps ++ map fst ns',

907− holes = holes ps \\ (map fst ns') }, plog ps)

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

908processTactic (MatchProblems all) ps

909− = let (ns', probs') = matchProblems all ps [] (problems ps)

909+ = do let (ns', probs') = matchProblems all ps [] (problems ps)

910− (ns'', probs'') = matchProblems all ps ns' probs'

910+ (ns'', probs'') = matchProblems all ps ns' probs'

911− pterm' = updateSolved ns'' (pterm ps) in

911+ pterm' = updateSolved ns'' (pterm ps)

912− traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

912+ traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $

913− return (ps { pterm = pterm', solved = Nothing, problems = probs'',

913+ return (ps { pterm = pterm', solved = Nothing, problems = probs'',

914− previous = Just ps, plog = "",

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

915− notunified = updateNotunified ns'' (notunified ps),

915+ notunified = updateNotunified ns'' (notunified ps),

916− recents = recents ps ++ map fst ns'',

916+ recents = recents ps ++ map fst ns'',

917− holes = holes ps \\ (map fst ns'') }, plog ps)

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

918processTactic t ps

919 = case holes ps of

920 [] -> fail "Nothing to fill in."

src/Idris/Core/TT.hs+9

@@ -553,6 +553,15 @@ deriving instance Binary Const

553deriving instance NFData Const

554!-}

555

556+isTypeConst :: Const -> Bool

557+isTypeConst (AType _) = True

558+isTypeConst StrType = True

559+isTypeConst ManagedPtrType = True

560+isTypeConst BufferType = True

561+isTypeConst PtrType = True

562+isTypeConst VoidType = True

563+isTypeConst _ = False

564+

556instance Sized Const where

565instance Sized Const where

557 size _ = 1

566 size _ = 1

558

567

src/Idris/ElabTerm.hs+85−52

@@ -138,6 +138,13 @@ buildTC ist info emode opts fn tm

138 else return (tm, ds, is)

139 where pattern = emode == ELHS

140

141+data ElabCtxt = ElabCtxt { e_inarg :: Bool,

142+ e_guarded :: Bool,

143+ e_intype :: Bool,

144+ e_qq :: Bool }

145+

146+initElabCtxt = ElabCtxt False False False False

147+

141-- Returns the set of declarations we need to add to complete the definition

148-- Returns the set of declarations we need to add to complete the definition

142-- (most likely case blocks to elaborate)

149-- (most likely case blocks to elaborate)

143

150

@@ -148,7 +155,7 @@ elab ist info emode opts fn tm

148 when (loglvl > 5) $ unifyLog True

155 when (loglvl > 5) $ unifyLog True

149 compute -- expand type synonyms, etc

156 compute -- expand type synonyms, etc

150 let fc = maybe "(unknown)"

157 let fc = maybe "(unknown)"

151− elabE (False, False, False, False) (elabFC info) tm -- (in argument, guarded, in type, in qquote)

158+ elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

152 end_unify

159 end_unify

153 ptm <- get_term

160 ptm <- get_term

154 when pattern -- convert remaining holes to pattern vars

161 when pattern -- convert remaining holes to pattern vars

@@ -186,7 +193,7 @@ elab ist info emode opts fn tm

186 -- and forces/delays. If you make a recursive call in elab', it is

193 -- and forces/delays. If you make a recursive call in elab', it is

187 -- normally correct to call elabE - the ones that don't are desugarings

194 -- normally correct to call elabE - the ones that don't are desugarings

188 -- typically

195 -- typically

189− elabE :: (Bool, Bool, Bool, Bool) -> Maybe FC -> PTerm -> ElabD ()

196+ elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

190 elabE ina fc' t =

197 elabE ina fc' t =

191 --do g <- goal

198 --do g <- goal

192 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

199 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

@@ -247,7 +254,7 @@ elab ist info emode opts fn tm

247

254

248 -- "guarded" means immediately under a constructor, to help find patvars

255 -- "guarded" means immediately under a constructor, to help find patvars

249

256

250− elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)

257+ elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

251 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

258 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

252 -> PTerm -- ^ The term to elaborate

259 -> PTerm -- ^ The term to elaborate

253 -> ElabD ()

260 -> ElabD ()

@@ -257,7 +264,11 @@ elab ist info emode opts fn tm

257-- elab' (_,_,inty) (PConstant c)

264-- elab' (_,_,inty) (PConstant c)

258-- | constType c && pattern && not reflection && not inty

265-- | constType c && pattern && not reflection && not inty

259-- = lift $ tfail (Msg "Typecase is not allowed")

266-- = lift $ tfail (Msg "Typecase is not allowed")

260− elab' ina fc (PConstant c) = do apply (RConstant c) []; solve

267+ elab' ina fc tm@(PConstant c)

268+ | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

269+ && isTypeConst c

270+ = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

271+ | otherwise = do apply (RConstant c) []; solve

261 elab' ina fc (PQuote r) = do fill r; solve

272 elab' ina fc (PQuote r) = do fill r; solve

262 elab' ina _ (PTrue fc _) =

273 elab' ina _ (PTrue fc _) =

263 do hnf_compute

274 do hnf_compute

@@ -296,7 +307,7 @@ elab ist info emode opts fn tm

296 [pimp (sUN "A") lt True,

307 [pimp (sUN "A") lt True,

297 pimp (sUN "B") rt False,

308 pimp (sUN "B") rt False,

298 pexp l, pexp r])

309 pexp l, pexp r])

299− elab' ina@(_, a, inty, qq) _ (PPair fc _ l r)

310+ elab' ina _ (PPair fc _ l r)

300 = do hnf_compute

311 = do hnf_compute

301 g <- goal

312 g <- goal

302 case g of

313 case g of

@@ -354,9 +365,12 @@ elab ist info emode opts fn tm

354-- elab' (_, _, inty) (PRef fc f)

365-- elab' (_, _, inty) (PRef fc f)

355-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

366-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

356-- = lift $ tfail (Msg "Typecase is not allowed")

367-- = lift $ tfail (Msg "Typecase is not allowed")

357− elab' (ina, guarded, inty, qq) _ (PRef fc n)

368+ elab' ec _ (PRef fc n)

358− | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq

369+ | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

370+ = do let ina = e_inarg ec

371+ guarded = e_guarded ec

372+ inty = e_intype ec

359− = do ctxt <- get_context

373+ ctxt <- get_context

360 let defined = case lookupTy n ctxt of

374 let defined = case lookupTy n ctxt of

361 [] -> False

375 [] -> False

362 _ -> True

376 _ -> True

@@ -374,8 +388,12 @@ elab ist info emode opts fn tm

374 bindable (UN xs) = True

388 bindable (UN xs) = True

375 bindable n = implicitable n

389 bindable n = implicitable n

376 elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])

390 elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])

391+ elab' ina _ tm@(PRef fc n)

392+ | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

393+ && isTConName n (tt_ctxt ist)

394+ = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

377− elab' ina _ (PRef fc n) = erun fc $ do apply (Var n) []; solve

395+ | otherwise = erun fc $ do apply (Var n) []; solve

378− elab' ina@(_, a, inty, qq) fc (PLam n Placeholder sc)

396+ elab' ina fc (PLam n Placeholder sc)

379 = do -- if n is a type constructor name, this makes no sense...

397 = do -- if n is a type constructor name, this makes no sense...

380 ctxt <- get_context

398 ctxt <- get_context

381 when (isTConName n ctxt) $

399 when (isTConName n ctxt) $

@@ -383,8 +401,8 @@ elab ist info emode opts fn tm

383 checkPiGoal n

401 checkPiGoal n

384 attack; intro (Just n);

402 attack; intro (Just n);

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

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

386− elabE (True, a, inty, qq) fc sc; solve

404+ elabE (ina { e_inarg = True } ) fc sc; solve

387− elab' ina@(_, a, inty, qq) fc (PLam n ty sc)

405+ elab' ec fc (PLam n ty sc)

388 = do tyn <- getNameFrom (sMN 0 "lamty")

406 = do tyn <- getNameFrom (sMN 0 "lamty")

389 -- if n is a type constructor name, this makes no sense...

407 -- if n is a type constructor name, this makes no sense...

390 ctxt <- get_context

408 ctxt <- get_context

@@ -398,12 +416,15 @@ elab ist info emode opts fn tm

398 hs <- get_holes

416 hs <- get_holes

399 introTy (Var tyn) (Just n)

417 introTy (Var tyn) (Just n)

400 focus tyn

418 focus tyn

419+

401− elabE (True, a, True, qq) fc ty

420+ elabE (ec { e_inarg = True, e_intype = True }) fc ty

402− elabE (True, a, inty, qq) fc sc

421+ elabE (ec { e_inarg = True }) fc sc

403 solve

422 solve

404− elab' ina@(_, a, _, qq) fc (PPi _ n Placeholder sc)

423+ elab' ina fc (PPi _ n Placeholder sc)

405− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) fc sc; solve

424+ = do attack; arg n (sMN 0 "ty")

425+ elabE (ina { e_inarg = True, e_intype = True }) fc sc

426+ solve

406− elab' ina@(_, a, _, qq) fc (PPi _ n ty sc)

427+ elab' ina fc (PPi _ n ty sc)

407 = do attack; tyn <- getNameFrom (sMN 0 "ty")

428 = do attack; tyn <- getNameFrom (sMN 0 "ty")

408 claim tyn RType

429 claim tyn RType

409 n' <- case n of

430 n' <- case n of

@@ -411,10 +432,11 @@ elab ist info emode opts fn tm

411 _ -> return n

432 _ -> return n

412 forall n' (Var tyn)

433 forall n' (Var tyn)

413 focus tyn

434 focus tyn

414− elabE (True, a, True, qq) fc ty

435+ let ec' = ina { e_inarg = True, e_intype = True }

436+ elabE ec' fc ty

415− elabE (True, a, True, qq) fc sc

437+ elabE ec' fc sc

416 solve

438 solve

417− elab' ina@(_, a, inty, qq) fc (PLet n ty val sc)

439+ elab' ina fc (PLet n ty val sc)

418 = do attack

440 = do attack

419 ivs <- get_instances

441 ivs <- get_instances

420 tyn <- getNameFrom (sMN 0 "letty")

442 tyn <- getNameFrom (sMN 0 "letty")

@@ -427,12 +449,14 @@ elab ist info emode opts fn tm

427 Placeholder -> return ()

449 Placeholder -> return ()

428 _ -> do focus tyn

450 _ -> do focus tyn

429 explicit tyn

451 explicit tyn

430− elabE (True, a, True, qq) fc ty

452+ elabE (ina { e_inarg = True, e_intype = True })

453+ fc ty

431 focus valn

454 focus valn

432− elabE (True, a, True, qq) fc val

455+ elabE (ina { e_inarg = True, e_intype = True })

456+ fc val

433 ivs' <- get_instances

457 ivs' <- get_instances

434 env <- get_env

458 env <- get_env

435− elabE (True, a, inty, qq) fc sc

459+ elabE (ina { e_inarg = True }) fc sc

436 when (not pattern) $

460 when (not pattern) $

437 mapM_ (\n -> do focus n

461 mapM_ (\n -> do focus n

438 g <- goal

462 g <- goal

@@ -448,7 +472,7 @@ elab ist info emode opts fn tm

448 expandLet n (case lookup n env of

472 expandLet n (case lookup n env of

449 Just (Let t v) -> v)

473 Just (Let t v) -> v)

450 solve

474 solve

451− elab' ina@(_, a, inty, qq) _ (PGoal fc r n sc) = do

475+ elab' ina _ (PGoal fc r n sc) = do

452 rty <- goal

476 rty <- goal

453 attack

477 attack

454 tyn <- getNameFrom (sMN 0 "letty")

478 tyn <- getNameFrom (sMN 0 "letty")

@@ -457,10 +481,10 @@ elab ist info emode opts fn tm

457 claim valn (Var tyn)

481 claim valn (Var tyn)

458 letbind n (Var tyn) (Var valn)

482 letbind n (Var tyn) (Var valn)

459 focus valn

483 focus valn

460− elabE (True, a, True, qq) (Just fc) (PApp fc r [pexp (delab ist rty)])

484+ elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])

461 env <- get_env

485 env <- get_env

462 computeLet n

486 computeLet n

463− elabE (True, a, inty, qq) (Just fc) sc

487+ elabE (ina { e_inarg = True }) (Just fc) sc

464 solve

488 solve

465-- elab' ina fc (PLet n Placeholder

489-- elab' ina fc (PLet n Placeholder

466-- (PApp fc r [pexp (delab ist rty)]) sc)

490-- (PApp fc r [pexp (delab ist rty)]) sc)

@@ -523,12 +547,16 @@ elab ist info emode opts fn tm

523-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

547-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

524-- = lift $ tfail (Msg "Typecase is not allowed")

548-- = lift $ tfail (Msg "Typecase is not allowed")

525 -- if f is local, just do a simple_app

549 -- if f is local, just do a simple_app

526− elab' (ina, g, inty, qq) _ tm@(PApp fc (PRef _ f) args)

550+ elab' ina _ tm@(PApp fc (PRef _ f) args)

527 = do env <- get_env

551 = do env <- get_env

552+ ty <- goal

553+ when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

554+ && isTConName f (tt_ctxt ist)) $

555+ lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

528 if (f `elem` map fst env && length args == 1)

556 if (f `elem` map fst env && length args == 1)

529 then -- simple app, as below

557 then -- simple app, as below

530− do simple_app (elabE (ina, g, inty, qq) (Just fc) (PRef fc f))

558+ do simple_app (elabE ina (Just fc) (PRef fc f))

531− (elabE (True, g, inty, qq) (Just fc) (getTm (head args)))

559+ (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

532 (show tm)

560 (show tm)

533 solve

561 solve

534 else

562 else

@@ -557,7 +585,7 @@ elab ist info emode opts fn tm

557 let (ns', eargs) = unzip $

585 let (ns', eargs) = unzip $

558 sortBy cmpArg (zip ns args)

586 sortBy cmpArg (zip ns args)

559 ulog <- getUnifyLog

587 ulog <- getUnifyLog

560− elabArgs ist (ina || not isinf, guarded, inty, qq)

588+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

561 [] fc False f ns'

589 [] fc False f ns'

562 (f == sUN "Force")

590 (f == sUN "Force")

563 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

591 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

@@ -565,7 +593,8 @@ elab ist info emode opts fn tm

565 ivs' <- get_instances

593 ivs' <- get_instances

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

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

567 -- i.e. no holes in them

595 -- i.e. no holes in them

568− when (not pattern || (ina && not tcgen && not guarded)) $

596+ when (not pattern || (e_inarg ina && not tcgen &&

597+ not (e_guarded ina))) $

569 mapM_ (\n -> do focus n

598 mapM_ (\n -> do focus n

570 g <- goal

599 g <- goal

571 env <- get_env

600 env <- get_env

@@ -646,13 +675,14 @@ elab ist info emode opts fn tm

646 setInjective (PApp _ (PRef _ n) _) = setinj n

675 setInjective (PApp _ (PRef _ n) _) = setinj n

647 setInjective _ = return ()

676 setInjective _ = return ()

648

677

649− elab' ina@(_, a, inty, qq) _ tm@(PApp fc f [arg])

678+ elab' ina _ tm@(PApp fc f [arg])

650 = erun fc $

679 = erun fc $

651− do simple_app (elabE ina (Just fc) f) (elabE (True, a, inty, qq) (Just fc) (getTm arg))

680+ do simple_app (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

652 (show tm)

681 (show tm)

653 solve

682 solve

654− elab' ina fc Placeholder = do (h : hs) <- get_holes

683+ elab' ina fc Placeholder

684+ = do (h : hs) <- get_holes

655− movelast h

685+ movelast h

656 elab' ina fc (PMetavar n) =

686 elab' ina fc (PMetavar n) =

657 do ptm <- get_term

687 do ptm <- get_term

658 -- When building the metavar application, leave out the unique

688 -- When building the metavar application, leave out the unique

@@ -705,7 +735,7 @@ elab ist info emode opts fn tm

705 elab' ina (Just fc) sc

735 elab' ina (Just fc) sc

706 elab' ina (Just fc) (PRef fc letn)

736 elab' ina (Just fc) (PRef fc letn)

707 solve

737 solve

708− elab' ina@(_, a, inty, qq) _ c@(PCase fc scr opts)

738+ elab' ina _ c@(PCase fc scr opts)

709 = do attack

739 = do attack

710 tyn <- getNameFrom (sMN 0 "scty")

740 tyn <- getNameFrom (sMN 0 "scty")

711 claim tyn RType

741 claim tyn RType

@@ -714,7 +744,7 @@ elab ist info emode opts fn tm

714 claim valn (Var tyn)

744 claim valn (Var tyn)

715 letbind scvn (Var tyn) (Var valn)

745 letbind scvn (Var tyn) (Var valn)

716 focus valn

746 focus valn

717− elabE (True, a, inty, qq) (Just fc) scr

747+ elabE (ina { e_inarg = True }) (Just fc) scr

718 -- Solve any remaining implicits - we need to solve as many

748 -- Solve any remaining implicits - we need to solve as many

719 -- as possible before making the 'case' type

749 -- as possible before making the 'case' type

720 unifyProblems

750 unifyProblems

@@ -779,7 +809,7 @@ elab ist info emode opts fn tm

779 elab' ina fc (PUnifyLog t) = do unifyLog True

809 elab' ina fc (PUnifyLog t) = do unifyLog True

780 elab' ina fc t

810 elab' ina fc t

781 unifyLog False

811 unifyLog False

782− elab' (ina, g, inty, qq) fc (PQuasiquote t goal) -- TODO: goal type

812+ elab' ina fc (PQuasiquote t goal) -- TODO: goal type

783 = do -- First extract the unquoted subterms, replacing them with fresh

813 = do -- First extract the unquoted subterms, replacing them with fresh

784 -- names in the quasiquoted term. Claim their reflections to be

814 -- names in the quasiquoted term. Claim their reflections to be

785 -- of type TT.

815 -- of type TT.

@@ -824,11 +854,11 @@ elab ist info emode opts fn tm

824 case goal of

854 case goal of

825 Nothing -> return ()

855 Nothing -> return ()

826 Just gTy -> do focus qTy

856 Just gTy -> do focus qTy

827− elabE (ina, g, inty, True) fc gTy

857+ elabE (ina { e_qq = True }) fc gTy

828

858

829 -- Elaborate the quasiquoted term into the hole

859 -- Elaborate the quasiquoted term into the hole

830 focus qTm

860 focus qTm

831− elabE (ina, g, inty, True) fc t

861+ elabE (ina { e_qq = True }) fc t

832 end_unify

862 end_unify

833

863

834 -- We now have an elaborated term. Reflect it and solve the

864 -- We now have an elaborated term. Reflect it and solve the

@@ -854,7 +884,7 @@ elab ist info emode opts fn tm

854

884

855 elabUnquote (n, tm)

885 elabUnquote (n, tm)

856 = do focus n

886 = do focus n

857− elabE (ina, g, inty, False) fc tm

887+ elabE (ina { e_qq = False }) fc tm

858

888

859

889

860 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

890 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

@@ -966,7 +996,7 @@ elab ist info emode opts fn tm

966

996

967 -- | Elaborate the arguments to a function

997 -- | Elaborate the arguments to a function

968 elabArgs :: IState -- ^ The current Idris state

998 elabArgs :: IState -- ^ The current Idris state

969− -> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)

999+ -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)

970 -> [Bool]

1000 -> [Bool]

971 -> FC -- ^ Source location

1001 -> FC -- ^ Source location

972 -> Bool

1002 -> Bool

@@ -976,10 +1006,15 @@ elab ist info emode opts fn tm

976 -> [PTerm] -- ^ (Laziness, argument)

1006 -> [PTerm] -- ^ (Laziness, argument)

977 -> ElabD ()

1007 -> ElabD ()

978 elabArgs ist ina failed fc retry f [] force _ = return ()

1008 elabArgs ist ina failed fc retry f [] force _ = return ()

979− elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

980− = elabArgs ist ina failed fc r f ns force args

981 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

1009 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

1010+ = do hs <- get_holes

1011+ if holeName `elem` hs then

1012+ do focus holeName

1013+ case t of

1014+ Placeholder -> do movelast holeName

1015+ elabArgs ist ina failed fc r f ns force args

982− = elabArg argName holeName t

1016+ _ -> elabArg argName holeName t

1017+ else elabArgs ist ina failed fc r f ns force args

983 where elabArg argName holeName t =

1018 where elabArg argName holeName t =

984 do -- solveAutos ist fn False

1019 do -- solveAutos ist fn False

985 now_elaborating fc f argName

1020 now_elaborating fc f argName

@@ -991,13 +1026,11 @@ elab ist info emode opts fn tm

991 let elab = if force then elab' else elabE

1026 let elab = if force then elab' else elabE

992 failed' <- -- trace (show (n, t, hs, tm)) $

1027 failed' <- -- trace (show (n, t, hs, tm)) $

993 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

1028 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

994− case holeName `elem` hs of

995− True -> do focus holeName;

1029+ do focus holeName;

996− g <- goal

1030+ g <- goal

997− ulog <- getUnifyLog

1031+ ulog <- getUnifyLog

998− traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

1032+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

999− elab ina (Just fc) t; return failed

1033+ elab ina (Just fc) t; return failed

1000− False -> return failed

1001 done_elaborating_arg f argName

1034 done_elaborating_arg f argName

1002 elabArgs ist ina failed fc r f ns force args

1035 elabArgs ist ina failed fc r f ns force args

1003 wrapErr f argName action =

1036 wrapErr f argName action =

test/proof001/test029.idr+4−2

@@ -3,12 +3,14 @@ module simple

3plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

5-- Base case

6−(Z + m = m + Z) <== plus_comm =

6+-- (Z + m = m + Z) <== plus_comm = -- broken by typecase check

7+plus_comm Z m =

7 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>

8 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>

8 (Z + m = m) in Refl

9 (Z + m = m) in Refl

10-- Step case

11-- Step case

11−(S k + m = m + S k) <== plus_comm =

12+-- (S k + m = m + S k) <== plus_comm =

13+plus_comm (S k) m =

12 rewrite ((k + m = m + k) <== plus_comm) in

14 rewrite ((k + m = m + k) <== plus_comm) in

13 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in

15 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in

14 Refl

16 Refl