mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
[ fix ] consider nest when guessing scrutinee (#3070)
This commit is contained in:
parent
9d083154a5
commit
0029257eec
@ -128,9 +128,7 @@ elabImplementation : {vars : _} ->
|
||||
elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named impName_in nusing mbody
|
||||
= do -- let impName_in = maybe (mkImplName fc iname ps) id impln
|
||||
-- If we're in a nested block, update the name
|
||||
let impName_nest = case lookup impName_in (names nest) of
|
||||
Just (Just n', _) => n'
|
||||
_ => impName_in
|
||||
let impName_nest = mapNestedName nest impName_in
|
||||
impName <- inCurrentNS impName_nest
|
||||
-- The interface name might be qualified, so check if it's an
|
||||
-- alias for something
|
||||
|
@ -836,9 +836,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
|
||||
" to " ++ show expargs ++ "\n\tFunction type " ++
|
||||
(show !(toFullNames fnty)) ++ "\n\tExpected app type "
|
||||
++ show exptyt))
|
||||
let fn = case lookup n (names nest) of
|
||||
Just (Just n', _) => n'
|
||||
_ => n
|
||||
let fn = mapNestedName nest n
|
||||
normalisePrims prims env
|
||||
!(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs autoargs namedargs False exp)
|
||||
where
|
||||
|
@ -13,6 +13,7 @@ import Core.Value
|
||||
import Idris.Syntax
|
||||
import Idris.REPL.Opts
|
||||
|
||||
import TTImp.Elab.App
|
||||
import TTImp.Elab.Check
|
||||
import TTImp.Elab.Delayed
|
||||
import TTImp.Elab.ImplicitBind
|
||||
@ -460,7 +461,7 @@ checkCase rig elabinfo nest env fc opts scr scrty_in alts exp
|
||||
= case getFn x of
|
||||
IVar _ n =>
|
||||
do defs <- get Ctxt
|
||||
[(n', (_, ty))] <- lookupTyName n (gamma defs)
|
||||
[(_, (_, ty))] <- lookupTyName (mapNestedName nest n) (gamma defs)
|
||||
| _ => guessScrType xs
|
||||
Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty)
|
||||
| _ => guessScrType xs
|
||||
|
@ -103,44 +103,38 @@ localHelper {vars} nest env nestdecls_in func
|
||||
-- Update the names in the declarations to the new 'nested' names.
|
||||
-- When we encounter the names in elaboration, we'll update to an
|
||||
-- application of the nested name.
|
||||
newName : NestedNames vars -> Name -> Name
|
||||
newName nest n
|
||||
= case lookup n (names nest) of
|
||||
Just (Just n', _) => n'
|
||||
_ => n
|
||||
|
||||
updateTyName : NestedNames vars -> ImpTy -> ImpTy
|
||||
updateTyName nest (MkImpTy loc' nameLoc n ty)
|
||||
= MkImpTy loc' nameLoc (newName nest n) ty
|
||||
= MkImpTy loc' nameLoc (mapNestedName nest n) ty
|
||||
|
||||
updateDataName : NestedNames vars -> ImpData -> ImpData
|
||||
updateDataName nest (MkImpData loc' n tycons dopts dcons)
|
||||
= MkImpData loc' (newName nest n) tycons dopts
|
||||
= MkImpData loc' (mapNestedName nest n) tycons dopts
|
||||
(map (updateTyName nest) dcons)
|
||||
updateDataName nest (MkImpLater loc' n tycons)
|
||||
= MkImpLater loc' (newName nest n) tycons
|
||||
= MkImpLater loc' (mapNestedName nest n) tycons
|
||||
|
||||
updateFieldName : NestedNames vars -> IField -> IField
|
||||
updateFieldName nest (MkIField fc rigc piinfo n rawimp)
|
||||
= MkIField fc rigc piinfo (newName nest n) rawimp
|
||||
= MkIField fc rigc piinfo (mapNestedName nest n) rawimp
|
||||
|
||||
updateRecordName : NestedNames vars -> ImpRecord -> ImpRecord
|
||||
updateRecordName nest (MkImpRecord fc n params opts conName fields)
|
||||
= MkImpRecord fc (newName nest n)
|
||||
= MkImpRecord fc (mapNestedName nest n)
|
||||
params
|
||||
opts
|
||||
(newName nest conName)
|
||||
(mapNestedName nest conName)
|
||||
(map (updateFieldName nest) fields)
|
||||
|
||||
updateRecordNS : NestedNames vars -> Maybe String -> Maybe String
|
||||
updateRecordNS _ Nothing = Nothing
|
||||
updateRecordNS nest (Just ns) = Just $ show $ newName nest (UN $ mkUserName ns)
|
||||
updateRecordNS nest (Just ns) = Just $ show $ mapNestedName nest (UN $ mkUserName ns)
|
||||
|
||||
updateName : NestedNames vars -> ImpDecl -> ImpDecl
|
||||
updateName nest (IClaim loc' r vis fnopts ty)
|
||||
= IClaim loc' r vis fnopts (updateTyName nest ty)
|
||||
updateName nest (IDef loc' n cs)
|
||||
= IDef loc' (newName nest n) cs
|
||||
= IDef loc' (mapNestedName nest n) cs
|
||||
updateName nest (IData loc' vis mbt d)
|
||||
= IData loc' vis mbt (updateDataName nest d)
|
||||
updateName nest (IRecord loc' ns vis mbt imprecord)
|
||||
|
@ -38,6 +38,13 @@ Weaken NestedNames where
|
||||
wknName (n, (mn, vars, rep))
|
||||
= (n, (mn, map weaken vars, \fc, nt => weaken (rep fc nt)))
|
||||
|
||||
-- replace nested name with full name
|
||||
export
|
||||
mapNestedName : NestedNames vars -> Name -> Name
|
||||
mapNestedName nest n = case lookup n (names nest) of
|
||||
(Just (Just n', _)) => n'
|
||||
_ => n
|
||||
|
||||
-- Unchecked terms, with implicit arguments
|
||||
-- This is the raw, elaboratable form.
|
||||
-- Higher level expressions (e.g. case, pattern matching let, where blocks,
|
||||
|
11
tests/idris2/basic/case002/WhereData.idr
Normal file
11
tests/idris2/basic/case002/WhereData.idr
Normal file
@ -0,0 +1,11 @@
|
||||
module Main
|
||||
|
||||
foo : Int -> Int
|
||||
foo x = case isLT of
|
||||
Yes => x*2
|
||||
No => x*4
|
||||
where
|
||||
data MyLT = Yes | No
|
||||
|
||||
isLT : MyLT
|
||||
isLT = if x < 20 then Yes else No
|
1
tests/idris2/basic/case002/expected
Normal file
1
tests/idris2/basic/case002/expected
Normal file
@ -0,0 +1 @@
|
||||
1/1: Building WhereData (WhereData.idr)
|
3
tests/idris2/basic/case002/run
Executable file
3
tests/idris2/basic/case002/run
Executable file
@ -0,0 +1,3 @@
|
||||
rm -rf build
|
||||
|
||||
$1 --no-color --console-width 0 --no-banner --check WhereData.idr
|
Loading…
Reference in New Issue
Block a user