1(* Code to recall that some partial functions (of type 'a -> 'b option)
2can be represented as sorted alists, and derive a fast conversion on
3applications of those functions. *)
4
5signature alist_treeLib = sig
6
7include Abbrev
8
9(* Syntax *)
10val alookup_tm : term;
11val option_choice_tm : term;
12val repr_tm : term;
13
14(* The repr set type *)
15type 'a alist_reprs
16
17(*
18   Representations of partial functions using sorted trees.
19   Requires a relation R and a theorem that shows
20   it is irreflexive and transitive. The destructor maps terms
21   of the domain type to some type that can be sorted in ML.
22   The conversion must prove R x y for any x, y where x is
23   sorted before y by the destructor and comparison.
24*)
25val mk_alist_reprs : thm -> conv -> (term -> 'a)
26    -> (('a * 'a) -> order) -> 'a alist_reprs
27
28(*
29   The representation set contains representations of various
30   partial functions, initially none.
31*)
32val peek_functions_in_rs : 'a alist_reprs -> term list
33
34(*
35   Adds a function's representation.
36
37   Requires a theorem f = rhs with a valid rhs.
38   A valid rhs is:
39     - ALOOKUP xs
40     - a function g in the repr set.
41     - option_choice_f of two valid rhs values
42*)
43val add_alist_repr : 'a alist_reprs -> thm -> unit
44
45(*
46   Converts f x to a concrete value (SOME y/NONE)
47   for functions f in the repr set.
48*)
49val reprs_conv : 'a alist_reprs -> conv
50
51end
52
53