RetroSearch Browse

Showing content from https://github.com/agda/agda/commit/ac2888a7addd0fe5533bee404690de1bb848e026 below:

File tree Expand file treeCollapse file tree 2 files changed

-4

lines changed

Filter options

Expand file treeCollapse file tree 2 files changed

-4

lines changed Original file line number Diff line number Diff line change


 @@ -45,6 +45,7 @@ import Agda.Utils.Maybe (filterMaybe)

45 45


 import Agda.Utils.Null

46 46


 import Agda.Syntax.Common.Pretty hiding ((<>))

47 47


 import qualified Agda.Syntax.Common.Pretty as P

48

+
 import Agda.Utils.Set1 ( Set1 )

48 49


 import Agda.Utils.Singleton

49 50


 import qualified Agda.Utils.Map as Map

50 51


 @@ -531,7 +532,9 @@ data ResolvedName

531 532


 FieldName (List1 AbstractName) -- ^ @('FldName' ==) . 'anameKind'@ for all names.

532 533 533 534


 | -- | Data or record constructor name.

534

-
 ConstructorName (Set Induction) (List1 AbstractName) -- ^ @isJust . 'isConName' . 'anameKind'@ for all names.

535

+
 ConstructorName

536

+
 (Set1 Induction) -- ^ 'Inductive' or 'CoInductive' or both.

537

+
 (List1 AbstractName) -- ^ @isJust . 'isConName' . 'anameKind'@ for all names.

535 538 536 539


 | -- | Name of pattern synonym.

537 540


 PatternSynResName (List1 AbstractName) -- ^ @('PatternSynName' ==) . 'anameKind'@ for all names.

Original file line number Diff line number Diff line change


 @@ -380,10 +380,10 @@ tryResolveName kinds names x = do

380 380


 possibleBaseNames = filter (canHaveSuffix . anameName . fst) $ possibleNames xbase

381 381


 suffixedNames = (,) <$> fromConcreteSuffix xsuffix <*> nonEmpty possibleBaseNames

382 382


 case (nonEmpty $ possibleNames x) of

383

-
 Just ds | let ks = fmap (isConName . anameKind . fst) ds

384

-
 , all isJust ks

383

+
 Just ds | Just ks <- traverse (isConName . anameKind . fst) ds

384

+
  -- all names resolve to a constructor name

385 385


 , isNothing suffixedNames ->

386

-
 return $ ConstructorName (Set.fromList $ List1.catMaybes ks) $ fmap (upd . fst) ds

386

+
 return $ ConstructorName (Set1.fromList ks) $ fmap (upd . fst) ds

387 387 388 388


 Just ds | all ((FldName ==) . anameKind . fst) ds , isNothing suffixedNames ->

389 389


 return $ FieldName $ fmap (upd . fst) ds

You can’t perform that action at this time.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4