-
Notifications
You must be signed in to change notification settings - Fork 86
/
Copy pathml_translatorLib.sig
166 lines (130 loc) · 6.58 KB
/
ml_translatorLib.sig
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
signature ml_translatorLib =
sig
include Abbrev
(* main functionality *)
val translate : thm -> thm (* e.g. translate listTheory.MAP *)
val translate_no_ind : thm -> thm
val abs_translate : thm -> thm
val abs_translate_no_ind : thm -> thm
val hol2deep : term -> thm (* e.g. try hol2deep ``\x.x`` *)
val hol2val : term -> term (* e.g. try hol2val ``5:num`` *)
val concretise : term list -> unit
val concretise_all : unit -> unit
val ml_prog_update : (ml_progLib.ml_prog_state ->
ml_progLib.ml_prog_state) -> unit
val get_ml_prog_state : unit -> ml_progLib.ml_prog_state
val declare_new_ref : string -> term -> thm
(* interface for teaching the translator about new types *)
val add_type_inv : term -> hol_type -> unit
val get_type_inv : hol_type -> term
val fetch_v_fun : hol_type -> (term * thm list)
val add_eval_thm : thm -> thm
val add_user_proved_v_thm : thm -> thm
val store_eq_thm : thm -> thm
val register_type : hol_type -> unit
val abs_register_type : hol_type -> unit
val ignore_type : hol_type -> unit
val register_exn_type : hol_type -> unit
val abs_register_exn_type : hol_type -> unit
val full_name_of_type : hol_type -> string
val case_of : hol_type -> thm
val eq_lemmas : unit -> thm list
(* prove an EqualityType, assuming some for parameters types if needed *)
val EqualityType_rule : hol_type list -> hol_type -> thm
(* CakeML signature generation and extraction *)
(* Get the CakeML signature of a named CakeML function which was created by translation *)
(* Returns ``:spec`` *)
val sig_of_mlname : string -> term
(* Get the CakeML signatures for a list of CakeML functions which were created by translation *)
(* Returns ``:spec list`` *)
val module_signatures : string list -> term
(* loading / storing state of translator *)
val translation_extends : string -> unit
val reset_translation : unit -> unit (* bring back to initial state *)
val finalise_translation : unit -> unit (* happens automatically at export *)
(* simplification of preconditions / sideconditions *)
val update_precondition : thm -> thm
(* configuration *)
val pick_name : (term -> string) ref
val use_long_names : bool ref
val use_mem_intro : bool ref
val next_ml_names : (string list) ref
val print_asts : bool ref
val use_full_type_names : bool ref
val add_preferred_thy : string -> unit
val find_def_for_const : (term -> thm) ref
val clean_on_exit : bool ref
val generate_sigs : bool ref
(* internals, for the monadic translation *)
val match_rec_pattern : term -> term * string * term
val install_rec_pattern : term -> string -> string -> unit
val uninstall_rec_patterns : unit -> unit
val preprocess_def : thm -> bool * thm list * thm option
val get_unique_name : string -> string
val get_next_ml_name : string -> string
val get_info : thm -> string * string * term * term * thm
val get_nchotomy_of : hol_type -> thm
val sat_hyp_lemma : thm
val comma : string list -> string
val rev_param_list : term -> term list
val print_fname : string -> thm -> unit
val last_fail : term ref
val check_inv : string -> term -> thm -> thm
val remove_primes : thm -> thm
val clean_assumptions : thm -> thm
val SIMP_EqualityType_ASSUMS : thm -> thm
val FORCE_GEN : term -> thm -> thm
val rename_bound_vars_rule : string -> thm -> thm
val clean_uppercase : string -> string
val prove_EvalPatRel : term -> (term -> thm) -> thm
val dest_pmatch_K_T : term -> term * (term * term) list
val dest_pmatch_row_K_T : term -> term * term
val is_pmatch : term -> bool
val to_pattern : term -> term
val pmatch_preprocess_conv : term -> thm
val register_term_types : (hol_type -> unit) -> term -> unit
val get_curr_v_defs : unit -> thm list
val get_pre_var : term -> string -> term
val ex_rename_bound_vars_rule : thm -> thm
val force_thm_the : thm option -> thm
val clean_precondition : thm -> thm
val quietDefine : term quotation -> thm
val derive_split : term -> thm
exception UnableToTranslate of term
val find_const_name : string -> string
val add_v_thms : string * string * thm * thm -> unit
val lookup_v_thm : term -> thm
val get_v_thms_ref : unit -> (string * string * term * thm * thm * string list) list ref
val remove_Eq_from_v_thm : thm -> thm
val clean_v_thms : unit -> unit
val filter_v_thms : ((string * string * term * thm * thm * string list) -> bool) -> int
(* Internal - handling type constructor names *)
val mk_cons_name : term -> string
val enter_cons_name : term * term -> string
val lookup_cons_name : string -> term * string list
val instantiate_cons_name : thm -> thm
val get_cons_names : unit -> (string * (term * string list)) list
(* Internal - for preprocess_monadic_def *)
val force_eqns : thm -> thm
val is_rec_def : thm -> bool
val mutual_to_single_line_def : thm -> thm list * thm option
val remove_pair_abs : thm -> thm
val get_preprocessor_rws : unit -> thm list
val AUTO_ETA_EXPAND_CONV : conv
val find_ind_thm : thm -> thm
val auto_prove : string -> term * tactic -> thm
(* for debugging *)
val pmatch_hol2deep_fail : term ref
val pmatch_hol2deep : term -> (term -> thm) -> thm
val prove_EvalPatBind_fail : term ref
val prove_EvalPatBind : term -> (term -> thm) -> thm
val prove_EvalPatRel_fail : term ref
val get_term :string -> term
val trace_timing_to : string option ref
(* returns the induction theorem for the latest rec translation *)
val latest_ind : unit -> thm
(* configure whether HOL_STRING_TYPE is to be used *)
val use_string_type : bool -> unit
(* configure whether sub_check is default for num subtraction *)
val use_sub_check : bool -> unit
end