Commit 918c0b39 authored by Committed by Ben Gamari
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
Showing with 857 additions and 79 deletions
This diff is collapsed.
This diff is collapsed.