11b4fb1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Rename to --optimise-nat-like-types.

commit11b4fb16ff9349133c81732e0d08587909a4ced6 authorMatus Tejiscak <ziman@functor.sk> dateFri 5 Apr 2019, 11:09 (8 years ago) parentc899bcf

2 files changed+16−4

unifiedsplit

CHANGELOG.md+6

@@ -10,6 +10,12 @@

1010 interfaces (i.e. types for names declared `export` and definitions of names

1111 declared `public export`) are unchanged.

1212

13+## Miscellaneous updates

14++ Compiler flag `--optimise-nat-like-types` enables compilation

15+ of `Nat`-like type families to big integers. A type family

16+ is `Nat`-like if, after erasure, it has two constructors,

17+ one nullary, the other one with exactly one recursive field.

18+

1319# New in 1.3.1

1420

1521## Tool updates

src/Idris/CmdOptions.hs+10−4

@@ -209,10 +209,16 @@ parseFlags = many $

209209 <|> flag' (AddOpt PETransform) (long "partial-eval")

210210 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

211211

212− <|> flag' (AddOpt GeneralisedNatHack) (long "opt-nat-likes"

213− <> help "Enable compilation of Nat-like types to bigints")

214− <|> flag' (RemoveOpt GeneralisedNatHack) (long "no-opt-nat-likes"

215− <> help "Disable compilation of Nat-like types to bigints")

212+ <|> flag' (AddOpt GeneralisedNatHack) (

213+ long "optimise-nat-like-types"

214+ <> long "optimize-nat-like-types"

215+ <> help "Enable compilation of Nat-like types to bigints"

216+ )

217+ <|> flag' (RemoveOpt GeneralisedNatHack) (

218+ long "no-optimise-nat-like-types"

219+ <> long "no-optimize-nat-like-types"

220+ <> help "Disable compilation of Nat-like types to bigints"

221+ )

216222

217223 <|> OptLevel <$> option auto (short 'O' <> long "level")

218224