equal
deleted
inserted
replaced
47 sig |
47 sig |
48 type encoding |
48 type encoding |
49 val empty : encoding |
49 val empty : encoding |
50 val insert : term -> encoding -> int * encoding |
50 val insert : term -> encoding -> int * encoding |
51 val lookup_code : term -> encoding -> int option |
51 val lookup_code : term -> encoding -> int option |
52 val lookup_term : int -> encoding -> term option |
52 val lookup_term : int -> encoding -> term option |
53 val remove_code : int -> encoding -> encoding |
53 val remove_code : int -> encoding -> encoding |
54 val remove_term : term -> encoding -> encoding |
54 val remove_term : term -> encoding -> encoding |
55 val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a |
|
56 end |
55 end |
57 = |
56 = |
58 struct |
57 struct |
59 |
58 |
60 type encoding = int * (int Termtab.table) * (term Inttab.table) |
59 type encoding = int * (int Termtab.table) * (term Inttab.table) |
73 fun remove_code c (e as (count, term2int, int2term)) = |
72 fun remove_code c (e as (count, term2int, int2term)) = |
74 (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term)) |
73 (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term)) |
75 |
74 |
76 fun remove_term t (e as (count, term2int, int2term)) = |
75 fun remove_term t (e as (count, term2int, int2term)) = |
77 (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term)) |
76 (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term)) |
78 |
|
79 fun fold f (_, term2int, _) = Termtab.fold f term2int |
|
80 |
77 |
81 end |
78 end |
82 |
79 |
83 exception Make of string; |
80 exception Make of string; |
84 exception Compute of string; |
81 exception Compute of string; |