Lambda support

Lampe/Lampe.lean

@@ -9,9 +9,10 @@ nr_def simple_muts<>(x : Field) -> Field {
   y
 }
 
-example : STHoare p Γ ⟦⟧ (simple_muts.fn.body _ h![] h![x]) fun v => v = x := by
+example : STHoare p Γ ⟦⟧ (simple_muts.fn.body _ h![] |>.body h![x]) fun v => v = x := by
   simp only [simple_muts]
   steps
+  try (exact _)
   simp_all
 
 nr_def weirdEq<I>(x : I, y : I) -> Unit {
@@ -21,7 +22,7 @@ nr_def weirdEq<I>(x : I, y : I) -> Unit {
   #assert(#eq(a, y) : bool) : Unit;
 }
 
-example {P} {x y : Tp.denote P .field} : STHoare P Γ ⟦⟧ (weirdEq.fn.body _ h![.field] h![x, y]) fun _ => x = y := by
+example {x y : Tp.denote p .field} : STHoare p Γ ⟦⟧ (weirdEq.fn.body _ h![.field] |>.body h![x, y]) fun _ => x = y := by
   simp only [weirdEq]
   steps
   simp_all
@@ -39,7 +40,7 @@ lemma BitVec.add_toNat_of_lt_max {a b : BitVec w} (h: a.toNat + b.toNat < 2^w) :
   rw [Nat.mod_eq_of_lt]
   assumption
 
-example {self that : Tp.denote P (.slice tp)} : STHoare P Γ ⟦⟧ (sliceAppend.fn.body _ h![tp] h![self, that]) fun v => v = self ++ that := by
+example {self that : Tp.denote p (.slice tp)} : STHoare p Γ ⟦⟧ (sliceAppend.fn.body _ h![tp] |>.body h![self, that]) fun v => v = self ++ that := by
   simp only [sliceAppend]
   steps
   rename Tp.denote _ tp.slice.ref => selfRef
@@ -48,7 +49,7 @@ example {self that : Tp.denote P (.slice tp)} : STHoare P Γ ⟦⟧ (sliceAppend
     steps
     have : (i + 1).toNat = i.toNat + 1 := by
       apply BitVec.add_toNat_of_lt_max
-      casesm* (Tp.denote P (.u 32)), (U _), Fin _
+      casesm* (Tp.denote p (.u 32)), (U _), Fin _
       simp at *
       linarith
     simp only [this, List.take_succ]
@@ -66,7 +67,7 @@ nr_def simple_if<>(x : Field, y : Field) -> Field {
   z
 }
 
-example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if.fn.body (Tp.denote p) h![] h![x, y])
+example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y])
   fun v => v = y := by
   simp only [simple_if]
   steps <;> tauto
@@ -82,14 +83,35 @@ nr_def simple_if_else<>(x : Field, y : Field) -> Field {
   z
 }
 
-example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if_else.fn.body (Tp.denote p) h![] h![x, y])
+example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body h![x, y])
   fun v => v = x := by
   simp only [simple_if_else]
   steps
   . simp only [decide_True, exists_const]
     sl
     contradiction
-  . simp_all
+  . aesop
+
+nr_def simple_lambda<>(x : Field, y : Field) -> Field {
+  let add = |a : Field, b : Field| -> Field { #add(a, b) : Field };
+  ^add(x, y) : Field;
+}
+
+example {p Γ} {x y : Tp.denote p Tp.field} :
+  STHoare p Γ ⟦⟧ (simple_lambda.fn.body _ h![] |>.body h![x, y])
+  fun v => v = (x + y) := by
+  simp only [simple_lambda]
+  steps
+  simp_all
+  steps
+  simp_all
+  rotate_left 2
+  simp_all [SLP.entails_self]
+  exact (fun v => v = x + y)
+  sl
+  aesop
+  sl
+  aesop
 
 def bulbulizeField : TraitImpl := {
   traitGenericKinds := [],
@@ -100,7 +122,7 @@ def bulbulizeField : TraitImpl := {
   impl := fun _ => [("bulbulize", nrfn![
     fn bulbulize<>(x : Field) -> Field {
       #add(x, x) : Field
-    }].2
+    }]
   )]
 }
 
@@ -111,9 +133,9 @@ def bulbulizeU32 : TraitImpl := {
   constraints := fun _ => [],
   self := fun _ => .u 32,
   impl := fun _ => [("bulbulize", nrfn![
-    fn bulbulize<>(x : u32) -> u32 {
+    fn bulbulize<>(_x : u32) -> u32 {
       69 : u32
-    }].2
+    }]
   )]
 }
 

Lampe/Lampe/Ast.lean

@@ -1,13 +1,17 @@
 import Mathlib
+
 import Lampe.Tp
 import Lampe.Data.HList
-import Lampe.State
+import Lampe.SeparationLogic.ValHeap
 import Lampe.Builtin
 
 namespace Lampe
 
 abbrev Ident := String
 
+/-- A reference to a lambda is represented as a reference to a unit type -/
+abbrev Tp.lambdaRef := Tp.ref .unit
+
 structure TraitRef where
 name : Ident
 traitGenericKinds : List Kind
@@ -21,44 +25,47 @@ structure TraitMethodImplRef where
 trait : TraitImplRef
 method : Ident
 
