Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Types #166

Merged
merged 75 commits into from
Oct 5, 2023
Merged

Types #166

merged 75 commits into from
Oct 5, 2023

Commits on Apr 14, 2023

  1. Starting a layer of abstraction.

    @SimonGuilloud
    SimonGuilloud committed Apr 14, 2023
    Configuration menu
    Copy the full SHA
    dbe7796 View commit details
    Browse the repository at this point in the history

Commits on Apr 24, 2023

  1. swrdgv

    @SimonGuilloud
    SimonGuilloud committed Apr 24, 2023
    Configuration menu
    Copy the full SHA
    6c042fa View commit details
    Browse the repository at this point in the history

  2. sedgf

    @SimonGuilloud
    SimonGuilloud committed Apr 24, 2023
    Configuration menu
    Copy the full SHA
    d520029 View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2023

  1. ONgoing work. FOL structure mostly implemented, substitutions ongoing.

    @SimonGuilloud
    SimonGuilloud committed Apr 25, 2023
    Configuration menu
    Copy the full SHA
    c65fb35 View commit details
    Browse the repository at this point in the history

  2. continued

    @SimonGuilloud
    SimonGuilloud committed Apr 25, 2023
    Configuration menu
    Copy the full SHA
    0ce9761 View commit details
    Browse the repository at this point in the history

Commits on Apr 26, 2023

  1. further changes

    @SimonGuilloud
    SimonGuilloud committed Apr 26, 2023
    Configuration menu
    Copy the full SHA
    9ccb586 View commit details
    Browse the repository at this point in the history

  2. LisaObject has a self type being self

    @SimonGuilloud
    SimonGuilloud committed Apr 26, 2023
    Configuration menu
    Copy the full SHA
    68736bd View commit details
    Browse the repository at this point in the history

Commits on Apr 27, 2023

  1. More improvements on substitution

    @SimonGuilloud
    SimonGuilloud committed Apr 27, 2023
    Configuration menu
    Copy the full SHA
    ddae31e View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2023

  1. More work

    @SimonGuilloud
    SimonGuilloud committed Apr 28, 2023
    Configuration menu
    Copy the full SHA
    5c845e5 View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2023

  1. multivar substitution

    @SimonGuilloud
    SimonGuilloud committed Apr 30, 2023
    Configuration menu
    Copy the full SHA
    a836795 View commit details
    Browse the repository at this point in the history

Commits on May 2, 2023

  1. improvements to MapProofTest

    @SimonGuilloud
    SimonGuilloud committed May 2, 2023
    Configuration menu
    Copy the full SHA
    bb6c1eb View commit details
    Browse the repository at this point in the history

Commits on May 7, 2023

  1. finished fol, need to do prooflib

    @SimonGuilloud
    SimonGuilloud committed May 7, 2023
    Configuration menu
    Copy the full SHA
    c4d7e94 View commit details
    Browse the repository at this point in the history

  2. started work on prooflib, cut plenty unused code in Library.scala

    @SimonGuilloud
    SimonGuilloud committed May 7, 2023
    Configuration menu
    Copy the full SHA
    080d045 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'cmain' into types

    @SimonGuilloud
    SimonGuilloud committed May 7, 2023
    Configuration menu
    Copy the full SHA
    0900263 View commit details
    Browse the repository at this point in the history

Commits on May 8, 2023

  1. more work on substitutions

    @SimonGuilloud
    SimonGuilloud committed May 8, 2023
    Configuration menu
    Copy the full SHA
    f55a856 View commit details
    Browse the repository at this point in the history

  2. updated WithTheorems

    @SimonGuilloud
    SimonGuilloud committed May 8, 2023
    Configuration menu
    Copy the full SHA
    1103c1c View commit details
    Browse the repository at this point in the history

Commits on May 9, 2023

  1. finished BasicSteptactics and substitutions

    @SimonGuilloud
    SimonGuilloud committed May 9, 2023
    Configuration menu
    Copy the full SHA
    a52e24d View commit details
    Browse the repository at this point in the history

  2. more corrections of tactics using unifier

    @SimonGuilloud
    SimonGuilloud committed May 9, 2023
    Configuration menu
    Copy the full SHA
    c317eca View commit details
    Browse the repository at this point in the history

Commits on May 12, 2023

  1. fixed F and K imports

    @SimonGuilloud
    SimonGuilloud committed May 12, 2023
    Configuration menu
    Copy the full SHA
    5603e26 View commit details
    Browse the repository at this point in the history

Commits on May 14, 2023

  1. finished PrrofHelpers and definitions. Definitions possibly not final

    @SimonGuilloud
    SimonGuilloud committed May 14, 2023
    Configuration menu
    Copy the full SHA
    dddaf6b View commit details
    Browse the repository at this point in the history

