60f3916 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1492 from edwinb/unique

Uniqueness fixes

commit60f39169fa790544dd577d78bf2d03ddb29841c6 authorEdwin Brady <edwin.brady@gmail.com> dateTue 26 Aug 2014, 12:15 (12 years ago) parent008cdb6 d3660ed

4 files changed+65−6

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+20−1 src/Idris/Elab/Utils.hs+31 src/Idris/ElabTerm.hs+11−2 test/unique002/unique002.idr+3−3

src/Idris/Elab/Clause.hs+20−1

@@ -442,6 +442,18 @@ propagateParams i ps t (PRef fc n)

442442 isImplicit (_ : is) n = isImplicit is n

443443propagateParams i ps t x = x

444444

445+findUnique :: Context -> Env -> Term -> [Name]

446+findUnique ctxt env (Bind n b sc)

447+ = let rawTy = forgetEnv (map fst env) (binderTy b)

448+ uniq = case check ctxt env rawTy of

449+ OK (_, UType UniqueType) -> True

450+ OK (_, UType NullType) -> True

451+ OK (_, UType AllTypes) -> True

452+ _ -> False in

453+ if uniq then n : findUnique ctxt ((n, b) : env) sc

454+ else findUnique ctxt ((n, b) : env) sc

455+findUnique _ _ _ = []

456+

445457-- Return the elaborated LHS/RHS, and the original LHS with implicits added

446458elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

447459 Idris (Either Term (Term, Term), PTerm)

@@ -520,7 +532,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

520532 windex <- getName

521533 let decls = nub (concatMap declared whereblock)

522534 let defs = nub (decls ++ concatMap defined whereblock)

523− let newargs = pvars ist lhs_tm

535+ let newargs_all = pvars ist lhs_tm

536+

537+ -- Unique arguments must be passed to the where block explicitly

538+ -- (since we can't control "usage" easlily otherwise). Remove them

539+ -- from newargs here

540+ let uniqargs = findUnique (tt_ctxt ist) [] lhs_tm

541+ let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all

542+

524543 let winfo = pinfo info newargs defs windex

525544 let wb = map (expandParamsD False ist decorate newargs defs) whereblock

526545

src/Idris/Elab/Utils.hs+31

@@ -13,6 +13,7 @@ import Idris.Core.Evaluate

1313import Idris.Core.Typecheck

1414

1515import Control.Applicative hiding (Const)

16+import Control.Monad.State

1617import Control.Monad

1718import Data.List

1819

@@ -205,3 +206,33 @@ paramNames args env (p : ps)

205206 else paramNames args env ps

206207 _ -> paramNames args env ps

207208 | otherwise = paramNames args env ps

209+

210+getUniqueUsed :: Context -> Term -> [Name]

211+getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

212+ where

213+ getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

214+ getUniq env us (Bind n b sc)

215+ = let uniq = case check ctxt env (forgetEnv (map fst env) (binderTy b)) of

216+ OK (_, UType UniqueType) -> True

217+ OK (_, UType NullType) -> True

218+ OK (_, UType AllTypes) -> True

219+ _ -> False in

220+ do getUniqB env us b

221+ getUniq ((n,b):env) ((n, uniq):us) sc

222+ getUniq env us (App f a) = do getUniq env us f; getUniq env us a

223+ getUniq env us (V i)

224+ | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

225+ getUniq env us (P _ n _)

226+ | Just u <- lookup n us = if u then use n else return ()

227+ getUniq env us _ = return ()

228+

229+ use n = do ns <- get; put (n : ns)

230+

231+ getUniqB env us (Let t v) = do getUniq env us t; getUniq env us v

232+ getUniqB env us (Guess t v) = do getUniq env us t; getUniq env us v

233+ getUniqB env us (Pi t v) = do getUniq env us t; getUniq env us v

234+ getUniqB env us (NLet t v) = do getUniq env us t; getUniq env us v

235+ getUniqB env us b = getUniq env us (binderTy b)

236+

237+

238+

src/Idris/ElabTerm.hs+11−2

@@ -17,6 +17,7 @@ import Idris.Core.Unify

1717import Idris.Core.Typecheck (check, recheck)

1818import Idris.ErrReverse (errReverse)

1919import Idris.ElabQuasiquote (extractUnquotes)

20+import Idris.Elab.Utils

2021import qualified Util.Pretty as U

2122

2223import Control.Applicative ((<$>))

@@ -629,8 +630,16 @@ elab ist info emode opts fn tm

629630 solve

630631 elab' ina Placeholder = do (h : hs) <- get_holes

631632 movelast h

632− elab' ina (PMetavar n) = let n' = mkN n in

633− do attack; defer [] n'; solve

633+ elab' ina (PMetavar n) =

634+ do ptm <- get_term

635+ -- When building the metavar application, leave out the unique

636+ -- names which have been used elsewhere in the term, since we

637+ -- won't be able to use them in the resulting application.

638+ let unique_used = getUniqueUsed (tt_ctxt ist) ptm

639+ let n' = mkN n

640+ attack

641+ defer unique_used n'

642+ solve

634643 where mkN n@(NS _ _) = n

635644 mkN n = case namespace info of

636645 Just xs@(_:_) -> sNS n xs

test/unique002/unique002.idr+3−3

@@ -14,7 +14,7 @@ showU xs = "[" ++ showU' xs ++ "]" where

1414foo : UList Int -> IO ()

1515foo xs = do -- let f = \x : Int => showU xs

1616 putStrLn $ free xs

17− putStrLn $ f 42

17+ putStrLn $ f 42 xs

1818 return ()

19− where f : Int -> String

20− f x = showU xs

19+ where f : Int -> Borrowed (UList Int) -> String

20+ f x xs = showU xs