fix(hax-lib): refinements: various fixes

cryspen · Jul 10, 2024 · 06e22f3 · 06e22f3
1 parent 45be3ca
commit 06e22f3
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 2 deletions.
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/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::*;
+    #[hax_lib::refinement_type(|x| true)]
+    pub struct DummyRefinement(u16);
+
+    fn elim_twice(x: DummyRefinement) -> u16 {
+        (DummyRefinement::new(x.get())).get()
+    }
+}