README.md 761 Bytes
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
# λMC – monadic translation of mini C

Here is the list of notations used in λMC:

**Monadic part**
- `x ←ᶜ y ;;ᶜ z` and `x ;;ᶜ z`: bind
- `e1 |||ᶜ e2`: par

**C translation**
- `♯ l` and `♯ₗ l`: `return` of literals and locations
- `allocᶜ ( e1 , e2 )`: alloc
- `e1 =ᶜ e2`: assign
- `∗ᶜ e`: dereference
- `e1 ;ᶜ e2` sequence points
- `ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`
- `whileᶜ ( e1 ) { e2 }`
- `callᶜ ( f , a )`
- Binary and unary operations:
  + `e1 +ᶜ e2`
  + `e1 -ᶜ e2`
  + `e1 *ᶜ e2`
  + `e1 ≤ᶜ e2`
  + `e1 <ᶜ e2`
  + `e1 ==ᶜ e2`
  + `e1 !=ᶜ e2`
  + `~ᶜ e`
- Pointer arithmetic:
  + `e1 +∗ᶜ e2`: addition
  + `e1 <∗ᶜ e2`: comparison
- "Pre" operations:
  + `e1 +=ᶜ e2`
  + `e1 +∗=ᶜ e2`