From 18e86621d5f7b6af8a2ead5f2f0da6480761e6fe Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Wed, 6 Jul 2022 10:08:27 +0200 Subject: [PATCH] Port verification code to the AST changes --- compiler/dcalc/ast.ml | 2 + compiler/dcalc/ast.mli | 1 + compiler/verification/conditions.ml | 64 ++++++++++++------------- compiler/verification/conditions.mli | 6 +-- compiler/verification/io.ml | 28 +++++------ compiler/verification/io.mli | 10 ++-- compiler/verification/solver.ml | 2 +- compiler/verification/solver.mli | 2 +- compiler/verification/z3backend.real.ml | 32 ++++++------- 9 files changed, 75 insertions(+), 72 deletions(-) diff --git a/compiler/dcalc/ast.ml b/compiler/dcalc/ast.ml index 8da4af76..c6686a7b 100644 --- a/compiler/dcalc/ast.ml +++ b/compiler/dcalc/ast.ml @@ -439,6 +439,8 @@ module Var = struct let get (V v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v) let compare (V x) (V y) = Bindlib.compare_vars x y + + let eq (V x) (V y) = Bindlib.eq_vars x y end module VarSet = Set.Make (Var) diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index 28896343..400bba81 100644 --- a/compiler/dcalc/ast.mli +++ b/compiler/dcalc/ast.mli @@ -418,6 +418,7 @@ module Var : sig val t: 'm expr Bindlib.var -> t val get: t -> 'm expr Bindlib.var val compare : t -> t -> int + val eq : t -> t -> bool end module VarMap : Map.S with type key = Var.t diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index 1fda9795..7043cb91 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -21,7 +21,7 @@ open Ast (** {1 Helpers and type definitions}*) -type vc_return = expr Marked.pos * typ Marked.pos VarMap.t +type 'm vc_return = 'm marked_expr * typ Marked.pos VarMap.t (** The return type of VC generators is the VC expression plus the types of any locally free variable inside that expression. *) @@ -32,30 +32,30 @@ type ctx = { scope_variables_typs : typ Marked.pos VarMap.t; } -let conjunction (args : vc_return list) (pos : Pos.t) : vc_return = +let conjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return = let acc, list = match args with | hd :: tl -> hd, tl - | [] -> ((ELit (LBool true), pos), VarMap.empty), [] + | [] -> ((ELit (LBool true), mark), VarMap.empty), [] in List.fold_left (fun (acc, acc_ty) (arg, arg_ty) -> - ( (EApp ((EOp (Binop And), pos), [arg; acc]), pos), + ( (EApp ((EOp (Binop And), mark), [arg; acc]), mark), VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty )) acc list -let negation ((arg, arg_ty) : vc_return) (pos : Pos.t) : vc_return = - (EApp ((EOp (Unop Not), pos), [arg]), pos), arg_ty +let negation ((arg, arg_ty) : 'm vc_return) (mark : 'm mark) : 'm vc_return = + (EApp ((EOp (Unop Not), mark), [arg]), mark), arg_ty -let disjunction (args : vc_return list) (pos : Pos.t) : vc_return = +let disjunction (args : 'm vc_return list) (mark : 'm mark) : 'm vc_return = let acc, list = match args with | hd :: tl -> hd, tl - | [] -> ((ELit (LBool false), pos), VarMap.empty), [] + | [] -> ((ELit (LBool false), mark), VarMap.empty), [] in List.fold_left - (fun ((acc, acc_ty) : vc_return) (arg, arg_ty) -> - ( (EApp ((EOp (Binop Or), pos), [arg; acc]), pos), + (fun ((acc, acc_ty) : 'm vc_return) (arg, arg_ty) -> + ( (EApp ((EOp (Binop Or), mark), [arg; acc]), mark), VarMap.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty )) acc list @@ -71,8 +71,8 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list = variables, or [fun () -> e1] for subscope variables. But what we really want to analyze is only [e1], so we match this outermost structure explicitely and have a clean verification condition generator that only runs on [e1] *) -let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) : - expr Marked.pos = +let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : 'm marked_expr) : + 'm marked_expr = match Marked.unmark e with | ErrorOnEmpty ( EDefault @@ -80,7 +80,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) : (ELit (LBool true), _), cons ), _ ) - when List.exists (fun x' -> Bindlib.eq_vars x x') ctx.input_vars -> + when List.exists (fun x' -> Var.eq (Var.t x) x') ctx.input_vars -> (* scope variables*) cons | EAbs (binder, [(TLit TUnit, _)]) -> @@ -90,7 +90,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) : | ErrorOnEmpty d -> d (* input subscope variables and non-input scope variable *) | _ -> - Errors.raise_spanned_error (Marked.get_mark e) + Errors.raise_spanned_error (pos e) "Internal error: this expression does not have the structure expected by \ the VC generator:\n\ %a" @@ -103,8 +103,8 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Marked.pos) : [b] such that if [b] is true, then [e] will never return an empty error. It also returns a map of all the types of locally free variables inside the expression. *) -let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Marked.pos) : - vc_return = +let rec generate_vc_must_not_return_empty (ctx : ctx) (e : 'm marked_expr) : + 'm vc_return = let out = match Marked.unmark e with | ETuple (args, _) | EArray args -> @@ -130,7 +130,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Marked.pos) : in ( vc_body_expr, List.fold_left - (fun acc (var, ty) -> VarMap.add var ty acc) + (fun acc (var, ty) -> VarMap.add (Var.t var) ty acc) vc_body_ty (List.map2 (fun x y -> x, y) (Array.to_list vars) typs) ) | EApp (f, args) -> @@ -197,8 +197,8 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Marked.pos) : [b] such that if [b] is true, then [e] will never return a conflict error. It also returns a map of all the types of locally free variables inside the expression. *) -let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Marked.pos) : - vc_return = +let rec generate_vs_must_not_return_confict (ctx : ctx) (e : 'm marked_expr) : + 'm vc_return = let out = (* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this function relies on. *) @@ -223,7 +223,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Marked.pos) : in ( vc_body_expr, List.fold_left - (fun acc (var, ty) -> VarMap.add var ty acc) + (fun acc (var, ty) -> VarMap.add (Var.t var) ty acc) vc_body_ty (List.map2 (fun x y -> x, y) (Array.to_list vars) typs) ) | EApp (f, args) -> @@ -279,8 +279,8 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : expr Marked.pos) : type verification_condition_kind = NoEmptyError | NoOverlappingExceptions -type verification_condition = { - vc_guard : expr Marked.pos; +type 'm verification_condition = { + vc_guard : 'm marked_expr; (* should have type bool *) vc_kind : verification_condition_kind; vc_scope : ScopeName.t; @@ -290,7 +290,7 @@ type verification_condition = { let rec generate_verification_conditions_scope_body_expr (ctx : ctx) - (scope_body_expr : expr scope_body_expr) : ctx * verification_condition list + (scope_body_expr : ('m expr, 'm) scope_body_expr) : ctx * 'm verification_condition list = match scope_body_expr with | Result _ -> ctx, [] @@ -301,7 +301,7 @@ let rec generate_verification_conditions_scope_body_expr let new_ctx, vc_list = match scope_let.scope_let_kind with | DestructuringInputStruct -> - { ctx with input_vars = scope_let_var :: ctx.input_vars }, [] + { ctx with input_vars = Var.t scope_let_var :: ctx.input_vars }, [] | ScopeVarDefinition | SubScopeVarDefinition -> (* For scope variables, we should check both that they never evaluate to emptyError nor conflictError. But for subscope variable definitions, @@ -328,7 +328,7 @@ let rec generate_verification_conditions_scope_body_expr (fun _ _ -> failwith "should not happen") ctx.scope_variables_typs vc_confl_typs; vc_scope = ctx.current_scope_name; - vc_variable = scope_let_var, scope_let.scope_let_pos; + vc_variable = Var.t scope_let_var, scope_let.scope_let_pos; }; ] in @@ -351,7 +351,7 @@ let rec generate_verification_conditions_scope_body_expr (fun _ _ -> failwith "should not happen") ctx.scope_variables_typs vc_empty_typs; vc_scope = ctx.current_scope_name; - vc_variable = scope_let_var, scope_let.scope_let_pos; + vc_variable = Var.t scope_let_var, scope_let.scope_let_pos; } :: vc_list | _ -> vc_list @@ -364,7 +364,7 @@ let rec generate_verification_conditions_scope_body_expr { new_ctx with scope_variables_typs = - VarMap.add scope_let_var scope_let.scope_let_typ + VarMap.add (Var.t scope_let_var) scope_let.scope_let_typ new_ctx.scope_variables_typs; } scope_let_next @@ -373,8 +373,8 @@ let rec generate_verification_conditions_scope_body_expr let rec generate_verification_conditions_scopes (decl_ctx : decl_ctx) - (scopes : expr scopes) - (s : ScopeName.t option) : verification_condition list = + (scopes : ('m expr, 'm) scopes) + (s : ScopeName.t option) : 'm verification_condition list = match scopes with | Nil -> [] | ScopeDef scope_def -> @@ -413,8 +413,8 @@ let rec generate_verification_conditions_scopes generate_verification_conditions_scopes decl_ctx next s @ vcs let generate_verification_conditions - (p : program) - (s : Dcalc.Ast.ScopeName.t option) : verification_condition list = + (p : 'm program) + (s : Dcalc.Ast.ScopeName.t option) : 'm verification_condition list = let vcs = generate_verification_conditions_scopes p.decl_ctx p.scopes s in (* We sort this list by scope name and then variable name to ensure consistent output for testing*) @@ -423,7 +423,7 @@ let generate_verification_conditions let to_str vc = Format.asprintf "%s.%s" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Marked.unmark vc.vc_variable)) + (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))) in String.compare (to_str vc1) (to_str vc2)) vcs diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli index 350645a1..da5d7b6e 100644 --- a/compiler/verification/conditions.mli +++ b/compiler/verification/conditions.mli @@ -25,8 +25,8 @@ type verification_condition_kind = (** This verification condition checks whether a definition never returns a conflict error *) -type verification_condition = { - vc_guard : Dcalc.Ast.typed_expr; +type 'm verification_condition = { + vc_guard : 'm Dcalc.Ast.marked_expr; (** This expression should have type [bool]*) vc_kind : verification_condition_kind; vc_scope : Dcalc.Ast.ScopeName.t; @@ -40,7 +40,7 @@ type verification_condition = { val generate_verification_conditions : 'm Dcalc.Ast.program -> Dcalc.Ast.ScopeName.t option -> - verification_condition list + 'm verification_condition list (** [generate_verification_conditions p None] will generate the verification conditions for all the variables of all the scopes of the program [p], while [generate_verification_conditions p (Some s)] will focus only on the diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 96d34bf3..0d7c8718 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -38,7 +38,7 @@ module type Backend = sig val translate_expr : backend_context -> - Dcalc.Ast.expr Utils.Marked.pos -> + 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding end @@ -53,7 +53,7 @@ module type BackendIO = sig val translate_expr : backend_context -> - Dcalc.Ast.expr Utils.Marked.pos -> + 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding type model @@ -62,17 +62,17 @@ module type BackendIO = sig | Success of vc_encoding * backend_context | Fail of string - val print_positive_result : Conditions.verification_condition -> string + val print_positive_result : 'm Conditions.verification_condition -> string val print_negative_result : - Conditions.verification_condition -> + 'm Conditions.verification_condition -> backend_context -> model option -> string val encode_and_check_vc : Dcalc.Ast.decl_ctx -> - Conditions.verification_condition * vc_encoding_result -> + 'm Conditions.verification_condition * vc_encoding_result -> unit end @@ -93,21 +93,21 @@ module MakeBackendIO (B : Backend) = struct | Success of B.vc_encoding * B.backend_context | Fail of string - let print_positive_result (vc : Conditions.verification_condition) : string = + let print_positive_result (vc : 'm Conditions.verification_condition) : string = match vc.Conditions.vc_kind with | Conditions.NoEmptyError -> Format.asprintf "%s This variable never returns an empty error" (Cli.with_style [ANSITerminal.yellow] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Marked.unmark vc.vc_variable))) + (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))) | Conditions.NoOverlappingExceptions -> Format.asprintf "%s No two exceptions to ever overlap for this variable" (Cli.with_style [ANSITerminal.yellow] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Marked.unmark vc.vc_variable))) + (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))) let print_negative_result - (vc : Conditions.verification_condition) + (vc : 'm Conditions.verification_condition) (ctx : B.backend_context) (model : B.model option) : string = let var_and_pos = @@ -116,14 +116,14 @@ module MakeBackendIO (B : Backend) = struct Format.asprintf "%s This variable might return an empty error:\n%s" (Cli.with_style [ANSITerminal.yellow] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Marked.unmark vc.vc_variable))) + (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))) (Pos.retrieve_loc_text (Marked.get_mark vc.vc_variable)) | Conditions.NoOverlappingExceptions -> Format.asprintf "%s At least two exceptions overlap for this variable:\n%s" (Cli.with_style [ANSITerminal.yellow] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Marked.unmark vc.vc_variable))) + (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))) (Pos.retrieve_loc_text (Marked.get_mark vc.vc_variable)) in let counterexample : string option = @@ -155,11 +155,11 @@ module MakeBackendIO (B : Backend) = struct expression [vc] **) let encode_and_check_vc (decl_ctx : decl_ctx) - (vc : Conditions.verification_condition * vc_encoding_result) : unit = + (vc : 'm Conditions.verification_condition * vc_encoding_result) : unit = let vc, z3_vc = vc in Cli.debug_print "For this variable:\n%s\n" - (Pos.retrieve_loc_text (Marked.get_mark vc.Conditions.vc_guard)); + (Pos.retrieve_loc_text (pos vc.Conditions.vc_guard)); Cli.debug_format "This verification condition was generated for %a:@\n%a" (Cli.format_with_style [ANSITerminal.yellow]) (match vc.vc_kind with @@ -182,6 +182,6 @@ module MakeBackendIO (B : Backend) = struct Cli.error_print "%s The translation to Z3 failed:\n%s" (Cli.with_style [ANSITerminal.yellow] "[%s.%s]" (Format.asprintf "%a" ScopeName.format_t vc.vc_scope) - (Bindlib.name_of (Marked.unmark vc.vc_variable))) + (Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable)))) msg end diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli index 94cd7211..52d6ac95 100644 --- a/compiler/verification/io.mli +++ b/compiler/verification/io.mli @@ -39,7 +39,7 @@ module type Backend = sig val is_model_empty : model -> bool val translate_expr : - backend_context -> Dcalc.Ast.typed_expr -> backend_context * vc_encoding + backend_context -> 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding end module type BackendIO = sig @@ -55,7 +55,7 @@ module type BackendIO = sig type vc_encoding val translate_expr : - backend_context -> Dcalc.Ast.typed_expr -> backend_context * vc_encoding + backend_context -> 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding type model @@ -63,17 +63,17 @@ module type BackendIO = sig | Success of vc_encoding * backend_context | Fail of string - val print_positive_result : Conditions.verification_condition -> string + val print_positive_result : 'm Conditions.verification_condition -> string val print_negative_result : - Conditions.verification_condition -> + 'm Conditions.verification_condition -> backend_context -> model option -> string val encode_and_check_vc : Dcalc.Ast.decl_ctx -> - Conditions.verification_condition * vc_encoding_result -> + 'm Conditions.verification_condition * vc_encoding_result -> unit end diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml index c47bf8d8..1ee78920 100644 --- a/compiler/verification/solver.ml +++ b/compiler/verification/solver.ml @@ -21,7 +21,7 @@ open Dcalc.Ast discharged by Z3, and attempts to solve them **) let solve_vc (decl_ctx : decl_ctx) - (vcs : Conditions.verification_condition list) : unit = + (vcs : 'm Conditions.verification_condition list) : 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.Io.init_backend (); diff --git a/compiler/verification/solver.mli b/compiler/verification/solver.mli index 8c972cb1..a8aa7887 100644 --- a/compiler/verification/solver.mli +++ b/compiler/verification/solver.mli @@ -17,4 +17,4 @@ (** Solves verification conditions using various proof backends *) val solve_vc : - Dcalc.Ast.decl_ctx -> Conditions.verification_condition list -> unit + Dcalc.Ast.decl_ctx -> 'm Conditions.verification_condition list -> unit diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 3e1928c6..001a14c3 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -99,7 +99,7 @@ let base_day = CalendarLib.Date.make 1900 1 1 (** [unique_name] returns the full, unique name corresponding to variable [v], as given by Bindlib **) -let unique_name (v : Var.t) : string = +let unique_name (v : 'm var) : string = Format.asprintf "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v) (** [date_to_int] translates [date] to an integer corresponding to the number of @@ -223,7 +223,7 @@ let print_model (ctx : context) (model : Model.model) : string = let v = StringMap.find symbol_name ctx.ctx_z3vars in Format.fprintf fmt "%s %s : %s" (Cli.with_style [ANSITerminal.blue] "%s" "-->") - (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) + (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of (Var.get v))) (print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e) else (* Declaration d is a function *) @@ -238,7 +238,7 @@ let print_model (ctx : context) (model : Model.model) : string = let v = StringMap.find symbol_name ctx.ctx_z3vars in Format.fprintf fmt "%s %s : %s" (Cli.with_style [ANSITerminal.blue] "%s" "-->") - (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) + (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of (Var.get v))) (* TODO: Model of a Z3 function should be pretty-printed *) (Model.FuncInterp.to_string f))) decls @@ -396,7 +396,7 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) : | TArrow (t1, t2) -> let ctx, z3_t1 = translate_typ ctx (Marked.unmark t1) in let ctx, z3_t2 = translate_typ ctx (Marked.unmark t2) in - let name = unique_name v in + let name = unique_name (Var.get v) in let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [z3_t1] z3_t2 in let ctx = add_funcdecl v fd ctx in let ctx = add_z3var name v ctx in @@ -415,7 +415,7 @@ let find_or_create_funcdecl (ctx : context) (v : Var.t) : let rec translate_op (ctx : context) (op : operator) - (args : expr Marked.pos list) : context * Expr.expr = + (args : 'm marked_expr list) : context * Expr.expr = match op with | Ternop _top -> let _e1, _e2, _e3 = @@ -426,7 +426,7 @@ let rec translate_op (Format.asprintf "[Z3 encoding] Ill-formed ternary operator application: %a" (Print.format_expr ctx.ctx_decl) - (EApp ((EOp op, Pos.no_pos), args), Pos.no_pos)) + (EApp ((EOp op, Untyped {pos=Pos.no_pos}), (List.map untype_expr args)), Untyped {pos=Pos.no_pos})) in failwith "[Z3 encoding] ternary operator application not supported" @@ -514,7 +514,7 @@ let rec translate_op (Format.asprintf "[Z3 encoding] Ill-formed binary operator application: %a" (Print.format_expr ctx.ctx_decl) - (EApp ((EOp op, Pos.no_pos), args), Pos.no_pos)) + (EApp ((EOp op, Untyped{pos=Pos.no_pos}), List.map untype_expr args), Untyped{pos=Pos.no_pos})) in match bop with @@ -561,7 +561,7 @@ let rec translate_op (Format.asprintf "[Z3 encoding] Ill-formed unary operator application: %a" (Print.format_expr ctx.ctx_decl) - (EApp ((EOp op, Pos.no_pos), args), Pos.no_pos)) + (EApp ((EOp op, Untyped{pos=Pos.no_pos}), List.map untype_expr args), Untyped{pos=Pos.no_pos})) in match uop with @@ -593,12 +593,12 @@ let rec translate_op (** [translate_expr] translate the expression [vc] to its corresponding Z3 expression **) -and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr +and translate_expr (ctx : context) (vc : 'm marked_expr) : context * Expr.expr = let translate_match_arm (head : Expr.expr) (ctx : context) - (e : expr Marked.pos * FuncDecl.func_decl list) : context * Expr.expr = + (e : 'm marked_expr * FuncDecl.func_decl list) : context * Expr.expr = let e, accessors = e in match Marked.unmark e with | EAbs (e, _) -> @@ -611,7 +611,7 @@ and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr let proj = Expr.mk_app ctx.ctx_z3 accessor [head] in (* The fresh variable should be substituted by a projection into the enum in the body, we add this to the context *) - let ctx = add_z3matchsubst fresh_v proj ctx in + let ctx = add_z3matchsubst (Var.t fresh_v) proj ctx in let body = Bindlib.msubst e [| fresh_e |] in translate_expr ctx body @@ -621,12 +621,12 @@ and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr match Marked.unmark vc with | EVar v -> ( - match VarMap.find_opt v ctx.ctx_z3matchsubsts with + match VarMap.find_opt (Var.t v) ctx.ctx_z3matchsubsts with | None -> (* We are in the standard case, where this is a true Catala variable *) - let t = VarMap.find v ctx.ctx_var in + let t = VarMap.find (Var.t v) ctx.ctx_var in let name = unique_name v in - let ctx = add_z3var name v ctx in + let ctx = add_z3var name (Var.t v) ctx in let ctx, ty = translate_typ ctx (Marked.unmark t) in let z3_var = Expr.mk_const_s ctx.ctx_z3 name ty in let ctx = @@ -698,7 +698,7 @@ and translate_expr (ctx : context) (vc : expr Marked.pos) : context * Expr.expr match Marked.unmark head with | EOp op -> translate_op ctx op args | EVar v -> - let ctx, fd = find_or_create_funcdecl ctx v in + let ctx, fd = find_or_create_funcdecl ctx (Var.t v) in (* Fold_right to preserve the order of the arguments: The head argument is appended at the head *) let ctx, z3_args = @@ -768,7 +768,7 @@ module Backend = struct 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 Marked.pos) = + let translate_expr (ctx : backend_context) (e : 'm marked_expr) = translate_expr ctx e let init_backend () =