55ffc21 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some display tweaks for explicit arguments

commit55ffc21e5f090415335b7ef32a694945547caf5f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 31 Aug 2015, 20:13 (11 years ago) parent60f0cb5

4 files changed+15−3

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Delaborate.hs+12 src/Idris/Interactive.hs+1−1 src/Idris/ProofSearch.hs+1−1

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1656,7 +1656,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16561656 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

16571657 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

16581658 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)

1659− | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs

1659+ | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs

16601660 || ppopt_pinames ppo && uname n =

16611661 depth d . bracket p startPrec . group $

16621662 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

src/Idris/Delaborate.hs+12

@@ -359,9 +359,21 @@ pprintErr' i (IncompleteTerm t)

359359 (map pprintIncomplete (nub $ getMissing [] [] t))))

360360 where

361361 pprintIncomplete (tm, arg)

362+ | expname arg

363+ = text "Can't infer explicit argument to" <+>

364+ annTm tm (pprintTerm i (delabSugared i tm))

365+ | otherwise

362366 = text "Can't infer argument" <+> annName arg <+> text "to" <+>

363367 annTm tm (pprintTerm i (delabSugared i tm))

364368

369+ expname (UN n) = case str n of

370+ ('_':_) -> True

371+ _ -> False

372+ expname (MN _ n) = case str n of

373+ ('_':_) -> True

374+ _ -> False

375+ expname _ = False

376+

365377 getMissing :: [Name] -> [Name] -> Term -> [(Term, Name)]

366378 getMissing hs env (Bind n (Hole ty) sc)

367379 = getMissing (n : hs) (n : env) sc

src/Idris/Interactive.hs+1−1

@@ -170,7 +170,7 @@ makeCase fn updatefile l n

170170 do let fb = fn ++ "~"

171171 runIO $ writeSource fb (unlines (before ++ newcase ++ later))

172172 runIO $ copyFile fb fn

173− else iPrintResult (showSep "\n" newcase)

173+ else iPrintResult (showSep "\n" newcase ++"\n")

174174 where addCaseSkel n line =

175175 let b = brackets False line in

176176 case findSubstr ('?':n) line of

src/Idris/ProofSearch.hs+1−1

@@ -321,7 +321,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

321321 isImp (PImp p _ _ _ _) = (True, p)

322322 isImp arg = (False, priority arg)

323323

324−-- In interactive mode, only search for things if there is some constructor

324+-- In interactive mode, only search for things if there is some

325325-- index to help pick a relevant constructor

326326checkConstructor :: IState -> [Name] -> ElabD ()

327327checkConstructor ist [] = return ()