From 57abfbf2c734c5b9896b652942004671e9f2fa3a Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Thu, 15 Jun 2023 16:33:14 +0200 Subject: [PATCH] Other pattern matching --- compiler/lcalc/closure_conversion.ml | 2 +- compiler/lcalc/compile_without_exceptions.ml | 6 +++--- compiler/lcalc/to_ocaml.ml | 1 + compiler/scalc/to_python.ml | 1 + compiler/verification/z3backend.real.ml | 3 +++ 5 files changed, 9 insertions(+), 4 deletions(-) diff --git a/compiler/lcalc/closure_conversion.ml b/compiler/lcalc/closure_conversion.ml index 1ea2f5f0..e4488b79 100644 --- a/compiler/lcalc/closure_conversion.ml +++ b/compiler/lcalc/closure_conversion.ml @@ -361,7 +361,7 @@ let closure_conversion (p : 'm program) : 'm program Bindlib.box = | TArrow _ -> true | TAny -> true | TOption t' -> type_contains_arrow t' - | TLit _ -> false + | TClosureEnv | TLit _ -> false | TArray ts -> type_contains_arrow ts | TTuple ts -> List.exists type_contains_arrow ts | TEnum e -> diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 8f420379..308c87f4 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -56,10 +56,10 @@ let rec trans_typ_keep (tau : typ) : typ = | TTuple ts -> TTuple (List.map trans_typ_keep ts) | TStruct s -> TStruct s | TEnum en -> TEnum en - | TOption _ -> + | TOption _ | TClosureEnv -> Messages.raise_internal_error - "The type option should not appear before the dcalc -> lcalc \ - translation step." + "The types option and closure_env should not appear before the dcalc \ + -> lcalc translation step." | TAny -> TAny | TArray ts -> TArray (TOption (trans_typ_keep ts), m) (* catala is not polymorphic *) diff --git a/compiler/lcalc/to_ocaml.ml b/compiler/lcalc/to_ocaml.ml index 0169ca3d..1de09146 100644 --- a/compiler/lcalc/to_ocaml.ml +++ b/compiler/lcalc/to_ocaml.ml @@ -174,6 +174,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit = (t1 @ [t2]) | TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1 | TAny -> Format.fprintf fmt "_" + | TClosureEnv -> failwith "unimplemented!" let format_var (fmt : Format.formatter) (v : 'm Var.t) : unit = let lowercase_name = diff --git a/compiler/scalc/to_python.ml b/compiler/scalc/to_python.ml index c592546f..ba371d1f 100644 --- a/compiler/scalc/to_python.ml +++ b/compiler/scalc/to_python.ml @@ -184,6 +184,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit = t1 format_typ_with_parens t2 | TArray t1 -> Format.fprintf fmt "List[%a]" format_typ_with_parens t1 | TAny -> Format.fprintf fmt "Any" + | TClosureEnv -> failwith "unimplemented!" let format_name_cleaned (fmt : Format.formatter) (s : string) : unit = s diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index d1a3a31e..5875143b 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -204,6 +204,8 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string = (* For now, only the length of arrays is modeled *) Format.asprintf "(length = %s)" (Expr.to_string e) | TAny -> failwith "[Z3 model]: Pretty-printing of Any not supported" + | TClosureEnv -> + failwith "[Z3 model]: Pretty-printing of closure_env not supported" (** [print_model] pretty prints a Z3 model, used to exhibit counter examples where verification conditions are not satisfied. The context [ctx] is useful @@ -277,6 +279,7 @@ let rec translate_typ (ctx : context) (t : naked_typ) : context * Sort.sort = Ultimately, the type of an array should also contain its elements *) ctx, Arithmetic.Integer.mk_sort ctx.ctx_z3 | TAny -> failwith "[Z3 encoding] TAny type not supported" + | TClosureEnv -> failwith "[Z3 encoding] TClosureEnv type not supported" (** [find_or_create_enum] attempts to retrieve the Z3 sort corresponding to the Catala enumeration [enum]. If no such sort exists yet, it constructs it by