Other pattern matching

This commit is contained in:
Denis Merigoux 2023-06-15 16:33:14 +02:00
parent a3087ee163
commit 57abfbf2c7
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
5 changed files with 9 additions and 4 deletions

View File

@ -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 ->

View File

@ -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 *)

View File

@ -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 =

View File

@ -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

View File

@ -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