mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 06:29:37 +03:00
Check datatypes are not redefined
We were checking, but only seeing if the type constructor was the same, which is not enough. Fixes #1776.
This commit is contained in:
parent
58dd2b50d7
commit
fbcd64372b
@ -479,8 +479,8 @@ checkUndefined fc n
|
|||||||
isUndefined :: FC -> Name -> Idris Bool
|
isUndefined :: FC -> Name -> Idris Bool
|
||||||
isUndefined fc n
|
isUndefined fc n
|
||||||
= do i <- getContext
|
= do i <- getContext
|
||||||
case lookupTy n i of
|
case lookupTyExact n i of
|
||||||
(_:_) -> return False
|
Just _ -> return False
|
||||||
_ -> return True
|
_ -> return True
|
||||||
|
|
||||||
setContext :: Context -> Idris ()
|
setContext :: Context -> Idris ()
|
||||||
|
@ -66,9 +66,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
|
|||||||
undef <- isUndefined fc n
|
undef <- isUndefined fc n
|
||||||
(cty, _, t, inacc) <- buildType info syn fc [] n t_in
|
(cty, _, t, inacc) <- buildType info syn fc [] n t_in
|
||||||
-- if n is defined already, make sure it is just a type declaration
|
-- if n is defined already, make sure it is just a type declaration
|
||||||
-- with the same type we've just elaborated
|
-- with the same type we've just elaborated, and no constructors
|
||||||
|
-- yet
|
||||||
i <- getIState
|
i <- getIState
|
||||||
checkDefinedAs fc n cty (tt_ctxt i)
|
checkDefinedAs fc n cty i
|
||||||
-- temporary, to check cons
|
-- temporary, to check cons
|
||||||
when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
|
when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
|
||||||
let cnameinfo = cinfo info (map cname dcons)
|
let cnameinfo = cinfo info (map cname dcons)
|
||||||
@ -124,14 +125,18 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
|
|||||||
[oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
|
[oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
|
||||||
_ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
|
_ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
|
||||||
|
|
||||||
checkDefinedAs fc n t ctxt
|
checkDefinedAs fc n t i
|
||||||
= case lookupDef n ctxt of
|
= let defined = tclift $ tfail (At fc (AlreadyDefined n))
|
||||||
|
ctxt = tt_ctxt i in
|
||||||
|
case lookupDef n ctxt of
|
||||||
[] -> return ()
|
[] -> return ()
|
||||||
[TyDecl _ ty] ->
|
[TyDecl _ ty] ->
|
||||||
case converts ctxt [] t ty of
|
case converts ctxt [] t ty of
|
||||||
OK () -> return ()
|
OK () -> case lookupCtxtExact n (idris_datatypes i) of
|
||||||
_ -> tclift $ tfail (At fc (AlreadyDefined n))
|
Nothing -> return ()
|
||||||
_ -> tclift $ tfail (At fc (AlreadyDefined n))
|
_ -> defined
|
||||||
|
_ -> defined
|
||||||
|
_ -> defined
|
||||||
-- parameters are names which are unchanged across the structure,
|
-- parameters are names which are unchanged across the structure,
|
||||||
-- which appear exactly once in the return type of a constructor
|
-- which appear exactly once in the return type of a constructor
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user