Merge pull request #2883 from FStarLang/guido_deps

Reducing some dependencies from the compiler into ulib

.scripts/README.md

@@ -34,4 +34,9 @@ In this folder, the following scripts are in use or can be used:
 
     + to test the Windows binary package created by the workflow
 
+* `simpl_graph.py`: this script simplifies a DOT-format graph (such as
+the one output by `fstar.exe --dep graph` by removing its transitive
+dependencies. This allows for a much better visualization. It is used by
+the `depgraph.pdf` rule in `src/Makefile.boot`.
+
 (TODO: expand this list)

.scripts/simpl_graph.py

@@ -0,0 +1,55 @@
+#!/usr/bin/env python3
+
+from parse import parse
+import sys
+
+def add(adj, m, n):
+    adj[m,n] = True
+
+def redundant(adj, nodes, i, j):
+    for k in nodes:
+        if k == i or k == j: continue
+        if adj.get((i,k), False) and adj.get((k,j), False):
+            return True
+
+    return False
+
+# Assumes the graph is already transitive
+def simpl (adj):
+    new_adj = {}
+    nodes = []
+    for (i, j) in adj.keys():
+        nodes.append(i)
+        nodes.append(j)
+
+    for (i, j) in adj.keys():
+        if i == j: continue
+        if redundant(adj, nodes, i ,j): continue
+        new_adj[i,j] = True
+
+    return new_adj
+
+def output (adj):
+    print ("digraph{")
+    for (i, j) in adj.keys():
+        print ("  \"{0}\" -> \"{1}\"".format(i, j))
+    print ("}")
+
+def parse_graph(fname):
+    adj = {}
+    f = open(fname, 'r')
+    lines = f.readlines()
+    for line in lines:
+        try:
+            # Brittle, FIXME
+            res = parse("  \"{}\" -> \"{}\"\n", line)
+            (i,j) = res.fixed
+            add(adj, i, j)
+        except AttributeError:
+            pass
+    return adj
+
+file = sys.argv[1]
+graph = parse_graph(file)
+graph2 = simpl(graph)
+output(graph2)

examples/crypto/HyE.RSA.fst

@@ -27,7 +27,6 @@
 
 module HyE.RSA
 
-open FStar.BaseTypes
 open FStar.List.Tot
 
 open Platform.Bytes

examples/crypto/attic/CCA2.RSA.fst

@@ -27,6 +27,8 @@ module CCA2.RSA
 open FStar.BaseTypes
 open FStar.List.Tot
 
+open FStar.UInt8
+
 assume type pkey
 assume type skey
 type bytes = list byte

examples/native_tactics/Pruning.fst

@@ -18,7 +18,6 @@ module Pruning
 open FStar.Algebra.Monoid
 open FStar.Array
 open FStar.Axiomatic.Array
-open FStar.BaseTypes
 open FStar.BitVector
 open FStar.Bytes
 open FStar.Char

examples/vale/X64.Semantics_s.fst

@@ -15,7 +15,6 @@
 *)
 module X64.Semantics_s
 
-open FStar.BaseTypes
 open X64.Machine_s
 
 module F = FStar.FunctionalExtensionality

src/.gitignore

@@ -6,6 +6,8 @@ u_boot_fsts
 u_ocaml-output
 
 dep.graph
+dep_simpl.graph
+depgraph.pdf
 
 [Bb]in/
 [Oo]bj/

src/Makefile.boot

@@ -90,14 +90,26 @@ EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES))		\
 	$(call msg, "DEPEND")
 	$(Q)$(FSTAR_C) --dep full		\
 		fstar/FStar.Main.fst		\
-		boot/FStar.Tests.Test.fst	\
+		tests/FStar.Tests.Test.fst	\
 		--odir $(OUTPUT_DIRECTORY)	\
 		$(EXTRACT)			> ._depend
 	@# We've generated deps for everything into fstar-lib/generated.
 	@# Here we fix up the .depend file to move tests out of the library.
 	$(Q)$(SED) 's,fstar-lib/generated/FStar_Test,fstar-tests/generated/FStar_Test,g' <._depend >.depend
 	$(Q)mkdir -p $(CACHE_DIR)
 
+.PHONY: depgraph.pdf
+depgraph.pdf :
+	$(call msg, "DEPEND")
+	$(Q)$(FSTAR_C) --dep graph\
+		fstar/FStar.Main.fst		\
+		tests/FStar.Tests.Test.fst	\
+		--odir $(OUTPUT_DIRECTORY)	\
+		$(EXTRACT)
+	$(Q)$(FSTAR_HOME)/.scripts/simpl_graph.py dep.graph > dep_simpl.graph
+	$(call msg, "DOT", $@)
+	$(Q)dot -Tpdf -o $@ dep_simpl.graph
+
 depend: .depend
 
 include .depend

