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/Primitives/Base.lean | 51 ---------------------------------
 1 file changed, 51 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index adec9a8b..9dbaf133 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -123,57 +123,6 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
   simp [Bind.bind]
   cases e <;> simp
 
--------------------------------
--- 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
-  -- 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
-
 ----------
 -- MISC --
 ----------
-- 
cgit v1.2.3