7e7d0eb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Elaboration of local applications

7e7d0ebEdwin Brady11 years ago

libs/base/Data/List/Views.idr+2−2

compare with master

unifiedsplit

@@ -117,8 +117,8 @@ filtered : (p : a -> a -> Bool) -> (xs : List a) -> Filtered p xs

117filtered p inp with (smallerAcc inp)

118 filtered p [] | with_pat = FNil

119 filtered p (x :: xs) | (Access xsrec)

120− = FRec (Delay (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs)))

120+ = FRec (filtered p (filter (\y => p y x) xs) | xsrec _ (filteredLOK p x xs))

121− (Delay (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs)))

121+ (filtered p (filter (\y => not (p y x)) xs) | xsrec _ (filteredROK p x xs))

122

123lenImpossible : (n = Z) -> (n = ((S k) + right)) -> Void

124lenImpossible {n = Z} _ Refl impossible

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

@@ -372,8 +372,11 @@ instance Show Err where

372 show (Msg s) = s

373 show (InternalMsg s) = "Internal error: " ++ show s

374 show (CantUnify rcv l r e sc i) = "CantUnify " ++ show rcv ++ " " ++

375− show l ++ " " ++ show r ++ " " ++

375+ show l ++ " and " ++ show r ++ " " ++

376 show e ++ " in " ++ show sc ++ " " ++ show i

377+ show (CantConvert l r sc) = "CantConvert " ++

378+ show l ++ " and " ++ show r ++ " " ++

379+ " in " ++ show sc

377 show (CantSolveGoal g _) = "CantSolve " ++ show g

380 show (CantSolveGoal g _) = "CantSolve " ++ show g

378 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

381 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

379 show (UnknownImplicit n f) = show n ++ " is not an implicit argument of " ++ show f

382 show (UnknownImplicit n f) = show n ++ " is not an implicit argument of " ++ show f

@@ -395,7 +398,7 @@ instance Show Err where

395 show (NotEquality _ _) = "NotEquality"

398 show (NotEquality _ _) = "NotEquality"

396 show (TooManyArguments _) = "TooManyArguments"

399 show (TooManyArguments _) = "TooManyArguments"

397 show (CantIntroduce _) = "CantIntroduce"

400 show (CantIntroduce _) = "CantIntroduce"

398− show (NoSuchVariable _) = "NoSuchVariable"

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

399 show (WithFnType _) = "WithFnType"

402 show (WithFnType _) = "WithFnType"

400 show (NoTypeDecl _) = "NoTypeDecl"

403 show (NoTypeDecl _) = "NoTypeDecl"

401 show (NotInjective _ _ _) = "NotInjective"

404 show (NotInjective _ _ _) = "NotInjective"

src/Idris/Elab/Term.hs+24−5

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

285 then solveAuto ist fn False (a, failc)

286 else return ()) as

287

288+ apt <- expandToArity t

288− itm <- if not pattern then insertImpLam ina t else return t

289+ itm <- if not pattern then insertImpLam ina apt else return apt

289 ct <- insertCoerce ina itm

290 ct <- insertCoerce ina itm

290 t' <- insertLazy ct

291 t' <- insertLazy ct

291 g <- goal

292 g <- goal

@@ -299,8 +300,8 @@ elab ist info emode opts fn tm

299 -- ++ "\nproblems " ++ show ps

300 -- ++ "\nproblems " ++ show ps

300 -- ++ "\n-----------\n") $

301 -- ++ "\n-----------\n") $

301 --trace ("ELAB " ++ show t') $

302 --trace ("ELAB " ++ show t') $

302− let fc = fileFC "Force"

303 env <- get_env

304+ let fc = fileFC "Force"

304 handleError (forceErr t' env)

305 handleError (forceErr t' env)

305 (elab' ina fc' t')

306 (elab' ina fc' t')

306 (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))

307 (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))

@@ -497,11 +498,12 @@ elab ist info emode opts fn tm

497 trySeq (x : xs) = let e1 = elab' ina fc x in

498 trySeq (x : xs) = let e1 = elab' ina fc x in

498 try' e1 (trySeq' e1 xs) True

499 try' e1 (trySeq' e1 xs) True

499 trySeq [] = fail "Nothing to try in sequence"

500 trySeq [] = fail "Nothing to try in sequence"

500− trySeq' deferr [] = proofFail deferr

501+ trySeq' deferr [] = do deferr; unifyProblems

501 trySeq' deferr (x : xs)

502 trySeq' deferr (x : xs)

502 = try' (tryCatch (do elab' ina fc x

503 = try' (tryCatch (do elab' ina fc x

503− solveAutos ist fn False)

504+ solveAutos ist fn False

505+ unifyProblems)

504− (\_ -> deferr))

506+ (\_ -> trySeq' deferr []))

505 (trySeq' deferr xs) True

507 (trySeq' deferr xs) True

506 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

508 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

507 env <- get_env

509 env <- get_env

@@ -1421,6 +1423,23 @@ elab ist info emode opts fn tm

1421 notImplicitable (PCase _ _ _) = True

1423 notImplicitable (PCase _ _ _) = True

1422 notImplicitable _ = False

1424 notImplicitable _ = False

1423

1425

1426+ -- Elaboration works more smoothly if we expand function applications

1427+ -- to their full arity and elaborate it all at once (better error messages

1428+ -- in particular)

1429+ expandToArity tm@(PApp fc f a) = do

1430+ env <- get_env

1431+ case fullApp tm of

1432+ -- if f is global, leave it alone because we've already

1433+ -- expanded it to the right arity

1434+ PApp fc ftm@(PRef _ _ f) args | Just aty <- lookup f env ->

1435+ do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))

1436+ return (mkPApp fc a ftm args)

1437+ _ -> return tm

1438+ expandToArity t = return t

1439+

1440+ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1441+ fullApp x = x

1442+

1424 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1443 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1425 | tcinstance i && not (toplevel_imp i)

1444 | tcinstance i && not (toplevel_imp i)

1426 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1445 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs