fix names growing in liftWhere and redundant error for ErrorHole
This commit is contained in:
@@ -5,7 +5,7 @@ stats = {}
|
|||||||
acc = ''
|
acc = ''
|
||||||
name = ''
|
name = ''
|
||||||
for line in open(fn):
|
for line in open(fn):
|
||||||
if line.startswith('const'):
|
if line.startswith('const') or line.startswith('let'):
|
||||||
if name: stats[name] = len(acc)
|
if name: stats[name] = len(acc)
|
||||||
acc = line
|
acc = line
|
||||||
name = line.split()[1]
|
name = line.split()[1]
|
||||||
|
|||||||
@@ -52,7 +52,7 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
|
|||||||
modifyRef Defs (updateMap qn (Fn $ wrapLam qs t'))
|
modifyRef Defs (updateMap qn (Fn $ wrapLam qs t'))
|
||||||
|
|
||||||
-- The rest
|
-- The rest
|
||||||
u' <- liftWhereTm qn env' u
|
u' <- liftWhereTm name env' u
|
||||||
pure $ LetRec fc nm (Erased fc) (Erased fc) u'
|
pure $ LetRec fc nm (Erased fc) (Erased fc) u'
|
||||||
where
|
where
|
||||||
-- TODO might be nice if we could nest the names (Foo.go.go) for nested where
|
-- TODO might be nice if we could nest the names (Foo.go.go) for nested where
|
||||||
|
|||||||
@@ -54,6 +54,8 @@ logMetas (Unsolved fc k ctx ty User cons :: rest) = do
|
|||||||
let msg = "\{env}\n -----------\n \{render 90 $ pprint names ty'}"
|
let msg = "\{env}\n -----------\n \{render 90 $ pprint names ty'}"
|
||||||
info fc "User Hole\n\{msg}"
|
info fc "User Hole\n\{msg}"
|
||||||
logMetas rest
|
logMetas rest
|
||||||
|
-- error is reported separately
|
||||||
|
logMetas (Unsolved fc k ctx ty ErrorHole cons :: rest) = logMetas rest
|
||||||
logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
|
logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
|
||||||
ty' <- forceMeta ty
|
ty' <- forceMeta ty
|
||||||
tm <- quote ctx.lvl ty'
|
tm <- quote ctx.lvl ty'
|
||||||
|
|||||||
Reference in New Issue
Block a user