0d8a153 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -276,6 +276,9 @@ Extra-source-files:

276 test/reg054/run

277 test/reg054/*.idr

278 test/reg054/expected

279+ test/reg055/run

280+ test/reg055/*.idr

281+ test/reg055/expected

279

282

280 test/basic001/run

283 test/basic001/run

281 test/basic001/*.idr

284 test/basic001/*.idr

libs/base/Language/Reflection/Errors.idr+1

@@ -20,6 +20,7 @@ data Err = Msg String

20 | CantIntroduce TT

21 | NoSuchVariable TTName

22 | WithFnType TT

23+ | CantMatch TT

23 | NoTypeDecl TTName

24 | NoTypeDecl TTName

24 | NotInjective TT TT TT

25 | NotInjective TT TT TT

25 | CantResolve TT

26 | CantResolve TT

libs/base/Language/Reflection/Utils.idr+1

@@ -262,6 +262,7 @@ instance Show Err where

262 show (CantIntroduce tm) = "CantIntroduce " ++ show tm

263 show (NoSuchVariable n) = "NoSuchVariable " ++ show n

264 show (WithFnType tm) = "WithFnType " ++ show tm

265+ show (CantMatch tm) = "CantMatch " ++ show tm

265 show (NoTypeDecl n) = "NoTypeDecl " ++ show n

266 show (NoTypeDecl n) = "NoTypeDecl " ++ show n

266 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

267 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

267 show (CantResolve tm) = "CantResolve " ++ show tm

268 show (CantResolve tm) = "CantResolve " ++ show tm

src/Idris/AbsSyntax.hs+23−10

@@ -1437,7 +1437,7 @@ addImpl' inpat env infns ist ptm

1437 | f `elem` infns = PInferRef fc f

1438 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1439 ai qq env ds (PHidden (PRef fc f))

1440− | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1440+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])

1441 ai qq env ds (PEq fc lt rt l r)

1442 = let lt' = ai qq env ds lt

1443 rt' = ai qq env ds rt

@@ -1632,8 +1632,6 @@ aiFn inpat expat qq ist fc f ds as

1632 find n (g : gs) acc = find n gs (g : acc)

1633

1634-- replace non-linear occurrences with _

1635−-- ASSUMPTION: This is called before adding 'alternatives' because otherwise

1636−-- it is hard to get right!

1637

1635

1638stripLinear :: IState -> PTerm -> PTerm

1636stripLinear :: IState -> PTerm -> PTerm

1639stripLinear i tm = evalState (sl tm) [] where

1637stripLinear i tm = evalState (sl tm) [] where

@@ -1643,17 +1641,25 @@ stripLinear i tm = evalState (sl tm) [] where

1643 = return $ PRef fc f

1641 = return $ PRef fc f

1644 | otherwise = do ns <- get

1642 | otherwise = do ns <- get

1645 if (f `elem` ns)

1643 if (f `elem` ns)

1646− then return Placeholder

1644+ then return $ PHidden (PRef fc f) -- Placeholder

1647 else do put (f : ns)

1645 else do put (f : ns)

1648 return (PRef fc f)

1646 return (PRef fc f)

1649 sl (PPatvar fc f)

1647 sl (PPatvar fc f)

1650 = do ns <- get

1648 = do ns <- get

1651 if (f `elem` ns)

1649 if (f `elem` ns)

1652− then return Placeholder

1650+ then return $ PHidden (PPatvar fc f) -- Placeholder

1653 else do put (f : ns)

1651 else do put (f : ns)

1654 return (PPatvar fc f)

1652 return (PPatvar fc f)

1653+ -- Assumption is that variables are all the same in each alternative

1655− sl t@(PAlternative _ (a : as)) = do sl a

1654+ sl t@(PAlternative b as) = do ns <- get

1655+ as' <- slAlts ns as

1656+ return (PAlternative b as')

1657+ where slAlts ns (a : as) = do put ns

1658+ a' <- sl a

1659+ as' <- slAlts ns as

1656− return t

1660+ return (a' : as')

1661+ slAlts ns [] = return []

1662+ sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1657 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1663 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var

1658 args' <- mapM slA args

1664 args' <- mapM slA args

1659 return $ PApp fc fn args'

1665 return $ PApp fc fn args'

@@ -1679,8 +1685,11 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1679 su (PRef fc f)

1685 su (PRef fc f)

1680 | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1686 | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)

1681 = Placeholder

1687 = Placeholder

1682− su (PApp fc fn args)

1688+ su (PApp fc f@(PRef _ fn) args)

1689+ | isDConName fn ctxt

1683− = PApp fc fn (fmap (fmap su) args)

1690+ = PApp fc f (fmap (fmap su) args)

1691+ su (PApp fc f args)

1692+ = PHidden (PApp fc f args)

1684 su (PAlternative b alts)

1693 su (PAlternative b alts)

1685 = let alts' = filter (/= Placeholder) (map su alts) in

1694 = let alts' = filter (/= Placeholder) (map su alts) in

1686 if null alts' then Placeholder

1695 if null alts' then Placeholder

@@ -1688,6 +1697,9 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1688 su (PPair fc p l r) = PPair fc p (su l) (su r)

1697 su (PPair fc p l r) = PPair fc p (su l) (su r)

1689 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1698 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1690 su t = t

1699 su t = t

1700+

1701+ ctxt = tt_ctxt i

1702+

1691stripUnmatchable i tm = tm

1703stripUnmatchable i tm = tm

1692

1704

1693mkPApp fc a f [] = f

1705mkPApp fc a f [] = f

@@ -1835,7 +1847,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1835 mty <- match' ty ty'

1847 mty <- match' ty ty'

1836 ms <- match' s s'

1848 ms <- match' s s'

1837 return (mt ++ mty ++ ms)

1849 return (mt ++ mty ++ ms)

1850+ match (PHidden x) y = match' x y

1838− match (PHidden x) (PHidden y) = match' x y

1851+ match x (PHidden y) = match' x y

1839 match (PUnifyLog x) y = match' x y

1852 match (PUnifyLog x) y = match' x y

1840 match x (PUnifyLog y) = match' x y

1853 match x (PUnifyLog y) = match' x y

1841 match (PNoImplicits x) y = match' x y

1854 match (PNoImplicits x) y = match' x y

src/Idris/AbsSyntaxTree.hs+8−1

@@ -585,7 +585,14 @@ deriving instance NFData PDecl'

585!-}

586

587-- For elaborator state

588+data EState = EState {

589+ case_decls :: [PDecl],

590+ delayed_elab :: [Elab' EState ()]

591+ }

592+

593+initEState = EState [] []

594+

588−type ElabD a = Elab' [PDecl] a

595+type ElabD a = Elab' EState a

589

596

590-- | One clause of a top-level definition. Term arguments to constructors are:

597-- | One clause of a top-level definition. Term arguments to constructors are:

591--

598--

src/Idris/Core/Binary.hs+3

@@ -120,6 +120,8 @@ instance Binary a => Binary (Err' a) where

120 put e

121 put (WithFnType t) = do putWord8 34

122 put t

123+ put (CantMatch t) = do putWord8 35

124+ put t

123

125

124 get = do i <- getWord8

126 get = do i <- getWord8

125 case i of

127 case i of

@@ -174,6 +176,7 @@ instance Binary a => Binary (Err' a) where

174 33 -> do x <- get ; y <- get

176 33 -> do x <- get ; y <- get

175 return $ ReflectionFailed x y

177 return $ ReflectionFailed x y

176 34 -> fmap WithFnType get

178 34 -> fmap WithFnType get

179+ 35 -> fmap CantMatch get

177 _ -> error "Corrupted binary data for Err'"

180 _ -> error "Corrupted binary data for Err'"

178----- Generated by 'derive'

181----- Generated by 'derive'

179

182

src/Idris/Core/CaseTree.hs−7

@@ -263,13 +263,6 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

263 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

264 if proj then return (stripLambdas t)

265 else return t

266−-- FIXME: This check is not quite right in some cases, and is breaking

267−-- perfectly valid code!

268−--

269−-- Issue #1717 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1717

270−-- if checkSameTypes (lstT st) tree

271−-- then return t

272−-- else Error (At fc (Msg "Typecase is not allowed"))

273 Error err -> Error (At fc err)

266 Error err -> Error (At fc err)

274 where args = map (\i -> sMN i "e") [0..]

267 where args = map (\i -> sMN i "e") [0..]

275 defaultCase True = STerm Erased

268 defaultCase True = STerm Erased

src/Idris/Core/Elaborate.hs+28

@@ -412,6 +412,34 @@ focus n = processTactic' (Focus n)

412movelast :: Name -> Elab' aux ()

413movelast n = processTactic' (MoveLast n)

414

415+dotterm :: Elab' aux ()

416+dotterm = do ES (p, a) s m <- get

417+ tm <- get_term

418+ case holes p of

419+ [] -> return ()

420+ (h : hs) ->

421+ do let outer = findOuter h [] tm

422+ let p' = p { dotted = (h, outer) : dotted p }

423+-- trace ("DOTTING " ++ show (h, outer) ++ "\n" ++

424+-- show tm) $

425+ put $ ES (p', a) s m

426+ where

427+ findOuter h env (P _ n _) | h == n = env

428+ findOuter h env (Bind n b sc)

429+ = union (foB b)

430+ (findOuter h env (instantiate (P Bound n (binderTy b)) sc))

431+ where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)

432+ foB (Let t v) = union (findOuter h env t) (findOuter h env v)

433+ foB b = findOuter h env (binderTy b)

434+ findOuter h env (App f a)

435+ = union (findOuter h env f) (findOuter h env a)

436+ findOuter h env _ = []

437+

438+

439+get_dotterm :: Elab' aux [(Name, [Name])]

440+get_dotterm = do ES (p, a) s m <- get

441+ return (dotted p)

442+

415-- | Set the zipper in the proof state to point at the current sub term

443-- | Set the zipper in the proof state to point at the current sub term

416-- (This currently happens automatically, so this will have no effect...)

444-- (This currently happens automatically, so this will have no effect...)

417zipHere :: Elab' aux ()

445zipHere :: Elab' aux ()

src/Idris/Core/ProofState.hs+19−8

@@ -31,6 +31,8 @@ data ProofState = PS { thname :: Name,

31 dontunify :: [Name], -- explicitly given by programmer, leave it

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

33 notunified :: [(Name, Term)],

34+ dotted :: [(Name, [Name])], -- dot pattern holes + environment

35+ -- either hole or something in env must turn up in the 'notunified' list during elaboration

34 solved :: Maybe (Name, Term),

36 solved :: Maybe (Name, Term),

35 problems :: Fails,

37 problems :: Fails,

36 injective :: [Name],

38 injective :: [Name],

@@ -214,7 +216,7 @@ unify' ctxt env topx topy =

214 lift $ unify ctxt env topx topy inj (holes ps)

216 lift $ unify ctxt env topx topy inj (holes ps)

215 (map fst (notunified ps)) while

217 (map fst (notunified ps)) while

216 let notu = filter (\ (n, t) -> case t of

218 let notu = filter (\ (n, t) -> case t of

217− P _ _ _ -> False

219+-- P _ _ _ -> False

218 _ -> n `elem` dont) u

220 _ -> n `elem` dont) u

219 traceWhen (unifylog ps)

221 traceWhen (unifylog ps)

220 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

222 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

@@ -287,7 +289,7 @@ newProof :: Name -> Context -> Type -> ProofState

287newProof n ctxt ty = let h = holeName 0

289newProof n ctxt ty = let h = holeName 0

288 ty' = vToP ty in

290 ty' = vToP ty in

289 PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

291 PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

290− (P Bound h ty'))) ty [] (h, []) []

292+ (P Bound h ty'))) ty [] (h, []) [] []

291 Nothing [] []

293 Nothing [] []

292 [] [] []

294 [] [] []

293 Nothing ctxt "" False False [] []

295 Nothing ctxt "" False False [] []

@@ -499,19 +501,27 @@ solve :: RunTactic

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

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

500 = do ps <- get

502 = do ps <- get

501 let (uh, uns) = unified ps

503 let (uh, uns) = unified ps

504+ dropdots <-

502− case lookup x (notunified ps) of

505+ case lookup x (notunified ps) of

503− Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

506+ Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

504− match_unify' ctxt env tm val

507+ do match_unify' ctxt env tm val

508+ return [x]

505− _ -> return []

509+ _ -> return []

506 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

510 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

507 holes ps \\ [x],

511 holes ps \\ [x],

508 solved = Just (x, val),

512 solved = Just (x, val),

509 notunified = updateNotunified [(x,val)]

513 notunified = updateNotunified [(x,val)]

510 (notunified ps),

514 (notunified ps),

511 recents = x : recents ps,

515 recents = x : recents ps,

512− instances = instances ps \\ [x] })

516+ instances = instances ps \\ [x],

517+ dotted = dropUnified dropdots (dotted ps) })

513 let tm' = subst x val sc in

518 let tm' = subst x val sc in

514 return tm'

519 return tm'

520+ where dropUnified ddots [] = []

521+ dropUnified ddots ((x, es) : ds)

522+ | x `elem` ddots || any (\e -> e `elem` ddots) es

523+ = dropUnified ddots ds

524+ | otherwise = (x, es) : dropUnified ddots ds

515solve _ _ h@(Bind x t sc)

525solve _ _ h@(Bind x t sc)

516 = do ps <- get

526 = do ps <- get

517 case findType x sc of

527 case findType x sc of

@@ -574,7 +584,8 @@ patvar n ctxt env (Bind x (Hole t) sc) =

574 solved = Just (x, P Bound n t),

584 solved = Just (x, P Bound n t),

575 notunified = updateNotunified [(x,P Bound n t)]

585 notunified = updateNotunified [(x,P Bound n t)]

576 (notunified ps),

586 (notunified ps),

577− injective = addInj n x (injective ps) })

587+ injective = addInj n x (injective ps)

588+ })

578 return $ Bind n (PVar t) (subst x (P Bound n t) sc)

589 return $ Bind n (PVar t) (subst x (P Bound n t) sc)

579 where addInj n x ps | x `elem` ps = n : ps

590 where addInj n x ps | x `elem` ps = n : ps

580 | otherwise = ps

591 | otherwise = ps

src/Idris/Core/TT.hs+1

@@ -147,6 +147,7 @@ data Err' t

147 | UniqueKindError Universe Name

148 | ProgramLineComment

149 | Inaccessible Name

150+ | CantMatch t

150 | NonCollapsiblePostulate Name

151 | NonCollapsiblePostulate Name

151 | AlreadyDefined Name

152 | AlreadyDefined Name

152 | ProofSearchFail (Err' t)

153 | ProofSearchFail (Err' t)

src/Idris/Delaborate.hs+4

@@ -262,6 +262,8 @@ pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

262pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

263pprintErr' i (WithFnType ty) =

264 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delab i ty))

265+pprintErr' i (CantMatch t) =

266+ text "Can't match on " <+> annTm t (pprintTerm i (delab i t))

265pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

267pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

266pprintErr' i UniverseError = text "Universe inconsistency"

268pprintErr' i UniverseError = text "Universe inconsistency"

267pprintErr' i (UniqueError NullType n)

269pprintErr' i (UniqueError NullType n)

@@ -513,3 +515,5 @@ showbasic n@(UN _) = show n

513showbasic (MN _ s) = str s

515showbasic (MN _ s) = str s

514showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

516showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

515showbasic (SN s) = show s

517showbasic (SN s) = show s

518+showbasic n = show n

519+

src/Idris/Elab/Clause.hs+12−10

@@ -445,7 +445,7 @@ checkPossible info fc tcgen fname lhs_in

445 i <- getIState

446 let lhs = addImplPat i lhs_in

447 -- if the LHS type checks, it is possible

448− case elaborate ctxt (sMN 0 "patLHS") infP []

448+ case elaborate ctxt (sMN 0 "patLHS") infP initEState

449 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

450 OK ((lhs', _, _), _) ->

451 do let lhs_tm = orderPats (getInferTerm lhs')

@@ -561,14 +561,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

561 [t] -> t

562 _ -> []

563 let params = getParamsInType i [] fn_is fn_ty

564− let lhs = mkLHSapp $ stripUnmatchable i $

564+ let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

565− propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))

565+ propagateParams i params fn_ty (addImplPat i lhs_in)

566+-- let lhs = mkLHSapp $

567+-- propagateParams i params fn_ty (addImplPat i lhs_in)

566 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

568 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

567 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

569 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

568 "\n" ++ show (fn_ty, fn_is))

570 "\n" ++ show (fn_ty, fn_is))

569

571

570 (((lhs', dlhs, []), probs, inj), _) <-

572 (((lhs', dlhs, []), probs, inj), _) <-

571− tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

573+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

572 (do res <- errAt "left hand side of " fname

574 (do res <- errAt "left hand side of " fname

573 (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

575 (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

574 probs <- get_probs

576 probs <- get_probs

@@ -642,7 +644,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

642 ctxt <- getContext -- new context with where block added

644 ctxt <- getContext -- new context with where block added

643 logLvl 5 "STARTING CHECK"

645 logLvl 5 "STARTING CHECK"

644 ((rhs', defer, is, probs), _) <-

646 ((rhs', defer, is, probs), _) <-

645− tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

647+ tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty initEState

646 (do pbinds ist lhs_tm

648 (do pbinds ist lhs_tm

647 mapM_ setinj (nub (params ++ inj))

649 mapM_ setinj (nub (params ++ inj))

648 setNextName

650 setNextName

@@ -652,7 +654,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

652 (erun fc $ psolve lhs_tm)

654 (erun fc $ psolve lhs_tm)

653 hs <- get_holes

655 hs <- get_holes

654 aux <- getAux

656 aux <- getAux

655− mapM_ (elabCaseHole aux) hs

657+ mapM_ (elabCaseHole (case_decls aux)) hs

656 tt <- get_term

658 tt <- get_term

657 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

659 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

658 probs <- get_probs

660 probs <- get_probs

@@ -793,10 +795,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

793 [t] -> t

795 [t] -> t

794 _ -> []

796 _ -> []

795 let params = getParamsInType i [] fn_is fn_ty

797 let params = getParamsInType i [] fn_is fn_ty

796− let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))

798+ let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

797 logLvl 2 ("LHS: " ++ show lhs)

799 logLvl 2 ("LHS: " ++ show lhs)

798 ((lhs', dlhs, []), _) <-

800 ((lhs', dlhs, []), _) <-

799− tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

801+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

800 (errAt "left hand side of with in " fname

802 (errAt "left hand side of with in " fname

801 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

803 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

802 let lhs_tm = orderPats (getInferTerm lhs')

804 let lhs_tm = orderPats (getInferTerm lhs')

@@ -812,7 +814,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

812 -- Elaborate wval in this context

814 -- Elaborate wval in this context

813 ((wval', defer, is), _) <-

815 ((wval', defer, is), _) <-

814 tclift $ elaborate ctxt (sMN 0 "withRHS")

816 tclift $ elaborate ctxt (sMN 0 "withRHS")

815− (bindTyArgs PVTy bargs infP) []

817+ (bindTyArgs PVTy bargs infP) initEState

816 (do pbinds i lhs_tm

818 (do pbinds i lhs_tm

817 setNextName

819 setNextName

818 -- TODO: may want where here - see winfo abpve

820 -- TODO: may want where here - see winfo abpve

@@ -892,7 +894,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

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

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

893 i <- getIState

895 i <- getIState

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

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

895− tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty []

897+ tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty initEState

896 (do pbinds i lhs_tm

898 (do pbinds i lhs_tm

897 setNextName

899 setNextName

898 (_, d, is) <- erun fc (build i info ERHS opts fname rhs)

900 (_, d, is) <- erun fc (build i info ERHS opts fname rhs)

src/Idris/Elab/Instance.hs+1−1

@@ -168,7 +168,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

168 let ty = addImpl i ty'

169 ctxt <- getContext

170 ((tyT, _, _), _) <-

171− tclift $ elaborate ctxt iname (TType (UVal 0)) []

171+ tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

172 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

173 ctxt <- getContext

174 (cty, _) <- recheckC fc [] tyT

src/Idris/Elab/Transform.hs+2−2

@@ -54,7 +54,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56 ((lhs', dlhs, []), _) <-

57− tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

57+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState

58 (erun fc (buildTC i info ELHS [] (sUN "transform")

59 (infTerm lhs)))

60 let lhs_tm = orderPats (getInferTerm lhs')

@@ -67,7 +67,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

67

68 let rhs = addImplBound i (map fst newargs) rhs_in

69 ((rhs', defer), _) <-

70− tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

70+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

71 (do pbinds i lhs_tm

72 setNextName

73 erun fc (build i info ERHS [] (sUN "transform") rhs)

src/Idris/Elab/Type.hs+1−1

@@ -66,7 +66,7 @@ buildType info syn fc opts n ty' = do

66 logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

67

68 ((tyT', defer, is), log) <-

69− tclift $ elaborate ctxt n (TType (UVal 0)) []

69+ tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70 (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

71

72 let tyT = patToImp tyT'

src/Idris/Elab/Value.hs+1−1

@@ -64,7 +64,7 @@ elabValBind info aspat norm tm_in

64 -- * elaboration as a function a -> b

65

66 ((tm', defer, is), _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP []

67+ tclift (elaborate ctxt (sMN 0 "val") infP initEState

68 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

69 let vtm = orderPats (getInferTerm tm')

70

src/Idris/ElabTerm.hs+40−8

@@ -94,7 +94,7 @@ build ist info emode opts fn tm

94 when tydecl (do update_term orderPats

95 mkPat)

96-- update_term liftPats)

97− is <- getAux

97+ EState is _ <- getAux

98 tt <- get_term

99 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

100 log <- getLog

@@ -130,7 +130,12 @@ buildTC ist info emode opts fn tm

130 [] -> return ()

131 ((_,_,_,_,e,_,_):es) -> if inf then return ()

132 else lift (Error e)

133+ dots <- get_dotterm

134+ -- 'dots' are the PHidden things which have not been solved by

135+ -- unification

136+ when (not (null dots)) $

137+ lift (Error (CantMatch (getInferTerm tm)))

133− is <- getAux

138+ EState is _ <- getAux

134 tt <- get_term

139 tt <- get_term

135 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

140 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

136 log <- getLog

141 log <- getLog

@@ -181,6 +186,8 @@ elab ist info emode opts fn tm

181 compute -- expand type synonyms, etc

186 compute -- expand type synonyms, etc

182 let fc = maybe "(unknown)"

187 let fc = maybe "(unknown)"

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

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

189+ est <- getAux

190+ sequence_ (delayed_elab est)

184 end_unify

191 end_unify

185 ptm <- get_term

192 ptm <- get_term

186 when pattern -- convert remaining holes to pattern vars

193 when pattern -- convert remaining holes to pattern vars

@@ -388,7 +395,7 @@ elab ist info emode opts fn tm

388 trySeq' deferr (x : xs)

395 trySeq' deferr (x : xs)

389 = try' (do elab' ina fc x

396 = try' (do elab' ina fc x

390 solveAutos ist fn False) (trySeq' deferr xs) True

397 solveAutos ist fn False) (trySeq' deferr xs) True

391− elab' ina _ (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats

398+ elab' ina _ (PPatvar fc n) | bindfree = do patvar n; update_term liftPats

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

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

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

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

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

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

@@ -587,9 +594,13 @@ elab ist info emode opts fn tm

587 | otherwise

594 | otherwise

588 = do env <- get_env

595 = do env <- get_env

589 ty <- goal

596 ty <- goal

597+ ctxt <- get_context

590 let unmatchableArgs = if pattern

598 let unmatchableArgs = if pattern

591 then getUnmatchable (tt_ctxt ist) f

599 then getUnmatchable (tt_ctxt ist) f

592 else []

600 else []

601+ -- Dot it if we're in a pattern and it isn't a constructor

602+-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm

603+

593 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

604 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

594 && isTConName f (tt_ctxt ist)) $

605 && isTConName f (tt_ctxt ist)) $

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

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

@@ -612,7 +623,6 @@ elab ist info emode opts fn tm

612 _ -> do mapM_ setInjective (map getTm args)

623 _ -> do mapM_ setInjective (map getTm args)

613 -- maybe more things are solvable now

624 -- maybe more things are solvable now

614 unifyProblems

625 unifyProblems

615− ctxt <- get_context

616 let guarded = isConName f ctxt

626 let guarded = isConName f ctxt

617-- trace ("args is " ++ show args) $ return ()

627-- trace ("args is " ++ show args) $ return ()

618 ns <- apply (Var f) (map isph args)

628 ns <- apply (Var f) (map isph args)

@@ -666,13 +676,15 @@ elab ist info emode opts fn tm

666 PLam _ _ _ -> 3

676 PLam _ _ _ -> 3

667 PRewrite _ _ _ _ -> 4

677 PRewrite _ _ _ _ -> 4

668 PResolveTC _ -> 0

678 PResolveTC _ -> 0

679+ PHidden _ -> 150

669 _ -> 1

680 _ -> 1

670

681

671 constraint (PConstraint _ _ _ _) = True

682 constraint (PConstraint _ _ _ _) = True

672 constraint _ = False

683 constraint _ = False

673

684

674 -- Score a point for every level where there is a non-constructor

685 -- Score a point for every level where there is a non-constructor

675− -- function (so higher score --> done later)

686+ -- function (so higher score --> done later), and lots of points

687+ -- if there is a PHidden since this should be unifiable.

676 -- Only relevant when on lhs

688 -- Only relevant when on lhs

677 conDepth d t | not pattern = 0

689 conDepth d t | not pattern = 0

678 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0

690 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0

@@ -681,6 +693,7 @@ elab ist info emode opts fn tm

681 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))

693 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))

682 conDepth d (PPatvar _ _) = 0

694 conDepth d (PPatvar _ _) = 0

683 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

695 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)

696+ conDepth d (PHidden _) = 150

684 conDepth d Placeholder = 0

697 conDepth d Placeholder = 0

685 conDepth d (PResolveTC _) = 0

698 conDepth d (PResolveTC _) = 0

686 conDepth d t = max (100 - d) 1

699 conDepth d t = max (100 - d) 1

@@ -810,7 +823,7 @@ elab ist info emode opts fn tm

810 (caseBlock fc cname'

823 (caseBlock fc cname'

811 (map (isScr scr) (reverse args')) opts)

824 (map (isScr scr) (reverse args')) opts)

812 -- elaborate case

825 -- elaborate case

813− updateAux (newdef : )

826+ updateAux (\e -> e { case_decls = newdef : case_decls e } )

814 -- if we haven't got the type yet, hopefully we'll get it later!

827 -- if we haven't got the type yet, hopefully we'll get it later!

815 movelast tyn

828 movelast tyn

816 solve

829 solve

@@ -930,8 +943,24 @@ elab ist info emode opts fn tm

930

943

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

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

932 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

945 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

946+ elab' ina fc (PHidden t)

947+ | reflection = elab' ina fc t

948+ | otherwise

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

950+ -- Dotting a hole means that either the hole or any outer

951+ -- hole (a hole outside any occurrence of it)

952+ -- must be solvable by unification as well as being filled

953+ -- in directly.

954+ -- Delay dotted things to the end, then when we elaborate them

955+ -- we can check the result against what was inferred

956+ movelast h

957+ delayElab $ do focus h

958+ dotterm

959+ elab' ina fc t

933 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

960 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

934

961

962+ delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

963+

935 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

964 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

936 isScr (PRef _ n) (n', b) = (n', (n == n', b))

965 isScr (PRef _ n) (n', b) = (n', (n == n', b))

937 isScr _ (n', b) = (n', (False, b))

966 isScr _ (n', b) = (n', (False, b))

@@ -1126,6 +1155,7 @@ pruneByType env t c as

1126 | otherwise = locallyBound ts

1155 | otherwise = locallyBound ts

1127 getName (PRef _ n) = Just n

1156 getName (PRef _ n) = Just n

1128 getName (PApp _ f _) = getName f

1157 getName (PApp _ f _) = getName f

1158+ getName (PHidden t) = getName t

1129 getName _ = Nothing

1159 getName _ = Nothing

1130

1160

1131pruneByType env (P _ n _) ctxt as

1161pruneByType env (P _ n _) ctxt as

@@ -1143,6 +1173,7 @@ pruneByType env (P _ n _) ctxt as

1143 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1173 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1144 headIs var f (PApp _ f' _) = headIs var f f'

1174 headIs var f (PApp _ f' _) = headIs var f f'

1145 headIs var f (PPi _ _ _ sc) = headIs var f sc

1175 headIs var f (PPi _ _ _ sc) = headIs var f sc

1176+ headIs var f (PHidden t) = headIs var f t

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

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

1147

1178

1148 typeHead var f f'

1179 typeHead var f f'

@@ -2195,6 +2226,7 @@ reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments

2195reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

2226reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]

2196reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

2227reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]

2197reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]

2228reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]

2229+reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]

2198reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2230reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]

2199reflectErr (NotInjective t1 t2 t3) =

2231reflectErr (NotInjective t1 t2 t3) =

2200 raw_apply (Var $ reflErrName "NotInjective")

2232 raw_apply (Var $ reflErrName "NotInjective")

@@ -2306,7 +2338,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "Te

2306 Right (TextPart msg)

2338 Right (TextPart msg)

2307reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2339reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2308 | n == reflm "NamePart" =

2340 | n == reflm "NamePart" =

2309− case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2341+ case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2310 Error e -> Left . InternalMsg $

2342 Error e -> Left . InternalMsg $

2311 "could not reify name term " ++

2343 "could not reify name term " ++

2312 show ttn ++

2344 show ttn ++

@@ -2314,7 +2346,7 @@ reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2314 OK (n', _)-> Right $ NamePart n'

2346 OK (n', _)-> Right $ NamePart n'

2315reifyReportPart (App (P (DCon _ _ _) n _) tm)

2347reifyReportPart (App (P (DCon _ _ _) n _) tm)

2316 | n == reflm "TermPart" =

2348 | n == reflm "TermPart" =

2317− case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2349+ case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

2318 Error e -> Left . InternalMsg $

2350 Error e -> Left . InternalMsg $

2319 "could not reify reflected term " ++

2351 "could not reify reflected term " ++

2320 show tm ++

2352 show tm ++

src/Idris/Prover.hs+8−8

@@ -53,10 +53,10 @@ showProof lit n ps

53 where bird = if lit then "> " else ""

54 break = "\n" ++ bird

55

56−proverSettings :: ElabState [PDecl] -> Settings Idris

56+proverSettings :: ElabState EState -> Settings Idris

57proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings

58

59−assumptionNames :: ElabState [PDecl] -> [String]

59+assumptionNames :: ElabState EState -> [String]

60assumptionNames e

61 = case envAtFocus (proof e) of

62 OK env -> names env

@@ -68,7 +68,7 @@ prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

68prove opt ctxt lit n ty

69 = do let ps = initElaborator n ctxt ty

70 ideslavePutSExp "start-proof-mode" n

71− (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing

71+ (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

72 iLOG $ "Adding " ++ show tm

73 i <- getIState

74 case idris_outputmode i of

@@ -99,7 +99,7 @@ prove opt ctxt lit n ty

99 runIO . hPutStrLn h $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n

100 _ -> return ()

101

102−elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

102+elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)

103elabStep st e = case runStateT eCheck st of

104 OK (a, st') -> return (a, st')

105 Error a -> ierror a

@@ -177,11 +177,11 @@ dumpState ist ps | (h : hs) <- holes ps = do

177 freeEnvNames :: Env -> [Name]

178 freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))

179

180−lifte :: ElabState [PDecl] -> ElabD a -> Idris a

180+lifte :: ElabState EState -> ElabD a -> Idris a

181lifte st e = do (v, _) <- elabStep st e

182 return v

183

184−receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)

184+receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)

185receiveInput h e =

186 do i <- getIState

187 let inh = if h == stdout then stdin else h

@@ -205,7 +205,7 @@ receiveInput h e =

205 Just (IdeSlave.DocsFor str) -> return (Just (":doc " ++ str))

206 _ -> return Nothing

207

208−ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])

208+ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

209ploop fn d prompt prf e h

210 = do i <- getIState

211 let autoSolve = opt_autoSolve (idris_options i)

@@ -327,7 +327,7 @@ ploop fn d prompt prf e h

327 putIState ist

328 return (False, e, False, prf, Right action))

329 (\err -> do putIState ist ; ierror err)

330− docStr :: Either Name Const -> Idris (Bool, ElabState [PDecl], Bool, [String], Either Err (Idris ()))

330+ docStr :: Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

331 docStr (Left n) = do ist <- getIState

332 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

333 [] -> return (False, e, False, prf,

test/proof003/test015.idr+3−3

@@ -106,9 +106,9 @@ Main.ntbEven = proof {

106-- There is almost certainly an easier proof. I don't care, for now :)

107

108Main.adc_lemma_2 = proof {

109− intro c,w,v,bit0,num0;

109+ intro w,v,num0,bit0

110− intro b0,v1,bit1,num1,b1;

110+ intro b0,v1,num1,bit1,b1

111− intro bc,x,x1,bX,bX1;

111+ intro c,bc,x,bX,x1,bX1

112 rewrite sym (plusZeroRightNeutral x);

113 rewrite sym (plusZeroRightNeutral v1);

114 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));

test/reg010/expected+2−5

@@ -1,5 +1,2 @@

1−reg010.idr:5:15:When elaborating right hand side of with block in usubst.unsafeSubst:

1+reg010.idr:5:15:When elaborating left hand side of with block in usubst.unsafeSubst:

2−Can't unify

2+Can't match on with block in usubst.unsafeSubst warg a P x x px

3− P x

4−with

5− P y

test/reg012/reg012.lidr+1−1

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

1> total soElim : (C : (b : Bool) -> So b -> Type) ->

2> C True Oh ->

3> (b : Bool) -> (s : So b) -> (C b s)

4−> soElim C coh .True .Oh = coh

4+> soElim C coh True Oh = coh

5

6> soFalseElim : So False -> a

7> soFalseElim x = void (soElim C () False x)

test/reg034/expected+2−22

@@ -1,24 +1,4 @@

1reg034.idr:6:5:When elaborating left hand side of bar:

2−When elaborating an application of main.bar:

2+Can't match on bar xs xs [91mRefl[0m

3− Can't unify

4− [92mlength[0m ys [94m=[0m [92mlength[0m ys

5− with

6− [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m ys

7−

8− Specifically:

9− Can't unify

10− [92mlength[0m ys

11− with

12− [92mlength[0m [95mxs[0m

13reg034.idr:9:5:When elaborating left hand side of foo:

3reg034.idr:9:5:When elaborating left hand side of foo:

14−When elaborating an application of main.foo:

4+Can't match on foo f x x [91mRefl[0m

15− Can't unify

16− [95mf[0m y [94m=[0m [95mf[0m y

17− with

18− [95mf[0m [95mx[0m [94m=[0m [95mf[0m y

19−

20− Specifically:

21− Can't unify

22− [95mf[0m y

23− with

24− [95mf[0m [95mx[0m

test/reg055/expectednew file+4

@@ -0,0 +1,4 @@

1+reg055.idr:5:3:When elaborating left hand side of g:

2+Can't match on g ([92mf[0m [91m0[0m)

3+reg055.idr:8:3:When elaborating left hand side of h:

4+Can't match on h x x

test/reg055/reg055.idrnew file+26

@@ -0,0 +1,26 @@

1+f : Nat -> Nat

2+f Z = Z

3+

4+g : Nat -> Nat

5+g (f Z) = 1

6+

7+h : Int -> Int -> Int

8+h x x = x

9+

10+data Parity : Nat -> Type where

11+ Even : Parity (n + n)

12+ Odd : Parity (S (n + n))

13+

14+foo : (n : Nat) -> Parity n -> Bool

15+foo (plus k k) Even = False

16+foo (S (plus k k)) Odd = True

17+

18+data EqualLists : List () -> List () -> Type where

19+ EL : EqualLists l l

20+

21+shouldWork : (l1,l2:List ()) -> EqualLists l1 l2 -> Bool

22+shouldWork [] [] EL = ?shouldWork_rhs_2

23+shouldWork (x :: xs) (x :: xs) EL = ?shouldWork_rhs_3

24+

25+-- shouldWork [] [] EL = ?x_1

26+-- shouldWork (x :: xs) (x :: xs) EL = ?x_2

test/reg055/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+idris $@ reg055.idr --check