Skip to content

Commit

Permalink
Refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
@FlorianCassayre
FlorianCassayre committed Mar 29, 2022
1 parent 9c98342 commit f2632cc
Show file tree
Hide file tree
Showing 54 changed files with 147 additions and 146 deletions.
7 changes: 0 additions & 7 deletions src/main/scala/masterproject/front/front.scala
View file

This file was deleted.

8 changes: 0 additions & 8 deletions src/main/scala/masterproject/front/proof/Proof.scala
View file

This file was deleted.

12 changes: 6 additions & 6 deletions ...n/scala/masterproject/front/fol/FOL.scala → ...florian/masterproject/front/fol/FOL.scala
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
package masterproject.front.fol
package me.cassayre.florian.masterproject.front.fol

import masterproject.front.fol.conversions.to.*
import masterproject.front.fol.conversions.from.*
import masterproject.front.fol.definitions.*
import masterproject.front.fol.ops.*
import masterproject.front.fol.utils.*
import me.cassayre.florian.masterproject.front.fol.conversions.to.*
import me.cassayre.florian.masterproject.front.fol.conversions.from.*
import me.cassayre.florian.masterproject.front.fol.definitions.*
import me.cassayre.florian.masterproject.front.fol.ops.*
import me.cassayre.florian.masterproject.front.fol.utils.*

object FOL extends FormulaDefinitions
with TermConversionsTo with FormulaConversionsTo
Expand Down
4 changes: 2 additions & 2 deletions ...fol/conversions/FrontKernelMappings.scala → ...fol/conversions/FrontKernelMappings.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package masterproject.front.fol.conversions
package me.cassayre.florian.masterproject.front.fol.conversions

import masterproject.front.fol.definitions.FormulaDefinitions
import me.cassayre.florian.masterproject.front.fol.definitions.FormulaDefinitions

