CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 16:28:12 +03:00
Code Issues Projects Releases Wiki Activity

Finished functorization

Browse Source
This commit is contained in:
Denis Merigoux 2022-01-19 10:17:19 +01:00
parent bc2742961f
commit a4002fefaf
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
5 changed files with 34 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
compiler/verification/io.ml
View File

@ -40,11 +40,18 @@ module type Backend = sig
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
end
module type SolverIo = sig
type vc_encoding
module type BackendIO = sig
val init_backend : unit -> unit
type backend_context
val make_context : decl_ctx -> typ Pos.marked VarMap.t -> backend_context
type vc_encoding
val translate_expr :
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
type model
type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
@ -58,11 +65,17 @@ module type SolverIo = sig
Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
end
module MakeSolverIO (B : Backend) = struct
type vc_encoding = B.vc_encoding
module MakeBackendIO (B : Backend) = struct
let init_backend = B.init_backend
type backend_context = B.backend_context
let make_context = B.make_context
type vc_encoding = B.vc_encoding
let translate_expr = B.translate_expr
type model = B.model
type vc_encoding_result = Success of B.vc_encoding * B.backend_context | Fail of string

16
compiler/verification/io.mli
View File

@ -40,11 +40,19 @@ module type Backend = sig
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
end
module type SolverIo = sig
type vc_encoding
module type BackendIO = sig
val init_backend : unit -> unit
type backend_context
val make_context :
Dcalc.Ast.decl_ctx -> Dcalc.Ast.typ Utils.Pos.marked Dcalc.Ast.VarMap.t -> backend_context
type vc_encoding
val translate_expr :
backend_context -> Dcalc.Ast.expr Utils.Pos.marked -> backend_context * vc_encoding
type model
type vc_encoding_result = Success of vc_encoding * backend_context | Fail of string
@ -58,8 +66,8 @@ module type SolverIo = sig
Dcalc.Ast.decl_ctx -> Conditions.verification_condition * vc_encoding_result -> unit
end
module MakeSolverIO : functor (B : Backend) ->
SolverIo
module MakeBackendIO : functor (B : Backend) ->
BackendIO
with type vc_encoding = B.vc_encoding
and type backend_context = B.backend_context
and type model = B.model

6
compiler/verification/solver.ml
View File

@ -21,15 +21,15 @@ let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verificati
unit =
(* Right now we only use the Z3 backend but the functorial interface should make it easy to mix
and match different proof backends. *)
Z3backend.Backend.init_backend ();
Z3backend.Io.init_backend ();
let z3_vcs =
List.map
(fun vc ->
( vc,
try
let ctx, z3_vc =
Z3backend.Backend.translate_expr
(Z3backend.Backend.make_context decl_ctx
Z3backend.Io.translate_expr
(Z3backend.Io.make_context decl_ctx
(VarMap.union
(fun _ _ _ ->
failwith "[Proof encoding]: A Variable cannot be both free and bound")

2
compiler/verification/z3backend.ml
View File

@ -601,4 +601,4 @@ module Backend = struct
}
end
module Io = Io.MakeSolverIO (Backend)
module Io = Io.MakeBackendIO (Backend)

8
compiler/verification/z3backend.mli
View File

@ -14,10 +14,4 @@
(** Interfacing with the Z3 SMT solver *)
module Backend : Io.Backend
module Io :
Io.SolverIo
with type backend_context = Backend.backend_context
and type model = Backend.model
and type vc_encoding = Backend.vc_encoding
module Io : Io.BackendIO