Skip to content

Commit

Permalink
Pretty printing fixes (#957)
Browse files Browse the repository at this point in the history 
* next: remove shape stuff

* use other event fields to ONLY filter `refine` mode events

* fix missing method call

---------

Co-authored-by: Nico Lehmann <nico.lehmannm@gmail.com>
  • Loading branch information
@ranjitjhala @nilehmann
ranjitjhala and nilehmann authored Dec 24, 2024
1 parent 19d89f4 commit 341ee46
Show file tree
Hide file tree
Showing 3 changed files with 52 additions and 34 deletions.
44 changes: 27 additions & 17 deletions crates/flux-middle/src/rty/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1394,25 +1394,35 @@ pub(crate) mod pretty {
flds: &[Expr],
is_named: bool,
) -> Result<NestedString, fmt::Error> {
let keys = if let Some(genv) = cx.genv()
&& let Ok(adt_sort_def) = genv.adt_sort_def_of(def_id)
{
adt_sort_def
.field_names()
.iter()
.map(|name| format!("{}", name))
.collect_vec()
let mut text = if is_named { format_cx!(cx, "{:?}", def_id) } else { format_cx!(cx, "") };
if flds.is_empty() {
// No fields, no index
Ok(NestedString { text, children: None, key: None })
} else if flds.len() == 1 {
// Single field, inline index
text += &format_cx!(cx, "{:?} ", flds[0].clone());
Ok(NestedString { text, children: None, key: None })
} else {
(0..flds.len()).map(|i| format!("arg{}", i)).collect_vec()
};
let text =
if is_named { format_cx!(cx, "{:?}{{..}}", def_id) } else { format_cx!(cx, "{{..}}") };
let mut children = vec![];
for (key, fld) in iter::zip(keys, flds) {
let fld_d = fld.fmt_nested(cx)?;
children.push(NestedString { key: Some(key), ..fld_d });
let keys = if let Some(genv) = cx.genv()
&& let Ok(adt_sort_def) = genv.adt_sort_def_of(def_id)
{
adt_sort_def
.field_names()
.iter()
.map(|name| format!("{}", name))
.collect_vec()
} else {
(0..flds.len()).map(|i| format!("arg{}", i)).collect_vec()
};
// Multiple fields, nested index
text += "{..}";
let mut children = vec![];
for (key, fld) in iter::zip(keys, flds) {
let fld_d = fld.fmt_nested(cx)?;
children.push(NestedString { key: Some(key), ..fld_d });
}
Ok(NestedString { text, children: Some(children), key: None })
}
Ok(NestedString { text, children: Some(children), key: None })
}

impl PrettyNested for Expr {
Expand Down
19 changes: 14 additions & 5 deletions crates/flux-middle/src/rty/pretty.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -225,10 +225,15 @@ struct IdxFmt(Expr);

impl PrettyNested for IdxFmt {
fn fmt_nested(&self, cx: &PrettyCx) -> Result<NestedString, fmt::Error> {
if let ExprKind::Aggregate(AggregateKind::Adt(def_id), flds) = self.0.kind() {
aggregate_nested(cx, *def_id, flds, false)
} else {
self.0.fmt_nested(cx)
let kind = self.0.kind();
match kind {
ExprKind::Aggregate(AggregateKind::Adt(def_id), flds) => {
aggregate_nested(cx, *def_id, flds, false)
}
ExprKind::Aggregate(AggregateKind::Tuple(0), _) => {
Ok(NestedString { text: String::new(), key: None, children: None })
}
_ => self.0.fmt_nested(cx),
}
}
}
Expand Down Expand Up @@ -700,7 +705,11 @@ impl PrettyNested for Ty {
TyKind::Indexed(bty, idx) => {
let bty_d = bty.fmt_nested(cx)?;
let idx_d = IdxFmt(idx.clone()).fmt_nested(cx)?;
let text = format!("{}[{}]", bty_d.text, idx_d.text);
let text = if idx_d.text.is_empty() {
bty_d.text
} else {
format!("{}[{}]", bty_d.text, idx_d.text)
};
let children = float_children(vec![bty_d.children, idx_d.children]);
Ok(NestedString { text, children, key: None })
}
Expand Down
23 changes: 11 additions & 12 deletions tools/vscode/src/extension.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ const execPromise = promisify(child_process.exec);

async function runShellCommand(env: NodeJS.ProcessEnv, command: string) {
try {
console.log("Running command: ", command);
// console.log("Running command: ", command);
const { stdout, stderr } = await execPromise(command, {
env: env,
cwd: vscode.workspace.workspaceFolders?.[0]?.uri.fsPath
Expand All @@ -107,7 +107,8 @@ async function runShellCommand(env: NodeJS.ProcessEnv, command: string) {

return stdout.trim();
} catch (error) {
console.log(`Command failed:`, error);
console.log(`Command failed!`);
// console.log(`Command failed:`, error);
// vscode.window.showErrorMessage(`Command failed: ${error}`);
// throw error;
}
Expand Down Expand Up @@ -181,7 +182,6 @@ class InfoProvider {
private updateInfo(fileName: string, fileInfo: LineInfo[]) {
const startMap = this.positionMap(fileInfo, Position.Start);
const endMap = this.positionMap(fileInfo, Position.End);
console.log("updateInfo:", fileName, startMap, endMap);
this._StartMap.set(fileName, startMap);
this._EndMap.set(fileName, endMap);
}
Expand All @@ -191,13 +191,10 @@ class InfoProvider {
const pos = this.currentPosition;
const line = this.currentLine;
const map = pos === Position.Start ? this._StartMap : this._EndMap;
console.log("getLineInfo (0):", file, pos, line, map);
if (file) {
const fileInfo = map.get(file);
console.log("getLineInfo (1):", fileInfo);
if (fileInfo) {
let lineInfo = fileInfo.get(line);
console.log("getLineInfo (2):", lineInfo);
return lineInfo;
} else {
return 'loading';
Expand All @@ -223,7 +220,6 @@ class InfoProvider {
this._StartMap.delete(src);
this._EndMap.delete(src);
beforeLoad();
// console.log("Running flux on ", src);
// run touch, cargo flux and load the new info
await runTouch(src);
const curAt = getFileModificationTime(file);
Expand All @@ -234,7 +230,6 @@ class InfoProvider {

public async loadFluxInfo() {
try {
// console.log("Loading flux info");
const lineInfos = await readFluxCheckerTrace();
lineInfos.forEach((lineInfo, fileName) => {
this.updateInfo(fileName, lineInfo);
Expand Down Expand Up @@ -287,7 +282,7 @@ function parseEnv(env: string): TypeEnv {
return JSON.parse(env)
.filter((bind: TypeEnvBind) => bind.name)
.map((b:any) => {
return {name: b.name, kind: b.kind, ty: parseNestedString(b.ty) }
return {name: b.name, kind: b.kind, ty: parseNestedString(b.ty), span: b.span};
});
}

Expand Down Expand Up @@ -354,7 +349,6 @@ class FluxViewProvider implements vscode.WebviewViewProvider {
this._currentState = DisplayState.Info;
this._currentRcx = parseRcx(info.rcx);
this._currentEnv = parseEnv(info.env);
console.log("UpdateView", this._currentEnv);
} else {
this._currentState = DisplayState.None;
}
Expand Down Expand Up @@ -456,7 +450,6 @@ class FluxViewProvider implements vscode.WebviewViewProvider {
} else {
body = this._getHtmlForMessage('No info available');
}
const sampleNestedHtml = nestedStringHtml(sampleData);

return `
<!DOCTYPE html>
Expand Down Expand Up @@ -611,9 +604,15 @@ type TypeEnvBind = {
name: string | null,
kind: string,
ty: NestedString,
span: StmtSpan,
}
type TypeEnv = TypeEnvBind[];

/*
*/


type RcxBind = {
name: string | string[],
sort: string,
Expand Down Expand Up @@ -667,7 +666,7 @@ function parseStatementSpanJSON(span: string): StmtSpan | undefined {
function parseEvent(event: any): [string, LineInfo] | undefined {
try {
const position = event.fields.event === 'statement_start' ? Position.Start : (event.fields.event === 'statement_end' ? Position.End : undefined);
if (position !== undefined) {
if (position !== undefined && event.span.name === 'refine') {
const stmt_span = parseStatementSpanJSON(event.fields.stmt_span_json);
if (stmt_span && stmt_span.file) {
const info = {line: stmt_span.end_line, pos: position, rcx: event.fields.rcx_json, env: event.fields.env_json};
Expand Down

0 comments on commit 341ee46

Please sign in to comment.