diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index b98dbeae7a..bf156f451b 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -1394,25 +1394,35 @@ pub(crate) mod pretty { flds: &[Expr], is_named: bool, ) -> Result { - 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 { diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index fcc1f95aca..757d5163fd 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -225,10 +225,15 @@ struct IdxFmt(Expr); impl PrettyNested for IdxFmt { fn fmt_nested(&self, cx: &PrettyCx) -> Result { - 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), } } } @@ -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 }) } diff --git a/tools/vscode/src/extension.ts b/tools/vscode/src/extension.ts index c8e1e1a0db..3bc360d252 100644 --- a/tools/vscode/src/extension.ts +++ b/tools/vscode/src/extension.ts @@ -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 @@ -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; } @@ -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); } @@ -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'; @@ -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); @@ -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); @@ -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}; }); } @@ -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; } @@ -456,7 +450,6 @@ class FluxViewProvider implements vscode.WebviewViewProvider { } else { body = this._getHtmlForMessage('No info available'); } - const sampleNestedHtml = nestedStringHtml(sampleData); return ` @@ -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, @@ -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};