Function arbitrary_expr

crates/ixon/src/expr.rs:172–297

Generate an arbitrary Expr using pointer-tree technique (no stack overflow)

(g: &mut Gen)

  }

  /// Count nested applications for telescope compression.
  pub fn app_telescope_count(&self) -> u64 {
    let mut count = 0u64;
    let mut curr = self;
    while let Expr::App(f, _) = curr {
      count += 1;
      curr = f.as_ref();
    }
    count
  }

  /// Count nested lambdas for telescope compression.
  pub fn lam_telescope_count(&self) -> u64 {
    let mut count = 0u64;
    let mut curr = self;
    while let Expr::Lam(_, _, body) = curr {
      count += 1;
      curr = body.as_ref();
    }
    count
  }

  /// Count nested foralls for telescope compression.
  pub fn all_telescope_count(&self) -> u64 {
    let mut count = 0u64;
    let mut curr = self;
    while let Expr::All(_, _, _, body) = curr {
      count += 1;
      curr = body.as_ref();
    }
    count
  }
}

#[cfg(test)]
pub mod tests {
  use super::*;
  use crate::constant::Constant;
  use crate::serialize::{get_expr, put_expr};
  use crate::tests::gen_range;
  use quickcheck::{Arbitrary, Gen};
  use quickcheck_macros::quickcheck;
  use std::ptr;

  #[derive(Clone, Copy)]
  enum Case {
    Var,
    Share,
    Str,
    Nat,
    Sort,
    Ref,
    Rec,
    App,
    Lam,
    All,
    Prj,
    Let,