Support running discharge after monomorphization and before lowering.

crates/filament/src/ir_passes/bundle_elim.rs

@@ -3,9 +3,9 @@ use crate::{
     ir_visitor::{Action, Construct, Visitor, VisitorData},
 };
 use fil_ir::{
-    self as ir, Access, AddCtx, Bind, Command, Component, Connect, Ctx,
-    DenseIndexInfo, DisplayCtx, Expr, Foreign, Info, InvIdx, Invoke, Liveness,
-    MutCtx, Port, PortIdx, PortOwner, Range, SparseInfoMap, Subst, Time,
+    self as ir, Access, AddCtx, Bind, Component, Connect, Ctx, DenseIndexInfo,
+    DisplayCtx, Expr, Foreign, InvIdx, Invoke, Liveness, MutCtx, Port, PortIdx,
+    PortOwner, Range, SparseInfoMap, Subst, Time,
 };
 use fil_utils as utils;
 use itertools::Itertools;
@@ -147,12 +147,26 @@ impl BundleElim {
                 let info = comp.add(info.clone());
 
                 // adds the new port to the component and return its index
-                comp.add(Port {
+                let pidx = comp.add(Port {
                     live,
                     owner,
                     info, // duplicate the info
                     width,
-                })
+                });
+
+                // Fill in the live idxs with a new dummy index
+                let port = ir::Param {
+                    owner: ir::ParamOwner::bundle(pidx),
+                    info: comp.add(ir::Info::param(
+                        "_".into(),
+                        utils::GPosIdx::UNKNOWN,
+                    )),
+                };
+                let port = comp.add(port);
+
+                comp.get_mut(pidx).live.idxs.push(port);
+
+                pidx
             })
             .collect();
         // delete the original port
