search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

FStar.Char: move type into smaller FStar.Char.Type module #3408

Open mtzguido opened 2 months ago

mtzguido commented 2 months ago

This reduces the dependencies that clients take on just for mentioning the char type or a character literal. Currently this brings in a lot to just check a module with let x = 'a':

Now lax-checking implementation of FStar.Pervasives.Native
Now lax-checking interface of FStar.Pervasives
Now lax-checking implementation of FStar.Mul
Now lax-checking interface of FStar.Classical
Now lax-checking implementation of FStar.StrongExcludedMiddle
Now lax-checking interface of FStar.Classical.Sugar
Now lax-checking implementation of FStar.List.Tot.Base
Now lax-checking implementation of FStar.List.Tot
Now lax-checking interface of FStar.Seq.Base
Now lax-checking interface of FStar.Seq.Properties
Now lax-checking implementation of FStar.Seq
Now lax-checking interface of FStar.Math.Lemmas
Now lax-checking implementation of FStar.BitVector
Now lax-checking interface of FStar.UInt32
Now lax-checking interface of FStar.Char

With this PR:

Now lax-checking implementation of FStar.Pervasives.Native
Now lax-checking interface of FStar.Pervasives
Now lax-checking interface of FStar.Char.Type
mtzguido commented 2 months ago

This requires the following krml patch:

diff --git a/include/krml/internal/types.h b/include/krml/internal/types.h
index e41b39be..71e8733f 100644
--- a/include/krml/internal/types.h
+++ b/include/krml/internal/types.h
@@ -28,7 +28,7 @@ typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
 typedef int64_t FStar_Int63_t, FStar_Int63_t_;

 typedef double FStar_Float_float;
-typedef uint32_t FStar_Char_char;
+typedef uint32_t FStar_Char_Type_char;
 typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;

 typedef void *FStar_Dyn_dyn;
diff --git a/krmllib/c/fstar_char.c b/krmllib/c/fstar_char.c
index f6931522..669220cc 100644
--- a/krmllib/c/fstar_char.c
+++ b/krmllib/c/fstar_char.c
@@ -3,6 +3,6 @@

 #include "FStar_Char.h"

