syn_sem/semantic/logic/
term.rs

1//! Term definitions.
2
3use crate::{semantic::entry::GlobalCx, TermIn};
4use logic_eval::{Name, Term};
5
6use crate::etc::util::IntoPathSegments;
7
8// '#' is a prefix to distinguish between reserved functors and user functors.
9pub(crate) const FUNCTOR_IMPL: &str = "#impl";
10pub(crate) const FUNCTOR_TRAIT: &str = "#trait";
11pub(crate) const FUNCTOR_ASSOC_TY: &str = "#assoc_ty";
12pub(crate) const FUNCTOR_ASSOC_FN: &str = "#assoc_fn";
13pub(crate) const FUNCTOR_INHER_FN: &str = "#inher_fn";
14pub(crate) const FUNCTOR_ASSOC_CONST_TY: &str = "#assoc_const_ty";
15pub(crate) const FUNCTOR_ASSOC_CONST_VAL: &str = "#assoc_const_val";
16pub(crate) const FUNCTOR_INHER_CONST: &str = "#inher_const";
17pub(crate) const FUNCTOR_REF: &str = "#ref";
18pub(crate) const FUNCTOR_MUT: &str = "#mut";
19pub(crate) const FUNCTOR_ARRAY: &str = "#array";
20pub(crate) const FUNCTOR_TUPLE: &str = "#tuple";
21pub(crate) const FUNCTOR_SIG: &str = "#sig";
22pub(crate) const FUNCTOR_INT: &str = "#int";
23pub(crate) const FUNCTOR_FLOAT: &str = "#float";
24pub(crate) const FUNCTOR_UNIT: &str = "#unit";
25pub(crate) const FUNCTOR_LIST: &str = "#list"; // 'logic-eval' doesn't have array('[]') yet.
26pub(crate) const FUNCTOR_ARG: &str = "#arg";
27pub(crate) const FUNCTOR_DYN_ARRAY_LEN: &str = "#dyn";
28
29// === impl/n ===
30
31/// `impl/1`
32///
33/// * Arg0 - Self type
34///
35/// # Examples
36///
37/// * Code   - impl Foo { .. }
38/// * Output - impl(Foo)
39pub fn impl_1<'gcx>(self_ty: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
40    Term {
41        functor: Name::with_intern(FUNCTOR_IMPL, gcx),
42        args: [self_ty].into(),
43    }
44}
45
46/// `impl/2`
47///
48/// * Arg0 - Self type
49/// * Arg1 - Trait
50///
51/// # Examples
52///
53/// * Code   - impl Trait for Foo { .. }
54/// * Output - impl(Foo, Trait)
55pub fn impl_2<'gcx>(
56    self_ty: TermIn<'gcx>,
57    trait_: TermIn<'gcx>,
58    gcx: &'gcx GlobalCx<'gcx>,
59) -> TermIn<'gcx> {
60    Term {
61        functor: Name::with_intern(FUNCTOR_IMPL, gcx),
62        args: [self_ty, trait_].into(),
63    }
64}
65
66// === trait/n ===
67
68/// `trait/1`
69///
70/// * Arg0 - Trait
71///
72/// # Examples
73///
74/// * Code   - trait Trait { .. }
75/// * Output - trait(Trait)
76pub fn trait_1<'gcx>(trait_: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
77    Term {
78        functor: Name::with_intern(FUNCTOR_TRAIT, gcx),
79        args: [trait_].into(),
80    }
81}
82
83// === assoc_ty/n ===
84
85/// `assoc_ty/4`
86///
87/// * Arg0 - Self type
88/// * Arg1 - Trait
89/// * Arg2 - Associated type
90/// * Arg3 - Assigned(Bound) type
91///
92/// # Examples
93///
94/// * Code   - impl Iterator for Foo { type Item = Bar; }
95/// * Output - assoc_ty(Foo, Iterator, Item, Bar)
96pub fn assoc_ty_4<'gcx>(
97    self_ty: TermIn<'gcx>,
98    trait_: TermIn<'gcx>,
99    assoc_ty: TermIn<'gcx>,
100    assign_ty: TermIn<'gcx>,
101    gcx: &'gcx GlobalCx<'gcx>,
102) -> TermIn<'gcx> {
103    Term {
104        functor: Name::with_intern(FUNCTOR_ASSOC_TY, gcx),
105        args: [self_ty, trait_, assoc_ty, assign_ty].into(),
106    }
107}
108
109// === assoc_fn/n ===
110
111/// `assoc_fn/3`
112///
113/// * Arg0 - Trait
114/// * Arg1 - Associated function name
115/// * Arg2 - Function signature
116///
117/// # Examples
118///
119/// * Code   - trait Trait { fn foo<T>(a: In0, b: In1) -> Out }
120/// * Output - assoc_fn(Trait, foo(T), sig(Out, In0, In1))
121pub fn assoc_fn_3<'gcx>(
122    trait_: TermIn<'gcx>,
123    fn_ident: TermIn<'gcx>,
124    sig: TermIn<'gcx>,
125    gcx: &'gcx GlobalCx<'gcx>,
126) -> TermIn<'gcx> {
127    Term {
128        functor: Name::with_intern(FUNCTOR_ASSOC_FN, gcx),
129        args: [trait_, fn_ident, sig].into(),
130    }
131}
132
133// === inher_fn/n ===
134
135/// `inher_fn/3`
136///
137/// * Arg0 - Self type
138/// * Arg1 - Inherent function name
139/// * Arg2 - Function signature
140///
141/// # Examples
142///
143/// * Code   - impl St { fn foo<T>(a: In0, b: In1) -> Out }
144/// * Output - inher_fn(St, foo(T), sig(Out, In0, In1))
145pub fn inher_fn_3<'gcx>(
146    self_ty: TermIn<'gcx>,
147    fn_ident: TermIn<'gcx>,
148    sig: TermIn<'gcx>,
149    gcx: &'gcx GlobalCx<'gcx>,
150) -> TermIn<'gcx> {
151    Term {
152        functor: Name::with_intern(FUNCTOR_INHER_FN, gcx),
153        args: [self_ty, fn_ident, sig].into(),
154    }
155}
156
157// === assoc_const_ty/n ===
158
159/// `assoc_const_ty/3`
160///
161/// * Arg0 - Trait
162/// * Arg1 - Associated const name
163/// * Arg2 - Type of the const
164///
165/// # Examples
166///
167/// * Code   - trait Trait { const A: ConstTy = .. }
168/// * Output - assoc_const_ty(Trait, A, ConstTy)
169pub fn assoc_const_ty_3<'gcx>(
170    trait_: TermIn<'gcx>,
171    const_ident: TermIn<'gcx>,
172    const_ty: TermIn<'gcx>,
173    gcx: &'gcx GlobalCx<'gcx>,
174) -> TermIn<'gcx> {
175    Term {
176        functor: Name::with_intern(FUNCTOR_ASSOC_CONST_TY, gcx),
177        args: [trait_, const_ident, const_ty].into(),
178    }
179}
180
181// === assoc_const_val/n ===
182
183/// `assoc_const_val/3`
184///
185/// * Arg0 - Trait
186/// * Arg1 - Associated const name
187/// * Arg2 - Const id
188///
189/// # Examples
190///
191/// * Code   - trait Trait { const A: ConstTy = Value }
192/// * Output - assoc_const_val(Trait, A, id to the Value)
193pub fn assoc_const_val_3<'gcx>(
194    trait_: TermIn<'gcx>,
195    const_ident: TermIn<'gcx>,
196    const_id: TermIn<'gcx>,
197    gcx: &'gcx GlobalCx<'gcx>,
198) -> TermIn<'gcx> {
199    Term {
200        functor: Name::with_intern(FUNCTOR_ASSOC_CONST_VAL, gcx),
201        args: [trait_, const_ident, const_id].into(),
202    }
203}
204
205/// `assoc_const_val/4`
206///
207/// * Arg0 - Self type
208/// * Arg1 - Trait
209/// * Arg2 - Associated const name
210/// * Arg3 - Const id
211///
212/// # Examples
213///
214/// * Code   - impl Trait for Foo { const A: ConstTy = Value }
215/// * Output - assoc_const_val(Foo, Trait, A, id to the Value)
216pub fn assoc_const_val_4<'gcx>(
217    self_ty: TermIn<'gcx>,
218    trait_: TermIn<'gcx>,
219    const_ident: TermIn<'gcx>,
220    const_id: TermIn<'gcx>,
221    gcx: &'gcx GlobalCx<'gcx>,
222) -> TermIn<'gcx> {
223    Term {
224        functor: Name::with_intern(FUNCTOR_ASSOC_CONST_VAL, gcx),
225        args: [self_ty, trait_, const_ident, const_id].into(),
226    }
227}
228
229// === inher_const/n ===
230
231/// `inher_const/4`
232///
233/// * Arg0 - Self type
234/// * Arg1 - Associated const name
235/// * Arg2 - Type of the const
236/// * Arg3 - Const id
237///
238/// # Examples
239///
240/// * Code   - impl Foo { const A: ConstTy = Value }
241/// * Output - inher_const(Foo, A, ConstTy, id to the Value)
242pub fn inher_const_4<'gcx>(
243    self_ty: TermIn<'gcx>,
244    const_ident: TermIn<'gcx>,
245    const_ty: TermIn<'gcx>,
246    const_id: TermIn<'gcx>,
247    gcx: &'gcx GlobalCx<'gcx>,
248) -> TermIn<'gcx> {
249    Term {
250        functor: Name::with_intern(FUNCTOR_INHER_CONST, gcx),
251        args: [self_ty, const_ident, const_ty, const_id].into(),
252    }
253}
254
255// === ref/n ===
256
257/// `ref/1`
258///
259/// * Arg0 - Type
260///
261/// # Examples
262///
263/// * Code   - &i32
264/// * Output - ref(i32)
265pub fn ref_1<'gcx>(ty: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
266    Term {
267        functor: Name::with_intern(FUNCTOR_REF, gcx),
268        args: [ty].into(),
269    }
270}
271
272// === mut/n ===
273
274/// `mut/1`
275///
276/// * Arg0 - Type
277///
278/// # Examples
279///
280/// * Code   - &mut i32
281/// * Output - ref(mut(i32))
282pub fn mut_1<'gcx>(ty: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
283    Term {
284        functor: Name::with_intern(FUNCTOR_MUT, gcx),
285        args: [ty].into(),
286    }
287}
288
289// === array/n ===
290
291/// `array/1`
292///
293/// * Arg0 - Element type
294///
295/// # Examples
296///
297/// * Code   - \[i32\]
298/// * Output - array(i32, dyn)
299pub fn array_1<'gcx>(elem: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
300    let len = Term {
301        functor: Name::with_intern(FUNCTOR_DYN_ARRAY_LEN, gcx),
302        args: [].into(),
303    };
304    Term {
305        functor: Name::with_intern(FUNCTOR_ARRAY, gcx),
306        args: [elem, len].into(),
307    }
308}
309
310/// `array/2`
311///
312/// * Arg0 - Element type
313/// * Arg1 - Length
314///
315/// # Examples
316///
317/// * Code   - \[i32; 2\]
318/// * Output - array(i32, 2)
319pub fn array_2<'gcx>(
320    elem: TermIn<'gcx>,
321    len: TermIn<'gcx>,
322    gcx: &'gcx GlobalCx<'gcx>,
323) -> TermIn<'gcx> {
324    Term {
325        functor: Name::with_intern(FUNCTOR_ARRAY, gcx),
326        args: [elem, len].into(),
327    }
328}
329
330// === tuple/n ===
331
332/// `tuple/n`
333///
334/// * Args - Element types
335///
336/// # Examples
337///
338/// * Code   - (A, B)
339/// * Output - tuple(A, B)
340pub fn tuple_n<'gcx>(elems: Vec<TermIn<'gcx>>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
341    Term {
342        functor: Name::with_intern(FUNCTOR_TUPLE, gcx),
343        args: elems,
344    }
345}
346
347// === sig/n ===
348
349/// `sig/n`
350///
351/// Creates a term representing a function signature.
352///
353/// * Args - Function parameters (Out, In0, In1, ...)
354///
355/// # Examples
356///
357/// * Code   - (a: In0, b: In1) -> Out
358/// * Output - sig(Out, In0, In1)
359pub fn sig_n<'gcx>(args: Vec<TermIn<'gcx>>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
360    Term {
361        functor: Name::with_intern(FUNCTOR_SIG, gcx),
362        args,
363    }
364}
365
366// === int/n ===
367
368/// `int/1`
369///
370/// * Arg0 - Integer type such as 'i32'
371///
372/// # Examples
373///
374/// * Code   - i32
375/// * Output - int(i32)
376pub fn int_1<'gcx>(int: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
377    Term {
378        functor: Name::with_intern(FUNCTOR_INT, gcx),
379        args: [int].into(),
380    }
381}
382
383// === float/n ===
384
385/// `float/1`
386///
387/// * Arg0 = Floating type such as 'f32'
388///
389/// # Examples
390///
391/// * Code   - f32
392/// * Output - float(f32)
393pub fn float_1<'gcx>(float: TermIn<'gcx>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
394    Term {
395        functor: Name::with_intern(FUNCTOR_FLOAT, gcx),
396        args: [float].into(),
397    }
398}
399
400// === unit/n ===
401
402/// `unit/0`
403///
404/// Type ()
405pub fn unit_0<'gcx>(gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
406    Term {
407        functor: Name::with_intern(FUNCTOR_UNIT, gcx),
408        args: [].into(),
409    }
410}
411
412// === list/n ===
413
414/// `list/n`
415///
416/// Creates a term that wraps the given arguments in.
417///
418/// * Args - Elements
419///
420/// # Examples
421///
422/// * Code   - a::B::<x::Y>::C
423/// * Output - list(a, B(list(x, Y)), C)
424pub fn list_n<'gcx>(elems: Vec<TermIn<'gcx>>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
425    Term {
426        functor: Name::with_intern(FUNCTOR_LIST, gcx),
427        args: elems,
428    }
429}
430
431// === arg/n ===
432
433/// `arg/n`
434///
435/// This allows us to make queries for finding all clauses that share the same functor but not
436/// arity. For example, we can find 'Foo(T)', 'Foo(T, U)' using just one 'Foo(X)' by introducing the
437/// 'arg'.
438///
439/// * Args - Anonymous number of arguments
440///
441/// # Examples
442///
443/// * Code   - Foo<T, U>
444/// * Output - Foo(arg(T, U))
445pub fn arg_n<'gcx>(args: Vec<TermIn<'gcx>>, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
446    Term {
447        functor: Name::with_intern(FUNCTOR_ARG, gcx),
448        args,
449    }
450}
451
452/// # Examples
453///
454/// * path - "a::b::C"
455/// * Output - list(a(arg), b(arg), C(arg))
456pub fn path_to_list<'gcx, T: IntoPathSegments>(path: T, gcx: &'gcx GlobalCx<'gcx>) -> TermIn<'gcx> {
457    let segments = path
458        .segments()
459        .map(|segment| {
460            let empty_arg = arg_n([].into(), gcx);
461            let functor = Name::with_intern(segment.as_ref(), gcx);
462            Term {
463                functor,
464                args: [empty_arg].into(),
465            }
466        })
467        .collect();
468
469    list_n(segments, gcx)
470}
syn_sem/semantic/logic/term.rs

syn_sem/semantic/logic/
term.rs
