Remove Semantics of K references in Syntax modules (#2783)

* update And syntax documentation

* update syntax docs to refer to kore-syntax.md#patterns

* fix links, updating docs

* add links to kore-syntax.md, update docs

* refer to kore-syntax

* reference kore-syntax.md

* escape backslash

* update comments on unified constructs

* Update docs/glossary.md

Co-authored-by: Raoul <1412344+RaoulSchaffranek@users.noreply.github.com>

* fix link to kore-syntax.md#patterns

* use haddock hyperlinks when possible

Co-authored-by: Raoul <1412344+RaoulSchaffranek@users.noreply.github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: 3 people

docs/glossary.md

@@ -40,7 +40,7 @@
 
 1. (noun)
    A syntactic element constructed according to the rules described in the
-   semantics-of-k document.
+   [kore-syntax document](http://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns).
 2. (noun)
    The internal representation of such a syntactic element. It may have
    constructs which cannot be represented directly into syntactic elements

kore/src/Kore/AST/Common.hs

@@ -7,11 +7,11 @@ the syntactic categories of a Kore definition that do not need unified
 constructs.
 
 Unified constructs are those that represent both meta and object versions of
-an AST term in a single data type (e.g. 'UnifiedSort' that can be either
-'Sort' or 'Sort')
+an AST term in a single data type (e.g. 'SymbolOrAlias' that can be either
+'Symbol' or 'Alias')
 
-Please refer to Section 9 (The Kore Language) of the
-<http://github.com/kframework/kore/blob/master/docs/semantics-of-k.pdf Semantics of K>.
+Please refer to
+<http://github.com/kframework/kore/blob/master/docs/kore-syntax.md kore-syntax.md>.
 -}
 module Kore.AST.Common (
     MLPatternType (..),
@@ -28,7 +28,7 @@ import GHC.Generics (
 import Kore.Unparser
 import Prelude.Kore
 
--- |Enumeration of patterns starting with @\@
+-- |Enumeration of patterns starting with @\\@
 data MLPatternType
     = AndPatternType
     | BottomPatternType

kore/src/Kore/Sort.hs

@@ -1,8 +1,8 @@
 {- |
 Copyright   : (c) Runtime Verification, 2018-2021
 
-Please refer to Section 9 (The Kore Language) of the
-<http://github.com/kframework/kore/blob/master/docs/semantics-of-k.pdf Semantics of K>.
+Please refer to
+<http://github.com/kframework/kore/blob/master/docs/kore-syntax.md kore-syntax.md>.
 -}
 module Kore.Sort (
     SortVariable (..),
@@ -56,10 +56,9 @@ import Kore.Unparser
 import Prelude.Kore
 import qualified Pretty
 
-{- | @SortVariable@ is a Kore sort variable.
+{- | 'SortVariable' is a Kore sort variable.
 
-@SortVariable@ corresponds to the @sort-variable@ syntactic category from the
-Semantics of K, Section 9.1.2 (Sorts).
+'SortVariable' corresponds to the @sort-variable@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#sorts kore-syntax.md#sorts>.
 -}
 newtype SortVariable = SortVariable
     {getSortVariable :: Id}
@@ -73,9 +72,8 @@ instance Unparse SortVariable where
     unparse = unparse . getSortVariable
     unparse2 SortVariable{getSortVariable} = unparse2 getSortVariable
 
-{- |'SortActual' corresponds to the @sort-constructor{sort-list}@ branch of the
-@object-sort@ and @meta-sort@ syntactic categories from the Semantics of K,
-Section 9.1.2 (Sorts).
+{- |'SortActual' corresponds to the @sort-identifier{sorts}@ branch of the
+@sort@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#sorts kore-syntax.md#sorts>.
 -}
 data SortActual = SortActual
     { sortActualName :: !Id
@@ -100,9 +98,8 @@ instance Unparse SortActual where
                     <> parameters2 sortActualSorts
                     <> ")"
 
-{- |'Sort' corresponds to the @object-sort@ and
-@meta-sort@ syntactic categories from the Semantics of K,
-Section 9.1.2 (Sorts).
+{- |'Sort' corresponds to the @sort@ syntactic category from
+<https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#sorts kore-syntax.md#sorts>.
 -}
 data Sort
     = SortVariableSort !SortVariable
@@ -173,10 +170,7 @@ substituteSortVariables substitution sort =
                         substituteSortVariables substitution <$> sortActualSorts
                     }
 
-{- |'MetaSortType' corresponds to the @meta-sort-constructor@ syntactic category
-from the Semantics of K, Section 9.1.2 (Sorts).
-
-Ths is not represented directly in the AST, we're using the string
+{- | Ths is not represented directly in the AST, we're using the string
 representation instead.
 -}
 data MetaSortType

kore/src/Kore/Syntax/And.hs

@@ -16,9 +16,7 @@ import Kore.Unparser
 import Prelude.Kore
 import qualified Pretty
 
-{- |'And' corresponds to the @\and@ branches of the @object-pattern@ and
-@meta-pattern@ syntactic categories from the Semantics of K,
-Section 9.1.4 (Patterns).
+{- |'And' corresponds to the @\\and@ branch of the @matching-logic-pattern@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns kore-syntax.md#patterns>.
 
 'andSort' is both the sort of the operands and the sort of the result.
 

kore/src/Kore/Syntax/Application.hs

@@ -7,11 +7,11 @@ the syntactic categories of a Kore definition that do not need unified
 constructs.
 
 Unified constructs are those that represent both meta and object versions of
-an AST term in a single data type (e.g. 'UnifiedSort' that can be either
-'Sort' or 'Sort')
+an AST term in a single data type (e.g. 'SymbolOrAlias' that can be either
+'Kore.Syntax.Sentence.Symbol' or 'Kore.Syntax.Sentence.Alias')
 
-Please refer to Section 9 (The Kore Language) of the
-<http://github.com/kframework/kore/blob/master/docs/semantics-of-k.pdf Semantics of K>.
+Please refer to
+<http://github.com/kframework/kore/blob/master/docs/kore-syntax.md kore-syntax.md>.
 -}
 module Kore.Syntax.Application (
     SymbolOrAlias (..),
@@ -28,9 +28,8 @@ import Kore.Unparser
 import Prelude.Kore
 import qualified Pretty
 
-{- |'SymbolOrAlias' corresponds to the @head{sort-list}@ branch of the
-@head@ syntactic category from the Semantics of K,
-Section 9.1.3 (Heads).
+{- |'SymbolOrAlias' corresponds to the @symbol-or-alias@ syntactic category from
+<https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#sentences kore-syntax.md#sentences>
 -}
 data SymbolOrAlias = SymbolOrAlias
     { symbolOrAliasConstructor :: !Id
@@ -55,8 +54,9 @@ instance Unparse SymbolOrAlias where
 instance From SymbolOrAlias SymbolOrAlias where
     from = id
 
-{- |'Application' corresponds to the @head(pattern-list)@ branches of the
-@pattern@ syntactic category from the Semantics of K, Section 9.1.4 (Patterns).
+{- |'Application' corresponds to the @application-pattern@ branch of the
+@pattern@ syntactic category from
+<https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns kore-syntax.md#patterns>.
 
 This represents the @σ(φ1, ..., φn)@ symbol patterns in Matching Logic.
 -}

kore/src/Kore/Syntax/Bottom.hs

@@ -15,8 +15,7 @@ import Kore.Sort
 import Kore.Unparser
 import Prelude.Kore
 
-{- | 'Bottom' corresponds to the @\bottom@ branches of the @pattern@ syntactic
-category from the Semantics of K, Section 9.1.4 (Patterns).
+{- | 'Bottom' corresponds to the @\\bottom@ branch of the @matching-logic-pattern@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns kore-syntax.md#patterns>.
 
 'bottomSort' is the sort of the result.
 -}

kore/src/Kore/Syntax/Ceil.hs

@@ -16,9 +16,7 @@ import Kore.Unparser
 import Prelude.Kore
 import qualified Pretty
 
-{- |'Ceil' corresponds to the @\ceil@ branches of the @object-pattern@ and
-@meta-pattern@ syntactic categories from the Semantics of K,
-Section 9.1.4 (Patterns).
+{- |'Ceil' corresponds to the @\\ceil@ branch of the @matching-logic-pattern@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns kore-syntax.md#patterns>.
 
 'ceilOperandSort' is the sort of the operand.
 

kore/src/Kore/Syntax/Definition.hs

@@ -29,8 +29,8 @@ import qualified Pretty
 {- | Currently, a 'Definition' consists of some 'Attributes' and a 'Module'
 
 Because there are plans to extend this to a list of 'Module's, the @definition@
-syntactic category from the Semantics of K, Section 9.1.6
-(Declaration and Definitions) is splitted here into 'Definition' and 'Module'.
+syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#definition-modules kore-syntax.md#definition-modules>
+(Declaration and Definitions) is split here into 'Definition' and 'Module'.
 
 'definitionAttributes' corresponds to the first non-terminal of @definition@,
 while the remaining three are grouped into 'definitionModules'.

kore/src/Kore/Syntax/DomainValue.hs

@@ -17,15 +17,13 @@ import Kore.Unparser
 import Prelude.Kore
 import qualified Pretty
 
-{- |'DomainValue' corresponds to the @\dv@ branch of the @object-pattern@
-syntactic category, which are not yet in the Semantics of K document,
-but they should appear in Section 9.1.4 (Patterns) at some point.
+{- |'DomainValue' corresponds to the @\\dv@ branch of the @matching-logic-pattern@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns kore-syntax.md#patterns>.
 
 'domainValueSort' is the sort of the result.
 
 This represents the encoding of an object constant, e.g. we may use
-\dv{Int{}}{"123"} instead of a representation based on constructors,
-e.g. succesor(succesor(...succesor(0)...))
+@\\dv{Int{}}{"123"}@ instead of a representation based on constructors,
+e.g. @succesor(succesor(...succesor(0)...))@
 -}
 data DomainValue sort child = DomainValue
     { domainValueSort :: !sort

kore/src/Kore/Syntax/Equals.hs

@@ -19,9 +19,7 @@ import Pretty (
  )
 import qualified Pretty
 
-{- |'Equals' corresponds to the @\equals@ branches of the @object-pattern@ and
-@meta-pattern@ syntactic categories from the Semantics of K,
-Section 9.1.4 (Patterns).
+{- |'Equals' corresponds to the @\\equals@ branch of the @matching-logic-pattern@ syntactic category from <https://github.com/kframework/kore/blob/master/docs/kore-syntax.md#patterns kore-syntax.md#patterns>.
 
 'equalsOperandSort' is the sort of the operand.