ftml_solver/
hoas.rs

1use std::borrow::Cow;
2
3use ftml_ontology::terms::{ApplicationTerm, Argument, ComponentVar, Term, helpers::IntoTerm};
4use ftml_uris::SymbolUri;
5
6use crate::{
7    Checker,
8    impls::solving::{Solutions, Solvable},
9    split::SplitStrategy,
10};
11
12#[derive(Debug, Clone)]
13pub struct HOASSymbols {
14    pub judgment: Option<SymbolUri>,
15    pub lambda: SymbolUri,
16    pub pi: SymbolUri,
17    pub any: SymbolUri,
18    pub apply: Option<SymbolUri>,
19    //dummies: std::sync::atomic::AtomicUsize,
20}
21impl HOASSymbols {
22    pub fn apply<'t, Split: SplitStrategy>(
23        &self,
24        checker: &Checker<Split>,
25        head: &'t Term,
26        arguments: impl Iterator<Item = Option<Term>>,
27    ) -> (Cow<'t, Term>, Solutions) {
28        let mut ret = Solutions::default();
29        if let Some(app) = self.apply.as_ref() {
30            (
31                arguments.fold(Cow::Borrowed(head), |h, a| {
32                    Cow::Owned(app.clone().apply_tms([
33                        h.into_owned(),
34                        a.unwrap_or_else(|| {
35                            let name = checker.new_solvable();
36                            ret.0
37                                .insert(Solvable::new(name.clone(), std::iter::empty()));
38                            name.into()
39                        }),
40                    ]))
41                }),
42                ret,
43            )
44        } else {
45            let args = arguments
46                .map(|t| {
47                    Argument::Simple(t.unwrap_or_else(|| {
48                        let name = checker.new_solvable();
49                        ret.0
50                            .insert(Solvable::new(name.clone(), std::iter::empty()));
51                        name.into()
52                    }))
53                })
54                .collect::<Box<[_]>>();
55            (
56                if args.is_empty() {
57                    Cow::Borrowed(head)
58                } else {
59                    Cow::Owned(Term::Application(ApplicationTerm::new(
60                        head.clone(),
61                        args,
62                        None,
63                    )))
64                },
65                ret,
66            )
67        }
68    }
69
70    pub fn get<Split: SplitStrategy>(checker: &Checker<Split>) -> Option<Self> {
71        let judgment = checker.rules.marker().iter().rev().find_map(|rl| {
72            rl.as_any()
73                .downcast_ref::<super::rules::IsJudgmentRule>()
74                .map(|rl| rl.0.clone())
75        });
76        let any = checker.rules.marker().iter().rev().find_map(|rl| {
77            rl.as_any()
78                .downcast_ref::<super::rules::operators::universe::AnyRule>()
79                .map(|rl| rl.0.clone())
80        })?;
81        let (lambda, pi, apply) = checker.rules.marker().iter().rev().find_map(|rl| {
82            rl.as_any()
83                .downcast_ref::<super::rules::HOASRule>()
84                .map(|rl| (rl.lambda.clone(), rl.pi.clone(), rl.apply.clone()))
85        })?;
86        Some(Self {
87            judgment,
88            lambda,
89            pi,
90            any,
91            apply, //dummies: std::sync::atomic::AtomicUsize::new(0),
92        })
93    }
94
95    pub fn wrap_vars<'c>(
96        &self,
97        args: impl DoubleEndedIterator<Item = ComponentVar>,
98        ret: &'c Term,
99    ) -> Cow<'c, Term> {
100        args.rev().fold(Cow::Borrowed(ret), |c, v| {
101            //let premise = self.wrap_judg(p).into_owned();
102            Cow::Owned(
103                self.pi
104                    .clone()
105                    .simple_bind(v.var, v.tp, v.df, c.into_owned()),
106            )
107        })
108    }
109
110    pub fn wrap_types<'c>(&self, args: &[Term], ret: &'c Term) -> Cow<'c, Term> {
111        let ret = self.wrap_judg(ret);
112        args.iter().rev().fold(ret, |c, p| {
113            let premise = self.wrap_judg(p).into_owned();
114            Cow::Owned(self.pi.clone().simple_bind(
115                crate::DUMMY.clone().into(),
116                Some(premise),
117                None,
118                c.into_owned(),
119            ))
120        })
121    }
122
123    #[inline]
124    pub fn let_in(var: ComponentVar, body: Term) -> Term {
125        ftml_uris::metatheory::LET_IN
126            .clone()
127            .simple_bind(var.var, var.tp, var.df, body)
128    }
129
130    #[inline]
131    pub fn lambda(&self, var: ComponentVar, body: Term) -> Term {
132        self.lambda
133            .clone()
134            .simple_bind(var.var, var.tp, var.df, body)
135    }
136
137    #[inline]
138    pub fn pi(&self, var: ComponentVar, body: Term) -> Term {
139        self.pi.clone().simple_bind(var.var, var.tp, var.df, body)
140    }
141
142    pub fn wrap_judg<'c>(&self, ret: &'c Term) -> Cow<'c, Term> {
143        self.judgment.as_ref().map_or_else(
144            || Cow::Borrowed(ret),
145            |j| {
146                Cow::Owned(self.apply.as_ref().map_or_else(
147                    || j.clone().apply_tms([ret.clone()]),
148                    |app| app.clone().apply_tms([j.clone().into(), ret.clone()]),
149                ))
150            },
151        )
152    }
153}
ftml_solver/hoas.rs

ftml_solver/
hoas.rs
