Add skip equation and skip case pattern edits

doc/source/edits.rst

@@ -147,6 +147,143 @@ Examples:
 
      skip method GHC.Base.Monad fail
 
+``skip equation`` – skip one equation of a function definition
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. index::
+  single: skip equation, edit
+
+Format:
+  | **skip equation** *qualified_function* *pattern* ...
+
+Effect:
+  Skip the equation of the function definition whose arguments are the specified
+  patterns.  Guards are not considered, only the patterns themselves.
+
+  For example, consider the following (silly) function definition:
+
+  .. code-block:: haskell
+
+     redundant :: Maybe Bool -> Maybe Bool -> Bool
+     redundant (Just True)  _        = False
+     redundant (Just False) _        = True
+     redundant _            _        = True
+     redundant _            (Just b) = b
+
+  The last case is redundant, so Coq will reject this definition.  However, we
+  can add the following edit:
+
+  .. code-block:: shell
+
+     skip equation ModuleName.redundant _ (Some b)
+  
+  And the last case will be deleted on the Coq side:
+
+  .. code-block:: coq
+
+     Definition redundant : option bool -> option bool -> bool :=
+       fun arg_0__ arg_1__ =>
+         match arg_0__, arg_1__ with
+         | Some true, _ => false
+         | Some false, _ => true
+         | _, _ => true
+         end.
+
+  Note that you have to use the translated name (``Some`` vs. ``Just``), and
+  most constructor names will be fully qualified.
+
+  Why would you want this?  This edit is most useful in tandem with ``skip
+  constructor`` (which see).  Suppose we have a function where the final catch-all
+  case can only match skipped constructors, such as
+
+  .. code-block:: haskell
+
+     data T = TranslateMe
+            | SkipMe
+     
+     function :: T -> Bool
+     function TranslateMe = True
+     function _           = False
+
+  Then, on skipping ``SkipMe``, this function's ``_`` case will be redundant,
+  and Coq would reject it.  We can fix this with
+
+   .. code-block:: shell
+
+      skip equation ModuleName.function _
+
+  to translate just the ``TranslateMe`` case.
+
+  See also ``skip case pattern`` for the equivalent edit for ``case`` and lambda-case
+  expressions.
+
+Examples:
+   .. code-block:: shell
+
+     skip equation ModuleName.redundant _ (Some b)
+     skip equation Core.hasSomeUnfolding _
+
+``skip case pattern`` – skip one alternative of a ``case`` expression
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. index::
+  single: skip case pattern, edit
+
+Format:
+  | **skip case pattern** *pattern*
+
+Effect:
+  Skip any alternative of a ``case`` expression (or a lambda-case expression)
+  which matches against the given pattern. Guards are not considered, only the
+  pattern itself.
+
+  For example, consider the following (silly) function definition:
+
+  .. code-block:: haskell
+
+     redundant :: Bool -> Bool
+     redundant b = not (case b of
+                          True  -> False
+                          False -> True
+                          _     -> True)
+
+  The last case is redundant, so Coq will reject this definition.  However, we
+  can add the following edit:
+
+  .. code-block:: shell
+
+     in ModuleName.redundant skip case pattern _
+  
+  And the last case will be deleted on the Coq side (reformatted):
+
+  .. code-block:: coq
+
+     Definition redundant : bool -> bool :=
+       fun b => negb (match b with
+                      | true => false
+                      | false => true
+                      end).
+
+  You can use an arbitrary pattern, not simply ``_``; constructor names must be
+  fully qualified and the names used must be those that appear *after* renaming.
+
+  Why would you want this?  This edit is most useful in tandem with ``skip
+  constructor`` (which see); see the discussion in ``skip equation`` for a
+  worked example (with a named function).
+
+  This edit is unusual in that you *very likely* want to use it with the ``in``
+  meta-edit to scope its effects to within a specific definition.  However, this
+  isn't mandatory; if, for some reason, you want to skip every ``_`` in every
+  ``case``, then ``skip case pattern _`` will do what you want.
+
+  See also ``skip equation`` for the equivalent edit for named functions.
+
+Examples:
+   .. code-block:: shell
+
+     in ModuleName.redundant skip case pattern _
+
+
 ``skip module`` – skip a module import
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 

