From ff23deb825d52edf4295159319238ad1a9323425 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 27 Jul 2025 14:29:14 -0700 Subject: [PATCH] [ fix ] error messages mangled by Idris to Newt translation --- src/Lib/Elab.newt | 4 ++-- src/Lib/Types.newt | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index df1d98e..0f5a657 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -490,7 +490,7 @@ unify env mode t u = do vtm <- eval Nil CBN tm appvtm <- vappSpine vtm sp' unify env mode t appvtm - _ => error fc' "unify failed \{show t} =?= \{show u} (no Fn :: Nil)\n env is \{show env}" + _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]\n env is \{show env}" unifyRef t@(VRef fc k sp) u = do debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}" @@ -500,7 +500,7 @@ unify env mode t u = do vtm <- eval Nil CBN tm tmsp <- vappSpine vtm sp unify env mode tmsp u - _ => error fc "unify failed \{show t} (no Fn :: Nil) =?= \{show u}\n env is \{show env}" + _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}\n env is \{show env}" unifyRef t u = unifyRest t u unifyVar : Val -> Val -> M UnifyResult diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index bfb14cb..74eb7d2 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -259,7 +259,7 @@ instance Show Val where show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})" show (VRef _ nm Lin) = show nm show (VRef _ nm sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})" - show (VMeta _ ix sp) = "(%meta \{show ix} (\{show $ snoclen sp} sp :: Nil))" + show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ snoclen sp} sp])" show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{showClosure x})" show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{showClosure y})" show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{showClosure y})" @@ -272,7 +272,7 @@ instance Show Val where show (VErased _) = "ERASED" -showClosure (MkClosure xs t) = "(%cl (\{show $ length xs} env :: Nil) \{show t})" +showClosure (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})" -- instance Show Closure where -- show = showClosure