@@ -116,6 +116,41 @@ mkPrec Prefix = Prefix
116116 show ((x, DeclaredFixity y), _ ) = show x ++ " at " ++ show y. fc
117117 show ((x, UndeclaredFixity ), _ ) = show x
118118
119+ checkConflictingBinding : Ref Ctxt Defs =>
120+ Ref Syn SyntaxInfo =>
121+ WithFC OpStr -> (foundFixity : FixityDeclarationInfo) ->
122+ (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
123+ checkConflictingBinding opName foundFixity use_site rhs
124+ = if isCompatible foundFixity use_site
125+ then pure ()
126+ else throw $ OperatorBindingMismatch
127+ {print = byShow} opName. fc foundFixity use_site (opNameToEither opName. val) rhs ! candidates
128+ where
129+
130+ isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
131+ isCompatible UndeclaredFixity (NoBinder lhs) = True
132+ isCompatible UndeclaredFixity _ = False
133+ isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo. bindingInfo == NotBinding
134+ isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo. bindingInfo == Typebind
135+ isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo. bindingInfo == Autobind
136+ isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr)
137+ = fixInfo. bindingInfo == Autobind
138+
139+ keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool
140+ keepCompatibleBinding compatibleBinder (name, def) = do
141+ fixities <- getFixityInfo (nameRoot name)
142+ let compatible = any (\ (_ , fx) => fx. bindingInfo == use_site. getBinder) fixities
143+ pure compatible
144+
145+ candidates : Core (List String)
146+ candidates = do let DeclaredFixity fxInfo = foundFixity
147+ | _ => pure [] -- if there is no declared fixity we can't know what's
148+ -- supposed to go there.
149+ Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo. bindingInfo)} opName. val. toName
150+ | Nothing => pure []
151+ ns <- currentNS <$> get Ctxt
152+ pure (showSimilarNames ns opName. val. toName nm cs)
153+
119154-- Check that an operator does not have any conflicting fixities in scope.
120155-- Each operator can have its fixity defined multiple times across multiple
121156-- modules as long as the fixities are consistent. If they aren't, the fixity
@@ -163,41 +198,6 @@ checkConflictingFixities usageType opn
163198 For example: %hide \{show fxName}
164199 " " "
165200
166- checkConflictingBinding : Ref Ctxt Defs =>
167- Ref Syn SyntaxInfo =>
168- WithFC OpStr -> (foundFixity : FixityDeclarationInfo) ->
169- (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
170- checkConflictingBinding opName foundFixity use_site rhs
171- = if isCompatible foundFixity use_site
172- then pure ()
173- else throw $ OperatorBindingMismatch
174- {print = byShow} opName. fc foundFixity use_site (opNameToEither opName. val) rhs ! candidates
175- where
176-
177- isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
178- isCompatible UndeclaredFixity (NoBinder lhs) = True
179- isCompatible UndeclaredFixity _ = False
180- isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo. bindingInfo == NotBinding
181- isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo. bindingInfo == Typebind
182- isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo. bindingInfo == Autobind
183- isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr)
184- = fixInfo. bindingInfo == Autobind
185-
186- keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool
187- keepCompatibleBinding compatibleBinder (name, def) = do
188- fixities <- getFixityInfo (nameRoot name)
189- let compatible = any (\ (_ , fx) => fx. bindingInfo == use_site. getBinder) fixities
190- pure compatible
191-
192- candidates : Core (List String)
193- candidates = do let DeclaredFixity fxInfo = foundFixity
194- | _ => pure [] -- if there is no declared fixity we can't know what's
195- -- supposed to go there.
196- Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo. bindingInfo)} opName. val. toName
197- | Nothing => pure []
198- ns <- currentNS <$> get Ctxt
199- pure (showSimilarNames ns opName. val. toName nm cs)
200-
201201checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool
202202
203203-- If the fixity declaration is not binding, there are no restrictions
0 commit comments