changed TYPE_INST of abstractions. Need to extends DEF_REF to elimina…

…te TypeInstAbstractionWithout and TypeInstAbstractionWith.
epfl-lara · Mar 21, 2024 · 4a2e05e · 4a2e05e
1 parent 1da0e3b
commit 4a2e05e
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 2 deletions.
diff --git a/lisa-sets/src/main/scala/lisa/hol/HOLSteps.scala b/lisa-sets/src/main/scala/lisa/hol/HOLSteps.scala
@@ -670,7 +670,9 @@ object HOLSteps extends lisa.HOL {
 
     def apply(using proof: Proof)(x: F.Variable, t:Term, prem: proof.Fact): proof.ProofTacticJudgement = TacticSubproof{
       val r = prem of (x := t)
-      have(r.statement) by Restate.from(r)
+      val s0 = have(r.statement) by Restate.from(r)
+      println("HERE ====================== Calling INST_TYPE")
+      have(DEF_RED.THM(s0))
     }
 
   }
@@ -897,6 +899,10 @@ object HOLSteps extends lisa.HOL {
   object DEF_RED extends ProofTactic {
     def apply(using proof: Proof)(t: Term): proof.ProofTacticJudgement = TacticSubproof{ ip ?=>
       t match
+        case tyaout: TypeInstAbstractionWithout => 
+          ???
+        case tyawith: TypeInstAbstractionWith => 
+          ???
         case ia: InstAbstraction => //  $λ*a*b*c...
           val base = ia.base
           val insts = ia.insts

diff --git a/lisa-sets/src/main/scala/lisa/hol/VarsAndFunctions.scala b/lisa-sets/src/main/scala/lisa/hol/VarsAndFunctions.scala
@@ -383,6 +383,8 @@ object VarsAndFunctions {
 
     override def substituteUnsafe(map: Map[F.SchematicLabel[?], F.LisaObject[?]]): Term = 
       if map.contains(repr) then map(repr).asInstanceOf[Term]
+      else if (defin.freeVariables.exists(v => map.contains(v))) then 
+        TypeInstAbstractionWithout(this, map.asInstanceOf)
       else 
         val newMap = map - bound
         AbstractionClosureWithoutFreeVars(reprId, bound.instType(newMap), body.substituteUnsafe(newMap), defin.substituteUnsafe(newMap).asInstanceOf)
@@ -406,6 +408,8 @@ object VarsAndFunctions {
     val typ = bound.typ |=> defin.outType
     override def substituteUnsafe(map: Map[F.SchematicLabel[?], F.LisaObject[?]]): AppliedFunction = 
       if map.contains(repr) then super.substituteUnsafe(map)
+      else if (defin.freeVariables.exists(v => map.contains(v))) then 
+        TypeInstAbstractionWith(this, map.asInstanceOf)
       else 
         val r = InstAbstraction(this, freeVars.map(v => map.getOrElse(v, v)).asInstanceOf)
         val exp = super.substituteUnsafe(map)
@@ -425,10 +429,21 @@ object VarsAndFunctions {
 
   }
 
+  class TypeInstAbstractionWithout(
+    val base:AbstractionClosureWithoutFreeVars,
+    val typeinst: Map[lisa.fol.FOL.SchematicLabel[?], lisa.fol.FOL.LisaObject[?]]
+  ) extends AbstractionClosureWithoutFreeVars(base.reprId, base.bound.substituteUnsafe(typeinst).asInstanceOf, base.body.substituteUnsafe(typeinst), base.defin.substituteUnsafe(typeinst).asInstanceOf)
+
+  class TypeInstAbstractionWith(
+    val base:AbstractionClosureWithFreeVars,
+    val typeinst: Map[lisa.fol.FOL.SchematicLabel[?], lisa.fol.FOL.LisaObject[?]]
+  ) extends AbstractionClosureWithFreeVars(base.repr.substituteUnsafe(typeinst).asInstanceOf, base.bound.substituteUnsafe(typeinst).asInstanceOf, base.body.substituteUnsafe(typeinst), base.freeVars.asInstanceOf, base.defin.substituteUnsafe(typeinst).asInstanceOf)
+
+
 
   object Abstraction {
 
-    val cache = collection.mutable.ListMap.empty[(F.Identifier, Term, Term), Abstraction & Term]
+    val cache = collection.mutable.HashMap.empty[(F.Identifier, Term, Term), Abstraction & Term]
     def apply(bound: TypedVar, body: Term): Abstraction & Term = {
       cache.getOrElseUpdate((bound.id, bound.typ, body), {
         val freeVars: Seq[TypedVar] = (body.freeVariables - bound).toSeq.sortBy(_.id.name).collect {