trait FrontKernelMappings {
this: FormulaDefinitions =>
Expand Down
6 changes: 3 additions & 3 deletions ...ersions/from/FormulaConversionsFrom.scala → ...ersions/from/FormulaConversionsFrom.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package masterproject.front.fol.conversions.from
package me.cassayre.florian.masterproject.front.fol.conversions.from

import masterproject.front.fol.conversions.FrontKernelMappings
import masterproject.front.fol.definitions.FormulaDefinitions
import me.cassayre.florian.masterproject.front.fol.conversions.FrontKernelMappings
import me.cassayre.florian.masterproject.front.fol.definitions.FormulaDefinitions

trait FormulaConversionsFrom extends TermConversionsFrom with FrontKernelMappings {
this: FormulaDefinitions =>
Expand Down
4 changes: 2 additions & 2 deletions ...onversions/from/TermConversionsFrom.scala → ...onversions/from/TermConversionsFrom.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package masterproject.front.fol.conversions.from
package me.cassayre.florian.masterproject.front.fol.conversions.from

import masterproject.front.fol.definitions.TermDefinitions
import me.cassayre.florian.masterproject.front.fol.definitions.TermDefinitions

trait TermConversionsFrom {
this: TermDefinitions =>
Expand Down
6 changes: 3 additions & 3 deletions ...conversions/to/FormulaConversionsTo.scala → ...conversions/to/FormulaConversionsTo.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package masterproject.front.fol.conversions.to
package me.cassayre.florian.masterproject.front.fol.conversions.to

import masterproject.front.fol.conversions.FrontKernelMappings
import masterproject.front.fol.definitions.FormulaDefinitions
import me.cassayre.florian.masterproject.front.fol.conversions.FrontKernelMappings
import me.cassayre.florian.masterproject.front.fol.definitions.FormulaDefinitions

trait FormulaConversionsTo extends TermConversionsTo with FrontKernelMappings {
this: FormulaDefinitions =>
Expand Down
6 changes: 3 additions & 3 deletions ...ol/conversions/to/TermConversionsTo.scala → ...ol/conversions/to/TermConversionsTo.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package masterproject.front.fol.conversions.to
package me.cassayre.florian.masterproject.front.fol.conversions.to

import masterproject.front.fol.definitions.TermDefinitions
import me.cassayre.florian.masterproject.front.fol.definitions.TermDefinitions

trait TermConversionsTo {
this: TermDefinitions =>
Expand All @@ -12,7 +12,7 @@ trait TermConversionsTo {

def toKernel(label: SchematicFunctionLabel[?]): lisa.kernel.fol.FOL.SchematicFunctionLabel =
lisa.kernel.fol.FOL.SchematicFunctionLabel(label.id, label.arity)

def toKernel(label: FunctionLabel[?]): lisa.kernel.fol.FOL.FunctionLabel = label match {
case constant: ConstantFunctionLabel[?] => toKernel(constant)
case schematic: SchematicFunctionLabel[?] => toKernel(schematic)
Expand Down
2 changes: 1 addition & 1 deletion ...t/fol/definitions/CommonDefinitions.scala → ...t/fol/definitions/CommonDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.front.fol.definitions
package me.cassayre.florian.masterproject.front.fol.definitions

trait CommonDefinitions {

Expand Down
2 changes: 1 addition & 1 deletion .../fol/definitions/FormulaDefinitions.scala → .../fol/definitions/FormulaDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.front.fol.definitions
package me.cassayre.florian.masterproject.front.fol.definitions

trait FormulaDefinitions extends FormulaLabelDefinitions with TermDefinitions {

Expand Down
2 changes: 1 addition & 1 deletion ...definitions/FormulaLabelDefinitions.scala → ...definitions/FormulaLabelDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.front.fol.definitions
package me.cassayre.florian.masterproject.front.fol.definitions

import scala.compiletime.constValue

Expand Down
2 changes: 1 addition & 1 deletion ...ont/fol/definitions/TermDefinitions.scala → ...ont/fol/definitions/TermDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.front.fol.definitions
package me.cassayre.florian.masterproject.front.fol.definitions

trait TermDefinitions extends TermLabelDefinitions {

Expand Down
2 changes: 1 addition & 1 deletion ...ol/definitions/TermLabelDefinitions.scala → ...ol/definitions/TermLabelDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.front.fol.definitions
package me.cassayre.florian.masterproject.front.fol.definitions

import scala.compiletime.constValue

Expand Down
4 changes: 2 additions & 2 deletions ...sterproject/front/fol/ops/CommonOps.scala → ...sterproject/front/fol/ops/CommonOps.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package masterproject.front.fol.ops
package me.cassayre.florian.masterproject.front.fol.ops

import masterproject.front.fol.definitions.CommonDefinitions
import me.cassayre.florian.masterproject.front.fol.definitions.CommonDefinitions

import scala.compiletime.ops.int.-

Expand Down
4 changes: 2 additions & 2 deletions ...terproject/front/fol/ops/FormulaOps.scala → ...terproject/front/fol/ops/FormulaOps.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package masterproject.front.fol.ops
package me.cassayre.florian.masterproject.front.fol.ops

import masterproject.front.fol.definitions.FormulaDefinitions
import me.cassayre.florian.masterproject.front.fol.definitions.FormulaDefinitions

trait FormulaOps extends CommonOps {
this: FormulaDefinitions =>
Expand Down
4 changes: 2 additions & 2 deletions ...masterproject/front/fol/ops/TermOps.scala → ...masterproject/front/fol/ops/TermOps.scala
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package masterproject.front.fol.ops
package me.cassayre.florian.masterproject.front.fol.ops

import masterproject.front.fol.definitions.TermDefinitions
import me.cassayre.florian.masterproject.front.fol.definitions.TermDefinitions

trait TermOps extends CommonOps {
this: TermDefinitions =>
Expand Down
8 changes: 4 additions & 4 deletions ...roject/front/fol/utils/FormulaUtils.scala → ...roject/front/fol/utils/FormulaUtils.scala
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
package masterproject.front.fol.utils
package me.cassayre.florian.masterproject.front.fol.utils

import masterproject.front.fol.conversions.to.FormulaConversionsTo
import masterproject.front.fol.definitions.FormulaDefinitions
import masterproject.front.fol.ops.CommonOps
import me.cassayre.florian.masterproject.front.fol.conversions.to.FormulaConversionsTo
import me.cassayre.florian.masterproject.front.fol.definitions.FormulaDefinitions
import me.cassayre.florian.masterproject.front.fol.ops.CommonOps

trait FormulaUtils extends TermUtils {
this: FormulaDefinitions & FormulaConversionsTo & CommonOps =>
Expand Down
8 changes: 4 additions & 4 deletions ...erproject/front/fol/utils/TermUtils.scala → ...erproject/front/fol/utils/TermUtils.scala
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
package masterproject.front.fol.utils
package me.cassayre.florian.masterproject.front.fol.utils

import masterproject.front.fol.conversions.to.TermConversionsTo
import masterproject.front.fol.definitions.TermDefinitions
import masterproject.front.fol.ops.CommonOps
import me.cassayre.florian.masterproject.front.fol.conversions.to.TermConversionsTo
import me.cassayre.florian.masterproject.front.fol.definitions.TermDefinitions
import me.cassayre.florian.masterproject.front.fol.ops.CommonOps

trait TermUtils {
this: TermDefinitions & TermConversionsTo & CommonOps =>
Expand Down
7 changes: 7 additions & 0 deletions src/main/scala/me/cassayre/florian/masterproject/front/front.scala
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package me.cassayre.florian.masterproject.front

import me.cassayre.florian.masterproject.front.fol.FOL
import me.cassayre.florian.masterproject.front.proof.Proof

export FOL._
export Proof._
8 changes: 8 additions & 0 deletions src/main/scala/me/cassayre/florian/masterproject/front/proof/Proof.scala
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
package me.cassayre.florian.masterproject.front.proof

import me.cassayre.florian.masterproject.front.proof.state.*
import me.cassayre.florian.masterproject.front.proof.predef.*

object Proof
extends ProofInterfaceDefinitions
with PredefRulesDefinitions with PredefTacticsDefinitions
8 changes: 4 additions & 4 deletions ...proof/predef/PredefRulesDefinitions.scala → ...proof/predef/PredefRulesDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
package masterproject.front.proof.predef
package me.cassayre.florian.masterproject.front.proof.predef

import masterproject.front.fol.FOL.*
import masterproject.front.unification.Unifier.*
import me.cassayre.florian.masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.unification.Unifier.*
import lisa.kernel.proof.SequentCalculus.*
import proven.tactics.SimplePropositionalSolver
import masterproject.front.proof.state.RuleDefinitions
import me.cassayre.florian.masterproject.front.proof.state.RuleDefinitions

trait PredefRulesDefinitions extends RuleDefinitions {

Expand Down
10 changes: 5 additions & 5 deletions ...oof/predef/PredefTacticsDefinitions.scala → ...oof/predef/PredefTacticsDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
package masterproject.front.proof.predef
package me.cassayre.florian.masterproject.front.proof.predef

import lisa.kernel.proof.SCProof
import masterproject.front.fol.FOL.*
import masterproject.front.unification.Unifier.*
import me.cassayre.florian.masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.unification.Unifier.*
import lisa.kernel.proof.SequentCalculus.*
import proven.tactics.SimplePropositionalSolver
import masterproject.front.proof.state.ProofEnvironmentDefinitions
import me.cassayre.florian.masterproject.front.proof.state.ProofEnvironmentDefinitions

trait PredefTacticsDefinitions extends ProofEnvironmentDefinitions {

Expand Down Expand Up @@ -118,7 +118,7 @@ trait PredefTacticsDefinitions extends ProofEnvironmentDefinitions {
}

// Aliases

val solveProp: TacticSolver.type = TacticSolver
val rewrite: TacticalRewrite.type = TacticalRewrite

Expand Down
4 changes: 2 additions & 2 deletions ...nt/proof/sequent/SequentDefinitions.scala → ...nt/proof/sequent/SequentDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package masterproject.front.proof.sequent
package me.cassayre.florian.masterproject.front.proof.sequent

import lisa.kernel.Printer
import masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.fol.FOL.*

trait SequentDefinitions {

Expand Down
6 changes: 3 additions & 3 deletions ...ject/front/proof/sequent/SequentOps.scala → ...ject/front/proof/sequent/SequentOps.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package masterproject.front.proof.sequent
package me.cassayre.florian.masterproject.front.proof.sequent

import masterproject.front.proof.sequent.SequentDefinitions
import masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.proof.sequent.SequentDefinitions
import me.cassayre.florian.masterproject.front.fol.FOL.*

trait SequentOps {
this: SequentDefinitions =>
Expand Down
4 changes: 2 additions & 2 deletions ...f/state/ProofEnvironmentDefinitions.scala → ...f/state/ProofEnvironmentDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
package masterproject.front.proof.state
package me.cassayre.florian.masterproject.front.proof.state

import lisa.kernel.Printer
import lisa.kernel.proof.{SCProof, SCProofChecker}
import lisa.kernel.proof.SequentCalculus.SCSubproof
import masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.fol.FOL.*

trait ProofEnvironmentDefinitions extends ProofStateDefinitions {

Expand Down
2 changes: 1 addition & 1 deletion ...oof/state/ProofInterfaceDefinitions.scala → ...oof/state/ProofInterfaceDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.front.proof.state
package me.cassayre.florian.masterproject.front.proof.state

trait ProofInterfaceDefinitions extends ProofEnvironmentDefinitions {

Expand Down
10 changes: 5 additions & 5 deletions ...t/proof/state/ProofStateDefinitions.scala → ...t/proof/state/ProofStateDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
package masterproject.front.proof.state
package me.cassayre.florian.masterproject.front.proof.state

import lisa.kernel.proof.SCProof
import masterproject.front.fol.FOL.*
import masterproject.front.unification.Unifier.*
import me.cassayre.florian.masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.unification.Unifier.*
import lisa.kernel.proof.SequentCalculus.{Rewrite, SCProofStep}
import masterproject.SCUtils
import masterproject.front.proof.sequent.{SequentDefinitions, SequentOps}
import me.cassayre.florian.masterproject.util.SCUtils
import me.cassayre.florian.masterproject.front.proof.sequent.{SequentDefinitions, SequentOps}

trait ProofStateDefinitions extends SequentDefinitions with SequentOps {

Expand Down
6 changes: 3 additions & 3 deletions ...t/front/proof/state/RuleDefinitions.scala → ...t/front/proof/state/RuleDefinitions.scala
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
package masterproject.front.proof.state
package me.cassayre.florian.masterproject.front.proof.state

import lisa.kernel.proof.SequentCalculus.SCProofStep
import masterproject.front.unification.Unifier.*
import masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.unification.Unifier.*
import me.cassayre.florian.masterproject.front.fol.FOL.*

import scala.collection.View

Expand Down
4 changes: 2 additions & 2 deletions ...erproject/front/unification/Unifier.scala → ...erproject/front/unification/Unifier.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package masterproject.front.unification
package me.cassayre.florian.masterproject.front.unification

import lisa.kernel.Printer
import masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.front.fol.FOL.*

import scala.annotation.tailrec

Expand Down
7 changes: 4 additions & 3 deletions .../masterproject/GoalBasedProofSystem.scala → ...project/legacy/GoalBasedProofSystem.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject
package me.cassayre.florian.masterproject.legacy

import lisa.kernel.fol.FOL.*
import lisa.KernelHelpers.*
Expand All @@ -7,8 +7,9 @@ import lisa.kernel.Printer.*
import lisa.kernel.proof.SequentCalculus.{Hypothesis, Sequent, Weakening, sequentToFormula}
import lisa.kernel.proof.{RunningTheory, SCProof, SCProofChecker}
import lisa.settheory.AxiomaticSetTheory
import masterproject.SCProofBuilder
import masterproject.SCProofBuilder.{SCExplicitProofStep, SCHighLevelProofStep, SCImplicitProofStep}
import me.cassayre.florian.masterproject.util.SCUtils
import me.cassayre.florian.masterproject.util.SCProofBuilder
import me.cassayre.florian.masterproject.util.SCProofBuilder.{SCExplicitProofStep, SCHighLevelProofStep, SCImplicitProofStep}
import proven.tactics.SimplePropositionalSolver

object GoalBasedProofSystem {
Expand Down
6 changes: 3 additions & 3 deletions ...terproject/GoalBasedProofSystemREPL.scala → ...ect/legacy/GoalBasedProofSystemREPL.scala
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package masterproject
package me.cassayre.florian.masterproject.legacy

import masterproject.parser.SCReader
import masterproject.GoalBasedProofSystem.*
import me.cassayre.florian.masterproject.parser.SCReader
import me.cassayre.florian.masterproject.legacy.GoalBasedProofSystem.*

import java.util.Scanner
import scala.util.{Failure, Success, Try}
Expand Down
12 changes: 6 additions & 6 deletions src/main/scala/masterproject/meta/Meta.scala → ...rian/masterproject/legacy/meta/Meta.scala
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
package masterproject.meta
package me.cassayre.florian.masterproject.legacy.meta

import lisa.kernel.Printer
import lisa.kernel.proof.{SCProof, SCProofChecker, SequentCalculus}
import masterproject.front.fol.FOL.*
import masterproject.parser.SCReader.*
import masterproject.front.unification.Unifier
import masterproject.front.unification.Unifier.*
import me.cassayre.florian.masterproject.front.fol.FOL.*
import me.cassayre.florian.masterproject.parser.SCReader.*
import me.cassayre.florian.masterproject.front.unification.Unifier
import me.cassayre.florian.masterproject.front.unification.Unifier.*
import lisa.kernel.proof.SequentCalculus.{Cut, Hypothesis, LeftAnd, RightAnd, SCProofStep, SCSubproof, Weakening}
import masterproject.SCUtils
import me.cassayre.florian.masterproject.util.SCUtils
import proven.tactics.SimplePropositionalSolver

object Meta {
Expand Down
2 changes: 1 addition & 1 deletion ...sterproject/parser/ReadingException.scala → ...sterproject/parser/ReadingException.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.parser
package me.cassayre.florian.masterproject.parser

import scala.util.parsing.input.Position

Expand Down
8 changes: 4 additions & 4 deletions .../scala/masterproject/parser/SCLexer.scala → ...lorian/masterproject/parser/SCLexer.scala
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
package masterproject.parser
package me.cassayre.florian.masterproject.parser

import masterproject.parser.ReadingException.LexingException
import masterproject.parser.SCToken
import masterproject.parser.SCToken.*
import me.cassayre.florian.masterproject.parser.ReadingException.LexingException
import me.cassayre.florian.masterproject.parser.SCToken
import me.cassayre.florian.masterproject.parser.SCToken.*

import scala.util.matching.Regex
import scala.util.parsing.combinator.RegexParsers
Expand Down
2 changes: 1 addition & 1 deletion ...scala/masterproject/parser/SCParsed.scala → ...orian/masterproject/parser/SCParsed.scala
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
package masterproject.parser
package me.cassayre.florian.masterproject.parser

import scala.util.parsing.input.{Position, Positional}

Expand Down
Loading

0 comments on commit f2632cc

Please sign in to comment.