Skip to content
Snippets Groups Projects
  • SimonGuilloud's avatar
    265ed45e
    Types (#166) · 265ed45e
    SimonGuilloud authored
    * Starting a layer of abstraction.
    
    * swrdgv
    
    * sedgf
    
    * ONgoing work. FOL structure mostly implemented, substitutions ongoing.
    
    * continued
    
    * further changes
    
    * LisaObject has a self type being self
    
    * More improvements on substitution
    
    * More work
    
    * multivar substitution
    
    * improvements to MapProofTest
    
    * finished fol, need to do prooflib
    
    * started work on prooflib, cut plenty unused code in Library.scala
    
    * more work on substitutions
    
    * updated WithTheorems
    
    * finished BasicSteptactics and substitutions
    
    * more corrections of tactics using unifier
    
    * fixed F and K imports
    
    * finished PrrofHelpers and definitions. Definitions possibly not final
    
    * Done most of the simpleDeducedSteps
    
    * ongoing work on types
    
    * added doc in Common.scala
    
    * more doc, some simplification
    
    * more doc and simplification of unneeded parts
    
    * fixed some export issues. Commented some tests. translation left for the future.
    
    * remove some debug code
    
    * add missing files
    
    * continue F integration. FInished with Set theory library files, now doing CommonTactics.scala (part is Dario's work).
    
    * simplifier remaining
    
    * renaming and mroe compatibility
    
    * more adaptations
    
    * merge build.sbt
    
    * fixing
    
    * transforming unification to Front
    
    * weird issues with match types and dotty
    
    * Compiles..? Need to simplify use of Arity in formula labels now. Finger crossed.
    
    * add missing files
    
    * still compiles
    
    * Term**0 |-> Term
    
    * Does not compile (dotty crash). Possibly due to covariant schematic labels.
    
    * Labels are contravariant
    
    * Weird "inherits conflicting instances of non-variant base trait LisaObject"
    
    * structure seems to work; Constant extends ConstantFunctionSymbol[0], issue with case class (has to reimplement).
    
    * back to the "common super type with case classes" structure
    
    * finished predicates, compiles. Connector left
    
    * Finished datastructure. TODO: Underlyings, Arity, uncomment asFront
    
    * Compiles, checked arity and underlyings (mostly)
    
    * Rehabilited asFront. Next stop, Substitution.
    
    * porting unificationUtils
    
    * half of unificationUtils done. Need to make Common even closer structure to kernel (variableFormula extends PredicateFormula)
    
    * progress through unification
    
    * compiles, progressing
    
    * safe for reset
    
    * only applySubst remaining.
    Note: given
    ```scala
    val s: Seq[(Variable, Term)]
    ```
    `s.toMap` crashes dotty. Instead, do `Map(s*)`.
    
    * Substitution done, everything compiles.
    
    * rehabilited commented function
    
    * utils tests compiles and pass.
    
    * Finished setTheorzLibrary, close to finish OLPropositionalSolver
    
    * Quantifiers.scala work, completed BasicProofTactic, implemented printing of terms and formulas
    
    * progress on compilation and run of SetTheory.scala
    
    * ordinals1 works
    
    * Everything works, even example package. Some tests are still commentated. Simplified a couple proofs.
    
    * Small improvements
    
    * Ready for demo
    
    * scalafix, scalafmt
    
    * git add
    
    * Removed unused option in build.sbt, run scalafixAll and scalafmtAll on lisa-examples, add a newline in build.properties
    265ed45e
    History
    Types (#166)
    SimonGuilloud authored
    * Starting a layer of abstraction.
    
    * swrdgv
    
    * sedgf
    
    * ONgoing work. FOL structure mostly implemented, substitutions ongoing.
    
    * continued
    
    * further changes
    
    * LisaObject has a self type being self
    
    * More improvements on substitution
    
    * More work
    
    * multivar substitution
    
    * improvements to MapProofTest
    
    * finished fol, need to do prooflib
    
    * started work on prooflib, cut plenty unused code in Library.scala
    
    * more work on substitutions
    
    * updated WithTheorems
    
    * finished BasicSteptactics and substitutions
    
    * more corrections of tactics using unifier
    
    * fixed F and K imports
    
    * finished PrrofHelpers and definitions. Definitions possibly not final
    
    * Done most of the simpleDeducedSteps
    
    * ongoing work on types
    
    * added doc in Common.scala
    
    * more doc, some simplification
    
    * more doc and simplification of unneeded parts
    
    * fixed some export issues. Commented some tests. translation left for the future.
    
    * remove some debug code
    
    * add missing files
    
    * continue F integration. FInished with Set theory library files, now doing CommonTactics.scala (part is Dario's work).
    
    * simplifier remaining
    
    * renaming and mroe compatibility
    
    * more adaptations
    
    * merge build.sbt
    
    * fixing
    
    * transforming unification to Front
    
    * weird issues with match types and dotty
    
    * Compiles..? Need to simplify use of Arity in formula labels now. Finger crossed.
    
    * add missing files
    
    * still compiles
    
    * Term**0 |-> Term
    
    * Does not compile (dotty crash). Possibly due to covariant schematic labels.
    
    * Labels are contravariant
    
    * Weird "inherits conflicting instances of non-variant base trait LisaObject"
    
    * structure seems to work; Constant extends ConstantFunctionSymbol[0], issue with case class (has to reimplement).
    
    * back to the "common super type with case classes" structure
    
    * finished predicates, compiles. Connector left
    
    * Finished datastructure. TODO: Underlyings, Arity, uncomment asFront
    
    * Compiles, checked arity and underlyings (mostly)
    
    * Rehabilited asFront. Next stop, Substitution.
    
    * porting unificationUtils
    
    * half of unificationUtils done. Need to make Common even closer structure to kernel (variableFormula extends PredicateFormula)
    
    * progress through unification
    
    * compiles, progressing
    
    * safe for reset
    
    * only applySubst remaining.
    Note: given
    ```scala
    val s: Seq[(Variable, Term)]
    ```
    `s.toMap` crashes dotty. Instead, do `Map(s*)`.
    
    * Substitution done, everything compiles.
    
    * rehabilited commented function
    
    * utils tests compiles and pass.
    
    * Finished setTheorzLibrary, close to finish OLPropositionalSolver
    
    * Quantifiers.scala work, completed BasicProofTactic, implemented printing of terms and formulas
    
    * progress on compilation and run of SetTheory.scala
    
    * ordinals1 works
    
    * Everything works, even example package. Some tests are still commentated. Simplified a couple proofs.
    
    * Small improvements
    
    * Ready for demo
    
    * scalafix, scalafmt
    
    * git add
    
    * Removed unused option in build.sbt, run scalafixAll and scalafmtAll on lisa-examples, add a newline in build.properties