moved Member and related definitions to Struct builtin file

Lampe/Lampe.lean

@@ -265,9 +265,9 @@ nr_def call_decl<>(x: Field, y : Field) -> Field {
    (s as Pair<Field>).a
  }
 
- example {x y : Tp.denote p .field} :
-   STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
-     ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
+example {x y : Tp.denote p .field} :
+  STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
+    ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
   simp only [call_decl, struct_construct]
   steps <;> tauto
   . simp_all [exists_const, SLP.true_star]

Lampe/Lampe/Builtin/Struct.lean

@@ -1,6 +1,22 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
+inductive Member : Tp → List Tp → Type where
+| head : Member tp (tp :: tps)
+| tail : Member tp tps → Member tp (tp' :: tps)
+
+@[reducible]
+def indexTpl (tpl : Tp.denoteArgs p tps) (mem : Member tp tps) : Tp.denote p tp := match tps with
+| tp :: _ => match tpl, mem with
+  | (h, _), .head => h
+  | (_, rem), .tail m => indexTpl rem m
+
+def exampleTuple {p} : Tp.denoteArgs p [.bool, .field, .field] := (true, 4, 5)
+
+example : indexTpl (p := p) exampleTuple Member.head = true := rfl
+example : indexTpl (p := p) exampleTuple Member.head.tail = 4 := rfl
+example : indexTpl (p := p) exampleTuple Member.head.tail.tail = 5 := rfl
+
 @[reducible]
 def listRep (rep : Tp → Type _) : List Tp → Type := fun l => match l with
 | tp :: tps => (rep tp) × (listRep rep tps)
@@ -30,7 +46,7 @@ example : replaceTuple' (p := p) exampleTuple Member.head.tail.tail 2 = (true, 4
 
 @[simp]
 theorem index_replaced_tpl :
-  indexTpl p (replaceTuple' tpl mem v') mem = v' := by
+  indexTpl (replaceTuple' tpl mem v') mem = v' := by
   induction mem <;> aesop
 
 /--
@@ -46,7 +62,7 @@ Defines the indexing/projection of a tuple with a `Member`.
 -/
 def projectTuple (mem : Member outTp fieldTps) := newGenericPureBuiltin
   (fun name => ⟨[.tuple name fieldTps], outTp⟩)
-  (fun _ h![tpl] => ⟨True, fun _ => indexTpl _ tpl mem⟩)
+  (fun _ h![tpl] => ⟨True, fun _ => indexTpl tpl mem⟩)
 
 
 def replaceTuple (mem : Member tp tps) := newGenericPureBuiltin

Lampe/Lampe/Hoare/Builtins.lean

@@ -473,7 +473,7 @@ theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem)
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem replaceTuple_intro {mem : Member tp tps} : STHoarePureBuiltin p Γ (Builtin.replaceTuple mem) (by tauto) h![tpl, v] := by
+theorem replaceTuple_intro {mem : Builtin.Member tp tps} : STHoarePureBuiltin p Γ (Builtin.replaceTuple mem) (by tauto) h![tpl, v] := by
   apply pureBuiltin_intro_consequence <;> try rfl
   tauto
 

Lampe/Lampe/Lens.lean

