From 3403bd6c834938a6b3bb1d17c3577be8f5808b31 Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Sat, 12 Oct 2024 13:47:53 -0700 Subject: [PATCH 01/12] Make BoolSort and F64Sort zero-sized types --- src/sort/bool.rs | 14 +++----------- src/sort/f64.rs | 14 +++----------- src/typechecking.rs | 4 ++-- 3 files changed, 8 insertions(+), 24 deletions(-) diff --git a/src/sort/bool.rs b/src/sort/bool.rs index aa1e8bb5..87d5e824 100644 --- a/src/sort/bool.rs +++ b/src/sort/bool.rs @@ -3,19 +3,11 @@ use crate::ast::Literal; use super::*; #[derive(Debug)] -pub struct BoolSort { - name: Symbol, -} - -impl BoolSort { - pub fn new(name: Symbol) -> Self { - Self { name } - } -} +pub struct BoolSort; impl Sort for BoolSort { fn name(&self) -> Symbol { - self.name + "bool".into() } fn as_arc_any(self: Arc) -> Arc { @@ -44,7 +36,7 @@ impl IntoSort for bool { type Sort = BoolSort; fn store(self, sort: &Self::Sort) -> Option { Some(Value { - tag: sort.name, + tag: sort.name(), bits: self as u64, }) } diff --git a/src/sort/f64.rs b/src/sort/f64.rs index 5c5430d7..d02915e0 100755 --- a/src/sort/f64.rs +++ b/src/sort/f64.rs @@ -3,19 +3,11 @@ use crate::ast::Literal; use ordered_float::OrderedFloat; #[derive(Debug)] -pub struct F64Sort { - name: Symbol, -} - -impl F64Sort { - pub fn new(name: Symbol) -> Self { - Self { name } - } -} +pub struct F64Sort; impl Sort for F64Sort { fn name(&self) -> Symbol { - self.name + "f64".into() } fn as_arc_any(self: Arc) -> Arc { @@ -70,7 +62,7 @@ impl IntoSort for f64 { type Sort = F64Sort; fn store(self, sort: &Self::Sort) -> Option { Some(Value { - tag: sort.name, + tag: sort.name(), bits: self.to_bits(), }) } diff --git a/src/typechecking.rs b/src/typechecking.rs index 49207694..bf7221bb 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -38,9 +38,9 @@ impl Default for TypeInfo { res.add_sort(UnitSort::new(UNIT_SYM.into()), DUMMY_SPAN.clone()); res.add_sort(StringSort::new("String".into()), DUMMY_SPAN.clone()); - res.add_sort(BoolSort::new("bool".into()), DUMMY_SPAN.clone()); + res.add_sort(BoolSort, DUMMY_SPAN.clone()); res.add_sort(I64Sort::new("i64".into()), DUMMY_SPAN.clone()); - res.add_sort(F64Sort::new("f64".into()), DUMMY_SPAN.clone()); + res.add_sort(F64Sort, DUMMY_SPAN.clone()); res.add_sort(RationalSort::new("Rational".into()), DUMMY_SPAN.clone()); res.presort_names.extend(MapSort::presort_names()); From c05832d7796e922e5dd023109c8598d25ffaee8e Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Sat, 12 Oct 2024 14:02:31 -0700 Subject: [PATCH 02/12] Make UnitSort, StringSort, and RationalSort ZSTs, and make RATS static --- src/actions.rs | 2 +- src/lib.rs | 6 +++--- src/sort/i64.rs | 14 +++----------- src/sort/rational.rs | 26 +++++++++----------------- src/sort/string.rs | 16 ++++------------ src/sort/unit.rs | 14 +++----------- src/typechecking.rs | 10 ++++------ 7 files changed, 27 insertions(+), 61 deletions(-) diff --git a/src/actions.rs b/src/actions.rs index 16454783..f64aa88c 100644 --- a/src/actions.rs +++ b/src/actions.rs @@ -284,7 +284,7 @@ impl EGraph { let ts = self.timestamp; let out = &function.schema.output; match function.decl.default.as_ref() { - None if out.name() == UNIT_SYM.into() => { + None if out.name() == UnitSort.name() => { function.insert(values, Value::unit(), ts); Value::unit() } diff --git a/src/lib.rs b/src/lib.rs index 3c76439a..f1a83d6c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -40,7 +40,7 @@ use thiserror::Error; use generic_symbolic_expressions::Sexp; use ast::*; -pub use typechecking::{TypeInfo, UNIT_SYM}; +pub use typechecking::TypeInfo; use crate::core::{AtomTerm, ResolvedCall}; use actions::Program; @@ -739,7 +739,7 @@ impl EGraph { .get(&sym) // function_to_dag should have checked this .unwrap(); - let out_is_unit = f.schema.output.name() == UNIT_SYM.into(); + let out_is_unit = f.schema.output.name() == UnitSort.name(); let mut buf = String::new(); let s = &mut buf; @@ -1367,7 +1367,7 @@ impl EGraph { let mut exprs: Vec = str_buf.iter().map(|&s| parse(s)).collect(); actions.push( - if function_type.is_datatype || function_type.output.name() == UNIT_SYM.into() { + if function_type.is_datatype || function_type.output.name() == UnitSort.name() { Action::Expr(span.clone(), Expr::Call(span.clone(), func_name, exprs)) } else { let out = exprs.pop().unwrap(); diff --git a/src/sort/i64.rs b/src/sort/i64.rs index 606c93e6..0e9ef1e7 100644 --- a/src/sort/i64.rs +++ b/src/sort/i64.rs @@ -3,19 +3,11 @@ use crate::{ast::Literal, constraint::AllEqualTypeConstraint}; use super::*; #[derive(Debug)] -pub struct I64Sort { - name: Symbol, -} - -impl I64Sort { - pub fn new(name: Symbol) -> Self { - Self { name } - } -} +pub struct I64Sort; impl Sort for I64Sort { fn name(&self) -> Symbol { - self.name + "i64".into() } fn as_arc_any(self: Arc) -> Arc { @@ -87,7 +79,7 @@ impl IntoSort for i64 { type Sort = I64Sort; fn store(self, sort: &Self::Sort) -> Option { Some(Value { - tag: sort.name, + tag: sort.name(), bits: self as u64, }) } diff --git a/src/sort/rational.rs b/src/sort/rational.rs index 739faf07..1508faab 100644 --- a/src/sort/rational.rs +++ b/src/sort/rational.rs @@ -7,24 +7,16 @@ use crate::{ast::Literal, util::IndexSet}; use super::*; -#[derive(Debug)] -pub struct RationalSort { - name: Symbol, - rats: Mutex>, +lazy_static! { + static ref RATS: Mutex> = Default::default(); } -impl RationalSort { - pub fn new(name: Symbol) -> Self { - Self { - name, - rats: Default::default(), - } - } -} +#[derive(Debug)] +pub struct RationalSort; impl Sort for RationalSort { fn name(&self) -> Symbol { - self.name + "Rational".into() } fn as_arc_any(self: Arc) -> Arc { @@ -130,18 +122,18 @@ impl Sort for RationalSort { impl FromSort for R { type Sort = RationalSort; - fn load(sort: &Self::Sort, value: &Value) -> Self { + fn load(_sort: &Self::Sort, value: &Value) -> Self { let i = value.bits as usize; - *sort.rats.lock().unwrap().get_index(i).unwrap() + *RATS.lock().unwrap().get_index(i).unwrap() } } impl IntoSort for R { type Sort = RationalSort; fn store(self, sort: &Self::Sort) -> Option { - let (i, _) = sort.rats.lock().unwrap().insert_full(self); + let (i, _) = RATS.lock().unwrap().insert_full(self); Some(Value { - tag: sort.name, + tag: sort.name(), bits: i as u64, }) } diff --git a/src/sort/string.rs b/src/sort/string.rs index ce115d6f..75530348 100644 --- a/src/sort/string.rs +++ b/src/sort/string.rs @@ -5,19 +5,11 @@ use crate::{ast::Literal, constraint::AllEqualTypeConstraint}; use super::*; #[derive(Debug)] -pub struct StringSort { - pub name: Symbol, -} - -impl StringSort { - pub fn new(name: Symbol) -> Self { - Self { name } - } -} +pub struct StringSort; impl Sort for StringSort { fn name(&self) -> Symbol { - self.name + "String".into() } fn as_arc_any(self: Arc) -> Arc { @@ -25,7 +17,7 @@ impl Sort for StringSort { } fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) { - assert!(value.tag == self.name); + assert!(value.tag == self.name()); let sym = Symbol::from(NonZeroU32::new(value.bits as _).unwrap()); ( 1, @@ -51,7 +43,7 @@ impl IntoSort for Symbol { type Sort = StringSort; fn store(self, sort: &Self::Sort) -> Option { Some(Value { - tag: sort.name, + tag: sort.name(), bits: NonZeroU32::from(self).get() as _, }) } diff --git a/src/sort/unit.rs b/src/sort/unit.rs index 31caf14a..be8c2892 100644 --- a/src/sort/unit.rs +++ b/src/sort/unit.rs @@ -2,19 +2,11 @@ use super::*; use crate::{ast::Literal, constraint::AllEqualTypeConstraint, ArcSort, PrimitiveLike}; #[derive(Debug)] -pub struct UnitSort { - name: Symbol, -} - -impl UnitSort { - pub fn new(name: Symbol) -> Self { - Self { name } - } -} +pub struct UnitSort; impl Sort for UnitSort { fn name(&self) -> Symbol { - self.name + "Unit".into() } fn as_arc_any(self: Arc) -> Arc { @@ -26,7 +18,7 @@ impl Sort for UnitSort { } fn make_expr(&self, _egraph: &EGraph, value: Value) -> (Cost, Expr) { - assert_eq!(value.tag, self.name); + assert_eq!(value.tag, self.name()); (1, GenericExpr::Lit(DUMMY_SPAN.clone(), Literal::Unit)) } } diff --git a/src/typechecking.rs b/src/typechecking.rs index bf7221bb..36212a13 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -36,12 +36,12 @@ impl Default for TypeInfo { global_types: Default::default(), }; - res.add_sort(UnitSort::new(UNIT_SYM.into()), DUMMY_SPAN.clone()); - res.add_sort(StringSort::new("String".into()), DUMMY_SPAN.clone()); + res.add_sort(UnitSort, DUMMY_SPAN.clone()); + res.add_sort(StringSort, DUMMY_SPAN.clone()); res.add_sort(BoolSort, DUMMY_SPAN.clone()); - res.add_sort(I64Sort::new("i64".into()), DUMMY_SPAN.clone()); + res.add_sort(I64Sort, DUMMY_SPAN.clone()); res.add_sort(F64Sort, DUMMY_SPAN.clone()); - res.add_sort(RationalSort::new("Rational".into()), DUMMY_SPAN.clone()); + res.add_sort(RationalSort, DUMMY_SPAN.clone()); res.presort_names.extend(MapSort::presort_names()); res.presort_names.extend(SetSort::presort_names()); @@ -62,8 +62,6 @@ impl Default for TypeInfo { } } -pub const UNIT_SYM: &str = "Unit"; - impl TypeInfo { pub(crate) fn infer_literal(&self, lit: &Literal) -> ArcSort { match lit { From d86fe2d71184280af8d5088695b1d9998cb545f1 Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Sat, 12 Oct 2024 14:47:26 -0700 Subject: [PATCH 03/12] Don't store ZSTs --- src/ast/expr.rs | 4 ++-- src/ast/remove_globals.rs | 18 +++++------------- src/constraint.rs | 17 +++++++---------- src/core.rs | 12 +++++------- src/lib.rs | 14 +++++++------- src/sort/fn.rs | 8 ++------ src/sort/map.rs | 12 +++--------- src/sort/mod.rs | 22 +++++++++++++--------- src/sort/set.rs | 19 ++++++------------- src/sort/vec.rs | 30 +++++++++--------------------- src/typechecking.rs | 18 ++---------------- 11 files changed, 61 insertions(+), 113 deletions(-) diff --git a/src/ast/expr.rs b/src/ast/expr.rs index 83f96566..bc27d317 100644 --- a/src/ast/expr.rs +++ b/src/ast/expr.rs @@ -123,9 +123,9 @@ pub enum GenericExpr { } impl ResolvedExpr { - pub fn output_type(&self, type_info: &TypeInfo) -> ArcSort { + pub fn output_type(&self) -> ArcSort { match self { - ResolvedExpr::Lit(_, lit) => type_info.infer_literal(lit), + ResolvedExpr::Lit(_, lit) => sort::literal_sort(lit), ResolvedExpr::Var(_, resolved_var) => resolved_var.sort.clone(), ResolvedExpr::Call(_, resolved_call, _) => resolved_call.output().clone(), } diff --git a/src/ast/remove_globals.rs b/src/ast/remove_globals.rs index 9c60e21c..c71ed2a9 100644 --- a/src/ast/remove_globals.rs +++ b/src/ast/remove_globals.rs @@ -5,11 +5,8 @@ //! When a globally-bound primitive value is used in the actions of a rule, //! we add a new variable to the query bound to the primitive value. -use crate::{ - core::ResolvedCall, typechecking::FuncType, FreshGen, GenericAction, GenericActions, - GenericExpr, GenericFact, GenericNCommand, GenericRule, HashMap, ResolvedAction, ResolvedExpr, - ResolvedFact, ResolvedFunctionDecl, ResolvedNCommand, ResolvedVar, Schema, SymbolGen, TypeInfo, -}; +use crate::*; +use crate::{core::ResolvedCall, typechecking::FuncType}; struct GlobalRemover<'a> { fresh: &'a mut SymbolGen, @@ -45,13 +42,12 @@ struct GlobalRemover<'a> { /// ((Add fresh_var_for_x fresh_var_for_x))) /// ``` pub(crate) fn remove_globals( - type_info: &TypeInfo, prog: Vec, fresh: &mut SymbolGen, ) -> Vec { let mut remover = GlobalRemover { fresh }; prog.into_iter() - .flat_map(|cmd| remover.remove_globals_cmd(type_info, cmd)) + .flat_map(|cmd| remover.remove_globals_cmd(cmd)) .collect() } @@ -91,15 +87,11 @@ fn remove_globals_action(action: ResolvedAction) -> ResolvedAction { } impl<'a> GlobalRemover<'a> { - fn remove_globals_cmd( - &mut self, - type_info: &TypeInfo, - cmd: ResolvedNCommand, - ) -> Vec { + fn remove_globals_cmd(&mut self, cmd: ResolvedNCommand) -> Vec { match cmd { GenericNCommand::CoreAction(action) => match action { GenericAction::Let(span, name, expr) => { - let ty = expr.output_type(type_info); + let ty = expr.output_type(); let func_decl = ResolvedFunctionDecl { name: name.name, diff --git a/src/constraint.rs b/src/constraint.rs index 493fb838..35f61f9e 100644 --- a/src/constraint.rs +++ b/src/constraint.rs @@ -273,7 +273,7 @@ impl Assignment { .collect(); let types: Vec<_> = args .iter() - .map(|arg| arg.output_type(typeinfo)) + .map(|arg| arg.output_type()) .chain(once( self.get(&AtomTerm::Var(DUMMY_SPAN.clone(), *corresponding_var)) .unwrap() @@ -351,8 +351,8 @@ impl Assignment { let rhs = self.annotate_expr(rhs, typeinfo); let types: Vec<_> = children .iter() - .map(|child| child.output_type(typeinfo)) - .chain(once(rhs.output_type(typeinfo))) + .map(|child| child.output_type()) + .chain(once(rhs.output_type())) .collect(); let resolved_call = ResolvedCall::from_resolution(head, &types, typeinfo); if !matches!(resolved_call, ResolvedCall::Func(_)) { @@ -379,10 +379,7 @@ impl Assignment { .iter() .map(|child| self.annotate_expr(child, typeinfo)) .collect(); - let types: Vec<_> = children - .iter() - .map(|child| child.output_type(typeinfo)) - .collect(); + let types: Vec<_> = children.iter().map(|child| child.output_type()).collect(); let resolved_call = ResolvedCall::from_resolution_func_types(head, &types, typeinfo) .ok_or_else(|| TypeError::UnboundFunction(*head, span.clone()))?; @@ -568,7 +565,7 @@ impl CoreAction { get_literal_and_global_constraints(&[e.clone(), n.clone()], typeinfo) .chain(once(Constraint::Assign( n.clone(), - typeinfo.get_sort_nofail::() as ArcSort, + std::sync::Arc::new(I64Sort) as ArcSort, ))) .collect(), ) @@ -684,8 +681,8 @@ fn get_literal_and_global_constraints<'a>( AtomTerm::Var(_, _) => None, // Literal to type constraint AtomTerm::Literal(_, lit) => { - let typ = type_info.infer_literal(lit); - Some(Constraint::Assign(arg.clone(), typ.clone())) + let typ = crate::sort::literal_sort(lit); + Some(Constraint::Assign(arg.clone(), typ)) } AtomTerm::Global(_, v) => { if let Some(typ) = type_info.lookup_global(v) { diff --git a/src/core.rs b/src/core.rs index c62d381c..5d3345ac 100644 --- a/src/core.rs +++ b/src/core.rs @@ -13,8 +13,7 @@ use std::hash::Hasher; use std::ops::AddAssign; -use crate::HashMap; -use crate::{typechecking::FuncType, *}; +use crate::{typechecking::FuncType, HashMap, *}; use typechecking::TypeError; #[derive(Debug, Clone, PartialEq, Eq)] @@ -190,10 +189,10 @@ impl GenericAtomTerm { } impl ResolvedAtomTerm { - pub fn output(&self, typeinfo: &TypeInfo) -> ArcSort { + pub fn output(&self) -> ArcSort { match self { ResolvedAtomTerm::Var(_, v) => v.sort.clone(), - ResolvedAtomTerm::Literal(_, l) => typeinfo.infer_literal(l), + ResolvedAtomTerm::Literal(_, l) => literal_sort(l), ResolvedAtomTerm::Global(_, v) => v.sort.clone(), } } @@ -838,12 +837,11 @@ impl ResolvedRule { fresh_gen: &mut SymbolGen, ) -> Result { let value_eq = &typeinfo.primitives.get(&Symbol::from("value-eq")).unwrap()[0]; - let unit = typeinfo.get_sort_nofail::(); self.to_canonicalized_core_rule_impl(typeinfo, fresh_gen, |at1, at2| { ResolvedCall::Primitive(SpecializedPrimitive { primitive: value_eq.clone(), - input: vec![at1.output(typeinfo), at2.output(typeinfo)], - output: unit.clone(), + input: vec![at1.output(), at2.output()], + output: Arc::new(UnitSort), }) }) } diff --git a/src/lib.rs b/src/lib.rs index f1a83d6c..e258eed4 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -678,11 +678,11 @@ impl EGraph { pub fn eval_lit(&self, lit: &Literal) -> Value { match lit { - Literal::Int(i) => i.store(&self.type_info.get_sort_nofail()).unwrap(), - Literal::F64(f) => f.store(&self.type_info.get_sort_nofail()).unwrap(), - Literal::String(s) => s.store(&self.type_info.get_sort_nofail()).unwrap(), - Literal::Unit => ().store(&self.type_info.get_sort_nofail()).unwrap(), - Literal::Bool(b) => b.store(&self.type_info.get_sort_nofail()).unwrap(), + Literal::Int(i) => i.store(&I64Sort).unwrap(), + Literal::F64(f) => f.store(&F64Sort).unwrap(), + Literal::String(s) => s.store(&StringSort).unwrap(), + Literal::Unit => ().store(&UnitSort).unwrap(), + Literal::Bool(b) => b.store(&BoolSort).unwrap(), } } @@ -1300,7 +1300,7 @@ impl EGraph { let mut termdag = TermDag::default(); for expr in exprs { let value = self.eval_resolved_expr(&expr)?; - let expr_type = expr.output_type(&self.type_info); + let expr_type = expr.output_type(); let term = self.extract(value, &mut termdag, &expr_type).1; use std::io::Write; writeln!(f, "{}", termdag.to_string(&term)) @@ -1412,7 +1412,7 @@ impl EGraph { .type_info .typecheck_program(&mut self.symbol_gen, &program)?; - let program = remove_globals(&self.type_info, program, &mut self.symbol_gen); + let program = remove_globals(program, &mut self.symbol_gen); Ok(program) } diff --git a/src/sort/fn.rs b/src/sort/fn.rs index 25a2b114..a19390fe 100644 --- a/src/sort/fn.rs +++ b/src/sort/fn.rs @@ -152,7 +152,6 @@ impl Sort for FunctionSort { typeinfo.add_primitive(Ctor { name: "unstable-fn".into(), function: self.clone(), - string: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Apply { name: "unstable-app".into(), @@ -214,7 +213,6 @@ impl FromSort for ValueFunction { struct FunctionCTorTypeConstraint { name: Symbol, function: Arc, - string: Arc, span: Span, } @@ -304,7 +302,7 @@ impl TypeConstraint for FunctionCTorTypeConstraint { // Otherwise we just try assuming it's this function, we don't know if it is or not vec![ - Constraint::Assign(arguments[0].clone(), self.string.clone()), + Constraint::Assign(arguments[0].clone(), Arc::new(StringSort)), output_sort_constraint, ] } @@ -314,7 +312,6 @@ impl TypeConstraint for FunctionCTorTypeConstraint { struct Ctor { name: Symbol, function: Arc, - string: Arc, } impl PrimitiveLike for Ctor { @@ -326,14 +323,13 @@ impl PrimitiveLike for Ctor { Box::new(FunctionCTorTypeConstraint { name: self.name, function: self.function.clone(), - string: self.string.clone(), span: span.clone(), }) } fn apply(&self, values: &[Value], egraph: Option<&mut EGraph>) -> Option { let egraph = egraph.expect("`unstable-fn` is not supported yet in facts."); - let name = Symbol::load(&self.string, &values[0]); + let name = Symbol::load(&StringSort, &values[0]); // self.function // .sorts // .insert(name.clone(), self.function.clone()); diff --git a/src/sort/map.rs b/src/sort/map.rs index dfdb7bb9..cf03245e 100644 --- a/src/sort/map.rs +++ b/src/sort/map.rs @@ -149,12 +149,10 @@ impl Sort for MapSort { typeinfo.add_primitive(NotContains { name: "map-not-contains".into(), map: self.clone(), - unit: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Contains { name: "map-contains".into(), map: self.clone(), - unit: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Remove { name: "map-remove".into(), @@ -162,7 +160,6 @@ impl Sort for MapSort { }); typeinfo.add_primitive(Length { name: "map-length".into(), - i64: typeinfo.get_sort_nofail(), map: self, }); } @@ -378,7 +375,6 @@ impl PrimitiveLike for Get { struct NotContains { name: Symbol, map: Arc, - unit: Arc, } impl PrimitiveLike for NotContains { @@ -389,7 +385,7 @@ impl PrimitiveLike for NotContains { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.map.clone(), self.map.key(), self.unit.clone()], + vec![self.map.clone(), self.map.key(), Arc::new(UnitSort)], span.clone(), ) .into_box() @@ -408,7 +404,6 @@ impl PrimitiveLike for NotContains { struct Contains { name: Symbol, map: Arc, - unit: Arc, } impl PrimitiveLike for Contains { @@ -419,7 +414,7 @@ impl PrimitiveLike for Contains { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.map.clone(), self.map.key(), self.unit.clone()], + vec![self.map.clone(), self.map.key(), Arc::new(UnitSort)], span.clone(), ) .into_box() @@ -464,7 +459,6 @@ impl PrimitiveLike for Remove { struct Length { name: Symbol, map: Arc, - i64: Arc, } impl PrimitiveLike for Length { @@ -475,7 +469,7 @@ impl PrimitiveLike for Length { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.map.clone(), self.i64.clone()], + vec![self.map.clone(), Arc::new(I64Sort)], span.clone(), ) .into_box() diff --git a/src/sort/mod.rs b/src/sort/mod.rs index e758a52c..86fe9fb4 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -157,23 +157,17 @@ impl IntoSort for Option { pub type PreSort = fn(typeinfo: &mut TypeInfo, name: Symbol, params: &[Expr]) -> Result; -pub(crate) struct ValueEq { - pub unit: Arc, -} - -lazy_static! { - static ref VALUE_EQ: Symbol = "value-eq".into(); -} +pub(crate) struct ValueEq; impl PrimitiveLike for ValueEq { fn name(&self) -> Symbol { - *VALUE_EQ + "value-eq".into() } fn get_type_constraints(&self, span: &Span) -> Box { AllEqualTypeConstraint::new(self.name(), span.clone()) .with_exact_length(3) - .with_output_sort(self.unit.clone()) + .with_output_sort(Arc::new(UnitSort)) .into_box() } @@ -186,3 +180,13 @@ impl PrimitiveLike for ValueEq { } } } + +pub fn literal_sort(lit: &Literal) -> ArcSort { + match lit { + Literal::Int(_) => Arc::new(I64Sort) as ArcSort, + Literal::F64(_) => Arc::new(F64Sort) as ArcSort, + Literal::String(_) => Arc::new(StringSort) as ArcSort, + Literal::Bool(_) => Arc::new(BoolSort) as ArcSort, + Literal::Unit => Arc::new(UnitSort) as ArcSort, + } +} diff --git a/src/sort/set.rs b/src/sort/set.rs index 6cd3b0be..1a97987d 100644 --- a/src/sort/set.rs +++ b/src/sort/set.rs @@ -136,12 +136,10 @@ impl Sort for SetSort { typeinfo.add_primitive(NotContains { name: "set-not-contains".into(), set: self.clone(), - unit: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Contains { name: "set-contains".into(), set: self.clone(), - unit: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Remove { name: "set-remove".into(), @@ -150,12 +148,10 @@ impl Sort for SetSort { typeinfo.add_primitive(Get { name: "set-get".into(), set: self.clone(), - i64: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Length { name: "set-length".into(), set: self.clone(), - i64: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Union { name: "set-union".into(), @@ -322,7 +318,6 @@ impl PrimitiveLike for Insert { struct NotContains { name: Symbol, set: Arc, - unit: Arc, } impl PrimitiveLike for NotContains { @@ -333,7 +328,7 @@ impl PrimitiveLike for NotContains { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.set.clone(), self.set.element(), self.unit.clone()], + vec![self.set.clone(), self.set.element(), Arc::new(UnitSort)], span.clone(), ) .into_box() @@ -352,7 +347,6 @@ impl PrimitiveLike for NotContains { struct Contains { name: Symbol, set: Arc, - unit: Arc, } impl PrimitiveLike for Contains { @@ -363,7 +357,7 @@ impl PrimitiveLike for Contains { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.set.clone(), self.set.element(), self.unit.clone()], + vec![self.set.clone(), self.set.element(), Arc::new(UnitSort)], span.clone(), ) .into_box() @@ -437,7 +431,6 @@ impl PrimitiveLike for Intersect { struct Length { name: Symbol, set: Arc, - i64: Arc, } impl PrimitiveLike for Length { @@ -448,7 +441,7 @@ impl PrimitiveLike for Length { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.set.clone(), self.i64.clone()], + vec![self.set.clone(), Arc::new(I64Sort)], span.clone(), ) .into_box() @@ -459,10 +452,10 @@ impl PrimitiveLike for Length { Some(Value::from(set.len() as i64)) } } + struct Get { name: Symbol, set: Arc, - i64: Arc, } impl PrimitiveLike for Get { @@ -473,7 +466,7 @@ impl PrimitiveLike for Get { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.set.clone(), self.i64.clone(), self.set.element()], + vec![self.set.clone(), Arc::new(I64Sort), self.set.element()], span.clone(), ) .into_box() @@ -481,7 +474,7 @@ impl PrimitiveLike for Get { fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { let set = ValueSet::load(&self.set, &values[0]); - let index = i64::load(&self.i64, &values[1]); + let index = i64::load(&I64Sort, &values[1]); set.iter().nth(index as usize).copied() } } diff --git a/src/sort/vec.rs b/src/sort/vec.rs index adc821b2..cedfb7d8 100644 --- a/src/sort/vec.rs +++ b/src/sort/vec.rs @@ -141,32 +141,26 @@ impl Sort for VecSort { typeinfo.add_primitive(NotContains { name: "vec-not-contains".into(), vec: self.clone(), - unit: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Contains { name: "vec-contains".into(), vec: self.clone(), - unit: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Length { name: "vec-length".into(), vec: self.clone(), - i64: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Get { name: "vec-get".into(), vec: self.clone(), - i64: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Set { name: "vec-set".into(), vec: self.clone(), - i64: typeinfo.get_sort_nofail(), }); typeinfo.add_primitive(Remove { name: "vec-remove".into(), vec: self, - i64: typeinfo.get_sort_nofail(), }) } @@ -375,7 +369,6 @@ impl PrimitiveLike for Pop { struct NotContains { name: Symbol, vec: Arc, - unit: Arc, } impl PrimitiveLike for NotContains { @@ -386,7 +379,7 @@ impl PrimitiveLike for NotContains { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.vec.clone(), self.vec.element(), self.unit.clone()], + vec![self.vec.clone(), self.vec.element(), Arc::new(UnitSort)], span.clone(), ) .into_box() @@ -405,7 +398,6 @@ impl PrimitiveLike for NotContains { struct Contains { name: Symbol, vec: Arc, - unit: Arc, } impl PrimitiveLike for Contains { @@ -416,7 +408,7 @@ impl PrimitiveLike for Contains { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.vec.clone(), self.vec.element(), self.unit.clone()], + vec![self.vec.clone(), self.vec.element(), Arc::new(UnitSort)], span.clone(), ) .into_box() @@ -435,7 +427,6 @@ impl PrimitiveLike for Contains { struct Length { name: Symbol, vec: Arc, - i64: Arc, } impl PrimitiveLike for Length { @@ -446,7 +437,7 @@ impl PrimitiveLike for Length { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.vec.clone(), self.i64.clone()], + vec![self.vec.clone(), Arc::new(I64Sort)], span.clone(), ) .into_box() @@ -461,7 +452,6 @@ impl PrimitiveLike for Length { struct Get { name: Symbol, vec: Arc, - i64: Arc, } impl PrimitiveLike for Get { @@ -472,7 +462,7 @@ impl PrimitiveLike for Get { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.vec.clone(), self.i64.clone(), self.vec.element()], + vec![self.vec.clone(), Arc::new(I64Sort), self.vec.element()], span.clone(), ) .into_box() @@ -480,7 +470,7 @@ impl PrimitiveLike for Get { fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { let vec = ValueVec::load(&self.vec, &values[0]); - let index = i64::load(&self.i64, &values[1]); + let index = i64::load(&I64Sort, &values[1]); vec.get(index as usize).copied() } } @@ -488,7 +478,6 @@ impl PrimitiveLike for Get { struct Set { name: Symbol, vec: Arc, - i64: Arc, } impl PrimitiveLike for Set { @@ -501,7 +490,7 @@ impl PrimitiveLike for Set { self.name(), vec![ self.vec.clone(), - self.i64.clone(), + Arc::new(I64Sort), self.vec.element.clone(), self.vec.clone(), ], @@ -512,7 +501,7 @@ impl PrimitiveLike for Set { fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { let mut vec = ValueVec::load(&self.vec, &values[0]); - let index = i64::load(&self.i64, &values[1]); + let index = i64::load(&I64Sort, &values[1]); vec[index as usize] = values[2]; vec.store(&self.vec) } @@ -521,7 +510,6 @@ impl PrimitiveLike for Set { struct Remove { name: Symbol, vec: Arc, - i64: Arc, } impl PrimitiveLike for Remove { @@ -532,7 +520,7 @@ impl PrimitiveLike for Remove { fn get_type_constraints(&self, span: &Span) -> Box { SimpleTypeConstraint::new( self.name(), - vec![self.vec.clone(), self.i64.clone(), self.vec.clone()], + vec![self.vec.clone(), Arc::new(I64Sort), self.vec.clone()], span.clone(), ) .into_box() @@ -540,7 +528,7 @@ impl PrimitiveLike for Remove { fn apply(&self, values: &[Value], _egraph: Option<&mut EGraph>) -> Option { let mut vec = ValueVec::load(&self.vec, &values[0]); - let i = i64::load(&self.i64, &values[1]); + let i = i64::load(&I64Sort, &values[1]); vec.remove(i.try_into().unwrap()); vec.store(&self.vec) } diff --git a/src/typechecking.rs b/src/typechecking.rs index 36212a13..4fd93ffc 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -54,27 +54,13 @@ impl Default for TypeInfo { res.presorts .insert("UnstableFn".into(), FunctionSort::make_sort); - res.add_primitive(ValueEq { - unit: res.get_sort_nofail(), - }); + res.add_primitive(ValueEq); res } } impl TypeInfo { - pub(crate) fn infer_literal(&self, lit: &Literal) -> ArcSort { - match lit { - Literal::Int(_) => self.sorts.get(&Symbol::from("i64")), - Literal::F64(_) => self.sorts.get(&Symbol::from("f64")), - Literal::String(_) => self.sorts.get(&Symbol::from("String")), - Literal::Bool(_) => self.sorts.get(&Symbol::from("bool")), - Literal::Unit => self.sorts.get(&Symbol::from("Unit")), - } - .unwrap() - .clone() - } - pub fn add_sort(&mut self, sort: S, span: Span) { self.add_arcsort(Arc::new(sort), span).unwrap() } @@ -190,7 +176,7 @@ impl TypeInfo { } NCommand::CoreAction(Action::Let(span, var, expr)) => { let expr = self.typecheck_expr(symbol_gen, expr, &Default::default())?; - let output_type = expr.output_type(self); + let output_type = expr.output_type(); self.global_types.insert(*var, output_type.clone()); let var = ResolvedVar { name: *var, From a3a78794a4bdeecc63fcb60987578bc0f6f31c2f Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Sat, 12 Oct 2024 15:01:32 -0700 Subject: [PATCH 04/12] Add Presort trait --- src/sort/fn.rs | 21 +++++++++++++------- src/sort/map.rs | 36 +++++++++++++++++++--------------- src/sort/mod.rs | 10 ++++++++++ src/sort/set.rs | 42 +++++++++++++++++++++------------------ src/sort/vec.rs | 10 ++++++++-- src/typechecking.rs | 48 +++++++++++++++++++++++++-------------------- 6 files changed, 102 insertions(+), 65 deletions(-) diff --git a/src/sort/fn.rs b/src/sort/fn.rs index a19390fe..d95ebac0 100644 --- a/src/sort/fn.rs +++ b/src/sort/fn.rs @@ -54,10 +54,22 @@ pub struct FunctionSort { } impl FunctionSort { - pub fn presort_names() -> Vec { + fn get_value(&self, value: &Value) -> ValueFunction { + let functions = self.functions.lock().unwrap(); + functions.get_index(value.bits as usize).unwrap().clone() + } +} + +impl Presort for FunctionSort { + fn name() -> Symbol { + "UnstableFn".into() + } + + fn presort_names() -> Vec { vec!["unstable-fn".into(), "unstable-app".into()] } - pub fn make_sort( + + fn make_sort( typeinfo: &mut TypeInfo, name: Symbol, args: &[Expr], @@ -102,11 +114,6 @@ impl FunctionSort { panic!("function sort must be called with list of input args and output sort"); } } - - fn get_value(&self, value: &Value) -> ValueFunction { - let functions = self.functions.lock().unwrap(); - functions.get_index(value.bits as usize).unwrap().clone() - } } impl Sort for FunctionSort { diff --git a/src/sort/map.rs b/src/sort/map.rs index cf03245e..db03c410 100644 --- a/src/sort/map.rs +++ b/src/sort/map.rs @@ -23,8 +23,27 @@ impl MapSort { fn value(&self) -> ArcSort { self.value.clone() } +} + +impl Presort for MapSort { + fn name() -> Symbol { + "Map".into() + } + + fn presort_names() -> Vec { + vec![ + "rebuild".into(), + "map-empty".into(), + "map-insert".into(), + "map-get".into(), + "map-not-contains".into(), + "map-contains".into(), + "map-remove".into(), + "map-length".into(), + ] + } - pub fn make_sort( + fn make_sort( typeinfo: &mut TypeInfo, name: Symbol, args: &[Expr], @@ -68,21 +87,6 @@ impl MapSort { } } -impl MapSort { - pub fn presort_names() -> Vec { - vec![ - "rebuild".into(), - "map-empty".into(), - "map-insert".into(), - "map-get".into(), - "map-not-contains".into(), - "map-contains".into(), - "map-remove".into(), - "map-length".into(), - ] - } -} - impl Sort for MapSort { fn name(&self) -> Symbol { self.name diff --git a/src/sort/mod.rs b/src/sort/mod.rs index 86fe9fb4..afa7c597 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -102,6 +102,16 @@ pub trait Sort: Any + Send + Sync + Debug { } } +pub trait Presort { + fn name() -> Symbol; + fn presort_names() -> Vec; + fn make_sort( + typeinfo: &mut TypeInfo, + name: Symbol, + args: &[Expr], + ) -> Result; +} + #[derive(Debug)] pub struct EqSort { pub name: Symbol, diff --git a/src/sort/set.rs b/src/sort/set.rs index 1a97987d..f7c68c58 100644 --- a/src/sort/set.rs +++ b/src/sort/set.rs @@ -22,8 +22,30 @@ impl SetSort { pub fn element_name(&self) -> Symbol { self.element.name() } +} + +impl Presort for SetSort { + fn name() -> Symbol { + "Set".into() + } + + fn presort_names() -> Vec { + vec![ + "set-of".into(), + "set-empty".into(), + "set-insert".into(), + "set-not-contains".into(), + "set-contains".into(), + "set-remove".into(), + "set-union".into(), + "set-diff".into(), + "set-intersect".into(), + "set-get".into(), + "set-length".into(), + ] + } - pub fn make_sort( + fn make_sort( typeinfo: &mut TypeInfo, name: Symbol, args: &[Expr], @@ -53,24 +75,6 @@ impl SetSort { } } -impl SetSort { - pub fn presort_names() -> Vec { - vec![ - "set-of".into(), - "set-empty".into(), - "set-insert".into(), - "set-not-contains".into(), - "set-contains".into(), - "set-remove".into(), - "set-union".into(), - "set-diff".into(), - "set-intersect".into(), - "set-get".into(), - "set-length".into(), - ] - } -} - impl Sort for SetSort { fn name(&self) -> Symbol { self.name diff --git a/src/sort/vec.rs b/src/sort/vec.rs index cedfb7d8..2311c672 100644 --- a/src/sort/vec.rs +++ b/src/sort/vec.rs @@ -21,8 +21,14 @@ impl VecSort { pub fn element_name(&self) -> Symbol { self.element.name() } +} + +impl Presort for VecSort { + fn name() -> Symbol { + "Vec".into() + } - pub fn presort_names() -> Vec { + fn presort_names() -> Vec { vec![ "vec-of".into(), "vec-append".into(), @@ -38,7 +44,7 @@ impl VecSort { ] } - pub fn make_sort( + fn make_sort( typeinfo: &mut TypeInfo, name: Symbol, args: &[Expr], diff --git a/src/typechecking.rs b/src/typechecking.rs index 4fd93ffc..12d90e05 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -1,6 +1,6 @@ use crate::{core::CoreRule, *}; use ast::Rule; -use hashbrown::hash_map; +use hashbrown::hash_map::Entry; #[derive(Clone, Debug)] pub struct FuncType { @@ -36,23 +36,17 @@ impl Default for TypeInfo { global_types: Default::default(), }; - res.add_sort(UnitSort, DUMMY_SPAN.clone()); - res.add_sort(StringSort, DUMMY_SPAN.clone()); - res.add_sort(BoolSort, DUMMY_SPAN.clone()); - res.add_sort(I64Sort, DUMMY_SPAN.clone()); - res.add_sort(F64Sort, DUMMY_SPAN.clone()); - res.add_sort(RationalSort, DUMMY_SPAN.clone()); + res.add_sort(UnitSort, DUMMY_SPAN.clone()).unwrap(); + res.add_sort(StringSort, DUMMY_SPAN.clone()).unwrap(); + res.add_sort(BoolSort, DUMMY_SPAN.clone()).unwrap(); + res.add_sort(I64Sort, DUMMY_SPAN.clone()).unwrap(); + res.add_sort(F64Sort, DUMMY_SPAN.clone()).unwrap(); + res.add_sort(RationalSort, DUMMY_SPAN.clone()).unwrap(); - res.presort_names.extend(MapSort::presort_names()); - res.presort_names.extend(SetSort::presort_names()); - res.presort_names.extend(VecSort::presort_names()); - res.presort_names.extend(FunctionSort::presort_names()); - - res.presorts.insert("Map".into(), MapSort::make_sort); - res.presorts.insert("Set".into(), SetSort::make_sort); - res.presorts.insert("Vec".into(), VecSort::make_sort); - res.presorts - .insert("UnstableFn".into(), FunctionSort::make_sort); + res.add_presort::(DUMMY_SPAN.clone()).unwrap(); + res.add_presort::(DUMMY_SPAN.clone()).unwrap(); + res.add_presort::(DUMMY_SPAN.clone()).unwrap(); + res.add_presort::(DUMMY_SPAN.clone()).unwrap(); res.add_primitive(ValueEq); @@ -61,16 +55,28 @@ impl Default for TypeInfo { } impl TypeInfo { - pub fn add_sort(&mut self, sort: S, span: Span) { - self.add_arcsort(Arc::new(sort), span).unwrap() + pub fn add_sort(&mut self, sort: S, span: Span) -> Result<(), TypeError> { + self.add_arcsort(Arc::new(sort), span) + } + + pub fn add_presort(&mut self, span: Span) -> Result<(), TypeError> { + let name = S::name(); + match self.presorts.entry(name) { + Entry::Occupied(_) => Err(TypeError::SortAlreadyBound(name, span)), + Entry::Vacant(e) => { + e.insert(S::make_sort); + self.presort_names.extend(S::presort_names()); + Ok(()) + } + } } pub fn add_arcsort(&mut self, sort: ArcSort, span: Span) -> Result<(), TypeError> { let name = sort.name(); match self.sorts.entry(name) { - hash_map::Entry::Occupied(_) => Err(TypeError::SortAlreadyBound(name, span)), - hash_map::Entry::Vacant(e) => { + Entry::Occupied(_) => Err(TypeError::SortAlreadyBound(name, span)), + Entry::Vacant(e) => { e.insert(sort.clone()); sort.register_primitives(self); Ok(()) From 5a6e17df56632be2fc756b5c0852772fc30a31cb Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Sat, 12 Oct 2024 15:09:02 -0700 Subject: [PATCH 05/12] Remove unused, undocumented macros --- src/sort/macros.rs | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/sort/macros.rs b/src/sort/macros.rs index 086c2045..bf4f41c6 100644 --- a/src/sort/macros.rs +++ b/src/sort/macros.rs @@ -1,28 +1,6 @@ -#[macro_export] -macro_rules! to_tt { - ($tt:tt, $callback:ident) => { - $callback!($tt) - }; -} - -#[macro_export] -macro_rules! unpack { - (& $t:ident) => { - $t - }; - ($t:ident) => { - $t - }; -} - -#[macro_export] macro_rules! add_primitives { - // ($egraph:expr, $($rest:tt)*) => { - // add_primitives!(@doubled $egraph, $($rest)*, $($rest)*) - // }; ($type_info:expr, $name:literal = |$($param:ident : $param_t:ty),*| -> $ret:ty { $body:expr } - // $name2:literal = |$($param2:ident : $(&)? $base_param_t:ident),*| -> $ret2:ty { $body2:expr } ) => {{ let type_info: &mut _ = $type_info; #[allow(unused_imports, non_snake_case)] From 6bbafdbc9358461fe9b621fda177226037fb57b3 Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Sat, 12 Oct 2024 15:28:03 -0700 Subject: [PATCH 06/12] Remove unconditional get_sort --- src/lib.rs | 20 ++++++-------------- src/sort/mod.rs | 2 ++ 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index e258eed4..c5e477c6 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1476,11 +1476,6 @@ impl EGraph { self.type_info.get_sort_by(pred) } - /// Returns a sort based on the type - pub fn get_sort(&self) -> Option> { - self.type_info.get_sort_by(|_| true) - } - /// Add a user-defined sort pub fn add_arcsort(&mut self, arcsort: ArcSort) -> Result<(), TypeError> { self.type_info.add_arcsort(arcsort, DUMMY_SPAN.clone()) @@ -1601,21 +1596,18 @@ mod tests { fn test_user_defined_primitive() { let mut egraph = EGraph::default(); egraph - .parse_and_run_program( - None, - " - (sort IntVec (Vec i64)) - ", - ) + .parse_and_run_program(None, "(sort IntVec (Vec i64))") .unwrap(); - let i64_sort: Arc = egraph.get_sort().unwrap(); + let int_vec_sort: Arc = egraph - .get_sort_by(|s: &Arc| s.element_name() == i64_sort.name()) + .get_sort_by(|s: &Arc| s.element_name() == I64Sort.name()) .unwrap(); + egraph.add_primitive(InnerProduct { - ele: i64_sort, + ele: I64Sort.into(), vec: int_vec_sort, }); + egraph .parse_and_run_program( None, diff --git a/src/sort/mod.rs b/src/sort/mod.rs index afa7c597..98748d84 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -31,7 +31,9 @@ use crate::*; pub trait Sort: Any + Send + Sync + Debug { fn name(&self) -> Symbol; + fn as_arc_any(self: Arc) -> Arc; + fn is_eq_sort(&self) -> bool { false } From 1af9f753ed4125f0d44f5782330b102b661bfedf Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Mon, 14 Oct 2024 22:55:12 -0700 Subject: [PATCH 07/12] Add comment to Presort --- src/sort/mod.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/sort/mod.rs b/src/sort/mod.rs index 98748d84..be772655 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -104,6 +104,10 @@ pub trait Sort: Any + Send + Sync + Debug { } } +// Note: this trait is currently intended to be implemented on the +// same struct as `Sort`. If in the future we have dynamic presorts +// (for example, we want to add partial application) we should revisit +// this and make the methods take a `self` parameter. pub trait Presort { fn name() -> Symbol; fn presort_names() -> Vec; From 62652c65aec98ba299a44c604a8865eb3d302ebb Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Mon, 14 Oct 2024 22:58:01 -0700 Subject: [PATCH 08/12] name -> presort_name, presort_names -> reserved_primitives --- src/sort/fn.rs | 4 ++-- src/sort/map.rs | 4 ++-- src/sort/mod.rs | 4 ++-- src/sort/set.rs | 4 ++-- src/sort/vec.rs | 4 ++-- src/typechecking.rs | 10 +++++----- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/sort/fn.rs b/src/sort/fn.rs index d95ebac0..05f42a92 100644 --- a/src/sort/fn.rs +++ b/src/sort/fn.rs @@ -61,11 +61,11 @@ impl FunctionSort { } impl Presort for FunctionSort { - fn name() -> Symbol { + fn presort_name() -> Symbol { "UnstableFn".into() } - fn presort_names() -> Vec { + fn reserved_primitives() -> Vec { vec!["unstable-fn".into(), "unstable-app".into()] } diff --git a/src/sort/map.rs b/src/sort/map.rs index db03c410..2c76ad55 100644 --- a/src/sort/map.rs +++ b/src/sort/map.rs @@ -26,11 +26,11 @@ impl MapSort { } impl Presort for MapSort { - fn name() -> Symbol { + fn presort_name() -> Symbol { "Map".into() } - fn presort_names() -> Vec { + fn reserved_primitives() -> Vec { vec![ "rebuild".into(), "map-empty".into(), diff --git a/src/sort/mod.rs b/src/sort/mod.rs index be772655..9f361cc4 100644 --- a/src/sort/mod.rs +++ b/src/sort/mod.rs @@ -109,8 +109,8 @@ pub trait Sort: Any + Send + Sync + Debug { // (for example, we want to add partial application) we should revisit // this and make the methods take a `self` parameter. pub trait Presort { - fn name() -> Symbol; - fn presort_names() -> Vec; + fn presort_name() -> Symbol; + fn reserved_primitives() -> Vec; fn make_sort( typeinfo: &mut TypeInfo, name: Symbol, diff --git a/src/sort/set.rs b/src/sort/set.rs index f7c68c58..e7265760 100644 --- a/src/sort/set.rs +++ b/src/sort/set.rs @@ -25,11 +25,11 @@ impl SetSort { } impl Presort for SetSort { - fn name() -> Symbol { + fn presort_name() -> Symbol { "Set".into() } - fn presort_names() -> Vec { + fn reserved_primitives() -> Vec { vec![ "set-of".into(), "set-empty".into(), diff --git a/src/sort/vec.rs b/src/sort/vec.rs index 2311c672..5072d180 100644 --- a/src/sort/vec.rs +++ b/src/sort/vec.rs @@ -24,11 +24,11 @@ impl VecSort { } impl Presort for VecSort { - fn name() -> Symbol { + fn presort_name() -> Symbol { "Vec".into() } - fn presort_names() -> Vec { + fn reserved_primitives() -> Vec { vec![ "vec-of".into(), "vec-append".into(), diff --git a/src/typechecking.rs b/src/typechecking.rs index 12d90e05..62db9d20 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -18,7 +18,7 @@ pub struct TypeInfo { // get the sort from the sorts name() pub presorts: HashMap, // TODO(yz): I want to get rid of this as now we have user-defined primitives and constraint based type checking - pub presort_names: HashSet, + pub reserved_primitives: HashSet, pub sorts: HashMap>, pub primitives: HashMap>, pub func_types: HashMap, @@ -29,7 +29,7 @@ impl Default for TypeInfo { fn default() -> Self { let mut res = Self { presorts: Default::default(), - presort_names: Default::default(), + reserved_primitives: Default::default(), sorts: Default::default(), primitives: Default::default(), func_types: Default::default(), @@ -60,12 +60,12 @@ impl TypeInfo { } pub fn add_presort(&mut self, span: Span) -> Result<(), TypeError> { - let name = S::name(); + let name = S::presort_name(); match self.presorts.entry(name) { Entry::Occupied(_) => Err(TypeError::SortAlreadyBound(name, span)), Entry::Vacant(e) => { e.insert(S::make_sort); - self.presort_names.extend(S::presort_names()); + self.reserved_primitives.extend(S::reserved_primitives()); Ok(()) } } @@ -466,7 +466,7 @@ impl TypeInfo { } pub(crate) fn is_primitive(&self, sym: Symbol) -> bool { - self.primitives.contains_key(&sym) || self.presort_names.contains(&sym) + self.primitives.contains_key(&sym) || self.reserved_primitives.contains(&sym) } pub(crate) fn lookup_user_func(&self, sym: Symbol) -> Option { From 566ef8cc243eb501cbdc71c1c350537562217805 Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Tue, 15 Oct 2024 11:10:17 -0700 Subject: [PATCH 09/12] Add doc comment for add_presort --- src/typechecking.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/typechecking.rs b/src/typechecking.rs index 62db9d20..80f0e464 100644 --- a/src/typechecking.rs +++ b/src/typechecking.rs @@ -59,6 +59,7 @@ impl TypeInfo { self.add_arcsort(Arc::new(sort), span) } + /// Adds a sort constructor to the typechecker's known set of types. pub fn add_presort(&mut self, span: Span) -> Result<(), TypeError> { let name = S::presort_name(); match self.presorts.entry(name) { From 09f33921d07aea712c6a628a92237728c49ecbc6 Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Tue, 15 Oct 2024 20:12:28 -0700 Subject: [PATCH 10/12] Try caching I64Sort Symbol --- src/sort/i64.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/sort/i64.rs b/src/sort/i64.rs index 0e9ef1e7..46e60c36 100644 --- a/src/sort/i64.rs +++ b/src/sort/i64.rs @@ -5,9 +5,13 @@ use super::*; #[derive(Debug)] pub struct I64Sort; +lazy_static! { + static ref I64_SORT_NAME: Symbol = "i64".into(); +} + impl Sort for I64Sort { fn name(&self) -> Symbol { - "i64".into() + *I64_SORT_NAME } fn as_arc_any(self: Arc) -> Arc { @@ -77,9 +81,9 @@ impl Sort for I64Sort { impl IntoSort for i64 { type Sort = I64Sort; - fn store(self, sort: &Self::Sort) -> Option { + fn store(self, _sort: &Self::Sort) -> Option { Some(Value { - tag: sort.name(), + tag: *I64_SORT_NAME, bits: self as u64, }) } From f04694a33d65316e666d3fc74b7473c2e841841e Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Tue, 15 Oct 2024 20:35:50 -0700 Subject: [PATCH 11/12] More sort name performance testing --- src/sort/i64.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sort/i64.rs b/src/sort/i64.rs index 46e60c36..9ee57c64 100644 --- a/src/sort/i64.rs +++ b/src/sort/i64.rs @@ -81,9 +81,9 @@ impl Sort for I64Sort { impl IntoSort for i64 { type Sort = I64Sort; - fn store(self, _sort: &Self::Sort) -> Option { + fn store(self, sort: &Self::Sort) -> Option { Some(Value { - tag: *I64_SORT_NAME, + tag: sort.name(), bits: self as u64, }) } From 8ae1427f67040e833526495678fa91351a17af00 Mon Sep 17 00:00:00 2001 From: Alex Fischman Date: Tue, 15 Oct 2024 20:52:24 -0700 Subject: [PATCH 12/12] Also cache names of other builtin sorts --- src/sort/bool.rs | 6 +++++- src/sort/f64.rs | 6 +++++- src/sort/rational.rs | 3 ++- src/sort/string.rs | 6 +++++- src/sort/unit.rs | 6 +++++- 5 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/sort/bool.rs b/src/sort/bool.rs index 87d5e824..1de0a55c 100644 --- a/src/sort/bool.rs +++ b/src/sort/bool.rs @@ -5,9 +5,13 @@ use super::*; #[derive(Debug)] pub struct BoolSort; +lazy_static! { + static ref BOOL_SORT_NAME: Symbol = "bool".into(); +} + impl Sort for BoolSort { fn name(&self) -> Symbol { - "bool".into() + *BOOL_SORT_NAME } fn as_arc_any(self: Arc) -> Arc { diff --git a/src/sort/f64.rs b/src/sort/f64.rs index d02915e0..6ed90a27 100755 --- a/src/sort/f64.rs +++ b/src/sort/f64.rs @@ -5,9 +5,13 @@ use ordered_float::OrderedFloat; #[derive(Debug)] pub struct F64Sort; +lazy_static! { + static ref F64_SORT_NAME: Symbol = "f64".into(); +} + impl Sort for F64Sort { fn name(&self) -> Symbol { - "f64".into() + *F64_SORT_NAME } fn as_arc_any(self: Arc) -> Arc { diff --git a/src/sort/rational.rs b/src/sort/rational.rs index 1508faab..f897ac86 100644 --- a/src/sort/rational.rs +++ b/src/sort/rational.rs @@ -8,6 +8,7 @@ use crate::{ast::Literal, util::IndexSet}; use super::*; lazy_static! { + static ref RATIONAL_SORT_NAME: Symbol = "Rational".into(); static ref RATS: Mutex> = Default::default(); } @@ -16,7 +17,7 @@ pub struct RationalSort; impl Sort for RationalSort { fn name(&self) -> Symbol { - "Rational".into() + *RATIONAL_SORT_NAME } fn as_arc_any(self: Arc) -> Arc { diff --git a/src/sort/string.rs b/src/sort/string.rs index 75530348..3cd6672f 100644 --- a/src/sort/string.rs +++ b/src/sort/string.rs @@ -7,9 +7,13 @@ use super::*; #[derive(Debug)] pub struct StringSort; +lazy_static! { + static ref STRING_SORT_NAME: Symbol = "String".into(); +} + impl Sort for StringSort { fn name(&self) -> Symbol { - "String".into() + *STRING_SORT_NAME } fn as_arc_any(self: Arc) -> Arc { diff --git a/src/sort/unit.rs b/src/sort/unit.rs index be8c2892..9f702cb9 100644 --- a/src/sort/unit.rs +++ b/src/sort/unit.rs @@ -4,9 +4,13 @@ use crate::{ast::Literal, constraint::AllEqualTypeConstraint, ArcSort, Primitive #[derive(Debug)] pub struct UnitSort; +lazy_static! { + static ref UNIT_SORT_NAME: Symbol = "Unit".into(); +} + impl Sort for UnitSort { fn name(&self) -> Symbol { - "Unit".into() + *UNIT_SORT_NAME } fn as_arc_any(self: Arc) -> Arc {