From 418eb24c7a365d2f980ad4734eb29129d6f8ecd4 Mon Sep 17 00:00:00 2001
From: Francesco Magliocca <franciman12@gmail.com>
Date: Fri, 20 May 2022 12:54:49 +0200
Subject: [PATCH] Start writing operational semantics

---
 docs/operational_semantics.md | 73 +++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 docs/operational_semantics.md

diff --git a/docs/operational_semantics.md b/docs/operational_semantics.md
new file mode 100644
index 0000000..0248f18
--- /dev/null
+++ b/docs/operational_semantics.md
@@ -0,0 +1,73 @@
+# milly's semantics
+
+We are going to define a desugared, restricted subset of `milly` called `core` for which we define an operational semantics.
+Afterwards a translation from the full syntax to the `core` is defined.
+
+## core
+
+For now we ignore ground types and their terms.
+
+Let us start by defining the `core` syntax:
+
+
+```
+t := t t                    (function application)
+   | \x. t                  (lambda abstraction)
+   | x                      (variable)
+   | true                   (bool literal)
+   | false                  (bool literal)
+   | let v = t in t         (let expression)
+   | (t_1, ..., t_n)        (tuple constructor)
+   | #n t                   (tuple projection)
+   | <alt: t>               (variant constructor)
+   | match t                (case expression)
+     {
+       <alt_1: x_1> -> t_1
+       ...
+       <alt_n: x_n> -> t_n
+     }
+```
+
+Values we consider:
+
+```
+v := \x. t           (Lambda function)
+   | true            (bool value)
+   | false           (bool value)
+   | <alt: v>        (variant value)
+   | (v_1, ..., v_n) (tuple value)
+```
+
+Types are:
+
+```
+type := bool                  (ground bool type)
+      | type -> type          (function type)
+      | <alt_1: type_1,       (variant type)
+         ...,
+         alt_n: type_n>
+      | (type_1, ..., type_n) (product type)
+```
+
+
+Typing rules:
+
+**Rule T-True**
+
+> true : bool
+
+**Rule T-False**
+
+> false : bool
+
+**Rule T-Tuple**
+
+**If** t_1 : T_1, ..., t_n : T_n
+
+> (t_1, ..., t_n) : (T_1, ..., T_n)
+
+**Rule T-Proj**
+
+**If** t : (T_1, ..., T_n)
+
+> #k t : T_k