diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/divDefLib.sml | 23 | ||||
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 67 |
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” |