Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Typeclass lang #76

Open
wants to merge 172 commits into
base: master
Choose a base branch
from
Open

Typeclass lang #76

wants to merge 172 commits into from

Conversation

Gordon-Sau
Copy link

  • Define a new type system that supports type classes. Because the new typeclassLang
  • As it is not completed yet, and the type system is quite different from the original type system, I put everything that is updated in typeclass/ so we don't have to break existing proofs.
  • The type soundness proof for NestedCase is still WIP and is currently cheated.

Gordon-Sau and others added 30 commits October 7, 2023 14:33
@Gordon-Sau
typeclass parsing: copy parsing from pure and change pureAST
9dbda8c
@Gordon-Sau
typeclass typing: copy pure_tcexp and pure_typing
b9a03e7 
typeclass tcexp: add Predtype to each expression
@Gordon-Sau
Merge remote-tracking branch 'origin/master' into typeclassLang
88a2a9e
@Gordon-Sau
typeclass kind_check: add an inductive set for kind_checking
1225587
@Gordon-Sau
typeclass: fixing holmake errors
8bd5a3a
@Gordon-Sau
typeclass: update type system, add kind check and pure_tcexp
5301eac
@Gordon-Sau
typeclass: update AST to support class and instance declarations
e9be6bf
@Gordon-Sau
typeclass: complete most of ast_to_cexp
00d42de
@Gordon-Sau
typeclass: add helper functions and lemmas in tcexp
199ad32
@Gordon-Sau
typeclass: update ast_to_cexp
792c135
@Gordon-Sau
tcexp: remove unnecessary keys in instinfo
68f8463
@Gordon-Sau
ast_to_cexp: transform all usage of finite map to mlmap
f672e3f
@myreen @Gordon-Sau
Move letrecs_distinct_def and Lets_def up
3e750b8
@myreen @Gordon-Sau
Make letrecs_distinct_def into an automatic simp
b1b1552
@myreen @Gordon-Sau
Move some definitions upwards
600e940
@hrutvik @Gordon-Sau
Delete some unnecessary dependencies in pure_tcexpTheory
7e97a54
@myreen @Gordon-Sau
Update translation for moves
a784aad
@myreen @Gordon-Sau
Tweak pure_pres
b56f03b
@myreen @Gordon-Sau
Tidy up some thunkLang files
55fceea
@myreen @Gordon-Sau
Fix App_Lam rule in bidir
b1dee19
@myreen @Gordon-Sau
Fix a broken proof (in an unused file)
4b2d955
@hrutvik @Gordon-Sau
Pass in numbers on command line
d8e147e
@hrutvik @Gordon-Sau
Fix a breakage
cb19eaf
@hrutvik @Gordon-Sau
Remove some test code
f706862
@myreen @Gordon-Sau
Delete unused things
604c23c
@myreen @Gordon-Sau
Remove Rec and rename to inline_rel
6be18ed
@myreen @Gordon-Sau
Remove rhs type
60ffb5e
@myreen @Gordon-Sau
Replace Binds with Lets
0795695
@myreen @Gordon-Sau
Define pre and tidy up proofs
6a549da
@myreen @Gordon-Sau
Remove boundvars from vars_of
0707363
Gordon-Sau and others added 27 commits June 30, 2024 14:32
@Gordon-Sau
complete the induction theorem for dictionary translation
5aed581
@Gordon-Sau
prove well-typedness of class_env_construct_dict
6c5dfb4
@hrutvik
Merge branch 'master' into typeclassLang
79e3fed
@hrutvik
Add type class work to regression + top-level Holmakefile
86f5f1a
@Gordon-Sau
Merge branch 'typeclassLang' of github.com:CakeML/pure into typeclass…
a14f29c 
…Lang
@Gordon-Sau
typeclassLang: refactoring: updates the fintate maps to remove some s…
2cbd29b 
…ide conditions and turns some tuples to records
@Gordon-Sau
typeclassLang: update typing Proof
ee383ac
@Gordon-Sau
typeclassLang: update typing Proof
c0e9c5e
@Gordon-Sau
typeclassLang: update the definition of type_elaborate_prog and prog_…
cd168ee 
…construct_dict
@Gordon-Sau
typeclass: prove the superclass accessors in the translated lang is w…
d10134b 
…el-typed
@Gordon-Sau
typeclass: prove that the method accessors are well-typed and fix the…
b47bb86 
… distinctness condition for the variables in typeclasss_typing
@Gordon-Sau
typeclass: prove impls well-typed and default implementations are wel…
be11591 
…l-typed
@Gordon-Sau
update main theorem
ec17734
@Gordon-Sau
typeclass: complete typing translation proof
e43ed9b
@Gordon-Sau
typeclass: remove trailing whitespace
d748f02
@Gordon-Sau
typeclass: fix test_typeclass_typing
9692a2d
@Gordon-Sau
typeclass: fix typeclass_env_map_impl
33f341f
@Gordon-Sau
typeclass: remove cycle_detection as it is now in HOL
614c35c
@Gordon-Sau
typeclass: fix ast_to_cexp and fix texp_wf
beaad40
@Gordon-Sau
typeclass: small cleanup
43fcd63
@Gordon-Sau
typeclass: update destruct_type_cons
7ec1b34
@Gordon-Sau
typeclass: update definition of exhaustive_cepat
0bf0a37
@Gordon-Sau
typeclass: fix exhaustive_cepat
daaf2a6
@Gordon-Sau
typeclass: fix type_soundness_next
5f8e72d
@Gordon-Sau
typeclass: fix type_soundness_up_to Case
a7e79fb
@Gordon-Sau
typeclass: fix the file structure. Revert changes in typing/ and move…
186f8ca 
… pure_tcexp and pure_tcexp_lemmas to typeclass/typing/, and remove the files that are not updated in typeclass/, and move typeclass_env_map_impl to typing
@Gordon-Sau
typeclass: add a readme
8a5541a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hrutvik hrutvik Awaiting requested review from hrutvik hrutvik is a code owner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@Gordon-Sau @myreen @hrutvik @KacperFKorban @IlmariReissumies