idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 17:21:59 +03:00
Code Issues Projects Releases Wiki Activity
A purely functional programming language with first class types
3,542 Commits 6 Branches 9 Tags 115 MiB
Idris 95.4%
C 2.3%
Scheme 0.6%
Racket 0.4%
Makefile 0.3%
Other 1%
196d08dd6d
Go to file
Alex1005a 196d08dd6d
Implement Precise Reference Counting for C backend (#2989) 
* start implement drop spec

* [RefC] remove vars after prim function call

* [RefC] gc pointer processing changed

* [RefC] fix memory leak in stringIteratorToString

* [RefC] runtime.c refactoring

* Implement basic reuse analisis

* [RefC] do not delete reusable variables in value in let

* [RefC] Use names instead tags in reuse map

* [RefC] Don't set all fields to null in reuse constructor

* Use record syntax in RefC

* Add some utility functions to RefC

* Sort output in garbageCollect refc test

* Add memory leak test for RefC

* [RefC] Remove variable only from body in let

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

* [RefC] Remove borrowed set from env

* [RefC] Use Ref variable for Enviroment instead of passing as an argument

* [RefC] Use locally function as combinator

* [RefC] removing unnecessary dup and remove during pattern matching

* Update refcTests and refcMemoryLeakTests

* Remove some test files

* move CHANGELOG entry to CHANGELOG_NEXT

* Move refc-memory tests

* Change calling convention test

* [RefC] [Test] Reuse test

---------

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Mathew Polzin <matt.polzin@gmail.com>
2024-02-12 00:43:17 -06:00
.github [ ci ] Bump deprecated versions of used CI actions to avoid warnings 2024-01-31 17:18:24 +03:00
benchmark [ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
bootstrap [ rc ] 0.7.0-rc2 2023-12-22 14:44:30 +01:00
docs Update starting.rst 2024-01-21 14:28:35 +02: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 [ elab ] Treat map and <*> with no bind in elab scripts runner 2024-01-17 17:45:19 +03:00
lint Lint utility 2021-01-16 10:00:03 +00:00
nix hopefully final refactor of buildIdris (#3200) 2024-01-21 23:05:26 -06: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 #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
src Implement Precise Reference Counting for C backend (#2989) 2024-02-12 00:43:17 -06:00
support Implement Precise Reference Counting for C backend (#2989) 2024-02-12 00:43:17 -06:00
tests Implement Precise Reference Counting for C backend (#2989) 2024-02-12 00:43:17 -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 Implement Precise Reference Counting for C backend (#2989) 2024-02-12 00:43:17 -06:00
CHANGELOG.md Add a new CHANGELOG_NEXT.md file and update documentation around CHANGELOG entries. (#3180) 2024-01-01 21:08:56 -06:00
config.mk Fix build on FreeBSD (#2852) 2023-01-14 08:19:12 -06: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 Implement Precise Reference Counting for C backend (#2989) 2024-02-12 00:43:17 -06:00
default.nix [ ci ] Simplify bootstrap process in nix (#2731) 2022-10-28 19:29:30 +01:00
flake.lock hopefully final refactor of buildIdris (#3200) 2024-01-21 23:05:26 -06:00
flake.nix hopefully final refactor of buildIdris (#3200) 2024-01-21 23:05:26 -06:00
idris2.ipkg [ cleanup ] --timing levels 2022-04-13 14:37:43 +01:00
idris2api.ipkg [ cleanup ] Post v0.7.0 cleanup 2023-12-25 13:49:26 +00:00
INSTALL.md Update INSTALL.md (#2708) 2024-01-14 11:39:03 -06:00
LICENSE Add licence and changelog and update REAMDE 2020-05-20 11:31:48 +01:00
Makefile Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06: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.