git.iko.soy/Idris-dev
on master help sign in
No need to check LHS for unique usage

Any duplication will be enforced by unification, and won't lead to sharing itself (does suggest the function will be hard to apply in interesting contexts though...)

commite1a2cf8509235e394f45e368482cb9a5dea7b93d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 27 Aug 2014, 22:14 (12 years ago) parentf57383c
3 files changed+8−8
compare with master
unifiedsplit
src/Idris/Core/Typecheck.hs+4−4 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Utils.hs+3−3
src/Idris/Core/Typecheck.hs+4−4
@@ -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)
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