6d7d3bd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2630 from david-christiansen/namesInQQ

6d7d3bdDavid Christiansen11 years ago

src/Idris/AbsSyntax.hs+82−67

compare with master

unifiedsplit

@@ -31,6 +31,8 @@ import Data.Maybe

31import qualified Data.Set as S

32import Data.Word (Word)

34+import Data.Generics.Uniplate.Data (descend, descendM)

35+

34import Debug.Trace

36import Debug.Trace

36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

38import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

@@ -2114,44 +2116,46 @@ substMatchShadow n shs tm t = sm shs t where

2114 fullApp x = x

2116 fullApp x = x

2115

2117

2116shadow :: Name -> Name -> PTerm -> PTerm

2118shadow :: Name -> Name -> PTerm -> PTerm

2117−shadow n n' t = sm t where

2119+shadow n n' t = sm 0 t where

2118− sm (PRef fc hl x) | n == x = PRef fc hl n'

2120+ sm 0 (PRef fc hl x) | n == x = PRef fc hl n'

2119− sm (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm t) (sm sc)

2121+ sm 0 (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm 0 t) (sm 0 sc)

2120− | otherwise = PLam fc x xfc (sm t) sc

2122+ | otherwise = PLam fc x xfc (sm 0 t) sc

2121− sm (PPi p x fc t sc) | n /= x = PPi p x fc (sm t) (sm sc)

2123+ sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)

2122− | otherwise = PPi p x fc (sm t) sc

2124+ | otherwise = PPi p x fc (sm 0 t) sc

2123− sm (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm t) (sm v) (sm sc)

2125+ sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)

2124− | otherwise = PLet fc x xfc (sm t) (sm v) sc

2126+ | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc

2125− sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

2127+ sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)

2126− sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

2128+ sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)

2127− sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

2129+ sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)

2128− sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)

2130+ sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)

2129− sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

2131+ sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)

2130− sm (PTyped x y) = PTyped (sm x) (sm y)

2132+ sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)

2131− sm (PPair f hls p x y) = PPair f hls p (sm x) (sm y)

2133+ sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)

2132− sm (PDPair f hls p x t y) = PDPair f hls p (sm x) (sm t) (sm y)

2134+ sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)

2133− sm (PAlternative ms a as) = PAlternative ms a (map sm as)

2135+ sm 0 (PAlternative ms a as) = PAlternative ms a (map (sm 0) as)

2134− sm (PTactics ts) = PTactics (map (fmap sm) ts)

2136+ sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)

2135− sm (PProof ts) = PProof (map (fmap sm) ts)

2137+ sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)

2136− sm (PHidden x) = PHidden (sm x)

2138+ sm 0 (PHidden x) = PHidden (sm 0 x)

2137− sm (PUnifyLog x) = PUnifyLog (sm x)

2139+ sm 0 (PUnifyLog x) = PUnifyLog (sm 0 x)

2138− sm (PNoImplicits x) = PNoImplicits (sm x)

2140+ sm 0 (PNoImplicits x) = PNoImplicits (sm 0 x)

2139− sm (PCoerced t) = PCoerced (sm t)

2141+ sm 0 (PCoerced t) = PCoerced (sm 0 t)

2140− sm x = x

2142+ sm ql (PQuasiquote tm ty) = PQuasiquote (sm (ql + 1) tm) (fmap (sm ql) ty)

2143+ sm ql (PUnquote tm) = PUnquote (sm (ql - 1) tm)

2144+ sm ql x = descend (sm ql) x

2141

2145

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

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

2143-- about with shadowing anywhere else).

2147-- about with shadowing anywhere else).

2144mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2148mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2145mkUniqueNames env shadows tm

2149mkUniqueNames env shadows tm

2146− = evalState (mkUniq initMap tm) (S.fromList env) where

2150+ = evalState (mkUniq 0 initMap tm) (S.fromList env) where

2147

2151

2148 initMap = M.fromList shadows

2152 initMap = M.fromList shadows

2149

2153

2150 inScope :: S.Set Name

2154 inScope :: S.Set Name

2151 inScope = S.fromList $ boundNamesIn tm

2155 inScope = S.fromList $ boundNamesIn tm

2152

