idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-10 13:44:21 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #501 from ohad/undotting-subsingletons

Browse Source 
Take into account syntactic sub-singletons when dotting in patterns
This commit is contained in:
Edwin Brady 2020-07-28 00:23:46 +01:00 committed by GitHub
commit 78ecd8a9f1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 25 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
src/TTImp/Elab/App.idr
View File

@ -315,11 +315,17 @@ mutual
else pure () else pure ()
checkPatTyValid fc defs env _ _ _ = pure () checkPatTyValid fc defs env _ _ _ = pure ()
dotErased : {auto c : Ref Ctxt Defs} -> dotErased : {auto c : Ref Ctxt Defs} -> (argty : NF vars) ->
Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp
dotErased mn argpos (InLHS lrig ) rig tm dotErased argty mn argpos (InLHS lrig ) rig tm
= if not (isErased lrig) && isErased rig = if not (isErased lrig) && isErased rig
then then do
-- if the argument type aty has a single constructor, there's no need
-- to dot it
mconsCount <- countConstructors argty
if mconsCount == Just 1 || mconsCount == Just 0
then pure tm
else
-- if argpos is an erased position of 'n', leave it, otherwise dot if -- if argpos is an erased position of 'n', leave it, otherwise dot if
-- necessary -- necessary
do defs <- get Ctxt do defs <- get Ctxt
@ -328,8 +334,21 @@ mutual
if argpos `elem` safeErase gdef if argpos `elem` safeErase gdef
then pure tm then pure tm
else pure $ dotTerm tm else pure $ dotTerm tm
else pure tm else pure tm
where where
||| Count the constructors of a fully applied concrete datatype
countConstructors : NF vars -> Core (Maybe Nat)
countConstructors (NTCon _ tycName _ n args) =
if length args == n
then do defs <- get Ctxt
Just gdef <- lookupCtxtExact tycName (gamma defs)
| Nothing => pure Nothing
let (TCon _ _ _ _ _ _ datacons _) = gdef.definition
| _ => pure Nothing
pure (Just (length datacons))
else pure Nothing
countConstructors _ = pure Nothing
dotTerm : RawImp -> RawImp dotTerm : RawImp -> RawImp
dotTerm tm dotTerm tm
= case tm of = case tm of
@ -340,7 +359,7 @@ mutual
IAs _ _ _ (Implicit _ _) => tm IAs _ _ _ (Implicit _ _) => tm
IAs fc p t arg => IAs fc p t (IMustUnify fc ErasedArg tm) IAs fc p t arg => IAs fc p t (IMustUnify fc ErasedArg tm)
_ => IMustUnify (getFC tm) ErasedArg tm _ => IMustUnify (getFC tm) ErasedArg tm
dotErased _ _ _ _ tm = pure tm dotErased _ _ _ _ _ tm = pure tm
-- Check the rest of an application given the argument type and the -- Check the rest of an application given the argument type and the
-- raw argument. We choose elaboration order depending on whether we know -- raw argument. We choose elaboration order depending on whether we know
@ -367,7 +386,7 @@ mutual
checkRestApp rig argRig elabinfo nest env fc tm x aty sc checkRestApp rig argRig elabinfo nest env fc tm x aty sc
(n, argpos) arg_in expargs impargs knownret expty (n, argpos) arg_in expargs impargs knownret expty
= do defs <- get Ctxt = do defs <- get Ctxt
arg <- dotErased n argpos (elabMode elabinfo) argRig arg_in arg <- dotErased aty n argpos (elabMode elabinfo) argRig arg_in
kr <- if knownret kr <- if knownret
then pure True then pure True
else do sc' <- sc defs (toClosure defaultOpts env (Erased fc False)) else do sc' <- sc defs (toClosure defaultOpts env (Erased fc False))