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

Jump to bottom

Restricting well-foundedness on inductives function-typed fields #2954

Merged
merged 5 commits into from
Aug 18, 2023
Merged

Restricting well-foundedness on inductives function-typed fields #2954

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
b8641e9
try a patch that restricts the well-foundedness axiom on function-typ…
nikswamy Jun 2, 2023
af03552
adding another test case, thanks @mtzguido
nikswamy Jun 2, 2023
cf9c5f8
Merge branch 'master' into nik_wf
nikswamy Aug 1, 2023
1461b7b
merge master in
nikswamy Aug 17, 2023
4db363a
for compatibility with previous encoding, use --ext compat:2954; rais…
nikswamy Aug 17, 2023
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
128 changes: 106 additions & 22 deletions ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml
View file
Open in desktop

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

32 changes: 22 additions & 10 deletions src/smtencoding/FStar.SMTEncoding.Encode.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1522,6 +1522,15 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =
let codomain_ordering, codomain_decls =
let _, formals' = BU.first_N n_tps formals in (* no codomain ordering for the parameters *)
let _, vars' = BU.first_N n_tps vars in
let norm t =
N.unfold_whnf' [Env.AllowUnboundUniverses;
Env.EraseUniverses;
Env.Unascribe;
//we don't know if this will terminate; so don't do recursive steps
Env.Exclude Env.Zeta]
env'.tcenv
t
in
let codomain_prec_l, cod_decls =
List.fold_left2
(fun (codomain_prec_l, cod_decls) formal var ->
Expand All @@ -1539,20 +1548,22 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =
then None //not useful for lemmas
else
let t = U.unrefine (U.comp_result c) in
let t = norm t in
if is_type t || U.is_sub_singleton t
then None //ordering on Type and squashed values is not useful
else Some (bs, c)
else (
let head, _ = U.head_and_args_full t in
match (U.un_uinst head).n with
| Tm_fvar fv ->
if BU.for_some (S.fv_eq_lid fv) mutuals
then Some (bs, c)
else None
| _ -> None
)
end
| _ ->
let head, _ = U.head_and_args t in
let t' = N.unfold_whnf' [Env.AllowUnboundUniverses;
Env.EraseUniverses;
Env.Unascribe;
//we don't know if this will terminate; so don't do recursive steps
Env.Exclude Env.Zeta]
env'.tcenv
t
in
let t' = norm t in
let head', _ = U.head_and_args t' in
match U.eq_tm head head' with
| U.Equal -> None //no progress after whnf
Expand All @@ -1572,7 +1583,8 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =

in
match binder_and_codomain_type formal.binder_bv.sort with
| None -> codomain_prec_l, cod_decls
| None ->
codomain_prec_l, cod_decls
| Some (bs, c) ->
//var bs << D ... var ...
let bs', guards', _env', bs_decls, _ = encode_binders None bs env' in
Expand Down
Loading