1signature encodeLib =
2sig
3        include Abbrev
4
5        val construct_bottom_value :
6            (hol_type -> bool) -> term -> hol_type -> term
7        val set_bottom_value : hol_type -> term -> unit
8        val target_bottom_value : hol_type -> term -> hol_type -> term
9        val get_encode_type  : hol_type -> hol_type -> hol_type
10        val get_decode_type  : hol_type -> hol_type -> hol_type
11        val get_detect_type  : hol_type -> hol_type -> hol_type
12        val get_map_type  : hol_type -> hol_type
13        val get_all_type  : hol_type -> hol_type
14        val get_fix_type  : hol_type -> hol_type -> hol_type
15        val mk_encode_var  : hol_type -> hol_type -> term
16        val mk_decode_var  : hol_type -> hol_type -> term
17        val mk_detect_var  : hol_type -> hol_type -> term
18        val mk_map_var  : hol_type -> term
19        val mk_all_var  : hol_type -> term
20        val mk_fix_var  : hol_type -> hol_type -> term
21        val get_encode_const  : hol_type -> hol_type -> term
22        val get_decode_const  : hol_type -> hol_type -> term
23        val get_map_const  : hol_type -> term
24        val get_all_const  : hol_type -> term
25        val get_fix_const  : hol_type -> hol_type -> term
26        val get_detect_const  : hol_type -> hol_type -> term
27        val get_all_function  : hol_type -> term
28        val get_decode_function  : hol_type -> hol_type -> term
29        val get_map_function  : hol_type -> term
30        val get_fix_function  : hol_type -> hol_type -> term
31        val get_detect_function  : hol_type -> hol_type -> term
32        val get_encode_function  : hol_type -> hol_type -> term
33        val mk_detect_term  : hol_type -> hol_type -> term
34        val mk_decode_term  : hol_type -> hol_type -> term
35        val mk_fix_term  : hol_type -> hol_type -> term
36        val mk_encode_term  : hol_type -> hol_type -> term
37        val mk_map_term  : hol_type -> term
38        val mk_all_term  : hol_type -> term
39        val ENCODE_CONV  : thm -> term -> thm
40        val DETECT_CONV  : hol_type -> term -> thm
41        val DECODE_CONV  : hol_type -> term -> thm
42        val FIX_CONV  : hol_type -> term -> thm
43        val mk_encodes  : hol_type -> hol_type -> unit
44        val CONSOLIDATE_CONV  : (term -> term) -> term -> thm
45        val mk_decodes  : hol_type -> hol_type -> unit
46        val mk_detects  : hol_type -> hol_type -> unit
47        val mk_maps  : hol_type -> unit
48        val mk_alls  : hol_type -> unit
49        val mk_fixs  : hol_type -> hol_type -> unit
50        val type_vars_avoiding_itself  : term -> hol_type -> hol_type list
51        val check_function  : (hol_type -> term) -> hol_type -> term
52        val get_sub_types : hol_type -> hol_type -> hol_type list
53        val wrap_full : string -> hol_type -> exn -> 'a
54
55        val mk_encode_decode_map_conc  : hol_type -> hol_type -> term
56        val mk_encode_map_encode_conc  : hol_type -> hol_type -> term
57        val mk_map_compose_conc  : hol_type -> term
58        val mk_decode_encode_fix_conc  : hol_type -> hol_type -> term
59        val mk_encode_detect_all_conc  : hol_type -> hol_type -> term
60        val mk_map_id_conc  : hol_type -> term
61        val mk_all_id_conc  : hol_type -> term
62        val mk_fix_id_conc  : hol_type -> hol_type -> term
63        val mk_general_detect_conc  : hol_type -> hol_type -> term
64        val mk_encode_decode_conc  : hol_type -> hol_type -> term
65        val mk_encode_detect_conc  : hol_type -> hol_type -> term
66        val mk_decode_encode_conc  : hol_type -> hol_type -> term
67        val FULL_ENCODE_DECODE_MAP_THM  : hol_type -> hol_type -> thm
68        val FULL_ENCODE_DETECT_ALL_THM  : hol_type -> hol_type -> thm
69        val FULL_ENCODE_MAP_ENCODE_THM  : hol_type -> hol_type -> thm
70        val FULL_DECODE_ENCODE_FIX_THM  : hol_type -> hol_type -> thm
71        val FULL_MAP_COMPOSE_THM  : hol_type -> thm
72        val FULL_MAP_ID_THM  : hol_type -> thm
73        val FULL_ALL_ID_THM  : hol_type -> thm
74        val FULL_FIX_ID_THM  : hol_type -> hol_type -> thm
75        val FULL_ENCODE_DECODE_THM  : hol_type -> hol_type -> thm
76        val FULL_ENCODE_DETECT_THM  : hol_type -> hol_type -> thm
77        val FULL_DECODE_ENCODE_THM  : hol_type -> hol_type -> thm
78        val ENCODER_CONV  : term -> thm
79        val APP_MAP_CONV  : term -> thm
80        val APP_ALL_CONV  : term -> thm
81        val DECODE_PAIR_CONV  : term -> thm
82        val DETECT_PAIR_CONV  : hol_type -> term -> thm
83        val encode_decode_map_tactic : hol_type -> hol_type -> term list * term ->
84                (term list * term) list * (thm list -> thm)
85        val encode_map_encode_tactic : hol_type -> hol_type -> term list * term ->
86                (term list * term) list * (thm list -> thm)
87        val map_compose_tactic : hol_type -> term list * term -> (term list * term) list * (thm list -> thm)
88        val encode_detect_all_tactic : hol_type -> hol_type -> term list * term ->
89                (term list * term) list * (thm list -> thm)
90        val LET_RAND_CONV  : term -> term -> thm
91        val decode_encode_fix_tactic : hol_type -> 'a -> term list * term ->
92                (term list * term) list * (thm list -> thm)
93        val fix_id_tactic : hol_type -> hol_type -> term list * term ->
94                (term list * term) list * (thm list -> thm)
95        val general_detect_tactic : hol_type -> hol_type -> term list * term ->
96                (term list * term) list * (thm list -> thm)
97        val detect_dead_rule  : hol_type -> hol_type -> thm
98        val all_id_tactic : 'a -> term list * term -> (term list * term) list * (thm list -> thm)
99        val map_id_tactic : 'a -> term list * term -> (term list * term) list * (thm list -> thm)
100        val initialise_source_function_generators  : unit -> unit
101        val initialise_coding_function_generators  : hol_type -> unit
102        val initialise_coding_theorem_generators  : hol_type -> unit
103
104        val mk_destructors : hol_type -> hol_type -> (thm list * thm list)
105
106        val encode_type : hol_type -> hol_type -> unit
107        val gen_encode_function : hol_type -> hol_type -> term
108        val gen_decode_function : hol_type -> hol_type -> term
109        val gen_detect_function : hol_type -> hol_type -> term
110
111        val MK_FST : thm -> thm
112        val MK_SND : thm -> thm
113
114        val CONSOLIDATE_CONV_data : (((term -> term) * term) option) ref
115
116        val predicate_equivalence : hol_type -> hol_type -> thm
117end