-inductive FunctionIdent : Type where
-| builtin : Builtin → FunctionIdent
-| decl : Ident → FunctionIdent
-| trait : TraitMethodImplRef → FunctionIdent
+inductive FunctionIdent (rep : Tp → Type) : Type where
+| builtin : Builtin → FunctionIdent rep
+| decl : Ident → FunctionIdent rep
+| lambda : rep .lambdaRef → FunctionIdent rep
+| trait : TraitMethodImplRef → FunctionIdent rep
 
 inductive Member : Tp → List Tp → Type where
 | head : Member tp (tp :: tps)
 | tail : Member tp tps → Member tp (tp' :: tps)
 
-inductive Expr (rep : Tp → Type): Tp → Type where
+inductive Expr (rep : Tp → Type) : Tp → Type where
 | lit : (tp : Tp) → Nat → Expr rep tp
 | var : rep tp → Expr rep tp
 | letIn : Expr rep t₁ → (rep t₁ → Expr rep t₂) → Expr rep t₂
-| call : HList Kind.denote tyKinds → (argTypes : List Tp) → (res : Tp) → FunctionIdent → HList rep argTypes → Expr rep res
+| call : HList Kind.denote tyKinds → (argTypes : List Tp) → (res : Tp) → FunctionIdent rep → HList rep argTypes → Expr rep res
 | ite : rep .bool → Expr rep a → Expr rep a → Expr rep a
 | 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
+
+structure Lambda (rep : Tp → Type) where
+  argTps : List Tp
+  outTp : Tp
+  body : HList rep argTps → Expr rep outTp
 
 structure Function : Type _ where
   generics : List Kind
-  inTps : HList Kind.denote generics → List Tp
-  outTp : HList Kind.denote generics → Tp
-  body : ∀ rep, (gs : HList Kind.denote generics) → HList rep (inTps gs) → Expr rep (outTp gs)
+  body : ∀ (rep : Tp → Type), (HList Kind.denote generics) → Lambda rep
 
 /-- Polymorphic identity -/
 example : Function := {
   generics := [.type]
-  inTps := fun h![x] => [x]
-  outTp := fun h![x] => x
-  body := fun _ h![_] h![x] => .var x
+  body := fun _ h![tp] => ⟨[tp], tp, fun h![x] => .var x⟩
 }
 
 structure FunctionDecl where
-name : Ident
-fn : Function
+  name : Ident
+  fn : Function
 
 structure Module where
-decls : List FunctionDecl
+  decls : List FunctionDecl
 
 structure Struct where
   name : String

Lampe/Lampe/Basic.lean

@@ -1,5 +1,4 @@
 import Lampe.Semantics
-import Lampe.SeparationLogic
 import Lampe.Syntax
 import Lampe.Ast
 import Lampe.Tp

Lampe/Lampe/Builtin/Basic.lean

@@ -1,29 +1,31 @@
-import Lampe.State
+import Lampe.SeparationLogic.ValHeap
 import Lampe.Data.Field
 import Lampe.Data.HList
-import Lampe.SeparationLogic
 import Lampe.Builtin.Helpers
 import Mathlib
 
 namespace Lampe
 
 abbrev Builtin.Omni := ∀(P:Prime),
-    State P →
+    ValHeap P →
     (argTps : List Tp) →
     (outTp : Tp) →
     HList (Tp.denote P) argTps →
-    (Option (State P × Tp.denote P outTp) → Prop) →
+    (Option (ValHeap P × Tp.denote P outTp) → Prop) →
     Prop
 
 def Builtin.omni_conseq (omni : Builtin.Omni) : Prop :=
-  ∀{P st argTps outTp args Q Q'}, omni P st argTps outTp args Q → (∀ r, Q r → Q' r) → omni P st argTps outTp args Q'
+  ∀ {P st argTps outTp args Q Q'},
+  omni P st argTps outTp args Q → (∀ r, Q r → Q' r) → omni P st argTps outTp args Q'
 
 def Builtin.omni_frame (omni : Builtin.Omni) : Prop :=
-  ∀{P st₁ st₂ argTps outTp args Q}, omni P st₁ argTps outTp args Q → st₁.Disjoint st₂ →
-    omni P (st₁ ∪ st₂) argTps outTp args (fun r => match r with
-      | some (st, v) => ((fun st => Q (some (st, v))) ⋆ (fun st => st = st₂)) st
-      | none => Q none
-    )
+  ∀ {P st₁ st₂ argTps outTp args Q},
+  omni P st₁ argTps outTp args Q →
+  st₁.Disjoint st₂ →
+  omni P (st₁ ∪ st₂) argTps outTp args (fun r => match r with
+    | some (st, v) => ((fun st => Q (some (st, v))) ⋆ (fun st => st = st₂)) st
+    | none => Q none
+  )
 
 structure Builtin where
   omni : Builtin.Omni

Lampe/Lampe/Builtin/Memory.lean

@@ -27,7 +27,7 @@ def ref : Builtin := {
     simp_all
     rfl
     simp [Finmap.insert_union]
-    simp_all [Finmap.insert_eq_singleton_union, Finmap.disjoint_union_left]
+    simp_all [Finmap.insert_eq_singleton_union, LawfulHeap.disjoint, Finmap.disjoint_union_left]
 }
 
 inductive readRefOmni : Omni where