1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-15 10:03:22 +03:00
Commit Graph

51 Commits

Author SHA1 Message Date
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
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
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
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
Jonathan Cubides
7b1371c4b9
Change terminating keyword behavior (#82) 2022-05-04 18:17:16 +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
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
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
ba47f11189
Implement type checker with polymorphism (#62) 2022-04-22 10:06:34 +02:00
Paul Cadman
caf4065644 [test] Add Anoma Haskell backend for VP 2022-04-11 11:09:45 +02:00
Paul Cadman
498c6ab087 [test] Update VP example 2022-04-11 11:09:45 +02:00
Jonathan Prieto-Cubides
86162090ce merging conflicts 2022-04-07 12:13:03 +02:00
Paul Cadman
3af9cb95ac
Restore correct handling of TypeAny and add positive typecheck tests (#34)
* [ format ] AbstractToMicroJuvix

* [ CI ] fixes

* [ CI ] fixes

* [ CI ] Using GHC 9.0 for Hlint

* [ CI ] Use static-checks for Dev as well

* [test] Add positive test for typechecker

* [test] Improve positive typechecker error output

* [typecheck] Restore correct handling of TypeAny

I mistakenly removed the matchTypes function in
https://github.com/heliaxdev/minijuvix/pull/22. This caused the handling
of TypeAny to break.

Literals have type TypeAny and so should be valid when matching against
any other type. The tests have been updated to reflect this.

* [test] Add positive MicroJuvix typecheck tests

* [ ormolu ] fixes

Co-authored-by: Jonathan Prieto-Cubides <jonathan.cubides@uib.no>
2022-04-05 22:02:03 +02:00
Jonathan Prieto-Cubides
4d918cd1fd [ CI ] New jobs: ormolu and hlint 2022-04-05 19:57:21 +02:00
Jan Mas Rovira
5f9887e69c define ParserResult and refactor 2022-04-05 16:12:13 +02:00
Jan Mas Rovira
22b5de42f3 setup InfoTable for parser 2022-04-05 00:46:04 +02:00
Jonathan Cubides
3fe3cc4305
Merge branch 'main' into dev 2022-04-04 19:11:26 +02:00
Jonathan Prieto-Cubides
a224d94709 [ pre-commit ] Add support and hooks 2022-04-04 17:44:08 +02:00
Jonathan Cubides
fd3622a274
Adds many new features (w.i.p v0.1.2) (#28)
* add references to the syntax and cleanup code

* [make] add .PHONY to Makefile targets

* [parser] add parser / pretty for axiom backends

* Pairing progress

* [scoper] Add support for Axiom backends

* [parser] Fix foreign block parsing

* [ app ] adds --no-colors flag for the scope command

* [ghc] upgrade to ghc 9.2.2

* use GHC2021

* [doc] Remove out-of-date comment

* [test] Add ambiguity tests

* [scoper] Improve resolution of local symbols

* [error] WIP improving ambiguity error messages

* [ clean-up ] new lab folder for experimentation

* [ app ] ixes the lint warning

* [ Termination ] removes Alga dependency

* [error] Add message for ambiguous symbol error

* [error] Add ambiguous module message

* [scoper] Remove ErrGeneric

* [test] Add test to suite

* [test] show diff when ast's are different

* [ lab ] folder organization

* [ Makefile ] add targets with --watch option (stack cmds) and remove unused things

* [ app ] add --version flag and fixed warnings and formatting

* [test] remove fromRightIO to fix ambiguity error

* [test] Add test of shadowing public open

* [scoper] Add visibility annotation for Name

* prepare buildIntoTable

* [ Concrete ] add instance of hashable for refs.

* add InfoTableBuilder effect

* [ scoper ] add InfoTableBuilder effect

* [ CHANGELOG ] updated v0.1.1

* [ README ] org version now

* fix package.yaml

* fix readme

* [microjuvix] implement basic typechecker

* add simple test for MicroJuvix type checker

* fix checking for constructors apps in patterns

* [scope] Move InfoTable to a new module

* [abstract] Make Iden use references instead of Name

* [abstract] Add InfoTable for abstract syntax

* [scoper] Add function clauses to scoped InfoTable

* [abstract] Add InfoTableBuilder for scoped to abstract

* [main] Fix callsites of translateModule

* [doc] Remove empty docs

* [scoper] Update emptyInfoTable with missing field

* rename some functions

* [minihaskell] add compilation to MiniHaskell

* [microjuvix] improve wrong type message

* Add a validity predicate example written in MiniJuvix

* [typecheck] Add error infrastructure for type errors

Add a pretty error for mismatched constructor type in a pattern match

* [test] Adds negative typecheck test for constructor

* [app] Adds microjuvix subcommands for printing / typechecking

* [typecheck] Add error message for ctor match args mistmatch

* [typecheck] Add descriptive messages for remainng errors

* [typecheck] Updates to error message copy

* [typecheck] fix merge conflicts:

* [highlight] add basic support for highlighting symbols

* [minijuvix-mode] add minijuvix-mode and basic description in the readme

* [readme] improve formatting

* automatically detect the root of the project and add --show-root flag

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Paul Cadman <pcadman@gmail.com>
2022-04-01 13:00:15 +02:00
Jan Mas Rovira
9708dd3fe3 [highlight] add basic support for highlighting symbols 2022-04-01 01:11:55 +02:00
Jonathan Prieto-Cubides
6ba1a4f4ff Add a validity predicate example written in MiniJuvix 2022-03-30 19:09:43 +02:00
Jan Mas Rovira
f121fe0d39 [minihaskell] add compilation to MiniHaskell 2022-03-30 16:03:56 +02:00
Jan Mas Rovira
153ebe36a2 add simple test for MicroJuvix type checker 2022-03-29 09:46:26 +02:00
Jonathan Cubides
de6fabf625
v0.1.1 (#15)
* add references to the syntax and cleanup code

* [make] add .PHONY to Makefile targets

* [parser] add parser / pretty for axiom backends

* Pairing progress

* [scoper] Add support for Axiom backends

* [parser] Fix foreign block parsing

* [ app ] adds --no-colors flag for the scope command

* [ghc] upgrade to ghc 9.2.2

* use GHC2021

* [doc] Remove out-of-date comment

* [test] Add ambiguity tests

* [scoper] Improve resolution of local symbols

* [error] WIP improving ambiguity error messages

* [ clean-up ] new lab folder for experimentation

* [ app ] ixes the lint warning

* [ Termination ] removes Alga dependency

* [error] Add message for ambiguous symbol error

* [error] Add ambiguous module message

* [scoper] Remove ErrGeneric

* [test] Add test to suite

* [test] show diff when ast's are different

* [ lab ] folder organization

* [ Makefile ] add targets with --watch option (stack cmds) and remove unused things

* [ app ] add --version flag and fixed warnings and formatting

* [test] remove fromRightIO to fix ambiguity error

* [test] Add test of shadowing public open

* [scoper] Add visibility annotation for Name

* prepare buildIntoTable

* [ Concrete ] add instance of hashable for refs.

* add InfoTableBuilder effect

* [ scoper ] add InfoTableBuilder effect

* [ CHANGELOG ] updated v0.1.1

* [ README ] org version now

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Co-authored-by: Paul Cadman <git@paulcadman.dev>
2022-03-25 18:16:34 +01:00
Paul Cadman
2ec85d39a4 [test] Add test of shadowing public open 2022-03-25 09:30:05 +00:00
Paul Cadman
339cc24541 [scoper] Improve resolution of local symbols 2022-03-24 10:28:15 +00:00
Paul Cadman
86110e063a [test] Add ambiguity tests 2022-03-24 10:22:03 +00:00
Paul Cadman
f527143e67 [parser] Fix foreign block parsing 2022-03-23 15:34:08 +00:00
Paul Cadman
20dfb7b736 [scoper] Add support for Axiom backends 2022-03-23 15:05:52 +00:00
Jan Mas Rovira
c6e3c99225 [scoped] add ScopedIden 2022-03-18 10:16:43 +01:00
Jan Mas Rovira
fa95f8be82 separate MiniHaskell into MicroJuvix and 'new' MiniHaskell 2022-03-17 18:18:10 +01:00
Jan Mas Rovira
fee0055ea0 parse and scope 'foreign' and 'compile' statements 2022-03-16 23:40:44 +01:00
Jan Mas Rovira
09303131a8 [test] improve test for literals 2022-03-16 12:42:06 +01:00
Jan Mas Rovira
271464df04 add integer and string literals 2022-03-15 12:37:33 +01:00
Jonathan Prieto-Cubides
7f501de774 [ tests ] added example about ordinals 2022-03-08 13:25:17 +01:00
Jonathan Prieto-Cubides
02c17c1d1f [ tests ] Uppercase type variables 2022-03-07 17:59:18 +01:00
Jonathan Prieto-Cubides
9ed5db7243 [ tests ] fixed definitions for flat and aux 2022-03-07 17:16:45 +01:00
Jonathan Prieto-Cubides
19c15a1a8e [ tests ] Adds some example of mutual recursion to test the termination checker 2022-03-07 16:39:14 +01:00
Jan Mas Rovira
f7b3d6042f [termination] implement callgraph using sets 2022-03-05 13:32:47 +01:00
Jan Mas Rovira
d6dda61e12 [termination] implement lexical order search 2022-03-04 02:13:43 +01:00
Jan Mas Rovira
95c7e6fa10 [tests] add ackermann function 2022-02-24 01:33:26 +01:00
Jan Mas Rovira
4b16e08b8d add some test files aimed at termination checking 2022-02-24 00:36:22 +01:00
Jan Mas Rovira
7ec3fede62 [tests] fix definition of Data.List.filter 2022-02-24 00:31:21 +01:00
Jan Mas Rovira
a8d7f183b8 [tests] add test for parenthesized operators: (+) 2022-02-23 10:59:56 +01:00
Jan Mas Rovira
3124052807 [tests] add more positive tests from the stdlib 2022-02-18 22:02:57 +01:00
Jan Mas Rovira
3ead694533 [tests] add test for a fragment of stdlib Data.List 2022-02-18 17:57:04 +01:00
Jan Mas Rovira
bdd155d712 [tests] add support for mocked file system in scope checker. Useful for multi
file tests
2022-02-18 17:48:21 +01:00