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
|
use crate::expr::*;
use crate::traits::StaticType;
#[allow(unused_imports)]
use crate::typecheck::{
type_of_const, TypeError, TypeMessage, TypecheckContext,
};
#[allow(unused_imports)]
use dhall_core::{Const, ExprF};
use std::borrow::Cow;
pub trait DynamicType {
fn get_type<'a>(&'a self) -> Result<Cow<'a, Type<'static>>, TypeError>;
}
impl<T: StaticType> DynamicType for T {
fn get_type<'a>(&'a self) -> Result<Cow<'a, Type<'static>>, TypeError> {
Ok(Cow::Owned(T::get_static_type()))
}
}
impl<'a> DynamicType for Type<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
Ok(Cow::Owned(
self.clone().into_normalized()?.get_type()?.into_owned(),
))
// match &self.0 {
// TypeInternal::Expr(e) => e.get_type(),
// TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))),
// TypeInternal::SuperType => Err(TypeError::new(
// &TypecheckContext::new(),
// dhall_core::rc(ExprF::Const(Const::Sort)),
// TypeMessage::Untyped,
// )),
// }
}
}
impl<'a> DynamicType for Normalized<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
match &self.1 {
Some(t) => Ok(Cow::Borrowed(t)),
None => Err(TypeError::new(
&TypecheckContext::new(),
self.0.embed_absurd(),
TypeMessage::Untyped,
)),
}
}
}
impl<'a> DynamicType for Typed<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
match &self.1 {
Some(t) => Ok(Cow::Borrowed(t)),
None => Err(TypeError::new(
&TypecheckContext::new(),
self.0.clone(),
TypeMessage::Untyped,
)),
}
}
}
|