summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/binary.rs22
-rw-r--r--dhall/src/expr.rs32
-rw-r--r--dhall/src/normalize.rs48
-rw-r--r--dhall/src/serde.rs2
-rw-r--r--dhall/src/traits/static_type.rs14
-rw-r--r--dhall/src/typecheck.rs65
6 files changed, 83 insertions, 100 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 0d9f28a..9c31d4c 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -2,7 +2,7 @@ use dhall_syntax::*;
use itertools::*;
use serde_cbor::value::value as cbor;
-type ParsedExpr = SubExpr<Label, X, Import>;
+type ParsedExpr = SubExpr<X, Import>;
#[derive(Debug)]
pub enum DecodeError {
@@ -18,32 +18,28 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
}
fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
- use cbor::Value::{Array, Bool, Null, Object, String, F64, I64, U64};
+ use cbor::Value::*;
use dhall_syntax::{BinOp, Builtin, Const};
- use ExprF::{
- Annot, App, BoolIf, BoolLit, DoubleLit, Embed, EmptyListLit, Field,
- IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit, OldOptionalLit, Pi,
- RecordLit, RecordType, SomeLit, TextLit, UnionLit, UnionType,
- };
+ use ExprF::*;
Ok(rc(match data {
String(s) => match Builtin::parse(s) {
Some(b) => ExprF::Builtin(b),
None => match s.as_str() {
"True" => BoolLit(true),
"False" => BoolLit(false),
- "Type" => ExprF::Const(Const::Type),
- "Kind" => ExprF::Const(Const::Kind),
- "Sort" => ExprF::Const(Const::Sort),
+ "Type" => Const(Const::Type),
+ "Kind" => Const(Const::Kind),
+ "Sort" => Const(Const::Sort),
_ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
},
},
- U64(n) => ExprF::Var(Var(Label::from("_"), *n as usize)),
+ U64(n) => Var(V(Label::from("_"), *n as usize)),
F64(x) => DoubleLit((*x).into()),
Bool(b) => BoolLit(*b),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
let l = Label::from(l.as_str());
- ExprF::Var(Var(l, *n as usize))
+ Var(V(l, *n as usize))
}
[U64(0), f, args..] => {
let mut f = cbor_value_to_dhall(&f)?;
@@ -96,7 +92,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
Err(DecodeError::WrongFormatError("binop".to_owned()))?
}
};
- ExprF::BinOp(op, x, y)
+ BinOp(op, x, y)
}
[U64(4), t] => {
let t = cbor_value_to_dhall(&t)?;
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index efc3928..5bde68f 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -23,17 +23,15 @@ macro_rules! derive_other_traits {
};
}
-type OutputSubExpr = SubExpr<Label, X, X>;
-
#[derive(Debug, Clone)]
pub(crate) struct Parsed(
- pub(crate) SubExpr<Label, Span, Import>,
+ pub(crate) SubExpr<Span, Import>,
pub(crate) ImportRoot,
);
derive_other_traits!(Parsed);
#[derive(Debug, Clone)]
-pub(crate) struct Resolved(pub(crate) SubExpr<Label, Span, Normalized>);
+pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>);
derive_other_traits!(Resolved);
pub(crate) use self::typed::TypedInternal;
@@ -59,12 +57,12 @@ impl std::fmt::Display for Normalized {
}
mod typed {
- use super::{OutputSubExpr, Type, Typed};
+ use super::{Type, Typed};
use crate::normalize::{Thunk, Value};
use crate::typecheck::{
TypeError, TypeInternal, TypeMessage, TypecheckContext,
};
- use dhall_syntax::{Const, Label, Var};
+ use dhall_syntax::{Const, Label, SubExpr, V, X};
use std::borrow::Cow;
#[derive(Debug, Clone)]
@@ -92,7 +90,7 @@ mod typed {
}
}
- pub(crate) fn to_expr(&self) -> OutputSubExpr {
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
self.to_value().normalize_to_expr()
}
@@ -131,7 +129,7 @@ mod typed {
}
}
- pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.shift(delta, var),
@@ -141,11 +139,7 @@ mod typed {
}
}
- pub(crate) fn subst_shift(
- &self,
- var: &Var<Label>,
- val: &Typed,
- ) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
match self {
TypedInternal::Value(th, t) => TypedInternal::Value(
th.subst_shift(var, val),
@@ -164,7 +158,7 @@ mod typed {
///
/// For a more general notion of "type", see [Type].
#[derive(Debug, Clone)]
-pub struct SimpleType(pub(crate) OutputSubExpr);
+pub struct SimpleType(pub(crate) SubExpr<X, X>);
derive_other_traits!(SimpleType);
pub(crate) use crate::typecheck::TypeInternal;
@@ -184,16 +178,16 @@ impl std::fmt::Display for Type {
// Exposed for the macros
#[doc(hidden)]
-impl From<SimpleType> for OutputSubExpr {
- fn from(x: SimpleType) -> OutputSubExpr {
+impl From<SimpleType> for SubExpr<X, X> {
+ fn from(x: SimpleType) -> SubExpr<X, X> {
x.0
}
}
// Exposed for the macros
#[doc(hidden)]
-impl From<OutputSubExpr> for SimpleType {
- fn from(x: OutputSubExpr) -> SimpleType {
+impl From<SubExpr<X, X>> for SimpleType {
+ fn from(x: SubExpr<X, X>) -> SimpleType {
SimpleType(x)
}
}
@@ -210,7 +204,7 @@ impl Normalized {
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
Normalized(TypedInternal::from_thunk_and_type(th, t))
}
- pub(crate) fn to_expr(&self) -> OutputSubExpr {
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
self.0.to_expr()
}
pub(crate) fn to_value(&self) -> Value {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3de12ee..8ae746d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,13 +6,13 @@ use dhall_proc_macros as dhall;
use dhall_syntax::context::Context;
use dhall_syntax::{
rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
- InterpolatedTextContents, Label, Natural, Span, SubExpr, Var, X,
+ InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
};
use crate::expr::{Normalized, Type, Typed, TypedInternal};
-type InputSubExpr = SubExpr<Label, Span, Normalized>;
-type OutputSubExpr = SubExpr<Label, X, X>;
+type InputSubExpr = SubExpr<Span, Normalized>;
+type OutputSubExpr = SubExpr<X, X>;
impl Typed {
/// Reduce an expression to its normal form, performing beta reduction
@@ -38,11 +38,11 @@ impl Typed {
Normalized(internal)
}
- pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Typed(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
Typed(self.0.subst_shift(var, val))
}
@@ -58,11 +58,11 @@ impl Typed {
#[derive(Debug, Clone)]
enum EnvItem {
Thunk(Thunk),
- Skip(Var<Label>),
+ Skip(V<Label>),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use EnvItem::*;
match self {
Thunk(e) => Thunk(e.shift(delta, var)),
@@ -70,7 +70,7 @@ impl EnvItem {
}
}
- pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
match self {
EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
@@ -93,8 +93,8 @@ impl NormalizationContext {
.insert(x.clone(), EnvItem::Skip(x.into())),
))
}
- fn lookup(&self, var: &Var<Label>) -> Value {
- let Var(x, n) = var;
+ fn lookup(&self, var: &V<Label>) -> Value {
+ let V(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Thunk(t)) => t.to_value(),
Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
@@ -118,11 +118,11 @@ impl NormalizationContext {
NormalizationContext(Rc::new(ctx))
}
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
}
- fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
NormalizationContext(Rc::new(
self.0.map(|_, e| e.subst_shift(var, val)),
))
@@ -144,7 +144,7 @@ pub(crate) enum Value {
NaturalSuccClosure,
Pi(Label, TypeThunk, TypeThunk),
- Var(Var<Label>),
+ Var(V<Label>),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -403,7 +403,7 @@ impl Value {
Value::AppliedBuiltin(b, vec![])
}
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -500,7 +500,7 @@ impl Value {
}
}
- pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -616,7 +616,7 @@ mod thunk {
OutputSubExpr, Value,
};
use crate::expr::Typed;
- use dhall_syntax::{Label, Var};
+ use dhall_syntax::{Label, V};
use std::cell::{Ref, RefCell};
use std::rc::Rc;
@@ -693,7 +693,7 @@ mod thunk {
}
}
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -707,7 +707,7 @@ mod thunk {
}
}
- fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -805,15 +805,11 @@ mod thunk {
apply_any(self.clone(), th)
}
- pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
self.0.borrow().shift(delta, var).into_thunk()
}
- pub(crate) fn subst_shift(
- &self,
- var: &Var<Label>,
- val: &Typed,
- ) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
self.0.borrow().subst_shift(var, val).into_thunk()
}
}
@@ -859,14 +855,14 @@ impl TypeThunk {
self.normalize_nf().normalize_to_expr()
}
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
}
}
- pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/serde.rs b/dhall/src/serde.rs
index bc76c49..96bc765 100644
--- a/dhall/src/serde.rs
+++ b/dhall/src/serde.rs
@@ -11,7 +11,7 @@ impl<'a, T: serde::Deserialize<'a>> Deserialize<'a> for T {
}
}
-struct Deserializer<'a>(Cow<'a, SubExpr<Label, X, X>>);
+struct Deserializer<'a>(Cow<'a, SubExpr<X, X>>);
impl serde::de::Error for Error {
fn custom<T>(msg: T) -> Self
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index c3f323b..f90b8df 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -32,7 +32,7 @@ pub trait SimpleStaticType {
fn get_simple_static_type() -> SimpleType;
}
-fn mktype(x: SubExpr<Label, X, X>) -> SimpleType {
+fn mktype(x: SubExpr<X, X>) -> SimpleType {
x.into()
}
@@ -106,22 +106,22 @@ impl SimpleStaticType for String {
impl<A: SimpleStaticType, B: SimpleStaticType> SimpleStaticType for (A, B) {
fn get_simple_static_type() -> SimpleType {
- let ta: SubExpr<_, _, _> = A::get_simple_static_type().into();
- let tb: SubExpr<_, _, _> = B::get_simple_static_type().into();
+ let ta: SubExpr<_, _> = A::get_simple_static_type().into();
+ let tb: SubExpr<_, _> = B::get_simple_static_type().into();
mktype(dhall::subexpr!({ _1: ta, _2: tb }))
}
}
impl<T: SimpleStaticType> SimpleStaticType for Option<T> {
fn get_simple_static_type() -> SimpleType {
- let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
+ let t: SubExpr<_, _> = T::get_simple_static_type().into();
mktype(dhall::subexpr!(Optional t))
}
}
impl<T: SimpleStaticType> SimpleStaticType for Vec<T> {
fn get_simple_static_type() -> SimpleType {
- let t: SubExpr<_, _, _> = T::get_simple_static_type().into();
+ let t: SubExpr<_, _> = T::get_simple_static_type().into();
mktype(dhall::subexpr!(List t))
}
}
@@ -142,8 +142,8 @@ impl<T: SimpleStaticType, E: SimpleStaticType> SimpleStaticType
for std::result::Result<T, E>
{
fn get_simple_static_type() -> SimpleType {
- let tt: SubExpr<_, _, _> = T::get_simple_static_type().into();
- let te: SubExpr<_, _, _> = E::get_simple_static_type().into();
+ let tt: SubExpr<_, _> = T::get_simple_static_type().into();
+ let te: SubExpr<_, _> = E::get_simple_static_type().into();
mktype(dhall::subexpr!(< Ok: tt | Err: te>))
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 63041bb..8b7f011 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -14,16 +14,13 @@ use dhall_syntax::*;
use self::TypeMessage::*;
-type InputSubExpr = SubExpr<Label, Span, Normalized>;
-type OutputSubExpr = SubExpr<Label, X, X>;
-
impl Resolved {
pub fn typecheck(self) -> Result<Typed, TypeError> {
type_of(self.0)
}
pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
- let expr = self.0;
- let ty = ty.to_expr().embed_absurd().note_absurd();
+ let expr: SubExpr<_, _> = self.0;
+ let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
}
/// Pretends this expression has been typechecked. Use with care.
@@ -46,7 +43,7 @@ impl Typed {
}
impl Normalized {
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Normalized(self.0.shift(delta, var))
}
pub(crate) fn to_type(self) -> Type {
@@ -58,7 +55,7 @@ impl Type {
pub(crate) fn to_normalized(&self) -> Normalized {
self.0.to_normalized()
}
- pub(crate) fn to_expr(&self) -> OutputSubExpr {
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
self.0.to_expr()
}
pub(crate) fn to_value(&self) -> Value {
@@ -76,10 +73,10 @@ impl Type {
fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
- pub(crate) fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Type(self.0.shift(delta, var))
}
- pub(crate) fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ pub(crate) fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
Type(self.0.subst_shift(var, val))
}
@@ -127,7 +124,7 @@ impl TypeInternal {
fn to_normalized(&self) -> Normalized {
self.to_typed().normalize()
}
- fn to_expr(&self) -> OutputSubExpr {
+ fn to_expr(&self) -> SubExpr<X, X> {
self.to_normalized().to_expr()
}
fn to_value(&self) -> Value {
@@ -151,14 +148,14 @@ impl TypeInternal {
_ => None,
}
}
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.shift(delta, var))),
Const(c) => Const(*c),
}
}
- fn subst_shift(&self, var: &Var<Label>, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &V<Label>, val: &Typed) -> Self {
use TypeInternal::*;
match self {
Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
@@ -176,12 +173,12 @@ impl PartialEq for TypeInternal {
#[derive(Debug, Clone)]
pub(crate) enum EnvItem {
- Type(Var<Label>, Type),
+ Type(V<Label>, Type),
Value(Normalized),
}
impl EnvItem {
- fn shift(&self, delta: isize, var: &Var<Label>) -> Self {
+ fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use EnvItem::*;
match self {
Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
@@ -208,8 +205,8 @@ impl TypecheckContext {
pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self {
TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
}
- pub(crate) fn lookup(&self, var: &Var<Label>) -> Option<Cow<'_, Type>> {
- let Var(x, n) = var;
+ pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> {
+ let V(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
Some(EnvItem::Value(t)) => Some(t.get_type()?),
@@ -241,12 +238,8 @@ fn function_check(a: Const, b: Const) -> Result<Const, ()> {
}
}
-fn match_vars(
- vl: &Var<Label>,
- vr: &Var<Label>,
- ctx: &[(&Label, &Label)],
-) -> bool {
- let (Var(xL, mut nL), Var(xR, mut nR)) = (vl, vr);
+fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(&Label, &Label)]) -> bool {
+ let (V(xL, mut nL), V(xR, mut nR)) = (vl, vr);
for &(xL2, xR2) in ctx {
match (nL, nR) {
(0, 0) if xL == xL2 && xR == xR2 => return true,
@@ -272,8 +265,8 @@ where
use dhall_syntax::ExprF::*;
fn go<'a, S, T>(
ctx: &mut Vec<(&'a Label, &'a Label)>,
- el: &'a SubExpr<Label, S, X>,
- er: &'a SubExpr<Label, T, X>,
+ el: &'a SubExpr<S, X>,
+ er: &'a SubExpr<T, X>,
) -> bool
where
S: ::std::fmt::Debug,
@@ -357,9 +350,9 @@ fn type_of_const(c: Const) -> Result<Type, TypeError> {
}
}
-fn type_of_builtin(b: Builtin) -> InputSubExpr {
+fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> {
use dhall_syntax::Builtin::*;
- rc(match b {
+ match b {
Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
List | Optional => dhall::expr!(
Type -> Type
@@ -439,8 +432,7 @@ fn type_of_builtin(b: Builtin) -> InputSubExpr {
OptionalNone => dhall::expr!(
forall (A: Type) -> Optional A
),
- })
- .note_absurd()
+ }
}
macro_rules! ensure_equal {
@@ -627,7 +619,10 @@ impl TypeIntermediate {
/// Takes an expression that is meant to contain a Type
/// and turn it into a type, typechecking it along the way.
-fn mktype(ctx: &TypecheckContext, e: InputSubExpr) -> Result<Type, TypeError> {
+fn mktype(
+ ctx: &TypecheckContext,
+ e: SubExpr<Span, Normalized>,
+) -> Result<Type, TypeError> {
Ok(type_with(ctx, e)?.to_type())
}
@@ -650,7 +645,7 @@ enum Ret {
/// succeeded, or an error if type-checking failed
fn type_with(
ctx: &TypecheckContext,
- e: InputSubExpr,
+ e: SubExpr<Span, Normalized>,
) -> Result<Typed, TypeError> {
use dhall_syntax::ExprF::{
Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
@@ -761,7 +756,7 @@ fn type_last_layer(
mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
});
- Ok(RetType(tb.subst_shift(&x.into(), &a)))
+ Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
}
Annot(x, t) => {
let t = t.to_type();
@@ -942,7 +937,9 @@ fn type_last_layer(
}
}
Const(c) => Ok(RetTyped(const_to_typed(c))),
- Builtin(b) => Ok(RetType(mktype(ctx, type_of_builtin(b))?)),
+ Builtin(b) => {
+ Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
+ }
BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -1001,7 +998,7 @@ fn type_last_layer(
/// `typeOf` is the same as `type_with` with an empty context, meaning that the
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
-fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
+fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
let ctx = TypecheckContext::new();
let e = type_with(&ctx, e)?;
// Ensure `e` has a type (i.e. `e` is not `Sort`)
@@ -1012,7 +1009,7 @@ fn type_of(e: InputSubExpr) -> Result<Typed, TypeError> {
/// The specific type error
#[derive(Debug)]
pub(crate) enum TypeMessage {
- UnboundVariable(Var<Label>),
+ UnboundVariable(V<Label>),
InvalidInputType(Normalized),
InvalidOutputType(Normalized),
NotAFunction(Typed),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:53:27 +0000