hyperon/metta/
types.rs

1//! Contains Rust functions working on types. All MeTTa
2//! specific constants are exported as a part of [metta] module.
3//!
4//! To designate the atom `a` has a type `A` one need add to the space the
5//! expression `(: a A)`. One can also assign a type to type, for example to
6//! designate `A` is a type add `(: A Type)`. `->` is used to create a function
7//! type, for example `(: foo (-> A B))`. Types can also be parameterized by
8//! type or by value. For example list of numbers can be represented as
9//! `(: ns (List Number))`.
10//!
11//! There are five special meta-types: `Atom`, `Symbol`, `Variable`, `Grounded`
12//! and `Expression`. These types should not be assigned explicitly, but they
13//! can be used in type expressions and will be checked. For example one can
14//! define a function which accepts `Atom` as an argument: `(: bar (-> Atom A))`.
15//! When such expression is interpreted the argument is accepted without
16//! reduction (see [metta::interpreter] algorithm).
17//!
18//! When atom has no type assigned by user it has type `%Undefined%`. The value
19//! of `%Undefined%` type can be matched with any type required.
20
21use super::*;
22use hyperon_atom::matcher::{Bindings, BindingsSet, apply_bindings_to_atom_move};
23use hyperon_space::DynSpace;
24
25use std::fmt::{Display, Debug};
26use itertools::Itertools;
27use hyperon_atom::gnd::number::Number;
28
29fn typeof_query(atom: &Atom, typ: &Atom) -> Atom {
30    Atom::expr(vec![HAS_TYPE_SYMBOL, atom.clone(), typ.clone()])
31}
32
33fn isa_query(sub_type: &Atom, super_type: &Atom) -> Atom {
34    Atom::expr(vec![SUB_TYPE_SYMBOL, sub_type.clone(), super_type.clone()])
35}
36
37fn query_has_type(space: &DynSpace, sub_type: &Atom, super_type: &Atom) -> BindingsSet {
38    space.borrow().query(&typeof_query(sub_type, super_type))
39}
40
41fn query_super_types(space: &DynSpace, sub_type: &Atom) -> Vec<Atom> {
42    // TODO: query should check that sub type is a type and not another typed symbol
43    let var_x = VariableAtom::new("X").make_unique();
44    let super_types = space.borrow().query(&isa_query(&sub_type, &Atom::Variable(var_x.clone())));
45    let atom_x = Atom::Variable(var_x);
46    super_types.into_iter().map(|bindings| { apply_bindings_to_atom_move(atom_x.clone(), &bindings) }).collect()
47}
48
49fn add_super_types(space: &DynSpace, sub_types: &mut Vec<Atom>, from: usize) {
50    let mut types = Vec::new();
51    sub_types.iter().skip(from).for_each(|typ| {
52        for typ in query_super_types(space, typ) {
53            if !sub_types.contains(&typ) {
54                types.push(typ);
55            }
56        }
57    });
58    if !types.is_empty() {
59        let from = sub_types.len();
60        sub_types.append(&mut types.clone());
61        add_super_types(space, sub_types, from);
62    }
63}
64
65fn check_arg_types(actual: &[Vec<AtomType>], meta: &[Vec<Atom>], types: &mut Vec<AtomType>, expected: &[Atom], ret_typ: &Atom, atom: &Atom, fn_type_atom: &Atom) -> () {
66    if actual.len() != expected.len() {
67        types.push(AtomType::error(fn_type_atom.clone(), Atom::expr([ERROR_SYMBOL, atom.clone(), INCORRECT_NUMBER_OF_ARGUMENTS_SYMBOL])));
68    } else {
69        check_arg_types_internal(actual, meta, expected, Bindings::new(), types, fn_type_atom, atom, ret_typ, actual.len());
70    }
71}
72
73fn check_arg_types_internal(actual: &[Vec<AtomType>], meta: &[Vec<Atom>], expected: &[Atom], bindings: Bindings, types: &mut Vec<AtomType>, fn_type_atom: &Atom, atom: &Atom, ret_typ: &Atom, start_len: usize) -> () {
74    log::trace!("check_arg_types: actual: {}, expected: {}",
75        actual.iter().format_with(", ", |v, f| f(&format_args!("{}", v.iter().format(", ")))),
76        expected.iter().format(", "));
77
78    match (actual, meta, expected) {
79        ([actual, actual_tail @ ..], [meta, meta_tail @ ..], [expected, expected_tail @ ..]) => {
80            let undefined_or_meta = actual.is_empty()
81                || *expected == ATOM_TYPE_UNDEFINED
82                || meta.contains(expected);
83            let matches: &mut dyn Iterator<Item=Bindings> = if undefined_or_meta {
84                &mut std::iter::once(bindings)
85            } else {
86                &mut actual.into_iter()
87                    .flat_map(|typ| match_reducted_types(typ.as_atom(), expected))
88                    .flat_map(|b| b.merge(&bindings))
89            };
90            let mut matches = matches.peekable();
91            if matches.peek().is_none() {
92                let idx = (start_len - actual_tail.len()) as i64;
93                for typ in actual {
94                    let error = Atom::expr([ERROR_SYMBOL, atom.clone(), Atom::expr([BAD_ARG_TYPE_SYMBOL, Atom::gnd(Number::Integer(idx)), expected.clone(), typ.as_atom().clone()])]);
95                    types.push(AtomType::error(fn_type_atom.clone(), error));
96                }
97            } else {
98                for b in matches {
99                    check_arg_types_internal(actual_tail, meta_tail, expected_tail, b, types, fn_type_atom, atom, ret_typ, start_len);
100                }
101            }
102        },
103        ([], [], []) => {
104            let typ = AtomType::application(apply_bindings_to_atom_move(ret_typ.clone(), &bindings));
105            types.push(typ);
106        },
107        _ => unreachable!(),
108    };
109    log::trace!("check_arg_types: actual: {}, expected: {}",
110        actual.iter().format_with(", ", |v, f| f(&format_args!("{}", v.iter().format(", ")))),
111        expected.iter().format(", "));
112}
113
114/// Returns true if passed type is a type of function.
115///
116/// # Examples
117///
118/// ```
119/// use hyperon_atom::expr;
120/// use hyperon::metta::types::is_func;
121///
122/// assert!(is_func(&expr!("->" "A" "B")));
123/// assert!(!is_func(&expr!("A")));
124/// assert!(!is_func(&expr!(("->"))));
125/// ```
126#[inline]
127pub fn is_func(typ: &Atom) -> bool {
128    match typ {
129        Atom::Expression(expr) => {
130            (expr.children().first() == Some(&ARROW_SYMBOL)) && (expr.children().len() > 1)
131        },
132        _ => false,
133    }
134}
135
136fn query_types(space: &DynSpace, atom: &Atom) -> Vec<Atom> {
137    let var_x = VariableAtom::new("X").make_unique();
138    let types = query_has_type(space, atom, &Atom::Variable(var_x.clone()));
139    let atom_x = Atom::Variable(var_x);
140    let mut types = types.into_iter().filter_map(|bindings| {
141        let atom = apply_bindings_to_atom_move(atom_x.clone(), &bindings);
142        if atom_x == atom || atom == ATOM_TYPE_UNDEFINED {
143            None
144        } else {
145            Some(atom)
146        }
147    }).collect();
148    add_super_types(space, &mut types, 0);
149    types
150}
151
152/// Splits function type on array of argument types and return type.
153fn get_arg_types<'a>(fn_typ: &'a AtomType) -> (&'a [Atom], &'a Atom) {
154    match fn_typ.as_atom() {
155        Atom::Expression(expr) => {
156            let children = expr.children();
157            match children {
158                [op,  args @ .., res] if *op == ARROW_SYMBOL => (args, res),
159                _ => panic!("Incorrect function type: {}", fn_typ)
160            }
161        },
162        _ => panic!("Incorrect function type: {}", fn_typ)
163    }
164}
165
166fn get_args(expr: &ExpressionAtom) -> &[Atom] {
167    &expr.children()[1..]
168}
169
170#[derive(Debug, PartialEq, Clone)]
171pub struct AtomType {
172    typ: Atom,
173    is_function: bool,
174    info: TypeInfo,
175}
176
177#[derive(Debug, PartialEq, Clone)]
178enum TypeInfo {
179    Application,
180    ApplicationError {
181        error: Atom,
182    },
183    Value,
184}
185
186impl AtomType {
187
188    #[inline]
189    pub fn undefined() -> Self {
190        Self {
191            typ: ATOM_TYPE_UNDEFINED,
192            is_function: false,
193            info: TypeInfo::Value,
194        }
195    }
196
197    #[inline]
198    pub fn value(typ: Atom) -> Self {
199        let is_function = is_func(&typ);
200        Self {
201            typ,
202            is_function,
203            info: TypeInfo::Value,
204        }
205    }
206
207    #[inline]
208    pub fn application(typ: Atom) -> Self {
209        let is_function = is_func(&typ);
210        Self {
211            typ,
212            is_function,
213            info: TypeInfo::Application,
214        }
215    }
216
217    #[inline]
218    pub fn error(typ: Atom, error: Atom) -> Self {
219        let is_function = is_func(&typ);
220        Self {
221            typ,
222            is_function,
223            info: TypeInfo::ApplicationError {
224                error,
225            }
226        }
227    }
228
229    #[inline]
230    pub fn is_error(&self) -> bool {
231        matches!(self.info, TypeInfo::ApplicationError{..})
232    }
233
234    #[inline]
235    pub fn is_valid(&self) -> bool {
236        !self.is_error()
237    }
238
239    #[inline]
240    pub fn is_function(&self) -> bool {
241        self.is_function
242    }
243    #[inline]
244    pub fn is_application(&self) -> bool {
245        matches!(self.info, TypeInfo::Application)
246    }
247
248    #[inline]
249    pub fn as_atom(&self) -> &Atom {
250        &self.typ
251    }
252
253    #[inline]
254    pub fn into_atom(self) -> Atom {
255        self.typ
256    }
257
258    #[inline]
259    pub fn get_error(&self) -> Option<&Atom> {
260        match &self.info {
261            TypeInfo::ApplicationError { error } => Some(error),
262            _ => None,
263        }
264    }
265
266    #[inline]
267    pub fn into_error(self) -> Option<Atom> {
268        match self.info {
269            TypeInfo::ApplicationError { error } => Some(error),
270            _ => None,
271        }
272    }
273
274    #[inline]
275    pub fn into_error_unchecked(self) -> Atom {
276        match self.info {
277            TypeInfo::ApplicationError { error } => error,
278            _ => panic!("Unexpected state"),
279        }
280    }
281
282    #[inline]
283    pub fn into_atom_or_error(self) -> Result<Atom, Atom>  {
284        match self.info {
285            TypeInfo::ApplicationError { error } => Err(error),
286            _ => Ok(self.typ),
287        }
288    }
289}
290
291impl Display for AtomType {
292    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
293        write!(f, "{}(", self.typ)
294            .and_then(|r| if self.is_application() { write!(f, "A") } else { Ok(r) })
295            .and_then(|r| if self.is_error() { write!(f, "E") } else { Ok(r) })
296            .and_then(|_| write!(f, ")"))
297    }
298}
299
300/// Returns vector of the types for the given `atom` in context of the given
301/// `space`. Returns [`%Undefined%`] if atom has no type assigned.
302/// # Examples
303///
304/// ```
305/// use hyperon_common::assert_eq_no_order;
306/// use hyperon_atom::Atom;
307/// use hyperon_macros::metta;
308/// use hyperon_space::DynSpace;
309/// use hyperon::space::grounding::GroundingSpace;
310/// use hyperon::metta::types::{AtomType, get_atom_types};
311///
312/// let mut space = GroundingSpace::new();
313/// space.add(metta!((: f (-> A B))));
314/// space.add(metta!((: a A)));
315/// space.add(metta!((: a B)));
316/// space.add(metta!((: b B)));
317///
318/// let space = DynSpace::from(space);
319/// assert_eq_no_order!(get_atom_types(&space, &metta!($x)), vec![AtomType::undefined()]);
320/// assert_eq_no_order!(get_atom_types(&space, &metta!(1)), vec![AtomType::value(metta!(Number))]);
321/// assert_eq_no_order!(get_atom_types(&space, &metta!(na)), vec![AtomType::undefined()]);
322/// assert_eq_no_order!(get_atom_types(&space, &metta!(a)), vec![AtomType::value(metta!(A)), AtomType::value(metta!(B))]);
323/// assert_eq_no_order!(get_atom_types(&space, &metta!((a b))), vec![AtomType::value(metta!((A B))), AtomType::value(metta!((B B)))]);
324/// assert_eq_no_order!(get_atom_types(&space, &metta!((f a))), vec![AtomType::application(metta!(B))]);
325/// assert_eq_no_order!(get_atom_types(&space, &metta!((f b))), vec![AtomType::error(metta!((-> A B)), metta!((Error (f b) (BadArgType 1 A B))))]);
326/// ```
327pub fn get_atom_types(space: &DynSpace, atom: &Atom) -> Vec<AtomType> {
328    let atom_types = get_atom_types_internal(space, atom);
329    if atom_types.is_empty() {
330        vec![AtomType::undefined()]
331    } else {
332        atom_types
333    }
334}
335
336struct ExprTypeInfo {
337    op_value_types: Vec<AtomType>,
338    op_func_types: Vec<AtomType>,
339    arg_types: Vec<Vec<AtomType>>,
340}
341
342impl ExprTypeInfo {
343    fn new(space: &DynSpace, expr: &ExpressionAtom) -> Self {
344        let (op, args) = expr.children().split_first().unwrap();
345        let op_types = get_atom_types_internal(space, op);
346        let mut op_func_types = Vec::with_capacity(op_types.len());
347        let mut op_value_types = Vec::with_capacity(op_types.len());
348        op_types.into_iter().for_each(|t| {
349            if t.is_function() {
350                op_func_types.push(t);
351            } else {
352                op_value_types.push(t);
353            }
354        });
355        let arg_types: Vec<Vec<AtomType>> = args.iter()
356            .map(|a| get_atom_types_internal(space, a)).collect();
357            // Code below allows returning partially defined tuples
358            // for example (a c) where (: a A) has type (A %Undefined%)
359            // see get_atom_types_tuple test
360            //.map(|a| {
361                //let mut types = get_atom_types_internal(space, a);
362                //if types.is_empty() {
363                    //types.push(AtomType::value(ATOM_TYPE_UNDEFINED));
364                //}
365                //types
366            //}).collect();
367        Self{ op_value_types, op_func_types, arg_types }
368    }
369
370    #[inline]
371    fn arity(&self) -> usize {
372        self.arg_types.len() + 1
373    }
374}
375
376fn get_atom_types_internal(space: &DynSpace, atom: &Atom) -> Vec<AtomType> {
377    log::trace!("get_atom_types_internal: atom: {}", atom);
378    let types = match atom {
379        // TODO: type of the variable could be actually a type variable,
380        // in this case inside each variant of type for the atom we should
381        // also keep bindings for the type variables. For example,
382        // we have an expression `(let $n (foo) (+ $n $n))`, where
383        // `(: let (-> $t $t $r $r))`, `(: foo (-> $tt))`,
384        // and `(: + (-> Num Num Num))`then type checker can find that
385        // `{ $r = $t = $tt = Num }`.
386        Atom::Variable(_) => vec![],
387        Atom::Grounded(gnd) => {
388            let typ = gnd.type_();
389            if typ == ATOM_TYPE_UNDEFINED {
390                vec![]
391            } else {
392                vec![AtomType::value(make_variables_unique(gnd.type_()))]
393            }
394        },
395        Atom::Symbol(_) => query_types(space, atom).into_iter()
396            .map(AtomType::value).collect(),
397        // TODO: empty expression should have unit type (->), but type checking
398        // code cannot handle functional type which doesn't return value
399        Atom::Expression(expr) if expr.children().len() == 0 => vec![],
400        Atom::Expression(expr) => {
401            let type_info = ExprTypeInfo::new(space, expr);
402            let mut types = get_tuple_types(space, atom, &type_info);
403            let applications = get_application_types(atom, expr, type_info);
404            types.extend(applications.into_iter());
405            types
406        },
407    };
408    log::debug!("get_atom_types_internal: return atom {} types {}", atom, types.iter().format(", "));
409    types
410}
411
412struct TupleIndex<'a> {
413    type_info: &'a ExprTypeInfo,
414    index: Vec<usize>,
415    max: Vec<usize>,
416    size: usize,
417}
418
419impl<'a> TupleIndex<'a> {
420    fn new(type_info: &'a ExprTypeInfo) -> Option<Self> {
421        let n_of_types = type_info.arg_types.iter()
422            .fold(type_info.op_value_types.len(), |n, types| n * types.len());
423        if n_of_types == 0 {
424            return None
425        }
426        let arity = type_info.arity();
427        let mut max = Vec::with_capacity(arity);
428        max.push(type_info.op_value_types.len());
429        max.extend(type_info.arg_types.iter().map(Vec::len));
430        let mut index = vec![0; arity];
431        index[arity - 1] = usize::wrapping_sub(index[arity - 1], 1);
432        Some(Self{ type_info, index, max, size: n_of_types })
433    }
434
435    #[inline]
436    fn inc(&mut self) -> bool {
437        let mut i = self.index.len() - 1;
438        loop {
439            let d = usize::wrapping_add(self.index[i], 1);
440            if d < self.max[i] {
441                self.index[i] = d;
442                return true;
443            } else {
444                if i == 0 {
445                    return false;
446                } else {
447                    self.index[i] = 0;
448                    i -= 1;
449                }
450            }
451        }
452    }
453
454    #[inline]
455    fn size(&self) -> usize {
456        self.size
457    }
458}
459
460impl<'a> Iterator for TupleIndex<'a> {
461    type Item = Vec<Atom>;
462    fn next(&mut self) -> Option<Self::Item> {
463        if self.inc() {
464            let arity = self.index.len();
465            let mut v = Vec::with_capacity(arity);
466            v.push(self.type_info.op_value_types[self.index[0]].as_atom().clone());
467            for i in 1..arity {
468                v.push(self.type_info.arg_types[i - 1][self.index[i]].as_atom().clone());
469            }
470            Some(v)
471        } else {
472            None
473        }
474    }
475}
476
477fn get_tuple_types(space: &DynSpace, atom: &Atom, type_info: &ExprTypeInfo) -> Vec<AtomType> {
478    let mut types = if let Some(index) = TupleIndex::new(type_info) {
479        let mut types = Vec::with_capacity(index.size());
480        index.for_each(|v| types.push(Atom::expr(v)));
481        types
482    } else {
483        vec![]
484    };
485
486    types.append(&mut query_types(space, atom));
487    add_super_types(space, &mut types, 0);
488    // FIXME: ineffective
489    let types: Vec<AtomType> = types.into_iter().map(AtomType::value).collect();
490    log::trace!("get_tuple_types: tuple {} types {}", atom, types.iter().format(", "));
491    types
492}
493
494// TODO: Three cases here:
495// 1. function call types are not found
496// 2. function call type with correct arg types are found
497// 3. only function call type with incorrect arg types are found
498//
499// In (1) we should return `vec![ Undefined ]` from `get_atom_types()` when no types found;
500// In (2) we should return the type which function returns but types are never empty;
501// In (3) we should return empty `Vec` when types are empty, because `validate_atom()` expects
502// empty `Vec` when atom is incorrectly typed.
503//
504// Thus we divide these three cases in a return value of the function:
505// - `None` corresponds to the first case
506// - `Some(vec![...])` corresponds to the second case
507// - `Some(vec![])` corresponds to the third case
508//
509// This is a tricky logic. To simplify it we could  separate tuple and
510// function application using separate Atom types. Or use an embedded atom
511// to designate function application.
512fn get_application_types(atom: &Atom, expr: &ExpressionAtom, type_info: ExprTypeInfo) -> Vec<AtomType> {
513    let args = get_args(expr);
514    let meta_arg_types: Vec<Vec<Atom>> = args.iter().map(|a| vec![get_meta_type(a), ATOM_TYPE_ATOM]).collect();
515    let mut types = Vec::with_capacity(type_info.op_func_types.len());
516    for fn_type in type_info.op_func_types.into_iter() {
517        let (expected, ret_typ) = get_arg_types(&fn_type);
518        let fn_type_atom = fn_type.as_atom();
519        check_arg_types(&type_info.arg_types, meta_arg_types.as_slice(), &mut types, expected, ret_typ, atom, fn_type_atom);
520    }
521    log::trace!("get_application_types: function application {} types {}", atom, types.iter().format(", "));
522    types
523}
524
525#[derive(Clone, PartialEq, Debug)]
526struct UndefinedTypeMatch { }
527
528impl Display for UndefinedTypeMatch {
529    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
530        write!(f, "{}", ATOM_TYPE_UNDEFINED)
531    }
532}
533
534impl Grounded for UndefinedTypeMatch {
535    fn type_(&self) -> Atom {
536        ATOM_TYPE_TYPE
537    }
538
539    fn as_match(&self) -> Option<&dyn CustomMatch> {
540        Some(self)
541    }
542}
543
544impl CustomMatch for UndefinedTypeMatch {
545    fn match_(&self, _other: &Atom) -> matcher::MatchResultIter {
546        Box::new(std::iter::once(hyperon_atom::matcher::Bindings::new()))
547    }
548}
549
550/// Matches two types and returns an iterator over resulting bindings.
551///
552/// # Examples
553///
554/// ```
555/// use hyperon_atom::{expr, bind};
556/// use hyperon_atom::matcher::Bindings;
557/// use hyperon::metta::types::match_reducted_types;
558///
559/// let bindings: Vec<Bindings> = match_reducted_types(&expr!("List" t), &expr!("List" "A")).collect();
560///
561/// assert_eq!(bindings, vec![ bind!{ t: expr!("A") } ]);
562/// ```
563pub fn match_reducted_types(left: &Atom, right: &Atom) -> matcher::MatchResultIter {
564    let left = replace_undefined_types(left);
565    let right = replace_undefined_types(right);
566    matcher::match_atoms(&left, &right)
567}
568
569fn replace_undefined_types(atom: &Atom) -> Atom {
570    let mut atom = atom.clone();
571    atom.iter_mut().filter(|atom| **atom == ATOM_TYPE_UNDEFINED)
572        .for_each(|atom| *atom = Atom::gnd(UndefinedTypeMatch{}));
573    atom
574}
575
576fn get_matched_types(space: &DynSpace, atom: &Atom, typ: &Atom) -> Vec<(Atom, Bindings)> {
577    let types = get_atom_types(space, atom);
578    types.into_iter().filter(AtomType::is_valid).flat_map(|t| {
579        // TODO: write a unit test
580        let t = make_variables_unique(t.into_atom());
581        match_reducted_types(&t, typ).map(move |bindings| (t.clone(), bindings))
582    }).collect()
583}
584
585/// Checks if passed `atom` has the given `typ` in context of the given `space`.
586/// This function can be used for a simple type check when there is no need
587/// to know type parameters.
588///
589/// # Examples
590///
591/// ```
592/// use hyperon_atom::expr;
593/// use hyperon::metta::runner::*;
594/// use hyperon::metta::text::SExprParser;
595/// use hyperon::metta::types::check_type;
596///
597/// let metta = Metta::new(None);
598/// metta.run(SExprParser::new("(: a A) (: a B)")).unwrap();
599///
600/// assert!(check_type(&metta.space(), &expr!("a"), &expr!("B")));
601/// ```
602pub fn check_type(space: &DynSpace, atom: &Atom, typ: &Atom) -> bool {
603    check_meta_type(atom, typ) || !get_matched_types(space, atom, typ).is_empty()
604}
605
606pub fn get_meta_type(atom: &Atom) -> Atom {
607    match atom {
608        Atom::Symbol(_) => ATOM_TYPE_SYMBOL,
609        Atom::Variable(_) => ATOM_TYPE_VARIABLE,
610        Atom::Grounded(_) => ATOM_TYPE_GROUNDED,
611        Atom::Expression(_) => ATOM_TYPE_EXPRESSION,
612    }
613}
614
615fn check_meta_type(atom: &Atom, typ: &Atom) -> bool {
616    *typ == ATOM_TYPE_ATOM || *typ == get_meta_type(atom)
617}
618
619/// Returns true if atom is typed correctly. For example it can be used to
620/// check if function arguments have correct types.
621///
622/// # Examples
623///
624/// ```
625/// use hyperon_atom::expr;
626/// use hyperon::metta::runner::*;
627/// use hyperon::metta::text::SExprParser;
628/// use hyperon::metta::types::validate_atom;
629///
630/// let metta = Metta::new(None);
631/// metta.run(SExprParser::new("(: foo (-> A B)) (: a A) (: b B)")).unwrap();
632///
633/// let space = metta.space();
634/// assert!(validate_atom(&space, &expr!("foo" "a")));
635/// assert!(!validate_atom(&space, &expr!("foo" "b")));
636/// ```
637pub fn validate_atom(space: &DynSpace, atom: &Atom) -> bool {
638    get_atom_types_internal(space, atom).iter().all(AtomType::is_valid)
639}
640
641#[cfg(test)]
642mod tests {
643    use super::*;
644    use hyperon_atom::matcher::atoms_are_equivalent;
645    use crate::metta::runner::*;
646    use crate::metta::text::SExprParser;
647    use hyperon_common::assert_eq_no_order;
648    use hyperon_macros::metta;
649
650    macro_rules! typ {
651        ($($typ:tt)*) => { AtomType::value(metta!($($typ)*)) }
652    }
653    macro_rules! typ_app {
654        ($($typ:tt)*) => { AtomType::application(metta!($($typ)*)) }
655    }
656    macro_rules! typ_err {
657        ($typ:tt , $err:tt) => { AtomType::error(metta!($typ), metta!($err)) }
658    }
659
660    fn metta_space(text: &str) -> DynSpace {
661        let metta = Metta::new(Some(EnvBuilder::test_env()));
662        let mut space = GroundingSpace::new();
663        let mut parser = SExprParser::new(text);
664        while let Some(atom) = parser.parse(&*metta.tokenizer().borrow()).unwrap() {
665            space.add(atom);
666        }
667        space.into()
668    }
669
670    fn atom(atom_str: &str) -> Atom {
671        let metta = Metta::new(Some(EnvBuilder::test_env()));
672        let mut parser = SExprParser::new(atom_str);
673        let atom = parser.parse(&*metta.tokenizer().borrow()).unwrap().expect("Single atom is expected");
674        atom
675    }
676
677    fn grammar_space() -> DynSpace {
678        let mut space = GroundingSpace::new();
679        space.add(expr!(":" "answer" ("->" "Sent" "Sent")));
680        space.add(expr!(":<" "Quest" "Sent"));
681        space.add(expr!(":<" ("Aux" "Subj" "Verb" "Obj") "Quest"));
682        space.add(expr!(":<" "Pron" "Subj"));
683        space.add(expr!(":<" "NG" "Subj"));
684        space.add(expr!(":<" "Pron" "Obj"));
685        space.add(expr!(":<" "NG" "Obj"));
686        space.add(expr!(":<" ("Det" "Noun") "NG"));
687        space.add(expr!(":" "you" "Pron"));
688        space.add(expr!(":" "do" "Aux"));
689        space.add(expr!(":" "do" "Verb"));
690        space.add(expr!(":" "like" "Verb"));
691        space.add(expr!(":" "a" "Det"));
692        space.add(expr!(":" "pizza" "Noun"));
693        space.into()
694    }
695
696    #[test]
697    fn test_check_type() {
698        let mut space = GroundingSpace::new();
699        space.add(expr!(":" "do" "Verb"));
700        space.add(expr!(":" "do" "Aux"));
701        let space = space.into();
702
703        let aux = sym!("Aux");
704        let verb = sym!("Verb");
705
706        let nonsense = sym!("nonsense");
707        assert!(check_type(&space, &nonsense, &ATOM_TYPE_UNDEFINED));
708        assert!(check_type(&space, &nonsense, &aux));
709
710        let _do = sym!("do");
711        assert!(check_type(&space, &_do, &ATOM_TYPE_UNDEFINED));
712        assert!(check_type(&space, &_do, &aux));
713        assert!(check_type(&space, &_do, &verb));
714        assert!(!check_type(&space, &_do, &sym!("Noun")));
715
716    }
717
718    #[test]
719    fn test_check_expr_type() {
720        let mut space = GroundingSpace::new();
721        space.add(expr!(":" "i" "Pron"));
722        space.add(expr!(":" "like" "Verb"));
723        space.add(expr!(":" "music" "Noun"));
724        space.add(expr!(":" ("do" "you" "like" "music") "Quest"));
725        space.add(expr!(":<" ("Pron" "Verb" "Noun") "Statement"));
726        let space = space.into();
727
728        let i_like_music = expr!("i" "like" "music");
729        assert!(check_type(&space, &i_like_music, &ATOM_TYPE_UNDEFINED));
730        assert!(check_type(&space, &i_like_music, &expr!("Pron" "Verb" "Noun")));
731        assert!(check_type(&space, &i_like_music, &sym!("Statement")));
732
733        assert!(check_type(&space, &expr!("do" "you" "like" "music"), &sym!("Quest")));
734    }
735
736    #[test]
737    fn nested_type() {
738        let space = metta_space("
739            (: a A)
740            (:< A B)
741            (:< B C)
742            (:< C D)
743        ");
744
745        assert!(check_type(&space, &atom("a"), &atom("D")));
746    }
747
748    #[test]
749    fn nested_loop_type() {
750        let space = metta_space("
751            (:< B A)
752            (: a A)
753            (:< A B)
754            (:< B C)
755        ");
756
757        assert!(check_type(&space, &atom("a"), &atom("C")));
758    }
759
760    #[test]
761    fn test_validate_atom() {
762        let space = grammar_space();
763        let expr = expr!("answer" ("do" "you" "like" ("a" "pizza")));
764
765        assert!(validate_atom(&space, &expr));
766    }
767
768    #[test]
769    fn validate_symbol() {
770        let space = DynSpace::new(GroundingSpace::new());
771        assert!(validate_atom(&space, &sym!("a")));
772    }
773
774    #[test]
775    fn simple_types() {
776        let space = metta_space("
777            (: blue Color)
778            (: balloon Object)
779        ");
780
781        assert!(check_type(&space, &atom("(blue balloon)"),
782            &atom("(Color Object)")));
783    }
784
785    #[test]
786    fn arrow_type() {
787        let space = metta_space("
788            (: a (-> B A))
789        ");
790
791        assert!(check_type(&space, &atom("a"), &atom("(-> B A)")));
792    }
793
794    #[test]
795    fn arrow_allows_specific_type() {
796        let space = metta_space("
797            (: a (-> B A))
798            (: b B)
799            (: c C)
800        ");
801
802        assert!(validate_atom(&space, &atom("(a b)")));
803        assert!(check_type(&space, &atom("(a b)"), &ATOM_TYPE_UNDEFINED));
804        assert!(!validate_atom(&space, &atom("(a c)")));
805        assert!(!check_type(&space, &atom("(a c)"), &ATOM_TYPE_UNDEFINED));
806    }
807
808    #[test]
809    fn validate_basic_expr() {
810        let space = DynSpace::new(GroundingSpace::new());
811        assert!(validate_atom(&space, &expr!({5})));
812        assert!(validate_atom(&space, &expr!("+" {3} {5})));
813        assert!(validate_atom(&space, &expr!("=" ("f" x) x)));
814    }
815
816    #[test]
817    fn simple_dep_types() {
818        let space = metta_space("
819            (: = (-> $t $t Prop))
820            (: Entity Prop)
821            (: Human (-> Entity Prop))
822            (: Socrates Entity)
823            (: (Human Socrates) Prop)
824            (: Plato Entity)
825            (: Mortal (-> Entity Prop))
826            (: HumansAreMortal (-> (Human $t) (Mortal $t)))
827            (: Time NotEntity)
828            (: SocratesIsHuman (Human Socrates))
829            (: SocratesIsMortal (Mortal Socrates))
830        ");
831        let t = &atom("Prop");
832        assert!(check_type(&space, &atom("(Human Socrates)"), t));
833        assert!(check_type(&space, &atom("(Human Plato)"), t));
834        assert!(!check_type(&space, &atom("(Human Time)"), t));
835        assert!(!validate_atom(&space, &atom("(Human Time)")));
836        assert!(!check_type(&space, &atom("(Human Time)"), &atom("((-> Entity Prop) NotEntity)")));
837        assert!(check_type(&space, &atom("(= Socrates Socrates)"), t));
838        assert!(check_type(&space, &atom("(= Socrates Plato)"), t));
839        assert!(check_type(&space, &atom("(= Socrates Untyped)"), t));
840        assert!(!check_type(&space, &atom("(= Socrates Time)"), t));
841
842        assert!(validate_atom(&space, &atom("(HumansAreMortal SocratesIsHuman)")));
843        assert!(!validate_atom(&space, &atom("(HumansAreMortal (Human Socrates))")));
844        assert!(!validate_atom(&space, &atom("(HumansAreMortal (Human Plato))")));
845        assert!(!validate_atom(&space, &atom("(HumansAreMortal (Human Time))")));
846        assert!(!validate_atom(&space, &atom("(HumansAreMortal Human)")));
847        assert!(!check_type(&space, &atom("(HumansAreMortal (Human Socrates))"),
848                            &atom("(Mortal Socrates)")));
849        assert!(check_type(&space, &atom("(HumansAreMortal SocratesIsHuman)"),
850                           &atom("(Mortal Socrates)")));
851
852        assert!(!validate_atom(&space, &atom("(= SocratesIsHuman (Human Socrates))")));
853        assert!(!validate_atom(&space, &atom("(= SocratesIsHuman (Human Plato))")));
854        assert!(!check_type(&space, &atom("(= SocratesIsHuman (Human Socrates))"), t));
855        assert!(!validate_atom(&space, &atom("(= SocratesIsHuman (Human Time))")));
856        assert!(validate_atom(&space, &atom("(= SocratesIsMortal (HumansAreMortal SocratesIsHuman))")));
857        assert!(validate_atom(&space, &atom("(= (Mortal Socrates) (Mortal Plato))")));
858    }
859
860    #[test]
861    fn dep_types_prop() {
862        let space = metta_space("
863            (: Sam Entity)
864            (: Frog (-> Entity Prop))
865            (: Green (-> Entity Prop))
866            (: Croaks (-> Entity Prop))
867            (: GreenAndCroaksIsFrog (-> (Green $t) (Croaks $t) (Frog $t)))
868            (: SamIsGreen (Green Sam))
869            (: SamCroaks (Croaks Sam))
870        ");
871        assert!(validate_atom(&space, &atom("(GreenAndCroaksIsFrog SamIsGreen SamCroaks)")));
872        assert!(check_type(&space, &atom("(GreenAndCroaksIsFrog SamIsGreen SamCroaks)"),
873                           &atom("(Frog Sam)")));
874    }
875
876    #[test]
877    fn arrow_allows_undefined_type() {
878        let space = metta_space("
879            (: a (-> B A))
880        ");
881
882        assert!(validate_atom(&space, &atom("(a b)")));
883    }
884
885    #[test]
886    fn arrow_has_type_of_returned_value() {
887        let space = metta_space("
888            (: a (-> B A))
889            (: b B)
890        ");
891
892        assert!(check_type(&space, &atom("(a b)"), &atom("A")));
893    }
894
895    #[test]
896    fn nested_arrow_type() {
897        let space = metta_space("
898            (: a (-> B A))
899            (: h (-> (-> B A) C))
900        ");
901
902        assert!(validate_atom(&space, &atom("(h a)")));
903    }
904
905    #[test]
906    fn nested_return_type() {
907        let space = metta_space("
908            (: a (-> B A))
909            (: b B)
910            (: h (-> A C))
911        ");
912
913        assert!(validate_atom(&space, &atom("(h (a b))")));
914    }
915
916    #[test]
917    fn validate_non_functional_expression() {
918        let space = metta_space("
919            (: a A)
920            (: b B)
921        ");
922
923        assert!(validate_atom(&space, &atom("(a b)")));
924    }
925
926    #[test]
927    fn check_type_non_functional_expression() {
928        let space = metta_space("
929            (: a (-> C D))
930            (: a A)
931            (: b B)
932        ");
933
934        assert!(check_type(&space, &atom("(a b)"), &atom("(A B)")));
935    }
936
937    #[test]
938    fn get_atom_types_symbol() {
939        let space = metta_space("
940            (: a A)
941            (: a AA)
942        ");
943        assert_eq_no_order!(get_atom_types(&space, &atom("a")), vec![typ!(A), typ!(AA)]);
944        assert_eq_no_order!(get_atom_types(&space, &atom("b")), vec![AtomType::undefined()]);
945    }
946
947    #[test]
948    fn get_atom_types_variable() {
949        let space = DynSpace::new(GroundingSpace::new());
950        assert_eq!(get_atom_types(&space, &atom("$x")), vec![AtomType::undefined()]);
951    }
952
953    #[test]
954    fn get_atom_types_grounded_atom() {
955        let space = DynSpace::new(GroundingSpace::new());
956        assert_eq!(get_atom_types(&space, &Atom::value(3)), vec![typ!(i32)]);
957    }
958
959    #[derive(Debug, Clone, PartialEq)]
960    struct GroundedAtomWithParameterizedType(Atom);
961
962    impl std::fmt::Display for GroundedAtomWithParameterizedType {
963        fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
964            write!(f, "GroundedAtomWithParameterizedType({})", self.0)
965        }
966    }
967
968    impl Grounded for GroundedAtomWithParameterizedType {
969        fn type_(&self) -> Atom {
970            self.0.clone()
971        }
972    }
973
974    #[test]
975    fn get_atom_types_variables_are_substituted_for_grounded_atom_type() {
976        let actual_type = Atom::var("t");
977        let gnd = GroundedAtomWithParameterizedType(actual_type.clone());
978        let resolved_type = get_atom_types(&GroundingSpace::new().into(), &Atom::gnd(gnd));
979        assert_eq!(resolved_type.len(), 1);
980        assert!(resolved_type[0].is_valid());
981        assert_ne!(resolved_type[0].as_atom(), &actual_type);
982        assert!(atoms_are_equivalent(resolved_type[0].as_atom(), &actual_type));
983    }
984
985    #[test]
986    fn parameterized_atom_types_should_not_conflict() {
987        let actual_type = Atom::expr([ARROW_SYMBOL, Atom::var("t"), Atom::var("t")]);
988        let gnd_1 = GroundedAtomWithParameterizedType(actual_type.clone());
989        let gnd_2 = GroundedAtomWithParameterizedType(actual_type.clone());
990        let resolved_type_1 = get_atom_types(&GroundingSpace::new().into(), &Atom::gnd(gnd_1));
991        let resolved_type_2 = get_atom_types(&GroundingSpace::new().into(), &Atom::gnd(gnd_2));
992
993        //Types of gnd_1 and gnd_2 are different in the space
994        assert_ne!(resolved_type_1, resolved_type_2);
995
996        //But the types are still equivalent
997        assert_eq!(resolved_type_1.len(), 1);
998        assert_eq!(resolved_type_2.len(), 1);
999        assert!(resolved_type_1[0].is_valid());
1000        assert!(resolved_type_2[0].is_valid());
1001        assert!(atoms_are_equivalent(resolved_type_1[0].as_atom(), &actual_type));
1002        assert!(atoms_are_equivalent(resolved_type_2[0].as_atom(), &actual_type));
1003        assert!(atoms_are_equivalent(resolved_type_1[0].as_atom(), resolved_type_2[0].as_atom()));
1004    }
1005
1006    #[test]
1007    fn get_atom_types_tuple() {
1008        let space = metta_space("
1009            (: a A)
1010            (: a AA)
1011            (: b B)
1012            (: b BB)
1013        ");
1014        assert_eq_no_order!(get_atom_types(&space, &metta!((a b))),
1015            vec![typ!((A B)), typ!((AA B)), typ!((A BB)), typ!((AA BB))]);
1016        assert_eq_no_order!(get_atom_types(&space, &metta!((a c))),
1017            vec![AtomType::undefined()]);
1018        assert_eq_no_order!(get_atom_types(&space, &metta!((c d))), vec![AtomType::undefined()]);
1019    }
1020
1021    #[test]
1022    fn get_atom_types_function_call_and_tuple() {
1023        let space = metta_space("
1024            (: a (-> B C))
1025            (: a A)
1026            (: b B)
1027        ");
1028        assert_eq!(get_atom_types(&space, &metta!((a b))), vec![typ!((A B)), typ_app!(C)]);
1029    }
1030
1031    #[test]
1032    fn get_atom_types_empty_expression() {
1033        let space = DynSpace::new(GroundingSpace::new());
1034        assert_eq!(get_atom_types(&space, &Atom::expr([])), vec![AtomType::undefined()]);
1035    }
1036
1037    #[test]
1038    fn get_atom_types_function_call_simple() {
1039        let space = metta_space("
1040            (: f (-> B C))
1041            (: b B)
1042        ");
1043        assert_eq!(get_atom_types(&space, &atom("(f b)")), vec![typ_app!(C)]);
1044        assert_eq!(get_atom_types(&space, &atom("(f a)")), vec![typ_app!(C)]);
1045    }
1046
1047    #[test]
1048    fn get_atom_types_function_call_meta_types() {
1049        let space = metta_space("
1050            (: f_atom (-> Atom D))
1051            (: f_expr (-> Expression D))
1052            (: f_var (-> Variable D))
1053            (: f_sym (-> Symbol D))
1054            (: f_gnd (-> Grounded D))
1055            (: b B)
1056        ");
1057        assert_eq!(get_atom_types(&space, &metta!((f_atom b))), vec![typ_app!(D)]);
1058        assert_eq!(get_atom_types(&space, &metta!((f_sym b))), vec![typ_app!(D)]);
1059        assert_eq!(get_atom_types(&space, &metta!((f_expr b))), vec![typ_err!((-> Expression D) , (Error (f_expr b) (BadArgType 1 Expression B)))]);
1060        assert_eq!(get_atom_types(&space, &metta!((f_var b))), vec![typ_err!((-> Variable D) , (Error (f_var b) (BadArgType 1 Variable B)))]);
1061        assert_eq!(get_atom_types(&space, &metta!((f_gnd b))), vec![typ_err!((-> Grounded D) , (Error (f_gnd b) (BadArgType 1 Grounded B)))]);
1062
1063        assert_eq!(get_atom_types(&space, &metta!((f_atom $b))), vec![typ_app!(D)]);
1064        //assert_eq!(get_atom_types(&space, &metta!((f_sym $b))), vec![]);
1065        //assert_eq!(get_atom_types(&space, &metta!((f_expr $b))), vec![]);
1066        assert_eq!(get_atom_types(&space, &metta!((f_var $b))), vec![typ_app!(D)]);
1067        //assert_eq!(get_atom_types(&space, &metta!((f_gnd $b))), vec![]);
1068
1069        assert_eq!(get_atom_types(&space, &metta!((f_atom (b)))), vec![typ_app!(D)]);
1070        // Here and below: when interpreter cannot find a function type for
1071        // expression it evaluates it. Thus any argument expression without
1072        // a function type can potentially suit as a legal argument.
1073        assert_eq!(get_atom_types(&space, &metta!((f_sym (b)))), vec![typ_err!((-> Symbol D) , (Error (f_sym (b)) (BadArgType 1 Symbol (B))))]);
1074        assert_eq!(get_atom_types(&space, &metta!((f_expr (b)))), vec![typ_app!(D)]);
1075        assert_eq!(get_atom_types(&space, &metta!((f_var (b)))), vec![typ_err!((-> Variable D) , (Error (f_var (b)) (BadArgType 1 Variable (B))))]);
1076        assert_eq!(get_atom_types(&space, &metta!((f_gnd (b)))), vec![typ_err!((-> Grounded D) , (Error (f_gnd (b)) (BadArgType 1 Grounded (B))))]);
1077
1078        assert_eq!(get_atom_types(&space, &metta!((f_atom 1))), vec![typ_app!(D)]);
1079        assert_eq!(get_atom_types(&space, &metta!((f_sym 1))), vec![typ_err!((-> Symbol D) , (Error (f_sym 1) (BadArgType 1 Symbol Number)))]);
1080        assert_eq!(get_atom_types(&space, &metta!((f_expr 1))), vec![typ_err!((-> Expression D) , (Error (f_expr 1) (BadArgType 1 Expression Number)))]);
1081        assert_eq!(get_atom_types(&space, &metta!((f_var 1))), vec![typ_err!((-> Variable D) , (Error (f_var 1) (BadArgType 1 Variable Number)))]);
1082        assert_eq!(get_atom_types(&space, &metta!((f_gnd 1))), vec![typ_app!(D)]);
1083    }
1084
1085    #[test]
1086    fn get_atom_types_function_call_incorrect_arguments() {
1087        let space = metta_space("
1088            (: a (-> C D))
1089            (: b B)
1090        ");
1091        assert_eq!(get_atom_types(&space, &atom("(a b)")), vec![typ_err!((-> C D), (Error (a b) (BadArgType 1 C B)))]);
1092    }
1093
1094    #[test]
1095    fn get_atom_types_function_call_parameterized_types() {
1096        let space = metta_space("
1097            (: = (-> $t $t Type))
1098            (: Some (-> $p Type))
1099            (: foo (-> (Some P)))
1100            (: bar (-> $p (Some $p)))
1101            (: p X)
1102            (: p P)
1103        ");
1104        assert_eq!(get_atom_types(&space, &atom("(= (foo) (bar p))")),
1105            vec![typ_app!(Type)]);
1106    }
1107
1108    #[test]
1109    fn check_type_parameterized_type_no_variable_bindings() {
1110        let space = metta_space("
1111            (: Pair (-> $a $b Type))
1112            (: A (Pair $c $d))
1113        ");
1114
1115        assert!(check_type(&space, &atom("A"), &atom("(Pair $e $f)")));
1116        assert!(check_type(&space, &atom("A"), &atom("(Pair $f $f)")));
1117    }
1118
1119    #[test]
1120    fn check_type_dependent_type_symbol_param() {
1121        let space = metta_space("
1122            (: === (-> $a $a Type))
1123            (: Refl (-> $x (=== $x $x)))
1124
1125            (: TermSym A)
1126        ");
1127
1128        assert!(check_type(&space, &atom("(Refl TermSym)"), &atom("(=== A A)")));
1129        assert!(!check_type(&space, &atom("(Refl TermSym)"), &atom("(=== A B)")));
1130        assert!(!check_type(&space, &atom("(Refl TermSym)"), &atom("(=== 42 A)")));
1131        assert!(!check_type(&space, &atom("(Refl TermSym)"), &atom("(=== A 42)")));
1132        assert!(check_type(&space, &atom("(Refl TermSym)"), &atom("(=== $a A)")));
1133        assert!(check_type(&space, &atom("(Refl TermSym)"), &atom("(=== A $a)")));
1134        assert!(check_type(&space, &atom("(Refl TermSym)"), &atom("(=== $a $a)")));
1135        assert!(check_type(&space, &atom("(Refl TermSym)"), &atom("(=== $a $b)")));
1136    }
1137
1138    #[test]
1139    fn check_type_dependent_type_grounded_param() {
1140        let space = metta_space("
1141            (: === (-> $a $a Type))
1142            (: Refl (-> $x (=== $x $x)))
1143
1144            (: TermGnd 42)
1145        ");
1146
1147        assert!(check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== 42 42)")));
1148        assert!(!check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== 42 24)")));
1149        assert!(!check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== 42 A)")));
1150        assert!(!check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== A 42)")));
1151        assert!(check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== $a 42)")));
1152        assert!(check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== 42 $a)")));
1153        assert!(check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== $a $a)")));
1154        assert!(check_type(&space, &atom("(Refl TermGnd)"), &atom("(=== $a $b)")));
1155    }
1156
1157    #[test]
1158    fn check_type_accept_meta_type() {
1159        let type_r = &atom("R");
1160        let space = metta_space("
1161            (: R Type)
1162            (: A Type)
1163            (: B Type)
1164            (: a A)
1165            (: b B)
1166
1167            (: aF (-> A R))
1168            (: atomF (-> Atom R))
1169            (: exprF (-> Expression R))
1170            (: gndF (-> Grounded R))
1171            (: symF (-> Symbol R))
1172            (: varF (-> Variable R))
1173        ");
1174
1175        assert!(check_type(&space, &atom("(aF a)"), type_r));
1176        assert!(!check_type(&space, &atom("(aF b)"), type_r));
1177        // TODO: (aF b) is incorrectly typed, but it is an Atom and check_type
1178        // returns True
1179        assert!(check_type(&space, &atom("(aF b)"), &ATOM_TYPE_ATOM));
1180        assert!(check_type(&space, &atom("(aF b)"), &ATOM_TYPE_EXPRESSION));
1181        assert!(!check_type(&space, &atom("(aF b)"), &ATOM_TYPE_SYMBOL));
1182
1183        assert!(check_type(&space, &atom("(atomF a)"), type_r));
1184        assert!(check_type(&space, &atom("(atomF ())"), type_r));
1185        assert!(check_type(&space, &atom("(exprF ())"), type_r));
1186        assert!(!check_type(&space, &atom("(exprF a)"), type_r));
1187        assert!(check_type(&space, &atom("(gndF 1)"), type_r));
1188        assert!(!check_type(&space, &atom("(gndF a)"), type_r));
1189        assert!(check_type(&space, &atom("(symF a)"), type_r));
1190        assert!(!check_type(&space, &atom("(symF 1)"), type_r));
1191        assert!(check_type(&space, &atom("(varF $a)"), type_r));
1192        assert!(!check_type(&space, &atom("(varF a)"), type_r));
1193    }
1194
1195    #[test]
1196    fn check_type_return_meta_type() {
1197        let type_r = &atom("R");
1198        let space = metta_space("
1199            (: R Type)
1200            (: A Type)
1201            (: B Type)
1202            (: a A)
1203            (: b B)
1204
1205            (: atomR (-> A Atom))
1206            (: exprR (-> A Expression))
1207            (: gndR (-> A Grounded))
1208            (: symR (-> A Symbol))
1209            (: varR (-> A Variable))
1210
1211            (: atomF (-> Atom R))
1212            (: exprF (-> Expression R))
1213            (: gndF (-> Grounded R))
1214            (: symF (-> Symbol R))
1215            (: varF (-> Variable R))
1216        ");
1217
1218        assert!(check_type(&space, &atom("(atomF (atomR a))"), type_r));
1219        assert!(check_type(&space, &atom("(atomF (exprR a))"), type_r));
1220        assert!(check_type(&space, &atom("(atomF (gndR a))"), type_r));
1221        assert!(check_type(&space, &atom("(atomF (symR a))"), type_r));
1222        assert!(check_type(&space, &atom("(atomF (varR a))"), type_r));
1223
1224        assert!(check_type(&space, &atom("(exprF (exprR a))"), type_r));
1225        // TODO: it is incorrectly typed, but (atomR a) is an Expression and
1226        // check_type returns True
1227        assert!(check_type(&space, &atom("(exprF (atomR a))"), type_r));
1228
1229        assert!(check_type(&space, &atom("(gndF (gndR a))"), type_r));
1230        assert!(!check_type(&space, &atom("(gndF (atomR a))"), type_r));
1231        assert!(check_type(&space, &atom("(symF (symR a))"), type_r));
1232        assert!(!check_type(&space, &atom("(symF (atomR a))"), type_r));
1233        assert!(check_type(&space, &atom("(varF (varR a))"), type_r));
1234        assert!(!check_type(&space, &atom("(varF (atomR a))"), type_r));
1235    }
1236
1237    #[test]
1238    fn validate_atom_accept_meta_type() {
1239        let space = metta_space("
1240            (: R Type)
1241            (: A Type)
1242            (: B Type)
1243            (: a A)
1244            (: b B)
1245
1246            (: aF (-> A R))
1247            (: atomF (-> Atom R))
1248            (: exprF (-> Expression R))
1249            (: gndF (-> Grounded R))
1250            (: symF (-> Symbol R))
1251            (: varF (-> Variable R))
1252        ");
1253
1254        assert!(validate_atom(&space, &atom("(aF a)")));
1255        assert!(!validate_atom(&space, &atom("(aF b)")));
1256
1257        assert!(validate_atom(&space, &atom("(atomF a)")));
1258        assert!(validate_atom(&space, &atom("(atomF ())")));
1259        assert!(validate_atom(&space, &atom("(exprF ())")));
1260        assert!(!validate_atom(&space, &atom("(exprF a)")));
1261        assert!(validate_atom(&space, &atom("(gndF 1)")));
1262        assert!(!validate_atom(&space, &atom("(gndF a)")));
1263        assert!(validate_atom(&space, &atom("(symF a)")));
1264        assert!(!validate_atom(&space, &atom("(symF 1)")));
1265        assert!(validate_atom(&space, &atom("(varF $a)")));
1266        assert!(!validate_atom(&space, &atom("(varF a)")));
1267    }
1268
1269    #[test]
1270    fn validate_atom_return_meta_type() {
1271        let space = metta_space("
1272            (: R Type)
1273            (: A Type)
1274            (: B Type)
1275            (: a A)
1276            (: b B)
1277
1278            (: atomR (-> A Atom))
1279            (: exprR (-> A Expression))
1280            (: gndR (-> A Grounded))
1281            (: symR (-> A Symbol))
1282            (: varR (-> A Variable))
1283
1284            (: atomF (-> Atom R))
1285            (: exprF (-> Expression R))
1286            (: gndF (-> Grounded R))
1287            (: symF (-> Symbol R))
1288            (: varF (-> Variable R))
1289        ");
1290
1291        assert!(validate_atom(&space, &atom("(atomF (atomR a))")));
1292        assert!(validate_atom(&space, &atom("(atomF (exprR a))")));
1293        assert!(validate_atom(&space, &atom("(atomF (gndR a))")));
1294        assert!(validate_atom(&space, &atom("(atomF (symR a))")));
1295        assert!(validate_atom(&space, &atom("(atomF (varR a))")));
1296
1297        assert!(validate_atom(&space, &atom("(exprF (exprR a))")));
1298        // TODO: (exprF (atomR a)) is incorrectly typed, but (atomR a)
1299        // is an Expression and validate_atom returns True
1300        assert!(validate_atom(&space, &atom("(exprF (atomR a))")));
1301
1302        assert!(validate_atom(&space, &atom("(gndF (gndR a))")));
1303        assert!(!validate_atom(&space, &atom("(gndF (atomR a))")));
1304        assert!(validate_atom(&space, &atom("(symF (symR a))")));
1305        assert!(!validate_atom(&space, &atom("(symF (atomR a))")));
1306        assert!(validate_atom(&space, &atom("(varF (varR a))")));
1307        assert!(!validate_atom(&space, &atom("(varF (atomR a))")));
1308    }
1309
1310    #[test]
1311    fn tuple_with_undefined_member() {
1312        let space = metta_space("(: F %Undefined%)");
1313        assert_eq!(get_atom_types_internal(&space, &atom("(F arg)")), vec![]);
1314
1315        let gnd = GroundedAtomWithParameterizedType(ATOM_TYPE_UNDEFINED);
1316        assert_eq!(get_atom_types_internal(&space, &expr!({gnd} "a")), vec![]);
1317    }
1318
1319}
hyperon/metta/types.rs

hyperon/metta/
types.rs
