Merge pull request #4240 from mtzguido/cleanups

mtzguido · web-flow · commit fb53f0a6a8ff · 2026-05-02T20:22:50.000-07:00
Small cleanups
diff --git a/examples/layeredeffects/SimpleHeap.fst b/examples/layeredeffects/SimpleHeap.fst
@@ -3,7 +3,6 @@
 *)
 module SimpleHeap
 
-module S = FStar.Set
 module F = FStar.FunctionalExtensionality
 
 (** Internal cell type: stores a typed value *)
diff --git a/examples/layeredeffects/SimpleHeap.fsti b/examples/layeredeffects/SimpleHeap.fsti
@@ -7,7 +7,6 @@
 module SimpleHeap
 
 module S = FStar.Set
-module F = FStar.FunctionalExtensionality
 
 (** The heap type *)
 val heap : Type u#1
diff --git a/pulse/share/pulse/examples/EqualOrDisjoint.fst b/pulse/share/pulse/examples/EqualOrDisjoint.fst
@@ -1,8 +1,6 @@
 module EqualOrDisjoint
 #lang-pulse
 open Pulse.Lib.Pervasives
-module R = Pulse.Lib.Reference
-module TR = Pulse.Lib.Trade
 open Pulse.Lib.Trade
 open Pulse.Lib.Forall.Util
 
diff --git a/pulse/share/pulse/examples/Quicksort.Base.fst b/pulse/share/pulse/examples/Quicksort.Base.fst
@@ -19,7 +19,6 @@ module Quicksort.Base
 
 open Pulse.Lib.Pervasives
 module A = Pulse.Lib.Array
