Calldecl support (#26)

reilabs · Dec 27, 2024 · 974f3e3 · 974f3e3
1 parent 0b7d5f3
commit 974f3e3
Show file tree

Hide file tree

Showing 5 changed files with 52 additions and 7 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -259,3 +259,25 @@ example {p} {x : Tp.denote p $ .u 8} :
   simp only [basic_cast]
   steps
   aesop
+
+nr_def call_decl<>(x: Field, y : Field) -> Field {
+   let s = @struct_construct<>(x, y) : Pair<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
+  simp only [call_decl, struct_construct]
+  steps <;> tauto
+  . simp_all [exists_const, SLP.true_star]
+    steps
+    simp_all [exists_const, SLP.true_star]
+    simp_all [SLP.entails, SLP.wand, SLP.star, SLP.lift, SLP.forall']
+    intros
+    exists ∅, ∅
+    simp_all
+    apply And.intro rfl ?_
+    exists ∅, ∅
+    simp_all
+    apply And.intro rfl rfl
diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -382,4 +382,17 @@ theorem callTrait_intro {impl} {fname fn}
   apply_assumption
   assumption
 
+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
+
 end Lampe.STHoare
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
@@ -79,9 +79,6 @@ syntax ident ":" nr_type : nr_param_decl
 
 syntax num ":" nr_type : nr_expr
 syntax ident : nr_expr
-syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr
-syntax nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr
-syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr
 syntax "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}" : nr_expr
 syntax "${" term "}" : nr_expr
 syntax "$" ident : nr_expr
@@ -94,12 +91,17 @@ syntax "for" ident "in" nr_expr ".." nr_expr nr_expr : nr_expr
 syntax "(" nr_expr ")" : nr_expr
 syntax "*(" nr_expr ")" : nr_expr
 syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr
-syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call
 
 syntax nr_typed_expr := nr_expr ":" nr_type
-syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr
+
 syntax "(" ident "as" nr_ident "<" nr_type,* ">" ")" "." ident : nr_expr -- Struct access
-syntax nr_ident "<" nr_type,* ">" "{" sepBy(nr_expr, ",", ",", allowTrailingSep) "}" : nr_expr -- Struct constructor
+syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr -- Struct constructor
+
+syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Builtin call
+syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr -- Trait call
+syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call
+syntax "@" nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr -- Decl call
+
 
 syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}"
 syntax nr_trait_constraint := nr_type ":" nr_ident "<" nr_type,* ">"
@@ -218,6 +220,11 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
 | `(nr_expr| ^ $i:ident ($args,*) : $tp) => do
   mkArgs args.getElems.toList fun argVals => do
     wrapSimple (←`(Lampe.Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k
+| `(nr_expr| @ $declName:nr_ident < $callGenVals:nr_type,* > ( $args,* ) : $tp) => do
+   let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type))
+   let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
+   mkArgs args.getElems.toList fun argVals => do
+     wrapSimple (←`(@Lampe.Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k
 | `(nr_expr| ( $selfTp as $traitName < $traitGenVals,* > ) :: $methodName < $callGenVals,* > ( $args,* ) : $tp) => do
   let argTps ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $_ : $ty) => mkNrType ty | _ => throwUnsupportedSyntax
   let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax

diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -536,8 +536,9 @@ macro "stephelper1" : tactic => `(tactic|(
     | apply skip_intro
     | apply nested_triple STHoare.callLambda_intro
     | apply lam_intro
-    | apply callTrait_intro
     | apply cast_intro
+    | apply callTrait_intro
+    | apply callDecl_intro
     -- memory builtins
     | apply var_intro
     | apply ref_intro
@@ -652,6 +653,7 @@ macro "stephelper3" : tactic => `(tactic|(
     | apply ramified_frame_top skip_intro
     | apply ramified_frame_top lam_intro
     | apply ramified_frame_top cast_intro
+    | apply ramified_frame_top callDecl_intro
     -- memory builtins
     | apply ramified_frame_top var_intro
     | apply ramified_frame_top ref_intro

diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean
@@ -61,6 +61,7 @@ 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