Expr.struct removed. Instead, mkStruct builtin is used. Example is added

reilabs · Dec 10, 2024 · 47afc5c · 47afc5c
1 parent bf7e113
commit 47afc5c
Show file tree

Hide file tree

Showing 5 changed files with 21 additions and 9 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -235,3 +235,9 @@ example : Pair_b = Fin.mk 1 (by tauto) := by rfl
 nr_def structConstruct<>(a : Field, b : Field) -> struct Pair<Field> {
   @Pair { a : Field, b : Field }
 }
+
+example {p} {a b : Tp.denote p .field} :
+  STHoare p Γ ⟦⟧ (structConstruct.fn.body _ h![] |>.body h![a, b]) (fun v => v.fst = a ∧ v.snd = (b, ())) := by
+  simp only [structConstruct]
+  steps
+  aesop
diff --git a/Lampe/Lampe/Ast.lean b/Lampe/Lampe/Ast.lean
@@ -44,7 +44,6 @@ inductive Expr (rep : Tp → Type) : Tp → Type where
 | skip : Expr rep .unit
 | loop : rep (.u s) → rep (.u s) → (rep (.u s) → Expr rep r) → Expr rep .unit
 | lambda : (argTps : List Tp) → (outTp : Tp) → (HList rep argTps → Expr rep outTp) → Expr rep .lambdaRef
-| struct : (name : String) → (fieldTps : List Tp) → (fieldArgs : HList rep fieldTps) → Expr rep (.tuple (some name) fieldTps)
 
 structure Lambda (rep : Tp → Type) where
   argTps : List Tp
@@ -85,11 +84,4 @@ structure TraitImpl where
 def Struct.tp (s: Struct) : HList Kind.denote s.genericKinds → Tp :=
   fun generics => .tuple (some s.name) $ s.fieldTypes generics
 
-@[reducible]
-def Struct.constructor (s: Struct) :
-  (generics : HList Kind.denote s.genericKinds) →
-  HList rep (s.fieldTypes generics) →
-  Expr rep (s.tp generics) :=
-  fun generics fieldExprs => .struct s.name (s.fieldTypes generics) fieldExprs
-
 end Lampe
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
@@ -9,6 +9,7 @@ import Lampe.Builtin.Field
 import Lampe.Builtin.Memory
 import Lampe.Builtin.Slice
 import Lampe.Builtin.Str
+import Lampe.Builtin.Struct
 
 namespace Lampe.STHoare
 
@@ -439,6 +440,11 @@ theorem writeRef_intro:
     simp [Finmap.union_singleton]
   . simp_all
 
+-- Struct
+
+theorem mkStruct_intro : STHoarePureBuiltin p Γ Builtin.mkStruct (by tauto) fieldExprs (a := (name, fieldTps)) := by
+  apply pureBuiltin_intro_consequence <;> tauto
+  tauto
 
 -- Misc
 

diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
@@ -12,6 +12,7 @@ import Lampe.Builtin.Field
 import Lampe.Builtin.Memory
 import Lampe.Builtin.Slice
 import Lampe.Builtin.Str
+import Lampe.Builtin.Struct
 
 namespace Lampe
 
@@ -262,7 +263,8 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
   let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax
   let structName ← mkNrIdent structName
   mkArgs argExprs fun argVals => do
-    wrapSimple (←`(@Lampe.Expr.struct _ $(Syntax.mkStrLit structName) $(←mkListLit argTps) $(←mkHListLit argVals))) vname k
+    -- wrapSimple (←`(@Lampe.Expr.struct _ $(Syntax.mkStrLit structName) $(←mkListLit argTps) $(←mkHListLit argVals))) vname k
+    wrapSimple (←`(Lampe.Expr.call h![] _ (.tuple (some $(Syntax.mkStrLit structName)) $(←mkListLit argTps)) (.builtin Builtin.mkStruct) $(←mkHListLit argVals))) vname k
 | _ => throwUnsupportedSyntax
 
 end

diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -580,6 +580,8 @@ macro "stephelper1" : tactic => `(tactic|(
     -- remainder
     | apply uRem_intro
     | apply iRem_intro
+    -- struct
+    | apply mkStruct_intro
   )
 ))
 
@@ -633,6 +635,8 @@ macro "stephelper2" : tactic => `(tactic|(
     -- remainder
     | apply consequence_frame_left uRem_intro
     | apply consequence_frame_left iRem_intro
+    -- struct
+    | apply consequence_frame_left mkStruct_intro
   )
   repeat sl
 ))
@@ -687,6 +691,8 @@ macro "stephelper3" : tactic => `(tactic|(
     -- remainder
     | apply ramified_frame_top uRem_intro
     | apply ramified_frame_top iRem_intro
+    -- struct
+    | apply ramified_frame_top mkStruct_intro
   )
   repeat sl
 ))