Skip to content

Commit

Permalink
Merge branch 'master' into auto_tuple
Browse files Browse the repository at this point in the history
  • Loading branch information
nikswamy authored Feb 7, 2024
2 parents c68706b + 5311850 commit 729caed
Show file tree
Hide file tree
Showing 18 changed files with 799 additions and 441 deletions.
7 changes: 4 additions & 3 deletions ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,7 @@ let mk_top_mllb (e: mlexpr): mllb =
mllb_add_unit=false;
mllb_def=e;
mllb_meta=[];
mllb_attrs=[];
print_typ=false }

(* names of F* functions which need to be handled differently *)
Expand Down Expand Up @@ -338,7 +339,7 @@ and resugar_app f args es: expression =

and get_variants (e : mlexpr) : Parsetree.case list =
match e.expr with
| MLE_Fun ([(id, _)], e) ->
| MLE_Fun ([{mlbinder_name=id}], e) ->
(match e.expr with
| MLE_Match ({expr = MLE_Var id'}, branches) when id = id' ->
map build_case branches
Expand Down Expand Up @@ -369,7 +370,7 @@ and build_constructor_expr ((path, sym), exp): expression =

and build_fun l e =
match l with
| ((id, ty)::tl) ->
| ({mlbinder_name=id; mlbinder_ty=ty}::tl) ->
let p = build_binding_pattern id in
Exp.fun_ Nolabel None p (build_fun tl e)
| [] -> build_expr e
Expand Down Expand Up @@ -476,7 +477,7 @@ let build_exn (sym, tys): type_exception =
Te.mk_exception ctor

let build_module1 path (m1: mlmodule1): structure_item option =
match m1 with
match m1.mlmodule1_m with
| MLM_Ty tydecl ->
(match build_tydecl tydecl with
| Some t -> Some (Str.mk t)
Expand Down
192 changes: 101 additions & 91 deletions ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml

Large diffs are not rendered by default.

64 changes: 36 additions & 28 deletions ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml

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

Loading

0 comments on commit 729caed

Please sign in to comment.