Commit Graph

400 Commits

Author SHA1 Message Date
Louis Gesbert
ba9fc85b84 Make exception output consistent across the interpreters 2024-02-26 14:56:43 +01:00
Louis Gesbert
e0928677b1 Small ocaml/js output rehaul
Print to json directly rather than depend on yojson and a ppx.

Note: this should be tested with the website in order to validate that the Json
output is 1-to-1.
(a second step could be to simplify this output, now that it's manual)
2024-02-21 11:28:56 +01:00
Louis Gesbert
afcc435593 CI: fix the check for bad promoted files 2024-02-12 16:44:14 +01:00
Louis Gesbert
721597a70d Small additional simplification 2024-02-12 15:39:29 +01:00
Louis Gesbert
e308ff8d02 Generalise the definition of lists of nested binders 2024-02-09 18:33:41 +01:00
Louis Gesbert
ea512bfd5b The typer doesn't handle monomorphised code yet
so don't retype after monomorphisation, which is now possible as the pass itself
correctly preserves types.

In time the typer will need a special case to get knowledge of the new types and
modified operator types.
2024-02-06 18:00:45 +01:00
Louis Gesbert
df70c5dd57 Simplify monomorphisation, and preserve type annotations 2024-02-06 18:00:25 +01:00
Louis Gesbert
870716a3f8 Factorise a bit more with more arguments to Expr.map
allowing a safer way to translate types both in expressions and annotations, and
clarifying the code of the dcalc->lcalc translation
2024-02-05 16:28:56 +01:00
Denis Merigoux
afa8ee44bf
Delete duplicate code from 9d3550374d 2024-02-01 17:23:31 +01:00
Denis Merigoux
d7e71885c1
Formatting 2024-02-01 17:22:42 +01:00
Louis Gesbert
f90de90299 Monomorphisation: access types directly 2024-02-01 12:27:54 +01:00
Louis Gesbert
2dba54b906 Monomorphisation: simplify type collection 2024-02-01 12:22:31 +01:00
Louis Gesbert
9d3550374d Remove constructor matching on strings 2024-02-01 12:17:51 +01:00
Louis Gesbert
cfdaf94989 Define Type.Map 2024-02-01 10:10:25 +01:00
Louis Gesbert
e47a1fc220 Improve translation of typing upon dcalc -> lcalc
A little bit of effort enables us to propagate valid typing annotations, making
subsequent typing re-inference easier (and avoiding a traversal just to remove
type annotations)
2024-01-31 19:15:27 +01:00
Louis Gesbert
7a4ac4364b Mark closure conversion as untyped
since it doesn't correctly propagate and update types. (Ideally it would, but
otherwise it would be better to remove the type annotations on the fly instead
of introducing wrong ones then cleaning them up).
2024-01-31 17:52:06 +01:00
Denis Merigoux
b48fb0e223
Array compilation to C is OK 2024-01-26 20:15:32 +01:00
Denis Merigoux
8a139f6a3c
Work on arrays 2024-01-22 16:49:58 +01:00
Denis Merigoux
5310e47e5b
Fix monomorphization problems with [TAny] left 2024-01-17 16:03:20 +01:00
Denis Merigoux
0a8fdde7de
Fix monomorphization 2024-01-17 14:02:32 +01:00
Denis Merigoux
a1ab58478c
Remove useless field 2024-01-17 11:29:39 +01:00
Denis Merigoux
9f03b6b931
Merge branch 'master' into c_backend
Some tests still failing...
2024-01-15 17:19:17 +01:00
Denis Merigoux
919dd2b812 Monomorphization properly done 2023-12-20 17:45:39 +01:00
Denis Merigoux
dcd883e53c
Uppercase constructors 2023-12-19 17:40:38 +01:00
Louis Gesbert
d3e7c565a9 Closure conversion: use multiple let-in 2023-12-19 17:30:32 +01:00
Louis Gesbert
a2efc94fd2 Register the option type in ctx when used in lcalc 2023-12-19 17:30:28 +01:00
Louis Gesbert
2823795f9f AST change: more specific application
As part of making tuples first-class citizens, expliciting the arity upon
function application was needed (so that a function of two args can
transparently -- in the surface language -- be applied to either two arguments
or a pair).

