1/* Title: Pure/term.scala 2 Author: Makarius 3 4Lambda terms, types, sorts. 5 6Note: Isabelle/ML is the primary environment for logical operations. 7*/ 8 9package isabelle 10 11 12object Term 13{ 14 /* types and terms */ 15 16 sealed case class Indexname(name: String, index: Int = 0) 17 { 18 override def toString: String = 19 if (index == -1) name 20 else { 21 val dot = 22 Symbol.explode(name).reverse match { 23 case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false 24 case c :: _ => Symbol.is_digit(c) 25 case _ => true 26 } 27 if (dot) "?" + name + "." + index 28 else if (index != 0) "?" + name + index 29 else "?" + name 30 } 31 } 32 33 type Class = String 34 type Sort = List[Class] 35 36 sealed abstract class Typ 37 case class Type(name: String, args: List[Typ] = Nil) extends Typ 38 { 39 override def toString: String = 40 if (this == dummyT) "_" 41 else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")" 42 } 43 case class TFree(name: String, sort: Sort = Nil) extends Typ 44 { 45 override def toString: String = 46 "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")" 47 } 48 case class TVar(name: Indexname, sort: Sort = Nil) extends Typ 49 { 50 override def toString: String = 51 "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")" 52 } 53 val dummyT = Type("dummy") 54 55 sealed abstract class Term 56 { 57 def head: Term = 58 this match { 59 case App(fun, _) => fun.head 60 case _ => this 61 } 62 } 63 case class Const(name: String, typargs: List[Typ] = Nil) extends Term 64 { 65 override def toString: String = 66 if (this == dummy) "_" 67 else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")" 68 } 69 case class Free(name: String, typ: Typ = dummyT) extends Term 70 { 71 override def toString: String = 72 "Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")" 73 } 74 case class Var(name: Indexname, typ: Typ = dummyT) extends Term 75 { 76 override def toString: String = 77 "Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")" 78 } 79 case class Bound(index: Int) extends Term 80 case class Abs(name: String, typ: Typ, body: Term) extends Term 81 case class App(fun: Term, arg: Term) extends Term 82 { 83 override def toString: String = 84 this match { 85 case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")" 86 case _ => "App(" + fun + "," + arg + ")" 87 } 88 } 89 90 def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty)) 91 val dummy: Term = dummy_pattern(dummyT) 92 93 sealed abstract class Proof 94 case object MinProof extends Proof 95 case class PBound(index: Int) extends Proof 96 case class Abst(name: String, typ: Typ, body: Proof) extends Proof 97 case class AbsP(name: String, hyp: Term, body: Proof) extends Proof 98 case class Appt(fun: Proof, arg: Term) extends Proof 99 case class AppP(fun: Proof, arg: Proof) extends Proof 100 case class Hyp(hyp: Term) extends Proof 101 case class PAxm(name: String, types: List[Typ]) extends Proof 102 case class OfClass(typ: Typ, cls: Class) extends Proof 103 case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof 104 case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof 105 106 107 /* type classes within the logic */ 108 109 object Class_Const 110 { 111 val suffix = "_class" 112 def apply(c: Class): String = c + suffix 113 def unapply(s: String): Option[Class] = 114 if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None 115 } 116 117 object OFCLASS 118 { 119 def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c)) 120 121 def apply(ty: Typ, c: Class): Term = 122 App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty))) 123 124 def unapply(t: Term): Option[(Typ, String)] = 125 t match { 126 case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1))) 127 if ty == ty1 => Some((ty, c)) 128 case _ => None 129 } 130 } 131 132 133 134 /** cache **/ 135 136 def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache = 137 new Cache(initial_size, max_string) 138 139 class Cache private[Term](initial_size: Int, max_string: Int) 140 extends isabelle.Cache(initial_size, max_string) 141 { 142 protected def cache_indexname(x: Indexname): Indexname = 143 lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) 144 145 protected def cache_sort(x: Sort): Sort = 146 if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_))) 147 148 protected def cache_typ(x: Typ): Typ = 149 { 150 if (x == dummyT) dummyT 151 else 152 lookup(x) match { 153 case Some(y) => y 154 case None => 155 x match { 156 case Type(name, args) => store(Type(cache_string(name), cache_typs(args))) 157 case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort))) 158 case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort))) 159 } 160 } 161 } 162 163 protected def cache_typs(x: List[Typ]): List[Typ] = 164 { 165 if (x.isEmpty) Nil 166 else { 167 lookup(x) match { 168 case Some(y) => y 169 case None => store(x.map(cache_typ(_))) 170 } 171 } 172 } 173 174 protected def cache_term(x: Term): Term = 175 { 176 lookup(x) match { 177 case Some(y) => y 178 case None => 179 x match { 180 case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs))) 181 case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ))) 182 case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ))) 183 case Bound(_) => store(x) 184 case Abs(name, typ, body) => 185 store(Abs(cache_string(name), cache_typ(typ), cache_term(body))) 186 case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) 187 } 188 } 189 } 190 191 protected def cache_proof(x: Proof): Proof = 192 { 193 if (x == MinProof) MinProof 194 else { 195 lookup(x) match { 196 case Some(y) => y 197 case None => 198 x match { 199 case PBound(_) => store(x) 200 case Abst(name, typ, body) => 201 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body))) 202 case AbsP(name, hyp, body) => 203 store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body))) 204 case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg))) 205 case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg))) 206 case Hyp(hyp) => store(Hyp(cache_term(hyp))) 207 case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types))) 208 case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls))) 209 case Oracle(name, prop, types) => 210 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types))) 211 case PThm(serial, theory_name, name, types) => 212 store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types))) 213 } 214 } 215 } 216 } 217 218 // main methods 219 def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } 220 def sort(x: Sort): Sort = synchronized { cache_sort(x) } 221 def typ(x: Typ): Typ = synchronized { cache_typ(x) } 222 def term(x: Term): Term = synchronized { cache_term(x) } 223 def proof(x: Proof): Proof = synchronized { cache_proof(x) } 224 225 def position(x: Position.T): Position.T = 226 synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } 227 } 228} 229