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