lawcho/c-in-agda

Subset of C embedded in Agda

A subset of C embedded in Agda

What's included

• An imperative Agda EDSL with C-like syntax
  • while loops, variables, arithmetic, if_then_else, and more
  • Simple types
  • Lightweight definition using PHOAS
• Heavy syntactic sugar for C emulation
• A handful of examples
• An interpreter
  • Pure, so can run in agda-mode
  • Type-safe, thanks to András Kovács's ST monad implementation
• An algebraic-effect library

What's not included

• Support for C functions
• A pretty-printer to C

Dependencies

• Agda (tested with Agda version 2.6.4-fc88821)
• Agda standard library (tested with git revision 833f0facb24151c82c50bdb2359d648cce9f9661)

Copying

Copying welcome.

Unless stated otherwise, all code is own work & public domain.