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

idris.cabal+3

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

276276 test/reg054/run

277277 test/reg054/*.idr

278278 test/reg054/expected

279+ test/reg055/run

280+ test/reg055/*.idr

281+ test/reg055/expected

279282

280283 test/basic001/run

281284 test/basic001/*.idr

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

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

2020 | CantIntroduce TT

2121 | NoSuchVariable TTName

2222 | WithFnType TT

23+ | CantMatch TT

2324 | NoTypeDecl TTName

2425 | NotInjective TT TT TT

2526 | CantResolve TT

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

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

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

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

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

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

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

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

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

src/Idris/AbsSyntax.hs+23−10

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

14371437 | f `elem` infns = PInferRef fc f

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

14391439 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 [])

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

14421442 = let lt' = ai qq env ds lt

14431443 rt' = ai qq env ds rt

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

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

16331633

16341634-- replace non-linear occurrences with _

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

1636−-- it is hard to get right!

16371635

16381636stripLinear :: IState -> PTerm -> PTerm

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

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

16431641 = return $ PRef fc f

16441642 | otherwise = do ns <- get

16451643 if (f `elem` ns)

1646− then return Placeholder

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

16471645 else do put (f : ns)

16481646 return (PRef fc f)

16491647 sl (PPatvar fc f)

16501648 = do ns <- get

16511649 if (f `elem` ns)

1652− then return Placeholder

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

16531651 else do put (f : ns)

16541652 return (PPatvar fc f)

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

1656− return t

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

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

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')

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

16581664 args' <- mapM slA args

16591665 return $ PApp fc fn args'

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

16791685 su (PRef fc f)

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

16811687 = Placeholder

1682− su (PApp fc fn args)

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

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

1689+ | isDConName fn ctxt

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

1691+ su (PApp fc f args)

1692+ = PHidden (PApp fc f args)

16841693 su (PAlternative b alts)

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

16861695 if null alts' then Placeholder

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

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

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

16901699 su t = t

1700+

1701+ ctxt = tt_ctxt i

1702+

16911703stripUnmatchable i tm = tm

16921704

16931705mkPApp fc a f [] = f

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

18351847 mty <- match' ty ty'

18361848 ms <- match' s s'

18371849 return (mt ++ mty ++ ms)

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+8−1

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

585585!-}

586586

587587-- For elaborator state

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

588+data EState = EState {

589+ case_decls :: [PDecl],

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

591+ }

592+

593+initEState = EState [] []

594+

595+type ElabD a = Elab' EState a

589596

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

591598--

src/Idris/Core/Binary.hs+3

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

120120 put e

121121 put (WithFnType t) = do putWord8 34

122122 put t

123+ put (CantMatch t) = do putWord8 35

124+ put t

123125

124126 get = do i <- getWord8

125127 case i of

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

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

175177 return $ ReflectionFailed x y

176178 34 -> fmap WithFnType get

179+ 35 -> fmap CantMatch get

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

178181----- Generated by 'derive'

179182

src/Idris/Core/CaseTree.hs−7

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

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

264264 if proj then return (stripLambdas t)

265265 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"))

273266 Error err -> Error (At fc err)

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

275268 defaultCase True = STerm Erased

src/Idris/Core/Elaborate.hs+28

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

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

413413movelast n = processTactic' (MoveLast n)

414414

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+

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

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

417445zipHere :: Elab' aux ()

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

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

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

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

3333 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

3436 solved :: Maybe (Name, Term),

3537 problems :: Fails,

3638 injective :: [Name],

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

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

215217 (map fst (notunified ps)) while

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

217− P _ _ _ -> False

219+-- P _ _ _ -> False

218220 _ -> n `elem` dont) u

219221 traceWhen (unifylog ps)

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

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

287289newProof n ctxt ty = let h = holeName 0

288290 ty' = vToP ty in

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

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

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

291293 Nothing [] []

292294 [] [] []

293295 Nothing ctxt "" False False [] []

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

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

500502 = do ps <- get

501503 let (uh, uns) = unified ps

502− case lookup x (notunified ps) of

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

504− match_unify' ctxt env tm val

505− _ -> return []

504+ dropdots <-

505+ case lookup x (notunified ps) of

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

507+ do match_unify' ctxt env tm val

508+ return [x]

509+ _ -> return []

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

507511 holes ps \\ [x],

508512 solved = Just (x, val),

509513 notunified = updateNotunified [(x,val)]

510514 (notunified ps),

511515 recents = x : recents ps,

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

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

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

513518 let tm' = subst x val sc in

514519 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

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

516526 = do ps <- get

517527 case findType x sc of

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

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

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

576586 (notunified ps),

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

587+ injective = addInj n x (injective ps)

588+ })

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

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

580591 | otherwise = ps

src/Idris/Core/TT.hs+1

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

147147 | UniqueKindError Universe Name

148148 | ProgramLineComment

149149 | Inaccessible Name

150+ | CantMatch t

150151 | NonCollapsiblePostulate Name

151152 | AlreadyDefined Name

152153 | ProofSearchFail (Err' t)

src/Idris/Delaborate.hs+4

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

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

263263pprintErr' i (WithFnType ty) =

264264 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))

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

266268pprintErr' i UniverseError = text "Universe inconsistency"

267269pprintErr' i (UniqueError NullType n)

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

513515showbasic (MN _ s) = str s

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

515517showbasic (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

445445 i <- getIState

446446 let lhs = addImplPat i lhs_in

447447 -- 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

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

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

451451 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

561561 [t] -> t

562562 _ -> []

563563 let params = getParamsInType i [] fn_is fn_ty

564− let lhs = mkLHSapp $ stripUnmatchable i $

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

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

565+ propagateParams i params fn_ty (addImplPat i lhs_in)

566+-- let lhs = mkLHSapp $

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

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

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

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

569571

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

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

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

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

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

574576 probs <- get_probs

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

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

643645 logLvl 5 "STARTING CHECK"

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

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

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

646648 (do pbinds ist lhs_tm

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

648650 setNextName

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

652654 (erun fc $ psolve lhs_tm)

653655 hs <- get_holes

654656 aux <- getAux

655− mapM_ (elabCaseHole aux) hs

657+ mapM_ (elabCaseHole (case_decls aux)) hs

656658 tt <- get_term

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

658660 probs <- get_probs

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

793795 [t] -> t

794796 _ -> []

795797 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)

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

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

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

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

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

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

802804 let lhs_tm = orderPats (getInferTerm lhs')

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

812814 -- Elaborate wval in this context

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

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

815− (bindTyArgs PVTy bargs infP) []

817+ (bindTyArgs PVTy bargs infP) initEState

816818 (do pbinds i lhs_tm

817819 setNextName

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

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

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

893895 i <- getIState

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

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

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

896898 (do pbinds i lhs_tm

897899 setNextName

898900 (_, 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

168168 let ty = addImpl i ty'

169169 ctxt <- getContext

170170 ((tyT, _, _), _) <-

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

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

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

173173 ctxt <- getContext

174174 (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

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

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

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

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

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

5959 (infTerm lhs)))

6060 let lhs_tm = orderPats (getInferTerm lhs')

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

6767

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

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

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

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

7171 (do pbinds i lhs_tm

7272 setNextName

7373 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

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

6767

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

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

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

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

7171

7272 let tyT = patToImp tyT'

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

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

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

6565

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

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

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

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

6969 let vtm = orderPats (getInferTerm tm')

7070

src/Idris/ElabTerm.hs+40−8

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

9494 when tydecl (do update_term orderPats

9595 mkPat)

9696-- update_term liftPats)

97− is <- getAux

97+ EState is _ <- getAux

9898 tt <- get_term

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

100100 log <- getLog

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

130130 [] -> return ()

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

132132 else lift (Error e)

133− is <- getAux

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)))

138+ EState is _ <- getAux

134139 tt <- get_term

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

136141 log <- getLog

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

181186 compute -- expand type synonyms, etc

182187 let fc = maybe "(unknown)"

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

189+ est <- getAux

190+ sequence_ (delayed_elab est)

184191 end_unify

185192 ptm <- get_term

186193 when pattern -- convert remaining holes to pattern vars

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

388395 trySeq' deferr (x : xs)

389396 = try' (do elab' ina fc x

390397 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

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

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

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

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

587594 | otherwise

588595 = do env <- get_env

589596 ty <- goal

597+ ctxt <- get_context

590598 let unmatchableArgs = if pattern

591599 then getUnmatchable (tt_ctxt ist) f

592600 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+

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

594605 && isTConName f (tt_ctxt ist)) $

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

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

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

613624 -- maybe more things are solvable now

614625 unifyProblems

615− ctxt <- get_context

616626 let guarded = isConName f ctxt

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

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

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

666676 PLam _ _ _ -> 3

667677 PRewrite _ _ _ _ -> 4

668678 PResolveTC _ -> 0

679+ PHidden _ -> 150

669680 _ -> 1

670681

671682 constraint (PConstraint _ _ _ _) = True

672683 constraint _ = False

673684

674685 -- 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.

676688 -- Only relevant when on lhs

677689 conDepth d t | not pattern = 0

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

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

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

682694 conDepth d (PPatvar _ _) = 0

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

696+ conDepth d (PHidden _) = 150

684697 conDepth d Placeholder = 0

685698 conDepth d (PResolveTC _) = 0

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

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

810823 (caseBlock fc cname'

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

812825 -- elaborate case

813− updateAux (newdef : )

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

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

815828 movelast tyn

816829 solve

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

930943

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

932945 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

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

934961

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

963+

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

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

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

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

11261155 | otherwise = locallyBound ts

11271156 getName (PRef _ n) = Just n

11281157 getName (PApp _ f _) = getName f

1158+ getName (PHidden t) = getName t

11291159 getName _ = Nothing

11301160

11311161pruneByType env (P _ n _) ctxt as

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

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

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

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

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

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

11471178

11481179 typeHead var f f'

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

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

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

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

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

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

21992231reflectErr (NotInjective t1 t2 t3) =

22002232 raw_apply (Var $ reflErrName "NotInjective")

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

23062338 Right (TextPart msg)

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

23082340 | n == reflm "NamePart" =

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

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

23102342 Error e -> Left . InternalMsg $

23112343 "could not reify name term " ++

23122344 show ttn ++

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

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

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

23162348 | n == reflm "TermPart" =

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

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

23182350 Error e -> Left . InternalMsg $

23192351 "could not reify reflected term " ++

23202352 show tm ++

src/Idris/Prover.hs+8−8

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

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

5454 break = "\n" ++ bird

5555

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

56+proverSettings :: ElabState EState -> Settings Idris

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

5858

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

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

6060assumptionNames e

6161 = case envAtFocus (proof e) of

6262 OK env -> names env

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

6868prove opt ctxt lit n ty

6969 = do let ps = initElaborator n ctxt ty

7070 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

7272 iLOG $ "Adding " ++ show tm

7373 i <- getIState

7474 case idris_outputmode i of

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

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

100100 _ -> return ()

101101

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

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

103103elabStep st e = case runStateT eCheck st of

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

105105 Error a -> ierror a

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

177177 freeEnvNames :: Env -> [Name]

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

179179

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

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

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

182182 return v

183183

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

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

185185receiveInput h e =

186186 do i <- getIState

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

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

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

206206 _ -> return Nothing

207207

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])

209209ploop fn d prompt prf e h

210210 = do i <- getIState

211211 let autoSolve = opt_autoSolve (idris_options i)

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

327327 putIState ist

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

329329 (\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 ()))

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

332332 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

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

test/proof003/test015.idr+3−3

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

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

107107

108108Main.adc_lemma_2 = proof {

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

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

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

109+ intro w,v,num0,bit0

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

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

112112 rewrite sym (plusZeroRightNeutral x);

113113 rewrite sym (plusZeroRightNeutral v1);

114114 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:

2−Can't unify

3− P x

4−with

5− P y

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

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

test/reg012/reg012.lidr+1−1

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

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

22> C True Oh ->

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

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

4+> soElim C coh True Oh = coh

55

66> soFalseElim : So False -> a

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

test/reg034/expected+2−22

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

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

2−When elaborating an application of main.bar:

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

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

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

14−When elaborating an application of main.foo:

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

4+Can't match on foo f x x [91mRefl[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