5492e60 · Idris-dev · git.iko.soy

53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

54recheck = recheck_borrowing False []

55

56−recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

56+recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

57 TC (Term, Type, UCs)

58recheck_borrowing uniq_check bs ctxt env tm orig

59 = let v = next_tvar ctxt in

65 return (tm, ty, constraints)

66

67check :: Context -> Env -> Raw -> TC (Term, Type)

68−check ctxt env tm

68+check ctxt env tm

69 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

70

71check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

93 ty@(Bind x (Pi s k) t) -> ty

94 _ -> normalise ctxt env fty

95 case fty' of

96− Bind x (Pi s k) t ->

96+ Bind x (Pi s k) t ->

97 do convertsC ctxt env aty s

98 let apty = simplify initContext env

99 (Bind x (Let aty av) t)

100 return (App fv av, apty)

101− t -> lift $ tfail $ NonFunctionType fv fty

101+ t -> lift $ tfail $ NonFunctionType fv fty

102 chk u env RType

103 | holes = return (TType (UVal 0), TType (UVal 0))

104 | otherwise = do (v, cs) <- get

135 = do (sv, st) <- chk u env s

136 (kv, kt) <- chk u env k

137 (tv, tt) <- chk st ((n, Pi sv kv) : env) t

138−-- let tv = mkUniquePi kv tv_in

139 (v, cs) <- get

138 (v, cs) <- get

140 case (normalise ctxt env st, normalise ctxt env tt) of

139 case (normalise ctxt env st, normalise ctxt env tt) of

141 (TType su, TType tu) -> do

140 (TType su, TType tu) -> do

148 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

147 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

149 (pToV n tv), k')

148 (pToV n tv), k')

150

149

151− where mkUniquePi kv (Bind n (Pi s k) sc)

150+ where mkUniquePi kv (Bind n (Pi s k) sc)

152 = let k' = smaller kv k in

151 = let k' = smaller kv k in

153 Bind n (Pi s k') (mkUniquePi k' sc)

152 Bind n (Pi s k') (mkUniquePi k' sc)

154− mkUniquePi kv (Bind n (Lam t) sc)

153+ mkUniquePi kv (Bind n (Lam t) sc)

155 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

154 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

156− mkUniquePi kv (Bind n (Let t v) sc)

155+ mkUniquePi kv (Bind n (Let t v) sc)

157 = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

156 = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

158 mkUniquePi kv t = t

157 mkUniquePi kv t = t

159

158

257-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

256-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

258-- in the scope more than once, this is an error.

257-- in the scope more than once, this is an error.

259checkUnique :: [Name] -> Context -> Env -> Term -> TC ()

258checkUnique :: [Name] -> Context -> Env -> Term -> TC ()

260−checkUnique borrowed ctxt env tm

259+checkUnique borrowed ctxt env tm

261 = evalStateT (chkBinders env (explicitNames tm)) []

260 = evalStateT (chkBinders env (explicitNames tm)) []

262− where

261+ where

263 isVar (P _ _ _) = True

262 isVar (P _ _ _) = True

264 isVar (V _) = True

263 isVar (V _) = True

265 isVar _ = False

264 isVar _ = False

272 chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

271 chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

273 | isVar a && owner == txt "Ownership" &&

272 | isVar a && owner == txt "Ownership" &&

274 (lend == txt "lend" || lend == txt "Read")

273 (lend == txt "lend" || lend == txt "Read")

275− = do chkBinders env t -- Check the type normally

274+ = do chkBinders env t -- Check the type normally

276 st <- get

275 st <- get

277 -- Remove the 'LendOnly' names from the unusable set

276 -- Remove the 'LendOnly' names from the unusable set

278− put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

277+ put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

279 chkBinders env a

278 chkBinders env a

280 put st -- Reset the old state after checking the argument

279 put st -- Reset the old state after checking the argument

281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

280 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

288 chkBinders ((n, b) : env) t

287 chkBinders ((n, b) : env) t

289 chkBinders env t = return ()

288 chkBinders env t = return ()

290

289

291− chkBinderName :: Env -> Name -> Binder Term ->

290+ chkBinderName :: Env -> Name -> Binder Term ->

292 StateT [(Name, (UniqueUse, Universe))] TC ()

291 StateT [(Name, (UniqueUse, Universe))] TC ()

293 chkBinderName env n b

292 chkBinderName env n b

294 = do let rawty = forgetEnv (map fst env) (binderTy b)

293 = do let rawty = forgetEnv (map fst env) (binderTy b)

295 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

294 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

296 case kind of

295 case kind of

297 UType UniqueType -> do ns <- get

296 UType UniqueType -> do ns <- get

298− if n `elem` borrowed

297+ if n `elem` borrowed

299 then put ((n, (LendOnly, NullType)) : ns)

298 then put ((n, (LendOnly, NullType)) : ns)

300 else put ((n, (Once, UniqueType)) : ns)

299 else put ((n, (Once, UniqueType)) : ns)

301 UType NullType -> do ns <- get

300 UType NullType -> do ns <- get

304 put ((n, (Once, AllTypes)) : ns)

303 put ((n, (Once, AllTypes)) : ns)

305 _ -> return ()

304 _ -> return ()

306

305

307− chkName n

306+ chkName n

308 = do ns <- get

307 = do ns <- get

309 case lookup n ns of

308 case lookup n ns of

310 Nothing -> return ()

309 Nothing -> return ()

311 Just (Many, k) -> return ()

310 Just (Many, k) -> return ()

312 Just (Never, k) -> lift $ tfail (UniqueError k n)

311 Just (Never, k) -> lift $ tfail (UniqueError k n)

313 Just (LendOnly, k) -> lift $ tfail (UniqueError k n)

312 Just (LendOnly, k) -> lift $ tfail (UniqueError k n)

314− Just (Once, k) -> put ((n, (Never, k)) :

313+ Just (Once, k) -> put ((n, (Never, k)) :

315 filter (\x -> fst x /= n) ns)

314 filter (\x -> fst x /= n) ns)

316−