-
Notifications
You must be signed in to change notification settings - Fork 5
/
hardwarePreamble.sml
112 lines (83 loc) · 3.29 KB
/
hardwarePreamble.sml
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
structure hardwarePreamble = struct
(* basic *)
open HolKernel Parse boolLib bossLib BasicProvers;
(* Additional *)
open listTheory wordsTheory;
open numLib wordsLib mp_then;
open hardwareMiscTheory;
(* Borrowed from cakeml: *)
val rveq = rpt BasicProvers.VAR_EQ_TAC;
val asm_exists_tac = goal_assum drule;
val asm_exists_any_tac = goal_assum (first_assum o mp_then Any mp_tac);
(* Handle multiple goals at the same time: *)
fun op THEN2 (tac1, tac2) = tac1 THEN1 tac2 THEN1 tac2;
infix THEN2;
fun op THEN3 (tac1, tac2) = tac1 THEN2 tac2 THEN1 tac2;
infix THEN3;
fun op THEN4 (tac1, tac2) = tac1 THEN3 tac2 THEN1 tac2;
infix THEN4;
fun op THEN5 (tac1, tac2) = tac1 THEN4 tac2 THEN1 tac2;
infix THEN5;
fun op THEN6 (tac1, tac2) = tac1 THEN5 tac2 THEN1 tac2;
infix THEN6;
(* drule-based tactics *)
fun drule_strip_tac (g as (tms, tm)) = let
val tm = tm |> dest_imp |> fst |> strip_forall |> snd
in
if not (is_imp tm) orelse is_neg tm then
strip_tac g
else
FAIL_TAC "drule_strip_tac" g
end;
fun drule_strip th = drule th \\ rpt (disch_then drule) \\ TRY drule_strip_tac \\ rveq;
fun rev_drule_strip th = rev_drule th \\ rpt (disch_then drule) \\ TRY drule_strip_tac \\ rveq;
val drule_first = first_x_assum drule \\ rpt (disch_then drule) \\ TRY drule_strip_tac;
val drule_last = last_x_assum drule \\ rpt (disch_then drule) \\ TRY drule_strip_tac;
fun strip_disch_tac (g as (tms, tm)) =
if not (is_neg tm) andalso is_imp tm then
strip_tac g
else
FAIL_TAC "strip_disch_tac" g;
val strip_tac' = gen_tac ORELSE strip_disch_tac;
val f_equals_tac = rpt (AP_THM_TAC ORELSE AP_TERM_TAC);
fun flip f x y = f y x;
fun sing x = [x];
fun fst_map f = map (fn (fst, snd) => (f fst, snd));
fun snd_map f = map (fn (fst, snd) => (fst, f snd));
(* Filters list l by the list of bools in filterl, if true, keep element, otherwise, drop it *)
(* TODO: Should maybe raise something better *)
fun filter_by_list l filterl =
case (l, filterl) of
([], []) => []
| (x::xs, y::ys) => append (if y then [x] else []) (filter_by_list xs ys)
| (_, _) => raise Empty;
fun EVAL_PROVE tm = EVAL tm |> EQT_ELIM;
fun EVAL_MP th = let
val ant = th |> concl |> dest_imp |> fst |> EVAL_PROVE
in
MP th ant
end;
fun lookup x nil = failwith "Unknown key"
| lookup x ((k, v) :: ls) = if x = k then v else lookup x ls;
fun lookup_opt x [] = NONE
| lookup_opt x ((k, v) :: ls) = if x = k then SOME v else lookup_opt x ls;
(* lookup from for terms *)
fun lookup_term x nil = failwith "Unknown term"
| lookup_term x ((k, v) :: ls) = if identical x k then v else lookup_term x ls;
(* lookup from assoc list based on key sameness *)
fun lookup_same x nil = NONE
| lookup_same x ((k, v) :: ls) = if same_const x k then SOME v else lookup_same x ls;
(* TODO: This is the same as Lib.can? (Not sure!) *)
fun can f x = (f x; true) handle HOL_ERR _ => false;
fun ASM_CONV_RULE c = (CONV_RULE c) o (HYP_CONV_RULE (K true) c);
(*fun drule th =
first_assum(mp_tac o MATCH_MP (ONCE_REWRITE_RULE[GSYM AND_IMP_INTRO] th));*)
fun is_bool_type ty =
is_type ty andalso (ty |> dest_type |> fst) = "bool";
(* https://stackoverflow.com/a/33606353 *)
fun writeFile filename content =
let val fd = TextIO.openOut filename
val _ = TextIO.output (fd, content) handle e => (TextIO.closeOut fd; raise e)
val _ = TextIO.closeOut fd
in () end;
end