author | wenzelm |
Thu, 03 Jan 2019 12:34:26 +0100 | |
changeset 69574 | b4ea943ce0b7 |
parent 68265 | f0899dad4877 |
child 70383 | 38ac2e714729 |
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 |
{ |
|
14 |
type Indexname = (String, Int) |
|
15 |
||
16 |
type Sort = List[String] |
|
17 |
val dummyS: Sort = List("") |
|
18 |
||
19 |
sealed abstract class Typ |
|
20 |
case class Type(name: String, args: List[Typ] = Nil) extends Typ |
|
21 |
case class TFree(name: String, sort: Sort = dummyS) extends Typ |
|
22 |
case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ |
|
23 |
val dummyT = Type("dummy") |
|
24 |
||
25 |
sealed abstract class Term |
|
26 |
case class Const(name: String, typ: Typ = dummyT) extends Term |
|
27 |
case class Free(name: String, typ: Typ = dummyT) extends Term |
|
28 |
case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
|
29 |
case class Bound(index: Int) extends Term |
|
30 |
case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
|
31 |
case class App(fun: Term, arg: Term) extends Term |
|
68265 | 32 |
|
33 |
||
34 |
||
35 |
/** cache **/ |
|
36 |
||
37 |
def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache = |
|
38 |
new Cache(initial_size, max_string) |
|
39 |
||
40 |
class Cache private[Term](initial_size: Int, max_string: Int) |
|
41 |
extends isabelle.Cache(initial_size, max_string) |
|
42 |
{ |
|
43 |
protected def cache_indexname(x: Indexname): Indexname = |
|
44 |
lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2)) |
|
45 |
||
46 |
protected def cache_sort(x: Sort): Sort = |
|
47 |
if (x == dummyS) dummyS |
|
48 |
else lookup(x) getOrElse store(x.map(cache_string(_))) |
|
49 |
||
50 |
protected def cache_typ(x: Typ): Typ = |
|
51 |
{ |
|
52 |
if (x == dummyT) dummyT |
|
53 |
else |
|
54 |
lookup(x) match { |
|
55 |
case Some(y) => y |
|
56 |
case None => |
|
57 |
x match { |
|
58 |
case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_)))) |
|
59 |
case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort))) |
|
60 |
case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort))) |
|
61 |
} |
|
62 |
} |
|
63 |
} |
|
64 |
||
65 |
protected def cache_term(x: Term): Term = |
|
66 |
{ |
|
67 |
lookup(x) match { |
|
68 |
case Some(y) => y |
|
69 |
case None => |
|
70 |
x match { |
|
71 |
case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ))) |
|
72 |
case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ))) |
|
73 |
case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ))) |
|
74 |
case Bound(index) => store(Bound(cache_int(index))) |
|
75 |
case Abs(name, typ, body) => |
|
76 |
store(Abs(cache_string(name), cache_typ(typ), cache_term(body))) |
|
77 |
case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) |
|
78 |
} |
|
79 |
} |
|
80 |
} |
|
81 |
||
82 |
// main methods |
|
83 |
def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } |
|
84 |
def sort(x: Sort): Sort = synchronized { cache_sort(x) } |
|
85 |
def typ(x: Typ): Typ = synchronized { cache_typ(x) } |
|
86 |
def term(x: Term): Term = synchronized { cache_term(x) } |
|
87 |
||
88 |
def position(x: Position.T): Position.T = |
|
89 |
synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
|
90 |
} |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
91 |
} |