d7b2913 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A simpler approach to handling name shadowing

It's hard to get right, so there's no need to be clever (indeed there's a need not to be clever). So just before elaboration (while adding implicits and resolving global names) we traverse a term and rename any binder which has already been used, inventing a unique name which is not used anywhere else in the term.

commitd7b2913e339fb689ecfb70e04466a69b76d5f977 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 18 Jan 2014, 18:13 (13 years ago) parentd711327

5 files changed+110−18

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+84−3 src/Idris/AbsSyntaxTree.hs+23−1 src/Idris/Core/Elaborate.hs+1−8 src/Idris/DSL.hs+1−1 src/Idris/ElabTerm.hs+1−5

src/Idris/AbsSyntax.hs+84−3

@@ -1195,7 +1195,8 @@ addImpl = addImpl' False [] []

11951195-- and *not* inside a PHidden

11961196

11971197addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1198−addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) [] ptm

1198+addImpl' inpat env infns ist ptm

1199+ = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)

11991200 where

12001201 ai env ds (PRef fc f)

12011202 | f `elem` infns = PInferRef fc f

@@ -1624,9 +1625,11 @@ substMatchShadow n shs tm t = sm shs t where

16241625shadow :: Name -> Name -> PTerm -> PTerm

16251626shadow n n' t = sm t where

16261627 sm (PRef fc x) | n == x = PRef fc n'

1627− sm (PLam x t sc) = PLam x (sm t) (sm sc)

1628− sm (PPi p x t sc) = PPi p x (sm t) (sm sc)

1628+ sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)

1629+ sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)

1630+ sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)

16291631 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1632+ sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

16301633 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

16311634 sm (PEq f x y) = PEq f (sm x) (sm y)

16321635 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

@@ -1634,9 +1637,87 @@ shadow n n' t = sm t where

16341637 sm (PPair f x y) = PPair f (sm x) (sm y)

16351638 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

16361639 sm (PAlternative a as) = PAlternative a (map sm as)

1640+ sm (PTactics ts) = PTactics (map (fmap sm) ts)

1641+ sm (PProof ts) = PProof (map (fmap sm) ts)

16371642 sm (PHidden x) = PHidden (sm x)

16381643 sm (PUnifyLog x) = PUnifyLog (sm x)

16391644 sm (PNoImplicits x) = PNoImplicits (sm x)

16401645 sm x = x

16411646

1647+-- Rename any binders which are repeated (so that we don't have to mess

1648+-- about with shadowing anywhere else).

1649+

1650+mkUniqueNames :: [Name] -> PTerm -> PTerm

1651+mkUniqueNames env tm = evalState (mkUniq tm) env where

1652+ inScope = boundNamesIn tm

1653+

1654+ mkUniqA arg = do t' <- mkUniq (getTm arg)

