Skip to content

Commit

Permalink
Merge pull request #178 from mtzguido/fix
Browse files Browse the repository at this point in the history
ExtractSteel: update for new F* error API
  • Loading branch information
mtzguido authored Sep 9, 2024
2 parents 4a52986 + ca69f1c commit c230565
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 26 deletions.
10 changes: 5 additions & 5 deletions src/extraction/ExtractSteel.fst
Original file line number Diff line number Diff line change
Expand Up @@ -164,14 +164,13 @@ let steel_translate_expr : translate_expr_t = fun env e ->
| MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_fp; _fp'; _opened; _p; _i; e])
when string_of_mlpath p = "Steel.ST.Util.with_invariant" ||
string_of_mlpath p = "Steel.Effect.Atomic.with_invariant" ->
Errors.raise_error
(Errors.Fatal_ExtractionUnsupported,
BU.format2
Errors.raise_error0
Errors.Fatal_ExtractionUnsupported
(BU.format2
"Extraction of with_invariant requires its argument to be a function literal \
at extraction time, try marking its argument inline_for_extraction (%s, %s)"
(string_of_int (fst e.loc))
(snd e.loc))
Range.dummyRange

| _ -> raise NotSupportedByKrmlExtension

Expand All @@ -197,7 +196,8 @@ let steel_translate_let : translate_let_t = fun env flavor lb ->
let expr = List.map (translate_expr env) (list_elements l) in
Some (DGlobal (meta, name, List.length tvars, t, EBufCreateL (Eternal, expr)))
with e ->
Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e)));
Errors.log_issue0 Errors.Warning_DefinitionNotTranslated
(BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e));
Some (DGlobal (meta, name, List.length tvars, t, EAny))
end
| _ -> raise NotSupportedByKrmlExtension
Expand Down
40 changes: 19 additions & 21 deletions src/ocaml/plugin/generated/ExtractSteel.ml

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

0 comments on commit c230565

Please sign in to comment.