author | wenzelm |
Thu, 15 Aug 2019 16:26:50 +0200 | |
changeset 70536 | fe4d545f12e3 |
parent 70535 | de6062ac70b6 |
child 70537 | 17160e0a60b6 |
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 |
|
70536 | 16 |
sealed case class Indexname(name: String, index: Int) |
43730 | 17 |
|
18 |
type Sort = List[String] |
|
19 |
val dummyS: Sort = List("") |
|
20 |
||
21 |
sealed abstract class Typ |
|
22 |
case class Type(name: String, args: List[Typ] = Nil) extends Typ |
|
23 |
case class TFree(name: String, sort: Sort = dummyS) extends Typ |
|
24 |
case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ |
|
25 |
val dummyT = Type("dummy") |
|
26 |
||
27 |
sealed abstract class Term |
|
28 |
case class Const(name: String, typ: Typ = dummyT) extends Term |
|
29 |
case class Free(name: String, typ: Typ = dummyT) extends Term |
|
30 |
case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
|
31 |
case class Bound(index: Int) extends Term |
|
32 |
case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
|
33 |
case class App(fun: Term, arg: Term) extends Term |
|
68265 | 34 |
|
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
35 |
sealed abstract class Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
36 |
case object MinProof extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
37 |
case class PBound(index: Int) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
case class Appt(fun: Proof, arg: Term) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
41 |
case class AppP(fun: Proof, arg: Proof) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
42 |
case class Hyp(hyp: Term) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
43 |
case class PAxm(name: String, types: List[Typ]) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
44 |
case class OfClass(typ: Typ, cls: String) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
45 |
case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
46 |
case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
47 |
|
68265 | 48 |
|
70385
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
49 |
/* Pure logic */ |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
50 |
|
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
51 |
def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty)) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
52 |
val propT: Typ = Type(Pure_Thy.PROP, Nil) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
53 |
def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2)) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
54 |
|
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
55 |
def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty)) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
56 |
|
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
57 |
def const_of_class(c: String): String = c + "_class" |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
58 |
|
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
59 |
def mk_of_sort(ty: Typ, s: Sort): List[Term] = |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
60 |
{ |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
61 |
val class_type = funT(itselfT(ty), propT) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
62 |
val t = mk_type(ty) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
63 |
s.map(c => App(Const(const_of_class(c), class_type), t)) |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
64 |
} |
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
65 |
|
68d2c533db9c
more operations: support type classes within the logic;
wenzelm
parents:
70383
diff
changeset
|
66 |
|
70383
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
67 |
/* type arguments of consts */ |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
68 |
|
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
69 |
def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] = |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
70 |
{ |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
71 |
var subst = Map.empty[String, Typ] |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
72 |
|
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
73 |
def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ) |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
74 |
def raw_match(arg: (Typ, Typ)) |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
75 |
{ |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
76 |
arg match { |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
77 |
case (TFree(a, _), ty) => |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
78 |
subst.get(a) match { |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
79 |
case None => subst += (a -> ty) |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
80 |
case Some(ty1) => if (ty != ty1) bad_match() |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
81 |
} |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
82 |
case (Type(c1, args1), Type(c2, args2)) if c1 == c2 => |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
83 |
(args1 zip args2).foreach(raw_match) |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
84 |
case _ => bad_match() |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
85 |
} |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
86 |
} |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
87 |
raw_match(decl, typ) |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
88 |
|
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
89 |
typargs.map(subst) |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
90 |
} |
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
91 |
|
38ac2e714729
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
wenzelm
parents:
68265
diff
changeset
|
92 |
|
68265 | 93 |
|
94 |
/** cache **/ |
|
95 |
||
96 |
def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache = |
|
97 |
new Cache(initial_size, max_string) |
|
98 |
||
99 |
class Cache private[Term](initial_size: Int, max_string: Int) |
|
100 |
extends isabelle.Cache(initial_size, max_string) |
|
101 |
{ |
|
102 |
protected def cache_indexname(x: Indexname): Indexname = |
|
70536 | 103 |
lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) |
68265 | 104 |
|
105 |
protected def cache_sort(x: Sort): Sort = |
|
106 |
if (x == dummyS) dummyS |
|
107 |
else lookup(x) getOrElse store(x.map(cache_string(_))) |
|
108 |
||
109 |
protected def cache_typ(x: Typ): Typ = |
|
110 |
{ |
|
111 |
if (x == dummyT) dummyT |
|
112 |
else |
|
113 |
lookup(x) match { |
|
114 |
case Some(y) => y |
|
115 |
case None => |
|
116 |
x match { |
|
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
117 |
case Type(name, args) => store(Type(cache_string(name), cache_typs(args))) |
68265 | 118 |
case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort))) |
119 |
case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort))) |
|
120 |
} |
|
121 |
} |
|
122 |
} |
|
123 |
||
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
124 |
protected def cache_typs(x: List[Typ]): List[Typ] = |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
125 |
{ |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
126 |
if (x.isEmpty) Nil |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
127 |
else { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
128 |
lookup(x) match { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
129 |
case Some(y) => y |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
130 |
case None => store(x.map(cache_typ(_))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
131 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
132 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
133 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
134 |
|
68265 | 135 |
protected def cache_term(x: Term): Term = |
136 |
{ |
|
137 |
lookup(x) match { |
|
138 |
case Some(y) => y |
|
139 |
case None => |
|
140 |
x match { |
|
141 |
case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ))) |
|
142 |
case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ))) |
|
143 |
case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ))) |
|
70536 | 144 |
case Bound(_) => store(x) |
68265 | 145 |
case Abs(name, typ, body) => |
146 |
store(Abs(cache_string(name), cache_typ(typ), cache_term(body))) |
|
147 |
case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) |
|
148 |
} |
|
149 |
} |
|
150 |
} |
|
151 |
||
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
152 |
protected def cache_proof(x: Proof): Proof = |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
153 |
{ |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
154 |
if (x == MinProof) MinProof |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
155 |
else { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
156 |
lookup(x) match { |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
157 |
case Some(y) => y |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
158 |
case None => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
159 |
x match { |
70536 | 160 |
case PBound(_) => store(x) |
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
161 |
case Abst(name, typ, body) => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
162 |
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
|
163 |
case AbsP(name, hyp, body) => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
164 |
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
|
165 |
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
|
166 |
case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg))) |
70535 | 167 |
case Hyp(hyp) => store(Hyp(cache_term(hyp))) |
168 |
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
|
169 |
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
|
170 |
case Oracle(name, prop, types) => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
171 |
store(Oracle(cache_string(name), cache_term(prop), cache_typs(types))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
172 |
case PThm(serial, name, types) => |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
173 |
store(PThm(serial, cache_string(name), cache_typs(types))) |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
174 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
175 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
176 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
177 |
} |
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
178 |
|
68265 | 179 |
// main methods |
180 |
def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } |
|
181 |
def sort(x: Sort): Sort = synchronized { cache_sort(x) } |
|
182 |
def typ(x: Typ): Typ = synchronized { cache_typ(x) } |
|
183 |
def term(x: Term): Term = synchronized { cache_term(x) } |
|
70533
031620901fcd
support for (fully reconstructed) proof terms in Scala;
wenzelm
parents:
70385
diff
changeset
|
184 |
def proof(x: Proof): Proof = synchronized { cache_proof(x) } |
68265 | 185 |
|
186 |
def position(x: Position.T): Position.T = |
|
187 |
synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
|
188 |
} |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43730
diff
changeset
|
189 |
} |