diff options
author | Matthías Páll Gissurarson <mpg@mpg.is> | 2018-02-18 11:01:06 -0500 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2018-02-18 11:56:26 -0500 |
commit | 918c0b393663e88f89becdb8520de477ce6a5463 (patch) | |
tree | b87053a748568feb0231361d1b3ca5bd65fc3971 /compiler/main | |
parent | 1ede46d415757f53af33bc6672bd9d3fba7f205d (diff) | |
download | haskell-918c0b393663e88f89becdb8520de477ce6a5463.tar.gz |
Add valid refinement substitution suggestions for typed holes
This adds valid refinement substitution suggestions for typed holes and
documentation thereof.
Inspired by Agda's refinement facilities, this extends the typed holes
feature to be able to search for valid refinement substitutions, which
are substitutions that have one or more holes in them.
When the flag `-frefinement-level-substitutions=n` where `n > 0` is
passed, we also look for valid refinement substitutions, i.e.
substitutions that are valid, but adds more holes. Consider the
following:
f :: [Integer] -> Integer
f = _
Here the valid substitutions suggested will be (with the new
`-funclutter-valid-substitutions` flag for less verbosity set):
```
Valid substitutions include
f :: [Integer] -> Integer
product :: forall (t :: * -> *).
Foldable t => forall a. Num a => t a -> a
sum :: forall (t :: * -> *).
Foldable t => forall a. Num a => t a -> a
maximum :: forall (t :: * -> *).
Foldable t => forall a. Ord a => t a -> a
minimum :: forall (t :: * -> *).
Foldable t => forall a. Ord a => t a -> a
head :: forall a. [a] -> a
(Some substitutions suppressed; use -fmax-valid-substitutions=N or
-fno-max-valid-substitutions)
```
When the `-frefinement-level-substitutions=1` flag is given, we
additionally compute and report valid refinement substitutions:
```
Valid refinement substitutions include
foldl1 _ :: forall (t :: * -> *).
Foldable t => forall a. (a -> a -> a) -> t a -> a
foldr1 _ :: forall (t :: * -> *).
Foldable t => forall a. (a -> a -> a) -> t a -> a
head _ :: forall a. [a] -> a
last _ :: forall a. [a] -> a
error _ :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack => [Char] -> a
errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
(Some refinement substitutions suppressed; use
-fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
```
Which are substitutions with holes in them. This allows e.g. beginners
to discover the fold functions and similar.
We find these refinement suggestions by considering substitutions that
don't fit the type of the hole, but ones that would fit if given an
additional argument. We do this by creating a new type variable with
newOpenFlexiTyVarTy (e.g. `t_a1/m[tau:1]`), and then considering
substitutions of the type `t_a1/m[tau:1] -> v` where `v` is the type of
the hole. Since the simplifier is free to unify this new type variable
with any type (and it is cloned before each check to avoid
side-effects), we can now discover any identifiers that would fit if
given another identifier of a suitable type. This is then generalized
so that we can consider any number of additional arguments by setting
the `-frefinement-level-substitutions` flag to any number, and then
considering substitutions like e.g. `foldl _ _` with two additional
arguments.
This can e.g. help beginners discover the `fold` functions.
This could also help more advanced users figure out which morphisms
they can use when arrow chasing.
Then you could write `m = _ . m2 . m3` where `m2` and `m3` are some
morphisms, and not only get exact fits, but also help in finding
morphisms that might get you a little bit closer to where you want to
go in the diagram.
Reviewers: bgamari
Reviewed By: bgamari
Subscribers: rwbarton, thomie, carter
Differential Revision: https://phabricator.haskell.org/D4357
Diffstat (limited to 'compiler/main')
-rw-r--r-- | compiler/main/DynFlags.hs | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 6cea932bf5..dc4967d136 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -555,7 +555,9 @@ data GeneralFlag | Opt_PprShowTicks | Opt_ShowHoleConstraints | Opt_NoShowValidSubstitutions + | Opt_UnclutterValidSubstitutions | Opt_NoSortValidSubstitutions + | Opt_AbstractRefSubstitutions | Opt_ShowLoadedModules -- Suppress all coercions, them replacing with '...' @@ -805,6 +807,12 @@ data DynFlags = DynFlags { -- to show in type error messages maxValidSubstitutions :: Maybe Int, -- ^ Maximum number of substitutions to -- show in typed hole error messages + maxRefSubstitutions :: Maybe Int, -- ^ Maximum number of refinement + -- substitutions to show in typed hole + -- error messages + refLevelSubstitutions :: Maybe Int, -- ^ Maximum level of refinement for + -- refinement substitutions in typed + -- typed hole error messages maxUncoveredPatterns :: Int, -- ^ Maximum number of unmatched patterns to show -- in non-exhaustiveness warnings simplTickFactor :: Int, -- ^ Multiplier for simplifier ticks @@ -1665,6 +1673,8 @@ defaultDynFlags mySettings myLlvmTargets = ruleCheck = Nothing, maxRelevantBinds = Just 6, maxValidSubstitutions = Just 6, + maxRefSubstitutions = Just 6, + refLevelSubstitutions = Nothing, maxUncoveredPatterns = 4, simplTickFactor = 100, specConstrThreshold = Just 2000, @@ -3290,6 +3300,14 @@ dynamic_flags_deps = [ (intSuffix (\n d -> d { maxValidSubstitutions = Just n })) , make_ord_flag defFlag "fno-max-valid-substitutions" (noArg (\d -> d { maxValidSubstitutions = Nothing })) + , make_ord_flag defFlag "fmax-refinement-substitutions" + (intSuffix (\n d -> d { maxRefSubstitutions = Just n })) + , make_ord_flag defFlag "fno-max-refinement-substitutions" + (noArg (\d -> d { maxRefSubstitutions = Nothing })) + , make_ord_flag defFlag "frefinement-level-substitutions" + (intSuffix (\n d -> d { refLevelSubstitutions = Just n })) + , make_ord_flag defFlag "fno-refinement-level-substitutions" + (noArg (\d -> d { refLevelSubstitutions = Nothing })) , make_ord_flag defFlag "fmax-uncovered-patterns" (intSuffix (\n d -> d { maxUncoveredPatterns = n })) , make_ord_flag defFlag "fsimplifier-phases" @@ -3904,6 +3922,8 @@ fFlagsDeps = [ flagSpec "show-hole-constraints" Opt_ShowHoleConstraints, flagSpec "no-show-valid-substitutions" Opt_NoShowValidSubstitutions, flagSpec "no-sort-valid-substitutions" Opt_NoSortValidSubstitutions, + flagSpec "abstract-refinement-substitutions" Opt_AbstractRefSubstitutions, + flagSpec "unclutter-valid-substitutions" Opt_UnclutterValidSubstitutions, flagSpec "show-loaded-modules" Opt_ShowLoadedModules, flagSpec "whole-archive-hs-libs" Opt_WholeArchiveHsLibs ] |