delete unused constructor ExcessBound

examples/factor.gcl

@@ -9,8 +9,8 @@ var a : Bool
 p := p + 1
 p := 3
 a := True
-[! a
-
+[!
+a := mod
 !]
 
 

examples/gcl_server.log

@@ -20,16 +20,3 @@ lookup file state map
 load: update notification sent
 load: end
 STextDocumentDidOpen end
-semantic token: start
-ask file state ref
-ask file state map
-lookup file state map
-  found
-hover: start
-ask file state ref
-ask file state map
-lookup file state map
-  found
-hover: success
-hover: response sent
-hover: end

src/GCL/WP/Types.hs

@@ -60,12 +60,10 @@ type TspSStmts = (Pred, Maybe Expr) -> [Stmt] -> WP Pred
 
 data StructWarning
   = MissingBound Range
-  | ExcessBound Range
   deriving (Eq, Show, Generic)
 
 instance Located StructWarning where
   locOf (MissingBound rng) = locOf rng
-  locOf (ExcessBound rng) = locOf rng
 
 data StructError
   = MissingAssertion Loc

src/Pretty/Error.hs

@@ -35,7 +35,6 @@ instance Pretty ParseError where
 
 instance Pretty StructWarning where
   pretty (MissingBound loc) = "Missing Bound" <+> pretty loc
-  pretty (ExcessBound  loc) = "Excess Bound" <+> pretty loc
 
 instance Pretty StructError where
   pretty (MissingAssertion     loc) = "Missing Assertion" <+> pretty loc

src/Render/Predicate.hs

@@ -17,15 +17,11 @@ import           Render.Syntax.Typed
 instance Render StructWarning where
   render (MissingBound _)
     = "Bound missing at the end of the assertion before the DO construct \" , bnd : ... }\""
-  render (ExcessBound _) =
-    "The bound annotation at this assertion is unnecessary"
 
 instance RenderSection StructWarning where
   renderSection x = case x of
     MissingBound range ->
       Section Yellow [Header "Bound Missing" (Just range), Paragraph (render x)]
-    ExcessBound range ->
-      Section Yellow [Header "Excess Bound" (Just range), Paragraph (render x)]
 
 instance RenderSection Spec where
   renderSection (Specification _ pre post range _) = Section

src/Server/Notification/Update.hs

@@ -51,10 +51,6 @@ instance JSON.ToJSON StructWarning where
     object [ "tag" .= JSON.String "MissingBound"
            , "range" .= JSON.toJSON (toLSPRange range)
            ]
-  toJSON (ExcessBound range) =
-    object [ "tag" .= JSON.String "ExcessBound"
-           , "range" .= JSON.toJSON (toLSPRange range)
-           ]
 
 instance JSON.ToJSON PO where
   toJSON :: PO -> JSON.Value