2156

2153− mkUniqA nmap arg = do t' <- mkUniq nmap (getTm arg)

2157+ mkUniqA ql nmap arg = do t' <- mkUniq ql nmap (getTm arg)

2154− return (arg { getTm = t' })

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

2155

2159

2156 -- Initialise the unique name with the environment length (so we're not

2160 -- Initialise the unique name with the environment length (so we're not

2157 -- looking for too long...)

2161 -- looking for too long...)

@@ -2161,10 +2165,11 @@ mkUniqueNames env shadows tm

2161

2165

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

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

2163 -- long as there are no bindings inside tactics though.

2167 -- long as there are no bindings inside tactics though.

2164− mkUniqT nmap tac = return tac

2168+ mkUniqT _ nmap tac = return tac

2165

2169

2170+ mkUniq :: Int -- ^ The number of quotations that we're under

2166− mkUniq :: M.Map Name Name -> PTerm -> State (S.Set Name) PTerm

2171+ -> M.Map Name Name -> PTerm -> State (S.Set Name) PTerm

2167− mkUniq nmap (PLam fc n nfc ty sc)

2172+ mkUniq 0 nmap (PLam fc n nfc ty sc)

2168 = do env <- get

2173 = do env <- get

2169 (n', sc') <-

2174 (n', sc') <-

2170 if n `S.member` env

2175 if n `S.member` env

@@ -2174,10 +2179,10 @@ mkUniqueNames env shadows tm

2174 else return (n, sc)

2179 else return (n, sc)

2175 put (S.insert n' env)

2180 put (S.insert n' env)

2176 let nmap' = M.insert n n' nmap

2181 let nmap' = M.insert n n' nmap

2177− ty' <- mkUniq nmap ty

2182+ ty' <- mkUniq 0 nmap ty

2178− sc'' <- mkUniq nmap' sc'

2183+ sc'' <- mkUniq 0 nmap' sc'

2179 return $! PLam fc n' nfc ty' sc''

2184 return $! PLam fc n' nfc ty' sc''

2180− mkUniq nmap (PPi p n fc ty sc)

2185+ mkUniq 0 nmap (PPi p n fc ty sc)

2181 = do env <- get

2186 = do env <- get

2182 (n', sc') <-

2187 (n', sc') <-

2183 if n `S.member` env

2188 if n `S.member` env

@@ -2187,10 +2192,10 @@ mkUniqueNames env shadows tm

2187 else return (n, sc)

2192 else return (n, sc)

2188 put (S.insert n' env)

2193 put (S.insert n' env)

2189 let nmap' = M.insert n n' nmap

2194 let nmap' = M.insert n n' nmap

2190− ty' <- mkUniq nmap ty

2195+ ty' <- mkUniq 0 nmap ty

2191− sc'' <- mkUniq nmap' sc'

2196+ sc'' <- mkUniq 0 nmap' sc'

2192 return $! PPi p n' fc ty' sc''

2197 return $! PPi p n' fc ty' sc''

2193− mkUniq nmap (PLet fc n nfc ty val sc)

2198+ mkUniq 0 nmap (PLet fc n nfc ty val sc)

2194 = do env <- get

2199 = do env <- get

2195 (n', sc') <-

2200 (n', sc') <-

2196 if n `S.member` env

2201 if n `S.member` env

@@ -2200,28 +2205,28 @@ mkUniqueNames env shadows tm

2200 else return (n, sc)

2205 else return (n, sc)

2201 put (S.insert n' env)

2206 put (S.insert n' env)

2202 let nmap' = M.insert n n' nmap

2207 let nmap' = M.insert n n' nmap

2203− ty' <- mkUniq nmap ty; val' <- mkUniq nmap val

2208+ ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val

2204− sc'' <- mkUniq nmap' sc'

2209+ sc'' <- mkUniq 0 nmap' sc'

2205 return $! PLet fc n' nfc ty' val' sc''

2210 return $! PLet fc n' nfc ty' val' sc''

2206− mkUniq nmap (PApp fc t args)

2211+ mkUniq 0 nmap (PApp fc t args)

2207− = do t' <- mkUniq nmap t

2212+ = do t' <- mkUniq 0 nmap t

2208− args' <- mapM (mkUniqA nmap) args

2213+ args' <- mapM (mkUniqA 0 nmap) args

2209 return $! PApp fc t' args'

2214 return $! PApp fc t' args'

2210− mkUniq nmap (PAppBind fc t args)

2215+ mkUniq 0 nmap (PAppBind fc t args)

2211− = do t' <- mkUniq nmap t

2216+ = do t' <- mkUniq 0 nmap t

2212− args' <- mapM (mkUniqA nmap) args

2217+ args' <- mapM (mkUniqA 0 nmap) args

2213 return $! PAppBind fc t' args'

2218 return $! PAppBind fc t' args'

2214− mkUniq nmap (PCase fc t alts)

2219+ mkUniq 0 nmap (PCase fc t alts)

2215− = do t' <- mkUniq nmap t

2220+ = do t' <- mkUniq 0 nmap t

2216− alts' <- mapM (\(x,y)-> do x' <- mkUniq nmap x; y' <- mkUniq nmap y

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

2217 return (x', y')) alts

2222 return (x', y')) alts

2218 return $! PCase fc t' alts'

2223 return $! PCase fc t' alts'

2219− mkUniq nmap (PIfThenElse fc c t f)

2224+ mkUniq 0 nmap (PIfThenElse fc c t f)

2220− = liftM3 (PIfThenElse fc) (mkUniq nmap c) (mkUniq nmap t) (mkUniq nmap f)

2225+ = liftM3 (PIfThenElse fc) (mkUniq 0 nmap c) (mkUniq 0 nmap t) (mkUniq 0 nmap f)

2221− mkUniq nmap (PPair fc hls p l r)

2226+ mkUniq 0 nmap (PPair fc hls p l r)

2222− = do l' <- mkUniq nmap l; r' <- mkUniq nmap r

2227+ = do l' <- mkUniq 0 nmap l; r' <- mkUniq 0 nmap r

2223 return $! PPair fc hls p l' r'

2228 return $! PPair fc hls p l' r'

2224− mkUniq nmap (PDPair fc hls p (PRef fc' hls' n) t sc)

2229+ mkUniq 0 nmap (PDPair fc hls p (PRef fc' hls' n) t sc)

2225 | t /= Placeholder

2230 | t /= Placeholder

2226 = do env <- get

2231 = do env <- get

2227 (n', sc') <- if n `S.member` env

2232 (n', sc') <- if n `S.member` env

@@ -2230,27 +2235,37 @@ mkUniqueNames env shadows tm

2230 else return (n, sc)

2235 else return (n, sc)

2231 put (S.insert n' env)

2236 put (S.insert n' env)

2232 let nmap' = M.insert n n' nmap

2237 let nmap' = M.insert n n' nmap

2233− t' <- mkUniq nmap t

2238+ t' <- mkUniq 0 nmap t

2234− sc'' <- mkUniq nmap' sc'

2239+ sc'' <- mkUniq 0 nmap' sc'

2235 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2240 return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2236− mkUniq nmap (PDPair fc hls p l t r)

2241+ mkUniq 0 nmap (PDPair fc hls p l t r)

2237− = do l' <- mkUniq nmap l; t' <- mkUniq nmap t; r' <- mkUniq nmap r

2242+ = do l' <- mkUniq 0 nmap l; t' <- mkUniq 0 nmap t; r' <- mkUniq 0 nmap r

2238 return $! PDPair fc hls p l' t' r'

2243 return $! PDPair fc hls p l' t' r'

2239− mkUniq nmap (PAlternative ns b as)

2244+ mkUniq 0 nmap (PAlternative ns b as)

2240 -- store the nmap and defer the rest until we've pruned the set

2245 -- store the nmap and defer the rest until we've pruned the set

2241 -- during elaboration

2246 -- during elaboration

2242 = return $ PAlternative (M.toList nmap ++ ns) b as

2247 = return $ PAlternative (M.toList nmap ++ ns) b as

2243− mkUniq nmap (PHidden t) = liftM PHidden (mkUniq nmap t)

2248+ mkUniq 0 nmap (PHidden t) = liftM PHidden (mkUniq 0 nmap t)

2244− mkUniq nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq nmap t)

2249+ mkUniq 0 nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq 0 nmap t)

2245− mkUniq nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq nmap t)

2250+ mkUniq 0 nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq 0 nmap t)

2246− mkUniq nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq nmap t)

2251+ mkUniq 0 nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq 0 nmap t)

2247− mkUniq nmap (PProof ts) = liftM PProof (mapM (mkUniqT nmap) ts)

2252+ mkUniq 0 nmap (PProof ts) = liftM PProof (mapM (mkUniqT 0 nmap) ts)

2248− mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)

2253+ mkUniq 0 nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT 0 nmap) ts)

