1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-11 08:25:46 +03:00
Commit Graph

486 Commits

Author SHA1 Message Date
Paul Cadman
b51623077a
Add "-Oz" optimization flag to clang args (#133)
The "-Oz" optimization flag optimizes to minimize the size of the
resulting binary.
2022-05-31 17:50:29 +02:00
Jonathan Cubides
edff265d31
Docs updates for 0.1.4 2022-05-31 12:28:08 +02:00
Paul Cadman
7e71122e7f
[app] Add compile command (#130)
* [app] Add compile command

The compile command drives the (external) clang compiler to build a WASM
binary from a minijuvix file.

The intermediate C files are stored in .minijuvix-build directory
relative to the directory where the command is executed.

The user can specify which runtime (standalone and libc) to build
against.

The file-embed library is used to embed the runtime files into the
minijuvix binary.

* TemplateHaskell is a default extension

* [app] Add the .minijuvix-build dir in the root of the project

* [app] Derive the default output filename from the inputfile

* [chore] Add .minijuvix-build to .gitignore
2022-05-30 17:46:17 +02:00
Jonathan Cubides
f16570e546
Add the termination checker to the pipeline (#111)
* [WIP] EntryPoint now has options. --no-termination is a new global opt.

* Add TerminationChecking to the pipeline

* Add TerminationChecking to the pipeline

* Keep GlobalOptions in App

* Fix reviewer's comments

* delete unnecessary parens

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2022-05-30 13:40:52 +02:00
janmasrovira
58534b8240
Use Interval in GenericError (#125) 2022-05-27 01:27:19 +02:00
Jonathan Cubides
a4eb2124b2
Generic Errors and refactoring (#123)
* w.i.p adoption of generic error type

* harmonize

* Remove the use of Error effect for internal bugs

* add location information to expression atom list

* Add GenericError instance for PatternAtoms

* Remove Maybe GenericError occurrences

* [ci] fix draft job's condition

* minor changes

* [stack] macos support ghc-opts

* Fix reviewer's comments

* remove accidentally commited file

* refactor to avoid duplication

* fix

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2022-05-26 17:52:08 +02:00
Jonathan Cubides
c7761100af
Add initial documentation (#119) (#120) (#121)
* Add initial docs generation website (#119)

* Add docs generation

* [makefile] add serve-docs target

* Fixed rebase conflicts

* Update pre-commit rev

* Added changelog
2022-05-23 16:56:59 +02:00
Jonathan Cubides
7e309eccdb
Add initial documentation (#119) (#120)
* Add initial docs generation website (#119)

* Add docs generation

* [makefile] add serve-docs target

* Fixed rebase conflicts

* Update pre-commit rev

* Added changelog
2022-05-23 16:20:02 +02:00
Jonathan Cubides
7e20e5083b
Add initial docs generation website (#119)
* Add docs generation

* [makefile] add serve-docs target
2022-05-20 16:16:16 +02:00
Jonathan Cubides
24d741922e
Add pre-commit, new policy for PRs and removal of dev in the CI#118)
* Remove dev. Add valid req.types for PRs. Add Concurrency

* [ci] Add pre-commit check

* [ci] w.i.p fixing when ci should trigger

* [ci] minor fix

* [ci] Fix pre-commit check
2022-05-20 10:45:03 +02:00
Paul Cadman
f987ef1c13
[doc] Fix internal link (#116)
GitHub org renderer doesn't support internal links.
2022-05-19 23:05:29 +02:00
Paul Cadman
cfc11fecc5
Add minic-runtime for linking without libc (#113)
* [minic] Add minic-runtime for linking without libc

The C generated by minic now depends on `minic-runtime.h`. There are two
versions of this, one that depends on libc and one that doesn't (i.e standalone).

The standalone runtime implements the minimal set of functions required for
the tests to compile and run.

The standalone runtime also contains a copy of
https://github.com/wingo/walloc, a small memory allocator that's
indended for use with WASM.

The benefit of using the standalone runtime is that the resulting
binaries are much smaller. For example the Nat example compiles to about
24k WASM binary with libc, the standalone version is 2.8k.

This commit adds a dependency on
https://hackage.haskell.org/package/file-embed for finding the path to
the minic-runtime directory in tests. It does not add any additional
transitive dependencies to the project.
2022-05-19 09:48:23 +02:00
janmasrovira
50ea7373ee
Improve error generation and handling (#108)
* add face and handling of not in scope symbol error

* small fix

* generic errors wip

* add App effect

* format

* add flycheck-minijuvix

* use absolute paths and refactor

* fix dir0

* add generic error instances and improve some errors

* format

* qualify strings

* use AnsiText

* add ToGenericError instances for the type checker errors

* improve error message

* improve handling of parsing errors
2022-05-18 17:10:10 +02:00
Paul Cadman
5b38727d39
Support uncurried higher order functions (#110)
* [minic] Translate TypeFunction to a C function pointer

* [minic] Add define macros for nullary functions

For example in the translation of:

inductive Nat {
  zero : Nat;
  suc : Nat → Nat;
};

The zero constructor is translated to a nullary C function:

static inline Nat_13_t * new_Zero_14_nullary()

and a macro:

\#define new_Zero_14 (new_Zero_14_nullary())

so that it can be referenced subsequently by the unapplied name
'new_Zero_14'.

A similar translation is applied to nullary top-level functions.

This means that uncurried higher-order functions now work.

* [chore] ormolu and hlint fixes

* [minic] Implement PR review suggestions

* [chore] Fix formatting
2022-05-17 15:12:36 +01:00
Paul Cadman
5ed3ef34c0
[cbackend] run minic tests with clang+wasi-sdk (#105)
* [cbackend] run minic tests with clang+wasi-sdk

* [docs] Add docs for setting up clang+wasi-sdk

* [doc] Updates README usage with clang

* [docs] Fix LLVM URL in README

* [docs] Fix README

* [doc] Update clang setup docs with wasm-ld
2022-05-16 16:17:28 +01:00
janmasrovira
f759f2a307
Highlight comments correctly (#106)
* highlight comments correctly

* add minijuvix.yaml files
2022-05-13 18:11:30 +02:00
janmasrovira
6bf0b1a839
Fix highlight command for modules with import statements (#102)
* fix highlight

* Add minijuvix.yaml to test directories

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2022-05-13 16:17:26 +02:00
janmasrovira
bd4ea3e54b
Support multiple modules in compilation (#100)
* translate MiniJuvix import statements to MicroJuvix include statements
2022-05-13 11:44:06 +02:00
Paul Cadman
a608e26e6a
[docs] Add usage example and move emacs docs (#96) 2022-05-13 09:40:04 +02:00
Jonathan Cubides
f9d9b10fc9
New target syntax and modular VP examples (#92)
* New target syntax and modular VP examples

* [ .gitignore ] updated

* Fix spaces new lines

* Remove outdated lab folder
2022-05-06 12:45:09 +02:00
janmasrovira
a24e0379d3
87 refactor warning related stuff (#91)
* remove all field selectors

* add local type signatures

* delete Wno-monomorphism-restriction and fix warnings

* [tests] inline two error messages

* remove Wno-missing-exported-signatures

* remove Wno-all-missed-specialisations

* remove Wno-missed-specialisations
2022-05-06 11:48:07 +02:00
Jonathan Prieto-Cubides
cb8e0fb911 v0.1.3 Update CHANGELOG 2022-05-05 18:37:06 +02:00
Jonathan Cubides
3004d1a404
Stricter stack builds and pedantic mode for CI (#78)
* Make CI even more pedantic

* remove aeson dependency

Co-authored-by: Paul Cadman <pcadman@gmail.com>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2022-05-05 15:21:04 +01:00
Paul Cadman
1d236f7007
[parser] Remove agda backend code (#86) 2022-05-05 15:11:18 +01:00
Paul Cadman
60236e7b58
Add C code generation backend (#68)
* [cbackend] Adds an AST for C

This should cover enough C to implement the microjuvix backend.

* [cbackend] Add C serializer using language-c library

We may decide to write our own serializer for the C AST but this
demonstrates that the C AST is sufficient at least.

* [cbackend] Declarations will always be typed

* [cbackend] Add CPP support to AST

* [cbackend] Rename some names for clarity

* [cbackend] Add translation of InductiveDef to C

* [cbackend] Add CLI for C backend

* [cbackend] Add stdbool.h to file header

* [cbackend] Allow Cpp and Verbatim code inline

* [cbackend] Add a newline after printing C

* [cbackend] Support foreign blocks

* [cbackend] Add support for axioms

* [cbackend] Remove code examples

* [cbackend] wip FunctionDef including Expressions

* [parser] Support esacping '}' inside a foreign block

* [cbackend] Add support for patterns in functions

* [cbackend] Add foreign C support to HelloWorld.mjuvix

* hlint fixes

* More hlint fixes not picked up by pre-commit

* [cbackend] Remove CompileStatement from MonoJuvix

* [cbackend] Add support for compile blocks

* [cbackend] Move compileInfo extraction to MonoJuvixResult

* [minihaskell] Fix compile block support

* [chore] Remove ununsed isBackendSupported function

* [chore] Remove unused imports

* [cbackend] Use a Reader for pattern bindings

* [cbackend] Fix compiler warnings

* [cbackend] Add support for nested patterns

* [cbackend] Use functions to instantiate argument names

* [cbackend] Add non-exhaustive pattern error message

* [cbackend] Adds test for c to WASM compile and execution

* [cbackend] Add links to test dependencies in quickstart

* [cbackend] Add test with inductive types and patterns

* [cbackend] Fix indentation

* [cbackend] Remove ExpressionTyped case

https://github.com/heliaxdev/minijuvix/issues/79

* [lexer] Fix lexing of \ inside a foreign block

* [cbackend] PR review fixes

* [chore] Remove unused import

* [cbackend] Rename CJuvix to MiniC

* [cbackend] Rename MonoJuvixToC to MonoJuvixToMiniC

* [cbackend] Add test for polymorphic function

* [cbackend] Add module for string literals
2022-05-05 14:12:17 +01:00
janmasrovira
077e53cfb1
84 monomorphisation naming inconsistency (#85)
* fix monomorphisation of constructor applications in patterns

* clean code

* hlint
2022-05-05 13:10:14 +02:00
Jonathan Cubides
7b1371c4b9
Change terminating keyword behavior (#82) 2022-05-04 18:17:16 +02:00
janmasrovira
8146b2a91d
[monojuvix] remove unused constructor ExpressionTyped (#80) 2022-05-04 18:03:59 +02:00
Jonathan Cubides
2b4cc3ee36
Add automatically updates/issues/merged PRs to the changelog (#74)
* [ .gitignore ] updated

* Add updated changelog waiting for new PRs

* Fixed minor typos
2022-05-04 14:06:29 +02:00
Jonathan Cubides
038042b733
Add terminating keyword (#71)
* Parsing terminating keyword

* cosmetics

* Add support for `terminating` keyword to function decl.

* Minor replacement

* Fix .mjuxix to .mjuvix and the module name
2022-05-04 14:05:58 +02:00
janmasrovira
13ce663fe1
bump stackage version and remove allow-newer (#76)
* bump stackage version and remove allow-newer

* update ci

* [chore] Invalidate CI cache

Co-authored-by: Paul Cadman <git@paulcadman.dev>
2022-05-04 12:57:42 +02:00
Jan Mas Rovira
fe8969b074 [monojuvix] properly print constructor parameters as atoms 2022-05-04 12:14:42 +02:00
janmasrovira
3acade4072
Monomorphization (#70)
* add TypeCallsBuilder and others

* implement propagation of type calls

* improve type propagation

* polymorphize fungible token

* sort type calls map pretty output

* use HashSet in TypeCallsMap

* renaming

* rename module

* improve indexing in type propagation

* draft monomorphization generation algorithm

* fix draft

* wip mono code generation

* wip code generation

* finish first candidate for code generation

* add monojuvix command

* fix MonoJuvix pretty printer to properly display name ids

* [monojuvix] improve clause pretty printing

* add support for function types in expressions

* properly translate function expressions

* ormolu

* add a basic positive test for monomorphization

* cleanup effect constraints

* collect type applications in axiom types

* apply some style improvements

* fix PolySimpleFungibleToken and add it to the test suite

* ignore polymorphic inductive definitions that are never used
2022-05-04 10:50:03 +02:00
Paul Cadman
c694388c9c
Merge pull request #69 from heliaxdev/rm-statement-compile
Remove StatementCompile in AST after scoping
2022-04-29 15:05:27 +01:00
Paul Cadman
541a9771d2 [chore] Remove StatementCompile in AST after scoping
The scoped -> abstract translation does not emit StatementCompile and so
any code dealing with StatementCompile after scoping was no-op.
2022-04-29 14:14:23 +01:00
janmasrovira
7392e8cc20
check if stderr supports ANSI and print accordingly (#67) 2022-04-29 12:18:09 +02:00
Paul Cadman
dc6fce8820
Add support for compile (by Jonathan) (#66)
* Add support for compile (by Jonathan)

* Remove error related to unsopported backend

Co-authored-by: Jonathan Prieto-Cubides <jonathan.cubides@uib.no>
2022-04-28 17:42:15 +02:00
janmasrovira
fb2999eaf1
add NameIdGen effect to the pipeline (#64)
* add NameIdGen effect to the pipeline

* run ormolu
2022-04-25 12:33:04 +02:00
janmasrovira
956b2ba828
Make the --show-name-ids flag global (#63)
* make flag --show-name-ids global

* make use of --show-name-ids flag in the termination commands
2022-04-25 10:40:24 +02:00
janmasrovira
ba47f11189
Implement type checker with polymorphism (#62) 2022-04-22 10:06:34 +02:00
Paul Cadman
c99c1825d1
[emacs] Add copy of agda-input to minijuvix-mode (#57)
This provides agda-input method (under the name `minijuvix`) to
minijuvix-mode.
2022-04-11 17:11:31 +02:00
janmasrovira
c823efb501
remove undefined (#56) 2022-04-11 16:20:26 +02:00
janmasrovira
66c0403544
Merge pull request #53 from heliaxdev/issue29
closes #29
2022-04-11 13:33:26 +02:00
Jan Mas Rovira
bcc18dd204 run ormolu 4 2022-04-11 13:27:57 +02:00
Jan Mas Rovira
48aadbcf3b make my friends hlint and ormolu happy 2022-04-11 13:23:55 +02:00
Paul Cadman
721ea4612d [test] Add Anoma Haskell backend for VP 2022-04-11 13:17:13 +02:00
Paul Cadman
d023ced9e4 [test] Update VP example 2022-04-11 13:17:13 +02:00
caryoscelus
3d3ba9d282 emacs mode: keep buffer saved after highlighting 2022-04-11 13:17:13 +02:00
Jan Mas Rovira
464749de5a fix #29 2022-04-11 13:08:37 +02:00
Paul Cadman
caf4065644 [test] Add Anoma Haskell backend for VP 2022-04-11 11:09:45 +02:00