summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/hol4/divDefLib.sml23
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml67
2 files changed, 49 insertions, 41 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index c9d8806d..128e0b0f 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -606,25 +606,9 @@ fun prove_body_is_valid_tac_step (asms, g) =
∃h y. is_valid_fp_body n h ∧ ∀g. ... g x = ... od
]}
*)
- (* Retrieve the scrutinee in the goal (‘x’).
- There are two cases:
- - either the function has the shape:
- {[
- (λ(y,z). ...) x
- ]}
- in which case we need to destruct ‘x’
- - or we have a normal ‘case ... of’
- *)
+ (* Retrieve the scrutinee in the goal (‘x’) *)
val body = (lhs o snd o strip_forall o fst o dest_disj) g
- val scrut =
- let
- val (app, x) = dest_comb body
- val (app, _) = dest_comb app
- val {Name=name, Thy=thy, Ty = _ } = dest_thy_const app
- in
- if thy = "pair" andalso name = "UNCURRY" then x else failwith "not a curried argument"
- end
- handle HOL_ERR _ => strip_all_cases_get_scrutinee body
+ val scrut = strip_all_cases_get_scrutinee_or_curried body
(* Retrieve the first quantified continuations from the goal (‘g’) *)
val qc = (hd o fst o strip_forall o fst o dest_disj) g
(* Check if the scrutinee is a recursive call *)
@@ -723,6 +707,7 @@ fun prove_body_is_valid (body : term) : thm =
(* Generate the lemma statement *)
val is_valid_tm = list_mk_icomb (is_valid_fp_body_tm, [n_tm, body])
+
val is_valid_thm = prove (is_valid_tm, prove_body_is_valid_tac NONE)
(* Replace ‘nvar’ with ‘0’ *)
val is_valid_thm = INST [nvar |-> zero_num_tm] is_valid_thm
@@ -902,7 +887,7 @@ fun DefineDiv (def_qt : term quotation) =
(* Because [store_definition] overrides existing names, it seems that in
practice we don't really need to delete the previous definitions
(we still do it: it doesn't cost much). *)
- val _ = app delete_binding thm_names
+ val _ = List.app delete_binding thm_names
val _ = map store_definition (zip thm_names def_eqs)
(* Also save the custom unfoldings, for evaluation (unit tests) *)
val _ = evalLib.add_unfold_thms thm_names
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 143e25ce..d19903b1 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -640,36 +640,59 @@ fun int_tac (asms, g) =
first_tac [cooper_tac, exfalso >- cooper_tac]) (asms, g)
end
+(* Remark.: [strip_case] is too smart for what we want.
+ For instance: (fst o strip_case) “if i = 0 then ... else ...”
+ returns “i” while we want to get “i = 0”.
+
+ Also, [dest_case] sometimes fails.
+
+ Ex.:
+ {[
+ val t = “result_CASE (if T then Return 0 else Fail Failure) (λy. Return ()) Fail Diverge”
+ dest_case t
+ ]}
+ TODO: file an issue
+
+ We use a custom function [get_case_scrutinee] instead of [dest_case] for this reason.
+ *)
+fun get_case_scrutinee t =
+ let
+ val (_, tms) = strip_comb t
+ in
+ hd tms
+ end
+
(* Repeatedly destruct cases and return the last scrutinee we get *)
fun strip_all_cases_get_scrutinee (t : term) : term =
if TypeBase.is_case t
then
- (* Remark.: [strip_case] is too smart for what we want.
- For instance: (fst o strip_case) “if i = 0 then ... else ...”
- returns “i” while we want to get “i = 0”.
-
- Also, [dest_case] sometimes fails.
-
- Ex.:
- {[
- val t = “result_CASE (if T then Return 0 else Fail Failure) (λy. Return ()) Fail Diverge”
- dest_case t
- ]}
- TODO: file an issue
-
- We use a custom function [get_case_scrutinee] instead of [dest_case] for this reason.
- *)
+ (strip_all_cases_get_scrutinee o get_case_scrutinee) t
+ else t
+
+(* Same as [strip_all_cases_get_scrutinee *but* if at some point we reach term
+ of the shape:
+ {[
+ (λ(y,z). ...) x
+ ]}
+ then we return the ‘x’
+ *)
+fun strip_all_cases_get_scrutinee_or_curried (t : term) : term =
let
- fun get_case_scrutinee t =
+ (* Check if we have a term of the shape “(λ(y,z). ...) x” *)
+ val scrut =
let
- val (_, tms) = strip_comb t
+ val (app, x) = dest_comb t
+ val (app, _) = dest_comb app
+ val {Name=name, Thy=thy, Ty = _ } = dest_thy_const app
in
- hd tms
+ if thy = "pair" andalso name = "UNCURRY" then x else failwith "not a curried argument"
end
- in
- (strip_all_cases_get_scrutinee o get_case_scrutinee) t
- end
- else t
+ handle HOL_ERR _ =>
+ if TypeBase.is_case t
+ then
+ (strip_all_cases_get_scrutinee_or_curried o get_case_scrutinee) t
+ else t
+ in scrut end
(*
TypeBase.dest_case “case ls of [] => T | _ => F”