-module R = Pulse.Lib.Reference
 module SZ = FStar.SizeT
 (* Base module with proof of correctness of Quicksort, partition, etc.
 #lang-pulse
diff --git a/pulse/share/pulse/examples/by-example/PulseByExample.fst b/pulse/share/pulse/examples/by-example/PulseByExample.fst
@@ -49,7 +49,6 @@ fn five_alt ()
 
 open Pulse.Lib.Reference
 open Pulse.Class.PtsTo
-module R = Pulse.Lib.Reference
 
 (* 
   Things to note:
@@ -114,7 +113,6 @@ fn test (r:ref int)
 }
 
 open Pulse.Lib.Array
-module A = Pulse.Lib.Array
 module SZ = FStar.SizeT
 open Pulse.Lib.BoundedIntegers
 
diff --git a/pulse/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst b/pulse/share/pulse/examples/by-example/PulseTutorial.AtomicsAndInvariants.fst
@@ -17,7 +17,6 @@
 module PulseTutorial.AtomicsAndInvariants
 #lang-pulse
 open Pulse.Lib.Pervasives
-module T = FStar.Tactics
 module U32 = FStar.UInt32
 
 //owns$
diff --git a/pulse/share/pulse/examples/parallel/Example.SimpleDBModel.fst b/pulse/share/pulse/examples/parallel/Example.SimpleDBModel.fst
@@ -3,7 +3,6 @@ module Example.SimpleDBModel
 open Pulse.Lib.Pervasives
 open Pulse.Lib.GhostPCMReference
 open FStar.Preorder
-module GR = Pulse.Lib.GhostPCMReference
 module MR = Pulse.Lib.MonotonicGhostRef
 let as_prop (p:prop) = p <==> True
 // A tiny db
diff --git a/pulse/src/checker/Pulse.Checker.Match.fst b/pulse/src/checker/Pulse.Checker.Match.fst
@@ -28,7 +28,6 @@ module T = FStar.Tactics.V2
 module L = FStar.List.Tot.Base
 module R = FStar.Reflection.V2
 module RT = FStar.Reflection.Typing
-module RU = Pulse.RuntimeUtils
 
 let br_typing_vis (g:env) (_:universe) (_:typ) (_:term) (_:pattern) (_:st_term) (_:comp_st) : Type = unit
 
diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst
@@ -23,6 +23,7 @@ open FStarC.Ident
 open FStarC.CheckedFiles
 open FStarC.Universal
 open FStarC.Util
+open FStarC.Syntax.Print
 
 open FStarC.Hooks (* KEEP: we need this module for its top-level effect. *)
 
diff --git a/src/fstar/FStarC.Main.fsti b/src/fstar/FStarC.Main.fsti
@@ -0,0 +1,20 @@
+(*
+   Copyright 2008-2016 Nikhil Swamy and 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 FStarC.Main
+
+open FStarC.Effect
+
+val main : unit -> ML unit
diff --git a/src/fstar/FStarC.Universal.fst b/src/fstar/FStarC.Universal.fst
@@ -29,6 +29,7 @@ open FStarC.Dependencies
 open FStarC.Extraction.ML.UEnv
 open FStarC.TypeChecker.Env
 open FStarC.Syntax.DsEnv
+open FStarC.Syntax.Print
 open FStarC.TypeChecker
 open FStarC.CheckedFiles
 
diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst
@@ -30,6 +30,7 @@ open FStarC.SMTEncoding.Util
 open FStarC.SMTEncoding.Env
 open FStarC.SMTEncoding.EncodeTerm
 open FStarC.Class.Show
+open FStarC.Syntax.Print {}
 
 module BU     = FStarC.Util
 module Const  = FStarC.Parser.Const
diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fsti b/src/smtencoding/FStarC.SMTEncoding.Encode.fsti
@@ -36,4 +36,4 @@ val encode_query: option (unit -> ML string)
                 -> ML (list decl  //prelude, translation of tcenv
                   & list ErrorReporting.label //labels in the query
                   & decl        //the query itself
-                  & list decl)  //suffix, evaluating labels in the model, etc
+                  & list decl)  //suffix, evaluating labels in the model, etc
diff --git a/src/smtencoding/FStarC.SMTEncoding.Env.fst b/src/smtencoding/FStarC.SMTEncoding.Env.fst
@@ -63,19 +63,6 @@ let mk_term_projector_by_pos (lid:lident) (i:int) : ML term =
 let mk_data_tester env l x = mk_tester (escape (string_of_lid l)) x
 (* ------------------------------------ *)
 (* New name generation *)
-type varops_t = {
-    push: unit -> ML unit;
-    pop: unit -> ML unit;
-    snapshot: unit -> ML (int & unit);
-    rollback: option int -> ML unit;
-    new_var:ident -> int -> ML string; (* each name is distinct and has a prefix corresponding to the name used in the program text *)
-    new_fvar:lident -> ML string;
-    fresh:string -> string -> ML string;  (* module name -> prefix -> name *)
-    reset_fresh:unit -> ML unit;
-    next_id: unit -> ML int;
-    mk_unique:string -> ML string;
-    reset_scope: unit -> ML unit
-}
 let varops =
     let initial_ctr = 100 in
     let ctr = mk_ref initial_ctr in
@@ -123,17 +110,6 @@ let varops =
 (* Each entry maps a Syntax variable to its encoding as a SMT2 term *)
 (* free variables, depending on whether or not they are fully applied ...  *)
 (* ... are mapped either to SMT2 functions, or to nullary tokens *)
-type fvar_binding = {
-    fvar_lid:  lident;
-    univ_arity : int;
-    smt_arity: int;
-    smt_id:    string;
-    smt_token: option term;
-    smt_fuel_partial_app:option (term & term);
-    fvb_thunked: bool;
-    needs_fuel_and_universe_instantiations: option univ_names;
-}
-
 let list_of (i:int) (f:int -> ML 'a)
 : ML (list 'a)
 = let rec aux i out : ML _ =
@@ -206,21 +182,6 @@ let check_valid_fvb fvb =
 
 let binder_of_eithervar v = (v, None)
 
-type env_t = {
-    bvar_bindings: PSMap.t (PIMap.t (bv & term));
-    fvar_bindings: (PSMap.t fvar_binding & list fvar_binding);  //list of fvar bindings for the current module
-                                                                   //remember them so that we can store them in the checked file
-    depth:int; //length of local var/tvar bindings
-    tcenv:Env.env;
-    warn:bool;
-    nolabels:bool;
-    use_zfuel_name:bool;
-    encode_non_total_function_typ:bool;
-    current_module_name:string;
-    encoding_quantifier:bool;
-    global_cache:SMap.t (decls_elt & lident);  //cache for hashconsing, 2nd arg is the module name of the decl -- see Encode.fs where it is used and updated
-}
-
 let print_env (e:env_t) : ML string =
     let bvars = PSMap.fold e.bvar_bindings (fun _k pi acc ->
         PIMap.fold pi (fun _i (x, _term) acc ->
diff --git a/src/smtencoding/FStarC.SMTEncoding.Env.fsti b/src/smtencoding/FStarC.SMTEncoding.Env.fsti
@@ -0,0 +1,123 @@
+(*
+   Copyright 2008-2014 Nikhil Swamy and 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 FStarC.SMTEncoding.Env
+
+open FStarC
+open FStarC.Effect
+open FStarC.TypeChecker.Env
+open FStarC.Syntax
+open FStarC.Syntax.Syntax
+open FStarC.TypeChecker
+open FStarC.SMTEncoding.Term
+open FStarC.Ident
+open FStarC.SMTEncoding.Util
+
+open FStarC.Class.Show
+
+val add_fuel : 'a -> list 'a -> ML (list 'a)
+val withenv : 'c -> ('a & 'b) -> ('a & 'b & 'c)
+val vargs : list (either typ term & 'b) -> ML (list (either typ term & 'b))
+
+val escape : string -> string
+val mk_term_projector_name : lident -> bv -> ML string
+val mk_univ_projector_name : lident -> int -> ML string
+val primitive_projector_by_pos : Env.env -> lident -> int -> ML string
+val mk_term_projector_name_by_pos : lident -> int -> ML string
+val mk_term_projector : lident -> bv -> ML term
+val mk_term_projector_by_pos : lident -> int -> ML term
+val mk_data_tester : 'a -> lident -> term -> ML term
+
+type varops_t = {
+    push: unit -> ML unit;
+    pop: unit -> ML unit;
+    snapshot: unit -> ML (int & unit);
+    rollback: option int -> ML unit;
+    new_var:ident -> int -> ML string;
+    new_fvar:lident -> ML string;
+    fresh:string -> string -> ML string;
+    reset_fresh:unit -> ML unit;
+    next_id: unit -> ML int;
+    mk_unique:string -> ML string;
+    reset_scope: unit -> ML unit
+}
+
+val varops : varops_t
+
+type fvar_binding = {
+    fvar_lid:  lident;
+    univ_arity : int;
+    smt_arity: int;
+    smt_id:    string;
+    smt_token: option term;
+    smt_fuel_partial_app:option (term & term);
+    fvb_thunked: bool;
+    needs_fuel_and_universe_instantiations: option univ_names;
+}
+
+val list_of : int -> (int -> ML 'a) -> ML (list 'a)
+val kick_partial_app : fvar_binding -> ML (option term)
+val fvb_to_string : fvar_binding -> ML string
+
+instance val showable_fvar_binding : showable fvar_binding
+
+val check_valid_fvb : fvar_binding -> ML unit
+val binder_of_eithervar : 'a -> ('a & option 'b)
+
+type env_t = {
+    bvar_bindings: PSMap.t (PIMap.t (bv & term));
+    fvar_bindings: (PSMap.t fvar_binding & list fvar_binding);
+    depth:int;
+    tcenv:Env.env;
+    warn:bool;
+    nolabels:bool;
+    use_zfuel_name:bool;
+    encode_non_total_function_typ:bool;
+    current_module_name:string;
+    encoding_quantifier:bool;
+    global_cache:SMap.t (decls_elt & lident);
+}
+
+val print_env : env_t -> ML string
+val lookup_bvar_binding : env_t -> bv -> option (bv & term)
+val lookup_fvar_binding : env_t -> lident -> option fvar_binding
+val add_bvar_binding : (bv & term) -> PSMap.t (PIMap.t (bv & term)) -> ML (PSMap.t (PIMap.t (bv & term)))
+val add_fvar_binding : fvar_binding -> (PSMap.t fvar_binding & list fvar_binding) -> (PSMap.t fvar_binding & list fvar_binding)
+val fresh_fvar : string -> string -> sort -> ML (string & term)
+val gen_term_var : env_t -> bv -> ML (string & term & env_t)
+val new_term_constant : env_t -> bv -> ML (string & term & env_t)
+val new_term_constant_from_string : env_t -> bv -> string -> ML (string & term & env_t)
+val push_term_var : env_t -> bv -> term -> ML env_t
+val lookup_term_var : env_t -> bv -> ML term
+val mk_fvb : lident -> string -> int -> int -> option term -> option (term & term) -> bool -> option univ_names -> ML fvar_binding
+val new_term_constant_and_tok_from_lid : env_t -> lident -> int -> int -> ML (string & string & env_t)
+val new_term_constant_and_tok_from_lid_maybe_thunked : env_t -> lident -> int -> int -> bool -> ML (string & option string & env_t)
+val fail_fvar_lookup : env_t -> lident -> ML 'a
+val lookup_lid : env_t -> lident -> ML fvar_binding
+val push_free_var_maybe_thunked_with_univs : env_t -> lident -> int -> int -> string -> option term -> bool -> option univ_names -> ML env_t
+val push_free_var_maybe_thunked : env_t -> lident -> int -> int -> string -> option term -> bool -> ML env_t
+val push_free_var_tok_with_fuel_and_univs : env_t -> lident -> int -> int -> string -> option term -> univ_names -> ML env_t
+val push_free_var : env_t -> lident -> int -> int -> string -> option term -> ML env_t
+val push_free_var_thunk : env_t -> lident -> int -> int -> string -> option term -> ML env_t
+val push_zfuel_name : env_t -> lident -> string -> string -> ML env_t
+val force_thunk : fvar_binding -> ML term
+val try_lookup_free_var : env_t -> lident -> ML (option term)
+val lookup_free_var : env_t -> lident -> ML term
+val lookup_free_var_name : env_t -> lident -> ML fvar_binding
+val lookup_free_var_sym : env_t -> lident -> ML (either op term & list term & int)
+val tok_of_name : env_t -> string -> ML (option term)
+val reset_current_module_fvbs : env_t -> env_t
+val get_current_module_fvbs : env_t -> list fvar_binding
+val add_fvar_binding_to_env : fvar_binding -> env_t -> ML env_t
diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst
@@ -34,6 +34,7 @@ open FStarC.Class.Show
 open FStarC.Class.PP
 open FStarC.Class.Hashable
 open FStarC.RBSet
+open FStarC.Syntax.Print {} // instances
 
 module BU       = FStarC.Util
 module Env      = FStarC.TypeChecker.Env
diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst
@@ -45,7 +45,6 @@ module PC = FStarC.Parser.Const
 module U  = FStarC.Syntax.Util
 module EMB = FStarC.Syntax.Embeddings
 module TcComm = FStarC.TypeChecker.Common
-module TEQ = FStarC.TypeChecker.TermEqAndSimplify
 module PO = FStarC.TypeChecker.Primops
 module Print = FStarC.Syntax.Print //bring into scope for show instances
 open FStarC.TypeChecker.Normalize.Unfolding
diff --git a/src/typechecker/FStarC.TypeChecker.TcEffect.fst b/src/typechecker/FStarC.TypeChecker.TcEffect.fst
@@ -37,7 +37,6 @@ module TcUtil = FStarC.TypeChecker.Util
 module Gen = FStarC.TypeChecker.Generalize
 module TEQ = FStarC.TypeChecker.TermEqAndSimplify
 
-module BU = FStarC.Util
 open FStarC.Class.Show
 open FStarC.Class.Tagged
 
diff --git a/tests/bug-reports/closed/Bug2069.fst b/tests/bug-reports/closed/Bug2069.fst
@@ -1,5 +1,4 @@
 module Bug2069
-module WF = FStar.WellFounded
 
 
 let id (a : Type u#aa) (x:a) : a = x
diff --git a/tests/machine_integers/TestRotate.fst b/tests/machine_integers/TestRotate.fst
@@ -4,10 +4,8 @@ open FStar.All
 open FStar.IO
 
 module U8   = FStar.UInt8
-module U16  = FStar.UInt16
 module U32  = FStar.UInt32
 module U64  = FStar.UInt64
-module I8   = FStar.Int8
 module I32  = FStar.Int32
 
 let check s (b:bool) : ML unit =
diff --git a/ulib/FStar.Injection.fsti b/ulib/FStar.Injection.fsti
@@ -2,7 +2,6 @@ module FStar.Injection
 
 open FStar.Fin
 open FStar.Functions
-module SZ = FStar.SizeT
 open FStar.SizeT { (/^), (%^), (+^), (-^), ( *^ )  }
 open FStar.Tactics.Easy
 
