Commit Graph

581 Commits

Author SHA1 Message Date
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