edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-05 03:17:21 +03:00
Code Issues Projects Releases Wiki Activity

Small tweak to record updates

Browse Source 
A bit more constraing solving in case it helps find the record type
This commit is contained in:
Edwin Brady 2020-02-01 13:32:39 +00:00
parent 6f4fa7ade9
commit cf27bbed66
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/TTImp/Elab/Record.idr
View File

@ -184,14 +184,19 @@ checkUpdate rig elabinfo nest env fc upds rec expected
_ => do (_, ty) <- checkImp rig elabinfo
nest env rec Nothing
pure ty
let solvemode = case elabMode elabinfo of
InLHS c => InLHS
_ => InTerm
delayOnFailure fc rig env recty needType $
\delayed =>
do exp <- getTerm recty
do solveConstraints solvemode Normal
exp <- getTerm recty
-- We can't just use the old NF on the second attempt,
-- because we might know more now, so recalculate it
let recty' = if delayed
then gnf env exp
else recty
logGlueNF 5 (show delayed ++ " record type " ++ show rec) env recty'
rcase <- recUpdate rig elabinfo fc nest env upds rec recty'
log 5 $ "Record update: " ++ show rcase
check rig elabinfo nest env rcase expected