Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some nits #3524

Merged
merged 4 commits into from
Oct 5, 2024
Merged

Some nits #3524

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
36f1f70
No FStar.Version.fst
mtzguido Oct 3, 2024
d94ad02
Tc: reducing --debug Low output, do not show sigelt bodies
mtzguido Oct 3, 2024
49770f7
Tc: some comments
mtzguido Oct 4, 2024
453f1a1
snap
mtzguido Oct 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 2 additions & 5 deletions ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

19 changes: 14 additions & 5 deletions ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

11 changes: 0 additions & 11 deletions src/basic/FStar.Version.fst
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions src/typechecker/FStar.TypeChecker.Tc.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -922,7 +922,7 @@ let add_sigelt_to_env (env:Env.env) (se:sigelt) (from_cache:bool) : Env.env =
if Debug.low ()
then BU.print2
">>>>>>>>>>>>>>Adding top-level decl to environment: %s (from_cache:%s)\n"
(show se) (show from_cache);
(Print.sigelt_to_string_short se) (show from_cache);

match se.sigel with
| Sig_inductive_typ _
Expand Down Expand Up @@ -1009,7 +1009,7 @@ let tc_decls env ses =
if Debug.low ()
then BU.print2 ">>>>>>>>>>>>>>Checking top-level %s decl %s\n"
(tag_of se)
(show se);
(Print.sigelt_to_string_short se);

if Options.ide_id_info_off() then Env.toggle_id_info env false;
if !dbg_IdInfoOn then Env.toggle_id_info env true;
Expand Down
10 changes: 7 additions & 3 deletions src/typechecker/FStar.TypeChecker.Util.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ open FStar.Syntax
open FStar.Dyn
open FStar.Class.Show
open FStar.Class.PP
open FStar.Class.Monoid

module SS = FStar.Syntax.Subst
module S = FStar.Syntax.Syntax
Expand Down Expand Up @@ -2863,10 +2864,13 @@ let instantiate_one_binder (env:env_t) (r:Range.range) (b:binder) : term & typ &
BU.print1 "instantiate_one_binder: result = %s\n" (show (r._1, r._2));
r

(* Will instantiate e, by applying it to some unification variables for its implicit
arguments, if that is needed to match the expected type in the environment. [t] is the type
of [e]. Returns elaborated [e'], its type [t'], and a guard. *)
let maybe_instantiate (env:Env.env) (e:term) (t:typ) : term & typ & guard_t =
let torig = SS.compress t in
if not env.instantiate_imp
then e, torig, Env.trivial_guard
then e, torig, mzero
else begin
if Debug.high () then
BU.print3 "maybe_instantiate: starting check for (%s) of type (%s), expected type is %s\n"
Expand Down Expand Up @@ -2927,9 +2931,9 @@ let maybe_instantiate (env:Env.env) (e:term) (t:typ) : term & typ & guard_t =
let tm, ty, aq, g = instantiate_one_binder env e.pos b in
let subst = NT(b.binder_bv, tm)::subst in
let args, bs, subst, g' = aux subst (decr_inst inst_n) rest in
(tm, aq)::args, bs, subst, Env.conj_guard g g'
(tm, aq)::args, bs, subst, g ++ g'

| _, bs -> [], bs, subst, Env.trivial_guard
| _, bs -> [], bs, subst, mzero
in
let args, bs, subst, guard = aux [] (inst_n_binders t) bs in
begin match args, bs with
Expand Down
Loading