b696f28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make unique name generation much quicker

b696f28Edwin Brady13 years ago

CHANGELOG+3−3

compare with master

unifiedsplit

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

5 type inference.

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

7* 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.

9* Lots of performance patches for generated JavaScript.

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

11 or show the type of expressions.

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

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

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

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

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

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

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

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

22* Updated 'effects' library

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

24* 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

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

1696 return (arg { getTm = t' })

1697

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+

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

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

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

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

1700 mkUniqT tac = return tac

1706 mkUniqT tac = return tac

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

1704 = do env <- get

1710 = do env <- get

1705 (n', sc') <-

1711 (n', sc') <-

1706 if n `elem` env

1712 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)

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

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

1709 else return (n, sc)

1716 else return (n, sc)

1710 put (n' : env)

1717 put (n' : env)

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

1715 = do env <- get

1722 = do env <- get

1716 (n', sc') <-

1723 (n', sc') <-

1717 if n `elem` env

1724 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)

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

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

1720 else return (n, sc)

1728 else return (n, sc)

1721 put (n' : env)

1729 put (n' : env)

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

1726 = do env <- get

1734 = do env <- get

1727 (n', sc') <-

1735 (n', sc') <-

1728 if n `elem` env

1736 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)

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

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

1731 else return (n, sc)

1740 else return (n, sc)

1732 put (n' : env)

1741 put (n' : env)