2249− mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)

2254+ mkUniq 0 nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq 0 nmap ts)

2250− mkUniq nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq nmap tm)

2255+ mkUniq 0 nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq 0 nmap tm)

2251− mkUniq nmap (PCoerced tm) = liftM PCoerced (mkUniq nmap tm)

2256+ mkUniq 0 nmap (PCoerced tm) = liftM PCoerced (mkUniq 0 nmap tm)

2252− mkUniq nmap t = return $ shadowAll (M.toList nmap) t

2257+ mkUniq 0 nmap t = return $ shadowAll (M.toList nmap) t

2253 where

2258 where

2254 shadowAll [] t = t

2259 shadowAll [] t = t

2255 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2260 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2256

2261

2262+ mkUniq ql nmap (PQuasiquote tm ty) =

2263+ do tm' <- mkUniq (ql + 1) nmap tm

2264+ ty' <- case ty of

2265+ Nothing -> return Nothing

2266+ Just t -> fmap Just $ mkUniq ql nmap t

2267+ return $! PQuasiquote tm' ty'

2268+ mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)

2269+

2270+ mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2271+

src/Idris/AbsSyntaxTree.hs+144−121

@@ -28,7 +28,7 @@ import qualified Control.Monad.Trans.Class as Trans (lift)

29import Data.Data (Data)

