add costing capability for builtins
Co-authored-by: rvcas <x@rvcas.dev>
This commit is contained in:
parent
84df3be139
commit
9f977f7e58
|
@ -196,7 +196,10 @@ impl Machine {
|
||||||
fn force_evaluate(&mut self, value: Value) -> Result<Term<NamedDeBruijn>, Error> {
|
fn force_evaluate(&mut self, value: Value) -> Result<Term<NamedDeBruijn>, Error> {
|
||||||
match value {
|
match value {
|
||||||
Value::Delay(body) => self.compute(&body),
|
Value::Delay(body) => self.compute(&body),
|
||||||
Value::Builtin { .. } => todo!(),
|
Value::Builtin { fun, term, runtime } => {
|
||||||
|
let force_term = Term::Force(Box::new(term));
|
||||||
|
todo!()
|
||||||
|
}
|
||||||
rest => Err(Error::NonPolymorphicInstantiation(rest)),
|
rest => Err(Error::NonPolymorphicInstantiation(rest)),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -244,7 +247,9 @@ impl Machine {
|
||||||
runtime: BuiltinRuntime,
|
runtime: BuiltinRuntime,
|
||||||
) -> Result<Value, Error> {
|
) -> Result<Value, Error> {
|
||||||
if runtime.is_ready() {
|
if runtime.is_ready() {
|
||||||
self.spend_budget(todo!())?;
|
let cost = runtime.to_ex_budget(&self.costs.builtin_costs);
|
||||||
|
|
||||||
|
self.spend_budget(cost)?;
|
||||||
|
|
||||||
runtime.call()
|
runtime.call()
|
||||||
} else {
|
} else {
|
||||||
|
@ -335,4 +340,13 @@ impl Value {
|
||||||
pub fn is_integer(&self) -> bool {
|
pub fn is_integer(&self) -> bool {
|
||||||
matches!(self, Value::Con(Constant::Integer(_)))
|
matches!(self, Value::Con(Constant::Integer(_)))
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn to_ex_mem(&self) -> i32 {
|
||||||
|
match self {
|
||||||
|
Value::Con(_) => todo!(),
|
||||||
|
Value::Delay(_) => 1,
|
||||||
|
Value::Lambda { .. } => 1,
|
||||||
|
Value::Builtin { .. } => 1,
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,3 +1,7 @@
|
||||||
|
use crate::builtins::DefaultFunction;
|
||||||
|
|
||||||
|
use super::Value;
|
||||||
|
|
||||||
/// Can be negative
|
/// Can be negative
|
||||||
#[derive(Debug, Clone, PartialEq, Copy, Default)]
|
#[derive(Debug, Clone, PartialEq, Copy, Default)]
|
||||||
pub struct ExBudget {
|
pub struct ExBudget {
|
||||||
|
@ -154,7 +158,7 @@ impl Default for BuiltinCosts {
|
||||||
fn default() -> Self {
|
fn default() -> Self {
|
||||||
Self {
|
Self {
|
||||||
add_integer: CostingFun {
|
add_integer: CostingFun {
|
||||||
memory: TwoArguments::MaxSize(MaxSize {
|
mem: TwoArguments::MaxSize(MaxSize {
|
||||||
intercept: 1,
|
intercept: 1,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
}),
|
}),
|
||||||
|
@ -164,7 +168,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
subtract_integer: CostingFun {
|
subtract_integer: CostingFun {
|
||||||
memory: TwoArguments::MaxSize(MaxSize {
|
mem: TwoArguments::MaxSize(MaxSize {
|
||||||
intercept: 1,
|
intercept: 1,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
}),
|
}),
|
||||||
|
@ -174,7 +178,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
multiply_integer: CostingFun {
|
multiply_integer: CostingFun {
|
||||||
memory: TwoArguments::AddedSizes(AddedSizes {
|
mem: TwoArguments::AddedSizes(AddedSizes {
|
||||||
intercept: 0,
|
intercept: 0,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
}),
|
}),
|
||||||
|
@ -185,7 +189,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
divide_integer: CostingFun {
|
divide_integer: CostingFun {
|
||||||
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
mem: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
intercept: 0,
|
intercept: 0,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
minimum: 1,
|
minimum: 1,
|
||||||
|
@ -199,7 +203,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
quotient_integer: CostingFun {
|
quotient_integer: CostingFun {
|
||||||
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
mem: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
intercept: 0,
|
intercept: 0,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
minimum: 1,
|
minimum: 1,
|
||||||
|
@ -213,7 +217,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
remainder_integer: CostingFun {
|
remainder_integer: CostingFun {
|
||||||
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
mem: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
intercept: 0,
|
intercept: 0,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
minimum: 1,
|
minimum: 1,
|
||||||
|
@ -227,7 +231,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
mod_integer: CostingFun {
|
mod_integer: CostingFun {
|
||||||
memory: TwoArguments::SubtractedSizes(SubtractedSizes {
|
mem: TwoArguments::SubtractedSizes(SubtractedSizes {
|
||||||
intercept: 0,
|
intercept: 0,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
minimum: 1,
|
minimum: 1,
|
||||||
|
@ -241,28 +245,28 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
equals_integer: CostingFun {
|
equals_integer: CostingFun {
|
||||||
memory: TwoArguments::ConstantCost(1),
|
mem: TwoArguments::ConstantCost(1),
|
||||||
cpu: TwoArguments::MinSize(MinSize {
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
intercept: 208512,
|
intercept: 208512,
|
||||||
slope: 421,
|
slope: 421,
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
less_than_integer: CostingFun {
|
less_than_integer: CostingFun {
|
||||||
memory: TwoArguments::ConstantCost(1),
|
mem: TwoArguments::ConstantCost(1),
|
||||||
cpu: TwoArguments::MinSize(MinSize {
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
intercept: 208896,
|
intercept: 208896,
|
||||||
slope: 511,
|
slope: 511,
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
less_than_equals_integer: CostingFun {
|
less_than_equals_integer: CostingFun {
|
||||||
memory: TwoArguments::ConstantCost(1),
|
mem: TwoArguments::ConstantCost(1),
|
||||||
cpu: TwoArguments::MinSize(MinSize {
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
intercept: 204924,
|
intercept: 204924,
|
||||||
slope: 473,
|
slope: 473,
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
append_byte_string: CostingFun {
|
append_byte_string: CostingFun {
|
||||||
memory: TwoArguments::AddedSizes(AddedSizes {
|
mem: TwoArguments::AddedSizes(AddedSizes {
|
||||||
intercept: 1000,
|
intercept: 1000,
|
||||||
slope: 571,
|
slope: 571,
|
||||||
}),
|
}),
|
||||||
|
@ -272,7 +276,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
cons_byte_string: CostingFun {
|
cons_byte_string: CostingFun {
|
||||||
memory: TwoArguments::AddedSizes(AddedSizes {
|
mem: TwoArguments::AddedSizes(AddedSizes {
|
||||||
intercept: 0,
|
intercept: 0,
|
||||||
slope: 1,
|
slope: 1,
|
||||||
}),
|
}),
|
||||||
|
@ -282,7 +286,7 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
slice_byte_string: CostingFun {
|
slice_byte_string: CostingFun {
|
||||||
memory: ThreeArguments::LinearInZ(LinearSize {
|
mem: ThreeArguments::LinearInZ(LinearSize {
|
||||||
intercept: 4,
|
intercept: 4,
|
||||||
slope: 0,
|
slope: 0,
|
||||||
}),
|
}),
|
||||||
|
@ -292,15 +296,15 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
length_of_byte_string: CostingFun {
|
length_of_byte_string: CostingFun {
|
||||||
memory: OneArgument::ConstantCost(10),
|
mem: OneArgument::ConstantCost(10),
|
||||||
cpu: OneArgument::ConstantCost(1000),
|
cpu: OneArgument::ConstantCost(1000),
|
||||||
},
|
},
|
||||||
index_byte_string: CostingFun {
|
index_byte_string: CostingFun {
|
||||||
memory: TwoArguments::ConstantCost(4),
|
mem: TwoArguments::ConstantCost(4),
|
||||||
cpu: TwoArguments::ConstantCost(57667),
|
cpu: TwoArguments::ConstantCost(57667),
|
||||||
},
|
},
|
||||||
equals_byte_string: CostingFun {
|
equals_byte_string: CostingFun {
|
||||||
memory: TwoArguments::ConstantCost(1),
|
mem: TwoArguments::ConstantCost(1),
|
||||||
cpu: TwoArguments::LinearOnDiagonal(ConstantOrLinear {
|
cpu: TwoArguments::LinearOnDiagonal(ConstantOrLinear {
|
||||||
constant: 245000,
|
constant: 245000,
|
||||||
intercept: 216773,
|
intercept: 216773,
|
||||||
|
@ -308,176 +312,255 @@ impl Default for BuiltinCosts {
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
less_than_byte_string: CostingFun {
|
less_than_byte_string: CostingFun {
|
||||||
memory: TwoArguments::ConstantCost(1),
|
mem: TwoArguments::ConstantCost(1),
|
||||||
cpu: TwoArguments::MinSize(MinSize {
|
cpu: TwoArguments::MinSize(MinSize {
|
||||||
intercept: 197145,
|
intercept: 197145,
|
||||||
slope: 156,
|
slope: 156,
|
||||||
}),
|
}),
|
||||||
},
|
},
|
||||||
less_than_equals_byte_string: CostingFun {
|
less_than_equals_byte_string: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
sha2_256: CostingFun {
|
sha2_256: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
sha3_256: CostingFun {
|
sha3_256: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
blake2b_256: CostingFun {
|
blake2b_256: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
verify_ed25519_signature: CostingFun {
|
verify_ed25519_signature: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
verify_ecdsa_secp256k1_signature: CostingFun {
|
verify_ecdsa_secp256k1_signature: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
verify_schnorr_secp256k1_signature: CostingFun {
|
verify_schnorr_secp256k1_signature: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
append_string: CostingFun {
|
append_string: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
equals_string: CostingFun {
|
equals_string: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
encode_utf8: CostingFun {
|
encode_utf8: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
decode_utf8: CostingFun {
|
decode_utf8: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
if_then_else: CostingFun {
|
if_then_else: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
choose_unit: CostingFun {
|
choose_unit: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
trace: CostingFun {
|
trace: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
fst_pair: CostingFun {
|
fst_pair: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
snd_pair: CostingFun {
|
snd_pair: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
choose_list: CostingFun {
|
choose_list: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
mk_cons: CostingFun {
|
mk_cons: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
head_list: CostingFun {
|
head_list: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
tail_list: CostingFun {
|
tail_list: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
null_list: CostingFun {
|
null_list: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
choose_data: CostingFun {
|
choose_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
constr_data: CostingFun {
|
constr_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
map_data: CostingFun {
|
map_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
list_data: CostingFun {
|
list_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
i_data: CostingFun {
|
i_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
b_data: CostingFun {
|
b_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
un_constr_data: CostingFun {
|
un_constr_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
un_map_data: CostingFun {
|
un_map_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
un_list_data: CostingFun {
|
un_list_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
un_i_data: CostingFun {
|
un_i_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
un_b_data: CostingFun {
|
un_b_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
equals_data: CostingFun {
|
equals_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
mk_pair_data: CostingFun {
|
mk_pair_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
mk_nil_data: CostingFun {
|
mk_nil_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
mk_nil_pair_data: CostingFun {
|
mk_nil_pair_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
serialise_data: CostingFun {
|
serialise_data: CostingFun {
|
||||||
memory: todo!(),
|
mem: todo!(),
|
||||||
cpu: todo!(),
|
cpu: todo!(),
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl BuiltinCosts {
|
||||||
|
pub fn to_ex_budget(&self, fun: DefaultFunction, args: &[Value]) -> ExBudget {
|
||||||
|
match fun {
|
||||||
|
DefaultFunction::AddInteger => ExBudget {
|
||||||
|
mem: self
|
||||||
|
.add_integer
|
||||||
|
.mem
|
||||||
|
.cost(args[0].to_ex_mem(), args[1].to_ex_mem()),
|
||||||
|
cpu: self
|
||||||
|
.add_integer
|
||||||
|
.cpu
|
||||||
|
.cost(args[0].to_ex_mem(), args[1].to_ex_mem()),
|
||||||
|
},
|
||||||
|
DefaultFunction::SubtractInteger => todo!(),
|
||||||
|
DefaultFunction::MultiplyInteger => todo!(),
|
||||||
|
DefaultFunction::DivideInteger => todo!(),
|
||||||
|
DefaultFunction::QuotientInteger => todo!(),
|
||||||
|
DefaultFunction::RemainderInteger => todo!(),
|
||||||
|
DefaultFunction::ModInteger => todo!(),
|
||||||
|
DefaultFunction::EqualsInteger => todo!(),
|
||||||
|
DefaultFunction::LessThanInteger => todo!(),
|
||||||
|
DefaultFunction::LessThanEqualsInteger => todo!(),
|
||||||
|
DefaultFunction::AppendByteString => todo!(),
|
||||||
|
DefaultFunction::ConsByteString => todo!(),
|
||||||
|
DefaultFunction::SliceByteString => todo!(),
|
||||||
|
DefaultFunction::LengthOfByteString => todo!(),
|
||||||
|
DefaultFunction::IndexByteString => todo!(),
|
||||||
|
DefaultFunction::EqualsByteString => todo!(),
|
||||||
|
DefaultFunction::LessThanByteString => todo!(),
|
||||||
|
DefaultFunction::LessThanEqualsByteString => todo!(),
|
||||||
|
DefaultFunction::Sha2_256 => todo!(),
|
||||||
|
DefaultFunction::Sha3_256 => todo!(),
|
||||||
|
DefaultFunction::Blake2b_256 => todo!(),
|
||||||
|
DefaultFunction::VerifySignature => todo!(),
|
||||||
|
DefaultFunction::VerifyEcdsaSecp256k1Signature => todo!(),
|
||||||
|
DefaultFunction::VerifySchnorrSecp256k1Signature => todo!(),
|
||||||
|
DefaultFunction::AppendString => todo!(),
|
||||||
|
DefaultFunction::EqualsString => todo!(),
|
||||||
|
DefaultFunction::EncodeUtf8 => todo!(),
|
||||||
|
DefaultFunction::DecodeUtf8 => todo!(),
|
||||||
|
DefaultFunction::IfThenElse => todo!(),
|
||||||
|
DefaultFunction::ChooseUnit => todo!(),
|
||||||
|
DefaultFunction::Trace => todo!(),
|
||||||
|
DefaultFunction::FstPair => todo!(),
|
||||||
|
DefaultFunction::SndPair => todo!(),
|
||||||
|
DefaultFunction::ChooseList => todo!(),
|
||||||
|
DefaultFunction::MkCons => todo!(),
|
||||||
|
DefaultFunction::HeadList => todo!(),
|
||||||
|
DefaultFunction::TailList => todo!(),
|
||||||
|
DefaultFunction::NullList => todo!(),
|
||||||
|
DefaultFunction::ChooseData => todo!(),
|
||||||
|
DefaultFunction::ConstrData => todo!(),
|
||||||
|
DefaultFunction::MapData => todo!(),
|
||||||
|
DefaultFunction::ListData => todo!(),
|
||||||
|
DefaultFunction::IData => todo!(),
|
||||||
|
DefaultFunction::BData => todo!(),
|
||||||
|
DefaultFunction::UnConstrData => todo!(),
|
||||||
|
DefaultFunction::UnMapData => todo!(),
|
||||||
|
DefaultFunction::UnListData => todo!(),
|
||||||
|
DefaultFunction::UnIData => todo!(),
|
||||||
|
DefaultFunction::UnBData => todo!(),
|
||||||
|
DefaultFunction::EqualsData => todo!(),
|
||||||
|
DefaultFunction::SerialiseData => todo!(),
|
||||||
|
DefaultFunction::MkPairData => todo!(),
|
||||||
|
DefaultFunction::MkNilData => todo!(),
|
||||||
|
DefaultFunction::MkNilPairData => todo!(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub struct CostingFun<T> {
|
pub struct CostingFun<T> {
|
||||||
pub memory: T,
|
pub mem: T,
|
||||||
pub cpu: T,
|
pub cpu: T,
|
||||||
}
|
}
|
||||||
|
|
||||||
pub enum OneArgument {
|
pub enum OneArgument {
|
||||||
ConstantCost(isize),
|
ConstantCost(i32),
|
||||||
LinearCost(LinearSize),
|
LinearCost(LinearSize),
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl OneArgument {
|
||||||
|
pub fn cost(&self, x: i32) -> i32 {
|
||||||
|
match self {
|
||||||
|
OneArgument::ConstantCost(c) => *c,
|
||||||
|
OneArgument::LinearCost(m) => m.slope * x + m.intercept,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
#[derive(Clone)]
|
||||||
pub enum TwoArguments {
|
pub enum TwoArguments {
|
||||||
ConstantCost(isize),
|
ConstantCost(i32),
|
||||||
LinearInX(LinearSize),
|
LinearInX(LinearSize),
|
||||||
LinearInY(LinearSize),
|
LinearInY(LinearSize),
|
||||||
AddedSizes(AddedSizes),
|
AddedSizes(AddedSizes),
|
||||||
|
@ -489,58 +572,123 @@ pub enum TwoArguments {
|
||||||
ConstAboveDiagonal(ConstantOrTwoArguments),
|
ConstAboveDiagonal(ConstantOrTwoArguments),
|
||||||
ConstBelowDiagonal(ConstantOrTwoArguments),
|
ConstBelowDiagonal(ConstantOrTwoArguments),
|
||||||
}
|
}
|
||||||
|
impl TwoArguments {
|
||||||
|
pub fn cost(&self, x: i32, y: i32) -> i32 {
|
||||||
|
match self {
|
||||||
|
TwoArguments::ConstantCost(c) => *c,
|
||||||
|
TwoArguments::LinearInX(l) => l.slope * x + l.intercept,
|
||||||
|
TwoArguments::LinearInY(l) => l.slope * y + l.intercept,
|
||||||
|
TwoArguments::AddedSizes(s) => s.slope * (x + y) + s.intercept,
|
||||||
|
TwoArguments::SubtractedSizes(s) => s.slope * s.minimum.min(x - y) + s.intercept,
|
||||||
|
TwoArguments::MultipliedSizes(s) => s.slope * (x * y) + s.intercept,
|
||||||
|
TwoArguments::MinSize(s) => s.slope * x.min(y) + s.intercept,
|
||||||
|
TwoArguments::MaxSize(s) => s.slope * x.max(y) + s.intercept,
|
||||||
|
TwoArguments::LinearOnDiagonal(l) => {
|
||||||
|
if x == y {
|
||||||
|
x * l.slope + l.intercept
|
||||||
|
} else {
|
||||||
|
l.constant
|
||||||
|
}
|
||||||
|
}
|
||||||
|
TwoArguments::ConstAboveDiagonal(l) => {
|
||||||
|
if x > y {
|
||||||
|
l.constant
|
||||||
|
} else {
|
||||||
|
let p = *l.model.clone();
|
||||||
|
p.cost(x, y)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
TwoArguments::ConstBelowDiagonal(l) => {
|
||||||
|
if x < y {
|
||||||
|
l.constant
|
||||||
|
} else {
|
||||||
|
let p = *l.model.clone();
|
||||||
|
p.cost(x, y)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub enum ThreeArguments {
|
pub enum ThreeArguments {
|
||||||
ConstantCost(isize),
|
ConstantCost(i32),
|
||||||
AddedSizes(AddedSizes),
|
AddedSizes(AddedSizes),
|
||||||
LinearInX(LinearSize),
|
LinearInX(LinearSize),
|
||||||
LinearInY(LinearSize),
|
LinearInY(LinearSize),
|
||||||
LinearInZ(LinearSize),
|
LinearInZ(LinearSize),
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl ThreeArguments {
|
||||||
|
pub fn cost(&self, x: i32, y: i32, z: i32) -> i32 {
|
||||||
|
match self {
|
||||||
|
ThreeArguments::ConstantCost(c) => *c,
|
||||||
|
ThreeArguments::AddedSizes(s) => (x + y + z) * s.slope + s.intercept,
|
||||||
|
ThreeArguments::LinearInX(l) => x * l.slope + l.intercept,
|
||||||
|
ThreeArguments::LinearInY(l) => y * l.slope + l.intercept,
|
||||||
|
ThreeArguments::LinearInZ(l) => z * l.slope + l.intercept,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
pub enum SixArguments {
|
pub enum SixArguments {
|
||||||
ConstantCost(isize),
|
ConstantCost(i32),
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl SixArguments {
|
||||||
|
pub fn cost(&self, _: i32, _: i32, _: i32, _: i32, _: i32, _: i32) -> i32 {
|
||||||
|
match self {
|
||||||
|
SixArguments::ConstantCost(c) => *c,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct LinearSize {
|
pub struct LinearSize {
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct AddedSizes {
|
pub struct AddedSizes {
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct SubtractedSizes {
|
pub struct SubtractedSizes {
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
pub minimum: isize,
|
pub minimum: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct MultipliedSizes {
|
pub struct MultipliedSizes {
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct MinSize {
|
pub struct MinSize {
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct MaxSize {
|
pub struct MaxSize {
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct ConstantOrLinear {
|
pub struct ConstantOrLinear {
|
||||||
pub constant: isize,
|
pub constant: i32,
|
||||||
pub intercept: isize,
|
pub intercept: i32,
|
||||||
pub slope: isize,
|
pub slope: i32,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
pub struct ConstantOrTwoArguments {
|
pub struct ConstantOrTwoArguments {
|
||||||
pub constant: isize,
|
pub constant: i32,
|
||||||
pub model: Box<TwoArguments>,
|
pub model: Box<TwoArguments>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use crate::{ast::Constant, builtins::DefaultFunction};
|
use crate::{ast::Constant, builtins::DefaultFunction};
|
||||||
|
|
||||||
use super::{
|
use super::{
|
||||||
|
cost_model::{BuiltinCosts, ExBudget},
|
||||||
// cost_model::{CostingFun, ExBudget},
|
// cost_model::{CostingFun, ExBudget},
|
||||||
Error,
|
Error,
|
||||||
Value,
|
Value,
|
||||||
|
@ -20,23 +21,15 @@ use super::{
|
||||||
|
|
||||||
#[derive(Clone, Debug)]
|
#[derive(Clone, Debug)]
|
||||||
pub struct BuiltinRuntime {
|
pub struct BuiltinRuntime {
|
||||||
meaning: BuiltinMeaning,
|
|
||||||
// budget: fn(Vec<u32>) -> ExBudget,
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Clone, Debug)]
|
|
||||||
struct BuiltinMeaning {
|
|
||||||
args: Vec<Value>,
|
args: Vec<Value>,
|
||||||
fun: DefaultFunction,
|
fun: DefaultFunction,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl BuiltinMeaning {
|
impl BuiltinRuntime {
|
||||||
pub fn new(fun: DefaultFunction) -> BuiltinMeaning {
|
pub fn new(fun: DefaultFunction) -> BuiltinRuntime {
|
||||||
Self { args: vec![], fun }
|
Self { args: vec![], fun }
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
impl BuiltinRuntime {
|
|
||||||
// fn from_builtin_runtime_options<G>(
|
// fn from_builtin_runtime_options<G>(
|
||||||
// eval_mode: EvalMode,
|
// eval_mode: EvalMode,
|
||||||
// cost: CostingFun<G>,
|
// cost: CostingFun<G>,
|
||||||
|
@ -48,37 +41,33 @@ impl BuiltinRuntime {
|
||||||
// }
|
// }
|
||||||
|
|
||||||
pub fn is_arrow(&self) -> bool {
|
pub fn is_arrow(&self) -> bool {
|
||||||
self.meaning.args.len() != self.meaning.fun.arity()
|
self.args.len() != self.fun.arity()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn is_ready(&self) -> bool {
|
pub fn is_ready(&self) -> bool {
|
||||||
self.meaning.args.len() == self.meaning.fun.arity()
|
self.args.len() == self.fun.arity()
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn call(&self) -> Result<Value, Error> {
|
pub fn call(&self) -> Result<Value, Error> {
|
||||||
self.meaning.fun.call(&self.meaning.args)
|
self.fun.call(&self.args)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn push(&mut self, arg: Value) -> Result<(), Error> {
|
pub fn push(&mut self, arg: Value) -> Result<(), Error> {
|
||||||
self.meaning.fun.check_type(&arg)?;
|
self.fun.check_type(&arg)?;
|
||||||
|
|
||||||
self.meaning.args.push(arg);
|
self.args.push(arg);
|
||||||
|
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
impl From<DefaultFunction> for BuiltinMeaning {
|
pub fn to_ex_budget(&self, costs: &BuiltinCosts) -> ExBudget {
|
||||||
fn from(fun: DefaultFunction) -> Self {
|
costs.to_ex_budget(self.fun, &self.args)
|
||||||
BuiltinMeaning::new(fun)
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl From<DefaultFunction> for BuiltinRuntime {
|
impl From<DefaultFunction> for BuiltinRuntime {
|
||||||
fn from(fun: DefaultFunction) -> Self {
|
fn from(fun: DefaultFunction) -> Self {
|
||||||
BuiltinRuntime {
|
BuiltinRuntime::new(fun)
|
||||||
meaning: fun.into(),
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue