You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
// A.fstimoduleAvalt:Type0vals0:Type0// We wrap the type in a match to trigger automatic coercion.inline_for_extractionlets1b=ifbthentelses0inline_for_extractionlets=s1falsevalt_eq_s:squash(t==s)// A.fstmoduleAlett=natlets0=natlett_eq_s=()// B.fstimoduleB// B.fstmoduleBopenAletf(x:t):s=x
Extracting ocaml code from B.fst results in this function, expectedly using magic:
If we add friend A to B.fst, then extraction can (again, as expected) see through the type definitions:
let (f : A.t -> A.s0) =funx -> x
However, --cmi uses magic (while it should probably behave as if everything was in the same file). Even more surprisingly, if you tag eithert or s0 as inline_for_extraction, then extraction with --cmi sees through the other definition as well (even though they are not defined in terms of each other):
Consider the following four files:
Extracting ocaml code from
B.fst
results in this function, expectedly using magic:If we add
friend A
toB.fst
, then extraction can (again, as expected) see through the type definitions:However,
--cmi
uses magic (while it should probably behave as if everything was in the same file). Even more surprisingly, if you tag eithert
ors0
asinline_for_extraction
, then extraction with--cmi
sees through the other definition as well (even though they are not defined in terms of each other):This is potentially related to the extraction failure in project-everest/mitls-fstar#260
The text was updated successfully, but these errors were encountered: