search

sweirich / trellys

Automatically exported from code.google.com/p/trellys
46 stars 6 forks source link

Make a distiction between Pre-Core and Core languages. #23

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
The current Zombie Trellys implemention has a single typechecker/elaborator, 
working on a single datatype representing syntax. Split this into two 
datatypes, and have a seperate typechecker for the core. We still have an 
erased language also. 

Existing and planned features fit into this as follows:

Pre-Core:
 - Bidirectionally typechecked.
 - Infers arguments for underscores.
 - Convenient things like "morejoin", "casevar"
 - typechecked and elaborated into core

Core:
 - "unidirectionally" typechecked, completely annotated
 - no erased arguments or other convenience features
 - typechecked

Erased language:
 - No typechecker. Operational semantics is defined for this language only.

Original issue reported on code.google.com by vilhelm....@gmail.com on 4 Jul 2011 at 10:42

GoogleCodeExporter commented 9 years ago

Original comment by stephanie.weirich on 4 Jul 2011 at 11:01