diff --git a/README.md b/README.md
index 0159390..568f77f 100644
--- a/README.md
+++ b/README.md
@@ -18,3 +18,17 @@ $ cargo install --path crates/argus_cli
$ cd ide && depot build
```
+
+## FAQ
+
+
rustup fails on installation
+
+If rustup fails, especially with an error like "could not rename downloaded file", this is probably because Flowistry is running rustup concurrently with another tool (like rust-analyzer). Until [rustup#988](https://github.com/rust-lang/rustup/issues/988) is resolved, there is unfortunately no automated way around this.
+
+To solve the issue, go to the command line and run:
+
+```
+rustup toolchain install nightly-2024-01-21 -c rust-src -c rustc-dev -c llvm-tools-preview
+```
+
+Then go back to VSCode and click "Continue" to let Flowistry continue installing.
diff --git a/crates/argus/src/analysis/entry.rs b/crates/argus/src/analysis/entry.rs
index 116a225..8ed2e47 100644
--- a/crates/argus/src/analysis/entry.rs
+++ b/crates/argus/src/analysis/entry.rs
@@ -8,7 +8,6 @@ use rustc_hir::BodyId;
use rustc_infer::{infer::InferCtxt, traits::PredicateObligation};
use rustc_middle::ty::{Predicate, TyCtxt, TypeckResults};
use rustc_trait_selection::traits::solve::Goal;
-use rustc_utils::source_map::range::CharRange;
use serde::Serialize;
use crate::{
@@ -209,10 +208,6 @@ pub(in crate::analysis) fn build_obligations_in_body<'tcx>(
body_id: BodyId,
typeck_results: &'tcx TypeckResults<'tcx>,
) -> (FullData<'tcx>, ObligationsInBody) {
- let hir = tcx.hir();
- let source_map = tcx.sess.source_map();
- let body = hir.body(body_id);
-
let obligations = tls::take_obligations();
let obligation_data = tls::unsafe_take_data();
diff --git a/crates/argus/src/analysis/mod.rs b/crates/argus/src/analysis/mod.rs
index c03af89..9407bb8 100644
--- a/crates/argus/src/analysis/mod.rs
+++ b/crates/argus/src/analysis/mod.rs
@@ -6,16 +6,18 @@ mod transform;
use anyhow::Result;
use fluid_let::fluid_let;
use rustc_hir::BodyId;
-use rustc_middle::ty::{print, TyCtxt};
+use rustc_middle::ty::TyCtxt;
pub(crate) use tls::{FullObligationData, SynIdx, UODIdx};
+#[cfg(feature = "testing")]
+use crate::types::intermediate::FullData;
pub(crate) use crate::types::intermediate::{
EvaluationResult, FulfillmentData,
};
use crate::{
ext::TyCtxtExt,
proof_tree::SerializedTree,
- types::{intermediate::FullData, ObligationsInBody, Target},
+ types::{ObligationsInBody, Target},
};
fluid_let! {
diff --git a/crates/argus/src/analysis/transform.rs b/crates/argus/src/analysis/transform.rs
index 7ea8dd0..0cc11b8 100644
--- a/crates/argus/src/analysis/transform.rs
+++ b/crates/argus/src/analysis/transform.rs
@@ -249,7 +249,7 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
.filter(|(_, that_id)| self.tcx.is_parent_of(**that_id, this_id))
.collect::>();
- let Some((expr_id, hir_id)) =
+ let Some((expr_id, _hir_id)) =
matching_expressions.iter().copied().find(|(_, this_id)| {
matching_expressions
.iter()
@@ -497,7 +497,6 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
let syn_id = self.synthetic_data.add(SyntheticData {
full_data: full_query_idx,
obligation: obligation.clone(),
- result: res,
});
let with_provenance = compute_provenance(
diff --git a/crates/argus/src/proof_tree/ext.rs b/crates/argus/src/proof_tree/ext.rs
index a8f36e9..2b4242c 100644
--- a/crates/argus/src/proof_tree/ext.rs
+++ b/crates/argus/src/proof_tree/ext.rs
@@ -1,9 +1,5 @@
-use rustc_hir::{def::Namespace, def_id::DefId, definitions::DefPathData};
+use rustc_hir::def_id::DefId;
use rustc_infer::infer::InferCtxt;
-use rustc_middle::ty::{
- print::{FmtPrinter, Print},
- TyCtxt,
-};
use rustc_trait_selection::{
solve::inspect::InspectCandidate,
traits::{
@@ -12,8 +8,10 @@ use rustc_trait_selection::{
},
};
+use crate::types::intermediate::EvaluationResult;
+
/// Pretty printing for results.
-pub trait PrettyResultExt {
+pub trait EvaluationResultExt {
fn pretty(&self) -> String;
fn is_yes(&self) -> bool;
}
@@ -25,17 +23,8 @@ pub trait CandidateExt {
fn is_informative_probe(&self) -> bool;
}
-// -----------------------------------------------
-// Impls
-
-// impl<'a, 'tcx, T: Print<'tcx, FmtPrinter<'a, 'tcx>>> PrettyPrintExt<'a, 'tcx>
-// for T
-// {
-// /* intentionally blank */
-// }
-
/// Pretty printer for results
-impl PrettyResultExt for Result {
+impl EvaluationResultExt for EvaluationResult {
fn is_yes(&self) -> bool {
matches!(self, Ok(Certainty::Yes))
}
diff --git a/crates/argus/src/proof_tree/mod.rs b/crates/argus/src/proof_tree/mod.rs
index 583d404..f5e97ea 100644
--- a/crates/argus/src/proof_tree/mod.rs
+++ b/crates/argus/src/proof_tree/mod.rs
@@ -119,9 +119,11 @@ impl Goal {
result: EvaluationResult,
) -> Self {
let necessity = infcx.guess_predicate_necessity(&goal.predicate);
+ let goal = infcx.resolve_vars_if_possible(*goal);
let num_vars =
serialize::var_counter::count_vars(infcx.tcx, goal.predicate);
- let goal_value = serialize_to_value(infcx, &GoalPredicateDef(*goal))
+
+ let goal_value = serialize_to_value(infcx, &GoalPredicateDef(goal))
.expect("failed to serialize goal");
Self {
diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs
index bfe7a9c..5042bed 100644
--- a/crates/argus/src/proof_tree/serialize.rs
+++ b/crates/argus/src/proof_tree/serialize.rs
@@ -1,7 +1,7 @@
use std::{collections::HashSet, ops::ControlFlow};
use anyhow::{bail, Result};
-use ext::*;
+use ext::{CandidateExt, EvaluationResultExt};
use index_vec::IndexVec;
use rustc_hir::def_id::DefId;
use rustc_infer::infer::InferCtxt;
@@ -65,22 +65,26 @@ impl SerializedTreeVisitor {
})
}
- fn check_for_cycle_from(&mut self, from: ProofNodeIdx) {
+ // TODO: cycle detection is too expensive for large trees, and strictly
+ // comparing the JSON values is a bad idea in general. We should wait
+ // until the new trait solver has some mechanism for detecting cycles
+ // and piggy back off that.
+ fn check_for_cycle_from(&mut self, _from: ProofNodeIdx) {
return;
- if self.cycle.is_some() {
- return;
- }
+ // if self.cycle.is_some() {
+ // return;
+ // }
- let to_root = self.topology.path_to_root(from);
+ // let to_root = self.topology.path_to_root(from);
- let node_start = &self.nodes[from];
- if to_root.iter_exclusive().any(|idx| {
- let n = &self.nodes[*idx];
- n == node_start
- }) {
- self.cycle = Some(to_root.into());
- }
+ // let node_start = &self.nodes[from];
+ // if to_root.iter_exclusive().any(|idx| {
+ // let n = &self.nodes[*idx];
+ // n == node_start
+ // }) {
+ // self.cycle = Some(to_root.into());
+ // }
}
}
diff --git a/crates/argus/src/proof_tree/topology.rs b/crates/argus/src/proof_tree/topology.rs
index 3e43039..bae3652 100644
--- a/crates/argus/src/proof_tree/topology.rs
+++ b/crates/argus/src/proof_tree/topology.rs
@@ -106,78 +106,19 @@ impl TreeTopology {
}
}
- // pub fn children(
- // &self,
- // from: ProofNodeIdx,
- // ) -> impl Iterator- {
- // let v = match self.children.get(&from) {
- // // Normally there are relatively few children.
- // Some(kids) => kids
- // .iter()
- // .copied()
- // .collect::>(),
- // None => SmallVec::<[ProofNodeIdx; 8]>::default(),
- // };
-
- // v.into_iter()
- // }
-
pub fn parent(&self, to: ProofNodeIdx) -> Option {
self.parent.get(&to).copied()
}
- // pub fn is_parent_of(
- // &self,
- // parent: ProofNodeIdx,
- // child: ProofNodeIdx,
- // ) -> bool {
- // if let Some(p) = self.parent(child) {
- // p == parent
- // } else {
- // false
- // }
- // }
-
- // pub fn is_child_of(&self, child: ProofNodeIdx, parent: ProofNodeIdx) -> bool {
- // self.is_parent_of(parent, child)
- // }
-
- // #[must_use]
- // pub fn add_in(&mut self, rhs: Self) -> Option<()> {
- // let lhs_keys = self.children.keys().collect::>();
- // for key in rhs.children.keys() {
- // if lhs_keys.contains(key) {
- // return None;
- // }
- // }
-
- // self.children.extend(rhs.children.into_iter());
- // self.parent.extend(rhs.parent.into_iter());
-
- // Some(())
- // }
-
- // pub fn is_member(&self, node: ProofNodeIdx) -> bool {
- // self
- // .children
- // .keys()
- // .chain(self.parent.keys())
- // .find(|&&n| n == node)
- // .is_some()
- // }
-
- // pub fn leaves(&self) -> impl Iterator
- + '_ {
- // self.parent.keys().filter(|n| self.is_leaf(**n)).copied()
- // }
-
pub fn path_to_root(&self, node: ProofNodeIdx) -> Path {
let mut root = node;
let mut curr = Some(node);
let path = std::iter::from_fn(move || {
+ let rootp = &mut root;
let prev = curr;
if let Some(n) = curr {
curr = self.parent(n);
- root = n;
+ *rootp = n;
}
prev
diff --git a/crates/argus/src/serialize/const.rs b/crates/argus/src/serialize/const.rs
index 4a2817c..658bcae 100644
--- a/crates/argus/src/serialize/const.rs
+++ b/crates/argus/src/serialize/const.rs
@@ -70,11 +70,7 @@ enum ConstKindDef<'tcx> {
#[cfg_attr(feature = "testing", ts(type = "BoundVariable"))]
data: BoundVariable,
},
- // TODO:
- // Placeholder {
- // #[serde(skip)] // TODO:
- // data: &'a Placeholder,
- // },
+ Placeholder,
Value {
#[cfg_attr(feature = "testing", ts(type = "ValTree"))]
data: ValTreeDef<'tcx>,
@@ -93,19 +89,19 @@ impl<'a, 'tcx: 'a> From<&Const<'tcx>> for ConstKindDef<'tcx> {
let kind = value.kind();
match kind {
- ConstKind::Unevaluated(uc) => ConstKindDef::Unevaluated { data: uc },
- ConstKind::Param(v) => ConstKindDef::Param { data: v },
- ConstKind::Value(v) => ConstKindDef::Value {
+ ConstKind::Unevaluated(uc) => Self::Unevaluated { data: uc },
+ ConstKind::Param(v) => Self::Param { data: v },
+ ConstKind::Value(v) => Self::Value {
data: ValTreeDef::new(v, self_ty),
},
- ConstKind::Expr(e) => ConstKindDef::Expr { data: e },
- ConstKind::Error(..) => ConstKindDef::Error,
+ ConstKind::Expr(e) => Self::Expr { data: e },
+ ConstKind::Error(..) => Self::Error,
- ConstKind::Bound(didx, bv) => ConstKindDef::Bound {
+ ConstKind::Bound(didx, bv) => Self::Bound {
data: BoundVariable::new(didx, bv),
},
- ConstKind::Infer(ic) => ConstKindDef::Infer { data: ic },
- ConstKind::Placeholder(..) => todo!(),
+ ConstKind::Infer(ic) => Self::Infer { data: ic },
+ ConstKind::Placeholder(..) => Self::Placeholder,
}
}
}
@@ -113,8 +109,7 @@ impl<'a, 'tcx: 'a> From<&Const<'tcx>> for ConstKindDef<'tcx> {
#[derive(Serialize)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export, rename = "InferConst"))]
-#[serde(tag = "type")]
-enum InferConstKindDef {
+pub enum InferConstDef {
// TODO: the `ConstVariableOrigin` doesn't seem to be publicly exposed.
// If it were, we could probe the InferCtxt for the origin of an unresolved
// infer var, potentially resulting in a named constant. But that isn't possible
@@ -126,43 +121,39 @@ enum InferConstKindDef {
Anon,
}
-pub struct InferConstDef;
impl InferConstDef {
- pub fn serialize<'tcx, S>(value: &InferConst, s: S) -> Result
- where
- S: serde::Serializer,
- {
- InferConstKindDef::from(value).serialize(s)
- }
-}
-
-impl From<&InferConst> for InferConstKindDef {
- fn from(value: &InferConst) -> Self {
+ pub fn new(value: &InferConst) -> Self {
// TODO: can we get the name of an inference variable?
match value {
InferConst::Fresh(_) | InferConst::EffectVar(_) | InferConst::Var(_) => {
- InferConstKindDef::Anon
+ Self::Anon
}
}
}
+
+ pub fn serialize<'tcx, S>(value: &InferConst, s: S) -> Result
+ where
+ S: serde::Serializer,
+ {
+ Self::new(value).serialize(s)
+ }
}
#[derive(Serialize)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export, rename = "ParamConst"))]
-pub struct ParamConstDefDef(
+pub struct ParamConstDef(
#[serde(with = "SymbolDef")]
#[cfg_attr(feature = "testing", ts(type = "Symbol"))]
Symbol,
);
-pub struct ParamConstDef;
impl ParamConstDef {
pub fn serialize<'tcx, S>(value: &ParamConst, s: S) -> Result
where
S: serde::Serializer,
{
- ParamConstDefDef(value.name).serialize(s)
+ Self(value.name).serialize(s)
}
}
@@ -227,56 +218,11 @@ impl<'tcx> UnevaluatedConstDef<'tcx> {
}
}
-pub struct AliasConstDef;
-impl AliasConstDef {
- pub fn serialize<'tcx, S>(
- value: &UnevaluatedConst<'tcx>,
- s: S,
- ) -> Result
- where
- S: serde::Serializer,
- {
- UnevaluatedConstDef::serialize(value, s)
- }
-}
-
-pub struct BoundConstDef;
-impl BoundConstDef {
- pub fn serialize<'tcx, S>(value: &BoundVar, s: S) -> Result
- where
- S: serde::Serializer,
- {
- // BoundVarDef::serialize(value, s)
- todo!()
- }
-}
-
-pub struct ExprConstDef;
-impl ExprConstDef {
- pub fn serialize<'tcx, S>(value: &Expr<'tcx>, s: S) -> Result
- where
- S: serde::Serializer,
- {
- ExprDef::serialize(value, s)
- }
-}
-
-pub struct ConstScalarIntDef<'tcx> {
- int: ScalarInt,
- ty: Ty<'tcx>,
-}
-
-impl<'tcx> ConstScalarIntDef<'tcx> {
- pub fn new(int: ScalarInt, ty: Ty<'tcx>) -> Self {
- Self { int, ty }
- }
-}
-
#[derive(Serialize)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export, rename = "ConstScalarInt"))]
#[serde(tag = "type")]
-enum ConstScalarIntDefDef {
+pub enum ConstScalarIntDef {
False,
True,
#[serde(rename_all = "camelCase")]
@@ -295,68 +241,58 @@ enum ConstScalarIntDefDef {
},
}
-impl<'tcx> From<&ConstScalarIntDef<'tcx>> for ConstScalarIntDefDef {
- fn from(value: &ConstScalarIntDef<'tcx>) -> Self {
+impl<'tcx> ConstScalarIntDef {
+ pub fn new(int: ScalarInt, ty: Ty<'tcx>) -> Self {
let infcx = get_dynamic_ctx();
let tcx = infcx.tcx;
- let this = value;
- match this.ty.kind() {
- Bool if this.int == ScalarInt::FALSE => ConstScalarIntDefDef::False,
- Bool if this.int == ScalarInt::TRUE => ConstScalarIntDefDef::True,
+ match ty.kind() {
+ Bool if int == ScalarInt::FALSE => Self::False,
+ Bool if int == ScalarInt::TRUE => Self::True,
Float(FloatTy::F32) => {
- let val = Single::try_from(this.int).unwrap();
- ConstScalarIntDefDef::Float {
+ let val = Single::try_from(int).unwrap();
+ Self::Float {
data: format!("{val}"),
is_finite: val.is_finite(),
}
}
Float(FloatTy::F64) => {
- let val = Double::try_from(this.int).unwrap();
- ConstScalarIntDefDef::Float {
+ let val = Double::try_from(int).unwrap();
+ Self::Float {
data: format!("{val}"),
is_finite: val.is_finite(),
}
}
Uint(_) | Int(_) => {
- // let int = ConstInt::new(
- // this.int,
- // matches!(this.ty.kind(), Int(_)),
- // this.ty.is_ptr_sized_integral(),
- // );
- ConstScalarIntDefDef::Int {
- data: format!("{}", this.int),
+ let int = ConstInt::new(
+ int,
+ matches!(ty.kind(), Int(_)),
+ ty.is_ptr_sized_integral(),
+ );
+ Self::Int {
+ data: format!("{:?}", int),
}
}
- Char if char::try_from(this.int).is_ok() => ConstScalarIntDefDef::Char {
- data: format!("{}", char::try_from(this.int).is_ok()),
+ Char if char::try_from(int).is_ok() => Self::Char {
+ data: format!("{}", char::try_from(int).is_ok()),
},
Ref(..) | RawPtr(..) | FnPtr(_) => {
- let data = this.int.assert_bits(tcx.data_layout.pointer_size);
- ConstScalarIntDefDef::Misc {
+ let data = int.assert_bits(tcx.data_layout.pointer_size);
+ Self::Misc {
data: format!("0x{data:x}"),
}
}
_ => {
- if this.int.size() == Size::ZERO {
- ConstScalarIntDefDef::Misc {
+ if int.size() == Size::ZERO {
+ Self::Misc {
data: "transmute(())".to_string(),
}
} else {
- ConstScalarIntDefDef::Misc {
- data: format!("transmute(0x{:x})", this.int),
+ Self::Misc {
+ data: format!("transmute(0x{:x})", int),
}
}
}
}
}
}
-
-impl<'tcx> Serialize for ConstScalarIntDef<'tcx> {
- fn serialize
(&self, s: S) -> Result
- where
- S: serde::Serializer,
- {
- ConstScalarIntDefDef::from(self).serialize(s)
- }
-}
diff --git a/crates/argus/src/serialize/mod.rs b/crates/argus/src/serialize/mod.rs
index c7fb48b..f87e745 100644
--- a/crates/argus/src/serialize/mod.rs
+++ b/crates/argus/src/serialize/mod.rs
@@ -116,6 +116,7 @@ macro_rules! define_helper {
pub struct $helper(bool);
impl $helper {
+ #[allow(dead_code)]
pub fn new() -> $helper {
$helper($tl.with(|c| c.replace(true)))
}
diff --git a/crates/argus/src/serialize/path/mod.rs b/crates/argus/src/serialize/path/mod.rs
index f871978..1c8f583 100644
--- a/crates/argus/src/serialize/path/mod.rs
+++ b/crates/argus/src/serialize/path/mod.rs
@@ -211,6 +211,7 @@ impl<'a, 'tcx: 'a> PathBuilder<'a, 'tcx> {
self.infcx.should_print_verbose()
}
+ #[allow(dead_code)]
pub fn print_value_path(
&mut self,
def_id: DefId,
diff --git a/crates/argus/src/serialize/path/pretty.rs b/crates/argus/src/serialize/path/pretty.rs
index 8181c2f..7e3487f 100644
--- a/crates/argus/src/serialize/path/pretty.rs
+++ b/crates/argus/src/serialize/path/pretty.rs
@@ -95,24 +95,22 @@ impl<'a, 'tcx: 'a> PathBuilder<'a, 'tcx> {
}
pub fn try_print_trimmed_def_path(&mut self, def_id: DefId) -> bool {
- return false; // FIXME:(gavinleroy)
-
- // if with_forced_trimmed_paths() && self.force_print_trimmed_def_path(def_id)
- // {
- // return true;
- // }
- // if self.tcx().sess.opts.unstable_opts.trim_diagnostic_paths
- // && self.tcx().sess.opts.trimmed_def_paths
- // && !with_no_trimmed_paths()
- // && !with_crate_prefix()
- // && let Some(symbol) = self.tcx().trimmed_def_paths(()).get(&def_id)
- // {
- // // CHANGE: write!(self, "{}", Ident::with_dummy_span(*symbol))?;
- // self.segments.push(PathSegment::unambiguous_name(*symbol));
- // true
- // } else {
- // false
- // }
+ if with_forced_trimmed_paths() && self.force_print_trimmed_def_path(def_id)
+ {
+ return true;
+ }
+ if self.tcx().sess.opts.unstable_opts.trim_diagnostic_paths
+ && self.tcx().sess.opts.trimmed_def_paths
+ && !with_no_trimmed_paths()
+ && !with_crate_prefix()
+ && let Some(symbol) = self.tcx().trimmed_def_paths(()).get(&def_id)
+ {
+ // CHANGE: write!(self, "{}", Ident::with_dummy_span(*symbol))?;
+ self.segments.push(PathSegment::unambiguous_name(*symbol));
+ true
+ } else {
+ false
+ }
}
/// Does the work of `try_print_visible_def_path`, building the
@@ -332,8 +330,6 @@ impl<'a, 'tcx: 'a> PathBuilder<'a, 'tcx> {
// print the enum name and the variant name. Otherwise, we do not print anything and let the
// caller use the `print_def_path` fallback.
fn force_print_trimmed_def_path(&mut self, def_id: DefId) -> bool {
- return false; // FIXME:(gavin);
-
let key = self.tcx().def_key(def_id);
let visible_parent_map = self.tcx().visible_parent_map(());
let kind = self.tcx().def_kind(def_id);
@@ -359,19 +355,18 @@ impl<'a, 'tcx: 'a> PathBuilder<'a, 'tcx> {
name
}
};
- // FIXME:(gavinleroy)
- // if let DefKind::Variant = kind
- // && let Some(symbol) = self.tcx().trimmed_def_paths(()).get(&def_id)
- // {
- // // If `Assoc` is unique, we don't want to talk about `Trait::Assoc`.
- // // CHANGE: self.write_str(get_local_name(self, *symbol, def_id, key).as_str())?;
- // self
- // .segments
- // .push(PathSegment::unambiguous_name(get_local_name(
- // self, *symbol, def_id, key,
- // )));
- // return true;
- // }
+ if let DefKind::Variant = kind
+ && let Some(symbol) = self.tcx().trimmed_def_paths(()).get(&def_id)
+ {
+ // If `Assoc` is unique, we don't want to talk about `Trait::Assoc`.
+ // CHANGE: self.write_str(get_local_name(self, *symbol, def_id, key).as_str())?;
+ self
+ .segments
+ .push(PathSegment::unambiguous_name(get_local_name(
+ self, *symbol, def_id, key,
+ )));
+ return true;
+ }
if let Some(symbol) = key.get_opt_name() {
if let DefKind::AssocConst | DefKind::AssocFn | DefKind::AssocTy = kind
&& let Some(parent) = self.tcx().opt_parent(def_id)
diff --git a/crates/argus/src/serialize/term.rs b/crates/argus/src/serialize/term.rs
index d0bb8cc..0830e38 100644
--- a/crates/argus/src/serialize/term.rs
+++ b/crates/argus/src/serialize/term.rs
@@ -82,7 +82,7 @@ enum ValTreeKind<'tcx> {
Leaf {
#[cfg_attr(feature = "testing", ts(type = "ConstScalarInt"))]
- data: ConstScalarIntDef<'tcx>,
+ data: ConstScalarIntDef,
kind: LeafKind,
},
}
diff --git a/crates/argus/src/serialize/ty.rs b/crates/argus/src/serialize/ty.rs
index cced5d1..ab006fb 100644
--- a/crates/argus/src/serialize/ty.rs
+++ b/crates/argus/src/serialize/ty.rs
@@ -29,7 +29,6 @@ impl<'tcx> TyDef<'tcx> {
}
}
-pub type TysDef = Slice__TyDef;
pub struct Slice__TyDef;
impl Slice__TyDef {
pub fn serialize<'tcx, S>(
@@ -377,16 +376,6 @@ impl<'tcx> PolyExistentialPredicatesDef<'tcx> {
Self { data, auto_traits }
}
-
- pub fn serialize(
- value: &ty::List>,
- s: S,
- ) -> Result
- where
- S: serde::Serializer,
- {
- Self::new(value).serialize(s)
- }
}
// -----------------------------------
@@ -958,48 +947,66 @@ pub enum GenericArgKindDef<'tcx> {
// TODO: gavinleroy
#[derive(Serialize)]
-#[serde(tag = "type")]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export, rename = "InferTy"))]
pub enum InferTyDef<'tcx> {
IntVar,
FloatVar,
- // TODO: We should also include source information
- #[serde(rename_all = "camelCase")]
- Named {
+ Named(
#[serde(with = "SymbolDef")]
#[cfg_attr(feature = "testing", ts(type = "Symbol"))]
- name: Symbol,
- path_def: path::PathDefNoArgs<'tcx>,
- },
+ Symbol,
+ path::PathDefNoArgs<'tcx>,
+ ),
+ Unnamed(path::PathDefNoArgs<'tcx>),
+ SourceInfo(String),
Unresolved,
}
impl<'tcx> InferTyDef<'tcx> {
pub fn new(value: &ty::InferTy) -> Self {
- use rustc_infer::infer::type_variable::TypeVariableOriginKind::TypeParameterDefinition;
+ use rustc_infer::infer::type_variable::{
+ TypeVariableOrigin, TypeVariableOriginKind::*,
+ };
let infcx = get_dynamic_ctx();
let tcx = infcx.tcx;
- let ty = ty::Ty::new_infer(tcx, *value);
+ let root_value = if let ty::InferTy::TyVar(v) = value {
+ ty::InferTy::TyVar(infcx.root_var(*v))
+ } else {
+ *value
+ };
- if let Some(type_origin) = infcx.type_var_origin(ty)
- && let TypeParameterDefinition(name, def_id) = type_origin.kind
- {
- Self::Named {
- name,
- path_def: path::PathDefNoArgs::new(def_id),
+ let ty = ty::Ty::new_infer(tcx, root_value);
+
+ match infcx.type_var_origin(ty) {
+ Some(TypeVariableOrigin {
+ kind: TypeParameterDefinition(name, def_id),
+ ..
+ }) => Self::Named(name, path::PathDefNoArgs::new(def_id)),
+
+ Some(TypeVariableOrigin {
+ kind: OpaqueTypeInference(def_id),
+ ..
+ }) => Self::Unnamed(path::PathDefNoArgs::new(def_id)),
+
+ Some(TypeVariableOrigin { span, .. }) if !span.is_dummy() => {
+ let span = rustc_span::Span::source_callsite(span);
+ if let Ok(snippet) = tcx.sess.source_map().span_to_snippet(span) {
+ Self::SourceInfo(snippet)
+ } else {
+ Self::Unresolved
+ }
}
- } else {
- match value {
- // TODO: can we do any better in these cases??
- ty::InferTy::TyVar(_) | ty::InferTy::FreshTy(_) => Self::Unresolved,
+
+ _ => match value {
ty::InferTy::IntVar(_) | ty::InferTy::FreshIntTy(_) => Self::IntVar,
ty::InferTy::FloatVar(_) | ty::InferTy::FreshFloatTy(_) => {
Self::FloatVar
}
- }
+ ty::InferTy::TyVar(_) | ty::InferTy::FreshTy(_) => Self::Unresolved,
+ },
}
}
@@ -1493,13 +1500,6 @@ pub struct ProjectionPredicateDef<'tcx> {
pub term: ty::Term<'tcx>,
}
-#[derive(Serialize)]
-#[serde(remote = "ty::UniverseIndex")]
-pub struct UniverseIndexDef {
- #[serde(skip)]
- pub(crate) private: u32,
-}
-
#[derive(Serialize)]
#[serde(remote = "ty::CoercePredicate")]
#[cfg_attr(feature = "testing", derive(TS))]
@@ -1552,22 +1552,6 @@ impl Slice__SymbolDef {
}
}
-pub struct Option__SymbolDef;
-impl Option__SymbolDef {
- pub fn serialize<'tcx, S>(
- value: &Option,
- s: S,
- ) -> Result
- where
- S: serde::Serializer,
- {
- match value {
- None => s.serialize_none(),
- Some(sym) => SymbolDef::serialize(sym, s),
- }
- }
-}
-
#[derive(Serialize)]
#[serde(remote = "ty::AliasRelationDirection")]
#[cfg_attr(feature = "testing", derive(TS))]
@@ -1580,11 +1564,16 @@ pub enum AliasRelationDirectionDef {
#[derive(Serialize)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export))]
-pub enum BoundVariable {}
+pub enum BoundVariable {
+ Error(String),
+}
impl BoundVariable {
- pub fn new(debruijn_idx: ty::DebruijnIndex, var: ty::BoundVar) -> Self {
- todo!("bound variables are not yet possible")
+ pub fn new(didx: ty::DebruijnIndex, var: ty::BoundVar) -> Self {
+ // FIXME: bound varialbes shouldn't be in serialized types, I haven't
+ // encountered one in the raw output, and before release this was a
+ // `panic`, which never fired.
+ Self::Error(format!("{var:?}^{didx:?}").to_string())
}
}
@@ -1627,7 +1616,9 @@ pub struct FnTrait<'tcx> {
#[cfg_attr(feature = "testing", ts(type = "Ty | undefined"))]
ret_ty: Option>,
- kind: FnTraitKind,
+ #[serde(with = "ClosureKindDef")]
+ #[cfg_attr(feature = "testing", ts(type = "ClosureKind"))]
+ kind: ty::ClosureKind,
}
#[derive(Serialize)]
@@ -1658,15 +1649,6 @@ pub struct AssocItemDef<'tcx> {
term: ty::Term<'tcx>,
}
-#[derive(Serialize)]
-#[cfg_attr(feature = "testing", derive(TS))]
-#[cfg_attr(feature = "testing", ts(export))]
-pub enum FnTraitKind {
- FnMut,
- Fn,
- FnOnce,
-}
-
impl<'tcx> OpaqueImpl<'tcx> {
fn insert_trait_and_projection(
tcx: ty::TyCtxt<'tcx>,
@@ -1830,11 +1812,11 @@ impl<'tcx> OpaqueImpl<'tcx> {
if matches!(arg_tys.kind(), ty::Tuple(_)) =>
{
let kind = if entry.fn_trait_ref.is_some() {
- FnTraitKind::Fn
+ ty::ClosureKind::Fn
} else if entry.fn_mut_trait_ref.is_some() {
- FnTraitKind::FnMut
+ ty::ClosureKind::FnMut
} else {
- FnTraitKind::FnOnce
+ ty::ClosureKind::FnOnce
};
let params = arg_tys.tuple_fields().iter().collect::>();
diff --git a/crates/argus/src/types.rs b/crates/argus/src/types.rs
index f8ce81e..91bc413 100644
--- a/crates/argus/src/types.rs
+++ b/crates/argus/src/types.rs
@@ -568,7 +568,6 @@ pub(super) mod intermediate {
// points to the used `InferCtxt`
pub full_data: UODIdx,
pub obligation: PredicateObligation<'tcx>,
- pub result: EvaluationResult,
}
pub(crate) struct SyntheticQueriesInBody<'tcx>(
diff --git a/crates/argus_cli/tests/workspaces/axum/src/tests/request_not_last.rs b/crates/argus_cli/tests/workspaces/axum/src/tests/request_not_last.rs
index c0b07b9..5e2f9ac 100644
--- a/crates/argus_cli/tests/workspaces/axum/src/tests/request_not_last.rs
+++ b/crates/argus_cli/tests/workspaces/axum/src/tests/request_not_last.rs
@@ -1,8 +1,9 @@
use axum::{body::Body, extract::Extension, http::Request};
+
use super::*;
async fn handler(_: Request, _: Extension) {}
fn test() {
- use_as_handler(handler);
+ use_as_handler(handler);
}
diff --git a/ide/packages/extension/package.json b/ide/packages/extension/package.json
index 62fff47..1b505bf 100644
--- a/ide/packages/extension/package.json
+++ b/ide/packages/extension/package.json
@@ -60,6 +60,7 @@
"glob": "^8.1.0",
"lodash": "^4.17.21",
"new-github-issue-url": "^1.0.0",
+ "open": "^8.2.1",
"react": "^18.0.0",
"react-dom": "^18.0.0",
"toml": "^3.0.0",
diff --git a/ide/packages/extension/src/commands.ts b/ide/packages/extension/src/commands.ts
index 4f6b4c1..7001c0c 100644
--- a/ide/packages/extension/src/commands.ts
+++ b/ide/packages/extension/src/commands.ts
@@ -2,6 +2,7 @@ import { BodyHash, ExprIdx, ObligationHash } from "@argus/common/bindings";
import { Filename } from "@argus/common/lib";
import { Cmd, Ctx } from "./ctx";
+import * as errors from "./errors";
export function inspect(ctx: Ctx): Cmd {
return async () => {
@@ -19,3 +20,9 @@ export function openError(ctx: Ctx): Cmd {
ctx.view!.blingObligation(file, bh, ei, oblHash);
};
}
+
+export function lastError(ctx: Ctx): Cmd {
+ return async () => {
+ return errors.lastError(ctx.extCtx);
+ };
+}
diff --git a/ide/packages/extension/src/ctx.ts b/ide/packages/extension/src/ctx.ts
index 791d76f..49ba939 100644
--- a/ide/packages/extension/src/ctx.ts
+++ b/ide/packages/extension/src/ctx.ts
@@ -25,7 +25,6 @@ import {
import { showErrorDialog } from "./errors";
import { globals } from "./main";
import { setup } from "./setup";
-import { StatusBar } from "./statusbar";
import {
RustEditor,
isDocumentInWorkspace,
@@ -409,6 +408,11 @@ class BackendCache {
// it is possible that no tree is returned. (Yes, but I'm working on it.)
const tree0 = _.compact(res.value)[0];
if (tree0 === undefined) {
+ showErrorDialog(`
+ Argus failed to find the appropriate proof tree.
+
+ This is likely a bug in Argus, please report it.
+ `);
return;
}
diff --git a/ide/packages/extension/src/errors.ts b/ide/packages/extension/src/errors.ts
index cb06558..bd7b5eb 100644
--- a/ide/packages/extension/src/errors.ts
+++ b/ide/packages/extension/src/errors.ts
@@ -1,6 +1,7 @@
import { ArgusError } from "@argus/common/lib";
import cp from "child_process";
import newGithubIssueUrl from "new-github-issue-url";
+import open from "open";
import os from "os";
import vscode from "vscode";
@@ -58,7 +59,7 @@ export const showError = async (error: ArgusError) => {
}
};
-export async function last_error(context: vscode.ExtensionContext) {
+export async function lastError(context: vscode.ExtensionContext) {
const error = context.workspaceState.get("err_log") as string;
await showError({ type: "build-error", error });
}
diff --git a/ide/packages/extension/src/main.ts b/ide/packages/extension/src/main.ts
index b566480..547bcb0 100644
--- a/ide/packages/extension/src/main.ts
+++ b/ide/packages/extension/src/main.ts
@@ -53,5 +53,6 @@ function createCommands(): Record {
// Private commands used internally, these should not appear in the command palette.
openError: { enabled: commands.openError },
+ lastError: { enabled: commands.lastError },
};
}
diff --git a/ide/packages/extension/src/setup.ts b/ide/packages/extension/src/setup.ts
index a16da35..ba1d614 100644
--- a/ide/packages/extension/src/setup.ts
+++ b/ide/packages/extension/src/setup.ts
@@ -1,6 +1,7 @@
import { ArgusArgs, CallArgus, Result } from "@argus/common/lib";
import cp from "child_process";
import _ from "lodash";
+import open from "open";
import os from "os";
import path from "path";
import vscode from "vscode";
@@ -89,18 +90,19 @@ const execNotifyBinary = async (
});
globals.statusBar.setState("loading", title);
-
return new Promise((resolve, reject) => {
proc.addListener("close", _ => {
globals.statusBar.setState("idle");
if (proc.exitCode !== 0) {
+ globals.statusBar.setState("error");
reject(stderrChunks.join(""));
} else {
resolve(Buffer.concat(stdoutChunks));
}
});
+
proc.addListener("error", e => {
- globals.statusBar.setState("idle");
+ globals.statusBar.setState("error");
reject(e.toString());
});
});
@@ -217,6 +219,9 @@ const checkVersionAndInstall = async (
);
if (choice === "Show fix") {
+ open(
+ "https://github.com/gavinleroy/argus/blob/master/README.md#rustup-fails-on-install"
+ );
await vscode.window.showInformationMessage(
'Click "Continue" once you have completed the fix.',
"Continue"
@@ -284,6 +289,7 @@ export async function setup(context: Ctx): Promise {
);
} catch (e: any) {
context.extCtx.workspaceState.update("err_log", e);
+ globals.statusBar.setState("error");
return {
type: "build-error",
error: e,
@@ -301,6 +307,7 @@ export async function setup(context: Ctx): Promise {
log("output", output);
outputTyped = JSON.parse(output);
} catch (e: any) {
+ globals.statusBar.setState("error");
return {
type: "analysis-error",
error: e.toString(),
@@ -310,6 +317,7 @@ export async function setup(context: Ctx): Promise {
log("Parsed output", outputTyped);
if ("Err" in outputTyped) {
+ globals.statusBar.setState("error");
return {
type: "analysis-error",
error: outputTyped.Err,
diff --git a/ide/packages/panoptes/src/HoverInfo.tsx b/ide/packages/panoptes/src/HoverInfo.tsx
index 4ff4f13..c8c75a2 100644
--- a/ide/packages/panoptes/src/HoverInfo.tsx
+++ b/ide/packages/panoptes/src/HoverInfo.tsx
@@ -1,5 +1,4 @@
import {
- FloatingDelayGroup,
FloatingPortal,
offset,
useFloating,
diff --git a/ide/packages/panoptes/src/Icons.css b/ide/packages/panoptes/src/Icons.css
index fb44e86..bc18678 100644
--- a/ide/packages/panoptes/src/Icons.css
+++ b/ide/packages/panoptes/src/Icons.css
@@ -1,4 +1,7 @@
.codicon {
position: relative;
top: 0.2em;
+
+ padding-right: 0.2em;
+ padding-left: 0.2em;
}
\ No newline at end of file
diff --git a/ide/packages/panoptes/src/TreeView/Directory.tsx b/ide/packages/panoptes/src/TreeView/Directory.tsx
index ecc6ebc..3e9f68e 100644
--- a/ide/packages/panoptes/src/TreeView/Directory.tsx
+++ b/ide/packages/panoptes/src/TreeView/Directory.tsx
@@ -66,12 +66,10 @@ type InfoWrapper = React.FC<{ n: ProofNodeIdx; Child: React.FC }>;
export const DirNode = ({
idx,
- styleEdge,
Children,
Wrapper = ({ n: _, Child }) => ,
}: {
idx: number;
- styleEdge: boolean;
Children: React.FC | null;
Wrapper: InfoWrapper;
}) => {
@@ -120,7 +118,6 @@ export const DirRecursive = ({
0
diff --git a/ide/packages/panoptes/src/TreeView/Graph.tsx b/ide/packages/panoptes/src/TreeView/Graph.tsx
index 7d9cfe0..bcbd4f0 100644
--- a/ide/packages/panoptes/src/TreeView/Graph.tsx
+++ b/ide/packages/panoptes/src/TreeView/Graph.tsx
@@ -32,7 +32,7 @@ const useCenteredTree = (
};
const getEdgeClass =
- (tree: TreeInfo) => (link: TreeLinkDatum, orientation: Orientation) => {
+ (tree: TreeInfo) => (link: TreeLinkDatum, _orientation: Orientation) => {
const sourceIdx = link.source.data.name as number;
const node = tree.node(sourceIdx);
return "Goal" in node
diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx
index 0827d7d..39e03bf 100644
--- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx
+++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx
@@ -6,11 +6,9 @@ import {
} from "@vscode/webview-ui-toolkit/react";
import _ from "lodash";
import React from "react";
-import ReactJson from "react-json-view";
import BottomUp from "./BottomUp";
import { TreeContext } from "./Context";
-import Graph from "./Graph";
import TopDown from "./TopDown";
import "./TreeApp.css";
import TreeCycle from "./TreeCycle";
diff --git a/ide/packages/panoptes/src/print/print.tsx b/ide/packages/panoptes/src/print/print.tsx
index 0cfd687..6c5b5b1 100644
--- a/ide/packages/panoptes/src/print/print.tsx
+++ b/ide/packages/panoptes/src/print/print.tsx
@@ -30,7 +30,7 @@ export const PrintWithFallback = ({
}) => {
const FallbackFromError = ({
error,
- resetErrorBoundary,
+ resetErrorBoundary: _,
}: {
error: any;
resetErrorBoundary: (...args: any[]) => void;
diff --git a/ide/packages/panoptes/src/print/private/const.tsx b/ide/packages/panoptes/src/print/private/const.tsx
index e571782..f3756d9 100644
--- a/ide/packages/panoptes/src/print/private/const.tsx
+++ b/ide/packages/panoptes/src/print/private/const.tsx
@@ -8,6 +8,7 @@ import {
import React from "react";
import { PrintDefPath, PrintValuePath } from "./path";
+import { DBraced, Placeholder } from "./syntax";
import { PrintExpr, PrintValueTree } from "./term";
import { PrintBoundVariable, PrintSymbol } from "./ty";
@@ -15,15 +16,15 @@ export const PrintConst = ({ o }: { o: Const }) => {
console.debug("Printing const", o);
switch (o.type) {
case "Error":
- return "{{const error}}";
+ return const error;
case "Param":
return ;
case "Infer":
return ;
case "Bound":
return ;
- // case "placeholder":
- // throw new Error("TODO");
+ case "Placeholder":
+ return _;
case "Unevaluated":
return ;
case "Value":
@@ -36,12 +37,10 @@ export const PrintConst = ({ o }: { o: Const }) => {
};
const PrintInferConst = ({ o }: { o: InferConst }) => {
- switch (o.type) {
- case "Anon": {
- return _;
- }
- default:
- throw new Error("Unknown infer const kind", o as any);
+ if (o === "Anon") {
+ return _;
+ } else {
+ throw new Error("Unknown infer const kind", o);
}
};
diff --git a/ide/packages/panoptes/src/print/private/path.tsx b/ide/packages/panoptes/src/print/private/path.tsx
index 3cbe936..abb094c 100644
--- a/ide/packages/panoptes/src/print/private/path.tsx
+++ b/ide/packages/panoptes/src/print/private/path.tsx
@@ -49,24 +49,14 @@ export const PrintDefPathShort = ({ o }: { o: DefinedPath }) => {
);
});
- return (
-
- {_.map(prefix, (segment, i) => {
- return ;
- })}
-
- );
+ return _.map(prefix, (segment, i) => (
+
+ ));
};
// PathSegment[]
export const PrintDefPathFull = ({ o }: { o: DefinedPath }) => {
- return (
- <>
- {_.map(o, (segment, i) => {
- return ;
- })}
- >
- );
+ return _.map(o, (segment, i) => );
};
export const PrintPathSegment = ({ o }: { o: PathSegment }) => {
@@ -89,10 +79,10 @@ export const PrintPathSegment = ({ o }: { o: PathSegment }) => {
? `#${o.disambiguator}`
: null;
return (
-
+ <>
{o.name}
{suffix}
-
+ >
);
}
case "Impl": {
@@ -101,6 +91,8 @@ export const PrintPathSegment = ({ o }: { o: PathSegment }) => {
return ;
case "As":
return ;
+ default:
+ throw new Error("Unknown impl kind", o.kind);
}
}
case "AnonImpl": {
diff --git a/ide/packages/panoptes/src/print/private/predicate.tsx b/ide/packages/panoptes/src/print/private/predicate.tsx
index 1f47107..6e66380 100644
--- a/ide/packages/panoptes/src/print/private/predicate.tsx
+++ b/ide/packages/panoptes/src/print/private/predicate.tsx
@@ -22,6 +22,7 @@ import {
PrintAliasTy,
PrintBinder,
PrintGenericArg,
+ PrintImplPolarity,
PrintRegion,
PrintTy,
} from "./ty";
@@ -71,31 +72,31 @@ export const PrintPredicateKind = ({ o }: { o: PredicateKind }) => {
return ;
} else if ("ObjectSafe" in o) {
return (
-
+ <>
The trait is object-safe
-
+ >
);
} else if ("Subtype" in o) {
const subty = o.Subtype;
const st = "<:";
return (
-
+ <>
{st}
-
+ >
);
} else if ("Coerce" in o) {
const coerce = o.Coerce;
return (
-
+ <>
→
-
+ >
);
} else if ("ConstEquate" in o) {
const [a, b] = o.ConstEquate;
return (
-
+ <>
=
-
+ >
);
} else if ("AliasRelate" in o) {
const [a, b, dir] = o.AliasRelate;
@@ -149,9 +150,9 @@ export const PrintClauseKind = ({ o }: { o: ClauseKind }) => {
} else if ("TypeOutlives" in o) {
const to = o.TypeOutlives;
return (
-
+ <>
:
-
+ >
);
} else if ("Projection" in o) {
const proj = o.Projection;
@@ -163,21 +164,21 @@ export const PrintClauseKind = ({ o }: { o: ClauseKind }) => {
} else if ("ConstArgHasType" in o) {
const [c, ty] = o.ConstArgHasType;
return (
-
+ <>
const as type
-
+ >
);
} else if ("WellFormed" in o) {
return (
-
+ <>
well-formed
-
+ >
);
} else if ("ConstEvaluatable" in o) {
return (
-
+ <>
can be evaluated
-
+ >
);
} else {
throw new Error("Unknown clause kind", o);
@@ -185,10 +186,9 @@ export const PrintClauseKind = ({ o }: { o: ClauseKind }) => {
};
export const PrintTraitPredicate = ({ o }: { o: TraitPredicate }) => {
- let polarity = o.polarity === "Negative" ? "!" : "";
return (
<>
- {polarity}
+
>
);
@@ -196,8 +196,8 @@ export const PrintTraitPredicate = ({ o }: { o: TraitPredicate }) => {
export const PrintTraitRef = ({ o }: { o: TraitRef }) => {
return (
-
+ <>
:
-
+ >
);
};
diff --git a/ide/packages/panoptes/src/print/private/syntax.css b/ide/packages/panoptes/src/print/private/syntax.css
index 329e6c5..1bfa01e 100644
--- a/ide/packages/panoptes/src/print/private/syntax.css
+++ b/ide/packages/panoptes/src/print/private/syntax.css
@@ -1,3 +1,7 @@
span.kw {
font-weight: bold;
+}
+
+span.placeholder {
+ color: var(--vscode-input-placeholderForeground);
}
\ No newline at end of file
diff --git a/ide/packages/panoptes/src/print/private/syntax.tsx b/ide/packages/panoptes/src/print/private/syntax.tsx
index b8e0083..7d6ea0b 100644
--- a/ide/packages/panoptes/src/print/private/syntax.tsx
+++ b/ide/packages/panoptes/src/print/private/syntax.tsx
@@ -9,6 +9,10 @@ import "./syntax.css";
// export const PathRoot: Ident = { name: "{{root}}" };
+export const Placeholder = ({ children }: React.PropsWithChildren) => {
+ return {children};
+};
+
export const Kw = ({ children }: React.PropsWithChildren) => {
return {children};
};
@@ -33,6 +37,36 @@ export const DBraced = ({ children }: React.PropsWithChildren) => {
);
};
+export const CBraced = ({ children }: React.PropsWithChildren) => {
+ return (
+
+ {"{"}
+ {children}
+ {"}"}
+
+ );
+};
+
+export const Parenthesized = ({ children }: React.PropsWithChildren) => {
+ return (
+
+ {"("}
+ {children}
+ {")"}
+
+ );
+};
+
+export const SqBraced = ({ children }: React.PropsWithChildren) => {
+ return (
+
+ {"["}
+ {children}
+ {"]"}
+
+ );
+};
+
const Interspersed = ({
components,
sep,
diff --git a/ide/packages/panoptes/src/print/private/term.tsx b/ide/packages/panoptes/src/print/private/term.tsx
index 41399ba..f833deb 100644
--- a/ide/packages/panoptes/src/print/private/term.tsx
+++ b/ide/packages/panoptes/src/print/private/term.tsx
@@ -14,7 +14,13 @@ import React from "react";
import { PrintConst } from "./const";
import { PrintConstScalarInt } from "./const";
import { PrintValuePath } from "./path";
-import { Angled, CommaSeparated, DBraced } from "./syntax";
+import {
+ Angled,
+ CommaSeparated,
+ DBraced,
+ Parenthesized,
+ SqBraced,
+} from "./syntax";
import { PrintSymbol, PrintTy } from "./ty";
export const PrintTerm = ({ o }: { o: Term }) => {
@@ -49,14 +55,14 @@ export const PrintExpr = ({ o }: { o: ExprDef }) => {
const [callable, args] = o.FunctionCall;
const argEs = _.map(args, arg => () => );
return (
-
+ <>
(
)
-
+ >
);
} else if ("Cast" in o) {
// TODO: handle cast kind "use"
- const [castKind, expr, ty] = o.Cast;
+ const [_castKind, expr, ty] = o.Cast;
return (
as
@@ -175,9 +181,9 @@ export const PrintValueTree = ({ o }: { o: ValTree }) => {
const PrintAggregateArray = ({ fields }: { fields: Const[] }) => {
const components = _.map(fields, field => () => );
return (
-
- []
-
+
+
+
);
};
@@ -185,10 +191,10 @@ const PrintAggregateTuple = ({ fields }: { fields: Const[] }) => {
const components = _.map(fields, field => () => );
const trailingComma = fields.length === 1 ? "," : null;
return (
- <>
- (
- {trailingComma})
- >
+
+
+ {trailingComma}
+
);
};
@@ -212,7 +218,10 @@ const PrintAggregateAdt = ({
const components = _.map(fields, field => () => );
return (
<>
- {head}()
+ {head}
+
+
+
>
);
}
diff --git a/ide/packages/panoptes/src/print/private/ty.tsx b/ide/packages/panoptes/src/print/private/ty.tsx
index b50f546..e8a5879 100644
--- a/ide/packages/panoptes/src/print/private/ty.tsx
+++ b/ide/packages/panoptes/src/print/private/ty.tsx
@@ -1,4 +1,5 @@
import {
+ Abi,
AliasTy,
AliasTyKind,
AssocItem,
@@ -28,14 +29,23 @@ import {
TypeAndMut,
UintTy,
} from "@argus/common/bindings";
-import _ from "lodash";
+import _, { isObject } from "lodash";
import React from "react";
import { Toggle } from "../../Toggle";
import { anyElems, fnInputsAndOutput, tyIsUnit } from "../../utilities/func";
import { PrintConst } from "./const";
import { PrintDefPath } from "./path";
-import { Angled, CommaSeparated, DBraced, PlusSeparated } from "./syntax";
+import {
+ Angled,
+ CBraced,
+ CommaSeparated,
+ DBraced,
+ Parenthesized,
+ Placeholder,
+ PlusSeparated,
+ SqBraced,
+} from "./syntax";
import { PrintTerm } from "./term";
export const PrintBinder = ({
@@ -52,8 +62,6 @@ export const PrintTy = ({ o }: { o: Ty }) => {
return ;
};
-// TODO: enums that don't have an inner object need to use a
-// comparison, instead of the `in` operator.
export const PrintTyKind = ({ o }: { o: TyKind }) => {
if ("Bool" === o) {
return "bool";
@@ -74,25 +82,24 @@ export const PrintTyKind = ({ o }: { o: TyKind }) => {
} else if ("Adt" in o) {
return ;
} else if ("Array" in o) {
- console.debug("Printing Array", o);
const [ty, sz] = o.Array;
return (
-
- [; ]
-
+
+ ;
+
);
} else if ("Slice" in o) {
return (
-
- []
-
+
+
+
);
} else if ("RawPtr" in o) {
const m = o.RawPtr.mutbl === "Not" ? "const" : "mut";
return (
-
+ <>
*{m}
-
+ >
);
} else if ("Ref" in o) {
const [r, ty, mtbl] = o.Ref;
@@ -101,9 +108,9 @@ export const PrintTyKind = ({ o }: { o: TyKind }) => {
mutbl: mtbl,
};
return (
-
+ <>
&
-
+ >
);
} else if ("FnDef" in o) {
return ;
@@ -112,9 +119,9 @@ export const PrintTyKind = ({ o }: { o: TyKind }) => {
} else if ("Tuple" in o) {
const components = _.map(o.Tuple, t => () => );
return (
-
- ()
-
+
+
+
);
} else if ("Placeholder" in o) {
return ;
@@ -189,9 +196,9 @@ export const PrintDynamicTy = ({ o }: { o: DynamicTyKind }) => {
const region = ;
const dynKind = o.kind === "Dyn" ? "dyn" : "dyn*";
return (
- <>
- ({dynKind} {head} + {region})
- >
+
+ {dynKind} {head} + {region}
+
);
};
@@ -243,20 +250,56 @@ export const PrintPolyFnSig = ({ o }: { o: PolyFnSig }) => {
);
return (
<>
- (
- {variadic}){ret}
+
+
+ {variadic}
+
+ {ret}
>
);
};
+ const PrintAbi = ({ abi }: { abi: Abi }) => {
+ if (abi === "Rust") {
+ return null;
+ }
+
+ const propertyAbis = [
+ "C",
+ "Cdecl",
+ "Stdcall",
+ "Fastcall",
+ "Vectorcall",
+ "Thiscall",
+ "Aapcs",
+ "Win64",
+ "SysV64",
+ "System",
+ ];
+
+ const fromString = (abi: string) => {
+ return `extern ${abi.toLowerCase()}`;
+ };
+
+ if (isObject(abi)) {
+ for (const prop in abi) {
+ if (propertyAbis.includes(prop)) {
+ return fromString(prop);
+ }
+ }
+ } else {
+ return fromString(abi);
+ }
+ };
+
const inner = (o: FnSig) => {
const unsafetyStr = o.unsafety === "Unsafe" ? "unsafe " : null;
- // TODO: we could write the ABI here, or expose it at least.
- const abi = o.abi === "Rust" ? null : "extern ";
+ const abi = ;
const [inputs, output] = fnInputsAndOutput(o.inputs_and_output);
return (
<>
- fn
+ {unsafetyStr} {abi} fn{" "}
+
>
);
};
@@ -270,9 +313,9 @@ export const PrintFnDef = ({ o }: { o: FnDef }) => {
return (
<>
} />{" "}
- {"{"}
-
- {"}"}
+
+
+
>
);
};
@@ -312,19 +355,28 @@ export const PrintPlaceholderTy = ({ o }: { o: PlaceholderBoundTy }) => {
};
export const PrintInferTy = ({ o }: { o: InferTy }) => {
- switch (o.type) {
- case "IntVar":
- return "{{int}}";
- case "FloatVar":
- return "{{float}}";
- case "Named":
- // NOTE: we also have access to the symbol it came from o.name
- return ;
- case "Unresolved":
- return "_";
- default:
- throw new Error("Unknown infer ty", o);
- }
+ const Inner =
+ o === "IntVar"
+ ? () => int
+ : o === "FloatVar"
+ ? () => float
+ : o === "Unresolved"
+ ? () => "_"
+ : "Named" in o
+ ? () =>
+ : "Unnamed" in o
+ ? () =>
+ : "SourceInfo" in o
+ ? () => {o.SourceInfo}
+ : () => {
+ throw new Error("Unknown infer ty", o);
+ };
+
+ return (
+
+
+
+ );
};
export const PrintTypeAndMut = ({ o }: { o: TypeAndMut }) => {
@@ -382,7 +434,11 @@ export const PrintIntTy = ({ o }: { o: IntTy }) => {
};
export const PrintBoundVariable = ({ o }: { o: BoundVariable }) => {
- throw new Error("TODO");
+ if ("Error" in o) {
+ return {o.Error};
+ } else {
+ throw new Error("Unknown bound variable", o);
+ }
};
export const PrintImplPolarity = ({ o }: { o: ImplPolarity }) => {
@@ -402,18 +458,22 @@ export const PrintOpaqueImplType = ({ o }: { o: OpaqueImpl }) => {
>
) : null;
return (
-
- ({o.kind}(){ret})
-
+
+ {o.kind}
+
+
+
+ {ret}
+
);
};
const PrintAssocItem = ({ o }: { o: AssocItem }) => {
console.debug("Printing AssocItem", o);
return (
-
+ <>
{o.name} =
-
+ >
);
};
diff --git a/ide/pnpm-lock.yaml b/ide/pnpm-lock.yaml
index 3ec52db..53bcef6 100644
--- a/ide/pnpm-lock.yaml
+++ b/ide/pnpm-lock.yaml
@@ -90,6 +90,9 @@ importers:
new-github-issue-url:
specifier: ^1.0.0
version: 1.0.0
+ open:
+ specifier: ^8.2.1
+ version: 8.2.1
react:
specifier: ^18.0.0
version: 18.0.0
@@ -1674,6 +1677,11 @@ packages:
resolution: {integrity: sha512-oIPzksmTg4/MriiaYGO+okXDT7ztn/w3Eptv/+gSIdMdKsJo0u4CfYNFJPy+4SKMuCqGw2wxnA+URMg3t8a/bQ==}
dev: true
+ /define-lazy-prop@2.0.0:
+ resolution: {integrity: sha512-Ds09qNh8yw3khSjiJjiUInaGX9xlqZDY7JVryGxdxV7NPeuqQfplOpQ66yJFZut3jLa5zOwkXw1g9EI2uKh4Og==}
+ engines: {node: '>=8'}
+ dev: true
+
/delaunator@5.0.0:
resolution: {integrity: sha512-AyLvtyJdbv/U1GkiS6gUUzclRoAY4Gs75qkMygJJhU75LW4DNuSF2RMzpxs9jw9Oz1BobHjTdkG3zdP55VxAqw==}
dependencies:
@@ -2178,6 +2186,12 @@ packages:
engines: {node: '>=12'}
dev: true
+ /is-docker@2.2.1:
+ resolution: {integrity: sha512-F+i2BKsFrH66iaUFc0woD8sLy8getkwTwtOBjvs56Cx4CgJDeKQeqfz8wAYiSb8JOprWhHH5p77PbmYCvvUuXQ==}
+ engines: {node: '>=8'}
+ hasBin: true
+ dev: true
+
/is-extglob@2.1.1:
resolution: {integrity: sha512-SbKbANkN603Vi4jEZv49LeVJMn4yGwsbzZworEoyEiutsN3nJYdbO36zfhGJ6QEDpOZIFkDtnq5JRxmvl3jsoQ==}
engines: {node: '>=0.10.0'}
@@ -2204,6 +2218,13 @@ packages:
resolution: {integrity: sha512-bCYeRA2rVibKZd+s2625gGnGF/t7DSqDs4dP7CrLA1m7jKWz6pps0LpYLJN8Q64HtmPKJ1hrN3nzPNKFEKOUiQ==}
dev: true
+ /is-wsl@2.2.0:
+ resolution: {integrity: sha512-fKzAra0rGJUUBwGBgNkHZuToZcn+TtXHpeCgmkMJMMYx1sQDYaCSyjJBSCa2nH1DGm7s3n1oBnohoVTBaN7Lww==}
+ engines: {node: '>=8'}
+ dependencies:
+ is-docker: 2.2.1
+ dev: true
+
/isarray@1.0.0:
resolution: {integrity: sha512-VLghIWNM6ELQzo7zwmcg0NmTVyWKYjvIeM83yjp0wRDTmUnrM678fQbcKBo6n2CJEF0szoG//ytg+TKla89ALQ==}
dev: true
@@ -2523,6 +2544,15 @@ packages:
wrappy: 1.0.2
dev: true
+ /open@8.2.1:
+ resolution: {integrity: sha512-rXILpcQlkF/QuFez2BJDf3GsqpjGKbkUUToAIGo9A0Q6ZkoSGogZJulrUdwRkrAsoQvoZsrjCYt8+zblOk7JQQ==}
+ engines: {node: '>=12'}
+ dependencies:
+ define-lazy-prop: 2.0.0
+ is-docker: 2.2.1
+ is-wsl: 2.2.0
+ dev: true
+
/optionator@0.9.3:
resolution: {integrity: sha512-JjCoypp+jKn1ttEFExxhetCKeJt9zhAgAve5FXHixTvFDW/5aEktX9bufBKLRRMdU7bNtpLfcGu94B3cdEJgjg==}
engines: {node: '>= 0.8.0'}