Implement TraceIfFalse type-checking and AST transformation.

This caused me some trouble. In my first approach, I ended up having
  multiple traces because nested values would be evaluated twice; once
  as condition, and once as part of the continuation.

  To prevent this, we can simply evaluate the condition once, and return
  plain True / False boolean as outcome. So this effectively transforms any
  expression:

  ```
  expr
  ```

  as

  ```
  if expr { True } else { trace("...", False) }
  ```
This commit is contained in:
KtorZ 2023-02-16 13:53:05 +01:00 committed by Lucas
parent 6a50bde666
commit e9e3f4f50a
6 changed files with 130 additions and 23 deletions

View File

@ -1017,6 +1017,12 @@ pub enum TraceKind {
Error,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Tracing {
NoTraces,
KeepTraces,
}
#[derive(Copy, Clone, PartialEq, Eq)]
pub struct Span {
pub start: usize,

View File

@ -1,5 +1,5 @@
use crate::{
ast::{ModuleKind, TypedModule, UntypedModule},
ast::{ModuleKind, Tracing, TypedModule, UntypedModule},
builtins, parser,
tipo::error::{Error, Warning},
IdGenerator,
@ -24,7 +24,14 @@ fn check_module(
module_types.insert("aiken".to_string(), builtins::prelude(&id_gen));
module_types.insert("aiken/builtin".to_string(), builtins::plutus(&id_gen));
let result = ast.infer(&id_gen, kind, "test/project", &module_types, &mut warnings);
let result = ast.infer(
&id_gen,
kind,
"test/project",
&module_types,
Tracing::KeepTraces,
&mut warnings,
);
result
.map(|o| (warnings.clone(), o))

View File

@ -5,13 +5,14 @@ use vec1::Vec1;
use crate::{
ast::{
Annotation, Arg, ArgName, AssignmentKind, BinOp, CallArg, Clause, ClauseGuard, Constant,
RecordUpdateSpread, Span, TraceKind, TypedArg, TypedCallArg, TypedClause, TypedClauseGuard,
TypedConstant, TypedIfBranch, TypedMultiPattern, TypedRecordUpdateArg, UnOp, UntypedArg,
UntypedClause, UntypedClauseGuard, UntypedConstant, UntypedIfBranch, UntypedMultiPattern,
UntypedPattern, UntypedRecordUpdateArg,
IfBranch, RecordUpdateSpread, Span, TraceKind, Tracing, TypedArg, TypedCallArg,
TypedClause, TypedClauseGuard, TypedConstant, TypedIfBranch, TypedMultiPattern,
TypedRecordUpdateArg, UnOp, UntypedArg, UntypedClause, UntypedClauseGuard, UntypedConstant,
UntypedIfBranch, UntypedMultiPattern, UntypedPattern, UntypedRecordUpdateArg,
},
builtins::{bool, byte_array, function, int, list, string, tuple},
expr::{TypedExpr, UntypedExpr},
format,
tipo::fields::FieldMap,
};
@ -29,6 +30,10 @@ use super::{
pub(crate) struct ExprTyper<'a, 'b> {
pub(crate) environment: &'a mut Environment<'b>,
// We tweak the tracing behavior during type-check. Traces are either kept or left out of the
// typed AST depending on this setting.
pub(crate) tracing: Tracing,
// Type hydrator for creating types from annotations
pub(crate) hydrator: Hydrator,
@ -377,6 +382,78 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
}
}
fn infer_trace_if_false(
&mut self,
value: UntypedExpr,
location: Span,
) -> Result<TypedExpr, Error> {
let var_true = TypedExpr::Var {
location,
name: "True".to_string(),
constructor: ValueConstructor {
public: true,
variant: ValueConstructorVariant::Record {
name: "True".to_string(),
arity: 0,
field_map: None,
location: Span::empty(),
module: String::new(),
constructors_count: 2,
},
tipo: bool(),
},
};
let var_false = TypedExpr::Var {
location,
name: "False".to_string(),
constructor: ValueConstructor {
public: true,
variant: ValueConstructorVariant::Record {
name: "False".to_string(),
arity: 0,
field_map: None,
location: Span::empty(),
module: String::new(),
constructors_count: 2,
},
tipo: bool(),
},
};
let text = TypedExpr::String {
location,
tipo: string(),
value: format!(
"{} ? False",
format::Formatter::new().expr(&value).to_pretty_string(999)
),
};
let typed_value = self.infer(value)?;
self.unify(typed_value.tipo(), bool(), typed_value.location(), false)?;
match self.tracing {
Tracing::NoTraces => Ok(typed_value),
Tracing::KeepTraces => Ok(TypedExpr::If {
location,
branches: vec1::vec1![IfBranch {
condition: typed_value,
body: var_true,
location,
}],
final_else: Box::new(TypedExpr::Trace {
location,
tipo: bool(),
text: Box::new(text),
then: Box::new(var_false),
}),
tipo: bool(),
}),
}
}
fn infer_binop(
&mut self,
name: BinOp,
@ -1879,12 +1956,15 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
})
}
Ok(TypedExpr::Trace {
match self.tracing {
Tracing::NoTraces => Ok(then),
Tracing::KeepTraces => Ok(TypedExpr::Trace {
location,
tipo,
then: Box::new(then),
text: Box::new(text),
})
}),
}
}
fn infer_value_constructor(
@ -2058,7 +2138,7 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
self.environment.instantiate(t, ids, &self.hydrator)
}
pub fn new(environment: &'a mut Environment<'b>) -> Self {
pub fn new(environment: &'a mut Environment<'b>, tracing: Tracing) -> Self {
let mut hydrator = Hydrator::new();
hydrator.permit_holes(true);
@ -2066,6 +2146,7 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
Self {
hydrator,
environment,
tracing,
ungeneralised_function_used: false,
}
}

View File

@ -3,8 +3,8 @@ use std::collections::HashMap;
use crate::{
ast::{
DataType, Definition, Function, Layer, ModuleConstant, ModuleKind, RecordConstructor,
RecordConstructorArg, Span, TypeAlias, TypedDefinition, TypedModule, UntypedDefinition,
UntypedModule, Use, Validator,
RecordConstructorArg, Span, Tracing, TypeAlias, TypedDefinition, TypedModule,
UntypedDefinition, UntypedModule, Use, Validator,
},
builtins,
builtins::function,
@ -29,6 +29,7 @@ impl UntypedModule {
kind: ModuleKind,
package: &str,
modules: &HashMap<String, TypeInfo>,
tracing: Tracing,
warnings: &mut Vec<Warning>,
) -> Result<TypedModule, Error> {
let name = self.name.clone();
@ -83,7 +84,8 @@ impl UntypedModule {
}
for def in consts.into_iter().chain(not_consts) {
let definition = infer_definition(def, &name, &mut hydrators, &mut environment, kind)?;
let definition =
infer_definition(def, &name, &mut hydrators, &mut environment, tracing, kind)?;
definitions.push(definition);
}
@ -148,6 +150,7 @@ fn infer_definition(
module_name: &String,
hydrators: &mut HashMap<String, Hydrator>,
environment: &mut Environment<'_>,
tracing: Tracing,
kind: ModuleKind,
) -> Result<TypedDefinition, Error> {
match def {
@ -192,7 +195,7 @@ fn infer_definition(
.map(|(arg_name, tipo)| arg_name.set_type(tipo.clone()))
.collect();
let mut expr_typer = ExprTyper::new(environment);
let mut expr_typer = ExprTyper::new(environment, tracing);
expr_typer.hydrator = hydrators
.remove(&name)
@ -266,6 +269,7 @@ fn infer_definition(
module_name,
hydrators,
environment,
tracing,
kind,
)? {
if !typed_fun.return_type.is_bool() {
@ -297,9 +301,14 @@ fn infer_definition(
}
Definition::Test(f) => {
if let Definition::Fn(f) =
infer_definition(Definition::Fn(f), module_name, hydrators, environment, kind)?
{
if let Definition::Fn(f) = infer_definition(
Definition::Fn(f),
module_name,
hydrators,
environment,
tracing,
kind,
)? {
environment.unify(f.return_type.clone(), builtins::bool(), f.location, false)?;
Ok(Definition::Test(f))
@ -505,7 +514,8 @@ fn infer_definition(
})
}
let typed_expr = ExprTyper::new(environment).infer_const(&annotation, *value)?;
let typed_expr =
ExprTyper::new(environment, tracing).infer_const(&annotation, *value)?;
let tipo = typed_expr.tipo();

View File

@ -177,7 +177,7 @@ mod test {
use crate::{module::ParsedModule, PackageName};
use aiken_lang::{
self,
ast::{ModuleKind, TypedDataType, TypedFunction},
ast::{ModuleKind, Tracing, TypedDataType, TypedFunction},
builder::{DataTypeKey, FunctionAccessKey},
builtins, parser,
tipo::TypeInfo,
@ -253,6 +253,7 @@ mod test {
module.kind,
&self.package.to_string(),
&self.module_types,
Tracing::NoTraces,
&mut warnings,
)
.expect("Failed to type-check module");

View File

@ -14,7 +14,7 @@ pub mod telemetry;
use crate::blueprint::{schema::Schema, Blueprint};
use aiken_lang::{
ast::{Definition, Function, ModuleKind, TypedDataType, TypedFunction},
ast::{Definition, Function, ModuleKind, Tracing, TypedDataType, TypedFunction},
builder::{DataTypeKey, FunctionAccessKey},
builtins,
tipo::TypeInfo,
@ -496,6 +496,8 @@ where
kind,
&self.config.name.to_string(),
&self.module_types,
// TODO: Make configurable
Tracing::KeepTraces,
&mut type_warnings,
)
.map_err(|error| Error::Type {