Skip to content

Commit

Permalink
Reformat Soda files
Browse files Browse the repository at this point in the history
  • Loading branch information
julianmendez committed Oct 29, 2024
1 parent e175cd7 commit 356f71d
Show file tree
Hide file tree
Showing 28 changed files with 46 additions and 15 deletions.
2 changes: 0 additions & 2 deletions Soda/se/umu/cs/soda/prototype/example/market/core/Market.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@


import Soda.se.umu.cs.soda.prototype.example.market.core.MyList

notation "Money" => Int
Expand Down
2 changes: 0 additions & 2 deletions Soda/se/umu/cs/soda/prototype/example/market/core/MyList.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@


import Soda.se.umu.cs.soda.prototype.example.market.core.Basic

class IndexOption ( A : Type )
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@


directive lean
import Soda.se.umu.cs.soda.prototype.example.market.core.MyList

Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@


directive lean
import Soda.se.umu.cs.soda.prototype.example.market.core.Basic

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -23,8 +27,6 @@ Notation "'Succ_'" := S (at level 99) .
*/




/*
directive lean
import Soda.se.umu.cs.soda.prototype.example.market.core.MyList
Expand Down Expand Up @@ -267,8 +269,6 @@ object MarketBuilder {
}




/*
directive lean
import Soda.se.umu.cs.soda.prototype.example.market.core.Basic
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@

package soda.se.umu.cs.soda.prototype.example.market.core

/*
* This package contains classes to model a market
*
*/

Original file line number Diff line number Diff line change
Expand Up @@ -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.
*/
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.main

/*
Expand All @@ -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

Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

class OperationParser

abstract
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.parser

import
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.serializer

import
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ class Market01

end


class Market02
extends
Market
Expand All @@ -35,6 +36,7 @@ class Market02

end


class Market03
extends
Market
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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_ ()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand Down Expand Up @@ -59,3 +58,4 @@ class OperationParserSpec ()
)

end

Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.core

/*
Expand All @@ -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

Original file line number Diff line number Diff line change
Expand Up @@ -35,3 +35,4 @@ class OperationParserSpec ()
)

end

Original file line number Diff line number Diff line change
Expand Up @@ -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
{

Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.parser

import
Expand All @@ -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

Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand All @@ -31,3 +30,4 @@ class YamlParserSpec ()
)

end

Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.serializer

import
Expand All @@ -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


Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,3 +28,4 @@ class Range
_tailrec_range (length) (Nil)

end

Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

class OperationGenerator

abstract
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.measurement

/*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@

package soda.se.umu.cs.soda.prototype.example.market.measurement

/*
Expand All @@ -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

0 comments on commit 356f71d

Please sign in to comment.