From e2411d65360182c73d007f0423154bf7aaa56ebe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Tue, 15 Oct 2024 09:14:44 +0200
Subject: [PATCH] cleanup: rename `forget_label` to `replace_label` (#75)

---
 src/core/DY.Core.Label.fst      |  6 +++---
 src/core/DY.Core.Trace.Base.fst | 11 ++++++++---
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/core/DY.Core.Label.fst b/src/core/DY.Core.Label.fst
index 894e6a3..59a4637 100644
--- a/src/core/DY.Core.Label.fst
+++ b/src/core/DY.Core.Label.fst
@@ -133,12 +133,12 @@ let intro_label_equal l1 l2 pf =
   reveal_opaque (`%can_flow) can_flow;
   reveal_opaque (`%is_corrupt) is_corrupt;
   introduce forall tr. l1.is_corrupt tr == l2.is_corrupt tr with (
-    pf (fmap_trace (forget_label unknown_label) tr);
+    pf (fmap_trace (replace_label unknown_label) tr);
     // These two lines prove surjectivity of `trace_forget_labels`
     // by showing that fmap_trace (forget_label public) is a right-inverse
     // (we could replace `public` with anything)
-    fmap_trace_compose (forget_label unknown_label) (forget_label ()) (forget_label ()) tr;
-    fmap_trace_identity (forget_label ()) tr;
+    fmap_trace_compose (replace_label unknown_label) forget_label forget_label tr;
+    fmap_trace_identity forget_label tr;
     FStar.PropositionalExtensionality.apply (l1.is_corrupt tr) (l2.is_corrupt tr)
   );
   assert(l1.is_corrupt `FStar.FunctionalExtensionality.feq` l2.is_corrupt);
diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst
index 27532e3..d0d4116 100644
--- a/src/core/DY.Core.Trace.Base.fst
+++ b/src/core/DY.Core.Trace.Base.fst
@@ -329,17 +329,22 @@ let rec fmap_trace f tr =
   | Snoc init last ->
     Snoc (fmap_trace f init) (fmap_trace_event f last)
 
-val forget_label:
+val replace_label:
   #a:Type -> #b:Type ->
   b ->
   a -> b
-let forget_label #a #b x _ = x
+let replace_label #a #b x _ = x
+
+val forget_label:
+  #a:Type ->
+  a -> unit
+let forget_label #a = replace_label ()
 
 val trace_forget_labels:
   trace ->
   trace_ unit
 let trace_forget_labels tr =
-  fmap_trace (forget_label ()) tr
+  fmap_trace forget_label tr
 
 val fmap_trace_identity:
   #a:Type ->