@@ -228,7 +242,7 @@ impl Visitor for BundleElim {
         connect: &mut Connect,
         data: &mut VisitorData,
     ) -> Action {
-        let Connect { src, dst, .. } = connect;
+        let Connect { src, dst, info } = connect;
 
         if !self.context.get(data.idx).contains(dst.port) {
             // we are writing to a local port here.
@@ -253,11 +267,12 @@ impl Visitor for BundleElim {
             src.into_iter()
                 .zip_eq(dst)
                 .map(|(src, dst)| {
-                    Command::Connect(Connect {
+                    Connect {
                         src: Access::port(src, &mut data.comp),
                         dst: Access::port(dst, &mut data.comp),
-                        info: data.comp.add(Info::empty()),
-                    })
+                        info: *info,
+                    }
+                    .into()
                 })
                 .collect(),
         )

crates/filament/src/ir_passes/discharge.rs

@@ -74,12 +74,12 @@ pub struct Discharge {
     /// Defined functions for `some` parameters on components
     comp_param_map: HashMap<ir::Foreign<ir::Param, ir::Component>, smt::SExpr>,
 
-    // Defined names
-    param_map: ir::DenseIndexInfo<ir::Param, smt::SExpr>,
-    ev_map: ir::DenseIndexInfo<ir::Event, smt::SExpr>,
+    // Defined names. These are sparse in case certain parameters or events have been invalidated.
+    param_map: ir::SparseInfoMap<ir::Param, smt::SExpr>,
+    ev_map: ir::SparseInfoMap<ir::Event, smt::SExpr>,
     // Composite expressions
-    expr_map: ir::DenseIndexInfo<ir::Expr, smt::SExpr>,
-    time_map: ir::DenseIndexInfo<ir::Time, smt::SExpr>,
+    expr_map: ir::SparseInfoMap<ir::Expr, smt::SExpr>,
+    time_map: ir::SparseInfoMap<ir::Time, smt::SExpr>,
     // Propositions
     prop_map: ir::DenseIndexInfo<ir::Prop, SExprWrapper>,
     // Propositions that have already been checked
@@ -609,7 +609,12 @@ impl Visitor for Discharge {
 
         let bs = self.sol.bool_sort();
         // Declare all expressions
-        for (idx, expr) in data.comp.exprs().iter() {
+        for (idx, expr) in data
+            .comp
+            .exprs()
+            .iter()
+            .filter(|(idx, _)| idx.valid(&data.comp))
+        {
             // do props inside of exprs ahead of time
             let relevant_props = idx
                 .relevant_props(&data.comp)
@@ -646,18 +651,31 @@ impl Visitor for Discharge {
         }
 
         // Declare all time expressions
-        for (idx, ir::Time { event, offset }) in data.comp.times().iter() {
-            let assign = self.plus(self.ev_map[*event], self.expr_map[*offset]);
-            let sexp = self
-                .sol
-                .define_const(Self::fmt_time(idx), int, assign)
-                .unwrap();
-            self.overflow_assert(sexp);
-            self.time_map.push(idx, sexp);
+        for (idx, ir::Time { event, offset }) in data
+            .comp
+            .times()
+            .iter()
+            .filter(|(idx, _)| idx.valid(&data.comp))
+        {
+            if self.ev_map.contains(*event) && self.expr_map.contains(*offset) {
+                let assign =
+                    self.plus(self.ev_map[*event], self.expr_map[*offset]);
+                let sexp = self
+                    .sol
+                    .define_const(Self::fmt_time(idx), int, assign)
+                    .unwrap();
+                self.overflow_assert(sexp);
+                self.time_map.push(idx, sexp);
+            }
         }
 
         // Declare all propositions
-        for (idx, prop) in data.comp.props().iter() {
+        for (idx, prop) in data
+            .comp
+            .props()
+            .iter()
+            .filter(|(idx, _)| idx.valid(&data.comp))
+        {
             // Define assertion equating the proposition to its assignment
             let assign = self.prop_to_sexp(prop);
             if let Ok(sexp) =

crates/filament/src/main.rs

@@ -97,6 +97,17 @@ fn run(opts: &cmdline::Opts) -> Result<(), u64> {
         ip::BundleElim,
         ip::AssignCheck
     }
+    // type check again before lowering
+    ir_pass_pipeline! {opts, ir;
+        ip::BuildDomination,
+        ip::TypeCheck,
+        ip::IntervalCheck,
+        ip::PhantomCheck,
+        ip::Assume
+    }
+    if !opts.unsafe_skip_discharge {
+        ir_pass_pipeline! {opts, ir; ip::Discharge }
+    }
 
     // Return early if we're asked to dump the interface
     if opts.dump_interface {

crates/ir/src/expr.rs

@@ -1,5 +1,5 @@
-use super::{AddCtx, Component, Ctx, ExprIdx, ParamIdx};
-use crate::{construct_binop, Prop, PropIdx};
+use super::{AddCtx, Component, Ctx, ExprIdx, MutCtx, ParamIdx};
+use crate::{construct_binop, Param, Prop, PropIdx};
 use fil_ast as ast;
 use std::fmt::Display;
 
@@ -112,6 +112,13 @@ impl ExprIdx {
 
 /// Queries over [ExprIdx]
 impl ExprIdx {
+    pub fn valid(
+        &self,
+        ctx: &(impl Ctx<Expr> + Ctx<Prop> + MutCtx<Param>),
+    ) -> bool {
+        self.relevant_vars(ctx).iter().all(|p| ctx.valid(*p))
+    }
+
     pub fn relevant_props(
         &self,
         ctx: &(impl Ctx<Expr> + Ctx<Prop>),

crates/ir/src/fact.rs

@@ -1,5 +1,7 @@
-use super::{idxs::PropIdx, AddCtx, Ctx, ExprIdx, InfoIdx, TimeIdx, TimeSub};
-use crate::{construct_binop, EventIdx, Expr, ParamIdx, Time};
+use super::{
+    idxs::PropIdx, AddCtx, Ctx, ExprIdx, InfoIdx, MutCtx, TimeIdx, TimeSub,
+};
+use crate::{construct_binop, Event, EventIdx, Expr, Param, ParamIdx, Time};
 use std::fmt::{self, Display};
 
 #[derive(Clone, PartialEq, Eq, Hash)]
@@ -357,6 +359,19 @@ impl PropIdx {
             }
         }
     }
+
+    pub fn valid(
+        &self,
+        ctx: &(impl Ctx<Prop>
+              + Ctx<Time>
+              + Ctx<Expr>
+              + MutCtx<Param>
+              + MutCtx<Event>),
+    ) -> bool {
+        let (props, events) = self.relevant_vars(ctx);
+        props.iter().all(|p| ctx.valid(*p))
+            && events.iter().all(|e| ctx.valid(*e))
+    }
 }
 
 #[derive(Clone, PartialEq, Eq)]

crates/ir/src/time.rs

@@ -1,4 +1,4 @@
-use crate::{DisplayCtx, Prop};
+use crate::{DisplayCtx, MutCtx, Param, Prop};
 
 use super::{
     AddCtx, Component, Ctx, EventIdx, Expr, ExprIdx, Foldable, ParamIdx,
@@ -61,6 +61,14 @@ impl TimeIdx {
         let time = ctx.get(self);
         time.offset.relevant_vars(ctx)
     }
+
+    pub fn valid(
+        &self,
+        ctx: &(impl Ctx<Time> + Ctx<Expr> + Ctx<Prop> + MutCtx<Param>),
+    ) -> bool {
+        let time = ctx.get(*self);
+        time.offset.valid(ctx)
+    }
 }
 
 #[derive(PartialEq, Eq, Hash, Clone)]