improve QName comparison time
This commit is contained in:
@@ -104,7 +104,8 @@ data QName : U where
|
|||||||
QN : List String -> String -> QName
|
QN : List String -> String -> QName
|
||||||
|
|
||||||
instance Eq QName where
|
instance Eq QName where
|
||||||
QN ns n == QN ns' n' = n == n' && ns == ns'
|
-- `if` gets us short circuit behavior, idris has a lazy `&&`
|
||||||
|
QN ns n == QN ns' n' = if n == n' then ns == ns' else False
|
||||||
|
|
||||||
instance Show QName where
|
instance Show QName where
|
||||||
show (QN Nil n) = n
|
show (QN Nil n) = n
|
||||||
|
|||||||
@@ -110,7 +110,8 @@ processTypeSig ns fc names tm = do
|
|||||||
-- let mstart = length' mc.metas
|
-- let mstart = length' mc.metas
|
||||||
traverse (checkAlreadyDef fc) names
|
traverse (checkAlreadyDef fc) names
|
||||||
ty <- check (mkCtx fc) tm (VU fc)
|
ty <- check (mkCtx fc) tm (VU fc)
|
||||||
ty <- zonk top 0 Nil ty
|
-- this is not needed
|
||||||
|
-- ty <- zonk top 0 Nil ty
|
||||||
log 1 $ \ _ => "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}"
|
log 1 $ \ _ => "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}"
|
||||||
ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil
|
ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil
|
||||||
|
|
||||||
@@ -161,7 +162,7 @@ processDef ns fc nm clauses = do
|
|||||||
-- TODO - make nf that expands all metas and drop zonk
|
-- TODO - make nf that expands all metas and drop zonk
|
||||||
-- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure.
|
-- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure.
|
||||||
-- Day1.newt is a test case
|
-- Day1.newt is a test case
|
||||||
-- tm' <- nf Nil tm
|
-- NOW - might not need this if we do it at compile time
|
||||||
tm' <- zonk top 0 Nil tm
|
tm' <- zonk top 0 Nil tm
|
||||||
debug $ \ _ => "NF\n\{render 80 $ pprint Nil tm'}"
|
debug $ \ _ => "NF\n\{render 80 $ pprint Nil tm'}"
|
||||||
-- This is done in Compile.newt now, we can't store the result because we need the real thing at compile time
|
-- This is done in Compile.newt now, we can't store the result because we need the real thing at compile time
|
||||||
|
|||||||
Reference in New Issue
Block a user