From 2f7059c1ac908a67a99b89c2d3d463af8fabeb22 Mon Sep 17 00:00:00 2001
From: Denis Merigoux <denis.merigoux@gmail.com>
Date: Wed, 19 Jan 2022 09:47:08 +0100
Subject: [PATCH] More functorization

---
 compiler/verification/io.ml         | 29 ++++++++++++++++++++-
 compiler/verification/io.mli        | 21 ++++++++++++---
 compiler/verification/z3backend.ml  |  4 ++-
 compiler/verification/z3backend.mli | 40 ++++++++---------------------
 4 files changed, 59 insertions(+), 35 deletions(-)

diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml
index dcabf25a..66123e28 100644
--- a/compiler/verification/io.ml
+++ b/compiler/verification/io.ml
@@ -31,9 +31,36 @@ module type Backend = sig
   val print_model : backend_context -> model -> string
 
   val is_model_empty : model -> bool
+
+  val translate_expr :
+    backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
 end
 
-module SolverIO (B : Backend) = struct
+module type SolverIo = sig
+  type vc_encoding
+
+  type backend_context
+
+  type model
+
+  type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
+
+  val print_positive_result : Conditions.verification_condition -> string
+
+  val print_negative_result :
+    Conditions.verification_condition -> backend_context -> model option -> string
+
+  val encode_and_check_vc :
+    Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
+end
+
+module MakeSolverIO (B : Backend) = struct
+  type vc_encoding = B.vc_encoding
+
+  type backend_context = B.backend_context
+
+  type model = B.model
+
   type vc_encoding_result = Success of B.vc_encoding * B.backend_context | Fail of string
 
   let print_positive_result (vc : Conditions.verification_condition) : string =
diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli
index a3afd0fd..cc334bd1 100644
--- a/compiler/verification/io.mli
+++ b/compiler/verification/io.mli
@@ -30,16 +30,31 @@ module type Backend = sig
   val print_model : backend_context -> model -> string
 
   val is_model_empty : model -> bool
+
+  val translate_expr :
+    backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
 end
 
-module SolverIO : functor (B : Backend) -> sig
-  type vc_encoding_result = Success of B.vc_encoding * B.backend_context | Fail of string
+module type SolverIo = sig
+  type vc_encoding
+
+  type backend_context
+
+  type model
+
+  type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
 
   val print_positive_result : Conditions.verification_condition -> string
 
   val print_negative_result :
-    Conditions.verification_condition -> B.backend_context -> B.model option -> string
+    Conditions.verification_condition -> backend_context -> model option -> string
 
   val encode_and_check_vc :
     Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
 end
+
+module MakeSolverIO : functor (B : Backend) ->
+  SolverIo
+    with type vc_encoding = B.vc_encoding
+     and type backend_context = B.backend_context
+     and type model = B.model
diff --git a/compiler/verification/z3backend.ml b/compiler/verification/z3backend.ml
index 3b40b434..188909c7 100644
--- a/compiler/verification/z3backend.ml
+++ b/compiler/verification/z3backend.ml
@@ -580,6 +580,8 @@ module Backend = struct
   let print_model (ctx : backend_context) (m : model) : string = print_model ctx m
 
   let is_model_empty (m : model) : bool = List.length (Z3.Model.get_decls m) = 0
+
+  let translate_expr (ctx : backend_context) (e : Dcalc.Ast.expr Pos.marked) = translate_expr ctx e
 end
 
-module Io = Io.SolverIO (Backend)
+module Io = Io.MakeSolverIO (Backend)
diff --git a/compiler/verification/z3backend.mli b/compiler/verification/z3backend.mli
index b2efa625..deff1e50 100644
--- a/compiler/verification/z3backend.mli
+++ b/compiler/verification/z3backend.mli
@@ -29,34 +29,14 @@ type context = {
 
 val translate_expr : context -> Dcalc.Ast.expr Utils.Pos.marked -> context * Z3.Expr.expr
 
-module Backend : sig
-  type backend_context = context
+module Backend :
+  Io.Backend
+    with type vc_encoding = Z3.Expr.expr
+     and type backend_context = context
+     and type model = Z3.Model.model
 
-  type vc_encoding = Z3.Expr.expr
-
-  val print_encoding : vc_encoding -> string
-
-  type model = Z3.Model.model
-
-  type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
-
-  val solve_vc_encoding : backend_context -> vc_encoding -> solver_result
-
-  val print_model : backend_context -> model -> string
-
-  val is_model_empty : model -> bool
-end
-
-module Io : sig
-  type vc_encoding_result = Io.SolverIO(Backend).vc_encoding_result =
-    | Success of Backend.vc_encoding * Backend.backend_context
-    | Fail of string
-
-  val print_positive_result : Conditions.verification_condition -> string
-
-  val print_negative_result :
-    Conditions.verification_condition -> Backend.backend_context -> Backend.model option -> string
-
-  val encode_and_check_vc :
-    Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
-end
+module Io :
+  Io.SolverIo
+    with type vc_encoding = Z3.Expr.expr
+     and type backend_context = context
+     and type model = Z3.Model.model