Adjust plugins and warnings

This commit is contained in:
Louis Gesbert 2023-11-03 15:09:02 +01:00
parent 0be2636e65
commit ab6bec390d
10 changed files with 13 additions and 6 deletions

View File

@ -326,7 +326,7 @@ let transform_closures_program (p : 'm program) : 'm program Bindlib.box =
match Mark.remove t with
| TArrow _ -> true
| TAny -> true
| TOption t' -> type_contains_arrow t'
| TDefault t' | TOption t' -> type_contains_arrow t'
| TClosureEnv | TLit _ -> false
| TArray ts -> type_contains_arrow ts
| TTuple ts -> List.exists type_contains_arrow ts

View File

@ -61,6 +61,7 @@ let rec trans_typ_keep (tau : typ) : typ =
"The types option and closure_env should not appear before the dcalc \
-> lcalc translation step."
| TAny -> TAny
| TDefault t -> TDefault t
| TArray ts ->
TArray (TOption (trans_typ_keep ts), m) (* catala is not polymorphic *)
| TArrow ([(TLit TUnit, _)], t2) -> Mark.remove (trans_typ_keep t2)

View File

@ -202,6 +202,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name Expr.option_enum
| TDefault t -> format_typ fmt t
| TEnum e -> Format.fprintf fmt "%a.t" format_to_module_name (`Ename e)
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a@]"

View File

@ -67,6 +67,7 @@ module To_jsoo = struct
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name Expr.option_enum
| TDefault t -> format_typ fmt t
| TEnum e -> Format.fprintf fmt "%a Js.t" format_enum_name e
| TArray t1 ->
Format.fprintf fmt "@[%a@ Js.js_array Js.t@]" format_typ_with_parens t1
@ -439,7 +440,7 @@ let run
Message.raise_error "This plugin requires the --trace flag.";
let prg, _, type_ordering =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
in
let modname =
(* TODO: module directive support *)

View File

@ -1388,7 +1388,7 @@ let options =
let run includes optimize ex_scope explain_options global_options =
let prg, ctx, _ =
Driver.Passes.dcalc global_options ~includes ~optimize
~check_invariants:false
~check_invariants:false ~typed:Expr.typed
in
Interpreter.load_runtime_modules prg;
let scope = Driver.Commands.get_scope_uid ctx ex_scope in

View File

@ -216,7 +216,7 @@ let run
options =
let prg, ctx, _ =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~avoid_exceptions ~closure_conversion
~avoid_exceptions ~closure_conversion ~typed:Expr.typed
in
let output_file, with_output =
Driver.Commands.get_output_format options ~ext:"_schema.json" output

View File

@ -259,7 +259,7 @@ let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) :
let run includes optimize check_invariants ex_scope options =
let prg, ctx, _ =
Driver.Passes.dcalc options ~includes ~optimize ~check_invariants
Driver.Passes.dcalc options ~includes ~optimize ~check_invariants ~typed:Expr.typed
in
Interpreter.load_runtime_modules prg;
let scope = Driver.Commands.get_scope_uid ctx ex_scope in

View File

@ -176,6 +176,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
| TOption some_typ ->
(* We translate the option type with an overloading by Python's [None] *)
Format.fprintf fmt "Optional[%a]" format_typ some_typ
| TDefault t -> format_typ fmt t
| TEnum e -> Format.fprintf fmt "%a" format_enum_name e
| TArrow (t1, t2) ->
Format.fprintf fmt "Callable[[%a], %a]"

View File

@ -172,7 +172,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
format_typ)
ts
| TStruct s -> Format.fprintf fmt "\"catala_struct_%a\"" format_struct_name s
| TOption some_typ ->
| TOption some_typ | TDefault some_typ ->
(* We loose track of optional value as they're crammed into NULL *)
format_typ fmt some_typ
| TEnum e -> Format.fprintf fmt "\"catala_enum_%a\"" format_enum_name e

View File

@ -206,6 +206,8 @@ let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
| TAny -> failwith "[Z3 model]: Pretty-printing of Any not supported"
| TClosureEnv ->
failwith "[Z3 model]: Pretty-printing of closure_env not supported"
| TDefault _ ->
failwith "[Z3 model]: Pretty-printing of default terms 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
@ -273,6 +275,7 @@ let rec translate_typ (ctx : context) (t : naked_typ) : context * Sort.sort =
| TTuple _ -> failwith "[Z3 encoding] TTuple type not supported"
| TEnum e -> find_or_create_enum ctx e
| TOption _ -> failwith "[Z3 encoding] TOption type not supported"
| TDefault _ -> failwith "[Z3 encoding] TDefault type not supported"
| TArrow _ -> failwith "[Z3 encoding] TArrow type not supported"
| TArray _ ->
(* For now, we are only encoding the (symbolic) length of an array.