vscode extension, predicates, other changes

components/dada-check/src/lib.rs

@@ -5,12 +5,15 @@ use dada_ir_ast::{
     span::Spanned,
 };
 use dada_ir_sym::{
-    ir::binder::{Binder, BoundTerm},
-    ir::classes::{SymAggregate, SymClassMember, SymField},
-    ir::functions::{SignatureSymbols, SymFunction, SymFunctionSignature, SymInputOutput},
-    ir::module::{SymItem, SymModule},
-    ir::types::{SymGenericKind, SymTy},
-    ir::variables::SymVariable,
+    ir::{
+        binder::{Binder, BoundTerm},
+        classes::{SymAggregate, SymClassMember, SymField},
+        functions::{SignatureSymbols, SymFunction, SymFunctionSignature, SymInputOutput},
+        generics::{SymWhereClause, SymWhereClauseKind},
+        module::{SymItem, SymModule},
+        types::{SymGenericKind, SymGenericTerm, SymPerm, SymPlace, SymTy},
+        variables::SymVariable,
+    },
     prelude::*,
 };
 
@@ -141,9 +144,11 @@ impl<'db> Check<'db> for SymInputOutput<'db> {
         let SymInputOutput {
             input_tys,
             output_ty,
+            where_clauses,
         } = self;
         input_tys.check(db);
         output_ty.check(db);
+        where_clauses.check(db);
     }
 }
 
@@ -183,3 +188,48 @@ impl<'db> Check<'db> for SymVariable<'db> {
         // the type appears.
     }
 }
+
+impl<'db> Check<'db> for SymWhereClause<'db> {
+    fn check(&self, db: &'db dyn crate::Db) {
+        self.subject(db).check(db);
+        self.kind(db).check(db);
+    }
+}
+
+impl<'db> Check<'db> for SymWhereClauseKind {
+    fn check(&self, _db: &'db dyn crate::Db) {
+        match self {
+            SymWhereClauseKind::Unique => (),
+            SymWhereClauseKind::Shared => (),
+            SymWhereClauseKind::Owned => (),
+            SymWhereClauseKind::Lent => (),
+        }
+    }
+}
+
+impl<'db> Check<'db> for SymGenericTerm<'db> {
+    fn check(&self, db: &'db dyn crate::Db) {
+        match self {
+            SymGenericTerm::Type(sym_ty) => sym_ty.check(db),
+            SymGenericTerm::Perm(sym_perm) => sym_perm.check(db),
+            SymGenericTerm::Place(sym_place) => sym_place.check(db),
+            SymGenericTerm::Error(_) => (),
+        }
+    }
+}
+
+impl<'db> Check<'db> for SymPerm<'db> {
+    fn check(&self, _db: &'db dyn crate::Db) {
+        // There *are* validity checks that need to be done on permissions,
+        // but they are done as part of the checking the item in which
+        // the permission appears.
+    }
+}
+
+impl<'db> Check<'db> for SymPlace<'db> {
+    fn check(&self, _db: &'db dyn crate::Db) {
+        // There *are* validity checks that need to be done on places,
+        // but they are done as part of the checking the item in which
+        // the place appears.
+    }
+}

components/dada-codegen/src/cx/generate_fn.rs

@@ -37,6 +37,7 @@ impl<'db> Cx<'db> {
                 SymInputOutput {
                     input_tys,
                     output_ty,
+                    where_clauses: _,
                 },
         } = self.codegen_signature(function, generics);
 
@@ -132,6 +133,7 @@ impl<'db> Cx<'db> {
                 input_output: SymInputOutput {
                     input_tys: vec![],
                     output_ty: SymTy::err(self.db, reported),
+                    where_clauses: vec![],
                 },
             },
         }

components/dada-compiler/src/lib.rs

@@ -169,6 +169,11 @@ impl Compiler {
         self.attach(|db| dada_probe::probe_variable_type(db, span))
     }
 
