From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 11:23:59 +0000
Subject: Add Hir as untyped alternative to TyExpr

---
 dhall/src/semantics/tck/tyexpr.rs | 70 +++++++--------------------------------
 1 file changed, 12 insertions(+), 58 deletions(-)

(limited to 'dhall/src/semantics/tck/tyexpr.rs')

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 1886646..fa578c0 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,17 +1,13 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value};
+use crate::semantics::{
+    rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value,
+};
 use crate::syntax::{ExprKind, Span, V};
 use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
 
-/// Stores an alpha-normalized variable.
-#[derive(Debug, Clone, Copy)]
-pub struct AlphaVar {
-    idx: usize,
-}
-
 #[derive(Debug, Clone)]
 pub(crate) enum TyExprKind {
     Var(AlphaVar),
@@ -27,15 +23,6 @@ pub(crate) struct TyExpr {
     span: Span,
 }
 
-impl AlphaVar {
-    pub(crate) fn new(idx: usize) -> Self {
-        AlphaVar { idx }
-    }
-    pub(crate) fn idx(&self) -> usize {
-        self.idx
-    }
-}
-
 impl TyExpr {
     pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
         TyExpr {
@@ -58,17 +45,19 @@ impl TyExpr {
         }
     }
 
+    pub fn to_hir(&self) -> Hir {
+        let kind = match self.kind() {
+            TyExprKind::Var(v) => HirKind::Var(v.clone()),
+            TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())),
+        };
+        Hir::new(kind, self.span())
+    }
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
-        tyexpr_to_expr(self, opts, &mut NameEnv::new())
+        self.to_hir().to_expr(opts)
     }
     pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        let opts = ToExprOptions {
-            normalize: true,
-            alpha: false,
-        };
-        let mut env = env.as_nameenv().clone();
-        tyexpr_to_expr(self, opts, &mut env)
+        self.to_hir().to_expr_tyenv(env)
     }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
@@ -88,41 +77,6 @@ impl TyExpr {
     }
 }
 
-fn tyexpr_to_expr<'a>(
-    tyexpr: &'a TyExpr,
-    opts: ToExprOptions,
-    env: &mut NameEnv,
-) -> NormalizedExpr {
-    rc(match tyexpr.kind() {
-        TyExprKind::Var(v) if opts.alpha => {
-            ExprKind::Var(V("_".into(), v.idx()))
-        }
-        TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)),
-        TyExprKind::Expr(e) => {
-            let e = e.map_ref_maybe_binder(|l, tye| {
-                if let Some(l) = l {
-                    env.insert_mut(l);
-                }
-                let e = tyexpr_to_expr(tye, opts, env);
-                if let Some(_) = l {
-                    env.remove_mut();
-                }
-                e
-            });
-
-            match e {
-                ExprKind::Lam(_, t, e) if opts.alpha => {
-                    ExprKind::Lam("_".into(), t, e)
-                }
-                ExprKind::Pi(_, t, e) if opts.alpha => {
-                    ExprKind::Pi("_".into(), t, e)
-                }
-                e => e,
-            }
-        }
-    })
-}
-
 impl std::fmt::Debug for TyExpr {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let mut x = fmt.debug_struct("TyExpr");
-- 
cgit v1.2.3