Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Quadratic name selection #4358

Open
nad opened this issue Jan 7, 2020 · 0 comments
Open

Quadratic name selection #4358

nad opened this issue Jan 7, 2020 · 0 comments

Comments

@nad
Copy link
Contributor

@nad nad commented Jan 7, 2020

I suspect that the following code leads to (roughly) quadratic behaviour:

-- | Create a concrete name that is not yet in scope.
freshConcreteName :: Range -> Int -> String -> ScopeM C.Name
freshConcreteName r i s = do
let cname = C.Name r C.NotInScope [Id $ stringToRawName $ s ++ show i]
rn <- resolveName $ C.QName cname
case rn of
UnknownName -> return cname
_ -> freshConcreteName r (i+1) s

Here is a test case that illustrates the problem:

open import Agda.Builtin.Unit

test :
  ⊤
test = λ
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
  x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt x@tt
   tt

If the number of function arguments is doubled, then the type-checking time is quadrupled (roughly). If the x@ strings are removed, then Agda still seems to exhibit (something like) quadratic behaviour, but the constant factor is lower, so I think this code can be used as a test case.

@nad nad added this to the 2.6.2 milestone Jan 7, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.