Tweak previous to acknowledge some vals

These are values whose type has been shadowed, instead of just being ignored, they get a dummy message.
CakeML · Jan 20, 2022 · 750cf68 · 750cf68
1 parent 9c67ac8
commit 750cf68
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 12 deletions.
diff --git a/basis/PrettyPrinterProgScript.sml b/basis/PrettyPrinterProgScript.sml
@@ -42,6 +42,7 @@ val res = tr "tuple" pp_paren_tuple_def;
 val res = tr "spaced_block" pp_spaced_block_def;
 val res = tr "app_block" pp_app_block_def;
 val res = tr "val_eq" pp_val_eq_def;
+val res = tr "val_hidden_type" pp_val_hidden_type_def;
 
 val res = translate pp_list_def;
 val res = translate pp_bool_def;

diff --git a/basis/pure/mlprettyprinterScript.sml b/basis/pure/mlprettyprinterScript.sml
@@ -71,15 +71,14 @@ End
 
 Definition pp_val_eq_def:
   pp_val_eq nm pp_f v = pp_app_block (strlit "val")
-    [ppd_token (implode nm); ppd_token (strlit "="); pp_f v]
+    [ppd_token (implode nm); ppd_token (strlit "="); pp_f v; ppd_token ("\n")]
 End
 
-Definition pp_val_eq_def:
-  pp_val_eq nm pp_f v = pp_app_block (strlit "val")
-    [ppd_token (implode nm); ppd_token (strlit "="); pp_f v]
+Definition pp_val_hidden_type_def:
+  pp_val_hidden_type nm = pp_app_block (strlit "val")
+    [ppd_token (implode nm); ppd_token (strlit ": <hidden type>\n")]
 End
 
-
 Definition pp_list_def:
   pp_list f xs = PP_Data F (app_list_wrap (strlit "[")
     (app_intersperse (strlit "; ") (MAP (\x. ppd_contents (f x)) xs))

diff --git a/compiler/printing/addPrintValsScript.sml b/compiler/printing/addPrintValsScript.sml
@@ -74,13 +74,13 @@ Definition id_str_def:
 End
 
 Definition print_of_val_def:
-  print_of_val tn (nm, inf_t) = (case inf_t_to_ast_t tn inf_t of
-      NONE => []
-    | SOME ast_t =>
-    [Dlet unknown_loc Pany (App Opapp [Var (Short "print_pp");
-        rpt_app (Var (Long "PrettyPrinter" (Short "val_eq")))
-            [Lit (StrLit (id_str nm)); pp_of_ast_t ast_t; Var nm]])]
-  )
+  print_of_val tn (nm, inf_t) =
+    let idl = Lit (StrLit (id_str nm)) in
+    Dlet unknown_loc Pany (App Opapp [Var (Short "print_pp");
+        (case inf_t_to_ast_t tn inf_t of
+          NONE => App Opapp [Var (Long "PrettyPrinter" (Short "val_hidden_type")); idl]
+        | SOME ast_t => rpt_app (Var (Long "PrettyPrinter" (Short "val_eq")))
+            [idl; pp_of_ast_t ast_t; Var nm])])
 End
 
 Definition val_prints_def: