Verites / verigraph

Software specification and verification system based on graph rewriting
https://verites.github.io/verigraph/
Apache License 2.0
37 stars 4 forks source link

Create and document code style #29

Open jsbezerra opened 7 years ago

jsbezerra commented 7 years ago

The following draft should be finished and published to Coding Style Guide

Verigraph Coding Style

This is a short document based on Johan Tibell's style guide describing the preferred coding style for this project. Some of these rules can be enforced by stylish-haskell, using the configuration file in the project root.

Formatting

Line Length

Maximum line length is 100 characters. "Going over is not the end of the world, but consider refactoring before you decide a line really must be longer."¹

Indentation

Tabs are illegal. Use spaces for indenting. Always indent to multiples of two.

Blank Lines

Whitespace

Export Lists

Data Declarations

Pragmas

Lists

Hanging Lambdas

Case Expressions

If-then-else Clauses

Imports

Comments

Punctuation

Top-Level Definitions

End-of-Line Comments

Links

Naming

Modules

Dealing with Laziness

Misc

Point-free style

Warnings

¹ As in the Elm style guide

ggazzi commented 7 years ago

Proposal for blank lines

Two blank lines between different sections of the source code. One blank line between top-level definitions. A blank line may be used between functions in a type class instance declaration if the function bodies are large. Use your judgement.

Avoid leaving blank lines within a single function. If you think they are necessary, consider splitting it into multiple top-level functions.

type Relabeling = (Map NodeId Node, Map EdgeId Edge, Map Variable Variable)

