support for (fully reconstructed) proof terms in Scala;
authorwenzelm
Thu Aug 15 16:02:47 2019 +0200 (7 months ago)
changeset 70533031620901fcd
parent 70531 2d2b5a8e8d59
child 70534 fb876ebbf5a7
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
src/Pure/term.scala
src/Pure/term_xml.scala
     1.1 --- a/src/Pure/term.scala	Wed Aug 14 19:50:23 2019 +0200
     1.2 +++ b/src/Pure/term.scala	Thu Aug 15 16:02:47 2019 +0200
     1.3 @@ -32,6 +32,19 @@
     1.4    case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
     1.5    case class App(fun: Term, arg: Term) extends Term
     1.6  
     1.7 +  sealed abstract class Proof
     1.8 +  case object MinProof extends Proof
     1.9 +  case class PBound(index: Int) extends Proof
    1.10 +  case class Abst(name: String, typ: Typ, body: Proof) extends Proof
    1.11 +  case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
    1.12 +  case class Appt(fun: Proof, arg: Term) extends Proof
    1.13 +  case class AppP(fun: Proof, arg: Proof) extends Proof
    1.14 +  case class Hyp(hyp: Term) extends Proof
    1.15 +  case class PAxm(name: String, types: List[Typ]) extends Proof
    1.16 +  case class OfClass(typ: Typ, cls: String) extends Proof
    1.17 +  case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
    1.18 +  case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof
    1.19 +
    1.20  
    1.21    /* Pure logic */
    1.22  
    1.23 @@ -101,13 +114,24 @@
    1.24            case Some(y) => y
    1.25            case None =>
    1.26              x match {
    1.27 -              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
    1.28 +              case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
    1.29                case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
    1.30                case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
    1.31              }
    1.32          }
    1.33      }
    1.34  
    1.35 +    protected def cache_typs(x: List[Typ]): List[Typ] =
    1.36 +    {
    1.37 +      if (x.isEmpty) Nil
    1.38 +      else {
    1.39 +        lookup(x) match {
    1.40 +          case Some(y) => y
    1.41 +          case None => store(x.map(cache_typ(_)))
    1.42 +        }
    1.43 +      }
    1.44 +    }
    1.45 +
    1.46      protected def cache_term(x: Term): Term =
    1.47      {
    1.48        lookup(x) match {
    1.49 @@ -125,11 +149,38 @@
    1.50        }
    1.51      }
    1.52  
    1.53 +    protected def cache_proof(x: Proof): Proof =
    1.54 +    {
    1.55 +      if (x == MinProof) MinProof
    1.56 +      else {
    1.57 +        lookup(x) match {
    1.58 +          case Some(y) => y
    1.59 +          case None =>
    1.60 +            x match {
    1.61 +              case MinProof => x
    1.62 +              case PBound(index) => store(PBound(cache_int(index)))
    1.63 +              case Abst(name, typ, body) =>
    1.64 +                store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
    1.65 +              case AbsP(name, hyp, body) =>
    1.66 +                store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
    1.67 +              case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
    1.68 +              case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
    1.69 +              case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
    1.70 +              case Oracle(name, prop, types) =>
    1.71 +                store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
    1.72 +              case PThm(serial, name, types) =>
    1.73 +                store(PThm(serial, cache_string(name), cache_typs(types)))
    1.74 +            }
    1.75 +        }
    1.76 +      }
    1.77 +    }
    1.78 +
    1.79      // main methods
    1.80      def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
    1.81      def sort(x: Sort): Sort = synchronized { cache_sort(x) }
    1.82      def typ(x: Typ): Typ = synchronized { cache_typ(x) }
    1.83      def term(x: Term): Term = synchronized { cache_term(x) }
    1.84 +    def proof(x: Proof): Proof = synchronized { cache_proof(x) }
    1.85  
    1.86      def position(x: Position.T): Position.T =
    1.87        synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
     2.1 --- a/src/Pure/term_xml.scala	Wed Aug 14 19:50:23 2019 +0200
     2.2 +++ b/src/Pure/term_xml.scala	Thu Aug 15 16:02:47 2019 +0200
     2.3 @@ -53,5 +53,19 @@
     2.4          { case (List(a), Nil) => Bound(int_atom(a)) },
     2.5          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
     2.6          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
     2.7 +
     2.8 +    def proof: T[Proof] =
     2.9 +      variant[Proof](List(
    2.10 +        { case (Nil, Nil) => MinProof },
    2.11 +        { case (List(a), Nil) => PBound(int_atom(a)) },
    2.12 +        { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
    2.13 +        { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
    2.14 +        { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
    2.15 +        { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
    2.16 +        { case (Nil, a) => Hyp(term(a)) },
    2.17 +        { case (List(a), b) => PAxm(a, list(typ)(b)) },
    2.18 +        { case (List(a), b) => OfClass(typ(b), a) },
    2.19 +        { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
    2.20 +        { case (List(a, b), c) => PThm(long_atom(a), b, list(typ)(c)) }))
    2.21    }
    2.22  }