@@ -0,0 +1,46 @@
+import Lampe.Ast
+import Lampe.Builtin.Struct
+import Lampe.Builtin.Array
+
+namespace Lampe
+
+inductive Access : Tp → Tp → Type _
+| tpl : (mem : Builtin.Member tp tps) → Access (.tuple name tps) tp
+| arr : (idx : Fin n.toNat) → Access (.array tp n) tp
+
+def Access.get (acc : Access tp₁ tp₂) (s : Tp.denote p tp₁) : Tp.denote p tp₂ := match acc with
+| .tpl mem => Builtin.indexTpl s mem
+| .arr idx => s.get idx
+
+def Access.modify (acc : Access tp₁ tp₂) (s : Tp.denote p tp₁) (v' : Tp.denote p tp₂) : Tp.denote p tp₁ := match acc with
+| .tpl mem => Builtin.replaceTuple' s mem v'
+| .arr idx => Builtin.replaceArray' s idx v'
+
+@[simp]
+theorem Access.modify_get {acc : Access tp₁ tp₂} : acc.get (acc.modify s v') = v' := by
+  unfold Access.modify Access.get
+  cases acc <;> simp_all
+
+inductive Lens : Tp → Tp → Type _
+| nil : Lens tp tp
+| cons : Lens tp₁ tp₂ → Access tp₂ tp₃ → Lens tp₁ tp₃
+
+@[simp]
+def Lens.get (lens : Lens tp₁ tp₂) (s : Tp.denote p tp₁) : Tp.denote p tp₂ := match lens with
+| .nil => s
+| .cons l₁ a₁ => a₁.get (l₁.get s)
+
+@[simp]
+def Lens.modify (lens : Lens tp₁ tp₂) (s : Tp.denote p tp₁) (v' : Tp.denote p tp₂) : Tp.denote p tp₁ := match lens with
+| .nil => v'
+| .cons l₁ a₂ => l₁.modify s (a₂.modify (l₁.get s) v')
+
+@[simp]
+theorem Lens.modify_get {l : Lens tp₁ tp₂} : l.get (l.modify s v') = v' := by
+  induction l
+  . unfold Lens.modify Lens.get
+    simp_all
+  . unfold Lens.get Lens.modify Access.get Access.modify
+    casesm* Access _ _ <;> simp_all
+
+end Lampe

Lampe/Lampe/Syntax.lean

@@ -90,8 +90,8 @@ def tupleFields (tp : Tp) := match tp with
 | _ => []
 
 def mkTupleMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : Nat) : m (TSyntax `term) := match i with
-| .zero => `(Member.head)
-| .succ n' => do `(Member.tail $(←mkTupleMember n'))
+| .zero => `(Builtin.Member.head)
+| .succ n' => do `(Builtin.Member.tail $(←mkTupleMember n'))
 
 def mkStructMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) (gs : List $ TSyntax `nr_type) (field : TSyntax `ident) : m (TSyntax `term) := do
   let gs ← mkHListLit (←gs.mapM fun gVal => mkNrType gVal)
@@ -159,7 +159,7 @@ def Expr.mkArray (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (
   Expr.call h![] _ (.array tp n) (.builtin $ .mkArray n) vals
 
 @[reducible]
-def Expr.readTuple (tpl : rep $ .tuple name tps) (mem : Member tp tps) : Expr rep tp :=
+def Expr.readTuple (tpl : rep $ .tuple name tps) (mem : Builtin.Member tp tps) : Expr rep tp :=
   Expr.call h![] [typeof tpl] tp (.builtin (@Builtin.projectTuple tp tps mem)) h![tpl]
 
 @[reducible]
@@ -171,7 +171,7 @@ def Expr.readSlice (sl : rep $ .slice tp) (idx : rep $ .u s) : Expr rep tp :=
   Expr.call h![] _ tp (.builtin .sliceIndex) h![sl, idx]
 
 @[reducible]
-def Expr.replaceTuple (tpl : rep $ .tuple name tps) (mem : Member tp tps) (v : rep tp) : Expr rep (.tuple name tps) :=
+def Expr.replaceTuple (tpl : rep $ .tuple name tps) (mem : Builtin.Member tp tps) (v : rep tp) : Expr rep (.tuple name tps) :=
   Expr.call h![] _ (.tuple name tps) (.builtin $ .replaceTuple mem) h![tpl, v]
 
 @[reducible]
@@ -402,7 +402,7 @@ def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [
   params.getElems.toList.enum.mapM fun (idx, paramSyn) => match paramSyn with
     | `(nr_param_decl| $paramName:ident : $paramType:nr_type) => do
       let paramDefTy ← `(match generics with
-        | $(←mkHListLit generics) => Member $(←mkNrType paramType) (Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) generics))
+        | $(←mkHListLit generics) => Builtin.Member $(←mkNrType paramType) (Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) generics))
       let paramDefSyn ← `(match generics with
         | $(←mkHListLit generics) => $(←mkTupleMember idx))
       let defnNameSyn := mkFieldName (←mkNrIdent structName) paramName.getId.toString

Lampe/Lampe/Tp.lean

@@ -57,31 +57,6 @@ def Kind.denote : Kind → Type
 | .nat => Nat
 | .type => Tp
 
-inductive Member : Tp → List Tp → Type where
-| head : Member tp (tp :: tps)
-| tail : Member tp tps → Member tp (tp' :: tps)
-
-@[reducible]
-def indexTpl (tpl : Tp.denoteArgs p tps) (mem : Member tp tps) : Tp.denote p tp := match tps with
-| tp :: _ => match tpl, mem with
-  | (h, _), .head => h
-  | (_, rem), .tail m => indexTpl rem m
-
-def exampleTuple {p} : Tp.denoteArgs p [.bool, .field, .field] := (true, 4, 5)
-
-example : indexTpl p exampleTuple Member.head = true := rfl
-example : indexTpl p exampleTuple Member.head.tail = 4 := rfl
-example : indexTpl p exampleTuple Member.head.tail.tail = 5 := rfl
-
-@[reducible]
-def newMember (tps : List Tp) (n : Fin tps.length) : Member (tps.get n) tps := match n with
-| Fin.mk .zero _ => match tps with | _ :: _ => Member.head
-| Fin.mk (.succ n') _ => match tps with | _ :: tps' => Member.tail $ newMember tps' (Fin.mk n' _)
-
-example : newMember [.bool, .field, .field] ⟨0, (by tauto)⟩ = Member.head := rfl
-example : newMember [.bool, .field, .field] ⟨1, (by tauto)⟩ = Member.head.tail := rfl
-example : newMember [.bool, .field, .field] ⟨2, (by tauto)⟩ = Member.head.tail.tail := rfl
-
 lemma List.replicate_head (hl : x :: xs = List.replicate n a) : x = a := by
   unfold List.replicate at hl
   aesop