Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Wingman: Config option to suppress proofstate styling #1966

Merged
merged 2 commits into from
Jun 25, 2021
Merged

Wingman: Config option to suppress proofstate styling #1966

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6c93d03
Config option to suppress proofstate styling
isovector Jun 22, 2021
75d7cac
Merge branch 'master' into suppress-proofstate-html
isovector Jun 25, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 4 additions & 0 deletions plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,8 +136,11 @@ properties :: Properties
, 'PropertyKey "max_use_ctor_actions" 'TInteger
, 'PropertyKey "timeout_duration" 'TInteger
, 'PropertyKey "auto_gas" 'TInteger
, 'PropertyKey "proofstate_styling" 'TBoolean
]
properties = emptyProperties
& defineBooleanProperty #proofstate_styling
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@berberman it's a little annoying that these properties need to be added in the opposite order as in the type. Is there a better pattern here?

Copy link
Collaborator

@berberman berberman Jun 23, 2021 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm I think the order only affects the type signature of properties, no?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but in the opposite order in which they're defined. Notice that I'm adding to the top of emptyProperties here, but the resulting type is added to the end of the type :(

"Should Wingman emit styling markup when showing metaprogram proof states?" True
& defineIntegerProperty #auto_gas
"The depth of the search tree when performing \"Attempt to fill hole\". Bigger values will be able to derive more solutions, but will take exponentially more time." 4
& defineIntegerProperty #timeout_duration
Expand All @@ -162,6 +165,7 @@ getTacticConfig pId =
<$> usePropertyLsp #max_use_ctor_actions pId properties
<*> usePropertyLsp #timeout_duration pId properties
<*> usePropertyLsp #auto_gas pId properties
<*> usePropertyLsp #proofstate_styling pId properties


getIdeDynflags
Expand Down
7 changes: 4 additions & 3 deletions plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,13 @@ module Wingman.Metaprogramming.Parser where

import qualified Control.Monad.Combinators.Expr as P
import qualified Control.Monad.Error.Class as E
import Control.Monad.Reader (ask)
import Data.Functor
import Data.Maybe (listToMaybe)
import qualified Data.Text as T
import qualified Refinery.Tactic as R
import qualified Text.Megaparsec as P
import Wingman.Auto
import Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext, getCurrentDefinitions)
import Wingman.Machinery (useNameFromHypothesis, useNameFromContext, getCurrentDefinitions)
import Wingman.Metaprogramming.Lexer
import Wingman.Metaprogramming.Parser.Documentation
import Wingman.Metaprogramming.ProofState (proofState, layout)
Expand Down Expand Up @@ -454,7 +453,9 @@ attempt_it rsl ctx jdg program =
tt
pure $ case res of
Left tes -> Left $ wrapError $ show tes
Right rtr -> Right $ layout $ proofState rtr
Right rtr -> Right
$ layout (cfg_proofstate_styling $ ctxConfig ctx)
$ proofState rtr


parseMetaprogram :: T.Text -> TacticsM ()
Expand Down
28 changes: 15 additions & 13 deletions plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/ProofState.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,24 +43,26 @@ data Ann
forceMarkdownNewlines :: String -> String
forceMarkdownNewlines = unlines . fmap (<> " ") . lines

layout :: Doc Ann -> String
layout
layout :: Bool -> Doc Ann -> String
layout use_styling
= forceMarkdownNewlines
. T.unpack
. renderSimplyDecorated id
renderAnn
renderUnann
(renderAnn use_styling)
(renderUnann use_styling)
. layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)

renderAnn :: Ann -> T.Text
renderAnn Goal = "<span style='color:#ef4026;'>"
renderAnn Hypoth = "```haskell\n"
renderAnn Status = "<span style='color:#6495ED;'>"

renderUnann :: Ann -> T.Text
renderUnann Goal = "</span>"
renderUnann Hypoth = "\n```\n"
renderUnann Status = "</span>"
renderAnn :: Bool -> Ann -> T.Text
renderAnn False _ = ""
renderAnn _ Goal = "<span style='color:#ef4026;'>"
renderAnn _ Hypoth = "```haskell\n"
renderAnn _ Status = "<span style='color:#6495ED;'>"

renderUnann :: Bool -> Ann -> T.Text
renderUnann False _ = ""
renderUnann _ Goal = "</span>"
renderUnann _ Hypoth = "\n```\n"
renderUnann _ Status = "</span>"

proofState :: RunTacticResults -> Doc Ann
proofState RunTacticResults{rtr_subgoals} =
Expand Down
2 changes: 2 additions & 0 deletions plugins/hls-tactics-plugin/src/Wingman/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ data Config = Config
{ cfg_max_use_ctor_actions :: Int
, cfg_timeout_seconds :: Int
, cfg_auto_gas :: Int
, cfg_proofstate_styling :: Bool
}
deriving (Eq, Ord, Show)

Expand All @@ -95,6 +96,7 @@ emptyConfig = Config
{ cfg_max_use_ctor_actions = 5
, cfg_timeout_seconds = 2
, cfg_auto_gas = 4
, cfg_proofstate_styling = True
}

------------------------------------------------------------------------------
Expand Down