dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

[ fix ] error messages mangled by Idris to Newt translation

Browse Source
This commit is contained in:
Steve Dunham
2025-07-27 14:29:14 -07:00
parent a79f92793b
commit ff23deb825
2 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
src/Lib/Elab.newt
View File

@@ -490,7 +490,7 @@ unify env mode t u = do
vtm <- eval Nil CBN tm vtm <- eval Nil CBN tm
appvtm <- vappSpine vtm sp' appvtm <- vappSpine vtm sp'
unify env mode t appvtm 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 unifyRef t@(VRef fc k sp) u = do
debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}" debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
@@ -500,7 +500,7 @@ unify env mode t u = do
vtm <- eval Nil CBN tm vtm <- eval Nil CBN tm
tmsp <- vappSpine vtm sp tmsp <- vappSpine vtm sp
unify env mode tmsp u 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 unifyRef t u = unifyRest t u
unifyVar : Val -> Val -> M UnifyResult unifyVar : Val -> Val -> M UnifyResult

4
src/Lib/Types.newt
View File

@@ -259,7 +259,7 @@ instance Show Val where
show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})" show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})"
show (VRef _ nm Lin) = show nm show (VRef _ nm Lin) = show nm
show (VRef _ nm sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})" 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 (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 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})" 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" 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 -- instance Show Closure where
-- show = showClosure -- show = showClosure