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

Further fix for #3213 #3215

Merged
merged 8 commits into from
Feb 12, 2024
Merged

Further fix for #3213 #3215

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
a7babd7
SMT: fix typo
mtzguido Dec 22, 2023
5b2c692
Normalizer: more typeclass use
mtzguido Feb 12, 2024
4659832
Normalizer: some refactor
mtzguido Feb 12, 2024
aea8db8
Normalizer: another fix for #3213
mtzguido Feb 12, 2024
dfac2c8
snap
mtzguido Feb 12, 2024
b5765fb
Update test, more robust
mtzguido Feb 12, 2024
6156792
Update expected output
mtzguido Feb 12, 2024
3e66169
Update WP optimization test
mtzguido Feb 12, 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
23 changes: 13 additions & 10 deletions ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
View file
Open in desktop

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

954 changes: 608 additions & 346 deletions ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion src/smtencoding/FStar.SMTEncoding.Term.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ F* would encode this to SMT as (roughly)
```
(declare-fun n () Term)
(assert (HasType n u32))
(assert (n = U32.uint_to_to 0))
(assert (n = U32.uint_to_t 0))
```

i.e., ground facts about the `n`'s typing and definition would be
Expand Down
12 changes: 7 additions & 5 deletions src/typechecker/FStar.TypeChecker.Cfg.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -214,11 +214,13 @@ let prim_from_list (l : list primitive_step) : prim_step_set =
let built_in_primitive_steps = prim_from_list built_in_primitive_steps_list
let equality_ops = prim_from_list equality_ops_list

let cfg_to_string cfg =
String.concat "\n"
["{";
BU.format1 " steps = %s" (steps_to_string cfg.steps);
"}" ]
instance showable_cfg : showable cfg = {
show = (fun cfg ->
String.concat "\n"
["{";
BU.format1 " steps = %s" (steps_to_string cfg.steps);
"}" ]);
}

let cfg_env cfg = cfg.tcenv

Expand Down
5 changes: 3 additions & 2 deletions src/typechecker/FStar.TypeChecker.Cfg.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,10 @@ open FStar.Syntax.Subst
open FStar.Syntax.Util
open FStar.TypeChecker
open FStar.TypeChecker.Env

open FStar.TypeChecker.Primops

open FStar.Class.Show

module S = FStar.Syntax.Syntax
module SS = FStar.Syntax.Subst
module BU = FStar.Compiler.Util
Expand Down Expand Up @@ -116,7 +117,7 @@ val primop_time_report : unit -> string

val cfg_env: cfg -> Env.env

val cfg_to_string : cfg -> string
instance val showable_cfg : showable cfg

val log : cfg -> (unit -> unit) -> unit
val log_top : cfg -> (unit -> unit) -> unit
Expand Down
Loading
Loading