smt2/client/
ident.rs

1use std::fmt;
2use crate::syntax;
3
4#[derive(Clone, PartialEq, Eq, Hash, Debug)]
5pub enum Ident {
6	Raw(String),
7	Sort(u32),
8	Fun(u32)
9}
10
11impl Ident {
12	pub fn raw(name: &'static str) -> Ident {
13		Ident::Raw(name.to_string())
14	}
15
16	pub fn sort(id: u32) -> Ident {
17		Ident::Sort(id)
18	}
19
20	pub fn function(id: u32) -> Ident {
21		Ident::Fun(id)
22	}
23
24	pub fn from_string(str: &String) -> Ident {
25		if str.len() > 4 {
26			if let Some("Sort") = str.get(0..4) {
27				let id_str = str.get(4..).unwrap();
28				match u32::from_str_radix(id_str, 16) {
29					Ok(id) => return Ident::Sort(id),
30					_ => ()
31				}
32			}
33		}
34
35		if str.len() > 1 {
36			if let Some("f") = str.get(0..1) {
37				let id_str = str.get(1..).unwrap();
38				match u32::from_str_radix(id_str, 16) {
39					Ok(id) => return Ident::Fun(id),
40					_ => ()
41				}
42			}
43		}
44
45		Ident::Raw(str.clone())
46	}
47
48	pub fn from_syntax(sym: &syntax::Symbol) -> Ident {
49		Self::from_string(&sym.id)
50	}
51}
52
53impl fmt::Display for Ident {
54	fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
55		match self {
56			Ident::Raw(name) => write!(f, "{}", name),
57			Ident::Sort(id) => write!(f, "Sort{:x}", id),
58			Ident::Fun(id) => write!(f, "f{:x}", id)
59		}
60	}
61}