Olivier
|
00bf829884
|
[WIP] equations environment using a union-find.
|
2023-02-12 18:24:31 +01:00 |
Olivier
|
3d51f8eb5a
|
[WIP] equations environment using a Hashtbl, but might not be a good idea !
|
2023-02-11 13:08:12 +01:00 |
Olivier
|
dbfc403051
|
WIP
|
2023-02-10 17:14:42 +01:00 |
Olivier
|
7e60ddf5f3
|
Not sure that it is correct.
|
2023-02-10 17:14:33 +01:00 |
Olivier
|
37bfb749ea
|
Not sure that this is necessary.
|
2023-02-10 17:14:33 +01:00 |
Olivier
|
033138d8b1
|
Generalization uses abstract structures for rigids variables.
|
2023-02-10 17:14:33 +01:00 |
Olivier
|
8e6a82de4b
|
Abstract structure.
|
2023-02-10 15:50:37 +01:00 |
Olivier
|
c27ea1669c
|
Add a scope type in the data.
|
2023-02-10 15:50:37 +01:00 |
Olivier
|
9b810e6090
|
Break a line.
|
2023-02-10 15:50:37 +01:00 |
Olivier
|
955f22773c
|
Typo.
|
2023-02-10 15:50:37 +01:00 |
Olivier
|
5f23395b5c
|
Add an UnboundTypeVariable error.
|
2023-01-26 14:30:09 +01:00 |
Olivier
|
0debfbb71b
|
More explicit error message printing.
|
2023-01-26 14:30:09 +01:00 |
Olivier
|
98ea579c6a
|
Remove unused equality check and change comments.
|
2023-01-26 14:30:09 +01:00 |
Alistair O'Brien
|
5bd10c668c
|
Apply 1 suggestion(s) to 1 file(s)
|
2023-01-26 14:30:09 +01:00 |
Olivier
|
bcb579eafc
|
Change 'int' to more correct 'nat' in the test suite.
|
2023-01-26 14:30:09 +01:00 |
Olivier
|
b9749e2b57
|
Add tests.
|
2023-01-26 14:30:09 +01:00 |
Olivier
|
a7006dcbb8
|
Smart constructors in TestF.ml.
|
2023-01-26 14:30:09 +01:00 |
Olivier
|
66c9de7c55
|
Add break in printing of annotations.
|
2023-01-26 14:30:05 +01:00 |
Olivier
|
eed3db1da6
|
Comments in F.ml
These comments should appear in F.mli too, but I'm waiting for feedbacks before I copy-paste them.
|
2023-01-26 14:19:03 +01:00 |
Olivier
|
384f9ac3c5
|
Add Refl / Use in System F.
The term Refl is a proof of a type equality TyEq(ty1,ty2) and Use is a construct that introduce a type equality in the typing context.
|
2023-01-26 14:18:59 +01:00 |
Olivier
|
473521d53a
|
Add absurd in F.
|
2023-01-26 14:16:53 +01:00 |
Olivier
|
784bb81952
|
Equality between types always uses graph translation.
|
2023-01-26 14:16:53 +01:00 |
Olivier
|
6946340570
|
Define type equalities in [Structure.ml].
This will be useful when we translate System F terms to graphs (a "structure" node of the graph will be represented by a Structure.structure).
|
2023-01-26 14:16:53 +01:00 |
Olivier
|
36980073f3
|
Add type equality in F.
|
2023-01-26 14:16:53 +01:00 |
Olivier
|
36bad208b0
|
Remove unused type declaration.
|
2023-01-26 14:16:53 +01:00 |
François Pottier
|
6fe129a761
|
Rename [STRUCTURE_OPT] to [GSTRUCTURE_OPT].
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
a431a97a4b
|
Comment.
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
f59698102e
|
Rename [OCSTRUCTURE] to [OSTRUCTURE].
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
9aedc2d4b5
|
Rename [OSTRUCTURE] to [DSTRUCTURE].
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
e6836149ca
|
Comment.
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
23cc9f785d
|
Some renamings and comments.
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
99a1694695
|
Rename SSTRUCTURE to STRUCTURE.
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
a709fca0b5
|
Decoder: fix and improve the documentation comment.
|
2022-12-26 22:55:01 +01:00 |
François Pottier
|
331fa6bc7d
|
Decoder: inline away [decode_id].
|
2022-12-26 22:55:01 +01:00 |
Gabriel Scherer
|
6d4443223d
|
remove is_leaf from the signature by moving variable decoding around
|
2022-12-26 22:55:01 +01:00 |
Gabriel Scherer
|
8dd21d7c36
|
Signatures.ml: remove STRUCTURE_LEAF as an intermediary abstraction
|
2022-12-26 22:55:01 +01:00 |
Gabriel Scherer
|
54021e46bd
|
simplify Signatures by requiring debug [pprint] everywhere
|
2022-12-26 22:55:01 +01:00 |
Gabriel Scherer
|
ea30d554e8
|
structure Signatures.ml with signature mixins
|
2022-12-26 22:55:01 +01:00 |
SCHERER Gabriel
|
56d987524c
|
Merge branch 'n-ary-fun-printing' into 'master'
Compact syntax for repeated abstractions and type abstractions.
See merge request fpottier/inferno!45
|
2022-11-22 15:41:56 +00:00 |
Olivier
|
d9ce1246e7
|
Improve printing of n-ary abstraction and type abstraction.
|
2022-11-22 12:07:55 +01:00 |
François Pottier
|
4b3e0aefb1
|
CHANGES.
|
2022-06-03 09:57:28 +02:00 |
POTTIER Francois
|
b680e870fe
|
Merge branch 'fix-bug-rigid' into 'master'
Fix a bug (incorrect assumption when using [letr1] in the client).
See merge request fpottier/inferno!43
|
2022-06-03 07:50:49 +00:00 |
Olivier
|
2dd89309c3
|
Fix a bug (incorrect assumption when using [letr1] in the client).
|
2022-05-19 13:00:29 +02:00 |
François Pottier
|
7e81ab63ef
|
TODO.
|
2022-04-08 11:17:16 +02:00 |
François Pottier
|
1940ed39e4
|
Documentation for [letr1] and [letrn].
|
2022-04-08 11:13:08 +02:00 |
François Pottier
|
a1dc9edf20
|
Add documentation comments.
|
2022-04-08 10:48:14 +02:00 |
François Pottier
|
21fe5539aa
|
Introduce type abbreviations for lists of things.
|
2022-04-08 10:38:08 +02:00 |
François Pottier
|
45cd7b266e
|
Comments.
|
2022-04-08 10:30:19 +02:00 |
François Pottier
|
0a3af39d42
|
Update an internal comment.
|
2022-04-08 10:27:18 +02:00 |
François Pottier
|
654532a4a7
|
Use two lists instead of a list of pairs in [CLet].
|
2022-04-08 10:13:40 +02:00 |