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
use arret_syntax::datum::DataStr;
use arret_syntax::span::Span;
use crate::hir;
use crate::ty;
use crate::ty::Ty;
#[derive(Debug, PartialEq, Clone)]
pub enum Destruc<P: hir::Phase> {
Scalar(Span, Scalar<P>),
List(Span, List<P>),
}
#[derive(Debug, PartialEq, Clone)]
pub struct List<P: hir::Phase> {
fixed: Vec<Destruc<P>>,
rest: Option<Box<Scalar<P>>>,
}
impl<P: hir::Phase> List<P> {
pub fn new(fixed: Vec<Destruc<P>>, rest: Option<Box<Scalar<P>>>) -> List<P> {
List { fixed, rest }
}
pub fn fixed(&self) -> &Vec<Destruc<P>> {
&self.fixed
}
pub fn rest(&self) -> &Option<Box<Scalar<P>>> {
&self.rest
}
}
#[derive(Debug, PartialEq, Clone)]
pub struct Scalar<P: hir::Phase> {
local_id: Option<hir::LocalId>,
source_name: DataStr,
ty: P::DeclType,
}
impl<P: hir::Phase> Scalar<P> {
pub fn new(local_id: Option<hir::LocalId>, source_name: DataStr, ty: P::DeclType) -> Scalar<P> {
Scalar {
local_id,
source_name,
ty,
}
}
pub fn local_id(&self) -> &Option<hir::LocalId> {
&self.local_id
}
pub fn source_name(&self) -> &DataStr {
&self.source_name
}
pub fn ty(&self) -> &P::DeclType {
&self.ty
}
}
pub fn subst_list_destruc(
free_ty_polys: &mut impl Iterator<Item = ty::Ref<ty::Poly>>,
list: List<hir::Lowered>,
) -> List<hir::Inferred> {
let fixed = list
.fixed
.into_iter()
.map(|fixed_destruc| subst_destruc(free_ty_polys, fixed_destruc))
.collect();
let rest = list
.rest
.map(|rest_destruc| Box::new(subst_scalar_destruc(free_ty_polys, *rest_destruc)));
List::new(fixed, rest)
}
pub fn subst_scalar_destruc(
free_ty_polys: &mut impl Iterator<Item = ty::Ref<ty::Poly>>,
scalar: Scalar<hir::Lowered>,
) -> Scalar<hir::Inferred> {
let Scalar {
local_id,
ty,
source_name,
} = scalar;
let poly_type = match ty {
hir::DeclTy::Known(poly) => poly,
hir::DeclTy::Free => free_ty_polys.next().unwrap(),
};
Scalar::new(local_id, source_name, poly_type)
}
pub fn subst_destruc(
free_ty_polys: &mut impl Iterator<Item = ty::Ref<ty::Poly>>,
destruc: Destruc<hir::Lowered>,
) -> Destruc<hir::Inferred> {
match destruc {
Destruc::Scalar(span, scalar) => {
Destruc::Scalar(span, subst_scalar_destruc(free_ty_polys, scalar))
}
Destruc::List(span, list) => Destruc::List(span, subst_list_destruc(free_ty_polys, list)),
}
}
pub fn poly_for_list_destruc(list: &List<hir::Inferred>) -> ty::List<ty::Poly> {
let fixed_polys = list.fixed().iter().map(poly_for_destruc).collect();
let rest_poly = match list.rest() {
Some(rest) => rest.ty().clone(),
None => Ty::never().into(),
};
ty::List::new(fixed_polys, rest_poly)
}
pub fn poly_for_destruc(destruc: &Destruc<hir::Inferred>) -> ty::Ref<ty::Poly> {
match destruc {
Destruc::Scalar(_, scalar) => scalar.ty().clone(),
Destruc::List(_, list) => poly_for_list_destruc(list).into(),
}
}