26cfbe9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Scoped implicits fix

26cfbe9Edwin Brady12 years ago

idris.cabal+3

compare with master

unifiedsplit

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

286 test/reg057/run

287 test/reg057/*.idr

288 test/reg057/expected

289+ test/reg058/run

290+ test/reg058/*.idr

291+ test/reg058/expected

289

292

290 test/basic001/run

293 test/basic001/run

291 test/basic001/*.idr

294 test/basic001/*.idr

libs/effects/Effects.idr+1

@@ -310,4 +310,5 @@ when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()

310when True e = Force e

311when False e = pure ()

312

313+

313-- --------------------------------------------------------------------- [ EOF ]

314-- --------------------------------------------------------------------- [ EOF ]

src/Idris/AbsSyntaxTree.hs+1

@@ -757,6 +757,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

757 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding

758 | PTyped PTerm PTerm -- ^ Term with explicit type

759 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

760+ | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

760 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

761 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

761 | PMatchApp FC Name -- ^ Make an application by type matching

762 | PMatchApp FC Name -- ^ Make an application by type matching

762 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

763 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

src/Idris/Core/Elaborate.hs+4−4

@@ -234,7 +234,7 @@ is_guess = do ES p _ _ <- get

234 _ -> return False

235

236-- Get the guess at the current hole, if there is one

237−get_guess :: Elab' aux Type

237+get_guess :: Elab' aux Term

238get_guess = do ES p _ _ <- get

239 b <- lift $ goalAtFocus (fst p)

240 case b of

@@ -674,7 +674,7 @@ checkPiGoal n

674 focus f

675

676simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

677−simple_app infer fun arg app0str =

677+simple_app infer fun arg str =

678 do a <- getNameFrom (sMN 0 "argTy")

679 b <- getNameFrom (sMN 0 "retTy")

680 f <- getNameFrom (sMN 0 "f")

@@ -705,8 +705,8 @@ simple_app infer fun arg app0str =

705 when (a `elem` hs) $ do movelast a

706 when (b `elem` hs) $ do movelast b

707 end_unify

708+ where

708− where regretWith err = try regret

709+ regretWith err = try regret (lift $ tfail err)

709− (lift $ tfail err)

710

711-- Abstract over an argument of unknown type, giving a name for the hole

712-- which we'll fill with the argument type too.

src/Idris/Core/ProofState.hs+6−4

@@ -853,6 +853,7 @@ updateProblems ps updates probs = up updates probs where

853 hs = holes ps

854 inj = injective ps

855 ctxt = context ps

856+ ulog = unifylog ps

856 usupp = map fst (notunified ps)

857 usupp = map fst (notunified ps)

857

858

858 up ns [] = (ns, [])

859 up ns [] = (ns, [])

@@ -864,8 +865,8 @@ updateProblems ps updates probs = up updates probs where

864 if newx || newy || ready ||

865 if newx || newy || ready ||

865 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

866 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

866 case unify ctxt env' x' y' inj hs usupp while of

867 case unify ctxt env' x' y' inj hs usupp while of

867− OK (v, []) -> -- trace ("DID " ++ show (x',y',ready,v)) $

868+ OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

868− up (ns ++ v) ps

869+ up (ns ++ v) ps

869 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

870 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

870 let (ns', ps') = up ns ps in

871 let (ns', ps') = up ns ps in

871 (ns', (x',y', False, env',err', while, um) : ps')

872 (ns', (x',y', False, env',err', while, um) : ps')

@@ -966,7 +967,9 @@ processTactic t ps

966 -- apply them here

967 -- apply them here

967 let ns' = dropGiven (dontunify ps') ns_in (holes ps')

968 let ns' = dropGiven (dontunify ps') ns_in (holes ps')

968 let pterm'' = updateSolved ns' (pterm ps')

969 let pterm'' = updateSolved ns' (pterm ps')

970+ traceWhen (unifylog ps)

971+ ("Updated problems after solve " ++ qshow probs' ++ "\n" ++

969− traceWhen (unifylog ps) ("(Toplevel) Dropping holes: " ++ show (map fst ns')) $

972+ "(Toplevel) Dropping holes: " ++ show (map fst ns')) $

970 return (ps' { pterm = pterm'',

973 return (ps' { pterm = pterm'',

971 solved = Nothing,

974 solved = Nothing,

972 problems = probs',

975 problems = probs',

@@ -989,7 +992,6 @@ process t h = tactic (Just h) (mktac t)

989 mktac (MatchFill r) = match_fill r

992 mktac (MatchFill r) = match_fill r

990 mktac (PrepFill n ns) = prep_fill n ns

993 mktac (PrepFill n ns) = prep_fill n ns

991 mktac CompleteFill = complete_fill

994 mktac CompleteFill = complete_fill

992− mktac Regret = regret

993 mktac Solve = solve

995 mktac Solve = solve

994 mktac (StartUnify n) = start_unify n

996 mktac (StartUnify n) = start_unify n

995 mktac Compute = compute

997 mktac Compute = compute

src/Idris/Core/TT.hs+3

@@ -1345,6 +1345,8 @@ showEnv' env t dbg = se 10 env t where

1345 = (show $ fst $ env!!i) ++

1346 if dbg then "{" ++ show i ++ "}" else ""

1347 | otherwise = "!!V " ++ show i ++ "!!"

1348+ se p env (Bind n b@(Pi (Just _) t k) sc)

1349+ = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1348 se p env (Bind n b@(Pi _ t k) sc)

1350 se p env (Bind n b@(Pi _ t k) sc)

1349 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc

1351 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc

1350 where arrow (TType _) = " -> "

1352 where arrow (TType _) = " -> "

@@ -1361,6 +1363,7 @@ showEnv' env t dbg = se 10 env t where

1361 sb env n (Lam t) = showb env "\\ " " => " n t

1363 sb env n (Lam t) = showb env "\\ " " => " n t

1362 sb env n (Hole t) = showb env "? " ". " n t

1364 sb env n (Hole t) = showb env "? " ". " n t

1363 sb env n (GHole i t) = showb env "?defer " ". " n t

1365 sb env n (GHole i t) = showb env "?defer " ". " n t

1366+ sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

1364 sb env n (Pi _ t _) = showb env "(" ") -> " n t

1367 sb env n (Pi _ t _) = showb env "(" ") -> " n t

1365 sb env n (PVar t) = showb env "pat " ". " n t

1368 sb env n (PVar t) = showb env "pat " ". " n t

1366 sb env n (PVTy t) = showb env "pty " ". " n t

1369 sb env n (PVTy t) = showb env "pty " ". " n t

src/Idris/Core/Unify.hs+3−3

@@ -153,7 +153,7 @@ match_unify ctxt env topx topy inj holes from =

153 h2 <- un bnames vx vy

154 combine bnames h1 h2

155 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

156− uB bnames (Pi _ tx _) (Pi _ ty _) = un bnames tx ty

156+ uB bnames (Pi i tx _) (Pi i' ty _) = un bnames tx ty

157 uB bnames x y = do UI s f <- get

158 let r = recoverable (normalise ctxt env (binderTy x))

159 (normalise ctxt env (binderTy y))

@@ -461,8 +461,8 @@ unify ctxt env topx topy inj holes usersupp from =

461 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy

462 combine bnames h1 h2

463 where sameBinder (Lam _) (Lam _) = True

464− sameBinder (Pi _ _ _) (Pi _ _ _) = True

464+ sameBinder (Pi i _ _) (Pi i' _ _) = True

465− sameBinder _ _ = False

465+ sameBinder _ _ = False -- never unify holes/guesses/etc

466 un' fn bnames x y

467 | OK True <- convEq' ctxt holes x y = do sc 1; return []

468 | isUniverse x && isUniverse y = do sc 1; return []

src/Idris/DeepSeq.hs+1

@@ -202,6 +202,7 @@ instance NFData PTerm where

202 rnf (PLet _ x1 x2 x3 x4)

203 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

204 rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

205+ rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

205 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

206 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

206 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

207 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

207 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

208 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/ElabTerm.hs+83−37

@@ -164,13 +164,14 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

164getUnmatchable ctxt n = []

165

166data ElabCtxt = ElabCtxt { e_inarg :: Bool,

167+ e_isfn :: Bool, -- ^ Function part of application

167 e_guarded :: Bool,

168 e_guarded :: Bool,

168 e_intype :: Bool,

169 e_intype :: Bool,

169 e_qq :: Bool,

170 e_qq :: Bool,

170 e_nomatching :: Bool -- ^ can't pattern match

171 e_nomatching :: Bool -- ^ can't pattern match

171 }

172 }

172

173

173−initElabCtxt = ElabCtxt False False False False False

174+initElabCtxt = ElabCtxt False False False False False False

174

175

175goal_polymorphic :: ElabD Bool

176goal_polymorphic :: ElabD Bool

176goal_polymorphic =

177goal_polymorphic =

@@ -244,7 +245,7 @@ elab ist info emode opts fn tm

244 then solveAuto ist fn False a

245 then solveAuto ist fn False a

245 else return ()) as

246 else return ()) as

246

247

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

248+ itm <- if not pattern then insertImpLam ina t else return t

248 ct <- insertCoerce ina itm

249 ct <- insertCoerce ina itm

249 t' <- insertLazy ct

250 t' <- insertLazy ct

250 g <- goal

251 g <- goal

@@ -596,17 +597,13 @@ elab ist info emode opts fn tm

596 _ -> lift $ tfail (NoSuchVariable fn)

597 _ -> lift $ tfail (NoSuchVariable fn)

597 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

598 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

598 solve

599 solve

599− -- This isn't a sound way of checking for Typecase - we need a

600− -- better way!

601−-- elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')

602−-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

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

604 -- if f is local, just do a simple_app

600 -- if f is local, just do a simple_app

601+ -- FIXME: Anyone feel like refactoring this mess? - EB

605− elab' ina _ tm@(PApp fc (PRef _ f) args_in)

602+ elab' ina topfc tm@(PApp fc (PRef _ f) args_in)

606 | pattern && not reflection && e_nomatching ina

603 | pattern && not reflection && e_nomatching ina

607 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

604 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

608− | otherwise

605+ | otherwise = implicitApp $

609− = do env <- get_env

606+ do env <- get_env

610 ty <- goal

607 ty <- goal

611 fty <- get_type (Var f)

608 fty <- get_type (Var f)

612 ctxt <- get_context

609 ctxt <- get_context

@@ -614,18 +611,18 @@ elab ist info emode opts fn tm

614 let unmatchableArgs = if pattern

611 let unmatchableArgs = if pattern

615 then getUnmatchable (tt_ctxt ist) f

612 then getUnmatchable (tt_ctxt ist) f

616 else []

613 else []

617− -- Dot it if we're in a pattern and it isn't a constructor

614+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

618−-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm

619−

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

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

621 && isTConName f (tt_ctxt ist)) $

616 && isTConName f (tt_ctxt ist)) $

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

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

623 if (f `elem` map fst env && length args == 1 && length args_in == 1)

618 if (f `elem` map fst env && length args == 1 && length args_in == 1)

624 then -- simple app, as below

619 then -- simple app, as below

625− do simple_app False (elabE ina (Just fc) (PRef fc f))

620+ do simple_app False

621+ (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))

626 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

622 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

627 (show tm)

623 (show tm)

628 solve

624 solve

625+ return []

629 else

626 else

630 do ivs <- get_instances

627 do ivs <- get_instances

631 ps <- get_probs

628 ps <- get_probs

@@ -656,22 +653,58 @@ elab ist info emode opts fn tm

656 (zip ns' (unmatchableArgs ++ repeat False))

653 (zip ns' (unmatchableArgs ++ repeat False))

657 (f == sUN "Force")

654 (f == sUN "Force")

658 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

655 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

656+ imp <- if (e_isfn ina) then

657+ do guess <- get_guess

658+ gty <- get_type (forget guess)

659+ env <- get_env

660+ let ty_n = normalise ctxt env gty

661+ return $ getReqImps ty_n

662+ else return []

663+ -- Now we find out how many implicits we needed at the

664+ -- end of the application by looking at the goal again

665+ -- - Have another go, but this time add the

666+ -- implicits (can't think of a better way than this...)

667+ case imp of

668+ rs@(_:_) | not pattern -> return rs -- quit, try again

659− solve

669+ _ -> do solve

670+ hs <- get_holes

660− ivs' <- get_instances

671+ ivs' <- get_instances

661− -- Attempt to resolve any type classes which have 'complete' types,

672+ -- Attempt to resolve any type classes which have 'complete' types,

662− -- i.e. no holes in them

673+ -- i.e. no holes in them

663− when (not pattern || (e_inarg ina && not tcgen &&

674+ when (not pattern || (e_inarg ina && not tcgen &&

664− not (e_guarded ina))) $

675+ not (e_guarded ina))) $

665− mapM_ (\n -> do focus n

676+ mapM_ (\n -> do focus n

666− g <- goal

677+ g <- goal

667− env <- get_env

678+ env <- get_env

668− hs <- get_holes

679+ hs <- get_holes

669− if all (\n -> not (n `elem` hs)) (freeNames g)

680+ if all (\n -> not (n `elem` hs)) (freeNames g)

670− then try (resolveTC False 7 g fn ist)

681+ then try (resolveTC False 7 g fn ist)

671− (movelast n)

682+ (movelast n)

672− else movelast n)

683+ else movelast n)

673− (ivs' \\ ivs)

684+ (ivs' \\ ivs)

685+ return []

686+ where

687+ -- Run the elaborator, which returns how many implicit

688+ -- args were needed, then run it again with those args. We need

689+ -- this because we have to elaborate the whole application to

690+ -- find out whether any computations have caused more implicits

691+ -- to be needed.

692+ implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

693+ implicitApp elab

694+ | pattern = do elab; return ()

695+ | otherwise

696+ = do s <- get

697+ imps <- elab

698+ case imps of

699+ [] -> return ()

700+ es -> do put s

701+ elab' ina topfc (PAppImpl tm es)

702+

703+ getReqImps (Bind x (Pi (Just i) ty _) sc)

704+ = i : getReqImps sc

705+ getReqImps _ = []

706+

674− where -- normal < alternatives < lambdas < rewrites < tactic < default tactic

707+ -- normal < alternatives < lambdas < rewrites < tactic < default tactic

675 -- reason for lambdas after alternatives is that having

708 -- reason for lambdas after alternatives is that having

676 -- the alternative resolved can help with typechecking the lambda

709 -- the alternative resolved can help with typechecking the lambda

677 -- or the rewrite. Rewrites/tactics need as much information

710 -- or the rewrite. Rewrites/tactics need as much information

@@ -744,15 +777,24 @@ elab ist info emode opts fn tm

744 setInjective (PApp _ (PRef _ n) _) = setinj n

777 setInjective (PApp _ (PRef _ n) _) = setinj n

745 setInjective _ = return ()

778 setInjective _ = return ()

746

779

747− elab' ina _ tm@(PApp fc f [arg])

780+ elab' ina _ tm@(PApp fc f [arg]) =

748− = erun fc $

781+ erun fc $

749 do simple_app (not $ headRef f)

782 do simple_app (not $ headRef f)

783+ (elabE (ina { e_isfn = True }) (Just fc) f)

750− (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

784+ (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

751 (show tm)

785 (show tm)

752 solve

786 solve

753 where headRef (PRef _ _) = True

787 where headRef (PRef _ _) = True

754 headRef (PApp _ f _) = headRef f

788 headRef (PApp _ f _) = headRef f

755 headRef _ = False

789 headRef _ = False

790+

791+ elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

792+ solve

793+ where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits

794+ appImpl (e : es) = simple_app False

795+ (appImpl es)

796+ (elab' ina fc Placeholder)

797+ (show f)

756 elab' ina fc Placeholder

798 elab' ina fc Placeholder

757 = do (h : hs) <- get_holes

799 = do (h : hs) <- get_holes

758 movelast h

800 movelast h

@@ -1072,16 +1114,20 @@ elab ist info emode opts fn tm

1072 = x : insertScopedImps fc sc xs

1114 = x : insertScopedImps fc sc xs

1073 insertScopedImps _ _ xs = xs

1115 insertScopedImps _ _ xs = xs

1074

1116

1075− insertImpLam t =

1117+ insertImpLam ina t =

1076 do ty <- goal

1118 do ty <- goal

1077 env <- get_env

1119 env <- get_env

1078 let ty' = normalise (tt_ctxt ist) env ty

1120 let ty' = normalise (tt_ctxt ist) env ty

1079 addLam ty' t

1121 addLam ty' t

1080 where

1122 where

1081 -- just one level at a time

1123 -- just one level at a time

1082− addLam (Bind n (Pi (Just _) _ _) sc) t

1124+ addLam (Bind n (Pi (Just _) _ _) sc) t =

1083− = do impn <- unique_hole (sMN 0 "imp")

1125+ do impn <- unique_hole (sMN 0 "imp")

1126+ if e_isfn ina -- apply to an implicit immediately

1127+ then return (PApp emptyFC

1128+ (PLam emptyFC impn Placeholder t)

1129+ [pexp Placeholder])

1084− return (PLam emptyFC impn Placeholder t)

1130+ else return (PLam emptyFC impn Placeholder t)

1085 addLam _ t = return t

1131 addLam _ t = return t

1086

1132

1087 insertCoerce ina t@(PCase _ _ _) = return t

1133 insertCoerce ina t@(PCase _ _ _) = return t

src/Idris/IBC.hs+1

@@ -1482,6 +1482,7 @@ instance Binary PTerm where

1482 PTyped x1 x2 -> do putWord8 7

1483 put x1

1484 put x2

1485+ PAppImpl x1 x2 -> error "PAppImpl in final term"

1485 PApp x1 x2 x3 -> do putWord8 8

1486 PApp x1 x2 x3 -> do putWord8 8

1486 put x1

1487 put x1

1487 put x2

1488 put x2

test/reg058/expectednew file

No changes to the content.

test/reg058/implicits.idrnew file+14

@@ -0,0 +1,14 @@

1+%default total

3+InterpBool : () -> Type

4+InterpBool () = {x : Type} -> x -> Nat

6+class IdrisBug (u : ()) where

7+ idrisBug : InterpBool u

9+instance IdrisBug () where

10+ idrisBug _ = Z

11+

12+f : Nat

13+f = idrisBug {u = ()} 'a'

14+

test/reg058/implicits2.idrnew file+19

@@ -0,0 +1,19 @@

1+import Data.Vect

3+impTy : Bool -> Type

4+impTy True = Int

5+impTy False = {n : Nat} -> Vect n Int -> Vect n Int

7+wibble : impTy False

8+wibble [] = []

9+wibble (x :: xs) = x * 2 :: wibble xs

10+

11+wobble : (b : Bool) -> impTy b

12+wobble True = 42

13+wobble False = wibble

14+

15+foo : Vect 4 Int

16+foo = wobble False [1,2,3,4]

17+

18+bar : Int

19+bar = wobble True

test/reg058/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+idris $@ implicits.idr --check

3+idris $@ implicits2.idr --check

5+rm -f *.ibc