forked from asutton/waffle
-
Notifications
You must be signed in to change notification settings - Fork 0
/
subst.hpp
35 lines (26 loc) · 878 Bytes
/
subst.hpp
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
#ifndef SUBST_HPP
#define SUBST_HPP
#include "ast.hpp"
// -------------------------------------------------------------------------- //
// Substitution
// A substitution maps bindings to the terms that will replace
// them. For example, in the substitution [x->s]t, we map
// occurrences of the variable 'x' to the term 's'.
//
// This class allows multiple substitutions to occur at the same
// time (e.g., [x->s1, y->s2]t).
//
// Note that while the key type of the map is an expr, it refers
// to terms that declare names or values.
struct Subst : std::map<Expr*, Expr*, Expr_less> {
Subst() = default;
Subst(Expr*, Expr*);
template<typename T, typename U>
Subst(Seq<T>*, Seq<U>*);
Expr* get(Expr*) const;
};
Expr* subst(Expr*, const Subst&);
Type* subst_type(Type*, const Subst&);
Term* subst_term(Term*, const Subst&);
#include "subst.ipp"
#endif