It was decided to actually explicit the whole type of arguments because the cost
is the same, and this is consistent with lambda definitions.

A related change done here is the replacement of the `EOp` node for operators by
an "operator application" `EAppOp` node, enforcing a pervasive invariant that
operators are always directly applied. This makes matches terser, and highlights
the fact that the treatment of operator application is almost always different
from function application in practice.
2023-12-19 17:27:40 +01:00
Denis Merigoux
9d9a2c4496
Start to implement proper monomorphization 2023-12-19 17:26:17 +01:00
Denis Merigoux
85bbb7be1c
Add monomorphizing option 2023-12-19 15:01:06 +01:00
Denis Merigoux
9358ad945e
Better type translation in closure conversion 2023-12-19 14:31:57 +01:00
Denis Merigoux
0323e71edb
Default types should be eliminated in compile_with_exceptions 2023-12-18 15:23:08 +01:00
Louis Gesbert
7160093682 Allow scope execution in compiled ocaml executables 2023-12-06 11:06:54 +01:00
Louis Gesbert
3649f92975 Rework resolution of module elements
This changes the `decl_ctx` to be toplevel only, with flattened references to
uids for most elements. The module hierarchy, which is still useful in a few
places, is kept separately.

Module names are also changed to UIDs early on, and support for module aliases
has been added (needs testing).

This resolves some issues with lookup, and should be much more robust, as well
as more convenient for most lookups.

The `decl_ctx` was also extended for string ident lookups, which avoids having
to keep the desugared resolution structure available throughout the compilation
chain.
2023-11-30 21:14:12 +01:00
Louis Gesbert
645c263ccc Fix closure-conversion
Joint debugging with @denismerigoux :)
2023-11-28 11:18:41 +01:00
Louis Gesbert
cf89204a4b Reformat 2023-11-27 11:17:38 +01:00
adelaett
a734413d39 typing default: fix ocaml runtime when using eoption 2023-11-27 11:17:38 +01:00
adelaett
576da177c5 Typed defaults: translate types in scope lets as well in the new
compile without exception passe
2023-11-27 11:12:35 +01:00
adelaett
1d72a57da4 Typed default: fix an issue to the error_on_empty constructor 2023-11-27 11:09:08 +01:00
adelaett
4a5335162e Typed default: implementing the type for handle defaults, as well as the
compile without exceptions compilation pass, using the newly found
invariant
2023-11-27 11:09:08 +01:00
adelaett
b0b83b14b9 Typed default: Implemented typing translating to the without exception compilation path. 2023-11-27 11:09:08 +01:00
adelaett
2c9f8ad8b1 Typed default: import the code from compile with exceptions to
re-implement without exceptions with the new typing of defaults terms.
2023-11-27 11:09:08 +01:00
Louis Gesbert
1efda5ca22 Typing defaults: support nested priorities
The way nested priorities are encoded use `< < excs | true :- nested > :- x >`,
which imply that `nested` can actually be ∅ ; to cope with this, the typing of
default terms is made more generic (the return type is now the same as the
`cons` type `'a`, rather than `<'a>`). For the general case, we add an explicit
`EPureDefault` node which just encapsulates its argument (a `return`, in monad
terminology).
2023-11-27 11:09:08 +01:00
Louis Gesbert
c4715ea86e Reformat 2023-11-27 11:09:08 +01:00
Louis Gesbert
bcf285913e Typing the HandleDefault operator 2023-11-27 11:06:33 +01:00
Louis Gesbert
ab6bec390d Adjust plugins and warnings 2023-11-27 11:06:16 +01:00
Louis Gesbert
4bce4e6322 Reformat 2023-09-27 13:14:38 +02:00
Louis Gesbert
f162f6e9bd Improve handling of module name definitions
and add some sanity-checks for consistency of used modules w.r.t. actually
loaded modules.
2023-09-27 13:14:03 +02:00
Louis Gesbert
63773e48b5 Update tests outputs 2023-09-27 13:08:15 +02:00
Louis Gesbert
bf048f0a74 Add a lightweight lexer for dependency extraction in Clerk
The base is there but not fully used yet in Clerk
2023-09-27 13:08:15 +02:00
Denis Merigoux
9cecf5587a
Register surface syntax languge in program troughout the compilation chain 2023-09-22 18:05:26 +02:00