From 668ae702c9cc3832c30f17afdb2af4c67cb5ff9b Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 28 Mar 2024 11:28:16 +0100
Subject: [PATCH] [wp] Extracted temp env creation into separate function
---
src/plugins/wp/Why3Import.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index a0f2a3601ea..1ca4b96334d 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -58,18 +58,13 @@ type tvars = C.logic_type W.Ty.Mtv.t
type uid_tvars = string W.Ty.Mtv.t
let rec lt_of_ty (tenv : tenv) (tvs : tvars) (ty: W.Ty.ty) : C.logic_type =
-
match ty.ty_node with
| Tyvar x -> W.Ty.Mtv.find x tvs
| Tyapp(s,ts) -> C.Ltype( ls_of_ts tenv s, List.map (lt_of_ty tenv tvs) ts)
and ls_of_ts (tenv : tenv) (ts : W.Ty.tysymbol): C.logic_type_info =
try W.Ty.Hts.find tenv ts with Not_found ->
- let temp_env : uid_tvars =
- List.fold_left
- (fun (tvs: uid_tvars) (tv: W.Ty.tvsymbol) ->
- W.Ty.Mtv.add tv (tv.tv_name.id_string) tvs
- ) W.Ty.Mtv.empty ts.ts_args
+ let temp_env = create_temp_env ts
in
let lt_params =
List.map
@@ -94,6 +89,11 @@ and lt_def_of_ts (tenv:tenv) (ts : W.Ty.tysymbol) (temp_env : uid_tvars) =
W.Ty.Mtv.map (fun aleph_name -> C.Lvar aleph_name) temp_env
in
Some (C.LTsyn (lt_of_ty tenv tvars ty))
+and create_temp_env (ts: W.Ty.tysymbol) : uid_tvars =
+ List.fold_left
+ (fun (tvs: uid_tvars) (tv: W.Ty.tvsymbol) ->
+ W.Ty.Mtv.add tv (tv.tv_name.id_string) tvs
+ ) W.Ty.Mtv.empty ts.ts_args
let import_theory env (tenv:tenv) thname =
let theory_name, theory_path = extract_path thname in
--
GitLab