author | wenzelm |
Fri, 03 Apr 2020 17:35:10 +0200 | |
changeset 71675 | 55cb4271858b |
parent 71601 | 97ccf48c2f0c |
child 71777 | 3875815f5967 |
permissions | -rw-r--r-- |
43730 | 1 |
/* Title: Pure/term.scala |
2 |
Author: Makarius |
|
3 |
||
43779 | 4 |
Lambda terms, types, sorts. |
43730 | 5 |
|
6 |
Note: Isabelle/ML is the primary environment for logical operations. |
|
7 |
*/ |
|
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
12 |
object Term |
|
13 |
{ |
|
70383
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
14 |
/* types and terms */ |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
15 |
|
70852 | 16 |
sealed case class Indexname(name: String, index: Int = 0) |
70537
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
17 |
{ |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
18 |
override def toString: String = |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
19 |
if (index == -1) name |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
20 |
else { |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
21 |
val dot = |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
22 |
Symbol.explode(name).reverse match { |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
23 |
case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
24 |
case c :: _ => Symbol.is_digit(c) |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
25 |
case _ => true |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
26 |
} |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
27 |
if (dot) "?" + name + "." + index |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
28 |
else if (index != 0) "?" + name + index |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
29 |
else "?" + name |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
30 |
} |
17160e0a60b6
Indexname.toString according to string_of_vname' in ML;
wenzelm
parents:
70536
diff
changeset
|
31 |
} |
43730 | 32 |
|
70850 | 33 |
type Class = String |
34 |
type Sort = List[Class] |
|
43730 | 35 |
|
36 |
sealed abstract class Typ |
|
37 |
case class Type(name: String, args: List[Typ] = Nil) extends Typ |
|
70846 | 38 |
{ |
39 |
override def toString: String = |
|
40 |
if (this == dummyT) "_" |
|
41 |
else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")" |
|
42 |
} |
|
70851 | 43 |
case class TFree(name: String, sort: Sort = Nil) extends Typ |
70846 | 44 |
{ |
45 |
override def toString: String = |
|
70851 | 46 |
"TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")" |
70846 | 47 |
} |
70851 | 48 |
case class TVar(name: Indexname, sort: Sort = Nil) extends Typ |
70846 | 49 |
{ |
50 |
override def toString: String = |
|
70851 | 51 |
"TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")" |
70846 | 52 |
} |
71601 | 53 |
val dummyT: Type = Type("dummy") |
43730 | 54 |
|
55 |
sealed abstract class Term |
|
71221 | 56 |
{ |
57 |
def head: Term = |
|
58 |
this match { |
|
59 |
case App(fun, _) => fun.head |
|
60 |
case _ => this |
|
61 |
} |
|
62 |
} |
|
70846 | 63 |
case class Const(name: String, typargs: List[Typ] = Nil) extends Term |
64 |
{ |
|
65 |
override def toString: String = |
|
70897 | 66 |
if (this == dummy) "_" |
67 |
else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")" |
|
70846 | 68 |
} |
43730 | 69 |
case class Free(name: String, typ: Typ = dummyT) extends Term |
70846 | 70 |
{ |
71 |
override def toString: String = |
|
72 |
"Free(" + name + (if (typ == dummyT) "" else "," + typ) + ")" |
|
73 |
} |
|
43730 | 74 |
case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
70846 | 75 |
{ |
76 |
override def toString: String = |
|
77 |
"Var(" + name + (if (typ == dummyT) "" else "," + typ) + ")" |
|
78 |
} |
|
43730 | 79 |
case class Bound(index: Int) extends Term |
70846 | 80 |
case class Abs(name: String, typ: Typ, body: Term) extends Term |
43730 | 81 |
case class App(fun: Term, arg: Term) extends Term |
70850 | 82 |
{ |
83 |
override def toString: String = |
|
84 |
this match { |
|
85 |
case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")" |
|
86 |
case _ => "App(" + fun + "," + arg + ")" |
|
87 |
} |
|
88 |
} |
|
68265 | 89 |
|
70897 | 90 |
def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty)) |
91 |
val dummy: Term = dummy_pattern(dummyT) |
|
92 |
||
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
93 |
sealed abstract class Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
94 |
case object MinProof extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
95 |
case class PBound(index: Int) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
96 |
case class Abst(name: String, typ: Typ, body: Proof) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
97 |
case class AbsP(name: String, hyp: Term, body: Proof) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
98 |
case class Appt(fun: Proof, arg: Term) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
99 |
case class AppP(fun: Proof, arg: Proof) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
100 |
case class Hyp(hyp: Term) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
101 |
case class PAxm(name: String, types: List[Typ]) extends Proof |
70850 | 102 |
case class OfClass(typ: Typ, cls: Class) extends Proof |
70834 | 103 |
case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof |
70916
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70897
diff
changeset
|
104 |
case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof |
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
105 |
|
68265 | 106 |
|
70850 | 107 |
/* type classes within the logic */ |
70385
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
108 |
|
70850 | 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 |
} |
|
70385
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
116 |
|
70850 | 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))) |
|
70385
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
123 |
|
70850 | 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 |
} |
|
70385
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
130 |
} |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
131 |
|
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
132 |
|
68265 | 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 = |
|
70536 | 143 |
lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) |
68265 | 144 |
|
145 |
protected def cache_sort(x: Sort): Sort = |
|
71601 | 146 |
if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string)) |
68265 | 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 { |
|
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
156 |
case Type(name, args) => store(Type(cache_string(name), cache_typs(args))) |
68265 | 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 |
||
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
163 |
protected def cache_typs(x: List[Typ]): List[Typ] = |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
164 |
{ |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
165 |
if (x.isEmpty) Nil |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
166 |
else { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
167 |
lookup(x) match { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
168 |
case Some(y) => y |
71601 | 169 |
case None => store(x.map(cache_typ)) |
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
170 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
171 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
172 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
173 |
|
68265 | 174 |
protected def cache_term(x: Term): Term = |
175 |
{ |
|
176 |
lookup(x) match { |
|
177 |
case Some(y) => y |
|
178 |
case None => |
|
179 |
x match { |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70559
diff
changeset
|
180 |
case Const(name, typargs) => store(Const(cache_string(name), cache_typs(typargs))) |
68265 | 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))) |
|
70536 | 183 |
case Bound(_) => store(x) |
68265 | 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 |
||
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
191 |
protected def cache_proof(x: Proof): Proof = |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
192 |
{ |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
193 |
if (x == MinProof) MinProof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
194 |
else { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
195 |
lookup(x) match { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
196 |
case Some(y) => y |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
197 |
case None => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
198 |
x match { |
70536 | 199 |
case PBound(_) => store(x) |
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
200 |
case Abst(name, typ, body) => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
201 |
store(Abst(cache_string(name), cache_typ(typ), cache_proof(body))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
202 |
case AbsP(name, hyp, body) => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
203 |
store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
204 |
case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
205 |
case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg))) |
70535 | 206 |
case Hyp(hyp) => store(Hyp(cache_term(hyp))) |
207 |
case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types))) |
|
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
208 |
case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
209 |
case Oracle(name, prop, types) => |
70834 | 210 |
store(Oracle(cache_string(name), cache_term(prop), cache_typs(types))) |
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70537
diff
changeset
|
211 |
case PThm(serial, theory_name, name, types) => |
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70537
diff
changeset
|
212 |
store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types))) |
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
213 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
214 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
215 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
216 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
217 |
|
68265 | 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) } |
|
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
223 |
def proof(x: Proof): Proof = synchronized { cache_proof(x) } |
68265 | 224 |
|
225 |
def position(x: Position.T): Position.T = |
|
226 |
synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
|
227 |
} |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
228 |
} |