relableGraph :: SymbolicGraph -> [Int] -> [Int] -> Text -> Relabeling
relableGraph graph newNodeIds newEdgeIds varSuffix =
  let
    varMap = Map.fromList [ (v, v <> varSuffix) | v <- freeVariablesOf graph ]
    nodeMap = Map.fromList
        [ (oldId, N newId newAttribute)
            | (N oldId oldAttribute, newId) <- zip (nodes graph) (map toEnum newNodeIds)
            , let newAttribute = oldAttribute >>= (`Map.lookup` varMap)
        ]
    edgeMap = Map.fromList
        [ (e, E e' src' tgt')
            | (E e src tgt, e') <- zip (edges graph) (map toEnum newEdgeIds)
            , let src' = nodeId (nodeMap Map.! src)
            , let tgt' = nodeId (nodeMap Map.! tgt)
        ]
  in (nodeMap, edgeMap, varMap)

asIntMap :: Enum k => Map k v -> IntMap v
asIntMap = IntMap.fromList . map (first fromEnum) . Map.toList

instance Cocomplete SymbolicMorphism where

  initialObject _ =  SymbolicGraph.Internal.empty
  calculateCoequalizer f g = calculateGenericCoequalizer (domain f) (codomain f) (mkPair f g)

  calculateCoproduct a b =
    let
      (nodeMapA, edgeMapA, varMapA) = relableGraph a [0 ..] [0 ..] "_a"
      (nodeMapB, edgeMapB, varMapB) = relableGraph b [length (nodes a) ..] [length (edges a) ..] "_b"
      coproductGraph = fromNodesAndEdges
        (Map.elems nodeMapA ++ Map.elems nodeMapB)
        (Map.elems edgeMapA ++ Map.elems edgeMapB)
        (renameVariables varMapA (restrictions a) ++ renameVariables varMapB (restrictions b))
    in
      ( makeEmbeddingInto coproductGraph a (nodeMapA, edgeMapA, varMapA)
      , makeEmbeddingInto coproductGraph b (nodeMapB, edgeMapB, varMapB)
      )
ggazzi commented 7 years ago

Proposal for whitespace

Surround binary operators with a single space on either side. Use your better judgement for the insertion of spaces around arithmetic operators but always be consistent about whitespace on either side of a binary operator. Don't insert a space after a lambda.

Good:

Avoid:

Bad:

ggazzi commented 7 years ago

Suggestion for Export Lists

Format export lists as follows:

module Data.Set
    (
      -- * The @Set@ type
      Set
    , empty
    , singleton

      -- * Querying
    , member
    ) where
jsbezerra commented 7 years ago

"Three blank lines between different sections of the source code."

How about two, only? ^^'

ggazzi commented 7 years ago

Proposal for Data Declarations

If the data type definition is broken into multiple lines, align the constructors deriving clause. Example:

data Status = Pending | Ok | Error
  deriving (Eq, Ord)

data HttpException
    = InvalidStatusCode Int
    | MissingContentHeader
    deriving (Eq, Ord, Show)

Format record types as follows. Don't align the field types or the comments.

data Person = Person
    { firstName :: String -- ^ First name
    , lastName :: String -- ^ Last name
    , age :: Int -- ^ Age
    } deriving (Eq, Show)
ggazzi commented 7 years ago

Proposal for Pragmas

Put pragmas immediately following the function they apply to. Example:

id :: a -> a
id x = x
{-# INLINE id #-}

Language pragmas should be listed on multiple lines as follows and sorted alphabetically. This can be managed by stylish-haskell.

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeClasses #-}
module Foo.Bar where

In the case of data type definitions you must put the pragma before the type it applies to. Example:

data Array e = Array
    {-# UNPACK #-} Int
    ByteArray
ggazzi commented 7 years ago

Proposal for Lists and List Comprehensions

If a list is broken into multiple lines, the first line break comes before the list, and its elements are aligned as follows. This ensures that all items of the list start on the same column of text, without requiring context-sensitive alignment.

shortList = [ 1, 2, 3 ]

longList =
  [ "this is a very long string"
  , "this is an even longer string that woudn't fit into the same line" ]

Similar rules apply to list comprehensions. When broken into multiple lines, the first line break comes before the comprehension. The generators should be indented 4 spaces further than the opening [. Again, this ensures all generators start on the same column of text, without requiring context-sensitive alignment.

nodeMap = Map.fromList
  [ (oldId, N newId newAttribute)
      | (N oldId oldAttribute, newId) <- zip (nodes graph) (map toEnum newNodeIds)
      , let newAttribute = oldAttribute >>= (`Map.lookup` varMap) ]
ggazzi commented 7 years ago

Proposal for Hanging Lambdas

You may or may not indent the code following a "hanging" lambda. Use your judgement. Some examples:

bar :: IO ()
bar = forM_ [1, 2, 3] $ \n -> do
  putStrLn "Here comes a number!"
  print n

foo :: IO ()
foo =
  alloca 10 $ \a ->
  alloca 20 $ \b ->
  cFunction a b
ggazzi commented 7 years ago

Proposal for If-then-else clauses

Generally, guards and pattern matches should be preferred over if-then-else clauses, where possible. Short cases should usually be put on a single line (when line length allows it).

Short cases should usually be put on a single line (when line length allows it). Otherwise, the clauses should be written similarly to how they work in more mainstream languages (e.g. python):

foo =
  if someCondition then
    someCode
  else
    someAlternativeCode

The same holds for monadic code (i.e. in do-notation):

foo = do
  someCode
  if condition then
    someMoreCode
  else
    someAlternativeCode

The same rule applies to nested do blocks:

foo = do
  instruction <- decodeInstruction
  skip <- load Memory.skip
  if skip == 0x0000 then do
    execute instruction
    addCycles $ instructionCycles instruction
  else do
    store Memory.skip 0x0000
    addCycles 1
ggazzi commented 7 years ago

Proposal for case expressions

The cases should be indented 2 spaces further that the line where case ... of appears. Don't align the arrows

foobar = case something of
  Just j -> foo
  Nothing -> bar
ggazzi commented 7 years ago

Proposal for Imports

Imports should be grouped in the following order:

  1. external library imports (from standard or third party libraries)
  2. imports from the same project

Put a blank line between each group of imports. The imports in each group should be sorted alphabetically, by module name, and aligned properly. Use stylish-haskell to ensure sorting and alignment.

Always use explicit import lists or qualified imports for standard and third party libraries. This makes the code more robust against changes in these libraries. Exception: The Prelude.