diff --git a/doc/source/edits.rst b/doc/source/edits.rst index d00b7bbac..4cd536969 100644 --- a/doc/source/edits.rst +++ b/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 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/emacs/edits.el b/emacs/edits.el index c43f38ed5..a37687404 100644 --- a/emacs/edits.el +++ b/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-*\\" . font-lock-keyword-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-type-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face) ("\\" . font-lock-builtin-face)) '("[./]edits\\'") nil diff --git a/examples/tests/Makefile b/examples/tests/Makefile index e304b7d8b..5fd1128ee 100644 --- a/examples/tests/Makefile +++ b/examples/tests/Makefile @@ -34,7 +34,8 @@ PASS = \ RedefineAddAxiom \ AddTheorem \ Existential \ - SkipConstructor + SkipConstructor \ + SkipMatches # tests that *should* pass but currently fail TODO_PASS = \ diff --git a/examples/tests/SkipConstructor.hs b/examples/tests/SkipConstructor.hs index dde2e9a8f..c2b31d1ed 100644 --- a/examples/tests/SkipConstructor.hs +++ b/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 diff --git a/examples/tests/SkipConstructor/edits b/examples/tests/SkipConstructor/edits index 451daf332..c8e2710ad 100644 --- a/examples/tests/SkipConstructor/edits +++ b/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 diff --git a/examples/tests/SkipMatches.hs b/examples/tests/SkipMatches.hs new file mode 100644 index 000000000..98813658c --- /dev/null +++ b/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) diff --git a/examples/tests/SkipMatches/edits b/examples/tests/SkipMatches/edits new file mode 100644 index 000000000..003358392 --- /dev/null +++ b/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 _ diff --git a/src/lib/HsToCoq/ConvertHaskell/Expr.hs b/src/lib/HsToCoq/ConvertHaskell/Expr.hs index b83e219f5..47ffaf873 100644 --- a/src/lib/HsToCoq/ConvertHaskell/Expr.hs +++ b/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 diff --git a/src/lib/HsToCoq/ConvertHaskell/Parameters/Edits.hs b/src/lib/HsToCoq/ConvertHaskell/Parameters/Edits.hs index 60969382a..8713840cd 100644 --- a/src/lib/HsToCoq/ConvertHaskell/Parameters/Edits.hs +++ b/src/lib/HsToCoq/ConvertHaskell/Parameters/Edits.hs @@ -1,13 +1,14 @@ -{-# LANGUAGE LambdaCase, TemplateHaskell, RecordWildCards, OverloadedStrings, FlexibleContexts, MultiParamTypeClasses, RankNTypes, DeriveGeneric #-} +{-# LANGUAGE LambdaCase, TemplateHaskell, RecordWildCards, OverloadedStrings, FlexibleContexts, MultiParamTypeClasses, RankNTypes, DeriveGeneric, GeneralizedNewtypeDeriving #-} module HsToCoq.ConvertHaskell.Parameters.Edits ( - Edits(..), typeSynonymTypes, dataTypeArguments, termination, redefinitions, additions, skipped, skippedConstructors, skippedClasses, skippedMethods, skippedModules, importedModules, hasManualNotation, axiomatizedModules, axiomatizedDefinitions, unaxiomatizedDefinitions, additionalScopes, orders, renamings, coinductiveTypes, classKinds, dataKinds, deleteUnusedTypeVariables, rewrites, obligations, renamedModules, simpleClasses, inlinedMutuals, replacedTypes, collapsedLets, inEdits, + Edits(..), typeSynonymTypes, dataTypeArguments, termination, redefinitions, additions, skipped, skippedConstructors, skippedClasses, skippedMethods, skippedEquations, skippedCasePatterns, skippedModules, importedModules, hasManualNotation, axiomatizedModules, axiomatizedDefinitions, unaxiomatizedDefinitions, additionalScopes, orders, renamings, coinductiveTypes, classKinds, dataKinds, deleteUnusedTypeVariables, rewrites, obligations, renamedModules, simpleClasses, inlinedMutuals, replacedTypes, collapsedLets, inEdits, HsNamespace(..), NamespacedIdent(..), Renamings, DataTypeArguments(..), dtParameters, dtIndices, CoqDefinition(..), definitionSentence, anAssertionVariety, ScopePlace(..), TerminationArgument(..), + NormalizedPattern(), getNormalizedPattern, normalizePattern, Rewrite(..), Rewrites, Edit(..), addEdit, buildEdits, useProgram, @@ -38,8 +39,10 @@ import HsToCoq.Coq.FreeVars () import HsToCoq.Coq.Gallina import HsToCoq.Coq.Gallina.Util +import HsToCoq.Coq.Subst (Subst()) import HsToCoq.Coq.Gallina.Rewrite (Rewrite(..), Rewrites) import HsToCoq.ConvertHaskell.Axiomatize +import HsToCoq.Coq.Pretty -------------------------------------------------------------------------------- @@ -85,6 +88,31 @@ data ScopePlace = SPValue | SPConstructor data TerminationArgument = WellFounded Order | Deferred | Corecursive deriving (Eq, Ord, Show, Read) +-- Used to match patterns that might disagree on the question of whether a name +-- is an @ArgsPat qid []@ or a @QualidPat@; this is useful when reading from an edits file. +newtype NormalizedPattern = NormalizedPattern Pattern + deriving (Eq, Ord, Show, Read, Subst, HasBV Qualid, Gallina) + +getNormalizedPattern :: NormalizedPattern -> Pattern +getNormalizedPattern (NormalizedPattern pat) = pat +{-# INLINE getNormalizedPattern #-} + +normalizePattern :: Pattern -> NormalizedPattern +normalizePattern = NormalizedPattern . go where + go (ArgsPat qid []) = QualidPat qid + go (ArgsPat qid args) = ArgsPat qid (go <$> args) + go (ExplicitArgsPat qid args) = ExplicitArgsPat qid (go <$> args) + go (InfixPat lhs op rhs) = InfixPat (go lhs) op (go rhs) + go (AsPat p qid) = AsPat (go p) qid + go (InScopePat p scope) = InScopePat (go p) scope + go (QualidPat qid) = QualidPat qid + go UnderscorePat = UnderscorePat + go (NumPat n) = NumPat n + go (StringPat s) = StringPat s + go (OrPats ps) = OrPats (goO <$> ps) + + goO (OrPattern ps) = OrPattern (go <$> ps) + data Edit = TypeSynonymTypeEdit Ident Ident | DataTypeArgumentsEdit Qualid DataTypeArguments | TerminationEdit Qualid TerminationArgument @@ -95,6 +123,8 @@ data Edit = TypeSynonymTypeEdit Ident Ident | SkipConstructorEdit Qualid | SkipClassEdit Qualid | SkipMethodEdit Qualid Ident + | SkipEquationEdit Qualid (NonEmpty Pattern) + | SkipCasePatternEdit Pattern | SkipModuleEdit ModuleName | ImportModuleEdit ModuleName | AxiomatizeModuleEdit ModuleName @@ -140,6 +170,8 @@ data Edits = Edits { _typeSynonymTypes :: !(Map Ident Ident) , _skippedConstructors :: !(Set Qualid) , _skippedClasses :: !(Set Qualid) , _skippedMethods :: !(Set (Qualid,Ident)) + , _skippedEquations :: !(Map Qualid (Set (NonEmpty NormalizedPattern))) + , _skippedCasePatterns :: !(Set NormalizedPattern) , _skippedModules :: !(Set ModuleName) , _importedModules :: !(Set ModuleName) , _axiomatizedModules :: !(Set ModuleName) @@ -186,12 +218,18 @@ duplicate_for' what disp x = "Duplicate " ++ what ++ " for " ++ disp x duplicate_for :: String -> String -> String duplicate_for what = duplicate_for' what id +-- Module-local duplicateI_for :: String -> Ident -> String duplicateI_for what = duplicate_for' what T.unpack +-- Module-local duplicateQ_for :: String -> Qualid -> String duplicateQ_for what = duplicate_for' what (T.unpack . qualidToIdent) +-- Module-local +duplicateP_for :: Gallina g => String -> g -> String +duplicateP_for what = duplicate_for' what showP + descDuplEdit :: Edit -> String descDuplEdit = \case TypeSynonymTypeEdit syn _ -> duplicateI_for "type synonym result types" syn @@ -202,6 +240,8 @@ descDuplEdit = \case SkipConstructorEdit con -> duplicateQ_for "skipped constructor requests" con SkipClassEdit cls -> duplicateQ_for "skipped class requests" cls SkipMethodEdit cls meth -> duplicate_for "skipped method requests" (prettyLocalName cls meth) + SkipEquationEdit fun pats -> duplicateP_for "skipped equation requests" (ArgsPat fun $ toList pats) + SkipCasePatternEdit pat -> duplicateP_for "skipped case pattern requests" pat SkipModuleEdit mod -> duplicate_for "skipped module requests" (moduleNameString mod) ImportModuleEdit mod -> duplicate_for "imported module requests" (moduleNameString mod) HasManualNotationEdit what -> duplicate_for "has manual notation" (moduleNameString what) @@ -234,32 +274,34 @@ descDuplEdit = \case addEdit :: MonadError String m => Edit -> Edits -> m Edits addEdit e = case e of - TypeSynonymTypeEdit syn res -> addFresh e typeSynonymTypes syn res - DataTypeArgumentsEdit ty args -> addFresh e dataTypeArguments ty args - TerminationEdit what ta -> addFresh e termination what ta - RedefinitionEdit def -> addFresh e redefinitions (defName def) def - SkipEdit what -> addFresh e skipped what () - SkipConstructorEdit con -> addFresh e skippedConstructors con () - SkipClassEdit cls -> addFresh e skippedClasses cls () - SkipMethodEdit cls meth -> addFresh e skippedMethods (cls,meth) () - SkipModuleEdit mod -> addFresh e skippedModules mod () - ImportModuleEdit mod -> addFresh e importedModules mod () - HasManualNotationEdit what -> addFresh e hasManualNotation what () - AxiomatizeModuleEdit mod -> addFresh e axiomatizedModules mod () - AxiomatizeDefinitionEdit what -> addFresh e axiomatizedDefinitions what () - UnaxiomatizeDefinitionEdit what -> addFresh e unaxiomatizedDefinitions what () - AdditionalScopeEdit place name scope -> addFresh e additionalScopes (place,name) scope - RenameEdit hs to -> addFresh e renamings hs to - ObligationsEdit what tac -> addFresh e obligations what tac - ClassKindEdit cls kinds -> addFresh e classKinds cls kinds - DataKindEdit cls kinds -> addFresh e dataKinds cls kinds - DeleteUnusedTypeVariablesEdit qid -> addFresh e deleteUnusedTypeVariables qid () - CoinductiveEdit ty -> addFresh e coinductiveTypes ty () - RenameModuleEdit m1 m2 -> addFresh e renamedModules m1 m2 - SimpleClassEdit cls -> addFresh e simpleClasses cls () - InlineMutualEdit fun -> addFresh e inlinedMutuals fun () - SetTypeEdit qid oty -> addFresh e replacedTypes qid oty - CollapseLetEdit qid -> addFresh e collapsedLets qid () + TypeSynonymTypeEdit syn res -> addFresh e typeSynonymTypes syn res + DataTypeArgumentsEdit ty args -> addFresh e dataTypeArguments ty args + TerminationEdit what ta -> addFresh e termination what ta + RedefinitionEdit def -> addFresh e redefinitions (defName def) def + SkipEdit what -> addFresh e skipped what () + SkipConstructorEdit con -> addFresh e skippedConstructors con () + SkipClassEdit cls -> addFresh e skippedClasses cls () + SkipMethodEdit cls meth -> addFresh e skippedMethods (cls,meth) () + SkipEquationEdit fun pats -> addFresh e (skippedEquations.at fun.non mempty) (normalizePattern <$> pats) () + SkipCasePatternEdit pat -> addFresh e skippedCasePatterns (normalizePattern pat) () + SkipModuleEdit mod -> addFresh e skippedModules mod () + ImportModuleEdit mod -> addFresh e importedModules mod () + HasManualNotationEdit what -> addFresh e hasManualNotation what () + AxiomatizeModuleEdit mod -> addFresh e axiomatizedModules mod () + AxiomatizeDefinitionEdit what -> addFresh e axiomatizedDefinitions what () + UnaxiomatizeDefinitionEdit what -> addFresh e unaxiomatizedDefinitions what () + AdditionalScopeEdit place name scope -> addFresh e additionalScopes (place,name) scope + RenameEdit hs to -> addFresh e renamings hs to + ObligationsEdit what tac -> addFresh e obligations what tac + ClassKindEdit cls kinds -> addFresh e classKinds cls kinds + DataKindEdit cls kinds -> addFresh e dataKinds cls kinds + DeleteUnusedTypeVariablesEdit qid -> addFresh e deleteUnusedTypeVariables qid () + CoinductiveEdit ty -> addFresh e coinductiveTypes ty () + RenameModuleEdit m1 m2 -> addFresh e renamedModules m1 m2 + SimpleClassEdit cls -> addFresh e simpleClasses cls () + InlineMutualEdit fun -> addFresh e inlinedMutuals fun () + SetTypeEdit qid oty -> addFresh e replacedTypes qid oty + CollapseLetEdit qid -> addFresh e collapsedLets qid () AddEdit mod def -> return . (additions.at mod.non mempty %~ (definitionSentence def:)) OrderEdit idents -> return . appEndo (foldMap (Endo . addEdge orders . swap) (adjacents idents)) RewriteEdit rewrite -> return . (rewrites %~ (rewrite:)) diff --git a/src/lib/HsToCoq/ConvertHaskell/Parameters/Parsers.y b/src/lib/HsToCoq/ConvertHaskell/Parameters/Parsers.y index d6e88667d..a432c638a 100644 --- a/src/lib/HsToCoq/ConvertHaskell/Parameters/Parsers.y +++ b/src/lib/HsToCoq/ConvertHaskell/Parameters/Parsers.y @@ -88,6 +88,9 @@ import HsToCoq.ConvertHaskell.Parameters.Parsers.Lexing set { TokWord "set" } no { TokWord "no" } collapse { TokWord "collapse" } + equation { TokWord "equation" } + case { TokWord "case" } + pattern { TokWord "pattern" } '=' { TokOp "=" } ':->' { TokOp ":->" } -- Tokens: Coq terms @@ -285,6 +288,8 @@ Edit :: { Edit } | skip constructor Qualid { SkipConstructorEdit $3 } | skip class Qualid { SkipClassEdit $3 } | skip method Qualid Word { SkipMethodEdit $3 $4 } + | skip equation Qualid Some(AtomicPattern) { SkipEquationEdit $3 $4 } + | skip case pattern Pattern { SkipCasePatternEdit $4 } | skip module Word { SkipModuleEdit (mkModuleNameT $3) } | import module Word { ImportModuleEdit (mkModuleNameT $3) } | manual notation Word { HasManualNotationEdit (mkModuleNameT $3) } @@ -459,15 +464,16 @@ MultPattern :: { MultPattern } -- arguments as variables. We could hard-code common nullary constructors. -- But can we do better? Pattern :: { Pattern } - : Qualid Some(AtomicPattern) { ArgsPat $1 (NEL.toList $2) } - | Pattern as Qualid { AsPat $1 $3 } - | AtomicPattern { $1 } + : Qualid Some(AtomicPattern) { ArgsPat $1 (NEL.toList $2) } + | '@' Qualid Some(AtomicPattern) { ExplicitArgsPat $2 $3 } + | Pattern as Qualid { AsPat $1 $3 } + | AtomicPattern { $1 } AtomicPattern :: { Pattern } - : '_' { UnderscorePat } - | Num { NumPat $1 } - | Qualid { QualidPat $1 } - | '(' Pattern ')' { $2 } + : '_' { UnderscorePat } + | Num { NumPat $1 } + | Qualid { QualidPat $1 } + | '(' Pattern ')' { $2 } Rewrite :: { Rewrite } : forall Many(Word) ',' EqlessTerm '=' Term { Rewrite $2 $4 $6 } diff --git a/src/lib/HsToCoq/ConvertHaskell/Pattern.hs b/src/lib/HsToCoq/ConvertHaskell/Pattern.hs index 5a9347ead..18ac01423 100644 --- a/src/lib/HsToCoq/ConvertHaskell/Pattern.hs +++ b/src/lib/HsToCoq/ConvertHaskell/Pattern.hs @@ -256,7 +256,6 @@ mutExcl (ConApp con1 args1) (ConApp con2 args2) = con1 /= con2 || mutExcls args1 args2 mutExcl _ _ = False - -- A simple completeness checker. Traverses the list of patterns, and keep -- tracks of all pattern summaries that we still need to match -- Internally, we use OtherSummary as “everything yet has to match”