Move backend relations to compiler/backend/languages/relations

CakeML / pure

A verified compiler for a lazy functional language

Other

31 stars 4 forks source link

Move backend relations to compiler/backend/languages/relations #35

Open myreen opened 1 year ago

myreen commented 1 year ago

This issue is about moving all syntactic relations to compiler/backend/languages/relations.

In that directory:

each file should only have one syntactic relation it "exports"
each file has 3 sections:
1. the definition of relation of interest from outside
2. the proofs (for internal use to this file only, can be local)
3. the from outside interesting thm
naming conventions:
- file name should start with language name
- exported exp_rel should have descriptive short name (not exp_rel)

hrutvik commented 1 year ago

Also, pure_letrec_{seq,spec}Theory/pure_inlineTheory/pure_demandTheory should really be moved from meta-theory to join the other compiler relations