author | wenzelm |
Wed, 21 Jun 2023 15:53:38 +0200 | |
changeset 78191 | 6e52cda26ad4 |
parent 78188 | fd68b98de1f6 |
child 78193 | 443a443bbe7b |
permissions | -rw-r--r-- |
76991 | 1 |
/* Title: Pure/ML/ml_heap.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
ML heap operations. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import java.nio.ByteBuffer |
|
11 |
import java.nio.channels.FileChannel |
|
12 |
import java.nio.file.StandardOpenOption |
|
13 |
||
14 |
||
15 |
object ML_Heap { |
|
16 |
/** heap file with SHA1 digest **/ |
|
17 |
||
18 |
private val sha1_prefix = "SHA1:" |
|
19 |
||
78182 | 20 |
def read_file_digest(heap: Path): Option[SHA1.Digest] = { |
76991 | 21 |
if (heap.is_file) { |
77711
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
22 |
val l = sha1_prefix.length |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
23 |
val m = l + SHA1.digest_length |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
24 |
val n = heap.file.length |
77718 | 25 |
val bs = Bytes.read_file(heap.file, offset = n - m) |
77711
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
26 |
if (bs.length == m) { |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
27 |
val s = bs.text |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
28 |
if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l))) |
76991 | 29 |
else None |
30 |
} |
|
77711
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
31 |
else None |
76991 | 32 |
} |
33 |
else None |
|
34 |
} |
|
35 |
||
78182 | 36 |
def write_file_digest(heap: Path): SHA1.Digest = |
37 |
read_file_digest(heap) getOrElse { |
|
77206 | 38 |
val digest = SHA1.digest(heap) |
39 |
File.append(heap, sha1_prefix + digest.toString) |
|
40 |
digest |
|
76991 | 41 |
} |
77720 | 42 |
|
43 |
||
44 |
/* SQL data model */ |
|
45 |
||
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
46 |
object Data extends SQL.Data("isabelle_heaps") { |
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
47 |
override lazy val tables = SQL.Tables(Base.table, Slices.table) |
78183 | 48 |
|
49 |
object Generic { |
|
50 |
val name = SQL.Column.string("name").make_primary_key |
|
51 |
} |
|
52 |
||
53 |
object Base { |
|
54 |
val name = Generic.name |
|
55 |
val size = SQL.Column.long("size") |
|
56 |
val digest = SQL.Column.string("digest") |
|
57 |
||
58 |
val table = make_table("", List(name, size, digest)) |
|
59 |
} |
|
60 |
||
61 |
object Slices { |
|
62 |
val name = Generic.name |
|
63 |
val slice = SQL.Column.int("slice").make_primary_key |
|
64 |
val content = SQL.Column.bytes("content") |
|
65 |
||
66 |
val table = make_table("slices", List(name, slice, content)) |
|
67 |
} |
|
68 |
||
69 |
def known_entry(db: SQL.Database, name: String): Boolean = |
|
70 |
db.execute_query_statementB( |
|
71 |
Base.table.select(List(Base.name), sql = Base.name.where_equal(name))) |
|
72 |
||
73 |
def defined_entry(db: SQL.Database, name: String): Option[SHA1.Digest] = |
|
74 |
db.execute_query_statementO[String]( |
|
75 |
Base.table.select(List(Base.digest), sql = Generic.name.where_equal(name)), |
|
76 |
_.string(Base.digest) |
|
77 |
).flatMap(proper_string).map(SHA1.fake_digest) |
|
78 |
||
79 |
def clean_entry(db: SQL.Database, name: String): Unit = { |
|
80 |
for (table <- List(Base.table, Slices.table)) { |
|
81 |
db.execute_statement(table.delete(sql = Base.name.where_equal(name))) |
|
82 |
} |
|
83 |
} |
|
84 |
||
85 |
def prepare_entry(db: SQL.Database, name: String): Unit = |
|
86 |
db.execute_statement(Base.table.insert(), body = |
|
87 |
{ stmt => |
|
88 |
stmt.string(1) = name |
|
89 |
stmt.long(2) = None |
|
90 |
stmt.string(3) = None |
|
91 |
}) |
|
92 |
||
93 |
def write_entry(db: SQL.Database, name: String, slice: Int, content: Bytes): Unit = |
|
94 |
db.execute_statement(Slices.table.insert(), body = |
|
95 |
{ stmt => |
|
96 |
stmt.string(1) = name |
|
97 |
stmt.int(2) = slice |
|
98 |
stmt.bytes(3) = content |
|
99 |
}) |
|
100 |
||
101 |
def finish_entry(db: SQL.Database, name: String, size: Long, digest: SHA1.Digest): Unit = |
|
102 |
db.execute_statement( |
|
103 |
Base.table.update(List(Base.size, Base.digest), sql = Base.name.where_equal(name)), |
|
104 |
body = |
|
105 |
{ stmt => |
|
106 |
stmt.long(1) = size |
|
107 |
stmt.string(2) = digest.toString |
|
108 |
}) |
|
109 |
} |
|
110 |
||
78186 | 111 |
def clean_entry(db: SQL.Database, name: String): Unit = |
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
112 |
Data.transaction_lock(db, create = true) { Data.clean_entry(db, name) } |
78186 | 113 |
|
78191 | 114 |
def store( |
78183 | 115 |
database: Option[SQL.Database], |
116 |
heap: Path, |
|
78188 | 117 |
slice: Long, |
78183 | 118 |
cache: Compress.Cache = Compress.Cache.none, |
119 |
): SHA1.Digest = { |
|
120 |
val digest = write_file_digest(heap) |
|
121 |
database match { |
|
122 |
case Some(db) => |
|
123 |
val name = heap.file_name |
|
124 |
val size = File.space(heap).bytes - sha1_prefix.length - SHA1.digest_length |
|
125 |
||
78188 | 126 |
val slices = (size.toDouble / slice.toDouble).ceil.toInt |
78183 | 127 |
val step = (size.toDouble / slices.toDouble).ceil.toLong |
128 |
||
129 |
try { |
|
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
130 |
Data.transaction_lock(db, create = true) { Data.prepare_entry(db, name) } |
78183 | 131 |
|
132 |
for (i <- 0 until slices) { |
|
133 |
val j = i + 1 |
|
134 |
val offset = step * i |
|
135 |
val limit = if (j < slices) step * j else size |
|
136 |
val content = |
|
137 |
Bytes.read_file(heap.file, offset = offset, limit = limit) |
|
138 |
.compress(cache = cache) |
|
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
139 |
Data.transaction_lock(db) { Data.write_entry(db, name, i, content) } |
78183 | 140 |
} |
141 |
||
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
142 |
Data.transaction_lock(db) { Data.finish_entry(db, name, size, digest) } |
78183 | 143 |
} |
144 |
catch { case exn: Throwable => |
|
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
145 |
Data.transaction_lock(db, create = true) { Data.clean_entry(db, name) } |
78183 | 146 |
throw exn |
147 |
} |
|
148 |
case None => |
|
149 |
} |
|
150 |
digest |
|
151 |
} |
|
76991 | 152 |
} |