+    /// Return type of the variable found at the given `span` or `None` if there is no variable there.
+    pub fn probe_expression_type(&self, span: AbsoluteSpan) -> Option<String> {
+        self.attach(|db| dada_probe::probe_expression_type(db, span))
+    }
+
     fn deduplicated(mut diagnostics: Vec<&Diagnostic>) -> Vec<&Diagnostic> {
         let mut new = Set::default();
         diagnostics.retain(|&d| new.insert(d));

components/dada-debug/src/root.rs

@@ -23,8 +23,14 @@ pub struct RootEvent {
 #[derive(Serialize)]
 #[serde(tag = "type")]
 enum RootEventPayload {
-    Diagnostic { message: String },
-    CheckLog { index: usize },
+    Diagnostic {
+        message: String,
+    },
+    CheckLog {
+        index: usize,
+        root_event_info: Option<serde_json::Value>,
+        total_events: Option<usize>,
+    },
 }
 
 // basic handler that responds with a static string
@@ -45,7 +51,20 @@ fn root_events(events: &[Arc<DebugEvent>]) -> anyhow::Result<Vec<RootEvent>> {
             DebugEventPayload::Diagnostic(diagnostic) => RootEventPayload::Diagnostic {
                 message: diagnostic.message.clone(),
             },
-            DebugEventPayload::CheckLog(_) => RootEventPayload::CheckLog { index },
+            DebugEventPayload::CheckLog(log_value) => {
+                // Extract root_event_info and total_events from the log_value
+                let root_event_info = log_value.get("root_event_info").cloned();
+                let total_events = log_value
+                    .get("total_events")
+                    .and_then(|v| v.as_u64())
+                    .map(|v| v as usize);
+
+                RootEventPayload::CheckLog {
+                    index,
+                    root_event_info,
+                    total_events,
+                }
+            }
         };
         let (text, line_start, col_start, line_end, col_end) =
             extract_span(&event.url, event.start, event.end)?;

components/dada-debug/src/server.rs

@@ -1,5 +1,8 @@
 use std::{
-    sync::{Arc, Mutex, mpsc::Receiver},
+    sync::{
+        Arc, Mutex,
+        mpsc::{Receiver, RecvTimeoutError},
+    },
     time::Duration,
 };
 
@@ -134,8 +137,12 @@ pub struct State {
 
 fn record_events(debug_rx: Receiver<DebugEvent>, state: Arc<State>) {
     while !*state.shutdown.lock().unwrap() {
-        if let Ok(event) = debug_rx.recv_timeout(Duration::from_secs(1)) {
-            state.debug_events.lock().unwrap().push(Arc::new(event));
+        match debug_rx.recv_timeout(Duration::from_secs(1)) {
+            Ok(event) => {
+                state.debug_events.lock().unwrap().push(Arc::new(event));
+            }
+            Err(RecvTimeoutError::Disconnected) => return,
+            Err(RecvTimeoutError::Timeout) => (),
         }
     }
 }

components/dada-debug/templates/index.hbs

@@ -2,6 +2,17 @@
 <html lang="en">
 <head>
 {{> header title="Dada Debug Log"}}
+<style>
+    .root-event-info, .event-count {
+        margin: 5px 0;
+        font-size: 14px;
+        color: #333;
+    }
+
+    .root-event-info strong, .event-count strong {
+        color: #007bff;
+    }
+</style>
 </head>
 <body>
 <h1>Dada Debug Log</h1>
@@ -12,6 +23,16 @@
         <a href="/view/{{payload.index}}">
             Type check log from {{url}}:{{line_start}}:{{col_start}}:{{line_end}}:{{col_end}}<br>
             <code>{{text}}</code>
+            {{#if payload.root_event_info}}
+            <div class="root-event-info">
+                <strong>Root Event:</strong> {{payload.root_event_info.description}}
+            </div>
+            {{/if}}
+            {{#if payload.total_events}}
+            <div class="event-count">
+                <strong>Total Events:</strong> {{payload.total_events}}
+            </div>
+            {{/if}}
         </a>
     </li>
 {{else if (is_type payload.type "Diagnostic")}}

components/dada-debug/templates/log.hbs

@@ -43,10 +43,33 @@
             color: #666;
             margin-left: 10px;
         }
+
+        .root-info {
+            background-color: #f5f5f5;
+            padding: 15px;
+            border-radius: 5px;
+            margin-bottom: 20px;
+            border-left: 4px solid #007bff;
+        }
+
+        .root-event-info, .event-count {
+            margin: 10px 0;
+            font-size: 14px;
+        }
     </style>
 </head>
 
 <body>
+    <div class="root-info">
+        <h2>Root Event Information</h2>
+        <div class="root-event-info">
+            <strong>Root Event Description:</strong> <span class="jsontree">{{root_event_info.description}}</span>
+        </div>
+        <div class="event-count">
+            <strong>Total Events:</strong> {{total_events}}
+        </div>
+    </div>
+
     <h1>Nested</h1>
 
     <div id="tasks">
@@ -139,4 +162,4 @@
 
 </body>
 
-</html>
+</html>

components/dada-ir-ast/src/ast/class_item.rs

@@ -6,7 +6,7 @@ use crate::{
     span::{Span, Spanned},
 };
 
-use super::{AstGenericDecl, Identifier, SpanVec};
+use super::{AstGenericDecl, AstWhereClauses, Identifier, SpanVec};
 
 /// Some kind of aggregate, like a class, struct, etc.
 ///
@@ -32,6 +32,9 @@ pub struct AstAggregate<'db> {
     #[return_ref]
     pub inputs: Option<SpanVec<'db, AstFieldDecl<'db>>>,
 
+    #[return_ref]
+    pub where_clauses: Option<AstWhereClauses<'db>>,
+
     /// The unparsed contents of the class.
     /// This can be parsed via the `members`
     /// method defined in `dada_parser::prelude`.

components/dada-ir-ast/src/ast/expr.rs

@@ -23,6 +23,7 @@ pub enum AstStatement<'db> {
 #[derive(SalsaSerialize)]
 #[salsa::tracked(debug)]
 pub struct AstLetStatement<'db> {
+    pub span: Span<'db>,
     pub mutable: Option<Span<'db>>,
     pub name: SpannedIdentifier<'db>,
     pub ty: Option<AstTy<'db>>,

components/dada-ir-ast/src/ast/function.rs

@@ -4,7 +4,7 @@ use serde::Serialize;
 
 use super::{AstGenericDecl, AstPerm, AstTy, SpanVec, SpannedIdentifier};
 use crate::{
-    ast::{AstVisibility, DeferredParse},
+    ast::{AstVisibility, AstWhereClauses, DeferredParse},
     span::{Span, Spanned},
 };
 
@@ -38,6 +38,10 @@ pub struct AstFunction<'db> {
     /// Return type of the function (if provided)
     pub output_ty: Option<AstTy<'db>>,
 
+    /// Where clauses (if any)
+    #[return_ref]
+    pub where_clauses: Option<AstWhereClauses<'db>>,
+
     /// Body (if provided)
     #[return_ref]
     pub body: Option<DeferredParse<'db>>,

components/dada-ir-ast/src/ast/types.rs

@@ -127,3 +127,46 @@ impl<'db> Spanned<'db> for AstGenericDecl<'db> {
         }
     }
 }
+
+/// Looks like `where WC1, ... WC2,`
+#[derive(SalsaSerialize)]
+#[salsa::tracked(debug)]
+pub struct AstWhereClauses<'db> {
+    /// Span of the where-clause keyword.
+    pub where_span: Span<'db>,
+
+    /// List of clauses that came after the keyword.
+    #[return_ref]
+    pub clauses: SpanVec<'db, AstWhereClause<'db>>,
+}
+
+/// A where-clause looks like `A is shared`, `A is lent`, `A is shared + lent`, etc.
+#[derive(SalsaSerialize)]
+#[salsa::tracked(debug)]
+pub struct AstWhereClause<'db> {
+    pub subject: AstGenericTerm<'db>,
+
+    #[return_ref]
+    pub kinds: SpanVec<'db, AstWhereClauseKind<'db>>,
+}
+
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Update, Debug, Serialize)]
+pub enum AstWhereClauseKind<'db> {
+    /// `ref`
+    Reference(Span<'db>),
+
+    /// `mut`
+    Mutable(Span<'db>),
+
+    /// `shared`
+    Shared(Span<'db>),
+
+    /// `unique`
+    Unique(Span<'db>),
+
+    /// `owned`
+    Owned(Span<'db>),
+
+    /// `lent`
+    Lent(Span<'db>),
+}

components/dada-ir-sym/src/check.rs

@@ -12,6 +12,7 @@ mod env;
 mod exprs;
 pub(crate) mod fields;
 pub(crate) mod functions;
+mod generics;
 mod inference;
 mod live_places;
 mod member_lookup;