Skip to content

Commit bd23320

Browse files
gebnerCopilot
gebner
and
Copilot
committed
Add antiquotation syntax to _inline_pulse
Support $&(expr) for lvalue and $(expr) for rvalue antiquotations inside _inline_pulse(...) expressions. The expressions inside antiquotations are Haunted-C expressions that get parsed and emitted via emit_lvalue / emit_rvalue respectively. - Add InlinePulseToken enum (Verbatim/RValueAntiquot/LValueAntiquot) and InlinePulseCode struct to IR - Change ExprT::InlinePulse to use InlinePulseCode instead of InlineCode - Add process_inline_pulse() to scan InlineCode tokens for $ patterns, extract balanced-paren content, and parse inner expressions - Update all passes (check, elab, emit, prune, pretty) for new types - Add ExprKind::into_doc() for lvalue antiquotation emission - Add test/antiquot.c with F*-verified antiquotation test Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent de431a2 commit bd23320

8 files changed

Lines changed: 203 additions & 21 deletions

File tree

‎src/hauntedc.rs‎

Lines changed: 80 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -439,7 +439,12 @@ fn expr_parser<
439439
.ok()
440440
.and_then(|i| snip_map.snippets.get(&i));
441441
match snip {
442-
Some(snip) => Ok(Rc::new(snip.clone())),
442+
Some(snip) => {
443+
let fallback_loc = sift.resolve_source_info(&span);
444+
let code =
445+
process_inline_pulse(&fallback_loc, snip, snip_map, target_widths);
446+
Ok(Rc::new(code))
447+
}
443448
None => Err(Rich::custom(span, format!("snippet {} not found", i))),
444449
}
445450
})
@@ -577,7 +582,7 @@ fn expr_parser<
577582
));
578583

579584
and_then!(type_name.delimited_by(punct(Punct::LParen), punct(Punct::RParen)), {
580-
InlinePulse(ty, code: Rc<InlineCode>: inline_pulse) = e =>
585+
InlinePulse(ty, code: Rc<InlinePulseCode>: inline_pulse) = e =>
581586
ExprT::InlinePulse(code, ty).with_loc(sift.resolve_source_info(&e.span())).into(),
582587
Plain(ty, x: Expr: cast_expression) = e =>
583588
ExprT::Cast(x.to_rvalue(), ty).with_loc(sift.resolve_source_info(&e.span())).into(),
@@ -811,3 +816,76 @@ pub fn parse_expr(
811816
}));
812817
output
813818
}
819+
820+
pub fn process_inline_pulse(
821+
fallback_loc: &Rc<SourceInfo>,
822+
code: &InlineCode,
823+
snippets: &SnippetMap,
824+
target_widths: &TargetIntWidths,
825+
) -> InlinePulseCode {
826+
let tokens = &code.tokens;
827+
let mut result = Vec::new();
828+
let mut i = 0;
829+
while i < tokens.len() {
830+
if &*tokens[i].text.val == "$" {
831+
let before = tokens[i].before;
832+
let is_lvalue;
833+
// Check for $& (lvalue) vs $ (rvalue)
834+
if i + 1 < tokens.len() && &*tokens[i + 1].text.val == "&" {
835+
is_lvalue = true;
836+
i += 2; // skip $ and &
837+
} else {
838+
is_lvalue = false;
839+
i += 1; // skip $
840+
}
841+
// Expect opening paren
842+
if i < tokens.len() && &*tokens[i].text.val == "(" {
843+
i += 1; // skip (
844+
// Collect tokens until matching )
845+
let mut depth = 1;
846+
let start = i;
847+
while i < tokens.len() && depth > 0 {
848+
if &*tokens[i].text.val == "(" {
849+
depth += 1;
850+
} else if &*tokens[i].text.val == ")" {
851+
depth -= 1;
852+
}
853+
if depth > 0 {
854+
i += 1;
855+
}
856+
}
857+
// tokens[start..i] are the inner tokens
858+
let inner_code = InlineCode {
859+
tokens: tokens[start..i].to_vec(),
860+
};
861+
let mut diags = Diagnostics::empty();
862+
let expr = parse_expr(
863+
&mut diags,
864+
fallback_loc,
865+
&inner_code,
866+
snippets,
867+
target_widths,
868+
);
869+
if is_lvalue {
870+
result.push(InlinePulseToken::LValueAntiquot { before, expr });
871+
} else {
872+
result.push(InlinePulseToken::RValueAntiquot { before, expr });
873+
}
874+
i += 1; // skip closing )
875+
} else {
876+
// Malformed: emit $ as verbatim
877+
result.push(InlinePulseToken::Verbatim(CodeToken {
878+
before,
879+
text: Ast {
880+
loc: fallback_loc.clone(),
881+
val: Rc::from("$"),
882+
},
883+
}));
884+
}
885+
} else {
886+
result.push(InlinePulseToken::Verbatim(tokens[i].clone()));
887+
i += 1;
888+
}
889+
}
890+
InlinePulseCode { tokens: result }
891+
}