Commits on May 25, 2023

  1. Done most of the simpleDeducedSteps

    @SimonGuilloud
    SimonGuilloud committed May 25, 2023
    Configuration menu
    Copy the full SHA
    99286a1 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'cmain' into types

    @SimonGuilloud
    SimonGuilloud committed May 25, 2023
    Configuration menu
    Copy the full SHA
    f1f977e View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. ongoing work on types

    @SimonGuilloud
    SimonGuilloud committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    88ff893 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2023

  1. Merge branch 'main' into types

    @SimonGuilloud
    SimonGuilloud committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    0a1a296 View commit details
    Browse the repository at this point in the history

  2. added doc in Common.scala

    @SimonGuilloud
    SimonGuilloud committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    fd65fc7 View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2023

  1. more doc, some simplification

    @SimonGuilloud
    SimonGuilloud committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    1b5cc63 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into types

    @SimonGuilloud
    SimonGuilloud committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    6f8c234 View commit details
    Browse the repository at this point in the history

  3. more doc and simplification of unneeded parts

    @SimonGuilloud
    SimonGuilloud committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    746915b View commit details
    Browse the repository at this point in the history

  4. fixed some export issues. Commented some tests. translation left for … 

    …the future.
    @SimonGuilloud
    SimonGuilloud committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    1981033 View commit details
    Browse the repository at this point in the history

  5. remove some debug code

    @SimonGuilloud
    SimonGuilloud committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    7533316 View commit details
    Browse the repository at this point in the history

  6. add missing files

    @SimonGuilloud
    SimonGuilloud committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    4c1c261 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2023

  1. continue F integration. FInished with Set theory library files, now d… 

    …oing CommonTactics.scala (part is Dario's work).
    @SimonGuilloud
    SimonGuilloud committed Aug 11, 2023
    Configuration menu
    Copy the full SHA
    02c1a3e View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2023

  1. simplifier remaining

    @SimonGuilloud
    SimonGuilloud committed Aug 14, 2023
    Configuration menu
    Copy the full SHA
    666009a View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2023

  1. renaming and mroe compatibility

    @SimonGuilloud
    SimonGuilloud committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    8403076 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into types

    @SimonGuilloud
    SimonGuilloud committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    955819d View commit details
    Browse the repository at this point in the history

  3. more adaptations

    @SimonGuilloud
    SimonGuilloud committed Aug 15, 2023
    Configuration menu
    Copy the full SHA
    6a45376 View commit details
    Browse the repository at this point in the history

Commits on Sep 11, 2023

  1. Merge branch 'main' into types

    @SimonGuilloud
    SimonGuilloud committed Sep 11, 2023
    Configuration menu
    Copy the full SHA
    be7137e View commit details
    Browse the repository at this point in the history

  2. merge build.sbt

    @SimonGuilloud
    SimonGuilloud committed Sep 11, 2023
    Configuration menu
    Copy the full SHA
    8fd8d72 View commit details
    Browse the repository at this point in the history

  3. fixing

    @SimonGuilloud
    SimonGuilloud committed Sep 11, 2023
    Configuration menu
    Copy the full SHA
    8a3a004 View commit details
    Browse the repository at this point in the history

  4. transforming unification to Front

    @SimonGuilloud
    SimonGuilloud committed Sep 11, 2023
    Configuration menu
    Copy the full SHA
    dd475e2 View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2023

  1. weird issues with match types and dotty

    @SimonGuilloud
    SimonGuilloud committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    a8af5a7 View commit details
    Browse the repository at this point in the history

  2. Compiles..? Need to simplify use of Arity in formula labels now. Fing… 

    …er crossed.
    @SimonGuilloud
    SimonGuilloud committed Sep 12, 2023
    Configuration menu
    Copy the full SHA
    c4c5d62 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2023

  1. add missing files

    @SimonGuilloud
    SimonGuilloud committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    c0cdbee View commit details
    Browse the repository at this point in the history

  2. still compiles

    @SimonGuilloud
    SimonGuilloud committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    da9147f View commit details
    Browse the repository at this point in the history

  3. Term**0 |-> Term

    @SimonGuilloud
    SimonGuilloud committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    2462f04 View commit details
    Browse the repository at this point in the history

  4. Does not compile (dotty crash). Possibly due to covariant schematic l… 

    …abels.
    @SimonGuilloud
    SimonGuilloud committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    af5b029 View commit details
    Browse the repository at this point in the history

  5. Labels are contravariant

    @SimonGuilloud
    SimonGuilloud committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    bc2c143 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'types' into types2

    @SimonGuilloud
    SimonGuilloud committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    f561156 View commit details
    Browse the repository at this point in the history

Commits on Sep 14, 2023

  1. Weird "inherits conflicting instances of non-variant base trait LisaO… 

    …bject"
    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    a32bc3b View commit details
    Browse the repository at this point in the history

  2. structure seems to work; Constant extends ConstantFunctionSymbol[0], … 

    …issue with case class (has to reimplement).
    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    45bd1af View commit details
    Browse the repository at this point in the history

  3. back to the "common super type with case classes" structure

    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    061e768 View commit details
    Browse the repository at this point in the history

  4. finished predicates, compiles. Connector left

    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    70b812e View commit details
    Browse the repository at this point in the history

  5. Finished datastructure. TODO: Underlyings, Arity, uncomment asFront

    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    bb7ab9a View commit details
    Browse the repository at this point in the history

  6. Compiles, checked arity and underlyings (mostly)

    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    93804f0 View commit details
    Browse the repository at this point in the history

  7. Rehabilited asFront. Next stop, Substitution.

    @SimonGuilloud
    SimonGuilloud committed Sep 14, 2023
    Configuration menu
    Copy the full SHA
    c604056 View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2023

  1. Merge branch 'main' into types2

    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    e4a38c4 View commit details
    Browse the repository at this point in the history

  2. porting unificationUtils

    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    3965dff View commit details
    Browse the repository at this point in the history

  3. half of unificationUtils done. Need to make Common even closer struct… 

    …ure to kernel (variableFormula extends PredicateFormula)
    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    fb98f77 View commit details
    Browse the repository at this point in the history

  4. progress through unification

    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    f1789ff View commit details
    Browse the repository at this point in the history

  5. compiles, progressing

    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    ea8c761 View commit details
    Browse the repository at this point in the history

  6. safe for reset

    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    4c30a17 View commit details
    Browse the repository at this point in the history

  7. only applySubst remaining. 

    Note: given
```scala
val s: Seq[(Variable, Term)]
```
`s.toMap` crashes dotty. Instead, do `Map(s*)`.
    @SimonGuilloud
    SimonGuilloud committed Sep 15, 2023
    Configuration menu
    Copy the full SHA
    51be8a9 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2023

  1. Substitution done, everything compiles.

    @SimonGuilloud
    SimonGuilloud committed Sep 16, 2023
    Configuration menu
    Copy the full SHA
    5637954 View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2023

  1. rehabilited commented function

    @SimonGuilloud
    SimonGuilloud committed Sep 17, 2023
    Configuration menu
    Copy the full SHA
    1eaf18a View commit details
    Browse the repository at this point in the history

  2. utils tests compiles and pass.

    @SimonGuilloud
    SimonGuilloud committed Sep 17, 2023
    Configuration menu
    Copy the full SHA
    70e66a2 View commit details
    Browse the repository at this point in the history

  3. Finished setTheorzLibrary, close to finish OLPropositionalSolver

    @SimonGuilloud
    SimonGuilloud committed Sep 17, 2023
    Configuration menu
    Copy the full SHA
    c6deaa2 View commit details
    Browse the repository at this point in the history

  4. Quantifiers.scala work, completed BasicProofTactic, implemented print… 

    …ing of terms and formulas
    @SimonGuilloud
    SimonGuilloud committed Sep 17, 2023
    Configuration menu
    Copy the full SHA
    1d416e3 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2023

  1. progress on compilation and run of SetTheory.scala

    @SimonGuilloud
    SimonGuilloud committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    e37e263 View commit details
    Browse the repository at this point in the history

  2. ordinals1 works

    @SimonGuilloud
    SimonGuilloud committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    acc0aeb View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2023

  1. Everything works, even example package. Some tests are still commenta… 

    …ted. Simplified a couple proofs.
    @SimonGuilloud
    SimonGuilloud committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    f7851cd View commit details
    Browse the repository at this point in the history

  2. Small improvements

    @SimonGuilloud
    SimonGuilloud committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    f4fd66f View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2023

  1. Ready for demo

    @SimonGuilloud
    SimonGuilloud committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    656bec8 View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2023

  1. scalafix, scalafmt

    @SimonGuilloud
    SimonGuilloud committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    ae8c694 View commit details
    Browse the repository at this point in the history

  2. git add

    @SimonGuilloud
    SimonGuilloud committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    06c5fe9 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2023

  1. Removed unused option in build.sbt, run scalafixAll and scalafmtAll o… 

    …n lisa-examples, add a newline in build.properties
    @SimonGuilloud
    SimonGuilloud committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    40d6e65 View commit details
    Browse the repository at this point in the history