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

git.iko.soy/Idris-dev

Merge pull request #2630 from david-christiansen/namesInQQ

Make name operations on PTerm quotation-aware

commit6d7d3bdba192da87f0000c25406aae61647ffea1 authorDavid Christiansen <david@davidchristiansen.dk> dateSat 19 Sep 2015, 08:54 (11 years ago) parent9243fdf 071d34b

4 files changed+267−189

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+82−67 src/Idris/AbsSyntaxTree.hs+144−121 test/meta002/Tacs.idr+40 test/meta002/expected+1−1

src/Idris/AbsSyntax.hs+82−67

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

3131import qualified Data.Set as S

3232import Data.Word (Word)

3333

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

35+

3436import Debug.Trace

3537

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

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

21142116 fullApp x = x

21152117

21162118shadow :: Name -> Name -> PTerm -> PTerm

2117−shadow n n' t = sm t where

2118− sm (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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2140− sm x = x

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

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

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

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

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

2124+ | otherwise = PPi p x fc (sm 0 t) 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

21412145

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

21432147-- about with shadowing anywhere else).

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

21452149mkUniqueNames env shadows tm

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

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

21472151

21482152 initMap = M.fromList shadows

21492153

21502154 inScope :: S.Set Name

21512155 inScope = S.fromList $ boundNamesIn tm

21522156

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

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

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

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

21552159

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

21572161 -- looking for too long...)

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

21612165

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

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

2164− mkUniqT nmap tac = return tac

2168+ mkUniqT _ nmap tac = return tac

21652169

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

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

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

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

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

21682173 = do env <- get

21692174 (n', sc') <-

21702175 if n `S.member` env

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

21742179 else return (n, sc)

21752180 put (S.insert n' env)

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

2177− ty' <- mkUniq nmap ty

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

2182+ ty' <- mkUniq 0 nmap ty

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

21792184 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)

21812186 = do env <- get

21822187 (n', sc') <-

21832188 if n `S.member` env

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

21872192 else return (n, sc)

21882193 put (S.insert n' env)

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

2190− ty' <- mkUniq nmap ty

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

2195+ ty' <- mkUniq 0 nmap ty

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

21922197 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)

21942199 = do env <- get

21952200 (n', sc') <-

21962201 if n `S.member` env

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

22002205 else return (n, sc)

22012206 put (S.insert n' env)

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

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

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

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

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

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

2206− mkUniq nmap (PApp fc t args)

2207− = do t' <- mkUniq nmap t

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

2211+ mkUniq 0 nmap (PApp fc t args)

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

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

22092214 return $! PApp fc t' args'

2210− mkUniq nmap (PAppBind fc t args)

2211− = do t' <- mkUniq nmap t

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

2215+ mkUniq 0 nmap (PAppBind fc t args)

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

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

22132218 return $! PAppBind fc t' args'

2214− mkUniq nmap (PCase fc t alts)

2215− = do t' <- mkUniq nmap t

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

2219+ mkUniq 0 nmap (PCase fc t alts)

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

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

22172222 return (x', y')) alts

22182223 return $! PCase fc t' alts'

2219− mkUniq nmap (PIfThenElse fc c t f)

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

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

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

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

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

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

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

22232228 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)

22252230 | t /= Placeholder

22262231 = do env <- get

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

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

22302235 else return (n, sc)

22312236 put (S.insert n' env)

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

2233− t' <- mkUniq nmap t

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

2238+ t' <- mkUniq 0 nmap t

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

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

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

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

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

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

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

2239− mkUniq nmap (PAlternative ns b as)

2244+ mkUniq 0 nmap (PAlternative ns b as)

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

22412246 -- during elaboration

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

22532258 where

22542259 shadowAll [] t = t

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

22562261

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)

2828

2929import Data.Data (Data)

3030import Data.Function (on)

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

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

3232import Data.List hiding (group)

3333import Data.Char

3434import qualified Data.Map.Strict as M

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

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

21782178

21792179allNamesIn :: PTerm -> [Name]

2180−allNamesIn tm = nub $ ni [] tm

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

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

2182− ni env (PRef _ _ n)

2182+ ni 0 env (PRef _ _ n)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2203− ni env _ = []

2204−

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

2206− niTacImp _ _ = []

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

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

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

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

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

2189+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (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 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

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

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

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

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

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

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

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

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

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

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

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

2203+

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+

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

2210+ niTacImp _ _ _ = []

22072211

22082212

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

22102214boundNamesIn :: PTerm -> [Name]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2230− ni set _ = set

2231−

2232− niTms set [] = set

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

2234−

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

2236− niTacImp set _ = set

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

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

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

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

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

2222+ ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) 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

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

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

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

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

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

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

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

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

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

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

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

2235+

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

2242+ niTms i set [] = set

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

2244+

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

2246+ niTacImp i set _ = set

22372247

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

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

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

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

22412251 where

2242− ni env (PRef _ _ n)

2252+ ni 0 env (PRef _ _ n)

22432253 | not (n `elem` env)

22442254 = case lookupTy n (tt_ctxt ist) of

22452255 [] -> [n]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2269− ni env _ = []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

22702285

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

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

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

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

22742289 where

2275− ni env (PRef _ _ n)

2290+ ni 0 env (PRef _ _ n)

22762291 | not (n `elem` env)

22772292 = case lookupTy n (tt_ctxt ist) of

22782293 [] -> [n]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2299− ni env _ = []

2300−

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

2302− niTacImp _ _ = []

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

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

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

2302+ ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (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

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

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

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

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

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

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

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

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

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

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

2314+

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+

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

2321+ niTacImp _ _ _ = []

23032322

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

23052324

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

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

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

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

2309− ni env (PRef _ _ n)

2328+ ni 0 env (PRef _ _ n)

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

23112330 = case lookupDefExact n (tt_ctxt ist) of

23122331 Nothing -> [n]

23132332 _ -> []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2330− ni env _ = []

2331−

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

2333− niTacImp _ _ = []

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

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

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

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

2337+ ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (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

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

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

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

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

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

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

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

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

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

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

2349+

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+

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

2356+ niTacImp _ _ _ = []

23342357

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

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

test/meta002/Tacs.idr+40

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

5252test2 : Nat

5353test2 = %runElab triv

5454

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+

5594

5695namespace STLC

5796

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

254293 -- Tacs.idr line 247 col 14:

255294 -- When elaborating right hand side of testElab3:

256295 -- 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:

22When checking right hand side of testElab3:

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