27 case class Free(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 |
28 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
29 case class Bound(index: Int) extends Term |
29 case class Bound(index: Int) extends Term |
30 case class Abs(name: String, typ: Typ = dummyT, body: Term) 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 |
31 case class App(fun: Term, arg: Term) extends Term |
|
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 } |
32 } |
91 } |
33 |
|