30import Data.Function (on)

31−import Data.Generics.Uniplate.Data (universe)

31+import Data.Generics.Uniplate.Data (universe, children)

32import Data.List hiding (group)

33import Data.Char

34import qualified Data.Map.Strict as M

@@ -2177,160 +2177,183 @@ getPArity _ = 0

2177-- Return all names, free or globally bound, in the given term.

2178

2179allNamesIn :: PTerm -> [Name]

2180−allNamesIn tm = nub $ ni [] tm

2180+allNamesIn tm = nub $ ni 0 [] tm

2181 where -- TODO THINK added niTacImp, but is it right?

2182− ni env (PRef _ _ n)

2182+ ni 0 env (PRef _ _ n)

2183 | not (n `elem` env) = [n]

2184− ni env (PPatvar _ n) = [n]

2184+ ni 0 env (PPatvar _ n) = [n]

2185− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2185+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2186− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2186+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2187− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

2187+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)

2188− ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f

2188+ ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f

2189− ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

2189+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2190− ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2190+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2191− ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc

2191+ ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

2192− ni env (PHidden tm) = ni env tm

2192+ ni 0 env (PHidden tm) = ni 0 env tm

2193− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2193+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2194− ni env (PTyped l r) = ni env l ++ ni env r

2194+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2195− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2195+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2196− ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r

2196+ ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r

2197− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2197+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2198− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2198+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2199− ni env (PAlternative ns a ls) = concatMap (ni env) ls

2199+ ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls

2200− ni env (PUnifyLog tm) = ni env tm

2200+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2201− ni env (PDisamb _ tm) = ni env tm

2201+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2202− ni env (PNoImplicits tm) = ni env tm

2202+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2203− ni env _ = []

2203+

2204−

2204+ ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty

2205+ ni i env (PUnquote tm) = ni (i - 1) env tm

2206+

2207+ ni i env tm = concatMap (ni i env) (children tm)

2208+

2205− niTacImp env (TacImp _ _ scr) = ni env scr

2209+ niTacImp i env (TacImp _ _ scr) = ni i env scr

2206− niTacImp _ _ = []

2210+ niTacImp _ _ _ = []

2207

2211

2208

2212

2209-- Return all names defined in binders in the given term

2213-- Return all names defined in binders in the given term

