1909c32 · Idris-dev · git.iko.soy

76 getIndent i n xs | take 9 xs == "instance " = i

77 getIndent i n xs | take (length n) xs == n = i

78 getIndent i n (x : xs) = getIndent (i + 1) n xs

79−

79+

80 getAppName (PApp _ r _) = getAppName r

81 getAppName (PRef _ _ r) = r

82 getAppName (PTyped n _) = getAppName n

120 if updatefile

121 then do let fb = fn ++ "~"

122 runIO $ writeSource fb (unlines (before ++ nonblank)

123− ++ extras ++

123+ ++ extras ++

124 (if null extras then ""

125 else "\n" ++ unlines rest))

126 runIO $ copyFile fb fn

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

194 Just (before, pos, after) ->

195 [before ++ (if b then "(" else "") ++ "case _ of",

196− take (pos + (if b then 6 else 5)) (repeat ' ') ++

196+ take (pos + (if b then 6 else 5)) (repeat ' ') ++

197 "case_val => ?" ++ n ++ (if b then ")" else "")

198 ++ after]

199 Nothing -> fail "No such metavariable"

208

209 findSubstr n xs = findSubstr' [] 0 n xs

210

211− findSubstr' acc i n xs | take (length n) xs == n

211+ findSubstr' acc i n xs | take (length n) xs == n

212 = Just (reverse acc, i, drop (length n) xs)

213 findSubstr' acc i n [] = Nothing

214 findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs

217

218

219

220−doProofSearch :: FilePath -> Bool -> Bool ->

220+doProofSearch :: FilePath -> Bool -> Bool ->

221 Int -> Name -> [Name] -> Maybe Int -> Idris ()

222doProofSearch fn updatefile rec l n hints Nothing

223 = doProofSearch fn updatefile rec l n hints (Just 20)

230 [] -> return n

231 ns -> ierror (CantResolveAlts ns)

232 i <- getIState

233− let (top, envlen, psnames, _)

233+ let (top, envlen, psnames, _)

234 = case lookup mn (idris_metavars i) of

235 Just (t, e, ns, False) -> (t, e, ns, False)

236 _ -> (Nothing, 0, [], True)

281 (mv, []) -> if (mv == n) then new else '?' : mv

282updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new

283updateMeta ('=':cs) n new = '=':updateMeta cs n new

284−updateMeta (c:cs) n new

284+updateMeta (c:cs) n new

285 = c : updateMeta cs n new

286updateMeta [] n new = ""

287

296guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new

297guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new

298guessBrackets brack ('=':cs) n new = guessBrackets False cs n new

299−guessBrackets brack (c:cs) n new

299+guessBrackets brack (c:cs) n new

300 = guessBrackets (brack || not (isSpace c)) cs n new

301guessBrackets brack [] n new = ""

302

308 isProv' _ ('}':cs) n = isProv' True cs n

309 isProv' p (_:cs) n = isProv' p cs n

310 isProv' _ [] n = False

311−

311+

312addBracket False new = new

313addBracket True new@('(':xs) | last xs == ')' = new

314addBracket True new | any isSpace new = '(' : new ++ ")"

322

323 -- if the name is in braces, rather than preceded by a ?, treat it

324 -- as a lemma in a provisional definition

325−

325+

326 let isProv = checkProv tyline (show n)

327

328 ctxt <- getContext

339 let skip = guessImps i (tt_ctxt i) mty

340 let classes = guessClasses i (tt_ctxt i) mty

341

342− let lem = show n ++ " : " ++

342+ let lem = show n ++ " : " ++

343 constraints i classes mty ++

344 showTmOpts (defaultPPOption { ppopt_pinames = True })

345 (stripMNBind skip margs (delab i mty))

379 where getIndent s = length (takeWhile isSpace s)

380

381 appArgs skip 0 _ = ""

382− appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)

382+ appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)

383 | (thead c /= '_' && n `notElem` skip)

384 = " " ++ show n ++ appArgs skip (i - 1) sc

385 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

386 appArgs skip i _ = ""

387

388 stripMNBind _ args t | args <= 0 = t

389− stripMNBind skip args (PPi b n@(UN c) _ ty sc)

389+ stripMNBind skip args (PPi b n@(UN c) _ ty sc)

390 | n `notElem` skip ||

391 take 4 (str c) == "__pi" -- keep in type, but not in app

392 = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)

399 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "

400

401 showConstraints i ns (Bind n (Pi _ ty _) sc)

402− | n `elem` ns = show (delab i ty) :

402+ | n `elem` ns = show (delab i ty) :

403 showConstraints i ns (substV (P Bound n Erased) sc)

404 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)

405 showConstraints _ _ _ = []

410 -- Also, make type class instances implicit

411 guessImps :: IState -> Context -> Term -> [Name]

412 -- machine names aren't lifted

413− guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

413+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

414 = n : guessImps ist ctxt sc

415 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

416− | guarded ctxt n (substV (P Bound n Erased) sc)

416+ | guarded ctxt n (substV (P Bound n Erased) sc)

417 = n : guessImps ist ctxt sc

418 | isClass ist ty

419 = n : guessImps ist ctxt sc

421 | ignoreName n = n : guessImps ist ctxt sc

422 | otherwise = guessImps ist ctxt sc

423 guessImps ist ctxt _ = []

424−

424+

425 paramty (TType _) = True

426 paramty (Bind _ (Pi _ (TType _) _) sc) = paramty sc

427 paramty _ = False

428−

428+

429 -- TMP HACK unusable name so don't lift

430 ignoreName n = case show n of

431 "_aX" -> True

444 Just _ -> True

445 _ -> False

446 | otherwise = False

447−

447+

448 isParamClass ist t

449 | (P _ n _, args) <- unApply t

450 = case lookupCtxtExact n (idris_classes ist) of

460 isConName f ctxt = any (guarded ctxt n) args

461-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

462-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc

463− guarded ctxt n (Bind _ (Pi _ t _) sc)

463+ guarded ctxt n (Bind _ (Pi _ t _) sc)

464 = guarded ctxt n t || guarded ctxt n sc

465 guarded ctxt n _ = False

466

467 blank = all isSpace

468

469 addLem before tyline lem lem_app later

470− = let (bef_end, blankline : bef_start)

470+ = let (bef_end, blankline : bef_start)

471 = case span (not . blank) (reverse before) of

472 (bef, []) -> (bef, "" : [])

473 x -> x

481 = case span (not . blank) later of

482 (bef, []) -> (bef, "" : [])

483 x -> x in

484− unlines $ before ++ tyline :

484+ unlines $ before ++ tyline :

485 (later_bef ++ [blankline, lem_app, blankline] ++

486 later_end)