Merge pull request #3 from julianmendez/19-improved-translators

19 improved translators

.github/workflows/ci.yml

@@ -18,8 +18,8 @@ jobs:
         - 17
         scala:
         - 2.11.12
-        - 2.12.17
-        - 2.13.10
+        - 2.12.18
+        - 2.13.11
         - 3.3.0
     steps:
     - name: Check out

build.sbt

@@ -2,16 +2,16 @@ import sbt.Keys.scalacOptions
 
 lazy val scala2_11 = "2.11.12"
 
-lazy val scala2_12 = "2.12.17"
+lazy val scala2_12 = "2.12.18"
 
-lazy val scala2_13 = "2.13.10"
+lazy val scala2_13 = "2.13.11"
 
 lazy val scala3_3 = "3.3.0"
 
 lazy val commonSettings =
   Seq(
     organization := "se.umu.cs.rai.soda",
-    version := "0.18.0",
+    version := "0.19.0",
     description := "Object-oriented functional language to describe, analyze, and model human-centered problems",
     homepage := Some(url("https://julianmendez.github.io/soda/")),
     startYear := Some(2020),

docs/README.md

@@ -1,7 +1,7 @@
 # Soda
 
-*Soda* (Symbolic Objective Descriptive Analysis) is an object-oriented functional language to describe, analyze, and
-model human-centered problems.
+*Soda* (Symbolic Objective Descriptive Analysis) is an object-oriented functional language to
+describe, analyze, and model human-centered problems.
 Due to its readability, it can be applied to model ethical problems.
 
 This project includes a translator to [Scala](https://scala-lang.org).
@@ -22,7 +22,7 @@ The reserved words are:
 - `this`, `subtype`, `supertype`
 - `false`, `true` , `not`, `and`, `or`
 - `package`, `import`
-- `theorem`, `proof`
+- `directive`
 
 
 ## Other Symbols
@@ -56,7 +56,8 @@ Special names:
 In Soda, variables cannot change their value. Thus, it is not possible to write `x = x + 1`.
 Loops can be managed with `range` and `fold` functions and tail recursion.
 
-The language does not provide `throw`, `try`, and `catch`, because those commands do not follow the functional style.
+The language does not provide `throw`, `try`, and `catch`, because those commands do not follow
+the functional style.
 
 
 ## Static Typing
@@ -70,7 +71,8 @@ This constructor is implemented with a *concrete class* (like a *case class* in
 
 Soda is designed to be integrated via the Java Virtual Machine.
 It is possible to define packages and to declare imports.
-This can be done in a separate file `Package.soda`, which is in the same directory as the source code.
+This can be done in a separate file `Package.soda`, which is in the same directory as the source
+code.
 
 
 ## Syntax Highlighting

docs/RELEASE-NOTES.md

@@ -1,11 +1,29 @@
 ---
+- - version: v0.19.0
+  - date: '2023-07-01'
+  - build: sbt '++ 3.3.0' clean compile test package assembly
+  - release: target/scala-3.3.0/soda-0.19.0.jar
+  - new_features:
+    - includes creation of instances with individual parameters, e.g. `Pair_ (fst) (snd)`
+      instead of `Pair_ (fst , snd)`
+    - includes an experimental translator to Lean 4, which can translate some snippets
+    - uses `Type` to define type membership of parametric types
+    - accepts that class `end` could have a class name
+    - accepts `def` as an optional reserved word to define functions
+    - includes the reserved word `directive` to include specific pieces of code depending
+      on the translator, especially for the translators to Lean and to Coq
+  - deprecated_features:
+    - the `proof` reserved word is no longer used, and a `theorem` block should include the
+      proof after stating the theorem
 - - version: v0.18.0
   - date: '2023-06-01'
   - build: sbt '++ 3.3.0' clean compile test package assembly
   - release: target/scala-3.3.0/soda-0.18.0.jar
   - new_features:
-    - assumes translation to `Package.scala` files as default configuration for the Scala translator
-    - expects multiple type parameters to be between different square brackets, e.g. `MyPair [A] [B]` instead of `MyPair [A, B]`
+    - assumes translation to `Package.scala` files as default configuration for the Scala
+      translator
+    - expects multiple type parameters to be between different square brackets, e.g.
+      `MyPair [A] [B]` instead of `MyPair [A, B]`
     - accepts intersection types (built with `&`) and union types (built with `|`)
   - bug_fixes:
     - fixes translation of reserved words after opening parenthesis
@@ -18,14 +36,16 @@
   - new_features:
     - includes an option to translate a whole Soda package into a single Scala file
     - reads `Package.soda` as prelude for a Soda file in the same directory
-    - requires `match`-`case` structures to be used at most once in a function definition, and cannot be nested in another structure
+    - requires `match`-`case` structures to be used at most once in a function definition, and
+      cannot be nested in another structure
     - improves function definition by allowing multiple lines in its signature
     - accepts reserved word `any` as a synonym for `lambda`
-    - accepts Unicode characters for reserved words, like the letter lambda for `lambda` and right arrows for `->`, `-->`, and `==>`
+    - accepts Unicode characters for reserved words, like the letter lambda for `lambda` and
+      right arrows for `->`, `-->`, and `==>`
     - includes a Bash script (`makeall.sh`) to build the project and create the binary file
   - deprecated_features:
     - the `end` reserved word for `match`-`case` is no longer used
-- version: v0.16.0
+- - version: v0.16.0
   - date: '2022-08-02'
   - new_features:
     - includes an extension to generate LaTeX files from source code
@@ -52,16 +72,21 @@
 - - version: v0.14.0
   - date: '2022-02-11'
   - new_features:
-    - uses curried functions instead of the uncurried ones, for example, replacing `f (x, y)` by `f (x) (y)`
-    - generates default constructors for all the abstract classes and these constructors are named like the class with an underscore (`_`) at the end
-    - renames the main class to be `Main` and `Main_` for the abstract and concrete classes respectively
+    - uses curried functions instead of the uncurried ones, for example, replacing `f (x, y)`
+      by `f (x) (y)`
+    - generates default constructors for all the abstract classes and these constructors are
+      named like the class with an underscore (`_`) at the end
+    - renames the main class to be `Main` and `Main_` for the abstract and concrete classes
+      respectively
     - uses `Main` class to detect the entry point
     - does not support the `with` reserved word
-    - changes the syntax of class declarations such that each super class needs its own line and the definition sign (`=`) is not used
+    - changes the syntax of class declarations such that each super class needs its own line and
+      the definition sign (`=`) is not used
     - includes reserved word `abstract` to define a block of abstract constants and functions
     - makes reserved word `import` define a block of classes to import
     - produces a more similar translation to Scala by removing the line joiners
-    - restricts how a constant or function is defined, such that the definiendum cannot be written in multiple lines
+    - restricts how a constant or function is defined, such that the definiendum cannot be
+      written in multiple lines
     - does not need opening brace (`{`) to start a class definition
     - uses word `end` to end a class definition
     - has `lambda` reserved word as 'recommended' instead of 'optional'
@@ -83,11 +108,14 @@
     - changes syntax of pattern matching to use `match`, `case`, `=>`, `end`
     - includes reserved words `theorem` and `proof` to write properties in Gallina (Coq)
     - makes annotation `@tailrec` only available to class methods
-    - adopts special prefixes `_tailrec_` for tail recursive functions and `_rec_` for recursive functions
+    - adopts special prefixes `_tailrec_` for tail recursive functions and `_rec_` for recursive
+      functions
     - uses a `let`-`in` structure in functions of unit tests
-    - discourages use of `let`-`in` structures and does not support nested use, to avoid long functions
+    - discourages use of `let`-`in` structures and does not support nested use, to avoid long
+      functions
   - deprecated_features:
-    - use of a `let`-`in` structure is only supported as main structure inside a test or function definition
+    - use of a `let`-`in` structure is only supported as main structure inside a test or
+      function definition
   - release: target/scala-3.1.0/soda-0.13.0.jar
 - - version: v0.12.0
   - date: '2021-10-08'
@@ -102,23 +130,27 @@
   - new_features:
     - compiles with Scala 3.0.2
     - has an improved documentation
-    - includes `match` and `case` for pattern matching, and synonym `|` at the beginning of the line for `case`
+    - includes `match` and `case` for pattern matching, and synonym `|` at the beginning of the
+      line for `case`
     - includes an optional `lambda` reserved word to make lambda expressions more explicit
     - includes type aliases for code translated to Scala 3
     - allows defining the body of a class without braces when the code is translated to Scala 3
     - adopts a naming standard for concrete classes to end in underscore
     - includes new synonyms, `<:` for `subtype` and `>:` for `supertype`
     - supports (again) the use of tuples on the left-hand side of a definition sign (`=`)
-    - renames (again) concrete classes in `OptionSD`, mapping `NoneSD` to `NoneSD_` and `SomeSD` to `SomeSD_`
+    - renames (again) concrete classes in `OptionSD`, mapping `NoneSD` to `NoneSD_` and `SomeSD`
+      to `SomeSD_`
   - build: sbt '++ 3.0.2' clean compile test package assembly
   - release: target/scala-3.0.2/soda-0.11.0.jar
 - - version: v0.10.0
   - date: '2021-08-08'
   - new_features:
-    - has its functions separated from concrete classes making abstract classes the only classes containing functions
+    - has its functions separated from concrete classes making abstract classes the only classes
+      containing functions
     - uses a uniform standard for constant names, function names, and class names
     - renames `foldLeft` and `foldLeftWhile` to just `fold` in `Recursive` library class
-    - renames concrete classes in `OptionSD`, mapping `NoneSD` to `NoElem` and `SomeSD` to `SomeElem`
+    - renames concrete classes in `OptionSD`, mapping `NoneSD` to `NoElem` and `SomeSD` to
+      `SomeElem`
     - includes a module for examples
   - build: sbt '++ 3.0.0' clean compile test package assembly
   - release: target/scala-3.0.0/soda-0.10.0.jar
@@ -127,9 +159,11 @@
   - new_features:
     - includes `let` and `in` reserved words to define a block of bindings
     - makes opening brackets (`[`) in the same line as the following
-    - makes closing parenthesis (`)`) and closing brackets (`]`) be in the same line as the previous one
+    - makes closing parenthesis (`)`) and closing brackets (`]`) be in the same line as the
+      previous one
     - makes reserved words `extends` and `with` be able to join lines,
-      either written at the beginning to join the previous line, or at the end to join the following line
+      either written at the beginning to join the previous line, or at the end to join the
+      following line
     - is compatible with Scala 2.12.14
   - deprecated_features:
     - synonym `suchthat` for `->` is no longer supported
@@ -138,12 +172,15 @@
 - - version: v0.8.0
   - date: '2021-05-23'
   - new_features:
-    - compiles with Scala 3.0.0 and is compatible with Scala 2.13.6, Scala 2.12.13, and Scala 2.11.12
+    - compiles with Scala 3.0.0 and is compatible with Scala 2.13.6, Scala 2.12.13, and Scala
+      2.11.12
     - lets Scala 3 reserved words be usable as variable, function, and class names
     - makes `=` (definition symbol) used to define values, functions, and classes
-    - replaces `new` command by `@new` annotation, which is only required to translations to Scala 2
+    - replaces `new` command by `@new` annotation, which is only required to translations to
+      Scala 2
     - expands Soda library in multiple files
-    - accepts `(` (opening parenthesis) at the end of a line to join lines, like `,` (comma) does
+    - accepts `(` (opening parenthesis) at the end of a line to join lines, like `,` (comma)
+      does
     - replaces `extends` to declare upper bounds of type parameters by `subtype`
     - includes `supertype` to declare lower bounds of type parameters
     - replaces all `package.scala` files by `Package` abstract classes to document the package
@@ -153,12 +190,15 @@
   - date: '2021-04-24'
   - new_features:
     - compiles with Scala 3.0.0-RC2
-    - makes `:=` (parameter definition symbol) as the symbol to define values for named parameters
-    - includes `extends` to declare upper bounds of type parameters, with the meaning 'subtype of'
+    - makes `:=` (parameter definition symbol) as the symbol to define values for named
+      parameters
+    - includes `extends` to declare upper bounds of type parameters, with the meaning
+      'subtype of'
     - includes a file expansion of a basic library when it finds `lib.soda`
     - produces better looking Scala translated source code
   - deprecated_features:
-    - does not support any longer the use of tuples on the left-hand side of a definition sign (`=`)
+    - does not support any longer the use of tuples on the left-hand side of a definition sign
+      (`=`)
   - bug_fixes:
     - fixes translation of constants that are lambda functions
   - build: sbt '++ 3.0.0-RC2' clean compile test package assembly
@@ -174,10 +214,12 @@
   - new_features:
     - translates functions without parameters as `lazy val`
     - changes its main package to `scopus`, and includes subpackages
-    - accepts `,` (comma) at the end of a line to join lines and allow multi-line function signatures
+    - accepts `,` (comma) at the end of a line to join lines and allow multi-line function
+      signatures
     - makes annotation `@tailrec` be automatically imported
     - allows annotation `@tailrec` only inside functions
-    - compiles with Scala 3.0.0-RC1 and is compatible with Scala 2.11.12, Scala 2.12.13, Scala 2.13.5
+    - compiles with Scala 3.0.0-RC1 and is compatible with Scala 2.11.12, Scala 2.12.13,
+      Scala 2.13.5
   - deprecated_features:
     - synonym `to` for `->` and synonym `in` for `:` are no longer supported
   - bug_fixes:
@@ -212,7 +254,8 @@
   - date: '2021-02-01'
   - new_features:
     - is compiled by default for Scala 3.0.0-M3
-    - includes a highlighting configuration file for [gedit](https://gitlab.gnome.org/GNOME/gedit/)
+    - includes a highlighting configuration file for
+      [gedit](https://gitlab.gnome.org/GNOME/gedit/)
     - renames synonym `that` to `suchthat`
     - includes annotation `@main` to indicate the entry point
     - has an updated manual
@@ -272,7 +315,8 @@
     - . `package`
     - . `import`
     - . `new`
-    - has `@tailrec` annotation to indicate tail recursion, and `@override` annotation to allow overriding JVM functions
+    - has `@tailrec` annotation to indicate tail recursion, and `@override` annotation to allow
+      overriding JVM functions
   - build: sbt clean compile test package assembly
   - release: target/scala-2.13/scopus-0.1.0.jar
 - - schema: RELEASE-NOTES.md.schema.yaml

documentation/src/site/tex/common/language.tex

@@ -1,7 +1,7 @@
 \usepackage{listings}
 
 \lstdefinelanguage{Soda}{
-    morekeywords={lambda, any, if, then, else, match, case, class, extends, abstract, end, this, subtype, supertype, false, true, not, and, or, package, import, theorem, proof, @new, @tailrec, @override},
+    morekeywords={lambda, any, def, if, then, else, match, case, class, extends, abstract, end, this, subtype, supertype, false, true, not, and, or, package, import, theorem, proof, @new, @tailrec, @override},
     sensitive=true,
     morecomment=[s]{/*}{*/},
     morestring=[b]"
@@ -40,7 +40,7 @@
 \newcommand{\reservedWordSoda}[1]{{\color{sodablue}\srccode{#1}}\xspace}
 \newcommand{\sodaType}[1]{\basicType{{#1}}}
 
-\newcommand{\sodadef}{\srccode{=}\xspace}
+\newcommand{\sodadefequal}{\srccode{=}\xspace}
 \newcommand{\sodacolon}{\srccode{:}\xspace}
 \newcommand{\sodaarrow}{{-\textgreater}\xspace}
 \newcommand{\sodaimplies}{{==\textgreater}\xspace}
@@ -51,6 +51,7 @@
 \newcommand{\sodalambda}{\reservedWordSoda{lambda}}
 \newcommand{\sodaany}{\reservedWordSoda{any}}
 
+\newcommand{\sodadef}{\reservedWordSoda{def}}
 \newcommand{\sodaif}{\reservedWordSoda{if}}
 \newcommand{\sodathen}{\reservedWordSoda{then}}
 \newcommand{\sodaelse}{\reservedWordSoda{else}}

examples/src/main/coq/soda/example/FactorialConcise.v

@@ -26,7 +26,8 @@ Module FactorialConciseSpec.
   Import FactorialConcise.
 
   Definition factorial_values : list (prod nat nat) :=
-    (pair 0 1) :: (pair 1 1) :: (pair 2 2) :: (pair 3 6) :: (pair 4 24) :: (pair 5 120) :: (pair 6 720) :: nil.
+    (pair 0 1) :: (pair 1 1) :: (pair 2 2) :: (pair 3 6) :: (pair 4 24) :: (pair 5 120) ::
+    (pair 6 720) :: nil.
 
   Example test_1 :
     map get_factorial (map fst factorial_values) = map snd factorial_values.

examples/src/main/coq/soda/example/FactorialWithFold.v

@@ -20,7 +20,8 @@ Module FactorialWithFoldSpec.
   Import FactorialWithFold.
 
   Definition factorial_values : list (prod nat nat) :=
-    (pair 0 1) :: (pair 1 1) :: (pair 2 2) :: (pair 3 6) :: (pair 4 24) :: (pair 5 120) :: (pair 6 720) :: nil.
+    (pair 0 1) :: (pair 1 1) :: (pair 2 2) :: (pair 3 6) :: (pair 4 24) :: (pair 5 120) ::
+    (pair 6 720) :: nil.
 
   Example test_1 :
     map get_factorial (map fst factorial_values) = map snd factorial_values.

examples/src/main/coq/soda/example/FiboExample.v

@@ -27,7 +27,9 @@ Module FiboExampleSpec.
   Import FiboExample.
 
   Definition fibonacci_values : list (prod nat nat) :=
-    (pair 0 0) :: (pair 1 1) :: (pair 2 1) :: (pair 3 2) :: (pair 4 3) :: (pair 5 5) :: (pair 6 8) :: (pair 7 13) :: (pair 8 21) :: (pair 9 34) :: (pair 10 55) :: (pair 11 89) :: (pair 12 144) :: nil.
+    (pair 0 0) :: (pair 1 1) :: (pair 2 1) :: (pair 3 2) :: (pair 4 3) :: (pair 5 5) ::
+    (pair 6 8) :: (pair 7 13) :: (pair 8 21) :: (pair 9 34) :: (pair 10 55) :: (pair 11 89) ::
+    (pair 12 144) :: nil.
 
   Example test_1 :
     map fib (map fst fibonacci_values) = map snd fibonacci_values.

examples/src/main/coq/soda/example/PatternMatching.v

@@ -50,7 +50,8 @@ Module PatternMatchingSpec.
   Import PatternMatching.
 
   Definition values : list (prod Param nat) :=
-    (pair (Singleton_ 5) 5) :: (pair (Pair_ 10 100) 55) :: (pair (Triplet_ 9 100 890) 333) :: nil.
+    (pair (Singleton_ 5) 5) :: (pair (Pair_ 10 100) 55) ::
+    (pair (Triplet_ 9 100 890) 333) :: nil.
 
   Example test_1 :
     map get_value (map fst values) = map snd values.

examples/src/main/coq/soda/example/PiIterator.v

@@ -129,7 +129,8 @@ Module PiIterator.
     in let new_status := (Status.Status_ r n q t l k)
     in (BigIntAndStatus.BigIntAndStatus_ ret new_status).
 
-  Fixpoint _tailrec_take (n : nat) (rev_seq : list nat) (s : Status.type) : (prod (list nat) Status.type) :=
+  Fixpoint _tailrec_take (n : nat) (rev_seq : list nat)
+      (s : Status.type) : (prod (list nat) Status.type) :=
     match n with
       | O => (pair (rev rev_seq) s)
       | S m =>
@@ -146,7 +147,8 @@ Module PiIteratorSpec.
 
   Import PiIterator.
 
-  Definition piStart : list nat := 3 :: 1 :: 4 :: 1 :: 5 :: 9 :: 2 :: 6 :: 5 :: 3 :: 5 :: 8 :: nil.
+  Definition piStart : list nat :=
+    3 :: 1 :: 4 :: 1 :: 5 :: 9 :: 2 :: 6 :: 5 :: 3 :: 5 :: 8 :: nil.
 
   Definition piSequence : list nat := PiIterator.take 12.
 

examples/src/main/coq/soda/example/SaladMaker.v

@@ -26,7 +26,8 @@ Module SaladMaker.
       | head :: tail =>
           if ( negb (condition_to_continue salad_so_far head) )
         then salad_so_far
-        else ( prepare_salad Ingredient Salad next_ingredient_function condition_to_continue tail (next_ingredient_function salad_so_far head) )
+        else ( prepare_salad Ingredient Salad next_ingredient_function
+          condition_to_continue tail (next_ingredient_function salad_so_far head) )
   end.
 
 End SaladMaker.
@@ -52,7 +53,8 @@ Import SaladMaker.
   Definition add_next_ingredient (salad_so_far : list SaladIngredient) (ingredient : SaladIngredient) : list SaladIngredient :=
     ingredient :: salad_so_far.
 
-  Definition has_salad_at_most_2_ingredients (salad_so_far : list SaladIngredient) (next_ingredient : SaladIngredient) : bool :=
+  Definition has_salad_at_most_2_ingredients (salad_so_far : list SaladIngredient)
+      (next_ingredient : SaladIngredient) : bool :=
     (length salad_so_far) <? 3.
 
   Definition ingredients := SaladIngredient_values.