2210boundNamesIn :: PTerm -> [Name]

2214boundNamesIn :: PTerm -> [Name]

2211−boundNamesIn tm = S.toList (ni S.empty tm)

2215+boundNamesIn tm = S.toList (ni 0 S.empty tm)

2212 where -- TODO THINK Added niTacImp, but is it right?

2216 where -- TODO THINK Added niTacImp, but is it right?

2217+ ni :: Int -> S.Set Name -> PTerm -> S.Set Name

2213− ni set (PApp _ f as) = niTms (ni set f) (map getTm as)

2218+ ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)

2214− ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)

2219+ ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)

2215− ni set (PCase _ c os) = niTms (ni set c) (map snd os)

2220+ ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)

2216− ni set (PIfThenElse _ c t f) = niTms set [c, t, f]

2221+ ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]

2217− ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc

2222+ ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc

2218− ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

2223+ ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc

2219− ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

2224+ ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p

2220− ni set (PRewrite _ l r _) = ni (ni set l) r

2225+ ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r

2221− ni set (PTyped l r) = ni (ni set l) r

2226+ ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r

2222− ni set (PPair _ _ _ l r) = ni (ni set l) r

2227+ ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r

2223− ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r

2228+ ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r

2224− ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r

2229+ ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r

2225− ni set (PAlternative ns a as) = niTms set as

2230+ ni 0 set (PAlternative ns a as) = niTms 0 set as

2226− ni set (PHidden tm) = ni set tm

2231+ ni 0 set (PHidden tm) = ni 0 set tm

2227− ni set (PUnifyLog tm) = ni set tm

2232+ ni 0 set (PUnifyLog tm) = ni 0 set tm

2228− ni set (PDisamb _ tm) = ni set tm

2233+ ni 0 set (PDisamb _ tm) = ni 0 set tm

2229− ni set (PNoImplicits tm) = ni set tm

2234+ ni 0 set (PNoImplicits tm) = ni 0 set tm

2230− ni set _ = set

2235+

2231−

2236+ ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty

2237+ ni i set (PUnquote tm) = ni (i - 1) set tm

2238+

2239+ ni i set tm = foldr S.union set (map (ni i set) (children tm))

2240+

2241+ niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name

2232− niTms set [] = set

2242+ niTms i set [] = set

2233− niTms set (x : xs) = niTms (ni set x) xs

2243+ niTms i set (x : xs) = niTms i (ni i set x) xs

2234−

2244+

2235− niTacImp set (TacImp _ _ scr) = ni set scr

2245+ niTacImp i set (TacImp _ _ scr) = ni i set scr

2236− niTacImp set _ = set

2246+ niTacImp i set _ = set

2237

2247

2238-- Return names which are valid implicits in the given term (type).

2248-- Return names which are valid implicits in the given term (type).

2239implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2249implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2240−implicitNamesIn uvars ist tm = nub $ ni [] tm

2250+implicitNamesIn uvars ist tm = nub $ ni 0 [] tm

2241 where

2251 where

2242− ni env (PRef _ _ n)

2252+ ni 0 env (PRef _ _ n)

2243 | not (n `elem` env)

2253 | not (n `elem` env)

2244 = case lookupTy n (tt_ctxt ist) of

2254 = case lookupTy n (tt_ctxt ist) of

2245 [] -> [n]

2255 [] -> [n]

2246 _ -> if n `elem` uvars then [n] else []

2256 _ -> if n `elem` uvars then [n] else []

2247− ni env (PApp _ f@(PRef _ _ n) as)

2257+ ni 0 env (PApp _ f@(PRef _ _ n) as)

2248− | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

2258+ | n `elem` uvars = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2249− | otherwise = concatMap (ni env) (map getTm as)

2259+ | otherwise = concatMap (ni 0 env) (map getTm as)

2250− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2260+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2251− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2261+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2252− ni env (PCase _ c os) = ni env c ++

2262+ ni 0 env (PCase _ c os) = ni 0 env c ++

2253 -- names in 'os', not counting the names bound in the cases

2263 -- names in 'os', not counting the names bound in the cases

