From 7efbf34f14664dc0fde852c238e414c5e26581fd Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Wed, 13 Mar 2024 20:09:44 +0100
Subject: [PATCH] [wp] Cache pattern for Ty.tysymbol
---
src/plugins/wp/Why3Import.ml | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 570067c07b1..6f6d3e93bda 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -33,6 +33,13 @@ let create_why3_env =
W.Env.create_env (WConf.loadpath (WConf.get_main (WConf.read_config None)))
end
+let rec get_ty_symbols_from_ty (tys : W.Ty.tysymbol) (tymap) =
+ try W.Wstdlib.Mstr.find tymap tys
+ with Not_found ->
+ let ty = tys.tysymbol in
+ tymap <- Mty.add tys.tysymbol tymap;
+
+
let () =
Boot.Main.extend
begin fun () ->
--
GitLab