complete parser, but compile time is slow
This commit is contained in:
parent
6632e897ba
commit
3adf2ff723
6 changed files with 482 additions and 14 deletions
|
|
@ -17,6 +17,8 @@ pub mod signals;
|
|||
|
||||
use std::time::Duration;
|
||||
|
||||
pub use expr::*;
|
||||
pub use signals::Signal;
|
||||
use thiserror::Error;
|
||||
|
||||
/// Errors generated by all Argus components.
|
||||
|
|
|
|||
|
|
@ -3,7 +3,15 @@ name = "argus-parser"
|
|||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
[lib]
|
||||
name = "argus_parser"
|
||||
|
||||
[[bin]]
|
||||
name = "argus_parser"
|
||||
path = "src/main.rs"
|
||||
|
||||
|
||||
[dependencies]
|
||||
argus-core = { version = "0.1.0", path = "../argus-core" }
|
||||
ariadne = "0.3.0"
|
||||
chumsky = "1.0.0-alpha.4"
|
||||
chumsky = { version = "1.0.0-alpha.4", features = ["default", "label"] }
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ pub type Span = SimpleSpan<usize>;
|
|||
pub type Output<'a> = Vec<(Token<'a>, Span)>;
|
||||
pub type Error<'a> = extra::Err<Rich<'a, char, Span>>;
|
||||
|
||||
#[derive(Clone, Debug, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug, PartialEq)]
|
||||
pub enum Token<'src> {
|
||||
Semicolon,
|
||||
LBracket,
|
||||
|
|
@ -14,8 +14,11 @@ pub enum Token<'src> {
|
|||
LParen,
|
||||
RParen,
|
||||
Comma,
|
||||
DotDot,
|
||||
Bool(bool),
|
||||
Num(&'src str),
|
||||
Int(i64),
|
||||
UInt(u64),
|
||||
Float(f64),
|
||||
Ident(&'src str),
|
||||
Minus,
|
||||
Plus,
|
||||
|
|
@ -49,8 +52,11 @@ impl<'src> fmt::Display for Token<'src> {
|
|||
Token::LParen => write!(f, "("),
|
||||
Token::RParen => write!(f, ")"),
|
||||
Token::Comma => write!(f, ","),
|
||||
Token::DotDot => write!(f, ".."),
|
||||
Token::Bool(val) => write!(f, "{}", val),
|
||||
Token::Num(val) => write!(f, "{}", val),
|
||||
Token::Int(val) => write!(f, "{}", val),
|
||||
Token::UInt(val) => write!(f, "{}", val),
|
||||
Token::Float(val) => write!(f, "{}", val),
|
||||
Token::Ident(ident) => write!(f, "{}", ident),
|
||||
Token::Minus => write!(f, "-"),
|
||||
Token::Plus => write!(f, "+"),
|
||||
|
|
@ -85,14 +91,22 @@ pub fn lexer<'src>() -> impl Parser<'src, &'src str, Output<'src>, Error<'src>>
|
|||
|
||||
let exp = just('e').or(just('E')).then(one_of("+-").or_not()).then(digits);
|
||||
|
||||
let number = just('-')
|
||||
let floating_number = just('-')
|
||||
.or_not()
|
||||
.then(text::int(10))
|
||||
.then(digits)
|
||||
.then(frac.or_not())
|
||||
.then(exp.or_not())
|
||||
.map_slice(Token::Num)
|
||||
.map_slice(|s: &str| Token::Float(s.parse().unwrap()))
|
||||
.boxed();
|
||||
|
||||
let signed_int = one_of("+-")
|
||||
.or_not()
|
||||
.then(digits)
|
||||
.map_slice(|s: &str| Token::Int(s.parse().unwrap()));
|
||||
let unsigned_int = digits.map_slice(|s: &str| Token::UInt(s.parse().unwrap()));
|
||||
|
||||
let number = choice((floating_number, signed_int, unsigned_int));
|
||||
|
||||
// A parser for control characters (delimiters, semicolons, etc.)
|
||||
let ctrl = choice((
|
||||
just(";").to(Token::Semicolon),
|
||||
|
|
@ -101,6 +115,7 @@ pub fn lexer<'src>() -> impl Parser<'src, &'src str, Output<'src>, Error<'src>>
|
|||
just("(").to(Token::LParen),
|
||||
just(")").to(Token::RParen),
|
||||
just(",").to(Token::Comma),
|
||||
just("..").to(Token::DotDot),
|
||||
));
|
||||
|
||||
// Lexer for operator symbols
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
//! # Argus logic syntax
|
||||
#![allow(dead_code)]
|
||||
|
||||
mod lexer;
|
||||
mod parser;
|
||||
|
||||
pub use lexer::{lexer, Error as LexError, Span, Token};
|
||||
pub use parser::{parser, Expr, Interval};
|
||||
|
|
|
|||
54
argus-parser/src/main.rs
Normal file
54
argus-parser/src/main.rs
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
use std::{env, fs};
|
||||
|
||||
use argus_parser::lexer;
|
||||
// use crate::parser::{parser, Error as ParseError};
|
||||
use ariadne::{sources, Color, Label, Report, ReportKind};
|
||||
use chumsky::Parser;
|
||||
|
||||
fn main() {
|
||||
let src = env::args().nth(1).expect("Expected expression");
|
||||
|
||||
let (tokens, mut errs) = lexer().parse(src.as_str()).into_output_errors();
|
||||
|
||||
println!("*** Outputting tokens ***");
|
||||
if let Some(tokens) = &tokens {
|
||||
for token in tokens {
|
||||
println!("-> {:?}", token);
|
||||
}
|
||||
}
|
||||
|
||||
let parse_errs = if let Some(tokens) = &tokens {
|
||||
let (ast, parse_errs) = parser()
|
||||
.map_with_span(|ast, span| (ast, span))
|
||||
.parse(tokens.as_slice().spanned((src.len()..src.len()).into()))
|
||||
.into_output_errors();
|
||||
|
||||
println!("*** Outputting tokens ***");
|
||||
println!("{:#?}", ast);
|
||||
|
||||
parse_errs
|
||||
} else {
|
||||
Vec::new()
|
||||
};
|
||||
|
||||
errs.into_iter()
|
||||
.map(|e| e.map_token(|c| c.to_string()))
|
||||
// .chain(parse_errs.into_iter().map(|e| e.map_token(|tok| tok.to_string())))
|
||||
.for_each(|e| {
|
||||
Report::build(ReportKind::Error, src.clone(), e.span().start)
|
||||
.with_message(e.to_string())
|
||||
.with_label(
|
||||
Label::new((src.clone(), e.span().into_range()))
|
||||
.with_message(e.reason().to_string())
|
||||
.with_color(Color::Red),
|
||||
)
|
||||
.with_labels(e.contexts().map(|(label, span)| {
|
||||
Label::new((src.clone(), span.into_range()))
|
||||
.with_message(format!("while parsing this {}", label))
|
||||
.with_color(Color::Yellow)
|
||||
}))
|
||||
.finish()
|
||||
.print(sources([(src.clone(), src.clone())]))
|
||||
.unwrap()
|
||||
});
|
||||
}
|
||||
|
|
@ -1,19 +1,406 @@
|
|||
use std::{env, fmt, fs};
|
||||
|
||||
use ariadne::{sources, Color, Label, Report, ReportKind};
|
||||
use chumsky::input::SpannedInput;
|
||||
use chumsky::prelude::*;
|
||||
use chumsky::Parser;
|
||||
|
||||
use crate::lexer::{lexer, Error as LexError, Span, Token};
|
||||
use crate::lexer::{Span, Token};
|
||||
|
||||
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
|
||||
pub enum Type {
|
||||
#[default]
|
||||
Unknown,
|
||||
Bool,
|
||||
UInt,
|
||||
Int,
|
||||
Float,
|
||||
}
|
||||
|
||||
impl Type {
|
||||
/// Get the lowest common supertype for the given types to a common
|
||||
fn get_common_cast(self, other: Self) -> Self {
|
||||
use Type::*;
|
||||
match (self, other) {
|
||||
(Unknown, other) | (other, Unknown) => other,
|
||||
(Bool, ty) | (ty, Bool) => ty,
|
||||
(UInt, Int) => Float,
|
||||
(UInt, Float) => Float,
|
||||
(Int, UInt) => Float,
|
||||
(Int, Float) => Float,
|
||||
(Float, UInt) => Float,
|
||||
(Float, Int) => Float,
|
||||
(lhs, rhs) => {
|
||||
assert_eq!(lhs, rhs);
|
||||
rhs
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Interval<'src> {
|
||||
a: Box<Spanned<Expr<'src>>>,
|
||||
b: Box<Spanned<Expr<'src>>>,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub enum UnaryOps {
|
||||
Neg,
|
||||
Not,
|
||||
Next,
|
||||
Always,
|
||||
Eventually,
|
||||
}
|
||||
|
||||
impl UnaryOps {
|
||||
fn default_type(&self) -> Type {
|
||||
match self {
|
||||
UnaryOps::Neg => Type::Float,
|
||||
_ => Type::Bool,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub enum BinaryOps {
|
||||
Add,
|
||||
Sub,
|
||||
Mul,
|
||||
Div,
|
||||
Lt,
|
||||
Le,
|
||||
Gt,
|
||||
Ge,
|
||||
Eq,
|
||||
Neq,
|
||||
And,
|
||||
Or,
|
||||
Implies,
|
||||
Xor,
|
||||
Equiv,
|
||||
Until,
|
||||
}
|
||||
|
||||
impl BinaryOps {
|
||||
fn default_type(&self) -> Type {
|
||||
match self {
|
||||
BinaryOps::Add | BinaryOps::Sub | BinaryOps::Mul | BinaryOps::Div => Type::Float,
|
||||
_ => Type::Bool,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum Expr<'src> {
|
||||
Error,
|
||||
Bool(bool),
|
||||
Int(i64),
|
||||
UInt(u64),
|
||||
Float(f64),
|
||||
Var {
|
||||
name: &'src str,
|
||||
kind: Type,
|
||||
},
|
||||
Unary {
|
||||
op: UnaryOps,
|
||||
interval: Option<Spanned<Interval<'src>>>,
|
||||
arg: Box<Spanned<Self>>,
|
||||
},
|
||||
Binary {
|
||||
op: BinaryOps,
|
||||
interval: Option<Spanned<Interval<'src>>>,
|
||||
args: (Box<Spanned<Self>>, Box<Spanned<Self>>),
|
||||
},
|
||||
}
|
||||
|
||||
impl<'src> Expr<'src> {
|
||||
fn get_type(&self) -> Type {
|
||||
match self {
|
||||
Expr::Error => Type::Unknown,
|
||||
Expr::Bool(_) => Type::Bool,
|
||||
Expr::Int(_) => Type::Int,
|
||||
Expr::UInt(_) => Type::UInt,
|
||||
Expr::Float(_) => Type::Float,
|
||||
Expr::Var { name: _, kind } => *kind,
|
||||
Expr::Unary {
|
||||
op,
|
||||
interval: _,
|
||||
arg: _,
|
||||
} => op.default_type(),
|
||||
Expr::Binary {
|
||||
op,
|
||||
interval: _,
|
||||
args: _,
|
||||
} => op.default_type(),
|
||||
}
|
||||
}
|
||||
|
||||
/// Make untyped (`Type::Unknown`) expressions into the given type.
|
||||
/// Returns a boolean flag to denote successful transformation or not.
|
||||
fn make_typed(&mut self, ty: Type) -> bool {
|
||||
match self {
|
||||
Expr::Var { name: _, kind } => {
|
||||
*kind = ty;
|
||||
true
|
||||
}
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
|
||||
fn var(name: &'src str) -> Self {
|
||||
Self::Var {
|
||||
name,
|
||||
kind: Type::Unknown,
|
||||
}
|
||||
}
|
||||
|
||||
fn unary_op(op: UnaryOps, arg: Box<Spanned<Self>>, interval: Option<Spanned<Interval<'src>>>) -> Self {
|
||||
let mut arg = arg;
|
||||
(*arg).0.make_typed(op.default_type());
|
||||
Self::Unary { op, interval, arg }
|
||||
}
|
||||
|
||||
fn binary_op(
|
||||
op: BinaryOps,
|
||||
args: (Box<Spanned<Self>>, Box<Spanned<Self>>),
|
||||
interval: Option<Spanned<Interval<'src>>>,
|
||||
) -> Self {
|
||||
let mut args = args;
|
||||
|
||||
let lhs = &mut (*args.0).0;
|
||||
let rhs = &mut (*args.1).0;
|
||||
|
||||
let common_type = lhs.get_type().get_common_cast(rhs.get_type());
|
||||
lhs.make_typed(common_type);
|
||||
rhs.make_typed(common_type);
|
||||
|
||||
Self::Binary { op, interval, args }
|
||||
}
|
||||
}
|
||||
|
||||
pub type Spanned<T> = (T, Span);
|
||||
|
||||
pub type Error<'tokens, 'src> = extra::Err<Rich<'tokens, Token<'src>, Span>>;
|
||||
|
||||
// The type of the input that our parser operates on. The input is the `&[(Token,
|
||||
// Span)]` token buffer generated by the lexer, wrapped in a `SpannedInput` which
|
||||
// 'splits' it apart into its constituent parts, tokens and spans, for chumsky
|
||||
// to understand.
|
||||
type ParserInput<'tokens, 'src> = SpannedInput<Token<'src>, Span, &'tokens [(Token<'src>, Span)]>;
|
||||
|
||||
pub fn parser<'tokens, 'src: 'tokens>(
|
||||
) -> impl Parser<'tokens, ParserInput<'tokens, 'src>, Spanned<Expr<'src>>, LexError<'src>> + Clone {
|
||||
pub fn num_expr_parser<'tokens, 'src: 'tokens>(
|
||||
) -> impl Parser<'tokens, ParserInput<'tokens, 'src>, Spanned<Expr<'src>>, Error<'tokens, 'src>> + Clone {
|
||||
recursive(|num_expr| {
|
||||
let var = select! { Token::Ident(ident) => Expr::Var{ name: ident.clone(), kind: Type::default()} }
|
||||
.labelled("variable");
|
||||
|
||||
let num_literal = select! {
|
||||
Token::Int(val) => Expr::Int(val),
|
||||
Token::UInt(val) => Expr::UInt(val),
|
||||
Token::Float(val) => Expr::Float(val),
|
||||
}
|
||||
.labelled("number literal");
|
||||
|
||||
let num_atom = var
|
||||
.or(num_literal)
|
||||
.map_with_span(|expr, span: Span| (expr, span))
|
||||
// Atoms can also just be normal expressions, but surrounded with parentheses
|
||||
.or(num_expr.clone().delimited_by(just(Token::LParen), just(Token::RParen)))
|
||||
// Attempt to recover anything that looks like a parenthesised expression but contains errors
|
||||
.recover_with(via_parser(nested_delimiters(
|
||||
Token::LParen,
|
||||
Token::RParen,
|
||||
[(Token::LBracket, Token::RBracket)],
|
||||
|span| (Expr::Error, span),
|
||||
)))
|
||||
.boxed();
|
||||
|
||||
let neg_op = just(Token::Minus)
|
||||
.map_with_span(|_, span: Span| (UnaryOps::Neg, span))
|
||||
.repeated()
|
||||
.foldr(num_atom, |op, rhs| {
|
||||
let span = op.1.start..rhs.1.end;
|
||||
(Expr::unary_op(op.0, Box::new(rhs), None), span.into())
|
||||
});
|
||||
|
||||
// Product ops (multiply and divide) have equal precedence
|
||||
let product_op = {
|
||||
let op = just(Token::Times)
|
||||
.to(BinaryOps::Mul)
|
||||
.or(just(Token::Divide).to(BinaryOps::Div));
|
||||
neg_op.clone().foldl(op.then(neg_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
// Sum ops (add and subtract) have equal precedence
|
||||
let sum_op = {
|
||||
let op = just(Token::Plus)
|
||||
.to(BinaryOps::Add)
|
||||
.or(just(Token::Minus).to(BinaryOps::Sub));
|
||||
product_op.clone().foldl(op.then(product_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
sum_op.labelled("numeric expression").as_context()
|
||||
})
|
||||
}
|
||||
|
||||
pub fn parser<'tokens, 'src: 'tokens>(
|
||||
) -> impl Parser<'tokens, ParserInput<'tokens, 'src>, Spanned<Expr<'src>>, Error<'tokens, 'src>> + Clone {
|
||||
let interval = {
|
||||
let num_literal = select! {
|
||||
Token::Int(val) => Expr::Int(val),
|
||||
Token::UInt(val) => Expr::UInt(val),
|
||||
Token::Float(val) => Expr::Float(val),
|
||||
}
|
||||
.map_with_span(|lit, span: Span| (lit, span));
|
||||
let sep = just(Token::Comma).or(just(Token::DotDot));
|
||||
|
||||
num_literal
|
||||
.then_ignore(sep)
|
||||
.then(num_literal)
|
||||
.delimited_by(just(Token::LBracket), just(Token::RBracket))
|
||||
.map(|(a, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(
|
||||
Interval {
|
||||
a: Box::new(a),
|
||||
b: Box::new(b),
|
||||
},
|
||||
span.into(),
|
||||
)
|
||||
})
|
||||
};
|
||||
let num_expr = num_expr_parser();
|
||||
|
||||
recursive(|expr| {
|
||||
let literal = select! {
|
||||
Token::Bool(val) => Expr::Bool(val),
|
||||
}
|
||||
.labelled("boolean literal");
|
||||
|
||||
let var = select! { Token::Ident(ident) => Expr::Var{ name: ident.clone(), kind: Type::default()} }
|
||||
.labelled("variable");
|
||||
|
||||
// Relational ops (<, <=, >, >=) have equal precedence
|
||||
let relational_op = {
|
||||
let op = just(Token::Lt).to(BinaryOps::Lt).or(just(Token::Le)
|
||||
.to(BinaryOps::Le)
|
||||
.or(just(Token::Gt).to(BinaryOps::Gt).or(just(Token::Ge).to(BinaryOps::Ge))));
|
||||
num_expr.clone().foldl(op.then(num_expr).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
// Equality ops (==, !=) have equal precedence
|
||||
let equality_op = {
|
||||
let op = just(Token::Eq)
|
||||
.to(BinaryOps::Eq)
|
||||
.or(just(Token::Neq).to(BinaryOps::Neq));
|
||||
relational_op
|
||||
.clone()
|
||||
.foldl(op.then(relational_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
}
|
||||
.labelled("atomic predicate");
|
||||
|
||||
let atom = equality_op
|
||||
.or(var.or(literal).map_with_span(|expr, span| (expr, span)))
|
||||
// Atoms can also just be normal expressions, but surrounded with parentheses
|
||||
.or(expr.clone().delimited_by(just(Token::LParen), just(Token::RParen)))
|
||||
// Attempt to recover anything that looks like a parenthesised expression but contains errors
|
||||
.recover_with(via_parser(nested_delimiters(
|
||||
Token::LParen,
|
||||
Token::RParen,
|
||||
[],
|
||||
|span| (Expr::Error, span),
|
||||
)))
|
||||
.boxed();
|
||||
|
||||
let not_op = just(Token::Not)
|
||||
.map_with_span(|_, span: Span| (UnaryOps::Not, span))
|
||||
.repeated()
|
||||
.foldr(atom, |op, rhs| {
|
||||
let span = op.1.start..rhs.1.end;
|
||||
(Expr::unary_op(op.0, Box::new(rhs), None), span.into())
|
||||
});
|
||||
|
||||
let next_op = just(Token::Next)
|
||||
.map_with_span(|_, span: Span| (UnaryOps::Next, span))
|
||||
.then(interval.or_not())
|
||||
.repeated()
|
||||
.foldr(not_op, |(op, interval), rhs| {
|
||||
let span = op.1.start..rhs.1.end;
|
||||
(Expr::unary_op(op.0, Box::new(rhs), interval), span.into())
|
||||
});
|
||||
|
||||
let unary_temporal_op = {
|
||||
let op = just(Token::Eventually)
|
||||
.to(UnaryOps::Eventually)
|
||||
.or(just(Token::Always).to(UnaryOps::Always));
|
||||
op.map_with_span(|op, span: Span| (op, span))
|
||||
.then(interval.or_not())
|
||||
.repeated()
|
||||
.foldr(next_op, |(op, interval), rhs| {
|
||||
let span = op.1.start..rhs.1.end;
|
||||
(Expr::unary_op(op.0, Box::new(rhs), interval), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
let binary_temporal_op = unary_temporal_op
|
||||
.clone()
|
||||
.then(just(Token::Until).to(BinaryOps::Until).then(interval.or_not()))
|
||||
.repeated()
|
||||
.foldr(unary_temporal_op, |(lhs, (op, interval)), rhs| {
|
||||
let span = lhs.1.start..rhs.1.end;
|
||||
assert_eq!(op, BinaryOps::Until);
|
||||
(
|
||||
Expr::binary_op(op, (Box::new(lhs), Box::new(rhs)), interval),
|
||||
span.into(),
|
||||
)
|
||||
});
|
||||
|
||||
let and_op = {
|
||||
let op = just(Token::And).to(BinaryOps::And);
|
||||
binary_temporal_op
|
||||
.clone()
|
||||
.foldl(op.then(binary_temporal_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
let or_op = {
|
||||
let op = just(Token::Or).to(BinaryOps::Or);
|
||||
and_op.clone().foldl(op.then(and_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
let xor_op = {
|
||||
let op = just(Token::Xor).to(BinaryOps::Xor);
|
||||
or_op.clone().foldl(op.then(or_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
let implies_equiv_op = {
|
||||
let op = just(Token::Implies)
|
||||
.to(BinaryOps::Implies)
|
||||
.or(just(Token::Equiv).to(BinaryOps::Equiv));
|
||||
xor_op.clone().foldl(op.then(xor_op).repeated(), |a, (op, b)| {
|
||||
let span = a.1.start..b.1.end;
|
||||
(Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
|
||||
})
|
||||
};
|
||||
|
||||
implies_equiv_op.labelled("expression").as_context()
|
||||
})
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue