check that a name is unused before adding a def
This commit is contained in:
parent
8d7326917a
commit
0987b91596
|
@ -8,3 +8,9 @@ def repeat-enum-case : {a} → {a} =
|
||||||
|
|
||||||
#[fail "duplicate tags"]
|
#[fail "duplicate tags"]
|
||||||
def repeat-enum-type : {a, a} = 'a
|
def repeat-enum-type : {a, a} = 'a
|
||||||
|
|
||||||
|
#[fail "double-def.X has already been defined"]
|
||||||
|
namespace double-def {
|
||||||
|
def0 X : ★ = {a}
|
||||||
|
def0 X : ★ = {a}
|
||||||
|
}
|
||||||
|
|
|
@ -335,6 +335,8 @@ export covering
|
||||||
fromPDef : PDefinition -> Eff FromParserPure NDefinition
|
fromPDef : PDefinition -> Eff FromParserPure NDefinition
|
||||||
fromPDef (MkPDef qty pname ptype pterm defLoc) = do
|
fromPDef (MkPDef qty pname ptype pterm defLoc) = do
|
||||||
name <- fromPBaseNameNS pname
|
name <- fromPBaseNameNS pname
|
||||||
|
when !(getsAt DEFS $ isJust . lookup name) $ do
|
||||||
|
throw $ AlreadyExists defLoc name
|
||||||
gqty <- globalPQty qty.val qty.loc
|
gqty <- globalPQty qty.val qty.loc
|
||||||
let sqty = globalToSubj gqty
|
let sqty = globalToSubj gqty
|
||||||
type <- traverse fromPTerm ptype
|
type <- traverse fromPTerm ptype
|
||||||
|
|
|
@ -32,6 +32,7 @@ data Error =
|
||||||
| DimNameInTerm Loc PBaseName
|
| DimNameInTerm Loc PBaseName
|
||||||
| DisplacedBoundVar Loc PName
|
| DisplacedBoundVar Loc PName
|
||||||
| WrapTypeError TypeError
|
| WrapTypeError TypeError
|
||||||
|
| AlreadyExists Loc Name
|
||||||
| LoadError Loc FilePath FileError
|
| LoadError Loc FilePath FileError
|
||||||
| ExpectedFail Loc
|
| ExpectedFail Loc
|
||||||
| WrongFail String Error Loc
|
| WrongFail String Error Loc
|
||||||
|
@ -112,6 +113,10 @@ parameters {opts : LayoutOpts} (showContext : Bool)
|
||||||
prettyError (WrapTypeError err) =
|
prettyError (WrapTypeError err) =
|
||||||
Typing.prettyError showContext $ trimContext 2 err
|
Typing.prettyError showContext $ trimContext 2 err
|
||||||
|
|
||||||
|
prettyError (AlreadyExists loc name) = pure $
|
||||||
|
vsep [!(prettyLoc loc),
|
||||||
|
sep [!(prettyFree name), "has already been defined"]]
|
||||||
|
|
||||||
prettyError (LoadError loc file err) = pure $
|
prettyError (LoadError loc file err) = pure $
|
||||||
vsep [!(prettyLoc loc),
|
vsep [!(prettyLoc loc),
|
||||||
"couldn't load file" <++> text file,
|
"couldn't load file" <++> text file,
|
||||||
|
|
Loading…
Reference in New Issue