1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133

//! This module provides a DLS for writing [`Term`](crate::algebra::Term)s within Rust.
//! See the tlspuffin crate for usage examples.

#[macro_export]
macro_rules! term {
    //
    // Handshake with QueryMatcher
    // `>$req_type:expr` must be the last part of the arm, even if it is not used.
    //
    ((!$precomp:literal, $counter:expr) / $typ:ty $(>$req_type:expr)?) => {{
        use $crate::algebra::dynamic_function::TypeShape;

        // ignore $req_type as we are overriding it with $type
        Term::from(term!((!$precomp, $counter) > TypeShape::of::<$typ>()))
    }};
    (($agent:expr, $counter:expr) / $typ:ty $(>$req_type:expr)?) => {{
        use $crate::algebra::dynamic_function::TypeShape;
        use $crate::algebra::Term;


        // ignore $req_type as we are overriding it with $type
        Term::from(term!(($agent, $counter) > TypeShape::of::<$typ>()))
    }};
    ((!$precomp:literal, $counter:expr) $(>$req_type:expr)?) => {{
        use $crate::algebra::signature::Signature;
        use $crate::algebra::Term;
        use $crate::trace::Source;

        let var = Signature::new_var($($req_type)?, Some(Source::Label(Some($precomp.into()))), None, $counter); // TODO: verify hat using here None is fine. Before a refactor it was: Some(TlsMessageType::Handshake(None))
        Term::from(DYTerm::Variable(var))
    }};
    (($agent:expr, $counter:expr) $(>$req_type:expr)?) => {{
        use $crate::algebra::signature::Signature;
        use $crate::algebra::{DYTerm,Term};
        use $crate::trace::Source;

        let var = Signature::new_var($($req_type)?, Some(Source::Agent($agent)), None, $counter); // TODO: verify hat using here None is fine. Before a refactor it was: Some(TlsMessageType::Handshake(None))
        Term::from(DYTerm::Variable(var))
    }};

    //
    // Handshake TlsMessageType with `$message_type` as `TlsMessageType`
    //
    ((!$precomp:literal, $counter:expr) [$message_type:expr] / $typ:ty $(>$req_type:expr)?) => {{
        use $crate::algebra::dynamic_function::TypeShape;

        // ignore $req_type as we are overriding it with $type
       Term::from(term!((!$precomp, $counter) [$message_type] > TypeShape::of::<$typ>()))
    }};
    (($agent:expr, $counter:expr) [$message_type:expr] / $typ:ty $(>$req_type:expr)?) => {{
        use $crate::algebra::dynamic_function::TypeShape;

        // ignore $req_type as we are overriding it with $type
        Term::from(term!(($agent, $counter) [$message_type] > TypeShape::of::<$typ>()))
    }};
    // Extended with custom $type
    ((!$precomp:literal, $counter:expr) [$message_type:expr] $(>$req_type:expr)?) => {{
        use $crate::algebra::signature::Signature;
        use $crate::algebra::Term;
        use $crate::trace::Source;

        let var = Signature::new_var($($req_type)?, Some(Source::Label(Some($precomp.into()))), $message_type, $counter);
        Term::from(DYTerm::Variable(var))
    }};
    (($agent:expr, $counter:expr) [$message_type:expr] $(>$req_type:expr)?) => {{
        use $crate::algebra::signature::Signature;
        use $crate::algebra::{DYTerm,Term};
        use $crate::trace::Source;

        let var = Signature::new_var($($req_type)?, Some(Source::Agent($agent)), $message_type, $counter);
        Term::from(DYTerm::Variable(var))
    }};

    //
    // Function Applications
    //
    ($func:ident ($($args:tt),*) $(>$req_type:expr)?) => {{
        use $crate::algebra::signature::Signature;
        use $crate::algebra::{DYTerm,Term};

        let func = Signature::new_function(&$func);
        #[allow(unused_assignments, unused_variables, unused_mut)]
        let mut i = 0;

        #[allow(unused_assignments)]
        #[allow(clippy::mixed_read_write_in_expression)]
        let arguments = vec![$({
            #[allow(unused)]
            if let Some(argument) = func.shape().argument_types.get(i) {
                i += 1;
                Term::from($crate::term_arg!($args > argument.clone()))
            } else {
                panic!("too many arguments specified for function {}", func)
            }
        }),*];

        Term::from(DYTerm::Application(func, arguments))
    }};
    // Shorthand for constants
    ($func:ident $(>$req_type:expr)?) => {{
        use $crate::algebra::signature::Signature;
        use $crate::algebra::{DYTerm,Term};


        let func = Signature::new_function(&$func);
        Term::from(DYTerm::Application(func, vec![]))
    }};

    //
    // Allows to use variables which already contain a term by starting with a `@`
    //
    (@$e:ident $(>$req_type:expr)?) => {{
        use $crate::algebra::{DYTerm,Term};

        let subterm: &Term<_> = &$e;
        Term::from(subterm.clone())
    }};
}

#[macro_export]
macro_rules! term_arg {
    // Somehow the following rules is very important
    ( ( $($e:tt)* ) $(>$req_type:expr)?) => {{
        use $crate::algebra::{DYTerm,Term};

        Term::from(term!($($e)* $(>$req_type)?))
    }};
    // not sure why I should need this
    // ( ( $e:tt ) ) => (ast!($e));
    ($e:tt $(>$req_type:expr)?) => {{
        Term::from(term!($e $(>$req_type)?))
    }};
}