idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-23 06:04:48 +03:00
Code Issues Projects Releases Wiki Activity
A purely functional programming language with first class types
3,768 Commits 5 Branches 9 Tags 95 MiB
Idris 95.4%
C 2.3%
Scheme 0.6%
Racket 0.4%
Makefile 0.3%
Other 1%
main
Go to file
Hattori, Hiroki f016dad5cd
[RefC] Object Immortalization and Pre-Generation of Constants (#3242) 
* [RefC] shrink value_header; object imortalized; stock well knwon values.

  * Shrink Value_Header to improve utilization of memory.
  * When refCounter reaches its maximum, the object is immortalized to
    avoid overflow. This immotalization is also used to represent
    statically allocated stock objects.
  * Prepare some commonly seen values and share it to improve memory usage.
  * Added debug code to dump memory stats.

* [RefC] Allocated constants statically; Predefined commonly seen values.

* Commonly seen values such as integers less than 100 are predefined and shared.
* Constant String, Int64, Bits64 and Double values are allocated statically as
  indestructible and shared.

* linter

* [RefC] make constants const.

* cleanup

* cleanup

* update CHANGELOG_NEXT

* [refc][test] revert debugging code

* Refactor constantName function in RefC.idr

Refactor constantName function to return Core String type
and handle unsupported types by throwing InternalError exception.

* lint

* fix typo in support/refc/memoryManagement.c

Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>

* [RefC] erase runtime error of constantName

* [RefC] Fixed the missing case expression coverage.

---------

Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
2024-11-20 17:15:26 -06:00
.github include hidden files in artifacts built by CI (#3382) 2024-09-10 21:51:59 -05:00
benchmark [ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
bootstrap idris2.ss: support powerpc (#3326) 2024-06-24 11:49:17 -05:00
docs [ literate ] Support typst in literate Idris (#3403) 2024-11-07 11:56:33 +00:00
icons Add icons 2020-05-20 18:48:55 +01:00
ipkg [ refactor ] S-Exp protocols to depend on fewer Idris modules (#3060) 2023-08-31 11:53:14 +01:00
libs [ base ] Add atomically function (#3380) 2024-09-11 09:18:47 +01:00
lint Lint utility 2021-01-16 10:00:03 +00:00
nix [ refactor ] Add a nix overlay (#3394) 2024-10-01 07:51:34 -05:00
Release Add a new CHANGELOG_NEXT.md file and update documentation around CHANGELOG entries. (#3180) 2024-01-01 21:08:56 -06:00
samples [fix] include stdio header in readline C code in example so it builds on all systems (#3378) 2024-09-01 08:57:24 -05:00
src [RefC] Object Immortalization and Pre-Generation of Constants (#3242) 2024-11-20 17:15:26 -06:00
support [RefC] Object Immortalization and Pre-Generation of Constants (#3242) 2024-11-20 17:15:26 -06:00
tests [RefC] Object Immortalization and Pre-Generation of Constants (#3242) 2024-11-20 17:15:26 -06:00
www [ fix ] missing modules in .ipkg files (#3124) 2023-10-27 20:37:00 +01:00
.editorconfig [ install ] Check if 'realpath' exists for Chez and Racket backends (#1210) 2021-04-06 15:42:04 +01:00
.gitattributes Mark bootstrap code as generated 2021-06-30 22:11:54 +01:00
.gitignore [ test ] Set IDRIS2_PREFIX to a local dir when testing 2023-10-04 14:34:03 +01:00
.readthedocs.yaml [ docs ] fix build by adding config file 2023-11-23 17:46:45 +00:00
bootstrap-stage1-chez.sh Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
bootstrap-stage1-racket.sh Write files into bootstrap-build directory during bootstrap 2021-07-04 03:17:13 +01:00
bootstrap-stage2.sh Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
CHANGELOG_NEXT.md [RefC] Object Immortalization and Pre-Generation of Constants (#3242) 2024-11-20 17:15:26 -06:00
CHANGELOG.md [ fix ] Data and Type Constructor tags for :di (#3395) 2024-10-05 08:37:26 +01:00
config.mk [ fix ] Use HOMEBREW_PREFIX instead of /opt/homebrew 2024-04-27 14:51:25 -07:00
CONTRIBUTING.md Add a new CHANGELOG_NEXT.md file and update documentation around CHANGELOG entries. (#3180) 2024-01-01 21:08:56 -06:00
CONTRIBUTORS Handle multiline comments in Package (ipkg) (#3386) 2024-09-24 10:26:30 -05:00
default.nix [ ci ] Simplify bootstrap process in nix (#2731) 2022-10-28 19:29:30 +01:00
flake.lock allow buildIdris output to be used as a dependency in other buildIdris calls more directly 2024-06-26 15:23:08 -05:00
flake.nix [ refactor ] Add a nix overlay (#3394) 2024-10-01 07:51:34 -05:00
idris2.ipkg [ cleanup ] --timing levels 2022-04-13 14:37:43 +01:00
idris2api.ipkg Add an option that dumps package details to JSON (#3293) 2024-06-11 11:32:22 +01:00
INSTALL.md Doc: Use executable command for opening lib docs 2024-06-05 12:05:01 +01:00
LICENSE Add licence and changelog and update REAMDE 2020-05-20 11:31:48 +01:00
Makefile [ fix ] propagate LDFLAGS and CPPFLAGS to test makefile 2024-04-27 14:40:07 -07:00
README.md wording 2023-11-13 11:42:27 +00:00

README.md

Idris 2

Documentation Status Build Status

Idris 2 is a purely functional programming language with first class types.

For installation instructions, see INSTALL.md.

The wiki lists a number of useful resources, in particular

Things still missing

  • Cumulativity (currently Type : Type. Bear that in mind when you think you've proved something)
  • rewrite doesn't yet work on dependent types

Contributions wanted

If you want to learn more about Idris, contributing to the compiler could be one way to do so. The contribution guidelines outline the process. Having read that, choose a good first issue or have a look at the contributions wanted for something more involved. This map should help you find your way around the source code. See the wiki page for more details.