Skip to content

Commit

Permalink
chore(update): tools, bump OCaml to 5.x
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Jun 6, 2024
1 parent 706a1ca commit f884988
Show file tree
Hide file tree
Showing 5 changed files with 34 additions and 73 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ Note:

1. Make sure to have the following installed on your system:

- [`opam`](https://opam.ocaml.org/) (`opam switch create 4.14.1`)
- [`opam`](https://opam.ocaml.org/) (`opam switch create 5.1.1`)
- [`rustup`](https://rustup.rs/)
- [`nodejs`](https://nodejs.org/)
- [`jq`](https://jqlang.github.io/jq/)
Expand Down
4 changes: 2 additions & 2 deletions engine/backends/fstar/fstar-surface-ast/FStar_String.ml
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ let get s i = BatUChar.code (BatUTF8.get s (Z.to_int i))
let collect f s =
let r = ref "" in
BatUTF8.iter (fun c -> r := !r ^ f (BatUChar.code c)) s; !r
let lowercase = BatString.lowercase
let uppercase = BatString.uppercase
let lowercase = BatString.lowercase_ascii
let uppercase = BatString.uppercase_ascii
let escaped = BatString.escaped
let index = get
exception Found of int
Expand Down
87 changes: 21 additions & 66 deletions flake.lock

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

2 changes: 1 addition & 1 deletion flake.nix
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
{
inputs = {
nixpkgs.url = "github:nixos/nixpkgs";
flake-utils.url = "github:numtide/flake-utils";
crane = {
url = "github:ipetkov/crane";
inputs = {
nixpkgs.follows = "nixpkgs";
flake-utils.follows = "flake-utils";
};
};
rust-overlay = {
Expand Down
12 changes: 9 additions & 3 deletions frontend/exporter/src/types/copied.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1205,11 +1205,17 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx>
Some(contents) => contents,
None => match kind {
// Introduce intermediate `Cast` from `T` to `U` when casting from a `#[repr(T)]` enum to `U`
rustc_middle::thir::ExprKind::Cast { source } if let rustc_middle::ty::TyKind::Adt(def, _) = s.thir().exprs[source].ty.kind() => {
rustc_middle::thir::ExprKind::Cast { source }
if let rustc_middle::ty::TyKind::Adt(def, _) =
s.thir().exprs[source].ty.kind() =>
{
let tcx = s.base().tcx;
let contents = kind.sinto(s);
use crate::rustc_middle::ty::util::IntTypeExt;
let repr_type = tcx.repr_options_of_def(def.did()).discr_type().to_ty(s.base().tcx);
let repr_type = tcx
.repr_options_of_def(def.did())
.discr_type()
.to_ty(s.base().tcx);
if repr_type == ty {
contents
} else {
Expand All @@ -1220,7 +1226,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> for rustc_middle::thir::Expr<'tcx>
contents: Box::new(contents),
hir_id,
attributes: vec![],
}
},
}
}
}
Expand Down

0 comments on commit f884988

Please sign in to comment.