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

git.iko.soy/Idris-dev

Elaboration of local applications

Expand application of local variables to all of their arguments in one go, where their type is known. This is better for type-directed disambiguation, and for reporting errors more accurately.

commit7e7d0eb19b03b05cd80cf9df31f7f176611d87ed authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 Apr 2016, 09:48 (11 years ago) parentd662e26

3 files changed+31−9

compare with master

unifiedsplit

libs/base/Data/List/Views.idr+2−2 src/Idris/Core/TT.hs+5−2 src/Idris/Elab/Term.hs+24−5

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

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

117117filtered p inp with (smallerAcc inp)

118118 filtered p [] | with_pat = FNil

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

120− = FRec (Delay (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)))

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

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

122122

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

124124lenImpossible {n = Z} _ Refl impossible

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

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

372372 show (Msg s) = s

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

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

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

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

376376 show e ++ " in " ++ show sc ++ " " ++ show i

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

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

379+ " in " ++ show sc

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

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

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

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

395398 show (NotEquality _ _) = "NotEquality"

396399 show (TooManyArguments _) = "TooManyArguments"

397400 show (CantIntroduce _) = "CantIntroduce"

398− show (NoSuchVariable _) = "NoSuchVariable"

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

399402 show (WithFnType _) = "WithFnType"

400403 show (NoTypeDecl _) = "NoTypeDecl"

401404 show (NotInjective _ _ _) = "NotInjective"

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

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

285285 then solveAuto ist fn False (a, failc)

286286 else return ()) as

287287

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

288+ apt <- expandToArity t

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

289290 ct <- insertCoerce ina itm

290291 t' <- insertLazy ct

291292 g <- goal

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

299300 -- ++ "\nproblems " ++ show ps

300301 -- ++ "\n-----------\n") $

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

302− let fc = fileFC "Force"

303303 env <- get_env

304+ let fc = fileFC "Force"

304305 handleError (forceErr t' env)

305306 (elab' ina fc' t')

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

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

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

498499 try' e1 (trySeq' e1 xs) True

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

500− trySeq' deferr [] = proofFail deferr

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

501502 trySeq' deferr (x : xs)

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

503− solveAutos ist fn False)

504− (\_ -> deferr))

504+ solveAutos ist fn False

505+ unifyProblems)

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

505507 (trySeq' deferr xs) True

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

507509 env <- get_env

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

14211423 notImplicitable (PCase _ _ _) = True

14221424 notImplicitable _ = False

14231425

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+

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

14251444 | tcinstance i && not (toplevel_imp i)

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