HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

Ad-hoc conversion to markdown.

This commit is contained in:
Achim D. Brucker 2016-10-13 05:07:32 +01:00
parent 3667e0f898
commit 173c721611
1 changed files with 88 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

185
CodingStyle → CodingStyle.md
View File

@ -1,6 +1,4 @@
# su4sml coding style
su4sml coding style
===================
We here document coding-style guidelines that should be adhered to. We here document coding-style guidelines that should be adhered to.
Much of the existing code is not yet following these guidelines, Much of the existing code is not yet following these guidelines,
@ -8,8 +6,7 @@ patches are welcome. This style-guide was inspired by the SML Style Guide
from Cornell university [1]. from Cornell university [1].
Chapter 1: Indentation and breaking long lines ## Chapter 1: Indentation and breaking long lines
==========
The limit on the length of lines is 80 columns and this is a hard The limit on the length of lines is 80 columns and this is a hard
limit. Using more than 80 columns causes your code to wrap around to limit. Using more than 80 columns causes your code to wrap around to
@ -20,21 +17,21 @@ spaces to control indenting. Indent by two spaces.
Long expressions can be broken up and the parts aligned, as in the second Long expressions can be broken up and the parts aligned, as in the second
example. Either is acceptable. example. Either is acceptable.
```sml
val x = "Long line..."^ val x = "Long line..."^
"Another long line." "Another long line."
val x = "Long line..."^ val x = "Long line..."^
"Another long line." "Another long line."
```
Case expressions should be indented as follows: Case expressions should be indented as follows:
```sml
case expr of case expr of
pat1 => ... pat1 => ...
| pat2 => ... | pat2 => ...
```
If expressions should be indented according to one of the following schemes: If expressions should be indented according to one of the following schemes:
```sml
if exp1 then exp2 if exp1 then if exp1 then exp2 if exp1 then
else if exp3 then exp4 exp2 else if exp3 then exp4 exp2
else if exp5 then exp6 else exp3 else if exp5 then exp6 else exp3
@ -42,13 +39,12 @@ else if exp5 then exp6 else exp3
if exp1 then exp2 else exp3 if exp1 then exp2 if exp1 then exp2 else exp3 if exp1 then exp2
else exp3 else exp3
```
Comments should be indented to the level of the line of code that follows the Comments should be indented to the level of the line of code that follows the
comment. comment.
Chapter 2: Factoring ## Chapter 2: Factoring
==========
Avoid breaking expressions over multiple lines. If a tuple consists of more Avoid breaking expressions over multiple lines. If a tuple consists of more
than two or three elements, you should consider using a record instead of a than two or three elements, you should consider using a record instead of a
@ -60,16 +56,17 @@ multiple lines to something that has good style is to factor the code using a
let expression. Consider the following: let expression. Consider the following:
Bad Bad
```sml
fun euclid (m:int,n:int) : (int * int * int) = fun euclid (m:int,n:int) : (int * int * int) =
if n=0 if n=0
then (b 1, b 0, m) then (b 1, b 0, m)
else (#2 (euclid (n, m mod n)), u - (m div n) * else (#2 (euclid (n, m mod n)), u - (m div n) *
(euclid (n, m mod n)), #3 (euclid (n, m mod n))) (euclid (n, m mod n)), #3 (euclid (n, m mod n)))
```
Better Better
```sml
fun euclid (m:int,n:int) : (int * int * int) = fun euclid (m:int,n:int) : (int * int * int) =
if n=0 if n=0
then (b 1, b 0, m) then (b 1, b 0, m)
@ -78,7 +75,7 @@ Better
u - (m div n) * (euclid (n, m mod n)), u - (m div n) * (euclid (n, m mod n)),
#3 (euclid (n, m mod n))) #3 (euclid (n, m mod n)))
```
Best Best
fun euclid (m:int,n:int) : (int * int * int) = fun euclid (m:int,n:int) : (int * int * int) =
@ -94,38 +91,36 @@ Best
Do not factor unnecessarily. Do not factor unnecessarily.
Bad Bad
```sml
let let
val x = TextIO.inputLine TextIO.stdIn val x = TextIO.inputLine TextIO.stdIn
in in
case x of case x of
... ...
end end
```
Good Good
```sml
case TextIO.inputLine TextIO.stdIn of case TextIO.inputLine TextIO.stdIn of
... ...
```
Bad (provided y is not a large expression): Bad (provided y is not a large expression):
```sml
let val x = y*y in x+z end let val x = y*y in x+z end
```
Good Good
```sml
y*y + z y*y + z
```
## Chapter 3: Comments
Chapter 3: Comments
==========
Comments should be written with SMLDoc [2] in mind; a, nightly updated, API Comments should be written with SMLDoc [2] in mind; a, nightly updated, API
documentation is available [3]. For example: documentation is available [3]. For example:
```sml
(** (**
* opens a file. * opens a file.
* @params {fileName, mode} * @params {fileName, mode}
@ -133,21 +128,22 @@ documentation is available [3]. For example:
* @param mode mode flag * @param mode mode flag
* @return file stream *) * @return file stream *)
val openFile : {fileName : string, mode : openMode} -> stream val openFile : {fileName : string, mode : openMode} -> stream
```
We mainly restrict ourselves to the following SMLDoc tags: We mainly restrict ourselves to the following SMLDoc tags:
```
@params gives names to formal parameters of functions and value constructors @params gives names to formal parameters of functions and value constructors
@param a description of a formal parameter @param a description of a formal parameter
@return a description about return value of the function @return a description about return value of the function
@see related items (specified text is not analyzed in the current version) @see related items (specified text is not analyzed in the current version)
@throws same as the @exception tag @throws same as the @exception tag
```
Signatures must be commented using SMLDoc. Signatures must be commented using SMLDoc.
Comments go above the code they reference, as in the following example: Comments go above the code they reference, as in the following example:
```sml
(** Sums a list of integers. *) (** Sums a list of integers. *)
val sum = foldl (op +) 0 val sum = foldl (op +) 0
```
Avoid Useless Comments. Avoid comments that merely repeat the code they Avoid Useless Comments. Avoid comments that merely repeat the code they
reference or state the obvious. Comments should state the invariants, the reference or state the obvious. Comments should state the invariants, the
non-obvious, or any references that have more information about the code. non-obvious, or any references that have more information about the code.
@ -172,17 +168,16 @@ Multi-line Commenting. When comments are printed on paper, the reader lacks the
advantage of color highlighting performed by an editor such as Emacs. advantage of color highlighting performed by an editor such as Emacs.
Multiline comments can be distinguished from code by preceding each line of the Multiline comments can be distinguished from code by preceding each line of the
comment with a * similar to the following: comment with a * similar to the following:
```sml
(** (**
* This is one of those rare but long comments * This is one of those rare but long comments
* that need to span multiple lines because * that need to span multiple lines because
* the code is unusually complex and requires * the code is unusually complex and requires
* extra explanation. *) * extra explanation. *)
fun complicatedFunction () = ... fun complicatedFunction () = ...
```
## Chapter 4: Parentheses
Chapter 4: Parentheses
==========
Over Parenthesizing. Parentheses have many semantic purposes in ML, including Over Parenthesizing. Parentheses have many semantic purposes in ML, including
constructing tuples, grouping sequences of side-effect expressions, forcing a constructing tuples, grouping sequences of side-effect expressions, forcing a
@ -198,7 +193,7 @@ already wrapped by a let...in...end block, you can drop the parentheses.
Alternative Block Styles. Blocks of code such as let...in...end, struct...end, Alternative Block Styles. Blocks of code such as let...in...end, struct...end,
and sig...end should be indented as follows. There are several alternative and sig...end should be indented as follows. There are several alternative
styles to choose from. styles to choose from.
```sml
fun foo bar = fun foo bar = fun foo bar = let fun foo bar = fun foo bar = fun foo bar = let
let let val p = 4 val p = 4 let let val p = 4 val p = 4
val p = 4 val q = 38 val q = 38 val p = 4 val q = 38 val q = 38
@ -206,11 +201,10 @@ fun foo bar = fun foo bar = fun foo bar = let
in bar * (p + q) bar * (p + q) in bar * (p + q) bar * (p + q)
bar * (p + q) end end bar * (p + q) end end
end end
```
## Chapter 5: Pattern matching
Chapter 5: Pattern matching
==========
No Incomplete Pattern Matches. Incomplete pattern matches are flagged with No Incomplete Pattern Matches. Incomplete pattern matches are flagged with
compiler warnings, which should be treated as errors. compiler warnings, which should be treated as errors.
@ -219,7 +213,7 @@ Pattern Match in the Function Arguments When Possible. Tuples, records and
datatypes can be deconstructed using pattern matching. If you simply datatypes can be deconstructed using pattern matching. If you simply
deconstruct the function argument before you do anything useful, it is better deconstruct the function argument before you do anything useful, it is better
to pattern match in the function argument. Consider these examples: to pattern match in the function argument. Consider these examples:
```sml
Bad Good Bad Good
fun f arg1 arg2 = let fun f (x,y) (z,_) = ... fun f arg1 arg2 = let fun f (x,y) (z,_) = ...
val x = #1 arg1 val x = #1 arg1
@ -237,7 +231,7 @@ fun f arg1 = let fun f {foo=x, bar=y, baz} = ...
in in
... ...
end end
```
Avoid Unnecessary Projections. Prefer pattern matching to projections with Avoid Unnecessary Projections. Prefer pattern matching to projections with
@ -246,6 +240,7 @@ as it is infrequent and the meaning is clearly understood from the context.
The above rule shows how to pattern-match in the function arguments. Here is The above rule shows how to pattern-match in the function arguments. Here is
an example for pattern matching with value declarations. an example for pattern matching with value declarations.
```sml
Bad Good Bad Good
let let let let
val v = someFunction() val (x,y) = someFunction() val v = someFunction() val (x,y) = someFunction()
@ -254,7 +249,7 @@ let let
in end in end
x+y x+y
end end
```
Combine nested case Expressions. Rather than nest case expressions, you can Combine nested case Expressions. Rather than nest case expressions, you can
@ -262,7 +257,7 @@ combine them by pattern matching against a tuple, provided the tests in the
case expressions are independent. Here is an example: case expressions are independent. Here is an example:
Bad Bad
```sml
let let
val d = Date.fromTimeLocal(Time.now()) val d = Date.fromTimeLocal(Time.now())
in in
@ -277,11 +272,11 @@ Bad
10 => print "Happy Metric Day" 10 => print "Happy Metric Day"
| _ => ()) | _ => ())
end end
```
Good Good
```sml
let let
val d = Date.fromTimeLocal(Time.now()) val d = Date.fromTimeLocal(Time.now())
in in
@ -291,7 +286,7 @@ Good
| (Date.Oct, 10) => print "Happy Metric Day" | (Date.Oct, 10) => print "Happy Metric Day"
| _ => () | _ => ()
end end
```
Avoid the use valOf, hd, or tl. The functions valOf, hd, and tl are used to Avoid the use valOf, hd, or tl. The functions valOf, hd, and tl are used to
deconstruct option types and list types. However, they raise exceptions on deconstruct option types and list types. However, they raise exceptions on
certain inputs. You should avoid these functions altogether. It is usually certain inputs. You should avoid these functions altogether. It is usually
@ -299,8 +294,7 @@ easy to achieve the same effect with pattern matching. If you cannot manage to
avoid them, you should handle any exceptions that they might raise. avoid them, you should handle any exceptions that they might raise.
Chapter 6: Naming and declarations ## Chapter 6: Naming and declarations
==========
Naming Conventions. The best way to tell at a glance something about the type Naming Conventions. The best way to tell at a glance something about the type
of a variable is to use the standard SML naming conventions. The following are of a variable is to use the standard SML naming conventions. The following are
@ -309,20 +303,20 @@ SML/NJ libraries:
Token SML Naming Convention Token SML Naming Convention
Variables Symbolic or initial lower case. Use embedded caps for multiword names. Variables Symbolic or initial lower case. Use embedded caps for multiword names.
Example: getItem Example: `getItem`
Functions Initial lower case. Use embedded caps for multiword names. Functions Initial lower case. Use embedded caps for multiword names.
Example: nameOf Example: `nameOf`
Constructors Initial upper case. Use embedded caps for multiword names. Historic Constructors Initial upper case. Use embedded caps for multiword names. Historic
exceptions are nil, true, and false. Rarely are symbolic names like :: used. exceptions are nil, true, and false. Rarely are symbolic names like :: used.
Example: Node, EmptyQueue Example: `Node`, `EmptyQueue`
Types All lower case. Use underscores for multiword names. Types All lower case. Use underscores for multiword names.
Example: priority_queue Example: `priority_queue`
Signatures All upper case. Use underscores for multiword names. Signatures All upper case. Use underscores for multiword names.
Example: PRIORITY_QUEUE Example: `PRIORITY_QUEUE`
Structures Initial upper case. Use embedded caps for multiword names. Structures Initial upper case. Use embedded caps for multiword names.
Example: PriorityQueue Example: `PriorityQueue`
Functors Same as structure convention, except Fn completes the name. Functors Same as structure convention, except Fn completes the name.
Example: PriorityQueueFn Example: `PriorityQueueFn`
These conventions are not enforced by the compiler, though violations of the These conventions are not enforced by the compiler, though violations of the
variable/constructor conventions ought to cause warning messages because of the variable/constructor conventions ought to cause warning messages because of the
@ -333,7 +327,7 @@ variable names that reflect their intended use. Choose words or combinations
of words describing the value. Variable names may be one letter in short let of words describing the value. Variable names may be one letter in short let
blocks. Functions used in a fold, filter, or map are often bound to the name blocks. Functions used in a fold, filter, or map are often bound to the name
f. Here is an example for short variable names: f. Here is an example for short variable names:
```sml
let let
val d = Date.fromTimeLocal(Time.now()) val d = Date.fromTimeLocal(Time.now())
val m = Date.minute d val m = Date.minute d
@ -342,7 +336,7 @@ let
in in
List.filter f [m,s] List.filter f [m,s]
end end
```
Avoid Global Mutable Variables. Mutable values should be local to closures and Avoid Global Mutable Variables. Mutable values should be local to closures and
almost never declared as a structure's value. Global mutable values cause many almost never declared as a structure's value. Global mutable values cause many
@ -362,26 +356,26 @@ by functions within the current structure are aliased to one or two letter
variables at the top of the struct block. This serves two purposes: it shortens variables at the top of the struct block. This serves two purposes: it shortens
the name of the structure and it documents the structures you use. Here is an the name of the structure and it documents the structures you use. Here is an
example: example:
```sml
struct struct
structure H = HashTable structure H = HashTable
structure T = TextIO structure T = TextIO
structure A = Array structure A = Array
... ...
end end
```
Order of Declarations in a Structure. When declaring elements in a structure, Order of Declarations in a Structure. When declaring elements in a structure,
you should first alias the structures you intend to use, followed by the types, you should first alias the structures you intend to use, followed by the types,
followed by exceptions, and lastly list all the value declarations for the followed by exceptions, and lastly list all the value declarations for the
structure. Here is an example: structure. Here is an example:
```sml
struct struct
structure L = List structure L = List
type foo = unit type foo = unit
exception InternalError exception InternalError
fun first list = L.nth(list,0) fun first list = L.nth(list,0)
end end
```
Every declaration within the structure should be indented the same amount. Every declaration within the structure should be indented the same amount.
@ -389,14 +383,14 @@ Moreover, every top-level structure should be restricted by a (documented)
signature. signature.
Functions should declared in their their curried form, e.g., Functions should declared in their their curried form, e.g.,
```sml
fun f x y = ... instead of fun f(x,y) = ... fun f x y = ... instead of fun f(x,y) = ...
```
Datatypes should be preferred to type synonyms in particular for Datatypes should be preferred to type synonyms in particular for
record types record types
Chapter 7: Verbosity ## Chapter 7: Verbosity
==========
Don't Rewrite Library Functions. The basis library and the SML/NJ library have Don't Rewrite Library Functions. The basis library and the SML/NJ library have
a great number of functions and data structures -- use them! Often students a great number of functions and data structures -- use them! Often students
@ -412,6 +406,7 @@ case that the type is bool, you should not be using if at all. Consider the
following: following:
```sml
Bad Good Bad Good
if e then true else false e if e then true else false e
if e then false else true not e if e then false else true not e
@ -421,40 +416,40 @@ if x then true else y x orelse y
if x then y else false x andalso y if x then y else false x andalso y
if x then false else y not x andalso y if x then false else y not x andalso y
if x then y else true not x orelse y if x then y else true not x orelse y
```
Misusing case Expressions. The case expression is misused in two common Misusing case Expressions. The case expression is misused in two common
situations. First, case should never be used in place of an if expression situations. First, case should never be used in place of an if expression
(that's why if exists). Note the following: (that's why if exists). Note the following:
```sml
case e of case e of
true => x true => x
| false => y | false => y
if e then x else y if e then x else y
```
The latter is much better. Another situation where if expressions are The latter is much better. Another situation where if expressions are
preferred over case expressions is as follows: preferred over case expressions is as follows:
```sml
case e of case e of
c => x (* c is a constant value *) c => x (* c is a constant value *)
| _ => y | _ => y
if e=c then x else y if e=c then x else y
```
The latter is definitely better. The other misuse is using case when pattern The latter is definitely better. The other misuse is using case when pattern
matching with a val declaration is enough. Consider the following: matching with a val declaration is enough. Consider the following:
```sml
val x = case expr of (y,z) => y val x = case expr of (y,z) => y
val (x,_) = expr val (x,_) = expr
```
The latter is better. The latter is better.
Other Common Misuses. Here are some other common mistakes to watch out for: Other Common Misuses. Here are some other common mistakes to watch out for:
```sml
Bad Good Bad Good
l::nil [l] l::nil [l]
l::[] [l] l::[] [l]
length + 0 length length + 0 length
@ -471,30 +466,30 @@ Int.compare(x,y)=GREATER x>y
Int.sign(x)=~1 x<0 Int.sign(x)=~1 x<0
Int.sign(x)=0 x=0 Int.sign(x)=0 x=0
Int.sign(x)=1 x>0 Int.sign(x)=1 x>0
```
Do not re-wrap Functions. When passing a function as an argument to another
Don't Re-wrap Functions. When passing a function as an argument to another
function, don't re-wrap the function unnecessarily. Here's an example: function, don't re-wrap the function unnecessarily. Here's an example:
```sml
List.map (fn x => Math.sqrt x) [1.0, 4.0, 9.0, 16.0] List.map (fn x => Math.sqrt x) [1.0, 4.0, 9.0, 16.0]
List.map Math.sqrt [1.0, 4.0, 9.0, 16.0] List.map Math.sqrt [1.0, 4.0, 9.0, 16.0]
```
The latter is better. Another case for rewrapping a function is often The latter is better. Another case for rewrapping a function is often
associated with infix binary operators. To prevent rewrapping the binary associated with infix binary operators. To prevent rewrapping the binary
operator, use the op keyword as in the following example: operator, use the op keyword as in the following example:
```sml
foldl (fn (x,y) => x + y) 0 foldl (fn (x,y) => x + y) 0
foldl (op +) 0 foldl (op +) 0
```
The latter is better. The latter is better.
Don't Needlessly Nest let Expressions. Multiple declarations may occur in the Don't Needlessly Nest let Expressions. Multiple declarations may occur in the
first block of a let...in...end expression. The bindings are performed first block of a let...in...end expression. The bindings are performed
sequentially, so you may use a name bound earlier in the same block. Consider sequentially, so you may use a name bound earlier in the same block. Consider
the following: the following:
```sml
let let
val x = 42 val x = 42
in in
@ -511,7 +506,7 @@ let
in in
x + y x + y
end end
```
The latter is better. The latter is better.
@ -522,8 +517,7 @@ This has the added benefit of letting you document the purpose of the value
with a name. with a name.
Chapter 9: File names and encoding ## Chapter 8: File names and encoding
==========
In general, a source file should only contain one signature or structure. In more In general, a source file should only contain one signature or structure. In more
detail: detail:
@ -537,8 +531,7 @@ and separated by underscore, e.g., ocl_term.sig
Source files should use the Unix line ending convention and be either encoding Source files should use the Unix line ending convention and be either encoding
using ASCII (preferred) or UTF-8. using ASCII (preferred) or UTF-8.
Chapter 9: Compatibility ## Chapter 9: Compatibility
==========
Any code developed must be portable among the supported SML systems Any code developed must be portable among the supported SML systems
(currently: sml/NJ, mlton, polyml 5.x). Moreover, the code should (currently: sml/NJ, mlton, polyml 5.x). Moreover, the code should
@ -547,25 +540,23 @@ warnings as errors. Keep in mind that polyml does only provide a subset
of the SML standard library. of the SML standard library.
Appendix I: Machine-support ## Appendix
=========== ### Appendix I: Machine-support
The following elisp-snippet provides marginal support for this coding-style for The following elisp-snippet provides marginal support for this coding-style for
the sml-mode [4] of Emacs [5]: the sml-mode [4] of Emacs [5]:
```emacs
(setq sml-indent-level 2) (setq sml-indent-level 2)
(setq sml-pipe-indent -2) (setq sml-pipe-indent -2)
(setq sml-case-indent t) (setq sml-case-indent t)
(setq sml-nested-if-indent t) (setq sml-nested-if-indent t)
(setq sml-type-of-indent nil) (setq sml-type-of-indent nil)
(setq sml-electric-semi-mode nil) (setq sml-electric-semi-mode nil)
```
Appendix II: References ### Appendix II: References
============ 1. http://www.cs.cornell.edu/Courses/cs312/2007fa/handouts/style.htm
2. SMLDoc. http://www.pllab.riec.tohoku.ac.jp/smlsharp/?SMLDoc
[1] http://www.cs.cornell.edu/Courses/cs312/2007fa/handouts/style.htm 3. http://projects.brucker.ch/su4sml/smldoc/
[2] SMLDoc. http://www.pllab.riec.tohoku.ac.jp/smlsharp/?SMLDoc 4. http://www.smlnj.org/doc/Emacs/sml-mode.html
[3] http://projects.brucker.ch/su4sml/smldoc/ 5. http://www.gnu.org/software/emacs/
[4] http://www.smlnj.org/doc/Emacs/sml-mode.html
[5] http://www.gnu.org/software/emacs/
--
Last updated on $Date:$