gorf_kiselyov/
lib.rs

1use lambda_calculus::Term;
2
3// use crate::underload::{Underload, K, underload_parser};
4
5#[derive(Eq, Ord, Clone, PartialEq, PartialOrd, Hash,Debug)]
6pub enum Ski {
7    S,
8    K,
9    B,
10    R,
11    U,
12    I,
13    App(Box<Ski>, Box<Ski>),
14}
15#[derive(Eq, Ord, Clone, PartialEq, PartialOrd, Hash)]
16pub enum RealSki {
17    RealApp(Box<RealSki>, Box<RealSki>),
18    S,
19    K,
20    I,
21}
22pub fn ra(a: RealSki, b: RealSki) -> RealSki {
23    return RealSki::RealApp(Box::new(a), Box::new(b));
24}
25impl From<Ski> for RealSki {
26    fn from(a: Ski) -> RealSki {
27        match a {
28            Ski::S => RealSki::S,
29            Ski::K => RealSki::K,
30            Ski::B => ra(ra(RealSki::S, ra(RealSki::K, RealSki::S)), RealSki::K),
31            //const R = S (K (S (K (S)) (K))) (S (K (S (I))) (K))
32            Ski::R => ra(
33                ra(
34                    RealSki::S,
35                    ra(
36                        RealSki::K,
37                        ra(ra(RealSki::S, ra(RealSki::K, RealSki::S)), RealSki::K),
38                    ),
39                ),
40                ra(
41                    ra(RealSki::S, ra(RealSki::K, ra(RealSki::S, RealSki::I))),
42                    RealSki::K,
43                ),
44            ),
45            Ski::U => ra(ra(RealSki::S, RealSki::I), RealSki::I),
46            Ski::I => RealSki::I,
47            Ski::App(a, b) => RealSki::RealApp(Box::new(Self::from(*a)), Box::new(Self::from(*b))),
48        }
49    }
50}
51impl RealSki {
52    pub fn convert_default(t: Term) -> RealSki {
53        return Self::from(Ski::convert_default(t));
54    }
55    // pub fn to_underload_str(self) -> String{
56    //     match self{
57    //         RealSki::RealApp(a, b) => format!("{}{}~^",a.to_underload_str(),b.to_underload_str()),
58    //         RealSki::S => "(:)~*(~)*a(~*(~^)*)*)".to_owned(),
59    //         RealSki::K => "(a(!)~*)".to_owned(),
60    //         RealSki::I => "()".to_owned(),
61    //     }
62    // }
63    // pub fn to_underload(self) -> Underload{
64    //     return underload_parser::<Simple<char>>().parse(self.to_underload_str()).unwrap();
65    // }
66}
67pub fn app(a: Ski, b: Ski) -> Ski {
68    return Ski::App(Box::new(a), Box::new(b));
69}
70pub type SkiBall = (usize, Ski);
71impl Ski {
72    pub fn convert(t: Term, hash: &impl Fn(SkiBall, SkiBall) -> Ski) -> SkiBall {
73        match t {
74            Term::Var(0) => (0, Ski::U),
75            Term::Var(1) => (1, Ski::I),
76            Term::Var(n) => {
77                let t = Ski::convert(Term::Var(n - 1), hash);
78                let n = t.0;
79                return (n + 1, hash((0, Ski::K), t));
80            }
81            Term::Abs(e) => {
82                let (n, d) = Ski::convert(*e, hash);
83                if n == 0 {
84                    return (0, Ski::App(Box::new(Ski::K), Box::new(d)));
85                }
86                return (n - 1, d);
87            }
88            Term::App(a) => {
89                let (e1, e2) = *a;
90                let t1 = Ski::convert(e1, hash);
91                let t2 = Ski::convert(e2, hash);
92                return (t1.0.max(t2.0), hash(t1, t2));
93            }
94        }
95    }
96    pub fn default_hash(a: SkiBall, b: SkiBall) -> Ski {
97        let (n1, d1) = a;
98        let (n2, d2) = b;
99        if n1 == 0 {
100            if n2 == 0 {
101                return Ski::App(Box::new(d1), Box::new(d2));
102            } else {
103                return Self::default_hash((0, app(Ski::B, d1)), (n2 - 1, d2));
104            }
105        } else {
106            if n2 == 0 {
107                return Self::default_hash((0, app(Ski::R, d2)), (n2 - 1, d1));
108            } else {
109                let a = Self::default_hash((0, Ski::S), (n1 - 1, d1));
110                return Self::default_hash((n1 - 1, a), (n2 - 1, d2));
111            }
112        }
113    }
114    pub fn convert_default(t: Term) -> Ski {
115        return Self::convert(t, &|a, b| Self::default_hash(a, b)).1;
116    }
117}
gorf_kiselyov/lib.rs

gorf_kiselyov/
lib.rs
