From 41d6f78a0ad6bd272164894bead3258b2001ec0c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 09:22:08 +0100
Subject: Update the tuples notations

---
 backends/lean/Base/Tuples.lean | 80 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 backends/lean/Base/Tuples.lean

(limited to 'backends/lean/Base/Tuples.lean')

diff --git a/backends/lean/Base/Tuples.lean b/backends/lean/Base/Tuples.lean
new file mode 100644
index 00000000..d8e4a843
--- /dev/null
+++ b/backends/lean/Base/Tuples.lean
@@ -0,0 +1,80 @@
+import Lean
+import Base.Utils
+
+namespace Primitives
+
+-------------------------------
+-- Tuple field access syntax --
+-------------------------------
+-- Declare new syntax `a.#i` for accessing the `i`-th term in a tuple
+-- The `noWs` parser is used to ensure there is no whitespace.
+syntax term noWs ".#" noWs num : term
+
+open Lean Meta Elab Term
+
+-- Auxliary function for computing the number of elements in a tuple (`Prod`) type.
+def getArity (type : Expr) : Nat :=
+  match type with
+  | .app (.app (.const ``Prod _) _) as => getArity as + 1
+  | _ => 1 -- It is not product
+
+-- Given a `tuple` of size `n`, construct a term that for accessing the `i`-th element
+def mkGetIdx (tuple : Expr) (n : Nat) (i : Nat) : MetaM Expr := do
+  match i with
+  | 0 => mkAppM ``Prod.fst #[tuple]
+  | i+1 =>
+    if n = 2 then
+      -- If the tuple has only two elements and `i` is not `0`,
+      -- we just return the second element.
+      mkAppM ``Prod.snd #[tuple]
+    else
+      -- Otherwise, we continue with the rest of the tuple.
+      let tuple ← mkAppM ``Prod.snd #[tuple]
+      mkGetIdx tuple (n-1) i
+
+-- Now, we define the elaboration function for the new syntax `a#i`
+elab_rules : term
+| `($a:term.#$i:num) => do
+  -- Convert `i : Syntax` into a natural number
+  let i := i.getNat
+  -- Return error if it is 0.
+  unless i ≥ 0 do
+    throwError "tuple index must be greater or equal to 0"
+  -- Convert `a : Syntax` into an `tuple : Expr` without providing expected type
+  let tuple ← elabTerm a none
+  let type ← inferType tuple
+  -- Instantiate assigned metavariable occurring in `type`
+  let type ← instantiateMVars type
+  /- In case we are indexing into a type abbreviation, we need to unfold the type.
+
+     TODO: we have to be careful about not unfolding too much,
+     for instance because of the following code:
+     ```
+     def Pair T U := T × U
+     def Tuple T U V := T × Pair U V
+     ```
+     We have to make sure that, given `x : Tuple T U V`, `x.1` evaluates
+     to the pair (an element of type `Pair T U`), not to the first field
+     of the pair (an element of type `T`).
+
+     We have a similar issue below if we generate code from the following Rust definition:
+     ```
+     struct Tuple(u32, (u32, u32));
+     ```
+     The issue is that in Rust, field 1 of `Tuple` is a pair `(u32, u32)`, but
+     in Lean there is no difference between `A × B × C` and `A × (B × C)`.
+
+     In case such situations happen we probably need to resort to chaining
+     the pair projectors, like in: `x.snd.fst`.
+   -/
+  let type ← whnf type
+  -- Ensure `tuple`'s type is a `Prod`uct.
+  unless type.isAppOf ``Prod do
+    throwError "tuple expected{indentExpr type}"
+  let n := getArity type
+  -- Ensure `i` is a valid index
+  unless i < n do
+    throwError "invalid tuple access at {i}, tuple has {n} elements"
+  mkGetIdx tuple n i
+
+end Primitives
-- 
cgit v1.2.3