‎src/ir/mod.rs‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -236,7 +236,7 @@ pub enum ExprT {
236236
BinOp(BinOp, Rc<Expr>, Rc<Expr>),
237237
FnCall(Rc<Ident>, Exprs),
238238
Cast(Rc<Expr>, Rc<Type>),
239-
InlinePulse(Rc<InlineCode>, Rc<Type>),
239+
InlinePulse(Rc<InlinePulseCode>, Rc<Type>),
240240
Live(Rc<Expr>),
241241
Old(Rc<Expr>),
242242
Forall(Rc<Ident>, Rc<Type>, Rc<Expr>),
@@ -340,6 +340,24 @@ impl InlineCode {
340340
}
341341
}
342342

343+
#[derive(Debug, PartialEq, Eq, Hash, Clone)]
344+
pub enum InlinePulseToken {
345+
Verbatim(CodeToken),
346+
RValueAntiquot {
347+
before: &'static str,
348+
expr: Rc<Expr>,
349+
},
350+
LValueAntiquot {
351+
before: &'static str,
352+
expr: Rc<Expr>,
353+
},
354+
}
355+
356+
#[derive(Debug, PartialEq, Eq, Hash, Clone)]
357+
pub struct InlinePulseCode {
358+
pub tokens: Vec<InlinePulseToken>,
359+
}
360+
343361
#[derive(Debug, PartialEq, Eq, Hash, Clone)]
344362
pub struct IncludeDecl {
345363
pub code: InlineCode,

‎src/ir/pretty.rs‎

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -139,14 +139,32 @@ impl PrettyIR for ExprT {
139139
.group())
140140
.append(RcDoc::line())
141141
.append(rval.to_doc()),
142-
ExprT::InlinePulse(inline_code, ty) => (RcDoc::text("(")
143-
.append(ty.to_doc())
144-
.append(")")
145-
.nest(2)
146-
.group())
147-
.append(RcDoc::line())
148-
.append(RcDoc::text("_inline_pulse(").append(inline_code.to_string()))
149-
.append(RcDoc::text(")")),
142+
ExprT::InlinePulse(inline_code, ty) => {
143+
let code_doc = RcDoc::concat(inline_code.tokens.iter().map(|tok| {
144+
match tok {
145+
InlinePulseToken::Verbatim(ct) => {
146+
RcDoc::text(ct.before).append(RcDoc::text(ct.text.val.to_string()))
147+
}
148+
InlinePulseToken::RValueAntiquot { before, expr } => RcDoc::text(*before)
149+
.append("$(")
150+
.append(expr.to_doc())
151+
.append(")"),
152+
InlinePulseToken::LValueAntiquot { before, expr } => RcDoc::text(*before)
153+
.append("$&(")
154+
.append(expr.to_doc())
155+
.append(")"),
156+
}
157+
}));
158+
(RcDoc::text("(")
159+
.append(ty.to_doc())
160+
.append(")")
161+
.nest(2)
162+
.group())
163+
.append(RcDoc::line())
164+
.append(RcDoc::text("_inline_pulse("))
165+
.append(code_doc)
166+
.append(RcDoc::text(")"))
167+
}
150168
ExprT::Live(v) => RcDoc::text("_live(")
151169
.append(v.to_doc())
152170
.append(")")

‎src/pass/check.rs‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -287,7 +287,18 @@ impl<'a> Checker<'a> {
287287
self.check_rvalue(env, rval);
288288
self.check_type(env, ty);
289289
}
290-
ExprT::InlinePulse(_inline_code, ty) => self.check_type(env, ty),
290+
ExprT::InlinePulse(code, ty) => {
291+
self.check_type(env, ty);
292+
for tok in &code.tokens {
293+
match tok {
294+
InlinePulseToken::RValueAntiquot { expr, .. }
295+
| InlinePulseToken::LValueAntiquot { expr, .. } => {
296+
self.check_rvalue(env, expr)
297+
}
298+
InlinePulseToken::Verbatim(_) => {}
299+
}
300+
}
301+
}
291302
ExprT::Live(lval) => self.check_rvalue(env, lval),
292303
ExprT::Old(rval) => self.check_rvalue(env, rval),
293304
ExprT::Forall(var, ty, body) | ExprT::Exists(var, ty, body) => {

‎src/pass/elab.rs‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,18 @@ impl<'a> Elaborator<'a> {
153153
// TODO: check that actual_ty can be casted to ty
154154
}
155155
ExprT::Error(ty) => self.elab_type(env, Rc::make_mut(ty)),
156-
ExprT::InlinePulse(_, ty) => self.elab_type(env, Rc::make_mut(ty)),
156+
ExprT::InlinePulse(code, ty) => {
157+
self.elab_type(env, Rc::make_mut(ty));
158+
for tok in &mut Rc::make_mut(code).tokens {
159+
match tok {
160+
InlinePulseToken::RValueAntiquot { expr, .. }
161+
| InlinePulseToken::LValueAntiquot { expr, .. } => {
162+
self.elab_rvalue(env, Rc::make_mut(expr))
163+
}
164+
InlinePulseToken::Verbatim(_) => {}
165+
}
166+
}
167+
}
157168
ExprT::UnOp(un_op, arg) => {
158169
self.elab_rvalue(env, Rc::make_mut(arg));
159170
match un_op {

‎src/pass/emit.rs‎

Lines changed: 37 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,13 @@ impl ExprKind {
3232
ExprKind::RValue(doc) => doc,
3333
}
3434
}
35+
36+
/// Extract the raw document without rvalue/lvalue conversion.
37+
fn into_doc(self) -> Doc {
38+
match self {
39+
ExprKind::LValue(doc) | ExprKind::RValue(doc) => doc,
40+
}
41+
}
3542
}
3643

3744
struct StrWriter {
@@ -331,7 +338,9 @@ fn subst_this_rvalue(env: &Env, nm: &mut NameMangling, rvalue: &mut Expr, this:
331338
ExprT::Cast(val, _) => {
332339
subst_this_rvalue(env, nm, Rc::make_mut(val), this);
333340
}
334-
ExprT::InlinePulse(val, _) => subst_inline_code_this(env, nm, Rc::make_mut(val), this),
341+
ExprT::InlinePulse(val, _) => {
342+
subst_inline_pulse_code_this(env, nm, Rc::make_mut(val), this)
343+
}
335344
ExprT::Error(_ty) => {}
336345
ExprT::Live(val) => subst_this_rvalue(env, nm, Rc::make_mut(val), this),
337346
ExprT::Old(val) => subst_this_rvalue(env, nm, Rc::make_mut(val), this),
@@ -350,11 +359,24 @@ fn subst_this_rvalue(env: &Env, nm: &mut NameMangling, rvalue: &mut Expr, this:
350359
}
351360
}
352361

353-
fn subst_inline_code_this(env: &Env, nm: &mut NameMangling, val: &mut InlineCode, this: &Rc<Expr>) {
362+
fn subst_inline_pulse_code_this(
363+
env: &Env,
364+
nm: &mut NameMangling,
365+
val: &mut InlinePulseCode,
366+
this: &Rc<Expr>,
367+
) {
354368
for tok in &mut val.tokens {
355-
// This is ridiculuously hacky....
356-
if &*tok.text.val == "this" {
357-
tok.text.val = Rc::from(emit_rvalue(env, nm, this).pretty(100).to_string());
369+
match tok {
370+
InlinePulseToken::Verbatim(ct) => {
371+
// This is ridiculuously hacky....
372+
if &*ct.text.val == "this" {
373+
ct.text.val = Rc::from(emit_rvalue(env, nm, this).pretty(100).to_string());
374+
}
375+
}
376+
InlinePulseToken::RValueAntiquot { expr, .. }
377+
| InlinePulseToken::LValueAntiquot { expr, .. } => {
378+
subst_this_rvalue(env, nm, Rc::make_mut(expr), this);
379+
}
358380
}
359381
}
360382
}
@@ -784,8 +806,16 @@ fn emit_rvalue_inner(env: &Env, nm: &mut NameMangling, v: &Expr) -> Doc {
784806
}
785807
ExprT::Error(_ty) => Doc::text("(admit())"),
786808
ExprT::InlinePulse(val, _) => parens(Doc::concat(val.tokens.iter().map(|tok| {
787-
Doc::text(tok.before)
788-
.append(annotated(&tok.text, Doc::text(tok.text.val.to_string())))
809+
match tok {
810+
InlinePulseToken::Verbatim(ct) => Doc::text(ct.before)
811+
.append(annotated(&ct.text, Doc::text(ct.text.val.to_string()))),
812+
InlinePulseToken::RValueAntiquot { before, expr } => {
813+
Doc::text(*before).append(emit_rvalue(env, nm, expr))
814+
}
815+
InlinePulseToken::LValueAntiquot { before, expr } => {
816+
Doc::text(*before).append(emit_expr(env, nm, expr).into_doc())
817+
}
818+
}
789819
}))),
790820
ExprT::BinOp(BinOp::LogAnd, lhs, rhs) => {
791821
if let Some(ty) = env.infer_rvalue(lhs) {

‎src/pass/prune.rs‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,16 @@ fn scan_expr(deps: &mut HashSet<DeclName>, rv: &Expr) {
116116
scan_type(deps, ty);
117117
}
118118
ExprT::Error(ty) => scan_type(deps, ty),
119-
ExprT::InlinePulse(_, ty) => scan_type(deps, ty),
119+
ExprT::InlinePulse(code, ty) => {
120+
scan_type(deps, ty);
121+
for tok in &code.tokens {
122+
match tok {
123+
InlinePulseToken::RValueAntiquot { expr, .. }
124+
| InlinePulseToken::LValueAntiquot { expr, .. } => scan_expr(deps, expr),
125+
InlinePulseToken::Verbatim(_) => {}
126+
}
127+
}
128+
}
120129
ExprT::UnOp(_, arg) => scan_expr(deps, arg),
121130
ExprT::BinOp(_, lhs, rhs) => {
122131
scan_expr(deps, lhs);

‎test/antiquot.c‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include "c2pulse.h"
2+
3+
void test_rvalue_antiquot(int *x)
4+
_ensures((_slprop) _inline_pulse(pure ($(*x) = $(*x))))
5+
{
6+
return;
7+
}

0 commit comments

Comments
 (0)