Fix abs

.gitignore

@@ -22,3 +22,6 @@ cache
 
 # emacs backup files
 *~
+hol-import/project/project/metals.sbt
+hol-import/project/metals.sbt
+project/project/metals.sbt

build.sbt

@@ -20,7 +20,7 @@ ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports"
 
 
 val commonSettings = Seq(
-  crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
+  crossScalaVersions := Seq("3.3.1"),
   run / fork := true
 )
 
@@ -40,10 +40,11 @@ val commonSettings3 = commonSettings ++ Seq(
     // "-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed
 
   ),
+  javaOptions += "-Xmx10G",
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
   libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0",
   //libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
-  libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
+  // libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
   Test / parallelExecution := false
 )
 
@@ -59,6 +60,8 @@ lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8
 scallion/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
 silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
 
+lazy val holimp = RootProject(file("./hol-import/"))
+
 lazy val root = Project(
     id = "lisa",
     base = file(".")
@@ -81,6 +84,7 @@ lazy val sets = Project(
   base = file("lisa-sets")
 )
   .settings(commonSettings3)
+  .dependsOn(holimp)
   .dependsOn(kernel, withTests(utils))
 
 lazy val utils = Project(

hol-import/build.sbt

@@ -0,0 +1,14 @@
+val scala3Version = "3.3.1"
+
+lazy val root = project
+  .in(file("."))
+  .settings(
+    name := "holimp",
+    version := "0.1.0-SNAPSHOT",
+
+    scalaVersion := scala3Version,
+
+    libraryDependencies += "org.scalameta" %% "munit" % "0.7.29" % Test,
+    libraryDependencies += "com.lihaoyi" %% "upickle" % "3.2.0",
+    libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0"
+  )

hol-import/project/build.properties

@@ -0,0 +1 @@
+sbt.version=1.9.9

hol-import/src/main/scala/holimp/Core.scala

@@ -0,0 +1,67 @@
+package holimp
+
+import java.awt.Window.Type
+
+object Core:
+
+  case class ApplicationOnNonFunctionException(term: Term) extends Exception(s"Constructed a term applying to a non-function.\n\tTerm: $term")
+
+  sealed trait Type
+  case class TypeVariable(name: String) extends Type
+  case class TypeApplication(name: String, args: List[Type]) extends Type
+
+  val BoolType = TypeApplication("bool", Nil)
+
+  object FunType:
+    def apply(in: Type, out: Type): Type = 
+      TypeApplication("fun", List(in, out))
+    def unapply(t: Type): Option[(Type, Type)] =
+      t match
+        case TypeApplication("fun", List(in, out)) => Some((in, out))
+        case  _ => None
+
+  sealed trait Term:
+    def tpe: Type
+
+  case class Variable(name: String, tpe: Type) extends Term
+  case class Constant(name: String, tpe: Type) extends Term
+  case class Combination(left: Term, right: Term) extends Term:
+    def tpe: Type = 
+      left.tpe match
+        case FunType(_, out) => out
+        case _ => throw ApplicationOnNonFunctionException(this)
+
+  case class Abstraction(absVar: Variable, inner: Term) extends Term:
+    def tpe: Type = 
+      FunType(absVar.tpe, inner.tpe)
+
+  sealed trait ProofStep
+  case class REFL(term: Term) extends ProofStep
+  case class TRANS(left: ProofStep, right: ProofStep) extends ProofStep
+  case class MK_COMB(left: ProofStep, right: ProofStep) extends ProofStep
+  case class ABS(absVar: Variable, from: ProofStep) extends ProofStep
+  case class BETA(term: Term) extends ProofStep
+  case class ASSUME(term: Term) extends ProofStep
+  case class EQ_MP(left: ProofStep, right: ProofStep) extends ProofStep
+  case class DEDUCT_ANTISYM_RULE(left: ProofStep, right: ProofStep) extends ProofStep
+  case class INST(from: ProofStep, insts: Map[Variable, Term]) extends ProofStep
+  case class INST_TYPE(from: ProofStep, insts: Map[TypeVariable, Type]) extends ProofStep
+  case class AXIOM(term: Term) extends ProofStep
+  case class DEFINITION(name: String, term: Term) extends ProofStep
+  case class TYPE_DEFINITION(name: String, term: Term, just: ProofStep) extends ProofStep
+
+  extension (t : Type) def pretty: String =
+    t match
+      case BoolType => "B"
+      case FunType(from, to) => s"(${from.pretty} => ${to.pretty})"
+      case TypeVariable(name) => name
+      case TypeApplication(name, args) => s"$name[${args.mkString(", ")}]"
+
+  extension (t: Term) def pretty: String =
+    t match
+      case Variable(name, tpe) => s"$name : ${tpe.pretty}"
+      case Constant(name, tpe) => s"$name : ${tpe.pretty}"
+      case Combination(left, right) => s"(${left.pretty}) (${right.pretty})"
+      case Abstraction(absVar, inner) => s"\\${absVar.pretty}. ${inner.pretty}"    
+
+end Core

hol-import/src/main/scala/holimp/Main.scala

@@ -0,0 +1,94 @@
+package holimp
+
+import Core.*
+import upickle.default.{ReadWriter => RW, *}
+import Parser._
+import upickle.default
+import java.io.File
+
+object JSONParser:
+  case class SplitProofStep(name: String, dep1: Int, dep2: Int, strdep: String, termdep: String, termsdeps: List[List[String]], typesdeps: List[List[String]])
+
+  case class RawStep(id: Int, pr: SplitProofStep)
+
+  given rws: RW[SplitProofStep] = macroRW 
+  given rw: RW[RawStep] = macroRW 
+
+  val fileBase = "/home/sguilloud/Lisa/lisa/proofs/prooftrace2"
+
+  def readJSON(file: File) = 
+    read[Array[RawStep]](file)
+
+  case class UnknownProofStepException(name: String) extends Exception
+  case class CouldNotParseException(msg: String, next: String) extends Exception(s"Could not parse\n\tMessage: $msg\n\tNext: $next")
+  case object IncompleteParsingException extends Exception
+  case object UnreachableCaseException extends Exception
+
+
+  extension [T] (res: ParseResult[T])
+    def getDone =
+      res match
+        case Success(out, next) if next.atEnd => out
+        case Success(_, _) => throw IncompleteParsingException
+        case NoSuccess(msg, next) => throw CouldNotParseException(msg, next.toString())
+        case _ => throw UnreachableCaseException
+
+
+  def parseTerm(str: String): Term = parse(term, str).getDone
+
+  def parseAsVar(str: String): Variable = parse(variable, str).getDone
+
+  def parseInst(insts: List[List[String]]): Map[Variable, Term] = 
+    insts.map{ case List(left, right) => parseAsVar(left) -> parseTerm(right); case _ => throw UnreachableCaseException}.toMap
+
+  def parseTypeInst(insts: List[List[String]]): Map[TypeVariable, Type] = 
+    def parseAsTVar(str: String) = parse(typeVariable, str).getDone
+    def parseType(str: String) = parse(typ, str).getDone
+    insts.map{ case List(left, right) => parseAsTVar(left) -> parseType(right); case _ => throw UnreachableCaseException}.toMap
+
+
+  val stepDict = Map.empty[Int, ProofStep]
+
+  def processSplitStep(step: SplitProofStep, map: Map[Int, ProofStep]): ProofStep = 
+    step.name match
+      case "REFL" => REFL(parseTerm(step.termdep))
+      case "TRANS" => TRANS(map(step.dep1), map(step.dep2))
+      case "MK_COMB" => MK_COMB(map(step.dep1), map(step.dep2))
+      case "ABS" => ABS(parseAsVar(step.termdep), map(step.dep1))
+      case "BETA" => BETA(parseTerm(step.termdep))
+      case "ASSUME" => ASSUME(parseTerm(step.termdep))
+      case "EQ_MP" => EQ_MP(map(step.dep1), map(step.dep2))
+      case "DEDUCT_ANTISYM_RULE" => DEDUCT_ANTISYM_RULE(map(step.dep1), map(step.dep2))
+      case "INST" => INST(map(step.dep1), parseInst(step.termsdeps))
+      case "INST_TYPE" => INST_TYPE(map(step.dep1), parseTypeInst(step.typesdeps))
+      case "AXIOM" => AXIOM(parseTerm(step.termdep))
+      case "DEFINITION" => DEFINITION(step.strdep, parseTerm(step.termdep))
+      case "TYPE_DEFINITION" => TYPE_DEFINITION(step.strdep, parseTerm(step.termdep), map(step.dep1))
+      case _ => throw UnknownProofStepException(step.name)
+
+
+  def getProofs =
+    val rawSteps = readJSON(File(s"$fileBase.proofs"))
+    val mapped = rawSteps.foldLeft(Map.empty[Int, ProofStep]) { case (map, RawStep(i, step)) =>
+      val readStep = processSplitStep(step, map)
+      map + (i -> readStep)
+    }
+    mapped
+
+  case class TheoremRef(id: Int, nm: String)
+
+  def getTheorems =
+    given rwt: RW[TheoremRef] = macroRW
+    read[List[TheoremRef]](File(s"$fileBase.names"))
+
+  def getStatements =
+    case class Sequent(hy: List[String], cc: String)
+    case class TheoremStatement(id: Int, th: Sequent)
+    given rwns: RW[Sequent] = macroRW
+    given rwn: RW[TheoremStatement] = macroRW
+    read[Array[TheoremStatement]](File(s"$fileBase.theorems")).map(th => th.id -> (th.th.hy.map(parseTerm), parseTerm(th.th.cc))).toMap
+
+@main def hello(): Unit =
+  // val m = JSONParser.getProofs
+  val thm = JSONParser.getStatements(188)
+  println(thm._2.pretty)

hol-import/src/main/scala/holimp/Parser.scala

@@ -0,0 +1,25 @@
+package holimp
+
+import Core.*
+import scala.util.parsing.combinator.*
+
+object Parser extends RegexParsers:
+    type Identifier = String
+
+    def isParen(c: Char): Boolean = c == '[' || c == ']' || c == '(' || c == ')'
+
+    def char: Parser[Char] = acceptIf(!isParen(_))(el => s"Unexpected: $el")
+    def identifier: Parser[Identifier] = rep1(char) ^^ {_.mkString}
+    def typ: Parser[Type] = typeVariable ||| typeApplication
+    def term: Parser[Term] = variable ||| constant ||| combination ||| abstraction
+
+    def variable: Parser[Variable] = "v(" ~ identifier ~ ")(" ~ typ ~ ")" ^^ { case _ ~ id ~ _ ~ tp ~ _ => Variable(id, tp) }
+    def constant: Parser[Constant] = "c(" ~ identifier ~ ")(" ~ typ ~ ")" ^^ { case _ ~ id ~ _ ~ tp ~ _ => Constant(id, tp) }
+    def combination: Parser[Combination] = "C(" ~ term ~ ")(" ~ term ~ ")" ^^ { case _ ~ t1 ~ _ ~ t2 ~ _ => Combination(t1, t2) }
+    def abstraction: Parser[Abstraction] = "A(" ~ variable ~ ")(" ~ term ~ ")" ^^ { case _ ~ v ~ _ ~ tm ~ _ => Abstraction(v, tm) }
+
+    def typeVariable: Parser[TypeVariable] = "t[" ~ identifier ~ "]" ^^ { case _ ~ id ~ _ => TypeVariable(id)}
+    def typeApplication: Parser[TypeApplication] = "T[" ~ identifier ~ "][" ~ rep(typeArg) ~ "]" ^^ { case _ ~ id ~ _ ~ args ~ _ => TypeApplication(id, args) }
+    def typeArg: Parser[Type] = "[" ~ typ ~ "]" ^^ { case _ ~ tp ~ _ => tp}
+
+end Parser

hol-import/src/main/scala/import.sc

@@ -0,0 +1,94 @@
+//> using dep "com.lihaoyi::upickle:3.2.0"
+
+object Core:
+
+  case class ApplicationOnNonFunctionException(term: Term) extends Exception(s"Constructed a term applying to a non-function.\n\tTerm: $term")
+
+  sealed trait Type
+  case object Unit extends Type
+  case object Bool extends Type
+  case object Ind extends Type
+  case class Func(inputType: Type, outputType: Type) extends Type
+  case class TypeVariable(name: String) extends Type
+  case class CustomType(name:String) extends Type
+
+  sealed trait Term:
+    def tpe: Type
+  case class Variable(name: String, tpe: Type) extends Term
+  case class Abstraction(x: Variable, inner: Term) extends Term:
+    def tpe: Type = Func(x.tpe, inner.tpe)
+  case class Application(fun: Term, arg: Term) extends Term:
+    def tpe: Type = 
+      fun.tpe match
+        case Func(inputType, outputType) => outputType
+        case _ => throw ApplicationOnNonFunctionException(this)
+  case class Constant(name: String, tpe: Type, paramTypes: List[TypeVariable]) extends Term
+end Core
+
+import Core.*
+
+import upickle.default.*
+import upickle.default.{ReadWriter => RW, macroRW}
+
+case class SplitProofStep(name: String, dep1: Int, dep2: Int, strdep: String, termdep: String, termsdeps: List[List[String]], typesdeps: List[List[String]])
+
+case class RawStep(id: Int, pr: SplitProofStep)
+
+given rws: RW[SplitProofStep] = macroRW 
+given rw: RW[RawStep] = macroRW 
+
+sealed trait ProofStep
+case class REFL(term: Term) extends ProofStep
+case class TRANS(left: ProofStep, right: ProofStep) extends ProofStep
+case class MK_COMB(left: ProofStep, right: ProofStep) extends ProofStep
+case class ABS(absVar: Variable, from: ProofStep) extends ProofStep
+case class BETA(from: ProofStep) extends ProofStep
+case class ASSUME(term: Term) extends ProofStep
+case class EQ_MP(left: ProofStep, right: ProofStep) extends ProofStep
+case class DEDUCT_ANTISYM_RULE(left: ProofStep, right: ProofStep) extends ProofStep
+case class INST(from: ProofStep, insts: Map[Variable, Term]) extends ProofStep
+case class INST_TYPE(from: ProofStep, insts: Map[TypeVariable, Type]) extends ProofStep
+case class AXIOM(term: Term) extends ProofStep
+case class DEFINITION(name: String, term: Term) extends ProofStep
+case class TYPE_DEFINITION(name: String, term: Term, just: ProofStep) extends ProofStep
+
+case class UnknownProofStepException(name: String) extends Exception
+
+def parseTerm(str: String): Term = 
+  def rec(str: String): Option[Term] =
+    val leading = str(0) 
+    ???
+  rec(str).get
+
+def parseAsVar(str: String): Variable = ???
+
+def parseInst(insts: List[List[String]]): Map[Variable, Term] = ???
+
+def parseTypeInst(insts: List[List[String]]): Map[TypeVariable, Type] = ???
+
+val stepDict = Map.empty[Int, ProofStep]
+
+def processSplitStep(using map: Map[Int, ProofStep])(step: SplitProofStep): ProofStep = 
+  step.name match
+    case "REFL" => REFL(parseTerm(step.termdep))
+    case "TRANS" => TRANS(map(step.dep1), map(step.dep2))
+    case "MK_COMB" => MK_COMB(map(step.dep1), map(step.dep2))
+    case "ABS" => ABS(parseAsVar(step.termdep), map(step.dep1))
+    case "BETA" => BETA(map(step.dep1))
+    case "ASSUME" => ASSUME(parseTerm(step.termdep))
+    case "EQ_MP" => EQ_MP(map(step.dep1), map(step.dep2))
+    case "DEDUCT_ANTISYM_RULE" => DEDUCT_ANTISYM_RULE(map(step.dep1), map(step.dep2))
+    case "INST" => INST(map(step.dep1), parseInst(step.termsdeps))
+    case "INST_TYPE" => INST_TYPE(map(step.dep1), parseTypeInst(step.typesdeps))
+    case "AXIOM" => AXIOM(parseTerm(step.termdep))
+    case "DEFINITION" => DEFINITION(step.strdep, parseTerm(step.termdep))
+    case "TYPE_DEFINITION" => TYPE_DEFINITION(step.strdep, parseTerm(step.termdep), map(step.dep1))
+    case _ => throw UnknownProofStepException(step.name)
+
+val rawSteps = read[Array[RawStep]](java.io.File("new.proofs"))
+val mapped = rawSteps.foldLeft(stepDict) { case (map, RawStep(i, step)) =>
+  val readStep = processSplitStep(using map)(step)
+  map + (i -> readStep)
+}
+println(mapped)
+

lisa-examples/src/main/scala/Test.scala

@@ -1,3 +1,4 @@
+import lisa.maths.settheory.types.TypeLib.|=>
 
 object Test extends lisa.Main {
 
@@ -53,5 +54,37 @@ object Test extends lisa.Main {
     have(thesis) by Restate.from(ax of (c, d, P := ===))
     showCurrentProof()
   }
+/*
+  {
+    val A = variable
+    val B = variable
+    val app = function[2]
+    val f = variable
+    val g = variable
+    val x = variable
+    val y = variable
+    val thm5 = Theorem(() |- ()) {
+      val s1 = have((f ∈ A, x ∈ B) |- (app(f, x) === app(f, x))) by Sorry
+      val s2 = have((f ∈ A, g ∈ A) |- (f===g)) by Sorry
+      val s3 = have((x ∈ B, y ∈ B) |- (x===y)) by Sorry
+      have((x ∈ B, y ∈ B, f ∈ A, g ∈ A) |- (app(f, x) === app(g, y))) by Substitution.ApplyRules(s2, s3)(s1)
+    }
+  }
+*/
+
+/*
+  {
+    val f = function[1]
+    val x = variable
+    val y = variable
+    val P = formulaVariable
+    val Q = predicate[1]
+    val thm6 = Theorem(() |- ()) {
+      val s1 = have (P |- (f(x) === f(y)) ) by Sorry
+      assume(Q(f(x)))
+      thenHave( Q(f(y)) ) by Substitution.ApplyRules(s1)
+    }
+  }
+  */
 
 }