git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1495 from edwinb/unique

Uniqueness changes

commit1270b7c14886e128d71c89c5f66b231d10c67103 authorEdwin Brady <edwin.brady@gmail.com> dateThu 28 Aug 2014, 15:32 (12 years ago) parent91eecdbe1a2cf8
3 files changed+8−17
compare with master
unifiedsplit
src/Idris/Core/Typecheck.hs+4−13 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Utils.hs+3−3
src/Idris/Core/Typecheck.hs+4−13
@@ -51,17 +51,17 @@ isType ctxt env tm = isType' (normalise ctxt env tm)
5151 | otherwise = fail (showEnv env tm ++ " is not a Type")
5252
5353recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
54−recheck = recheck_borrowing []
54+recheck = recheck_borrowing False []
5555
56−recheck_borrowing :: [Name] -> Context -> Env -> Raw -> Term ->
56+recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->
5757 TC (Term, Type, UCs)
58−recheck_borrowing bs ctxt env tm orig
58+recheck_borrowing uniq_check bs ctxt env tm orig
5959 = let v = next_tvar ctxt in
6060 case runStateT (check' False ctxt env tm) (v, []) of -- holes banned
6161 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig
6262 Error e -> Error e
6363 OK ((tm, ty), constraints) ->
64− do checkUnique bs ctxt env tm
64+ do when uniq_check $ checkUnique bs ctxt env tm
6565 return (tm, ty, constraints)
6666
6767check :: Context -> Env -> Raw -> TC (Term, Type)
@@ -281,20 +281,11 @@ checkUnique borrowed ctxt env tm
281281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a
282282 chkBinders env (Bind n b t)
283283 = do chkBinderName env n b
284− -- Must be safe whether we evaluate the scope or binder first
285− -- (Surely there is a tidier rule than this...?)
286284 st <- get
287− chkBinders env (binderTy b)
288285 case b of
289286 Let t v -> chkBinders env v
290287 _ -> return ()
291288 chkBinders ((n, b) : env) t
292−-- put st
293−-- chkBinders env (binderTy b)
294−-- case b of
295−-- Let t v -> chkBinders env v
296−-- _ -> return ()
297−-- chkBinders ((n, b) : env) t
298289 chkBinders env t = return ()
299290
300291 chkBinderName :: Env -> Name -> Binder Term ->
src/Idris/Elab/Clause.hs+1−1
@@ -600,7 +600,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
600600 logLvl 6 $ " ==> " ++ show (forget rhs')
601601
602602 (crhs, crhsty) <- if not inf
603− then recheckC_borrowing borrowed fc [] rhs'
603+ then recheckC_borrowing True borrowed fc [] rhs'
604604 else return (rhs', clhsty)
605605 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
606606 case converts ctxt [] clhsty crhsty of
src/Idris/Elab/Utils.hs+3−3
@@ -21,12 +21,12 @@ import Debug.Trace
2121
2222import qualified Data.Map as Map
2323
24−recheckC = recheckC_borrowing []
24+recheckC = recheckC_borrowing False []
2525
26−recheckC_borrowing bs fc env t
26+recheckC_borrowing uniq_check bs fc env t
2727 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
2828 ctxt <- getContext
29− (tm, ty, cs) <- tclift $ case recheck_borrowing bs ctxt env (forget t) t of
29+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of
3030 Error e -> tfail (At fc e)
3131 OK x -> return x
3232 addConstraints fc cs