# HG changeset patch
# User haftmann
# Date 1648139675 0
# Node ID a2c5efb7298ae90e7c2c16169f598baadda03d68
# Parent  8fcf5770863633951f662de545f2ac901764e783
disentangled

diff -r 8fcf57708636 -r a2c5efb7298a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Mar 23 20:26:33 2022 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:35 2022 +0000
@@ -53,6 +53,7 @@
   val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
   val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
+  val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val is_IVar: iterm -> bool
   val is_IAbs: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
@@ -78,7 +79,6 @@
   type program = stmt Code_Symbol.Graph.T
   val unimplemented: program -> string list
   val implemented_deps: program -> string list
-  val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_constr: program -> Code_Symbol.T -> bool
   val is_case: stmt -> bool
@@ -268,6 +268,17 @@
       (Name.invent_names vars "a" ((take l o drop j) tys));
   in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
 
+fun map_terms_bottom_up f (t as IConst _) = f t
+  | map_terms_bottom_up f (t as IVar _) = f t
+  | map_terms_bottom_up f (t1 `$ t2) = f
+      (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
+  | map_terms_bottom_up f ((v, ty) `|=> t) = f
+      ((v, ty) `|=> map_terms_bottom_up f t)
+  | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
+      (ICase { term = map_terms_bottom_up f t, typ = ty,
+        clauses = (map o apply2) (map_terms_bottom_up f) clauses,
+        primitive = map_terms_bottom_up f t0 });
+
 fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
 and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss
   | exists_plain_dict_var_pred f (Dict_Var x) = f x
@@ -308,17 +319,6 @@
   |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
   |> map_filter (fn Constant c => SOME c | _ => NONE);
 
-fun map_terms_bottom_up f (t as IConst _) = f t
-  | map_terms_bottom_up f (t as IVar _) = f t
-  | map_terms_bottom_up f (t1 `$ t2) = f
-      (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
-  | map_terms_bottom_up f ((v, ty) `|=> t) = f
-      ((v, ty) `|=> map_terms_bottom_up f t)
-  | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
-      (ICase { term = map_terms_bottom_up f t, typ = ty,
-        clauses = (map o apply2) (map_terms_bottom_up f) clauses,
-        primitive = map_terms_bottom_up f t0 });
-
 fun map_classparam_instances_as_term f =
   (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')