Merge pull request #763 from hacspec/various-fixes-refinements

fix(hax-lib): refinements: various fixes
hacspec · Jul 10, 2024 · 30b2ac9 · 30b2ac9
2 parents 640d31e + 0b3e700
commit 30b2ac9
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 7 deletions.
diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
@@ -229,7 +229,11 @@ fn run_engine(
                 }
                 FromEngine::PrettyPrintRust(code) => {
                     let code = match syn::parse_file(&code) {
-                        Ok(file) => Ok(prettyplease::unparse(&file)),
+                        Ok(file) => match std::panic::catch_unwind(|| prettyplease::unparse(&file))
+                        {
+                            Ok(pp) => Ok(pp),
+                            Err(err) => Err(format!("prettyplease panicked with: {:#?}", err)),
+                        },
                         Err(err) => Err(format!("{}", err)),
                     };
                     send!(&ToEngine::PrettyPrintedRust(code));

diff --git a/engine/lib/phases/phase_newtype_as_refinement.ml b/engine/lib/phases/phase_newtype_as_refinement.ml
@@ -21,14 +21,15 @@ module Make (F : Features.T) =
           inherit [_] Visitors.map as super
 
           method! visit_expr () e =
+            let e = super#visit_expr () e in
             match e.e with
             | App { f = { e = GlobalVar f; _ }; args = [ inner ]; _ }
               when Ast.Global_ident.eq_name Hax_lib__Refinement__new f
                    || Ast.Global_ident.eq_name Hax_lib__RefineAs__into_checked f
                    || Ast.Global_ident.eq_name Hax_lib__Refinement__get_mut f
                    || Ast.Global_ident.eq_name Hax_lib__Refinement__get f ->
                 { e with e = Ascription { typ = e.typ; e = inner } }
-            | _ -> super#visit_expr () e
+            | _ -> e
 
           method! visit_item () i =
             match i.v with

diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst
@@ -3,7 +3,6 @@ module Hax_lib.Int
 open Core
 
 unfold type t_Int = int
-unfold type impl__Int__to_u16
 
 unfold let impl__Int__to_u8 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
 unfold let impl__Int__to_u16 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n

diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -44,6 +44,16 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
     f_sub = fun (self: t_Int) (other: t_Int) -> self + other
   }
 '''
+"Attributes.Nested_refinement_elim.fst" = '''
+module Attributes.Nested_refinement_elim
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let t_DummyRefinement = x: u16{true}
+
+let elim_twice (x: t_DummyRefinement) : u16 = ((x <: u16) <: t_DummyRefinement) <: u16
+'''
 "Attributes.Newtype_pattern.fst" = '''
 module Attributes.Newtype_pattern
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -183,10 +193,7 @@ let t_NoE =
       ~.out }
 
 let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
-  (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +!
-  (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8)
-  <:
-  t_BoundedU8 1uy 23uy
+  (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy
 
 let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
   x +! x <: t_Even

diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
@@ -223,3 +223,12 @@ mod refinement_types {
     #[hax_lib::refinement_type(|x| x == 4 || x == 5 || x == 10 || x == 11)]
     pub struct CompressionFactor(u8);
 }
+mod nested_refinement_elim {
+    use hax_lib::*;
+    #[refinement_type(|x| true)]
+    pub struct DummyRefinement(u16);
+
+    fn elim_twice(x: DummyRefinement) -> u16 {
+        (DummyRefinement::new(x.get())).get()
+    }
+}