1655+ return (arg { getTm = t' })

1656+

1657+ -- FIXME: Probably ought to do this for completeness! It's fine as

1658+ -- long as there are no bindings inside tactics though.

1659+ mkUniqT tac = return tac

1660+

1661+ mkUniq :: PTerm -> State [Name] PTerm

1662+ mkUniq (PLam n ty sc)

1663+ = do env <- get

1664+ (n', sc') <-

1665+ if n `elem` env

1666+ then do let n' = uniqueName n (env ++ inScope)

1667+ return (n', shadow n n' sc)

1668+ else return (n, sc)

1669+ put (n' : env)

1670+ ty' <- mkUniq ty

1671+ sc'' <- mkUniq sc'

1672+ return $! PLam n' ty' sc''

1673+ mkUniq (PPi p n ty sc)

1674+ = do env <- get

1675+ (n', sc') <-

1676+ if n `elem` env

1677+ then do let n' = uniqueName n (env ++ inScope)

1678+ return (n', shadow n n' sc)

1679+ else return (n, sc)

1680+ put (n' : env)

1681+ ty' <- mkUniq ty

1682+ sc'' <- mkUniq sc'

1683+ return $! PPi p n' ty' sc''

1684+ mkUniq (PLet n ty val sc)

1685+ = do env <- get

1686+ (n', sc') <-

1687+ if n `elem` env

1688+ then do let n' = uniqueName n (env ++ inScope)

1689+ return (n', shadow n n' sc)

1690+ else return (n, sc)

1691+ put (n' : env)

1692+ ty' <- mkUniq ty; val' <- mkUniq val

1693+ sc'' <- mkUniq sc'

1694+ return $! PLet n' ty' val' sc''

1695+ mkUniq (PApp fc t args)

1696+ = do t' <- mkUniq t

1697+ args' <- mapM mkUniqA args

1698+ return $! PApp fc t' args'

1699+ mkUniq (PAppBind fc t args)

1700+ = do t' <- mkUniq t

1701+ args' <- mapM mkUniqA args

1702+ return $! PAppBind fc t' args'

1703+ mkUniq (PCase fc t alts)

1704+ = do t' <- mkUniq t

1705+ alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y

1706+ return (x', y')) alts

1707+ return $! PCase fc t' alts'

1708+ mkUniq (PPair fc l r)

1709+ = do l' <- mkUniq l; r' <- mkUniq r

1710+ return $! PPair fc l' r'

1711+ mkUniq (PDPair fc l t r)

1712+ = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r

1713+ return $! PDPair fc l' t' r'

1714+ mkUniq (PAlternative b as)

1715+ = liftM (PAlternative b) (mapM mkUniq as)

1716+ mkUniq (PHidden t) = liftM PHidden (mkUniq t)

1717+ mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)

1718+ mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)

1719+ mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

1720+ mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

1721+ mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

1722+ mkUniq t = return t

16421723

src/Idris/AbsSyntaxTree.hs+23−1

@@ -1415,8 +1415,30 @@ allNamesIn tm = nub $ ni [] tm

14151415 ni env (PNoImplicits tm) = ni env tm

14161416 ni env _ = []

14171417

1418−-- Return names which are free in the given term.

1418+-- Return all names defined in binders in the given term

1419+boundNamesIn :: PTerm -> [Name]

1420+boundNamesIn tm = nub $ ni tm

1421+ where

1422+ ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

1423+ ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

1424+ ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

1425+ ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1426+ ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1427+ ni (PPi _ n ty sc) = n : (ni ty ++ ni sc)

1428+ ni (PEq _ l r) = ni l ++ ni r

1429+ ni (PRewrite _ l r _) = ni l ++ ni r

1430+ ni (PTyped l r) = ni l ++ ni r

1431+ ni (PPair _ l r) = ni l ++ ni r

1432+ ni (PDPair _ (PRef _ n) t r) = ni t ++ ni r

1433+ ni (PDPair _ l t r) = ni l ++ ni t ++ ni r

1434+ ni (PAlternative a as) = concatMap (ni) as

1435+ ni (PHidden tm) = ni tm

1436+ ni (PUnifyLog tm) = ni tm

1437+ ni (PDisamb _ tm) = ni tm

1438+ ni (PNoImplicits tm) = ni tm

1439+ ni _ = []

14191440

1441+-- Return names which are free in the given term.

14201442namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

14211443namesIn uvars ist tm = nub $ ni [] tm

14221444 where

src/Idris/Core/Elaborate.hs+1−8

@@ -244,14 +244,7 @@ unique_hole' reusable n

244244 let bs = bound_in (pterm (fst p)) ++

245245 bound_in (ptype (fst p))

246246 let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)

247− n' <-

248−-- case lookupTy n (context (fst p)) of

249−-- [] -> if not (n `elem` holes (fst p) ++

250−-- bs ++ dontunify (fst p) ++ usedns (fst p))

251−-- then return n

252−-- else getNameFrom n

253−-- _ -> getNameFrom n

254− return $! uniqueNameCtxt (context (fst p)) n nouse

247+ n' <- return $! uniqueNameCtxt (context (fst p)) n nouse

255248 ES (p, a) s u <- get

256249 case n' of

257250 MN i _ -> when (i >= nextname p) $

src/Idris/DSL.hs+1−1

@@ -132,7 +132,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

132132 db' (PAppBind fc t args)

133133 = do args' <- dbs args

134134 (bs, n) <- get

135− let nm = sMN n ("bindApp" ++ show n)

135+ let nm = sUN ("_bindApp" ++ show n)

136136 put ((nm, fc, PApp fc t args') : bs, n+1)

137137 return (PRef fc nm)

138138 db' (PApp fc t args)

src/Idris/ElabTerm.hs+1−5

@@ -261,16 +261,12 @@ elab ist info pattern opts fn tm

261261 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

262262 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

263263 elab' ina@(_, a, inty) (PLam n Placeholder sc)

264− = do -- n' <- unique_hole n

265− -- let sc' = mapPT (repN n n') sc

266− ptm <- get_term

264+ = do ptm <- get_term

267265 g <- goal

268266 checkPiGoal n

269267 attack; intro (Just n);

270268 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

271269 elabE (True, a, inty) sc; solve

272− where repN n n' (PRef fc x) | x == n' = PRef fc n'

273− repN _ _ t = t

274270 elab' ina@(_, a, inty) (PLam n ty sc)

275271 = do hsin <- get_holes

276272 ptmin <- get_term