Higher order functions (#29)

Lampe/Lampe/Ast.lean

@@ -9,9 +9,6 @@ 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
@@ -25,21 +22,17 @@ structure TraitMethodImplRef where
   trait : TraitImplRef
   method : Ident
 
-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 Expr (rep : Tp → Type) : Tp → Type where
 | lit : (tp : Tp) → Nat → Expr rep tp
+| fn : (argTps : List Tp) → (outTp : Tp) → (r : FuncRef argTps outTp) → Expr rep (.fn argTps outTp)
 | 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 rep → HList rep argTypes → Expr rep res
+| call : (argTps : List Tp) → (outTp : Tp) → (rep $ .fn argTps outTp) → (args : HList rep argTps) → Expr rep outTp
+| callBuiltin : (argTps : List Tp) → (outTp : Tp) → (b : Builtin) → (args : HList rep argTps) → Expr rep outTp
 | 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
+| lam : (argTps : List Tp) → (outTp : Tp) → (HList rep argTps → Expr rep outTp) → Expr rep (.fn argTps outTp)
 
 structure Lambda (rep : Tp → Type) where
   argTps : List Tp

Lampe/Lampe/Hoare/Builtins.lean

@@ -21,7 +21,7 @@ Introduction rule for pure builtins.
 theorem pureBuiltin_intro {A : Type} {a : A} {sgn desc args} :
   STHoare p Γ
     ⟦⟧
-    (.call h![] (sgn a).fst (sgn a).snd (.builtin (Builtin.newGenericPureBuiltin sgn desc)) args)
+    (.callBuiltin (sgn a).fst (sgn a).snd (Builtin.newGenericPureBuiltin sgn desc) args)
     (fun v => ∃h, (v = (desc a args).snd h)) := by
   unfold STHoare
   intro H
@@ -44,7 +44,7 @@ lemma pureBuiltin_intro_consequence
     (h2 : outTp = (sgn a).snd)
     (hp : (h: (desc a (h1 ▸ args)).fst) → Q (h2 ▸ (desc a (h1 ▸ args)).snd h)) :
     STHoare p Γ ⟦⟧
-      (.call h![] argTps outTp (.builtin (Builtin.newGenericPureBuiltin sgn desc)) args)
+      (.callBuiltin argTps outTp (Builtin.newGenericPureBuiltin sgn desc) args)
       fun v => Q v := by
   subst_vars
   dsimp only at *
@@ -369,7 +369,7 @@ theorem strAsBytes_intro : STHoarePureBuiltin p Γ Builtin.strAsBytes (by tauto)
 theorem ref_intro :
     STHoare p Γ
       ⟦⟧
-      (.call h![] [tp] (Tp.ref tp) (.builtin .ref) h![v])
+      (.callBuiltin [tp] (.ref tp) .ref h![v])
       (fun r => [r ↦ ⟨tp, v⟩]) := by
   unfold STHoare
   intro H
@@ -393,7 +393,7 @@ theorem ref_intro :
 theorem readRef_intro :
     STHoare p Γ
     [r ↦ ⟨tp, v⟩]
-    (.call h![] [tp.ref] tp (.builtin .readRef) h![r])
+    (.callBuiltin [.ref tp] tp .readRef h![r])
     (fun v' => ⟦v' = v⟧ ⋆ [r ↦ ⟨tp, v⟩]) := by
   unfold STHoare
   intro H
@@ -426,7 +426,7 @@ theorem readRef_intro :
 theorem writeRef_intro :
     STHoare p Γ
     [r ↦ ⟨tp, v⟩]
-    (.call h![] [tp.ref, tp] .unit (.builtin .writeRef) h![r, v'])
+    (.callBuiltin [.ref tp, tp] .unit .writeRef h![r, v'])
     (fun _ => [r ↦ ⟨tp, v'⟩]) := by
   unfold STHoare
   intro H
@@ -471,7 +471,7 @@ theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem)
 theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
     STHoare p Γ
     [r ↦ ⟨tp₁, s⟩]
-    (.call h![] [tp₁.ref] tp₂ (.builtin $ .readLens lens) h![r])
+    (.callBuiltin [tp₁.ref] tp₂ (.readLens lens) h![r])
     (fun v' => ⟦lens.get s = some v'⟧ ⋆ [r ↦ ⟨tp₁, s⟩]) := by
   unfold STHoare THoare
   intros H st h
@@ -491,7 +491,7 @@ theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
  theorem modifyLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} {s : Tp.denote p tp₁} {v : Tp.denote p tp₂} :
     STHoare p Γ
     [r ↦ ⟨tp₁, s⟩]
-    (.call h![] [tp₁.ref, tp₂] .unit (.builtin $ .modifyLens lens) h![r, v])
+    (.callBuiltin [tp₁.ref, tp₂] .unit (.modifyLens lens) h![r, v])
     (fun _ => ∃∃h, [r ↦ ⟨tp₁, lens.modify s v |>.get h⟩]) := by
   unfold STHoare THoare
   intros H st h
@@ -528,7 +528,7 @@ theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
 theorem getLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
     STHoare p Γ
     ⟦⟧
-    (.call h![] [tp₁] tp₂ (.builtin $ .getLens lens) h![s])
+    (.callBuiltin [tp₁] tp₂ (.getLens lens) h![s])
     (fun v => ⟦lens.get s = some v⟧) := by
   unfold STHoare THoare
   intros H st h
@@ -547,7 +547,7 @@ theorem assert_intro : STHoarePureBuiltin p Γ Builtin.assert (by tauto) h![a] (
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem cast_intro [Builtin.CastTp tp tp'] : STHoare p Γ ⟦⟧ (.call h![] [tp] tp' (.builtin .cast) h![v])
+theorem cast_intro [Builtin.CastTp tp tp'] : STHoare p Γ ⟦⟧ (.callBuiltin [tp] tp' .cast h![v])
    (fun v' => ∃∃ h, ⟦@Builtin.CastTp.cast tp tp' _ p v h = v'⟧) := by
    unfold STHoare THoare
    intros

Lampe/Lampe/Hoare/SepTotal.lean

@@ -30,7 +30,7 @@ abbrev STHoarePureBuiltin p (Γ : Env)
   (_ : b = @Builtin.newGenericPureBuiltin A sgn desc)
   (args : HList (Tp.denote p) (sgn a).fst) : Prop :=
     STHoare p Γ ⟦⟧
-      (.call h![] (sgn a).fst (sgn a).snd (.builtin b) args)
+      (.callBuiltin (sgn a).fst (sgn a).snd b args)
       (fun v => ∃h, v = (desc a (args)).snd h)
 
 namespace STHoare
@@ -133,7 +133,7 @@ lemma Finmap.union_singleton [DecidableEq α] {β : α → Type u} {r : α} {v v
 theorem fresh_intro :
   STHoare p Γ
       ⟦⟧
-      (.call h![] [] tp (.builtin .fresh) h![])
+      (.callBuiltin [] tp .fresh h![])
       (fun _ => ⟦⟧) := by
   unfold STHoare
   intro H
@@ -306,42 +306,9 @@ theorem skip_intro :
   . apply SLP.ent_star_top
     tauto
 
-theorem callLambda_intro {lambdaBody} {P : SLP (State p)} {Q : Tp.denote p outTp → SLP (State p)}:
-  @STHoare outTp p Γ P (lambdaBody args) Q →
-  STHoare p Γ (P ⋆ [λref ↦ ⟨argTps, outTp, lambdaBody⟩])
-    (Expr.call h![] argTps outTp (.lambda ref) args)
-    (fun v => (Q v) ⋆ [λref ↦ ⟨argTps, outTp, lambdaBody⟩]) := by
-  intros
-  rename_i h
-  unfold STHoare THoare
-  intros
-  constructor <;> tauto
-  unfold SLP.star at *
-  . rename_i st h
-    obtain ⟨st₁, ⟨st₂, ⟨_, h₂, h₃, _⟩⟩⟩ := h
-    obtain ⟨st₁', ⟨st₂', _⟩⟩ := h₃
-    simp_all only [State.union_parts, Finmap.mem_union, Finmap.mem_singleton, or_true,
-      Finmap.lookup_union_left]
-    generalize hL : (⟨_, _, _⟩ : Lambda _) = lmb at *
-    have _ : ref ∉ st₁'.lambdas := by
-      rename_i h₃
-      obtain ⟨hi₁, _, _, hi₂⟩ := h₃
-      simp only [State.lmbSingleton] at hi₂
-      simp only [LawfulHeap.disjoint] at hi₁
-      obtain ⟨_, hj₁⟩ := hi₁
-      rw [hi₂] at hj₁
-      tauto
-    simp [Finmap.lookup_union_right (by tauto)]
-  . apply consequence <;> tauto
-    apply consequence_frame_left
-    rotate_left 2
-    exact P
-    exact h
-    simp only [SLP.true_star, SLP.entails_self]
-
 theorem lam_intro :
-  STHoare p Γ ⟦⟧ (.lambda argTps outTp lambdaBody)
-    fun v => [λv ↦ ⟨argTps, outTp, lambdaBody⟩] := by
+  STHoare p Γ ⟦⟧ (.lam argTps outTp lambdaBody)
+    fun v => ∃∃ r, ⟦v = FuncRef.lambda r⟧ ⋆ [λr ↦ ⟨argTps, outTp, lambdaBody⟩] := by
   unfold STHoare THoare
   intros H st h
   constructor
@@ -361,38 +328,81 @@ theorem lam_intro :
       rw [Finmap.Disjoint.symm_iff]
       apply Finmap.singleton_disjoint_of_not_mem (by assumption)
     simp only [Finmap.insert_eq_singleton_union, Finmap.union_comm_of_disjoint hd]
-  . unfold State.lmbSingleton
-    tauto
+  . unfold State.lmbSingleton SLP.exists'
+    exists r
+    simp_all only [SLP.true_star]
   . apply SLP.ent_star_top
     tauto
 
-theorem callTrait_intro {impl} {fname fn}
-    (h_trait : TraitResolution Γ traitRef impl)
-    (h_fn : (fname, fn) ∈ impl)
-    (hkc : fn.generics = tyKinds)
-    (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTypes)
-    (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res)
-    (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q):
+theorem callLambda_intro {lambdaBody} {P : SLP $ State p}
+  {Q : Tp.denote p outTp → SLP (State p)}
+  {fnRef : Tp.denote p (.fn argTps outTp)}
+  {hlam : STHoare p Γ P (lambdaBody args) Q} :
+  STHoare p Γ (P ⋆ ∃∃ r, ⟦fnRef = FuncRef.lambda r⟧ ⋆ [λr ↦ ⟨argTps, outTp, lambdaBody⟩])
+    (Expr.call argTps outTp fnRef args)
+    (fun v => (Q v) ⋆ ∃∃ r, ⟦fnRef = FuncRef.lambda r⟧ ⋆ [λr ↦ ⟨argTps, outTp, lambdaBody⟩]) := by
+  unfold STHoare THoare
+  intros H st h
+  have h₁ : ∃ r, fnRef = .lambda r := by
+    simp only [SLP.star, SLP.exists', SLP.lift] at h
+    tauto
+  obtain ⟨r, _⟩ := h₁
+  apply Omni.callLambda <;> tauto
+  . obtain ⟨st₁, st₂, _, _, ⟨_, _, _, _, _, _, _, _, _, _, ⟨_, _⟩, _⟩, _⟩ := h
+    subst_vars
+    simp_all only [FuncRef.lambda.injEq]
+    subst_vars
+    simp_all only [LawfulHeap.empty_union, LawfulHeap.empty_disjoint]
+    simp only [State.union_parts]
+    rw [Finmap.lookup_union_left, Finmap.lookup_union_right]
+    <;> simp only [State.lmbSingleton, LawfulHeap.disjoint, State.union_parts] at *
+    . simp_all
+    . apply Finmap.singleton_disjoint_iff_not_mem.mp
+      simp_all only
+      tauto
+    . simp_all
+  apply STHoare.consequence_frame_left <;> tauto
+
+theorem callDecl_intro {fnRef : Tp.denote p (.fn argTps outTp)}
+    {href : H ⊢ ⟦fnRef = (.decl fnName kinds generics)⟧ ⋆ (⊤ : SLP $ State p)}
+    {h_fn : (fnName, fn) ∈ Γ.functions}
+    {hkc : fn.generics = kinds}
+    {htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps}
+    {htco : (fn.body _ (hkc ▸ generics) |>.outTp) = outTp}
+    {h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q} :
+    STHoare p Γ H (Expr.call argTps outTp fnRef args) Q := by
+  unfold STHoare THoare
+  intros
+  have _ : fnRef = (.decl fnName kinds generics) := by
+    rename_i h'
+    apply SLP.extract_prop at h' <;> tauto
+  apply Omni.callDecl <;> tauto
+
+
+theorem callTrait_intro {impls : List $ Ident × Function} {fnRef : Tp.denote p (.fn argTps outTp)}
+    (href : H ⊢  ⟦fnRef = (.trait selfTp traitName traitKinds traitGenerics fnName kinds generics)⟧ ⋆ (⊤ : SLP $ State p))
+    (h_trait : TraitResolution Γ ⟨⟨traitName, traitKinds, traitGenerics⟩, selfTp⟩ impls)
+    (h_fn : (fnName, fn) ∈ impls)
+    (hkc : fn.generics = kinds)
+    (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps)
+    (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = outTp)
+    (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q) :
     STHoare p Γ H
-      (@Expr.call _ tyKinds generics argTypes res (.trait ⟨traitRef, fname⟩) args)
+      (Expr.call argTps outTp fnRef args)
       Q := by
   unfold STHoare THoare
   intros
-  apply Omni.callTrait <;> try assumption
-  apply_assumption
-  assumption
+  have _ : fnRef = (.trait selfTp traitName traitKinds traitGenerics fnName kinds generics) := by
+    rename_i h'
+    apply SLP.extract_prop at h' <;> tauto
+  apply Omni.callTrait <;> tauto
 
-theorem callDecl_intro {fname fn}
-     (h_fn : (fname, fn) ∈ Γ.functions)
-     (hkc : fn.generics = tyKinds)
-     (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps)
-     (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res)
-     (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q):
-     STHoare p Γ H
-       (@Expr.call _ tyKinds generics argTps res (.decl fname) args)
-       Q := by
-   unfold STHoare THoare
-   intros
-   apply Omni.callDecl <;> tauto
+theorem fn_intro : STHoare p Γ ⟦⟧ (.fn argTps outTp r) fun v => v = r := by
+  unfold STHoare THoare
+  intro H st hp
+  constructor
+  simp only
+  apply SLP.ent_star_top
+  assumption
 
 end Lampe.STHoare

Lampe/Lampe/Hoare/Total.lean

@@ -45,7 +45,7 @@ theorem letIn_intro {P Q}
 theorem ref_intro {v P} :
     THoare p Γ
       (fun st => ∀r, r ∉ st → P r ⟨(st.vals.insert r ⟨tp, v⟩), st.lambdas⟩)
-      (.call h![] [tp] (Tp.ref tp) (.builtin .ref) h![v])
+      (.callBuiltin [tp] (.ref tp) .ref h![v])
       P := by
   unfold THoare
   intros
@@ -56,7 +56,7 @@ theorem ref_intro {v P} :
 theorem readRef_intro {ref} :
     THoare p Γ
       (fun st => st.vals.lookup ref = some ⟨tp, v⟩ ∧ P v st)
-      (.call h![] [tp.ref] tp (.builtin .readRef) h![ref])
+      (.callBuiltin [.ref tp] tp .readRef h![ref])
       P := by
   unfold THoare
   intros
@@ -66,7 +66,7 @@ theorem readRef_intro {ref} :
 theorem writeRef_intro {ref v} :
     THoare p Γ
       (fun st => ref ∈ st ∧ P () ⟨(st.vals.insert ref ⟨tp, v⟩), st.lambdas⟩)
-      (.call h![] [tp.ref, tp] .unit (.builtin .writeRef) h![ref, v])
+      (.callBuiltin [.ref tp, tp] .unit .writeRef h![ref, v])
       P := by
   unfold THoare
   intros
@@ -76,7 +76,7 @@ theorem writeRef_intro {ref v} :
 theorem fresh_intro {P} :
     THoare p Γ
       (∀∀v, P v)
-      (.call h![] [] tp (.builtin .fresh) h![])
+      (.callBuiltin [] tp .fresh h![])
       P := by
   unfold THoare
   intro st h