2254− (nub (concatMap (ni env) (map snd os))

2264+ (nub (concatMap (ni 0 env) (map snd os))

2255− \\ nub (concatMap (ni env) (map fst os)))

2265+ \\ nub (concatMap (ni 0 env) (map fst os)))

2256− ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2266+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2257− ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

2267+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2258− ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc

2268+ ni 0 env (PPi p n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2259− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2269+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2260− ni env (PTyped l r) = ni env l ++ ni env r

2270+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2261− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2271+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2262− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2272+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2263− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2273+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2264− ni env (PAlternative ns a as) = concatMap (ni env) as

2274+ ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2265− ni env (PHidden tm) = ni env tm

2275+ ni 0 env (PHidden tm) = ni 0 env tm

2266− ni env (PUnifyLog tm) = ni env tm

2276+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2267− ni env (PDisamb _ tm) = ni env tm

2277+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2268− ni env (PNoImplicits tm) = ni env tm

2278+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2269− ni env _ = []

2279+

2280+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++

2281+ maybe [] (ni i env) ty

2282+ ni i env (PUnquote tm) = ni (i - 1) env tm

2283+

2284+ ni i env tm = concatMap (ni i env) (children tm)

2270

2285

2271-- Return names which are free in the given term.

2286-- Return names which are free in the given term.

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

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

2273−namesIn uvars ist tm = nub $ ni [] tm

2288+namesIn uvars ist tm = nub $ ni 0 [] tm

2274 where

2289 where

2275− ni env (PRef _ _ n)

2290+ ni 0 env (PRef _ _ n)

2276 | not (n `elem` env)

2291 | not (n `elem` env)

2277 = case lookupTy n (tt_ctxt ist) of

2292 = case lookupTy n (tt_ctxt ist) of

2278 [] -> [n]

2293 [] -> [n]

2279 _ -> if n `elem` (map fst uvars) then [n] else []

2294 _ -> if n `elem` (map fst uvars) then [n] else []

2280− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2295+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2281− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2296+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2282− ni env (PCase _ c os) = ni env c ++

2297+ ni 0 env (PCase _ c os) = ni 0 env c ++

2283 -- names in 'os', not counting the names bound in the cases

2298 -- names in 'os', not counting the names bound in the cases

2284− (nub (concatMap (ni env) (map snd os))

2299+ (nub (concatMap (ni 0 env) (map snd os))

2285− \\ nub (concatMap (ni env) (map fst os)))

2300+ \\ nub (concatMap (ni 0 env) (map fst os)))

2286− ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2301+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2287− ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc

2302+ ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2288− ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2303+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2289− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2304+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2290− ni env (PTyped l r) = ni env l ++ ni env r

2305+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2291− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2306+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2292− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2307+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2293− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2308+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2294− ni env (PAlternative ns a as) = concatMap (ni env) as

2309+ ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2295− ni env (PHidden tm) = ni env tm

2310+ ni 0 env (PHidden tm) = ni 0 env tm

2296− ni env (PUnifyLog tm) = ni env tm

2311+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2297− ni env (PDisamb _ tm) = ni env tm

2312+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2298− ni env (PNoImplicits tm) = ni env tm

2313+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2299− ni env _ = []

2314+

2300−

2315+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2316+ ni i env (PUnquote tm) = ni (i - 1) env tm

2317+

2318+ ni i env tm = concatMap (ni i env) (children tm)

2319+

2301− niTacImp env (TacImp _ _ scr) = ni env scr

2320+ niTacImp i env (TacImp _ _ scr) = ni i env scr

2302− niTacImp _ _ = []

2321+ niTacImp _ _ _ = []

2303

2322

2304-- Return which of the given names are used in the given term.

2323-- Return which of the given names are used in the given term.

2305

2324

2306usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

2325usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

2307−usedNamesIn vars ist tm = nub $ ni [] tm

2326+usedNamesIn vars ist tm = nub $ ni 0 [] tm

2308 where -- TODO THINK added niTacImp, but is it right?

2327 where -- TODO THINK added niTacImp, but is it right?

2309− ni env (PRef _ _ n)

2328+ ni 0 env (PRef _ _ n)

2310 | n `elem` vars && not (n `elem` env)

2329 | n `elem` vars && not (n `elem` env)

2311 = case lookupDefExact n (tt_ctxt ist) of

2330 = case lookupDefExact n (tt_ctxt ist) of

2312 Nothing -> [n]

2331 Nothing -> [n]

2313 _ -> []

2332 _ -> []

2314− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2333+ ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2315− ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2334+ ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env) (map getTm as)

