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

Fixing mistaken erasure of effectful type applications #3518

Merged
merged 6 commits into from
Oct 3, 2024
Merged

Fixing mistaken erasure of effectful type applications #3518

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
eac472d
track effects when instantiating type arguments when generating ML, t…
nikswamy Oct 2, 2024
a06d574
snap
nikswamy Oct 2, 2024
f3c86bd
add a test case
nikswamy Oct 2, 2024
86558dd
snap
nikswamy Oct 2, 2024
a56b285
Merge remote-tracking branch 'origin/master' into nik_3473
nikswamy Oct 3, 2024
bca036a
a bit of cleanup, adding some comments
nikswamy Oct 3, 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
22 changes: 17 additions & 5 deletions ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml
View file
Open in desktop

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

7 changes: 4 additions & 3 deletions ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml
View file
Open in desktop

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

15 changes: 8 additions & 7 deletions ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml
View file
Open in desktop

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

1,152 changes: 613 additions & 539 deletions ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml
View file
Open in desktop

Large diffs are not rendered by default.

123 changes: 68 additions & 55 deletions ocaml/fstar-lib/generated/FStar_Extraction_ML_UEnv.ml
View file
Open in desktop

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

8 changes: 4 additions & 4 deletions ocaml/fstar-lib/generated/FStar_MRef.ml
View file
Open in desktop

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

5 changes: 4 additions & 1 deletion ocaml/fstar-lib/generated/FStar_Monotonic_Seq.ml
View file
Open in desktop

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

17 changes: 15 additions & 2 deletions src/extraction/FStar.Extraction.ML.Code.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -314,6 +314,11 @@ let string_of_mlconstant (sctt : mlconstant) =


(* -------------------------------------------------------------------- *)
let string_of_etag = function
| E_PURE -> ""
| E_ERASABLE -> "Erased"
| E_IMPURE -> "Impure"

let rec doc_of_mltype' (currentModule : mlsymbol) (outer : level) (ty : mlty) =
match ty with
| MLTY_Var x ->
Expand Down Expand Up @@ -344,10 +349,10 @@ let rec doc_of_mltype' (currentModule : mlsymbol) (outer : level) (ty : mlty) =
hbox (reduce1 [args; text name])
end

| MLTY_Fun (t1, _, t2) ->
| MLTY_Fun (t1, et, t2) ->
let d1 = doc_of_mltype currentModule (t_prio_fun, Left ) t1 in
let d2 = doc_of_mltype currentModule (t_prio_fun, Right) t2 in
maybe_paren outer t_prio_fun (hbox (reduce1 [d1; text " -> "; d2]))
maybe_paren outer t_prio_fun (hbox (reduce1 [d1; text "->"; d2]))

| MLTY_Top ->
if Util.codegen_fsharp()
Expand Down Expand Up @@ -854,3 +859,11 @@ let string_of_mlty (cmod) (e:mlty) =
instance showable_mlexpr : showable mlexpr = {
show = string_of_mlexpr ([], "");
}

instance showable_mlty : showable mlty = {
show = string_of_mlty ([], "");
}

instance showable_etag : showable e_tag = {
show = string_of_etag
}
2 changes: 2 additions & 0 deletions src/extraction/FStar.Extraction.ML.Code.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,3 +30,5 @@ val string_of_mlty: mlpath -> mlty -> string
val pretty: int -> doc -> string

instance val showable_mlexpr : showable mlexpr
instance val showable_mlty : showable mlty
instance val showable_etag : showable e_tag
10 changes: 5 additions & 5 deletions src/extraction/FStar.Extraction.ML.Syntax.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,16 +97,16 @@ let apply_obj_repr : mlexpr -> mlty -> mlexpr = fun x t ->
let ty_param_names (tys:list ty_param) : list string =
tys |> List.map (fun {ty_param_name} -> ty_param_name)

let push_unit (ts : mltyscheme) : mltyscheme =
let push_unit eff (ts : mltyscheme) : mltyscheme =
let vs, ty = ts in
vs, MLTY_Fun(ml_unit_ty, E_PURE, ty)
vs, MLTY_Fun(ml_unit_ty, eff, ty)

let pop_unit (ts : mltyscheme) : mltyscheme =
let pop_unit (ts : mltyscheme) : e_tag & mltyscheme =
let vs, ty = ts in
match ty with
| MLTY_Fun (l, E_PURE, t) ->
| MLTY_Fun (l, eff, t) ->
if l = ml_unit_ty
then vs, t
then eff, (vs, t)
else failwith "unexpected: pop_unit: domain was not unit"
| _ ->
failwith "unexpected: pop_unit: not a function type"
Expand Down
4 changes: 2 additions & 2 deletions src/extraction/FStar.Extraction.ML.Syntax.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,8 +239,8 @@ val apply_obj_repr : mlexpr -> mlty -> mlexpr

val ty_param_names (tys:list ty_param) : list string

val push_unit (ts : mltyscheme) : mltyscheme
val pop_unit (ts : mltyscheme) : mltyscheme
val push_unit (eff:e_tag) (ts : mltyscheme) : mltyscheme
val pop_unit (ts : mltyscheme) : e_tag & mltyscheme
Copy link
Collaborator Author

@nikswamy nikswamy Oct 3, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

push_unit is called when replacing the type arguments of a function with a unit.

pop_unit is the converse, eliminating a polymorphic function with a type application where the type argument is extracted as unit.

We now record the effect of type application as an e_tag, i.e., Pure, Erasable, Impure


val mltyscheme_to_string (tsc:mltyscheme) : string
val mlbranch_to_string (b:mlbranch) : string
Expand Down
Loading