edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-25 22:06:33 +03:00
Code Issues Projects Releases Wiki Activity

Unelaborate hole applications properly

Browse Source 
This was left over from Blodwen (where it was also wrong :)) but the way
we apply metavariables now means we don't need to do anything fancy when
unelaborating them for pretty printing.
This commit is contained in:
Edwin Brady 2019-07-03 15:31:46 +01:00
parent 89c8314a0f
commit 6f5d3f5fef
5 changed files with 26 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/TTImp/Unelab.idr
View File

@ -146,20 +146,18 @@ mutual
unelabBinder umode fc env x b sc sc' scty
unelabTy' umode env (App fc fn arg)
= do (fn', fnty) <- unelabTy umode env fn
case fn' of
IHole _ _ => pure (fn', Erased fc)
_ => do (arg', argty) <- unelabTy umode env arg
defs <- get Ctxt
case !(nf defs env fnty) of
NBind _ x (Pi rig Explicit ty) sc
=> do sc' <- sc defs (toClosure defaultOpts env arg)
pure (IApp fc fn' arg',
!(quote defs env sc'))
NBind _ x (Pi rig p ty) sc
=> do sc' <- sc defs (toClosure defaultOpts env arg)
pure (IImplicitApp fc fn' (Just x) arg',
!(quote defs env sc'))
_ => pure (IApp fc fn' arg', Erased fc)
(arg', argty) <- unelabTy umode env arg
defs <- get Ctxt
case !(nf defs env fnty) of
NBind _ x (Pi rig Explicit ty) sc
=> do sc' <- sc defs (toClosure defaultOpts env arg)
pure (IApp fc fn' arg',
!(quote defs env sc'))
NBind _ x (Pi rig p ty) sc
=> do sc' <- sc defs (toClosure defaultOpts env arg)
pure (IImplicitApp fc fn' (Just x) arg',
!(quote defs env sc'))
_ => pure (IApp fc fn' arg', Erased fc)
unelabTy' umode env (As fc p tm)
= do (p', _) <- unelabTy' umode env p
(tm', ty) <- unelabTy' umode env tm

2
tests/Main.idr
View File

@ -30,7 +30,7 @@ idrisTests
"basic021", "basic022", "basic023", "basic024",
"coverage001", "coverage002", "coverage003", "coverage004",
"error001", "error002", "error003", "error004", "error005",
"error006",
"error006", "error007",
"import001", "import002",
"interactive001", "interactive002", "interactive003", "interactive004",
"interactive005", "interactive006", "interactive007", "interactive008",

4
tests/idris2/error007/CongErr.idr Normal file
View File

@ -0,0 +1,4 @@
import Data.Fin
fsprf : x === y -> FS x = FS y
fsprf p = cong _ p

6
tests/idris2/error007/expected Normal file
View File

@ -0,0 +1,6 @@
1/1: Building CongErr (CongErr.idr)
CongErr.idr:4:11--5:1:While processing right hand side of Main.fsprf at CongErr.idr:4:1--5:1:
Can't solve constraint between:
?_ x
and
FS x

3
tests/idris2/error007/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check CongErr.idr
rm -rf build