src/Makefile.boot.common

@@ -5,20 +5,17 @@
 INCLUDE_PATHS = \
 	../ulib \
 	basic \
-	basic/boot \
 	extraction \
 	fstar \
 	parser \
 	prettyprint \
-	prettyprint/boot \
 	reflection \
 	smtencoding \
 	syntax \
 	tactics \
 	tosyntax \
 	typechecker \
-	tests \
-	tests/boot
+	tests
 
 CACHE_DIR?=$(FSTAR_HOME)/src/.cache.boot
 

ulib/FStar.BaseTypes.fsti → src/basic/FStar.BaseTypes.fsti

@@ -1,5 +1,5 @@
 (*
-   Copyright 2008-2018 Microsoft Research
+   Copyright 2008-2023 Microsoft Research
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.
@@ -20,15 +20,14 @@ module FStar.BaseTypes
 /// a single module, providing abbreviations for them.
 
 type char = FStar.Char.char
-type float = FStar.Float.float
-type double = FStar.Float.double
-type byte = FStar.UInt8.byte
-type int8 = FStar.Int8.t
-type uint8 = FStar.UInt8.t
-type int16 = FStar.Int16.t
-type uint16 = FStar.UInt16.t
-type int32 = FStar.Int32.t
-type uint32 = FStar.UInt32.t
-type int64 = FStar.Int64.t
-type uint64 = FStar.UInt64.t
-
+type float
+type double
+type byte
+type int8
+type uint8
+type int16
+type uint16
+type int32
+type uint32
+type int64
+type uint64

src/basic/FStar.Char.fsti

@@ -0,0 +1,32 @@
+(*
+   Copyright 2008-2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.Char
+
+(* This is a trimmed-down version of ulib/FStar.Char, realized by the
+same ML implementation. It is here to prevent dependencies from the
+compiler into the UInt32 module. *)
+
+new
+val char:eqtype
+
+type char_code
+
+val int_of_char : char -> Tot int
+val char_of_int : int -> Tot char
+
+val lowercase: char -> Tot char
+val uppercase: char -> Tot char

src/parser/FStar.Parser.Dep.fst

@@ -383,9 +383,11 @@ let dependences_of (file_system_map:files_for_module_name)
       |> List.filter (fun k -> k <> fn) (* skip current module, cf #451 *)
 
 let print_graph (graph:dependence_graph) =
-  Util.print_endline "A DOT-format graph has been dumped in the current directory as dep.graph";
-  Util.print_endline "With GraphViz installed, try: fdp -Tpng -odep.png dep.graph";
-  Util.print_endline "Hint: cat dep.graph | grep -v _ | grep -v prims";
+  if not (Options.silent ()) then begin
+    Util.print_endline "A DOT-format graph has been dumped in the current directory as dep.graph";
+    Util.print_endline "With GraphViz installed, try: fdp -Tpng -odep.png dep.graph";
+    Util.print_endline "Hint: cat dep.graph | grep -v _ | grep -v prims"
+  end;
   Util.write_file "dep.graph" (
     "digraph {\n" ^
     String.concat "\n" (List.collect

src/syntax/FStar.Syntax.Hash.fst

@@ -84,8 +84,6 @@ let hash_pair (h:'a -> mm H.hash_code) (i:'b -> mm H.hash_code) (x:('a * 'b))
   : mm H.hash_code
   = mix (h (fst x)) (i (snd x))
 
-let hash_byte (b:FStar.BaseTypes.byte) : mm H.hash_code = ret (H.of_int (UInt8.v b))
-
 let rec hash_term (t:term)
   : mm H.hash_code
   = maybe_memoize t hash_term'
@@ -240,7 +238,7 @@ and hash_constant =
   | Const_int (s, o) -> mix (of_int 313)
                              (mix (of_string s)
                                     (hash_option hash_sw o))
-  | Const_char c -> mix (of_int 317) (of_int (UInt32.v (Char.u32_of_char c)))
+  | Const_char c -> mix (of_int 317) (of_int (Char.int_of_char c))
   | Const_real s -> mix (of_int 337) (of_string s)
   | Const_string (s, _) -> mix (of_int 349) (of_string s)
   | Const_range_of -> of_int 353

tests/ide/lsp/nonexisting_dependency.in

@@ -1,6 +1,6 @@
-Content-Length: 3960
+Content-Length: 3938
 
-{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///root/non-existing/fstar/FStar/src/basic/FStar.Const.fst","languageId":"fstar","version":1,"text":"(*\n   Copyright 2008-2020 Microsoft Research\n\n   Licensed under the Apache License, Version 2.0 (the \"License\");\n   you may not use this file except in compliance with the License.\n   You may obtain a copy of the License at\n\n       http://www.apache.org/licenses/LICENSE-2.0\n\n   Unless required by applicable law or agreed to in writing, software\n   distributed under the License is distributed on an \"AS IS\" BASIS,\n   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n   See the License for the specific language governing permissions and\n   limitations under the License.\n*)\nmodule FStar.Const\nopen FStar.Compiler.Effect module List = FStar.Compiler.List\nopen FStar.Compiler.Effect module List = FStar.Compiler.List\n\nopen FStar.BaseTypes\n\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype signedness = | Unsigned | Signed\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype width = | Int8 | Int16 | Int32 | Int64\n\n(* NB:\n    Const_int (_, None) is not a canonical representation for a mathematical integer\n    e.g., you can have both\n    Const_int(\"0x3ffffff\", None)\n    and\n    Const_int(\"67108863\", None)\n    which represent the same number\n    You should do an \"FStar.Compiler.Util.ensure_decimal\" on the\n    string representation before comparing integer constants.\n\n    eq_const below does that for you\n*)\n\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype sconst =\n  | Const_effect\n  | Const_unit\n  | Const_bool        of bool\n  | Const_int         of string * option (signedness * width) (* When None, means \"mathematical integer\", i.e. Prims.int. *)\n  | Const_char        of char (* unicode code point: char in F#, int in OCaml *)\n  | Const_float       of double\n  | Const_real        of string\n  | Const_bytearray   of array byte * FStar.Compiler.Range.range\n  | Const_string      of string * FStar.Compiler.Range.range                (* UTF-8 encoded *)\n  | Const_range_of                                           (* `range_of` primitive *)\n  | Const_set_range_of                                       (* `set_range_of` primitive *)\n  | Const_range       of FStar.Compiler.Range.range                         (* not denotable by the programmer *)\n  | Const_reify                                              (* a coercion from a computation to a Tot term *)\n  | Const_reflect     of Ident.lid                           (* a coercion from a Tot term to an l-computation type *)\n\nlet eq_const c1 c2 =\n    match c1, c2 with\n    | Const_int (s1, o1), Const_int(s2, o2) ->\n      FStar.Compiler.Util.ensure_decimal s1 = FStar.Compiler.Util.ensure_decimal s2 &&\n      o1=o2\n    | Const_bytearray(a, _), Const_bytearray(b, _) -> a=b\n    | Const_string(a, _), Const_string(b, _) -> a=b\n    | Const_reflect l1, Const_reflect l2 -> Ident.lid_equals l1 l2\n    | _ -> c1=c2\n\nopen FStar.BigInt\nlet rec pow2 (x:bigint) : bigint =\n  if eq_big_int x zero\n  then one\n  else mult_big_int two (pow2 (pred_big_int x))\n\n\nlet bounds signedness width =\n    let n =\n        match width with\n        | Int8 -> big_int_of_string \"8\"\n        | Int16 -> big_int_of_string \"16\"\n        | Int32 -> big_int_of_string \"32\"\n        | Int64 -> big_int_of_string \"64\"\n    in\n    let lower, upper =\n      match signedness with\n      | Unsigned ->\n        zero, pred_big_int (pow2 n)\n      | Signed ->\n        let upper = pow2 (pred_big_int n) in\n        minus_big_int upper, pred_big_int upper\n    in\n    lower, upper\n\nlet within_bounds repr signedness width =\n  let lower, upper = bounds signedness width in\n  let value = big_int_of_string (FStar.Compiler.Util.ensure_decimal repr) in\n  le_big_int lower value && le_big_int value upper\n"}}}
+{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///root/non-existing/fstar/FStar/src/basic/FStar.Const.fst","languageId":"fstar","version":1,"text":"(*\n   Copyright 2008-2020 Microsoft Research\n\n   Licensed under the Apache License, Version 2.0 (the \"License\");\n   you may not use this file except in compliance with the License.\n   You may obtain a copy of the License at\n\n       http://www.apache.org/licenses/LICENSE-2.0\n\n   Unless required by applicable law or agreed to in writing, software\n   distributed under the License is distributed on an \"AS IS\" BASIS,\n   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n   See the License for the specific language governing permissions and\n   limitations under the License.\n*)\nmodule FStar.Const\nopen FStar.Compiler.Effect module List = FStar.Compiler.List\nopen FStar.Compiler.Effect module List = FStar.Compiler.List\n\n\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype signedness = | Unsigned | Signed\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype width = | Int8 | Int16 | Int32 | Int64\n\n(* NB:\n    Const_int (_, None) is not a canonical representation for a mathematical integer\n    e.g., you can have both\n    Const_int(\"0x3ffffff\", None)\n    and\n    Const_int(\"67108863\", None)\n    which represent the same number\n    You should do an \"FStar.Compiler.Util.ensure_decimal\" on the\n    string representation before comparing integer constants.\n\n    eq_const below does that for you\n*)\n\n// IN F*: [@@ PpxDerivingYoJson; PpxDerivingShow ]\ntype sconst =\n  | Const_effect\n  | Const_unit\n  | Const_bool        of bool\n  | Const_int         of string * option (signedness * width) (* When None, means \"mathematical integer\", i.e. Prims.int. *)\n  | Const_char        of char (* unicode code point: char in F#, int in OCaml *)\n  | Const_float       of double\n  | Const_real        of string\n  | Const_bytearray   of array byte * FStar.Compiler.Range.range\n  | Const_string      of string * FStar.Compiler.Range.range                (* UTF-8 encoded *)\n  | Const_range_of                                           (* `range_of` primitive *)\n  | Const_set_range_of                                       (* `set_range_of` primitive *)\n  | Const_range       of FStar.Compiler.Range.range                         (* not denotable by the programmer *)\n  | Const_reify                                              (* a coercion from a computation to a Tot term *)\n  | Const_reflect     of Ident.lid                           (* a coercion from a Tot term to an l-computation type *)\n\nlet eq_const c1 c2 =\n    match c1, c2 with\n    | Const_int (s1, o1), Const_int(s2, o2) ->\n      FStar.Compiler.Util.ensure_decimal s1 = FStar.Compiler.Util.ensure_decimal s2 &&\n      o1=o2\n    | Const_bytearray(a, _), Const_bytearray(b, _) -> a=b\n    | Const_string(a, _), Const_string(b, _) -> a=b\n    | Const_reflect l1, Const_reflect l2 -> Ident.lid_equals l1 l2\n    | _ -> c1=c2\n\nopen FStar.BigInt\nlet rec pow2 (x:bigint) : bigint =\n  if eq_big_int x zero\n  then one\n  else mult_big_int two (pow2 (pred_big_int x))\n\n\nlet bounds signedness width =\n    let n =\n        match width with\n        | Int8 -> big_int_of_string \"8\"\n        | Int16 -> big_int_of_string \"16\"\n        | Int32 -> big_int_of_string \"32\"\n        | Int64 -> big_int_of_string \"64\"\n    in\n    let lower, upper =\n      match signedness with\n      | Unsigned ->\n        zero, pred_big_int (pow2 n)\n      | Signed ->\n        let upper = pow2 (pred_big_int n) in\n        minus_big_int upper, pred_big_int upper\n    in\n    lower, upper\n\nlet within_bounds repr signedness width =\n  let lower, upper = bounds signedness width in\n  let value = big_int_of_string (FStar.Compiler.Util.ensure_decimal repr) in\n  le_big_int lower value && le_big_int value upper\n"}}}
 Content-Length: 46
 
-{"jsonrpc":"2.0","method":"exit","params":{}}
+{"jsonrpc":"2.0","method":"exit","params":{}}

tests/micro-benchmarks/Pruning.fst

@@ -19,7 +19,6 @@ module Pruning
 open FStar.Algebra.Monoid
 open FStar.Array
 open FStar.Axiomatic.Array
-open FStar.BaseTypes
 open FStar.BitVector
 open FStar.Bytes
 open FStar.Char

tests/micro-benchmarks/Unit1.Basic.fst

@@ -15,7 +15,7 @@
 *)
 module Unit1.Basic
 open FStar.All
-open FStar.BaseTypes
+open FStar.Char
 
 type t =
   | A

tests/micro-benchmarks/Unit1.Projectors1.fst

@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module Unit1.Projectors1
-open FStar.BaseTypes
+open FStar.Char
 
 type t = 
   | T : x:int -> y:nat -> t

tests/tactics/Pruning.fst

@@ -18,7 +18,6 @@ module Pruning
 open FStar.Algebra.Monoid
 open FStar.Array
 open FStar.Axiomatic.Array
-open FStar.BaseTypes
 open FStar.BitVector
 open FStar.Bytes
 open FStar.Char

ulib/Makefile

@@ -43,7 +43,7 @@ clean: clean_checked
 
 DOC_FILES=prims.fst FStar.Pervasives.Native.fst FStar.Pervasives.fst \
 	  FStar.Squash.fsti FStar.Classical.fsti FStar.BigOps.fsti \
-	  FStar.BaseTypes.fsti FStar.BitVector.fst FStar.BV.fsti \
+	  FStar.BitVector.fst FStar.BV.fsti \
 	  FStar.Char.fsti FStar.Date.fsti FStar.DependentMap.fsti \
 	  FStar.Dyn.fsti FStar.Exn.fst FStar.Fin.fst FStar.Float.fsti \
 	  FStar.FunctionalExtensionality.fsti FStar.Float.fsti \