1 /* Author: Denis Paluca, TU Muenchen |
|
2 |
|
3 Encoding of Isabelle symbols. |
|
4 */ |
|
5 |
|
6 'use strict'; |
|
7 |
|
8 import { TextEncoder } from 'util' |
|
9 import * as symbol from '../symbol' |
|
10 import { Prefix_Tree, Tree_Node } from './prefix_tree' |
|
11 |
|
12 class Encode_Data |
|
13 { |
|
14 prefix_tree: Prefix_Tree |
|
15 min_length: number |
|
16 max_length: number |
|
17 |
|
18 constructor(origin: Uint8Array[], replacement: Uint8Array[]) |
|
19 { |
|
20 this.prefix_tree = new Prefix_Tree() |
|
21 |
|
22 for (let i = 0; i < origin.length; i++) { |
|
23 const entry = origin[i] |
|
24 if (!this.min_length || this.min_length > entry.length) |
|
25 this.min_length = entry.length |
|
26 |
|
27 if (!this.max_length || this.max_length< entry.length) |
|
28 this.max_length = entry.length |
|
29 |
|
30 this.prefix_tree.insert(Array.from(entry), Array.from(replacement[i])) |
|
31 } |
|
32 } |
|
33 } |
|
34 |
|
35 export class Symbol_Encoder |
|
36 { |
|
37 private symbols: Encode_Data |
|
38 private sequences: Encode_Data |
|
39 |
|
40 constructor(entries: symbol.Entry[]) |
|
41 { |
|
42 let syms: Uint8Array[] = [] |
|
43 let seqs: Uint8Array[] = [] |
|
44 const encoder = new TextEncoder() |
|
45 for (const {symbol, code} of entries) { |
|
46 seqs.push(encoder.encode(symbol)) |
|
47 syms.push(encoder.encode(String.fromCharCode(code))) |
|
48 } |
|
49 this.symbols = new Encode_Data(syms, seqs) |
|
50 this.sequences = new Encode_Data(seqs, syms) |
|
51 } |
|
52 |
|
53 encode(content: Uint8Array): Uint8Array |
|
54 { |
|
55 return this.code(content, this.sequences, this.symbols) |
|
56 } |
|
57 |
|
58 decode(content: Uint8Array): Uint8Array |
|
59 { |
|
60 return this.code(content, this.symbols, this.sequences) |
|
61 } |
|
62 |
|
63 private code(content: Uint8Array, origin: Encode_Data, replacements: Encode_Data): Uint8Array |
|
64 { |
|
65 const result: number[] = [] |
|
66 |
|
67 for (let i = 0; i < content.length; i++) { |
|
68 if (i > content.length - origin.min_length) { |
|
69 result.push(content[i]) |
|
70 continue |
|
71 } |
|
72 |
|
73 let word: number[] = [] |
|
74 let node: Tree_Node |
|
75 for (let j = i; j < i + origin.max_length; j++) { |
|
76 word.push(content[j]) |
|
77 node = origin.prefix_tree.get_node(word) |
|
78 if (!node || node.end) { |
|
79 break |
|
80 } |
|
81 } |
|
82 |
|
83 if (node && node.end) { |
|
84 result.push(...(node.value as number[])) |
|
85 i += word.length - 1 |
|
86 continue |
|
87 } |
|
88 result.push(content[i]) |
|
89 } |
|
90 |
|
91 return new Uint8Array(result) |
|
92 } |
|
93 } |
|