use std::collections::HashMap;
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct NotationEntry {
pub kind: NotationKind,
pub name: String,
pub pattern: Vec<NotationPart>,
pub expansion: String,
pub priority: u32,
pub scopes: Vec<String>,
}
impl NotationEntry {
pub fn new(
kind: NotationKind,
name: String,
pattern: Vec<NotationPart>,
expansion: String,
priority: u32,
) -> Self {
Self {
kind,
name,
pattern,
expansion,
priority,
scopes: Vec::new(),
}
}
pub fn with_scopes(mut self, scopes: Vec<String>) -> Self {
self.scopes = scopes;
self
}
pub fn in_scope(&self, scope: &str) -> bool {
self.scopes.iter().any(|s| s == scope)
}
pub fn is_global(&self) -> bool {
self.scopes.is_empty()
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct ScopeGuard<'a> {
pub(super) env: &'a mut NotationEnv,
}
impl<'a> ScopeGuard<'a> {
#[allow(dead_code)]
pub fn new(env: &'a mut NotationEnv) -> Self {
env.push_scope();
ScopeGuard { env }
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct OperatorAlias {
pub alias: String,
pub canonical: String,
}
impl OperatorAlias {
#[allow(dead_code)]
pub fn new(alias: &str, canonical: &str) -> Self {
OperatorAlias {
alias: alias.to_string(),
canonical: canonical.to_string(),
}
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum NotationCategory {
Term,
Tactic,
Command,
Custom(String),
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct OperatorEntry {
pub symbol: String,
pub fixity: Fixity,
pub precedence: u32,
pub expansion: String,
}
impl OperatorEntry {
pub fn new(symbol: String, fixity: Fixity, precedence: u32, expansion: String) -> Self {
Self {
symbol,
fixity,
precedence,
expansion,
}
}
pub fn is_prefix(&self) -> bool {
self.fixity == Fixity::Prefix
}
pub fn is_infix(&self) -> bool {
matches!(self.fixity, Fixity::Infixl | Fixity::Infixr)
}
pub fn is_postfix(&self) -> bool {
self.fixity == Fixity::Postfix
}
pub fn is_left_assoc(&self) -> bool {
self.fixity == Fixity::Infixl
}
pub fn is_right_assoc(&self) -> bool {
self.fixity == Fixity::Infixr
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct OverloadRegistry {
pub entries: Vec<OverloadEntry>,
}
impl OverloadRegistry {
#[allow(dead_code)]
pub fn new() -> Self {
OverloadRegistry {
entries: Vec::new(),
}
}
#[allow(dead_code)]
pub fn register(&mut self, entry: OverloadEntry) {
self.entries.push(entry);
}
#[allow(dead_code)]
pub fn best_overload(&self, symbol: &str) -> Option<&OverloadEntry> {
self.entries
.iter()
.filter(|e| e.symbol == symbol)
.max_by_key(|e| e.priority)
}
#[allow(dead_code)]
pub fn all_overloads(&self, symbol: &str) -> Vec<&OverloadEntry> {
self.entries.iter().filter(|e| e.symbol == symbol).collect()
}
}
#[derive(Debug, Clone)]
pub struct NotationTable {
entries: Vec<NotationEntry>,
operators: HashMap<String, OperatorEntry>,
scoped_entries: HashMap<String, Vec<usize>>,
active_scopes: Vec<String>,
}
impl NotationTable {
pub fn new() -> Self {
Self {
entries: Vec::new(),
operators: HashMap::new(),
scoped_entries: HashMap::new(),
active_scopes: Vec::new(),
}
}
pub fn register_notation(&mut self, entry: NotationEntry) {
let idx = self.entries.len();
for scope in &entry.scopes {
self.scoped_entries
.entry(scope.clone())
.or_default()
.push(idx);
}
self.entries.push(entry);
}
pub fn register_operator(&mut self, entry: OperatorEntry) {
self.operators.insert(entry.symbol.clone(), entry);
}
pub fn lookup_prefix(&self, symbol: &str) -> Option<&OperatorEntry> {
self.operators
.get(symbol)
.filter(|op| op.fixity == Fixity::Prefix)
}
pub fn lookup_infix(&self, symbol: &str) -> Option<&OperatorEntry> {
self.operators
.get(symbol)
.filter(|op| matches!(op.fixity, Fixity::Infixl | Fixity::Infixr))
}
pub fn lookup_postfix(&self, symbol: &str) -> Option<&OperatorEntry> {
self.operators
.get(symbol)
.filter(|op| op.fixity == Fixity::Postfix)
}
pub fn lookup_operator(&self, symbol: &str) -> Option<&OperatorEntry> {
self.operators.get(symbol)
}
pub fn get_precedence(&self, symbol: &str) -> Option<u32> {
self.operators.get(symbol).map(|op| op.precedence)
}
pub fn get_entry(&self, index: usize) -> Option<&NotationEntry> {
self.entries.get(index)
}
pub fn notation_count(&self) -> usize {
self.entries.len()
}
pub fn operator_count(&self) -> usize {
self.operators.len()
}
pub fn open_scope(&mut self, scope: &str) -> Vec<&NotationEntry> {
if !self.active_scopes.contains(&scope.to_string()) {
self.active_scopes.push(scope.to_string());
}
self.scoped_entries
.get(scope)
.map(|indices| {
indices
.iter()
.filter_map(|&idx| self.entries.get(idx))
.collect()
})
.unwrap_or_default()
}
pub fn close_scope(&mut self, scope: &str) {
self.active_scopes.retain(|s| s != scope);
}
pub fn is_scope_active(&self, scope: &str) -> bool {
self.active_scopes.contains(&scope.to_string())
}
pub fn active_scope_names(&self) -> &[String] {
&self.active_scopes
}
pub fn active_notations(&self) -> Vec<&NotationEntry> {
self.entries
.iter()
.filter(|entry| {
entry.is_global() || entry.scopes.iter().any(|s| self.active_scopes.contains(s))
})
.collect()
}
pub fn find_by_name(&self, name: &str) -> Vec<&NotationEntry> {
self.entries.iter().filter(|e| e.name == name).collect()
}
pub fn find_by_kind(&self, kind: &NotationKind) -> Vec<&NotationEntry> {
self.entries.iter().filter(|e| &e.kind == kind).collect()
}
pub fn find_operators_by_fixity(&self, fixity: &Fixity) -> Vec<&OperatorEntry> {
self.operators
.values()
.filter(|op| &op.fixity == fixity)
.collect()
}
pub fn all_operator_symbols(&self) -> Vec<&str> {
let mut symbols: Vec<&str> = self.operators.keys().map(|s| s.as_str()).collect();
symbols.sort();
symbols
}
pub fn compare_precedence(&self, a: &str, b: &str) -> Option<std::cmp::Ordering> {
let pa = self.get_precedence(a)?;
let pb = self.get_precedence(b)?;
Some(pa.cmp(&pb))
}
pub fn builtin_operators() -> Self {
let mut table = Self::new();
table.register_operator(OperatorEntry::new(
"+".to_string(),
Fixity::Infixl,
65,
"HAdd.hAdd".to_string(),
));
table.register_operator(OperatorEntry::new(
"-".to_string(),
Fixity::Infixl,
65,
"HSub.hSub".to_string(),
));
table.register_operator(OperatorEntry::new(
"*".to_string(),
Fixity::Infixl,
70,
"HMul.hMul".to_string(),
));
table.register_operator(OperatorEntry::new(
"/".to_string(),
Fixity::Infixl,
70,
"HDiv.hDiv".to_string(),
));
table.register_operator(OperatorEntry::new(
"%".to_string(),
Fixity::Infixl,
70,
"HMod.hMod".to_string(),
));
table.register_operator(OperatorEntry::new(
"^".to_string(),
Fixity::Infixr,
75,
"HPow.hPow".to_string(),
));
table.register_operator(OperatorEntry::new(
"=".to_string(),
Fixity::Infixl,
50,
"Eq".to_string(),
));
table.register_operator(OperatorEntry::new(
"!=".to_string(),
Fixity::Infixl,
50,
"Ne".to_string(),
));
table.register_operator(OperatorEntry::new(
"<".to_string(),
Fixity::Infixl,
50,
"LT.lt".to_string(),
));
table.register_operator(OperatorEntry::new(
">".to_string(),
Fixity::Infixl,
50,
"GT.gt".to_string(),
));
table.register_operator(OperatorEntry::new(
"<=".to_string(),
Fixity::Infixl,
50,
"LE.le".to_string(),
));
table.register_operator(OperatorEntry::new(
">=".to_string(),
Fixity::Infixl,
50,
"GE.ge".to_string(),
));
table.register_operator(OperatorEntry::new(
"&&".to_string(),
Fixity::Infixl,
35,
"And".to_string(),
));
table.register_operator(OperatorEntry::new(
"||".to_string(),
Fixity::Infixl,
30,
"Or".to_string(),
));
table.register_operator(OperatorEntry::new(
"!".to_string(),
Fixity::Prefix,
100,
"Not".to_string(),
));
table.register_operator(OperatorEntry::new(
"->".to_string(),
Fixity::Infixr,
25,
"Arrow".to_string(),
));
table.register_operator(OperatorEntry::new(
":=".to_string(),
Fixity::Infixl,
1,
"Assign".to_string(),
));
let ops: Vec<(String, NotationKind, u32, String)> = vec![
("+".into(), NotationKind::Infixl, 65, "HAdd.hAdd".into()),
("-".into(), NotationKind::Infixl, 65, "HSub.hSub".into()),
("*".into(), NotationKind::Infixl, 70, "HMul.hMul".into()),
("/".into(), NotationKind::Infixl, 70, "HDiv.hDiv".into()),
("%".into(), NotationKind::Infixl, 70, "HMod.hMod".into()),
("^".into(), NotationKind::Infixr, 75, "HPow.hPow".into()),
("=".into(), NotationKind::Infixl, 50, "Eq".into()),
("!=".into(), NotationKind::Infixl, 50, "Ne".into()),
("<".into(), NotationKind::Infixl, 50, "LT.lt".into()),
(">".into(), NotationKind::Infixl, 50, "GT.gt".into()),
("<=".into(), NotationKind::Infixl, 50, "LE.le".into()),
(">=".into(), NotationKind::Infixl, 50, "GE.ge".into()),
("&&".into(), NotationKind::Infixl, 35, "And".into()),
("||".into(), NotationKind::Infixl, 30, "Or".into()),
("!".into(), NotationKind::Prefix, 100, "Not".into()),
("->".into(), NotationKind::Infixr, 25, "Arrow".into()),
(":=".into(), NotationKind::Infixl, 1, "Assign".into()),
];
for (sym, kind, prec, expansion) in ops {
let pattern = match &kind {
NotationKind::Prefix => {
vec![
NotationPart::Literal(sym.clone()),
NotationPart::Placeholder("x".into()),
]
}
NotationKind::Postfix => {
vec![
NotationPart::Placeholder("x".into()),
NotationPart::Literal(sym.clone()),
]
}
_ => {
vec![
NotationPart::Placeholder("lhs".into()),
NotationPart::Literal(sym.clone()),
NotationPart::Placeholder("rhs".into()),
]
}
};
table.register_notation(NotationEntry::new(kind, sym, pattern, expansion, prec));
}
table
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct NotationFormatter {
pub registry: NotationRegistry,
}
impl NotationFormatter {
#[allow(dead_code)]
pub fn new(reg: NotationRegistry) -> Self {
NotationFormatter { registry: reg }
}
#[allow(dead_code)]
pub fn rule_count(&self) -> usize {
self.registry.rules.len()
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct NotationRule {
pub pattern: String,
pub expansion: String,
pub prec: PrecLevel,
pub namespace: Option<String>,
}
impl NotationRule {
#[allow(dead_code)]
pub fn new(pattern: &str, expansion: &str, prec: PrecLevel) -> Self {
NotationRule {
pattern: pattern.to_string(),
expansion: expansion.to_string(),
prec,
namespace: None,
}
}
#[allow(dead_code)]
pub fn in_namespace(mut self, ns: &str) -> Self {
self.namespace = Some(ns.to_string());
self
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum NotationTokenKind {
Literal(String),
Hole,
NamedHole(String),
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct OverloadEntry {
pub symbol: String,
pub typeclass: String,
pub priority: u32,
}
impl OverloadEntry {
#[allow(dead_code)]
pub fn new(symbol: &str, typeclass: &str, priority: u32) -> Self {
OverloadEntry {
symbol: symbol.to_string(),
typeclass: typeclass.to_string(),
priority,
}
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct NotationRegistry {
pub rules: Vec<NotationRule>,
}
impl NotationRegistry {
#[allow(dead_code)]
pub fn new() -> Self {
NotationRegistry { rules: Vec::new() }
}
#[allow(dead_code)]
pub fn register(&mut self, rule: NotationRule) {
self.rules.push(rule);
}
#[allow(dead_code)]
pub fn find_by_pattern(&self, pattern: &str) -> Vec<&NotationRule> {
self.rules.iter().filter(|r| r.pattern == pattern).collect()
}
#[allow(dead_code)]
pub fn find_by_namespace(&self, ns: &str) -> Vec<&NotationRule> {
self.rules
.iter()
.filter(|r| r.namespace.as_deref() == Some(ns))
.collect()
}
#[allow(dead_code)]
pub fn len(&self) -> usize {
self.rules.len()
}
#[allow(dead_code)]
pub fn is_empty(&self) -> bool {
self.rules.is_empty()
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct BuiltinPrecTable {
pub entries: Vec<(String, u32, bool)>,
}
impl BuiltinPrecTable {
#[allow(dead_code)]
pub fn standard() -> Self {
BuiltinPrecTable {
entries: vec![
("=".to_string(), 50, false),
("<".to_string(), 50, false),
(">".to_string(), 50, false),
("<=".to_string(), 50, false),
(">=".to_string(), 50, false),
("≠".to_string(), 50, false),
("∧".to_string(), 35, true),
("∨".to_string(), 30, true),
("→".to_string(), 25, false),
("↔".to_string(), 20, false),
("+".to_string(), 65, true),
("-".to_string(), 65, true),
("*".to_string(), 70, true),
("/".to_string(), 70, true),
("%".to_string(), 70, true),
("^".to_string(), 75, false),
],
}
}
#[allow(dead_code)]
pub fn lookup(&self, op: &str) -> Option<(u32, bool)> {
self.entries
.iter()
.find(|(o, _, _)| o == op)
.map(|(_, p, l)| (*p, *l))
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct NotationScope {
pub name: String,
pub rules: Vec<NotationRule>,
}
impl NotationScope {
#[allow(dead_code)]
pub fn new(name: &str) -> Self {
NotationScope {
name: name.to_string(),
rules: Vec::new(),
}
}
#[allow(dead_code)]
pub fn add_rule(&mut self, rule: NotationRule) {
self.rules.push(rule);
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct MacroRule {
pub name: String,
pub params: Vec<String>,
pub body: String,
}
impl MacroRule {
#[allow(dead_code)]
pub fn new(name: &str, params: Vec<&str>, body: &str) -> Self {
MacroRule {
name: name.to_string(),
params: params.into_iter().map(|s| s.to_string()).collect(),
body: body.to_string(),
}
}
#[allow(dead_code)]
pub fn instantiate(&self, args: &[&str]) -> String {
if args.len() != self.params.len() {
return format!(
"(macro-error: {} expects {} args, got {})",
self.name,
self.params.len(),
args.len()
);
}
let mut result = self.body.clone();
for (param, arg) in self.params.iter().zip(args.iter()) {
result = result.replace(param.as_str(), arg);
}
result
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct SyntaxSugarLibrary {
pub sugars: Vec<SyntaxSugar>,
}
impl SyntaxSugarLibrary {
#[allow(dead_code)]
pub fn new() -> Self {
SyntaxSugarLibrary { sugars: Vec::new() }
}
#[allow(dead_code)]
pub fn add(&mut self, sugar: SyntaxSugar) {
self.sugars.push(sugar);
}
#[allow(dead_code)]
pub fn find(&self, name: &str) -> Option<&SyntaxSugar> {
self.sugars.iter().find(|s| s.name == name)
}
#[allow(dead_code)]
pub fn len(&self) -> usize {
self.sugars.len()
}
#[allow(dead_code)]
pub fn is_empty(&self) -> bool {
self.sugars.is_empty()
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct SyntaxExtension {
pub name: String,
pub is_infix: bool,
pub is_prefix: bool,
pub is_postfix: bool,
}
impl SyntaxExtension {
#[allow(dead_code)]
pub fn infix(name: &str) -> Self {
SyntaxExtension {
name: name.to_string(),
is_infix: true,
is_prefix: false,
is_postfix: false,
}
}
#[allow(dead_code)]
pub fn prefix(name: &str) -> Self {
SyntaxExtension {
name: name.to_string(),
is_infix: false,
is_prefix: true,
is_postfix: false,
}
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct OperatorAliasTable {
pub entries: Vec<OperatorAlias>,
}
impl OperatorAliasTable {
#[allow(dead_code)]
pub fn new() -> Self {
OperatorAliasTable {
entries: Vec::new(),
}
}
#[allow(dead_code)]
pub fn add(&mut self, alias: OperatorAlias) {
self.entries.push(alias);
}
#[allow(dead_code)]
pub fn resolve(&self, op: &str) -> String {
self.entries
.iter()
.find(|e| e.alias == op)
.map(|e| e.canonical.clone())
.unwrap_or_else(|| op.to_string())
}
#[allow(dead_code)]
pub fn len(&self) -> usize {
self.entries.len()
}
#[allow(dead_code)]
pub fn is_empty(&self) -> bool {
self.entries.is_empty()
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct NotationGroup {
pub name: String,
pub rules: Vec<NotationRule>,
pub active: bool,
}
impl NotationGroup {
#[allow(dead_code)]
pub fn new(name: &str) -> Self {
NotationGroup {
name: name.to_string(),
rules: Vec::new(),
active: true,
}
}
#[allow(dead_code)]
pub fn add(&mut self, rule: NotationRule) {
self.rules.push(rule);
}
#[allow(dead_code)]
pub fn deactivate(&mut self) {
self.active = false;
}
#[allow(dead_code)]
pub fn active_rules(&self) -> Vec<&NotationRule> {
if self.active {
self.rules.iter().collect()
} else {
Vec::new()
}
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct NotationPriorityQueue {
pub rules: Vec<NotationRule>,
}
impl NotationPriorityQueue {
#[allow(dead_code)]
pub fn new() -> Self {
NotationPriorityQueue { rules: Vec::new() }
}
#[allow(dead_code)]
pub fn insert(&mut self, rule: NotationRule) {
let pos = self
.rules
.partition_point(|r| r.prec.value >= rule.prec.value);
self.rules.insert(pos, rule);
}
#[allow(dead_code)]
pub fn rules_at_or_above(&self, prec: u32) -> Vec<&NotationRule> {
self.rules.iter().filter(|r| r.prec.value >= prec).collect()
}
#[allow(dead_code)]
pub fn len(&self) -> usize {
self.rules.len()
}
#[allow(dead_code)]
pub fn is_empty(&self) -> bool {
self.rules.is_empty()
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum NotationKind {
Prefix,
Postfix,
Infixl,
Infixr,
Notation,
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct SyntaxSugar {
pub name: String,
pub surface: String,
pub core: String,
}
impl SyntaxSugar {
#[allow(dead_code)]
pub fn new(name: &str, surface: &str, core: &str) -> Self {
SyntaxSugar {
name: name.to_string(),
surface: surface.to_string(),
core: core.to_string(),
}
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct PatternMatcher {
pub pattern: Vec<String>,
}
impl PatternMatcher {
#[allow(dead_code)]
#[allow(clippy::should_implement_trait)]
pub fn from_str(s: &str) -> Self {
PatternMatcher {
pattern: s.split_whitespace().map(|t| t.to_string()).collect(),
}
}
#[allow(dead_code)]
pub fn hole_count(&self) -> usize {
self.pattern.iter().filter(|t| t.as_str() == "_").count()
}
#[allow(dead_code)]
pub fn all_holes(&self) -> bool {
self.pattern.iter().all(|t| t.as_str() == "_")
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum Fixity {
Prefix,
Infixl,
Infixr,
Postfix,
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone)]
pub struct NotationConflict {
pub pattern: String,
pub expansion_a: String,
pub expansion_b: String,
}
#[allow(dead_code)]
#[allow(missing_docs)]
pub struct NotationEnv {
pub scopes: Vec<Vec<NotationRule>>,
}
impl NotationEnv {
#[allow(dead_code)]
pub fn new() -> Self {
NotationEnv {
scopes: vec![Vec::new()],
}
}
#[allow(dead_code)]
pub fn push_scope(&mut self) {
self.scopes.push(Vec::new());
}
#[allow(dead_code)]
pub fn pop_scope(&mut self) {
if self.scopes.len() > 1 {
self.scopes.pop();
}
}
#[allow(dead_code)]
pub fn add(&mut self, rule: NotationRule) {
if let Some(scope) = self.scopes.last_mut() {
scope.push(rule);
}
}
#[allow(dead_code)]
pub fn lookup(&self, pattern: &str) -> Vec<&NotationRule> {
let mut result = Vec::new();
for scope in self.scopes.iter().rev() {
for rule in scope {
if rule.pattern == pattern {
result.push(rule);
}
}
}
result
}
#[allow(dead_code)]
pub fn total_rules(&self) -> usize {
self.scopes.iter().map(|s| s.len()).sum()
}
}
#[allow(dead_code)]
#[allow(missing_docs)]
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PrecLevel {
pub value: u32,
pub left_assoc: bool,
pub right_assoc: bool,
}
impl PrecLevel {
#[allow(dead_code)]
pub fn left(value: u32) -> Self {
PrecLevel {
value,
left_assoc: true,
right_assoc: false,
}
}
#[allow(dead_code)]
pub fn right(value: u32) -> Self {
PrecLevel {
value,
left_assoc: false,
right_assoc: true,
}
}
#[allow(dead_code)]
pub fn none(value: u32) -> Self {
PrecLevel {
value,
left_assoc: false,
right_assoc: false,
}
}
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum NotationPart {
Literal(String),
Placeholder(String),
Prec(u32),
}