idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

[ perf ] Move unnecessary toFullNames calls under a logC (#1423)

Browse Source 
Fixed by converting the name of the equality type constructor to a resolved name
so that unresolved names do not show up in the unifier.
This commit is contained in:
Ruslan Feizerakhmanov 2021-05-17 13:13:35 +03:00 committed by GitHub
parent 11761daa76
commit d97f5266de
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Core/Unify.idr
View File

@ -1157,9 +1157,10 @@ mutual
(NDCon xfc x tagx ax xs)
(NDCon yfc y tagy ay ys)
unifyNoEta mode loc env (NTCon xfc x tagx ax xs) (NTCon yfc y tagy ay ys)
= do x <- toFullNames x
y <- toFullNames y
log "unify" 20 $ "Comparing type constructors " ++ show x ++ " and " ++ show y
= do logC "unify" 20 $ do
x <- toFullNames x
y <- toFullNames y
pure $ "Comparing type constructors " ++ show x ++ " and " ++ show y
if x == y
then do let xs = map snd xs
let ys = map snd ys

2
src/TTImp/ProcessDef.idr
View File

@ -596,7 +596,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env
let eqName = NS builtinNS (UN "Equal")
Just (TCon t ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs)
| _ => throw (InternalError "Cannot find builtin Equal")
let eqTyCon = Ref vfc (TyCon t ar) eqName
let eqTyCon = Ref vfc (TyCon t ar) !(toResolvedNames eqName)
let wargn : Name
wargn = MN "warg" 0