diff --git a/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean b/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean index be63e64..f282d4a 100644 --- a/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean +++ b/Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean @@ -1,5 +1,3 @@ - - import Soda.se.umu.cs.soda.prototype.example.market.core.MyList notation "Money" => Int diff --git a/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean b/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean index 8410d17..3dbf7d9 100644 --- a/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean +++ b/Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean @@ -1,5 +1,3 @@ - - import Soda.se.umu.cs.soda.prototype.example.market.core.Basic class IndexOption ( A : Type ) diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda index 63fd492..eddc725 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Market.soda @@ -1,5 +1,4 @@ - directive lean import Soda.se.umu.cs.soda.prototype.example.market.core.MyList diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda index b65d382..f4f03b6 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/MyList.soda @@ -1,5 +1,4 @@ - directive lean import Soda.se.umu.cs.soda.prototype.example.market.core.Basic diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala index 2298c30..783aeb2 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala @@ -5,6 +5,10 @@ package soda.se.umu.cs.soda.prototype.example.market.core * */ + + + + type Nat = Int object Succ_ { def apply (n : Int) : Int = n + 1 @@ -23,8 +27,6 @@ Notation "'Succ_'" := S (at level 99) . */ - - /* directive lean import Soda.se.umu.cs.soda.prototype.example.market.core.MyList @@ -267,8 +269,6 @@ object MarketBuilder { } - - /* directive lean import Soda.se.umu.cs.soda.prototype.example.market.core.Basic diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda index 611d891..466c4d1 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda @@ -1,6 +1,8 @@ + package soda.se.umu.cs.soda.prototype.example.market.core /* * This package contains classes to model a market * */ + diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.scala b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.scala index 8f86bf0..3bf0ac3 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.scala +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.scala @@ -17,6 +17,10 @@ import soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser import soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser import soda.se.umu.cs.soda.prototype.example.market.serializer.YamlSerializer + + + + /** * This is the main entry point. */ diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.soda index d1e18ba..f7917f2 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/main/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.main /* @@ -17,3 +18,4 @@ import soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser soda.se.umu.cs.soda.prototype.example.market.serializer.YamlSerializer + diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParser.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParser.soda index 262fca2..b289597 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParser.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParser.soda @@ -1,3 +1,4 @@ + class OperationParser abstract diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda index d19991c..5ef76c8 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.parser import diff --git a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda index 6aa4e85..18a71ca 100644 --- a/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda +++ b/core/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.serializer import diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda index 7ec255d..a3c4fd2 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketCollection.soda @@ -17,6 +17,7 @@ class Market01 end + class Market02 extends Market @@ -35,6 +36,7 @@ class Market02 end + class Market03 extends Market diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda index 39ae19c..aa2031a 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/MarketSpec.soda @@ -6,7 +6,6 @@ class MarketSpec () check [A : Type] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = assert (obtained == expected) - module = MarketMod_ (true) market01 : Market = Market01_ () diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/OperationProcessorSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/OperationProcessorSpec.soda index 813ac5d..8195673 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/OperationProcessorSpec.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/OperationProcessorSpec.soda @@ -6,7 +6,6 @@ class OperationParserSpec () check [A : Type] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = assert (obtained == expected) - read_file (file_name : String) : String = @new String ( Files .readAllBytes ( @@ -59,3 +58,4 @@ class OperationParserSpec () ) end + diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala index bd2281b..ffedc54 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.scala @@ -12,6 +12,10 @@ import java.io.StringReader import soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser import soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser + + + + trait Market01 extends Market diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda index 34176cc..66aecd1 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/core/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.core /* @@ -12,3 +13,4 @@ import java.io.StringReader soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser + diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParserSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParserSpec.soda index d96119d..f43abeb 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParserSpec.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/OperationParserSpec.soda @@ -35,3 +35,4 @@ class OperationParserSpec () ) end + diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.scala b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.scala index 7c85cb5..5036f22 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.scala +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.scala @@ -14,6 +14,10 @@ import soda.se.umu.cs.soda.prototype.example.market.core.OpPrice import soda.se.umu.cs.soda.prototype.example.market.core.OpSell import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined + + + + trait Example0Instance { diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda index 2ec3af9..afcb9e9 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.parser import @@ -14,3 +15,4 @@ import soda.se.umu.cs.soda.prototype.example.market.core.OpPrice soda.se.umu.cs.soda.prototype.example.market.core.OpSell soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined + diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/YamlParserSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/YamlParserSpec.soda index 50e1ce8..d9b3b2a 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/YamlParserSpec.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/parser/YamlParserSpec.soda @@ -6,7 +6,6 @@ class YamlParserSpec () check [A : Type] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = assert (obtained == expected) - read_file (file_name : String) : String = @new String ( Files .readAllBytes ( @@ -31,3 +30,4 @@ class YamlParserSpec () ) end + diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.scala b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.scala index a5a8597..3014535 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.scala +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.scala @@ -21,6 +21,10 @@ import soda.se.umu.cs.soda.prototype.example.market.core.OperationProcessor import soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser import soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser + + + + case class YamlParserSpec () extends AnyFunSuite diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda index a0bc16e..84ae605 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.serializer import @@ -22,4 +23,3 @@ import soda.se.umu.cs.soda.prototype.example.market.parser.OperationParser soda.se.umu.cs.soda.prototype.example.market.parser.YamlParser - diff --git a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/YamlSerializerSpec.soda b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/YamlSerializerSpec.soda index 6337882..cf2da6e 100644 --- a/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/YamlSerializerSpec.soda +++ b/core/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/serializer/YamlSerializerSpec.soda @@ -6,7 +6,6 @@ class YamlParserSpec () check [A : Type] (obtained : A) (expected : A) : org.scalatest.compatible.Assertion = assert (obtained == expected) - read_file (file_name : String) : String = @new String ( Files .readAllBytes ( diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda index 94343f3..ae82404 100644 --- a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda +++ b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Basic.soda @@ -28,3 +28,4 @@ class Range _tailrec_range (length) (Nil) end + diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda index fdc6b7a..02a21c0 100644 --- a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda +++ b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/OperationGenerator.soda @@ -1,3 +1,4 @@ + class OperationGenerator abstract diff --git a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda index 0bc847e..70342e9 100644 --- a/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda +++ b/measurement/src/main/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.measurement /* diff --git a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala index fce1ea5..1ca6d92 100644 --- a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala +++ b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.scala @@ -21,6 +21,10 @@ import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined_ import soda.se.umu.cs.soda.prototype.example.market.core.OperationEnum + + + + case class OperationGeneratorSpec () extends AnyFunSuite diff --git a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda index 14dba53..c946398 100644 --- a/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda +++ b/measurement/src/test/scala/soda/se/umu/cs/soda/prototype/example/market/measurement/Package.soda @@ -1,3 +1,4 @@ + package soda.se.umu.cs.soda.prototype.example.market.measurement /* @@ -21,3 +22,4 @@ import soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined soda.se.umu.cs.soda.prototype.example.market.core.OpUndefined_ soda.se.umu.cs.soda.prototype.example.market.core.OperationEnum +