Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Experiments: numeric model 'analytic-engine' #228

Open
wants to merge 20 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
276d1f8
Experiments; numeric model 'analytic-engine'
archaephyrryx Oct 28, 2024
075ffb1
Add proptest tests (and dependency) to analytic-engine
archaephyrryx Oct 29, 2024
a593690
Add elaboration module for analytic-engine
archaephyrryx Oct 30, 2024
7bac2a0
Finish inference engine, elaborator, add printer
archaephyrryx Oct 31, 2024
f3afd74
Add parser crate with REPL for analytic-engine
archaephyrryx Nov 4, 2024
611e8d0
Fix bugs in show_typed_unary_op
archaephyrryx Nov 4, 2024
2d0a22a
Add precedence and fragment-based printing
archaephyrryx Nov 4, 2024
88b1df6
Add intervening space between unary op and arg
archaephyrryx Nov 4, 2024
065c7a0
Add spaces around raw binop in printing
archaephyrryx Nov 4, 2024
6c7253b
Add eval model for concrete machine-int functions
archaephyrryx Nov 6, 2024
c2af9fe
Refine eval model
archaephyrryx Nov 6, 2024
f6bd699
Expand set of predefined machine-int mixed-type operations
archaephyrryx Nov 6, 2024
e4131b6
Retool op-definition macros, implement 480 common fns
archaephyrryx Nov 7, 2024
3914e63
Remove unused imports of std::ops from eval
archaephyrryx Nov 7, 2024
3613edc
Prototype code-generation simulacrum
archaephyrryx Nov 7, 2024
d14087f
Define first-class unary and cast backend fns
archaephyrryx Nov 8, 2024
e621b32
Add Display for Ops, streamline Expr Debug impl
archaephyrryx Nov 8, 2024
017e691
Refactor NumRep to eliminate Auto from casts
archaephyrryx Nov 8, 2024
3333a8c
Fix expr grammar in parser based on NumRep refactor
archaephyrryx Nov 8, 2024
3da5f3a
Simplify operations in elaborator using MachineRep
archaephyrryx Nov 8, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Finish inference engine, elaborator, add printer
archaephyrryx committed Oct 31, 2024
commit 7bac2a0a32428d024d7bd81b0aaded6d15ab8306
123 changes: 76 additions & 47 deletions experiments/analytic-engine/src/core.rs
Original file line number Diff line number Diff line change
@@ -22,15 +22,29 @@ pub enum BasicUnaryOp {

#[derive(Clone, Copy, PartialEq, PartialOrd, Eq, Ord, Debug, Hash)]
pub enum NumRep {
Abstract {
auto: bool,
},
Auto,
Concrete {
is_signed: bool,
bit_width: BitWidth,
},
}

impl std::fmt::Display for NumRep {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match *self {
NumRep::U8 => write!(f, "u8",),
NumRep::U16 => write!(f, "u16"),
NumRep::U32 => write!(f, "u32"),
NumRep::U64 => write!(f, "u64"),
NumRep::I8 => write!(f, "i8"),
NumRep::I16 => write!(f, "i16"),
NumRep::I32 => write!(f, "i32"),
NumRep::I64 => write!(f, "i64"),
NumRep::AUTO => write!(f, "?"),
}
}
}

