From 057f68ea639c52c33cff36017fc3f1365503934b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 23 May 2023 12:31:54 +0200
Subject: Fix some minor issues

---
 backends/hol4/divDefLib.sml            | 23 ++----------
 backends/hol4/primitivesBaseTacLib.sml | 67 +++++++++++++++++++++++-----------
 2 files changed, 49 insertions(+), 41 deletions(-)

(limited to 'backends')

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”
-- 
cgit v1.2.3