2316− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

2335+ ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env) (map snd os)

2317− ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2336+ ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

2318− ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc

2337+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

2319− ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2338+ ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2320− ni env (PRewrite _ l r _) = ni env l ++ ni env r

2339+ ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2321− ni env (PTyped l r) = ni env l ++ ni env r

2340+ ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

2322− ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2341+ ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

2323− ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2342+ ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

2324− ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

2343+ ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r

2325− ni env (PAlternative ns a as) = concatMap (ni env) as

2344+ ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as

2326− ni env (PHidden tm) = ni env tm

2345+ ni 0 env (PHidden tm) = ni 0 env tm

2327− ni env (PUnifyLog tm) = ni env tm

2346+ ni 0 env (PUnifyLog tm) = ni 0 env tm

2328− ni env (PDisamb _ tm) = ni env tm

2347+ ni 0 env (PDisamb _ tm) = ni 0 env tm

2329− ni env (PNoImplicits tm) = ni env tm

2348+ ni 0 env (PNoImplicits tm) = ni 0 env tm

2330− ni env _ = []

2349+

2331−

2350+ ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty

2351+ ni i env (PUnquote tm) = ni (i - 1) env tm

2352+

2353+ ni i env tm = concatMap (ni i env) (children tm)

2354+

2332− niTacImp env (TacImp _ _ scr) = ni env scr

2355+ niTacImp i env (TacImp _ _ scr) = ni i env scr

2333− niTacImp _ _ = []

2356+ niTacImp _ _ _ = []

2334

2357

2335-- Return the list of inaccessible (= dotted) positions for a name.

2358-- Return the list of inaccessible (= dotted) positions for a name.

2336getErasureInfo :: IState -> Name -> [Int]

2359getErasureInfo :: IState -> Name -> [Int]

test/meta002/Tacs.idr+40

@@ -52,6 +52,45 @@ test1 = %runElab triv

52test2 : Nat

53test2 = %runElab triv

55+obvious : Elab ()

56+obvious = do g <- goalType

57+ case g of

58+ `(() : Type) =>

59+ do fill `(() : ())

60+ solve

61+ `((~a, ~b) : Type) =>

62+ do aH <- gensym "a"

63+ bH <- gensym "b"

64+ claim aH a

65+ claim bH b

66+ fill `(MkPair {A=~a} {B=~b} ~(Var aH) ~(Var bH))

67+ solve

68+ focus aH; obvious

69+ focus bH; obvious

70+ `(Either ~a ~b) =>

71+ (do h <- gensym "a"

72+ claim h a

73+ fill `(Left {a=~a} {b=~b} ~(Var h))

74+ solve

75+ focus h; obvious) <|>

76+ -- This second h didn't work at one point - this

77+ -- test makes sure the fix stays fixed. The

78+ -- uniquification of binder names didn't

79+ -- appropriately treat quotation.

80+ (do h <- gensym "a"

81+ claim h b

82+ fill `(Right {a=~a} {b=~b} ~(Var h))

83+ solve

84+ focus h; obvious)

85+

86+easy : ()

87+easy = %runElab obvious

88+

89+

90+easy2 : ((), ((), (Either () Void)))

91+easy2 = %runElab obvious

92+

93+

56namespace STLC

95namespace STLC

@@ -254,3 +293,4 @@ namespace STLC

254 -- Tacs.idr line 247 col 14:

293 -- Tacs.idr line 247 col 14:

255 -- When elaborating right hand side of testElab3:

294 -- When elaborating right hand side of testElab3:

256 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value

295 -- Unifying ty and Tacs.STLC.ARR ty t would lead to infinite value

296+

test/meta002/expected+1−1

@@ -1,3 +1,3 @@

1−Tacs.idr:251:15:

1+Tacs.idr:290:15:

2When checking right hand side of testElab3:

3Unifying ty and ARR ty t would lead to infinite value