equal
deleted
inserted
replaced
1 Trie = Main + |
|
2 consts assoc :: "('key * 'val)list => 'key => 'val option" |
|
3 primrec "assoc [] x = None" |
|
4 "assoc (p#ps) x = |
|
5 (let (a,b) = p in if a=x then Some b else assoc ps x)" |
|
6 datatype ('a,'v)trie = Trie ('v option) "('a * ('a,'v)trie)list" |
|
7 consts value :: ('a,'v)trie => 'v option |
|
8 alist :: "('a,'v)trie => ('a * ('a,'v)trie)list" |
|
9 primrec "value(Trie ov al) = ov" |
|
10 primrec "alist(Trie ov al) = al" |
|
11 consts lookup :: ('a,'v)trie => 'a list => 'v option |
|
12 primrec "lookup t [] = value t" |
|
13 "lookup t (a#as) = (case assoc (alist t) a of |
|
14 None => None |
|
15 | Some at => lookup at as)" |
|
16 consts update :: ('a,'v)trie => 'a list => 'v => ('a,'v)trie |
|
17 |
|
18 primrec |
|
19 "update t [] v = Trie (Some v) (alist t)" |
|
20 "update t (a#as) v = (let tt = (case assoc (alist t) a of |
|
21 None => Trie None [] | Some at => at) |
|
22 in Trie (value t) ((a,update tt as v)#alist t))" |
|
23 end |
|