Merge pull request #380 from FStarLang/protz_misc2

Intermediary variable elimination in the presence of polymorphic type applications
FStarLang · Sep 29, 2023 · f8d97a5 · f8d97a5
2 parents 6698dd1 + 6ecaa6a
commit f8d97a5
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/lib/Helpers.ml b/lib/Helpers.ml
@@ -243,6 +243,8 @@ let is_readonly_builtin_lid lid =
     [ "FStar"; "UInt32" ], "v";
     [ "FStar"; "UInt128" ], "uint128_to_uint64";
     [ "FStar"; "UInt128" ], "uint64_to_uint128";
+    [ "Eurydice" ], "vec_len";
+    [ "Eurydice" ], "vec_index";
   ] in
   List.exists (fun lid' ->
     let lid = Idents.string_of_lident lid in
@@ -292,6 +294,8 @@ class ['self] readonly_visitor = object (self: 'self)
         List.for_all (self#visit_expr_w ()) es
     | EQualified lid when is_readonly_builtin_lid lid ->
         List.for_all (self#visit_expr_w ()) es
+    | ETApp ({ node = EQualified lid; _ }, _) when is_readonly_builtin_lid lid ->
+        List.for_all (self#visit_expr_w ()) es
     | _ ->
         false
 end

diff --git a/lib/Simplify.ml b/lib/Simplify.ml
@@ -76,6 +76,7 @@ class ['self] safe_use = object (self: 'self)
     match e.node with
     | EOp _ -> super#visit_EApp env e es
     | EQualified lid when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es
+    | ETApp ({ node = EQualified lid; _ }, _) when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es
     | _ -> self#unordered env (e :: es)
 
   method! visit_ELet env _ e1 e2 = self#sequential env e1 (Some e2)