emacs/edits.el

@@ -1,6 +1,6 @@
 (define-generic-mode hs-to-coq-edits-mode
   '(?#)
-  '("value" "type" "data" "synonym" "arguments" "parameters" "indices" "redefine" "skip" "manual" "import" "notation" "class" "kinds" "delete" "unused" "variables" "axiomatize" "definition" "unaxiomatize" "termination" "deferred" "corecursive" "coinductive" "obligations" "method" "rename" "rewrite" "order" "module" "add" "scope" "constructor" "simple" "inline" "mutual" "set" "no" "collapse" "=" ":->")
+  '("value" "type" "data" "synonym" "arguments" "parameters" "indices" "redefine" "skip" "manual" "import" "notation" "class" "kinds" "delete" "unused" "variables" "axiomatize" "definition" "unaxiomatize" "termination" "deferred" "corecursive" "coinductive" "obligations" "method" "rename" "rewrite" "order" "module" "add" "scope" "constructor" "simple" "inline" "mutual" "set" "no" "collapse" "equation" "case" "pattern" "=" ":->")
   '(("^\\s-*\\<in\\>" . font-lock-keyword-face) ("\\<Qed\\>" . font-lock-builtin-face) ("\\<Defined\\>" . font-lock-builtin-face) ("\\<Admitted\\>" . font-lock-builtin-face) ("\\<as\\>" . font-lock-type-face) ("\\<fun\\>" . font-lock-type-face) ("\\<fix\\>" . font-lock-type-face) ("\\<cofix\\>" . font-lock-type-face) ("\\<forall\\>" . font-lock-type-face) ("\\<match\\>" . font-lock-type-face) ("\\<end\\>" . font-lock-type-face) ("\\<struct\\>" . font-lock-type-face) ("\\<with\\>" . font-lock-type-face) ("\\<for\\>" . font-lock-type-face) ("\\<measure\\>" . font-lock-type-face) ("\\<wf\\>" . font-lock-type-face) ("\\<Inductive\\>" . font-lock-builtin-face) ("\\<CoInductive\\>" . font-lock-builtin-face) ("\\<Definition\\>" . font-lock-builtin-face) ("\\<Instance\\>" . font-lock-builtin-face) ("\\<Let\\>" . font-lock-builtin-face) ("\\<let\\>" . font-lock-builtin-face) ("\\<in\\>" . font-lock-builtin-face) ("\\<Fixpoint\\>" . font-lock-builtin-face) ("\\<CoFixpoint\\>" . font-lock-builtin-face) ("\\<Local\\>" . font-lock-builtin-face) ("\\<Axiom\\>" . font-lock-builtin-face) ("\\<Theorem\\>" . font-lock-builtin-face) ("\\<Lemma\\>" . font-lock-builtin-face) ("\\<Remark\\>" . font-lock-builtin-face) ("\\<Fact\\>" . font-lock-builtin-face) ("\\<Corollary\\>" . font-lock-builtin-face) ("\\<Proposition\\>" . font-lock-builtin-face) ("\\<Example\\>" . font-lock-builtin-face) ("\\<Proof\\>" . font-lock-builtin-face))
   '("[./]edits\\'")
   nil

examples/tests/Makefile

@@ -34,7 +34,8 @@ PASS = \
   RedefineAddAxiom \
   AddTheorem \
   Existential \
-	SkipConstructor
+	SkipConstructor \
+	SkipMatches
 
 # tests that *should* pass but currently fail
 TODO_PASS = \

examples/tests/SkipConstructor.hs

@@ -27,7 +27,7 @@ nestedPattern (True, Just Ok2)    = Just Ok1
 nestedPattern (True, Just SkipMe) = Just SkipMe -- This case should be skipped
 nestedPattern _                   = Nothing
 
--- Issue #130
+-- Issue #130; see also issue #135
 extraUnderscore :: T -> T
 extraUnderscore Ok1             = Ok1
 extraUnderscore Ok2             = Ok2

examples/tests/SkipConstructor/edits

@@ -2,5 +2,8 @@ skip constructor SkipConstructor.NonPositive
 skip constructor SkipConstructor.Record
 skip constructor SkipConstructor.SkipMe
 
+# In the future, it'd be great to infer this – see issue #135
+skip equation SkipConstructor.extraUnderscore _
+
 # We don't link against GHC
 skip SkipConstructor.Default__T

examples/tests/SkipMatches.hs

@@ -0,0 +1,36 @@
+{-# LANGUAGE LambdaCase #-}
+{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
+
+module SkipMatches where
+
+-- See also issue #130
+skipEquation :: Bool -> Bool
+skipEquation True  = False
+skipEquation False = True
+skipEquation _     = True -- This underscore case is redundant and needs to be eliminated
+
+skipEquationMultipleArgs :: Bool -> Bool -> Bool
+skipEquationMultipleArgs True  _     = False
+skipEquationMultipleArgs False _     = True
+skipEquationMultipleArgs _     True  = True  -- This case is redundant and needs to be eliminated
+skipEquationMultipleArgs _     False = False -- This case is redundant and needs to be eliminated
+
+skipCasePattern :: Bool -> Bool
+skipCasePattern b = case b of
+  True   -> False
+  False  -> True
+  _      -> True -- This underscore case is redundant and needs to be eliminated (locally)
+  ignore -> True -- This variable case is redundant and needs to be eliminated (globally)
+
+skipLambdaCasePattern :: Bool -> Bool
+skipLambdaCasePattern = \case
+  True   -> False
+  False  -> True
+  _      -> True -- This underscore case is redundant and needs to be eliminated (locally)
+  ignore -> True -- This variable case is redundant and needs to be eliminated (globally)
+
+preserveCasePattern :: Bool -> Bool
+preserveCasePattern = \case
+  True   -> False
+  _      -> True -- This underscore case is NOT redundant
+  ignore -> True -- This variable case is redundant and needs to be eliminated (globally)

examples/tests/SkipMatches/edits

@@ -0,0 +1,11 @@
+skip equation SkipMatches.skipEquation _
+
+# We have to write the patterns using the *translated* names
+skip equation SkipMatches.skipEquationMultipleArgs _ true
+skip equation SkipMatches.skipEquationMultipleArgs _ false
+
+in SkipMatches.skipCasePattern       skip case pattern _
+in SkipMatches.skipLambdaCasePattern skip case pattern _
+
+skip case pattern ignore
+in SkipMatches.redundant skip case pattern _

src/lib/HsToCoq/ConvertHaskell/Expr.hs

@@ -130,10 +130,11 @@ convertExpr' (HsLit lit) =
     HsDoublePrim _ _       -> convUnsupported "`Double#' literals"
 
 convertExpr' (HsLam mg) =
-  uncurry Fun <$> convertFunction mg
+  uncurry Fun <$> convertFunction [] mg -- We don't skip any equations in an ordinary lambda
 
-convertExpr' (HsLamCase mg) =
-  uncurry Fun <$> convertFunction mg
+convertExpr' (HsLamCase mg) = do
+  skipPats <- views (edits.skippedCasePatterns) (S.map pure)
+  uncurry Fun <$> convertFunction skipPats mg
 
 convertExpr' (HsApp e1 e2) =
   App1 <$> convertLExpr e1 <*> convertLExpr e2
@@ -181,8 +182,9 @@ convertExpr' (ExplicitTuple exprs _boxity) = do
   pure $ maybe id Fun (nonEmpty $ map (Inferred Coq.Explicit . Ident) args) tuple
 
 convertExpr' (HsCase e mg) = do
-  scrut <- convertLExpr e
-  bindIn "scrut" scrut $ \scrut -> convertMatchGroup [scrut] mg
+  scrut    <- convertLExpr e
+  skipPats <- views (edits.skippedCasePatterns) (S.map pure)
+  bindIn "scrut" scrut $ \scrut -> convertMatchGroup skipPats [scrut] mg
 
 convertExpr' (HsIf overloaded c t f) =
   if maybe True isNoSyntaxExpr overloaded
@@ -439,13 +441,16 @@ convertLExpr = convertExpr . unLoc
 
 --------------------------------------------------------------------------------
 
-convertFunction :: LocalConvMonad r m => MatchGroup GhcRn (LHsExpr GhcRn) -> m (Binders, Term)
-convertFunction mg | Just alt <- isTrivialMatch mg = convTrivialMatch alt
-convertFunction mg = do
+convertFunction :: LocalConvMonad r m
+                => Set (NonEmpty NormalizedPattern)
+                -> MatchGroup GhcRn (LHsExpr GhcRn)
+                -> m (Binders, Term)
+convertFunction _ mg | Just alt <- isTrivialMatch mg = convTrivialMatch alt
+convertFunction skipEqns mg = do
   let n_args = matchGroupArity mg
   args <- replicateM n_args (genqid "arg") >>= maybe err pure . nonEmpty
   let argBinders = (Inferred Coq.Explicit . Ident) <$> args
-  match <- convertMatchGroup (Qualid <$> args) mg
+  match <- convertMatchGroup skipEqns (Qualid <$> args) mg
   pure (argBinders, match)
  where
    err = convUnsupported "convertFunction: Empty argument list"
@@ -654,12 +659,15 @@ chainFallThroughs cases failure = go (reverse cases) failure where
 -- * Group patterns that are mutually exclusive, and put them in match-with clauses.
 --   Add a catch-all case if that group is not complete already.
 -- * Chain these groups.
-convertMatchGroup :: LocalConvMonad r m =>
-    NonEmpty Term ->
-    MatchGroup GhcRn (LHsExpr GhcRn) ->
-    m Term
-convertMatchGroup args (MG (L _ alts) _ _ _) = do
-    convAlts <- catMaybes <$> traverse (convertMatch . unLoc) alts
+convertMatchGroup :: LocalConvMonad r m
+                  => Set (NonEmpty NormalizedPattern)
+                  -> NonEmpty Term
+                  -> MatchGroup GhcRn (LHsExpr GhcRn)
+                  -> m Term
+convertMatchGroup skipEqns args (MG (L _ alts) _ _ _) = do
+    allConvAlts <- traverse (convertMatch . unLoc) alts
+    let convAlts = [alt | Just alt@(MultPattern pats, _, _) <- allConvAlts
+                        , (normalizePattern <$> pats) `notElem` skipEqns ]
     -- TODO: Group
     convGroups <- groupMatches convAlts
 
@@ -886,7 +894,9 @@ convertTypedBinding convHsTy FunBind{..}   = do
             then case unLoc $ mg_alts fun_matches of
                    [L _ (GHC.Match _ [] grhss)] -> convertGRHSs [] grhss patternFailure
                    _ -> convUnsupported "malformed multi-match variable definitions"
-            else uncurry Fun <$> convertFunction fun_matches
+            else do
+              skipEqns <- view $ edits.skippedEquations.at name.non mempty
+              uncurry Fun <$> convertFunction skipEqns fun_matches
 
         addScope <- maybe id (flip InScope) <$> view (edits.additionalScopes.at (SPValue, name))
 
@@ -996,8 +1006,8 @@ convertMethodBinding name FunBind{..}   = withCurrentDefinition name $ do
                [L _ (GHC.Match _ [] grhss)] -> convertGRHSs [] grhss patternFailure
                _ -> convUnsupported "malformed multi-match variable definitions"
         else do
-          (argBinders, match) <- convertFunction fun_matches
-          pure $  Fun argBinders match
+          skipEqns <- view $ edits.skippedEquations.at name.non mempty
+          uncurry Fun <$> convertFunction skipEqns fun_matches
       pure $ ConvertedDefinitionBinding $ ConvertedDefinition name [] Nothing defn
 
 convertTypedBindings :: LocalConvMonad r m