b696f28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make unique name generation much quicker

Especially in large do blocks with ambiguity and unnamed bindings. We make names unique in advance to simplify lots of other stuff, but we really don't want to generate-and-test loads of possibilities. This is a bit of a hack, but it just makes sure we generate a name that's already likely to be unique.

commitb696f28d341b59bb570e1bdd8c0c011208b9c5c2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 4 Apr 2014, 15:11 (13 years ago) parent06e2b1d

2 files changed+15−6

compare with master

unifiedsplit

CHANGELOG+3−3 src/Idris/AbsSyntax.hs+12−3

CHANGELOG+3−3

@@ -5,7 +5,7 @@ New in 0.9.12:

55 type inference.

66* New 'Lazy' type, replacing laziness annotations.

77* JavaScript and Node codegen now understand the %include directive.

8−* Concept up 'null' is now understood in the JavaScript and Node codegen.

8+* Concept of 'null' is now understood in the JavaScript and Node codegen.

99* Lots of performance patches for generated JavaScript.

1010* New commands :eval (:e) and :type (:t) in the prover, which either normalise

1111 or show the type of expressions.

@@ -17,8 +17,8 @@ New in 0.9.12:

1717 ||| @ n the first number (examined by the function)

1818 ||| @ m the second number (not examined)

1919 plus (n, m : Nat) -> Nat

20−* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

21− of proof automation. Use ":set autosolve" and ":unset autosolve".

20+* Allow the auto-solve behaviour in the prover to be disabled, for easier

21+ debugging of proof automation. Use ":set autosolve" and ":unset autosolve".

2222* Updated 'effects' library

2323* New :apropos command at REPL to search documentation, names, and types

2424* Unification errors are now slightly more informative

src/Idris/AbsSyntax.hs+12−3

@@ -1695,6 +1695,12 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

16951695 mkUniqA arg = do t' <- mkUniq (getTm arg)

16961696 return (arg { getTm = t' })

16971697

1698+ -- Initialise the unique name with the environment length (so we're not

1699+ -- looking for too long...)

1700+ initN (UN n) l = UN $ txt (str n ++ show l)

1701+ initN (MN i s) l = MN (i+l) s

1702+ initN n l = n

1703+

16981704 -- FIXME: Probably ought to do this for completeness! It's fine as

16991705 -- long as there are no bindings inside tactics though.

17001706 mkUniqT tac = return tac

@@ -1704,7 +1710,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17041710 = do env <- get

17051711 (n', sc') <-

17061712 if n `elem` env

1707− then do let n' = uniqueName n (env ++ inScope)

1713+ then do let n' = uniqueName (initN n (length env))

1714+ (env ++ inScope)

17081715 return (n', shadow n n' sc)

17091716 else return (n, sc)

17101717 put (n' : env)

@@ -1715,7 +1722,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17151722 = do env <- get

17161723 (n', sc') <-

17171724 if n `elem` env

1718− then do let n' = uniqueName n (env ++ inScope)

1725+ then do let n' = uniqueName (initN n (length env))

1726+ (env ++ inScope)

17191727 return (n', shadow n n' sc)

17201728 else return (n, sc)

17211729 put (n' : env)

@@ -1726,7 +1734,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

17261734 = do env <- get

17271735 (n', sc') <-

17281736 if n `elem` env

1729− then do let n' = uniqueName n (env ++ inScope)

1737+ then do let n' = uniqueName (initN n (length env))

1738+ (env ++ inScope)

17301739 return (n', shadow n n' sc)

17311740 else return (n, sc)

17321741 put (n' : env)