impl NumRep {
pub const I8: NumRep = NumRep::Concrete {
is_signed: true,
@@ -66,15 +80,10 @@ impl NumRep {
bit_width: BitWidth::Bits64,
};

pub const AUTO: NumRep = NumRep::Abstract { auto: true };
pub const AMBIGUOUS: NumRep = NumRep::Abstract { auto: false };
pub const AUTO: NumRep = NumRep::Auto;
}

impl NumRep {
pub const fn is_abstract(&self) -> bool {
matches!(self, NumRep::Abstract { .. })
}
}



/// Representative min and max bounds for a numeric type
@@ -91,6 +100,14 @@ impl std::fmt::Display for Bounds {
}

impl Bounds {
pub fn new(min: Number, max: Number) -> Self {
Self { min, max }
}

pub fn singleton(n: Number) -> Self {
Self { min: n.clone(), max: n }
}

/// Returns `true` if every value in `sub_range` is also within `self`.
///
/// If `inferior` has inverted bounds, will panic.
@@ -132,7 +149,7 @@ macro_rules! bounds_of {
impl NumRep {
pub(crate) fn as_bounds(&self) -> Option<Bounds> {
let (min, max) = match self {
NumRep::Abstract { .. } => return None,
NumRep::Auto => return None,
&NumRep::U8 => bounds_of!(u8),
&NumRep::U16 => bounds_of!(u16),
&NumRep::U32 => bounds_of!(u32),
@@ -145,8 +162,8 @@ impl NumRep {
Some(Bounds { min, max })
}

pub const fn is_auto(&self) -> bool {
matches!(self, NumRep::Abstract { auto: true })
pub const fn is_auto(self) -> bool {
matches!(self, NumRep::Auto)
}
}

@@ -159,7 +176,7 @@ pub enum BitWidth {
}

#[derive(Clone, PartialEq, Debug)]
pub struct TypedConst(BigInt, NumRep);
pub struct TypedConst(pub BigInt, pub NumRep);

impl std::fmt::Display for TypedConst {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
@@ -174,15 +191,14 @@ impl std::fmt::Display for TypedConst {
NumRep::I32 => write!(f, "{}i32", n),
NumRep::I64 => write!(f, "{}i64", n),
NumRep::AUTO => write!(f, "{}?", n),
NumRep::AMBIGUOUS => write!(f, "{}??", n),
}
}
}

impl TypedConst {
/// Returns `true` if the stored `NumRep` is abstract (either auto or ambiguous).
pub fn is_abstract(&self) -> bool {
self.1.is_abstract()
pub fn is_abstract(self) -> bool {
self.1.is_auto()
}

/// Returns `true` if `self` is representable, which is true if either:
@@ -193,7 +209,7 @@ impl TypedConst {
if let Some(bounds) = rep.as_bounds() {
n >= &bounds.min && n <= &bounds.max
} else {
debug_assert!(rep.is_abstract());
debug_assert!(rep.is_auto());
true
}
}
@@ -262,23 +278,35 @@ impl std::fmt::Display for Value {

#[derive(Clone, Copy, Debug)]
pub struct BinOp {
op: BasicBinOp,
pub op: BasicBinOp,
// If None: op(T, T | auto) -> T, op(T0, T1) { T0 != T1 } -> ambiguous; otherwise, forces rep for `Some(rep)``
out_rep: Option<NumRep>,
pub out_rep: Option<NumRep>,
}

impl BinOp {
pub fn output_type(&self, left: NumRep, right: NumRep) -> NumRep {
pub fn output_type(&self, left: NumRep, right: NumRep) -> Option<NumRep> {
if let Some(rep) = self.out_rep {
rep
Some(rep)
} else if left == right || right.is_auto() {
left
Some(left)
} else if left.is_auto() {
right
Some(right)
} else {
NumRep::AMBIGUOUS
None
}
}

pub fn cast_rep(&self) -> Option<NumRep> {
self.out_rep
}

pub fn is_cast_and(&self, predicate: impl Fn(NumRep) -> bool) -> bool {
self.out_rep.is_some_and(predicate)
}

pub(crate) fn get_op(&self) -> BasicBinOp {
self.op
}
}

#[derive(Clone, Copy, Debug)]
@@ -289,12 +317,24 @@ pub struct UnaryOp {
}
impl UnaryOp {
fn output_type(&self, in_rep: NumRep) -> NumRep {
if let Some(rep) = self.out_rep {
if let Some(rep) = self.out_rep {
rep
} else {
in_rep
}
}

pub fn cast_rep(&self) -> Option<NumRep> {
self.out_rep
}

pub fn is_cast_and(&self, predicate: fn(NumRep) -> bool) -> bool {
self.out_rep.is_some_and(predicate)
}

pub(crate) fn get_op(&self) -> BasicUnaryOp {
self.op
}
}

#[derive(Clone, Debug)]
@@ -307,15 +347,15 @@ pub enum Expr {
}

impl Expr {
pub(crate) fn get_rep(&self) -> NumRep {
pub(crate) fn get_rep(&self) -> Option<NumRep> {
match self {
Expr::Const(tc) => tc.get_rep(),
Expr::Cast(rep, _) => *rep,
Expr::Const(tc) => Some(tc.get_rep()),
Expr::Cast(rep, _) => Some(*rep),
Expr::BinOp(bin_op, expr, expr1) => {
bin_op.output_type(expr.get_rep(), expr1.get_rep())
bin_op.output_type(expr.get_rep()?, expr1.get_rep()?)
}
Expr::UnaryOp(unary_op, expr) => {
unary_op.output_type(expr.get_rep())
Some(unary_op.output_type(expr.get_rep()?))
}
}
}
@@ -325,28 +365,17 @@ impl Expr {
pub enum EvalError {
DivideByZero,
RemainderNonPositive,
Unrepresentable(Value),
ArithOrCastOption,
// TryUnwrapNone,
// TryUnwrapConst,
Ambiguous(NumRep, NumRep),
}

impl std::fmt::Display for EvalError {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
EvalError::DivideByZero => write!(f, "attempted division by zero"),
EvalError::RemainderNonPositive => write!(f, "remainder rhs must be positive"),
EvalError::Unrepresentable(value) => write!(f, "value `{value}` is unrepresentable"),
EvalError::ArithOrCastOption => {
write!(f, "arithmetic and casts on Value::Opt not supported")
EvalError::Ambiguous(rep0, rep1) => {
write!(f, "operation over {rep0} and {rep1} must have an explicit output representation to be evaluated")
}
// EvalError::TryUnwrapNone => {
// write!(f, "TryUnwrap called over expr evaluating to Opt(None)")
// }
// EvalError::TryUnwrapConst => write!(
// f,
// "TryUnwrap called over expr evaluating to Const (and not Opt)"
// ),
}
}
}
@@ -396,7 +425,7 @@ impl Expr {
} else if rep0.is_auto() {
rep1
} else {
NumRep::AMBIGUOUS
return Err(EvalError::Ambiguous(rep0, rep1))
}
}
};
@@ -446,7 +475,7 @@ mod tests {
use proptest::prelude::*;

fn abstract_strategy() -> BoxedStrategy<NumRep> {
prop_oneof![Just(NumRep::AUTO), Just(NumRep::AMBIGUOUS)].boxed()
prop_oneof![Just(NumRep::AUTO)].boxed()
}

fn concrete_strategy() -> BoxedStrategy<NumRep> {
409 changes: 385 additions & 24 deletions experiments/analytic-engine/src/elaborator.rs
Original file line number Diff line number Diff line change
@@ -14,6 +14,35 @@ pub(crate) enum PrimInt {

pub const PRIM_INTS: [PrimInt; 8] = [PrimInt::U8, PrimInt::U16, PrimInt::U32, PrimInt::U64, PrimInt::I8, PrimInt::I16, PrimInt::I32, PrimInt::I64];

#[derive(Debug)]
pub struct TryFromAutoError;

impl std::fmt::Display for TryFromAutoError {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "cannot convert `NumRep::AUTO` to `PrimInt`")
}
}

impl std::error::Error for TryFromAutoError {}

impl TryFrom<NumRep> for PrimInt {
type Error = TryFromAutoError;

fn try_from(value: NumRep) -> Result<Self, Self::Error> {
match value {
NumRep::Auto => Err(TryFromAutoError),
NumRep::U8 => Ok(PrimInt::U8),
NumRep::U16 => Ok(PrimInt::U16),
NumRep::U32 => Ok(PrimInt::U32),
NumRep::U64 => Ok(PrimInt::U64),
NumRep::I8 => Ok(PrimInt::I8),
NumRep::I16 => Ok(PrimInt::I16),
NumRep::I32 => Ok(PrimInt::I32),
NumRep::I64 => Ok(PrimInt::I64),
}
}
}

impl From<PrimInt> for NumRep {
fn from(value: PrimInt) -> Self {
match value {
@@ -52,25 +81,37 @@ pub(crate) enum TypedExpr<TypeRep> {
ElabCast(TypeRep, NumRep, Box<TypedExpr<TypeRep>>),
}

impl<T> TypedExpr<T> {
pub fn get_type(&self) -> &T {
match self {
TypedExpr::ElabConst(t, _) => t,
TypedExpr::ElabBinOp(t, _, _, _) => t,
TypedExpr::ElabUnaryOp(t, _, _) => t,
TypedExpr::ElabCast(t, _, _) => t,
}
}

}

type Sig1<T> = (T, T);
type Sig2<T> = ((T, T), T);

#[derive(Clone, Debug)]
struct TypedBinOp<TypeRep> {
sig: Sig2<TypeRep>,
inner: BinOp,
pub(crate) struct TypedBinOp<TypeRep> {
pub(crate) sig: Sig2<TypeRep>,
pub(crate) inner: BinOp,
}

#[derive(Clone, Debug)]
struct TypedUnaryOp<TypeRep> {
sig: Sig1<TypeRep>,
inner: UnaryOp,
pub(crate) struct TypedUnaryOp<TypeRep> {
pub(crate) sig: Sig1<TypeRep>,
pub(crate) inner: UnaryOp,
}

pub(crate) mod inference {
use std::collections::HashSet;

use crate::core::{BitWidth, Bounds, Expr, NumRep, TypedConst};
use crate::core::{Bounds, Expr, NumRep, TypedConst};

use super::{IntType, PrimInt};

@@ -112,6 +153,13 @@ pub(crate) mod inference {
}
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) enum VType {
Int(IntType),
Within(Bounds),
Abstract(UType),
}

#[derive(Clone, Debug, Default)]
enum Alias {
#[default]
@@ -190,6 +238,7 @@ pub(crate) mod inference {
Encompasses(crate::core::Bounds),
}


impl std::fmt::Display for Constraint {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
@@ -225,6 +274,7 @@ pub(crate) mod inference {
}

pub(crate) fn has_unique_assignment(&self) -> bool {
// REVIEW - there are smarter ways of calculating this
let mut solutions = 0;
for prim_int in super::PRIM_INTS.iter() {
match self.is_satisfied_by(IntType::Prim(*prim_int)) {
@@ -237,6 +287,26 @@ pub(crate) mod inference {
}
solutions == 1
}

// NOTE - should only be called on Encompasses
pub(crate) fn get_unique_solution(&self) -> InferenceResult<IntType> {
// REVIEW - there are smarter ways of calculating this
let mut solutions = Vec::with_capacity(8);
for prim_int in super::PRIM_INTS.iter() {
match self.is_satisfied_by(IntType::Prim(*prim_int)) {
Some(true) => {
solutions.push(*prim_int);
}
Some(false) => (),
None => panic!("unexpected call to get_unique_solution on `{self}` (either trivial or insoluble)"),
}
}
match solutions.as_slice() {
[] => Err(InferenceError::NoSolution),
[uniq] => Ok(IntType::Prim(*uniq)),
_ => Err(InferenceError::MultipleSolutions),
}
}
}


@@ -247,21 +317,38 @@ pub(crate) mod inference {
}

#[derive(Debug)]
enum InferenceError {
pub enum InferenceError {
Unrepresentable(TypedConst, IntType),
BadUnification(Constraint, Constraint),
AbstractCast,
Ambiguous,
NoSolution,
MultipleSolutions,
Eval(crate::core::EvalError),
}

impl std::fmt::Display for InferenceError {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
InferenceError::Unrepresentable(c, int_type) => write!(f, "inference requires that `{}` be assigned type `{}`, which cannot represent it", c, int_type),
InferenceError::BadUnification(cx1, cx2) => write!(f, "constraints `{}` and `{}` cannot be unified", cx1, cx2),
InferenceError::AbstractCast => write!(f, "casts and operations cannot explicitly produce abstract NumReps"),
InferenceError::Ambiguous => write!(f, "mixed-type binary operation must have out_rep on operation to avoid ambiguity"),
InferenceError::Eval(e) => write!(f, "inference abandoned due to evaluation error: {}", e),
InferenceError::NoSolution => write!(f, "no valid assignment of PrimInt types produce a fully representable tree"),
InferenceError::MultipleSolutions => write!(f, "multiple assignments of PrimInt produce a fully representable tree, in absence of tie-breaking mechanism"),
}
}
}

impl std::error::Error for InferenceError {}
impl std::error::Error for InferenceError {
fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
match self {
InferenceError::Eval(e) => Some(e),
_ => None,
}
}
}

pub type InferenceResult<T> = Result<T, InferenceError>;

@@ -594,6 +681,20 @@ pub(crate) mod inference {
}
}

fn unify_var_utype(&mut self, uvar: UVar, utype: UType) -> InferenceResult<()> {
let _ = self.unify_var_constraint(uvar, Constraint::Equiv(utype))?;
Ok(())
}


fn unify_var_rep(&mut self, uvar: UVar, rep: NumRep) -> InferenceResult<()> {
if rep.is_auto() {
return Ok(());
}
let t = UType::Int(IntType::Prim(PrimInt::try_from(rep).unwrap()));
self.unify_var_utype(uvar, t)
}

fn unify_constraint_pair(&mut self, c1: Constraint, c2: Constraint) -> InferenceResult<Constraint> {
match (c1, c2) {
(Constraint::Equiv(t1), Constraint::Equiv(t2)) => {
@@ -617,11 +718,16 @@ pub(crate) mod inference {
}

impl InferenceEngine {
fn infer_var_expr(&mut self, e: &Expr) -> InferenceResult<UVar> {
let topvar = match e {
pub(crate) fn infer_var_expr(&mut self, e: &Expr) -> InferenceResult<(UVar, NumRep)> {
let (top_var, top_rep) = match e {
Expr::Const(typed_const) => {
match typed_const.get_rep() {
NumRep::Abstract { .. } => self.get_new_uvar(),
let rep = typed_const.get_rep();
let var = match rep {
NumRep::AUTO => {
let this_var = self.get_new_uvar();
self.unify_var_constraint(this_var, Constraint::Encompasses(Bounds::singleton(typed_const.as_raw_value().clone())))?;
this_var
}
NumRep::U8 => self.init_var_simple(UType::Int(IntType::Prim(PrimInt::U8)))?.0,
NumRep::U16 => self.init_var_simple(UType::Int(IntType::Prim(PrimInt::U16)))?.0,
NumRep::U32 => self.init_var_simple(UType::Int(IntType::Prim(PrimInt::U32)))?.0,
@@ -630,25 +736,280 @@ pub(crate) mod inference {
NumRep::I16 => self.init_var_simple(UType::Int(IntType::Prim(PrimInt::I16)))?.0,
NumRep::I32 => self.init_var_simple(UType::Int(IntType::Prim(PrimInt::I32)))?.0,
NumRep::I64 => self.init_var_simple(UType::Int(IntType::Prim(PrimInt::I64)))?.0,
}
};
(var, rep)
}
Expr::BinOp(bin_op, lhs, rhs) => {
let var = self.get_new_uvar();
let v_lhs = self.infer_var_expr(&lhs)?;
let v_rhs = self.infer_var_expr(&rhs)?;
let out_rep = bin_op.output_type(lhs.get_rep(), rhs.get_rep());
match out_rep {
// FIXME - figure out what the logic should be...
_ => todo!(),
let this_var = self.get_new_uvar();
let (l_var, l_rep) = self.infer_var_expr(&lhs)?;
let (r_var, r_rep) = self.infer_var_expr(&rhs)?;
if bin_op.is_cast_and(NumRep::is_auto) {
return Err(InferenceError::AbstractCast);
}
let cast_rep = bin_op.cast_rep();
let this_rep = match (l_rep, r_rep) {
(NumRep::AUTO, NumRep::AUTO) => {
self.unify_var_pair(this_var, l_var)?;
self.unify_var_pair(this_var, r_var)?;
if let Some(rep) = cast_rep {
self.unify_var_rep(this_var, rep)?;
rep
} else {
{
// REVIEW - do we need to go this far?
match e.eval() {
Ok(v) => match v.as_const() {
Some(c) => {
// NOTE - if there is a const-evaluable result for the computation, use it to refine our constraints on which types satisfy the aliased Auto
let bounds = Bounds::singleton(c.as_raw_value().clone());
self.unify_var_constraint(this_var, Constraint::Encompasses(bounds))?;
}
None => {
// FIXME - this isn't a hard error necessarily, but our model isn't complex enough for non-TypedConst values to emerge
unimplemented!("Value::AsConst returned None (unexpectedly) when called from InferenceEngine::infer_var_expr");
}
}
Err(e) => {
// NOTE - If the computation will fail regardless, there is no need to infer the type-information of the AST
// REVIEW - make sure that we are confident in EvalErrors being sound reasons to fail type-inference, both now and going forward
return Err(InferenceError::Eval(e))
}
}
}
NumRep::AUTO
}
}
(rep0, rep1) if rep0 == rep1 => {
if let Some(rep) = cast_rep {
self.unify_var_rep(this_var, rep)?;
rep
} else {
self.unify_var_rep(this_var, rep0)?;
rep0
}
}
(rep0, rep1) => {
if let Some(rep) = cast_rep {
self.unify_var_rep(this_var, rep)?;
if l_rep.is_auto() {
debug_assert!(!r_rep.is_auto());
self.unify_var_pair(this_var, l_var)?;
}
if r_rep.is_auto() {
debug_assert!(!l_rep.is_auto());
self.unify_var_pair(this_var, r_var)?;
}
rep
} else {
if l_rep.is_auto() {
debug_assert!(!r_rep.is_auto());
self.unify_var_rep(this_var, rep1)?;
self.unify_var_rep(l_var, rep1)?;
rep1
} else if r_rep.is_auto() {
self.unify_var_rep(this_var, rep0)?;
self.unify_var_rep(r_var, rep0)?;
rep0
} else {
return Err(InferenceError::Ambiguous);
}
}
}

};
(this_var, this_rep)
}
Expr::UnaryOp(unary_op, expr) => {
let this_var = self.get_new_uvar();
let (inner_var, inner_rep) = self.infer_var_expr(&expr)?;
if unary_op.is_cast_and(NumRep::is_auto) {
return Err(InferenceError::AbstractCast);
}
let cast_rep = unary_op.cast_rep();
let this_rep = match inner_rep {
NumRep::AUTO => {
self.unify_var_pair(this_var, inner_var)?;
if let Some(rep) = cast_rep {
self.unify_var_rep(this_var, rep)?;
rep
} else {
{
// REVIEW - do we need to go this far?
match e.eval() {
Ok(v) => match v.as_const() {
Some(c) => {
// NOTE - if there is a const-evaluable result for the computation, use it to refine our constraints on which types satisfy the aliased Auto
let bounds = Bounds::singleton(c.as_raw_value().clone());
self.unify_var_constraint(this_var, Constraint::Encompasses(bounds))?;
}
None => {
// FIXME - this isn't a hard error necessarily, but our model isn't complex enough for non-TypedConst values to emerge
unimplemented!("Value::AsConst returned None (unexpectedly) when called from InferenceEngine::infer_var_expr");
}
}
Err(e) => {
// NOTE - If the computation will fail regardless, there is no need to infer the type-information of the AST
// REVIEW - make sure that we are confident in EvalErrors being sound reasons to fail type-inference, both now and going forward
return Err(InferenceError::Eval(e))
}
}
}
NumRep::AUTO
}
}
rep0 => {
if let Some(rep) = cast_rep {
self.unify_var_rep(this_var, rep)?;
rep
} else {
self.unify_var_rep(this_var, rep0)?;
rep0
}
}
};
(this_var, this_rep)
}
Expr::Cast(rep, expr) => {
let this_var = self.get_new_uvar();
let (inner_var, inner_rep) = self.infer_var_expr(&expr)?;
if rep.is_auto() {
return Err(InferenceError::AbstractCast);
}
if inner_rep.is_auto() {
self.unify_var_rep(inner_var, *rep)?;
}
self.unify_var_rep(this_var, *rep)?;
(this_var, *rep)
}
Expr::UnaryOp(unary_op, expr) => todo!(),
Expr::Cast(num_rep, expr) => todo!(),
};
Ok(topvar)
Ok((top_var, top_rep))
}

fn to_whnf_vtype(&self, t: UType) -> VType {
match t {
UType::Var(v) => {
let v0 = self.get_canonical_uvar(v);
match &self.constraints[v0.0] {
Constraints::Indefinite => VType::Abstract(v0.into()),
Constraints::Invariant(Constraint::Equiv(ut)) => self.to_whnf_vtype(*ut),
Constraints::Invariant(Constraint::Encompasses(bounds)) => VType::Within(bounds.clone()),
}
}
UType::Int(int_type) => VType::Int(int_type),
}
}

pub(crate) fn substitute_uvar_vtype(&self, v: UVar) -> InferenceResult<Option<VType>> {
match &self.constraints[self.get_canonical_uvar(v).0] {
Constraints::Indefinite => Ok(None),
Constraints::Invariant(cx) => Ok(match cx {
Constraint::Equiv(ut) => Some(self.to_whnf_vtype(*ut)),
Constraint::Encompasses(bounds) => Some(VType::Within(bounds.clone()))
})
}
}
}

impl InferenceEngine {
pub fn reify(&self, t: UType) -> Option<IntType> {
match t {
UType::Var(uv) => {
let v = self.get_canonical_uvar(uv);
match self.substitute_uvar_vtype(v) {
Ok(Some(t0)) => match t0 {
VType::Int(int_type) => Some(int_type),
VType::Within(bounds) => match Constraint::get_unique_solution(&Constraint::Encompasses(bounds.clone())) {
Ok(int_type) => Some(int_type),
Err(_) => None,
}
VType::Abstract(utype) => self.reify(utype),
}
Err(_) => None,
Ok(None) => {
match &self.constraints[v.0] {
_ => None,
}
}
}
}
UType::Int(i) => Some(i),
}
}
}
}

use inference::{InferenceEngine, UVar};

pub struct Elaborator {
next_index: usize,
ie: InferenceEngine,
}

impl Elaborator {
fn get_and_increment_index(&mut self) -> usize {
let ret = self.next_index;
self.next_index += 1;
ret
}

fn increment_index(&mut self) {
self.next_index += 1;
}

fn get_index(&self) -> usize {
self.next_index
}

pub(crate) fn new(ie: InferenceEngine) -> Self {
Self { next_index: 0, ie }
}

fn get_type_from_index(&self, index: usize) -> IntType {
let uvar = UVar::new(index);
let Some(t) = self.ie.reify(uvar.into()) else {
unreachable!("unable to reify {uvar}")
};
t
}

pub(crate) fn elaborate_expr(&mut self, expr: &Expr) -> TypedExpr<IntType> {
let index = self.get_and_increment_index();
match expr {
Expr::Const(typed_const) => {
let t = self.get_type_from_index(index);
TypedExpr::ElabConst(t, typed_const.clone())
}
Expr::BinOp(bin_op, x, y) => {
let t_x = self.elaborate_expr(x);
let t_y = self.elaborate_expr(y);
let t = self.get_type_from_index(index);
TypedExpr::ElabBinOp(
t,
TypedBinOp {
sig: ((*t_x.get_type(), *t_y.get_type()), t),
inner: *bin_op,
},
Box::new(t_x),
Box::new(t_y),
)
}
Expr::UnaryOp(unary_op, inner) => {
let t_inner = self.elaborate_expr(inner);
let t = self.get_type_from_index(index);
TypedExpr::ElabUnaryOp(
t,
TypedUnaryOp {
sig: (*t_inner.get_type(), t),
inner: *unary_op,
},
Box::new(t_inner),
)
}
Expr::Cast(rep, inner) => {
let t_inner = self.elaborate_expr(inner);
let t = self.get_type_from_index(index);
TypedExpr::ElabCast(t, *rep, Box::new(t_inner))
}
}
}
}
1 change: 1 addition & 0 deletions experiments/analytic-engine/src/lib.rs
Original file line number Diff line number Diff line change
@@ -4,3 +4,4 @@ extern crate num_traits;

pub mod core;
pub mod elaborator;
pub mod printer;
125 changes: 125 additions & 0 deletions experiments/analytic-engine/src/printer.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,125 @@
use crate::elaborator::{TypedExpr, TypedBinOp, TypedUnaryOp, IntType, PrimInt, Elaborator};
use num_bigint::BigInt;
use crate::core::{BasicBinOp, BinOp, Expr, NumRep, UnaryOp};
use crate::elaborator::inference::InferenceEngine;

fn show_bin_op(bin_op: &BinOp) -> String {
let token = match bin_op.get_op() {
BasicBinOp::Add => "+",
BasicBinOp::Sub => "-",
BasicBinOp::Mul => "*",
BasicBinOp::Div => "/",
BasicBinOp::Rem => "%",
};
if let Some(rep) = bin_op.cast_rep() {
format!("{}{}", token, rep)
} else {
format!("{}", token)
}
}

fn show_typed_bin_op(bin_op: &TypedBinOp<IntType>) -> String {
let token = match bin_op.inner.get_op() {
BasicBinOp::Add => "+",
BasicBinOp::Sub => "-",
BasicBinOp::Mul => "*",
BasicBinOp::Div => "/",
BasicBinOp::Rem => "%",
};
format!("({} : ({},{}) -> {})", token, bin_op.sig.0.0, bin_op.sig.0.1, bin_op.sig.1)
}

fn show_typed_unary_op(unary_op: &TypedUnaryOp<IntType>) -> String {
let token = match unary_op.inner.get_op() {
crate::core::BasicUnaryOp::Negate => "~",
crate::core::BasicUnaryOp::AbsVal => "abs",
};
format!("({} : {} -> {})", token, unary_op.sig.1, unary_op.sig.1)
}


fn show_unary_op(unary_op: &UnaryOp) -> String {
let token = match unary_op.get_op() {
crate::core::BasicUnaryOp::Negate => "~",
crate::core::BasicUnaryOp::AbsVal => "abs",
};
if let Some(rep) = unary_op.cast_rep() {
format!("{}{}", token, rep)
} else {
format!("{}", token)
}
}

// FIXME - adopt pretty-printing engine with precedence rules
fn show_expr(expr: &Expr) -> String {
match expr {
Expr::Const(typed_const) => format!("{}", typed_const),
Expr::BinOp(bin_op, expr, expr1) => format!("({} {} {})", show_expr(expr), show_bin_op(bin_op), show_expr(expr1)),
Expr::UnaryOp(unary_op, expr) => format!("{}({})", show_unary_op(unary_op), show_expr(expr)),
Expr::Cast(num_rep, expr) => format!("{} as {}", show_expr(expr), num_rep),
}
}

// FIXME - adopt pretty-printing engine with precedence rules
fn show_typed_expr(t_expr: &TypedExpr<IntType>) -> String {
match t_expr {
TypedExpr::ElabConst(t, typed_const) => {
format!("({}: {})", typed_const, t)
}
TypedExpr::ElabBinOp(t, typed_bin_op, typed_expr, typed_expr1) => {
format!("({} {} {} : {})", show_typed_expr(typed_expr), show_typed_bin_op(typed_bin_op), show_typed_expr(typed_expr1), t)
}
TypedExpr::ElabUnaryOp(t, typed_unary_op, typed_expr) => {
format!("({}({}) : {})", show_typed_expr(typed_expr), show_typed_unary_op(typed_unary_op), t)
}
TypedExpr::ElabCast(t, num_rep, typed_expr) => {
format!("({} as {} : {})", show_typed_expr(typed_expr), num_rep, t)
}
}
}

pub fn print_conversion(expr: &Expr) {
let mut ie = InferenceEngine::new();
match ie.infer_var_expr(expr) {
Ok(_) => {
let mut elab = Elaborator::new(ie);
let t_expr = elab.elaborate_expr(expr);
println!("Raw: {}", show_expr(expr));
println!("Elaborated: {}", show_typed_expr(&t_expr));
}
Err(e) => {
eprintln!("Inference failed ({}) on {:?}", e, expr);
}
}
}





#[cfg(test)]
mod tests {
use super::*;
use crate::core::TypedConst;

#[test]
fn test_print_conversion() {
let expr = {
Expr::BinOp(
BinOp { op: BasicBinOp::Add, out_rep: None },
Box::new(
Expr::BinOp( BinOp { op: BasicBinOp::Add, out_rep: Some(NumRep::U32) },
Box::new(Expr::Const(TypedConst(BigInt::from(10), NumRep::U32))),
Box::new(Expr::Const(TypedConst(BigInt::from(-1), NumRep::I32))),
)),
Box::new(
Expr::Const(TypedConst(BigInt::from(5), NumRep::Auto))
)
)
};
print_conversion(
&expr
)
}

}