-FStar_Char_char FStar_Char_char_of_u32(uint32_t x) {
+FStar_Char_Type_char FStar_Char_Type_char_of_u32(uint32_t x) {
   return x;
 }
diff --git a/krmllib/c/fstar_string.c b/krmllib/c/fstar_string.c
index 1117bfa2..7e920134 100644
--- a/krmllib/c/fstar_string.c
+++ b/krmllib/c/fstar_string.c
@@ -28,7 +28,7 @@ Prims_string FStar_String_strcat(Prims_string s0, Prims_string s1) {
 }

-krml_checked_int_t FStar_String_index_of(Prims_string s1, FStar_Char_char fc) {
+krml_checked_int_t FStar_String_index_of(Prims_string s1, FStar_Char_Type_char fc) {
   if (fc > 127) {
     KRML_HOST_PRINTF("FStar.Char.char overflow at %s:%d\n", __FILE__, __LINE__);
     KRML_HOST_EXIT(252);
diff --git a/krmllib/c/lowstar_printf.c b/krmllib/c/lowstar_printf.c
index 409dfbf1..91a8a4ab 100644
--- a/krmllib/c/lowstar_printf.c
+++ b/krmllib/c/lowstar_printf.c
@@ -17,7 +17,7 @@
   PRINTB(N, T, M2)

 PRINT2 (string, Prims_string, "s", "s")
-PRINT2 (char, FStar_Char_char, PRIu32, PRIx32)
+PRINT2 (char, FStar_Char_Type_char, PRIu32, PRIx32)
 PRINT2 (u8, uint8_t, PRIu8, PRIx8)
 PRINT2 (u16, uint16_t, PRIu16, PRIx16)
 PRINT2 (u32, uint32_t, PRIu32, PRIx32)
gebner commented 2 months ago

This reduces the dependencies that clients take on just for mentioning the char type or a character literal. Currently this brings in a lot to just check a module with let x = 'a':

Now lax-checking implementation of FStar.Pervasives.Native
Now lax-checking interface of FStar.Pervasives
Now lax-checking implementation of FStar.Mul
Now lax-checking interface of FStar.Classical
Now lax-checking implementation of FStar.StrongExcludedMiddle
Now lax-checking interface of FStar.Classical.Sugar
Now lax-checking implementation of FStar.List.Tot.Base
Now lax-checking implementation of FStar.List.Tot
Now lax-checking interface of FStar.Seq.Base
Now lax-checking interface of FStar.Seq.Properties
Now lax-checking implementation of FStar.Seq
Now lax-checking interface of FStar.Math.Lemmas
Now lax-checking implementation of FStar.BitVector
Now lax-checking interface of FStar.UInt32
Now lax-checking interface of FStar.Char

FWIW, we could eliminate the Classical.Sugar dependency by adding an interface to FStar.List.Tot.Base.fst (which includes proofs right now!).

mtzguido commented 2 months ago

Good point! I did this for List.Tot.Properties yesterday but didn't do Base yet. It was a bit of pain, wondering if we can do something more systematic to, say, find proofs in fstis and/or infer an interface for a module.

gebner commented 2 months ago

I'm not sure if it's worth it to automate the interface-generation step, but I think a reasonable policy would be that interfaces shouldn't depend on "proof modules":

❯ fstar.exe --dep make {,experimental/}*.fsti 2>/dev/null | grep -v 'Tactics.*:' | rg '\.fsti:.*(Classical|Lemmas)'
FStar.GSet.fsti: FStar.Classical.fsti FStar.Set.fsti FStar.Pervasives.fsti prims.fst
FStar.GhostSet.fsti: FStar.Classical.fsti FStar.Set.fsti FStar.Pervasives.fsti prims.fst
LowStar.Literal.fsti: FStar.Pervasives.Native.fst FStar.Map.fsti FStar.Set.fsti FStar.Seq.fst FStar.Int.Cast.Full.fst FStar.Math.Lemmas.fsti FStar.UInt8.fsti FStar.String.fsti FStar.List.Tot.fst FStar.UInt32.fsti FStar.Char.fsti FStar.Mul.fst FStar.HyperStack.ST.fsti FStar.HyperStack.fst LowStar.ImmutableBuffer.fst LowStar.Buffer.fst FStar.Pervasives.fsti prims.fst
FStar.Modifies.fsti: FStar.ModifiesGen.fsti FStar.Map.fsti FStar.Heap.fst FStar.Pervasives.Native.fst FStar.Classical.fsti FStar.UInt32.fsti FStar.Preorder.fst FStar.Set.fsti /home/gebner/FStar/ulib/legacy/FStar.Buffer.fst FStar.HyperStack.ST.fsti FStar.HyperStack.fst FStar.Pervasives.fsti prims.fst
FStar.Endianness.fsti: FStar.Mul.fst FStar.Seq.fst FStar.Math.Lemmas.fsti FStar.UInt64.fsti FStar.UInt32.fsti FStar.UInt8.fsti FStar.Pervasives.fsti prims.fst
FStar.UInt.fsti: FStar.Seq.Base.fsti FStar.Math.Lemmas.fsti FStar.BitVector.fsti FStar.Mul.fst FStar.Pervasives.fsti prims.fst
FStar.Matrix.fsti: FStar.Classical.fsti FStar.Mul.fst FStar.IntegerIntervals.fst FStar.Math.Lemmas.fsti FStar.Seq.Base.fsti FStar.Seq.Permutation.fsti FStar.Algebra.CommMonoid.Fold.fsti FStar.Algebra.CommMonoid.Equiv.fst FStar.Pervasives.fsti prims.fst
FStar.Int.fsti: FStar.Seq.fst FStar.UInt.fsti FStar.Math.Lemmas.fsti FStar.BitVector.fsti FStar.Mul.fst FStar.Pervasives.fsti prims.fst