From 0ce048e4d95b08e50dec0f2e0f6736f3c5b646f2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 7 Apr 2019 00:24:34 +0200 Subject: More typecheck --- dhall/src/typecheck.rs | 164 ++++++++++++++++++++++++++----------------------- 1 file changed, 86 insertions(+), 78 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 0ebc67e..29ad6d4 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,5 +1,4 @@ #![allow(non_snake_case)] -use std::collections::HashSet; use std::fmt; use crate::expr::*; @@ -12,10 +11,6 @@ use self::TypeMessage::*; impl Resolved { pub fn typecheck(self) -> Result> { - // let typ = Type(Box::new(Normalized(crate::typecheck::type_of( - // self.0.clone(), - // )?))); - // Ok(Typed(self.0, typ)) let typ = crate::typecheck::type_of_(self.0.clone())?; Ok(typ) } @@ -24,11 +19,23 @@ impl Typed { fn as_expr(&self) -> &SubExpr { &self.0 } + fn into_expr(self) -> SubExpr { + self.0 + } + pub fn into_type(self) -> Type { + self.1 + } pub fn get_type(&self) -> &Type { &self.1 } } impl Normalized { + fn as_expr(&self) -> &SubExpr { + &self.0 + } + fn into_expr(self) -> SubExpr { + self.0 + } pub fn get_type(&self) -> &Type { &self.1 } @@ -37,11 +44,8 @@ impl Normalized { } } impl Type { - // pub fn as_expr(&self) -> &Normalized { - // &*self.0 - // } fn as_expr(&self) -> &SubExpr { - &self.as_normalized().0 + &self.as_normalized().as_expr() } fn as_normalized(&self) -> &Normalized { use TypeInternal::*; @@ -50,13 +54,24 @@ impl Type { Universe(_) => unimplemented!(), } } + fn into_expr(self) -> SubExpr { + use TypeInternal::*; + match self.0 { + Expr(e) => e.into_expr(), + Universe(_) => unimplemented!(), + } + } pub fn get_type(&self) -> &Type { - self.as_normalized().get_type() + use TypeInternal::*; + match &self.0 { + Expr(e) => e.get_type(), + Universe(_) => unimplemented!(), + // Universe(n) => &Type(Universe(n+1)), + } } } -const TYPE_OF_SORT: crate::expr::Type = - crate::expr::Type(TypeInternal::Universe(4)); +const TYPE_OF_SORT: Type = Type(TypeInternal::Universe(4)); fn rule(a: Const, b: Const) -> Result { use dhall_core::Const::*; @@ -89,11 +104,7 @@ fn match_vars(vl: &V