diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index d52bb147c3..1dc4301f4a 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -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 diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 06141ff62b..31e4f5fc1d 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -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 diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index ba5e03f348..95ca225856 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -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 diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index 6107e8d1eb..048208b39d 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -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) diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 71f6857940..a358f41d4e 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -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, diff --git a/tests/idris2/basic/case002/WhereData.idr b/tests/idris2/basic/case002/WhereData.idr new file mode 100644 index 0000000000..a00d5444e8 --- /dev/null +++ b/tests/idris2/basic/case002/WhereData.idr @@ -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 diff --git a/tests/idris2/basic/case002/expected b/tests/idris2/basic/case002/expected new file mode 100644 index 0000000000..28f2441181 --- /dev/null +++ b/tests/idris2/basic/case002/expected @@ -0,0 +1 @@ +1/1: Building WhereData (WhereData.idr) diff --git a/tests/idris2/basic/case002/run b/tests/idris2/basic/case002/run new file mode 100755 index 0000000000..43b46c6ae5 --- /dev/null +++ b/tests/idris2/basic/case002/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --check WhereData.idr