From c5feece5cdd7bd3d755faeb2bc13cb747edcf61a Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Wed, 17 Apr 2024 16:51:45 +0200
Subject: [PATCH] [wp] Formatting
---
src/plugins/wp/Why3Import.ml | 20 ++++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 1442041f3ae..e0dcadab0dc 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -79,12 +79,15 @@ let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
) txs ([], W.Ty.Mtv.empty)
-let rec lt_of_ty (tenv : tenv) (tvs : tvars) ((thname, thpaths)) (ty: W.Ty.ty) : C.logic_type =
+
+let rec lt_of_ty (tenv : tenv) (tvs : tvars) (thname, thpaths) (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( lti_of_ts tenv s (thname, thpaths), List.map (lt_of_ty tenv tvs (thname, thpaths)) ts)
+ | Tyapp(s,ts) -> C.Ltype( lti_of_ts tenv s (thname, thpaths),
+ List.map (lt_of_ty tenv tvs (thname, thpaths)) ts)
+
-and lti_of_ts (tenv : tenv) (ts : W.Ty.tysymbol) ((thname, thpaths)): C.logic_type_info =
+and lti_of_ts (tenv : tenv) (ts : W.Ty.tysymbol) (thname, thpaths): C.logic_type_info =
try W.Ty.Hts.find tenv ts with Not_found ->
let (lt_params,tvars) = tvars_of_txs ts.ts_args in
let lt_def =
@@ -94,7 +97,7 @@ and lti_of_ts (tenv : tenv) (ts : W.Ty.tysymbol) ((thname, thpaths)): C.logic_ty
in
let lti =
C.{
- lt_name = construct_acsl_name thpaths thname ts.ts_name.id_string; (* "int::Int::add" *)
+ lt_name = construct_acsl_name thpaths thname ts.ts_name.id_string;
lt_params ; lt_def ;
lt_attr = [];
}
@@ -105,9 +108,9 @@ and lti_of_ts (tenv : tenv) (ts : W.Ty.tysymbol) ((thname, thpaths)): C.logic_ty
(* --- Functions --- *)
(* -------------------------------------------------------------------------- *)
-let lv_of_ty (tenv:tenv) (tvars:tvars) ((thname, thpaths)) (index) (ty:W.Ty.ty) : C.logic_var =
+let lv_of_ty (tenv:tenv) (tvars:tvars) (thname, thpaths)(index) (ty:W.Ty.ty) : C.logic_var =
Cil_const.make_logic_var_formal (Printf.sprintf "x%d" index)
- @@ (lt_of_ty tenv tvars ((thname, thpaths)) ty)
+ @@ (lt_of_ty tenv tvars (thname, thpaths) ty)
let lr_of_ty_opt (lt_opt) =
match lt_opt with
@@ -115,7 +118,7 @@ let lr_of_ty_opt (lt_opt) =
| Some tr -> tr
-let li_of_ls (tenv:tenv) (ls : W.Term.lsymbol) (lenv:lenv) ((thname, thpaths)) : C.logic_info =
+let li_of_ls (tenv:tenv) (ls : W.Term.lsymbol) (lenv:lenv) (thname, thpaths) : C.logic_info =
let l_tparams,tvars =
tvars_of_txs @@ W.Ty.Stv.elements @@ W.Term.ls_ty_freevars ls in
let l_type = Option.map (lt_of_ty tenv tvars (thname, thpaths)) ls.ls_value in
@@ -140,8 +143,6 @@ let li_of_ls (tenv:tenv) (ls : W.Term.lsymbol) (lenv:lenv) ((thname, thpaths)) :
(* -------------------------------------------------------------------------- *)
-
-
let import_theory env (tenv:tenv) (lenv:lenv) thname =
let theory_name, theory_path = extract_path thname in
L.debug ~level:0 "Theory name : %s" theory_name;
@@ -206,7 +207,6 @@ let () =
L.debug ~level:0 "TY %a" pp_id ls.ls_name;
L.debug ~level:0 "LI %a" pp_li li;
) lenv
-
end
(* -------------------------------------------------------------------------- *)
--
GitLab