CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Implement expansion of equality tests

Browse Source 
This adds an optional pass that recursively expands equality tests across
structures and enums, on lcalc.

NOTE: this is a temporary solution.

- all tests are completely inlined, which may be a bit bloated
- due to the lack of primitives (and expressive pattern-matching), checking
  equality on enums generates a 2-level pattern matching, quadratic in the
  number of constructors
- this is completely separate from the monomorphisation pass, which morally
  should take care of generating this code (as specific functions rather
  than inlined code)

So, while this should work as a place-holder for now, it actually seems more
reasonable mid-term (before we do it through monomorphisation) to do this
translation at the backend level, i.e. when generating the C code, when we have
full access to the representation of enums.
This commit is contained in:
Louis Gesbert 2024-07-31 22:34:50 +02:00
parent 3f6d8bf358
commit edb8db9ada
19 changed files with 263 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Makefile
View File

@ -236,8 +236,14 @@ testsuite: unit-tests
reset-tests: .FORCE $(CLERK_BIN)
$(CLERK_TEST) tests doc --reset
tests/%: .FORCE
$(CLERK_TEST) test $@
# tests/%: .FORCE
# $(CLERK_TEST) test $@
%.c.exe: %.catala_en $(CATALA_BIN) .FORCE
$(CATALA_BIN) c $<
gcc --std=c89 -Wall -pedantic -I runtimes/c/ $*.c -lgmp -Wno-unused-but-set-variable -o $*.c.exe
$@
.FORCE:
##########################################
# Website assets

7
compiler/catala_utils/cli.ml
View File

@ -351,6 +351,13 @@ module Flags = struct
versions of the enumeration, and transform tuples into named \
structs. "
let expand_ops =
value
& flag
& info ["expand-ops"]
~doc:
"In LCalc, expand equality operators to only rely on comparisons of literals. "
let dead_value_assignment =
value
& flag

1
compiler/catala_utils/cli.mli
View File

@ -58,6 +58,7 @@ module Flags : sig
val closure_conversion : bool Term.t
val keep_special_ops : bool Term.t
val monomorphize_types : bool Term.t
val expand_ops : bool Term.t
val dead_value_assignment : bool Term.t
val no_struct_literals : bool Term.t
val include_dirs : raw_file list Term.t

39
compiler/driver.ml
View File

@ -228,7 +228,8 @@ module Passes = struct
~check_invariants
~(typed : ty mark)
~closure_conversion
~monomorphize_types :
~monomorphize_types
~expand_ops :
typed Lcalc.Ast.program * Scopelang.Dependency.TVertex.t list =
let prg, type_ordering =
dcalc options ~includes ~optimize ~check_invariants ~typed
@ -240,6 +241,10 @@ module Passes = struct
| Typed _ -> Lcalc.From_dcalc.translate_program prg
| Custom _ -> invalid_arg "Driver.Passes.lcalc"
in
let prg =
if expand_ops then Lcalc.Expand_op.program prg
else prg
in
let prg =
if optimize then begin
Message.debug "Optimizing lambda calculus...";
@ -250,7 +255,9 @@ module Passes = struct
let prg =
if not closure_conversion then (
Message.debug "Retyping lambda calculus...";
Typing.program ~fail_on_any:false ~internal_check:true prg)
let prg = Typing.program ~fail_on_any:false ~internal_check:true prg in
if expand_ops then Lcalc.Expand_op.program prg
else prg)
else (
Message.debug "Performing closure conversion...";
let prg = Lcalc.Closure_conversion.closure_conversion prg in
@ -286,11 +293,12 @@ module Passes = struct
~keep_special_ops
~dead_value_assignment
~no_struct_literals
~monomorphize_types :
~monomorphize_types
~expand_ops :
Scalc.Ast.program * Scopelang.Dependency.TVertex.t list =
let prg, type_ordering =
lcalc options ~includes ~optimize ~check_invariants ~typed:Expr.typed
~closure_conversion ~monomorphize_types
~closure_conversion ~monomorphize_types ~expand_ops
in
debug_pass_name "scalc";
( Scalc.From_lcalc.translate_program
@ -710,10 +718,11 @@ module Commands = struct
check_invariants
closure_conversion
monomorphize_types
expand_ops
ex_scope_opt =
let prg, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~closure_conversion ~typed ~monomorphize_types
~closure_conversion ~typed ~monomorphize_types ~expand_ops
in
let _output_file, with_output = get_output_format options output in
with_output
@ -748,12 +757,14 @@ module Commands = struct
$ Cli.Flags.check_invariants
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.expand_ops
$ Cli.Flags.ex_scope_opt)
let interpret_lcalc
typed
closure_conversion
monomorphize_types
expand_ops
options
includes
optimize
@ -761,7 +772,7 @@ module Commands = struct
ex_scope_opt =
let prg, _ =
Passes.lcalc options ~includes ~optimize ~check_invariants
~closure_conversion ~monomorphize_types ~typed
~closure_conversion ~monomorphize_types ~typed ~expand_ops
in
Interpreter.load_runtime_modules
~hashf:(Hash.finalise ~closure_conversion ~monomorphize_types)
@ -770,7 +781,7 @@ module Commands = struct
(get_scopeopt_uid prg.decl_ctx ex_scope_opt)
let interpret_cmd =
let f lcalc closure_conversion monomorphize_types no_typing =
let f lcalc closure_conversion monomorphize_types expand_ops no_typing =
if not lcalc then
if closure_conversion || monomorphize_types then
Message.error
@ -780,8 +791,8 @@ module Commands = struct
else if no_typing then interpret_dcalc Expr.untyped
else interpret_dcalc Expr.typed
else if no_typing then
interpret_lcalc Expr.untyped closure_conversion monomorphize_types
else interpret_lcalc Expr.typed closure_conversion monomorphize_types
interpret_lcalc Expr.untyped closure_conversion monomorphize_types expand_ops
else interpret_lcalc Expr.typed closure_conversion monomorphize_types expand_ops
in
Cmd.v
(Cmd.info "interpret"
@ -794,6 +805,7 @@ module Commands = struct
$ Cli.Flags.lcalc
$ Cli.Flags.closure_conversion
$ Cli.Flags.monomorphize_types
$ Cli.Flags.expand_ops
$ Cli.Flags.no_typing
$ Cli.Flags.Global.options
$ Cli.Flags.include_dirs
@ -812,6 +824,7 @@ module Commands = struct
let prg, type_ordering =
Passes.lcalc options ~includes ~optimize ~check_invariants
~typed:Expr.typed ~closure_conversion ~monomorphize_types:false
~expand_ops:true
in
let output_file, with_output =
get_output_format options ~ext:".ml" output
@ -850,11 +863,12 @@ module Commands = struct
dead_value_assignment
no_struct_literals
monomorphize_types
expand_ops
ex_scope_opt =
let prg, _ =
Passes.scalc options ~includes ~optimize ~check_invariants
~closure_conversion ~keep_special_ops ~dead_value_assignment
~no_struct_literals ~monomorphize_types
~no_struct_literals ~monomorphize_types ~expand_ops
in
let _output_file, with_output = get_output_format options output in
with_output
@ -891,6 +905,7 @@ module Commands = struct
$ Cli.Flags.dead_value_assignment
$ Cli.Flags.no_struct_literals
$ Cli.Flags.monomorphize_types
$ Cli.Flags.expand_ops
$ Cli.Flags.ex_scope_opt)
let python
@ -903,7 +918,7 @@ module Commands = struct
let prg, type_ordering =
Passes.scalc options ~includes ~optimize ~check_invariants
~closure_conversion ~keep_special_ops:false ~dead_value_assignment:true
~no_struct_literals:false ~monomorphize_types:false
~no_struct_literals:false ~monomorphize_types:false ~expand_ops:false
in
let output_file, with_output =
@ -933,7 +948,7 @@ module Commands = struct
Passes.scalc options ~includes ~optimize ~check_invariants
~closure_conversion:true ~keep_special_ops:true
~dead_value_assignment:false ~no_struct_literals:true
~monomorphize_types:false
~monomorphize_types:false ~expand_ops:true
in
let output_file, with_output = get_output_format options ~ext:".c" output in
Message.debug "Compiling program into C...";

2
compiler/driver.mli
View File

@ -53,6 +53,7 @@ module Passes : sig
typed:'m Shared_ast.mark ->
closure_conversion:bool ->
monomorphize_types:bool ->
expand_ops:bool ->
Shared_ast.typed Lcalc.Ast.program * Scopelang.Dependency.TVertex.t list
val scalc :
@ -65,6 +66,7 @@ module Passes : sig
dead_value_assignment:bool ->
no_struct_literals:bool ->
monomorphize_types:bool ->
expand_ops:bool ->
Scalc.Ast.program * Scopelang.Dependency.TVertex.t list
end

139
compiler/lcalc/expand_op.ml Normal file
View File

@ -0,0 +1,139 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2024 Inria,
contributor: Louis Gesbert <louis.gesbert@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
open Catala_utils
open Shared_ast
let rec resolve_eq ctx pos ty args m =
let conjunction = function
| [] -> Expr.elit (LBool true) m
| e0 :: el ->
List.fold_left (fun acc e ->
Expr.eappop ~op:(And, pos) ~args:[acc; e]
~tys:[TLit TBool, pos; TLit TBool, pos] m)
e0 el
in
match Mark.remove ty with
| TArrow _ | TClosureEnv -> Message.error "Invalid comparison of functions"
| TLit TUnit -> Expr.elit (LBool true) m
| TLit TBool -> Expr.eappop ~op:(Eq_boo_boo, pos) ~args ~tys:[ty; ty] m
| TLit TInt -> Expr.eappop ~op:(Eq_int_int, pos) ~args ~tys:[ty; ty] m
| TLit TRat -> Expr.eappop ~op:(Eq_rat_rat, pos) ~args ~tys:[ty; ty] m
| TLit TMoney -> Expr.eappop ~op:(Eq_mon_mon, pos) ~args ~tys:[ty; ty] m
| TLit TDuration -> Expr.eappop ~op:(Eq_dur_dur, pos) ~args ~tys:[ty; ty] m
| TLit TDate -> Expr.eappop ~op:(Eq_dat_dat, pos) ~args ~tys:[ty; ty] m
| TTuple tys ->
let size = List.length tys in
let eqs =
List.mapi
(fun i ty ->
resolve_eq ctx pos ty
(List.map (fun e -> Expr.make_tupleaccess e i size pos) args)
m)
tys
in
conjunction eqs
| TStruct name ->
let fields = StructName.Map.find name ctx.ctx_structs in
let eqs =
List.rev @@
StructField.Map.fold (fun field ty acc ->
resolve_eq ctx pos ty
(List.map (fun e ->
Expr.estructaccess ~name ~field ~e (Expr.with_ty m ty))
args)
m
:: acc)
fields []
in
conjunction eqs
| TEnum name ->
(* FIXME: this is terrible (quadratic in size in the number of variants) ; but we need a new operator or specific backend constructs to be able to do better, matching is the only possible way to deconstruct an enum at the moment *)
let (arg1, arg2) = match args with
| [ arg1; arg2 ] -> arg1, arg2
| _ -> assert false
in
let constrs = EnumName.Map.find name ctx.ctx_enums in
let cases =
EnumConstructor.Map.mapi (fun cstr ty ->
let v1 = Var.make "v1" in
let cases =
EnumConstructor.Map.mapi (fun cstr2 ty ->
if EnumConstructor.equal cstr cstr2 then
let v2 = Var.make "v2" in
Expr.make_abs [|v2|]
(resolve_eq ctx pos ty
[Expr.evar v1 (Expr.with_ty m ty); Expr.evar v2 (Expr.with_ty m ty)]
m)
[ty]
pos
else
Expr.make_abs [|Var.make "_"|] (Expr.elit (LBool false) m) [ty] pos)
constrs
in
Expr.make_abs [|v1|]
(Expr.ematch ~name ~e:arg2 ~cases m)
[ty]
pos)
constrs
in
Expr.ematch ~name ~e:arg1 ~cases m
| TArray ty ->
let tbool = TLit TBool, pos in
let map2_f =
let x = Var.make "x" in
let y = Var.make "y" in
Expr.make_abs [|x; y|]
(resolve_eq ctx pos ty
[Expr.evar x (Expr.with_ty m ty); Expr.evar y (Expr.with_ty m ty)]
m)
[ty; ty]
pos
in
let fold_f =
let acc = Var.make "acc" in
let x = Var.make "x" in
Expr.make_abs [|acc; x|]
(conjunction [Expr.evar acc m;
Expr.evar x m])
[tbool; tbool]
pos
in
let bool_list =
Expr.eappop ~op:(Map2, pos) ~args:(map2_f :: args)
~tys:[TArrow ([ty; ty], (tbool)), pos;
TArray ty, pos;
TArray ty, pos]
(Expr.with_ty m (TArray tbool, pos))
in
Expr.eappop ~op:(Fold, pos) ~args:[fold_f; Expr.elit (LBool true) m; bool_list]
~tys:[TArrow ([tbool; tbool], tbool), pos;
tbool;
TArray tbool, pos]
m
| TOption _ | TDefault _ -> assert false
| TAny ->
Message.error ~internal:true "Unknown type for equality resolution"
let rec expr ctx = function
| EAppOp { op = Eq, pos; args; tys = [ty; ty2] }, m ->
assert (Type.equal ty ty2);
let args = List.map (expr ctx) args in
resolve_eq ctx pos ty args m
| e -> Expr.map ~f:(expr ctx) ~op:Fun.id e
let program p =
Program.map_exprs ~varf:Fun.id ~f:(expr p.decl_ctx) p

23
compiler/lcalc/expand_op.mli Normal file
View File

@ -0,0 +1,23 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2024 Inria,
contributor: Louis Gesbert <louis.gesbert@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
(** This transformation expands the equality operator, that is polymorphic and needs code generation on the backends that don't natively support it ; note that this is a place-holder, generating inline expansions, and is planned to be replaced with a more serious implementation that generates specific functions. In particular, currently, comparison of enums is quadratic in size. *)
open Shared_ast
val expr: decl_ctx -> 'm Ast.expr -> 'm Ast.expr boxed
val program: 'm Ast.program -> 'm Ast.program

2
compiler/plugins/api_web.ml
View File

@ -477,7 +477,7 @@ let run
let options = Global.enforce_options ~trace:true () in
let prg, type_ordering =
Driver.Passes.lcalc options ~includes ~optimize ~check_invariants
~closure_conversion ~typed:Expr.typed ~monomorphize_types
~closure_conversion ~typed:Expr.typed ~monomorphize_types ~expand_ops:false
in
let jsoo_output_file, with_formatter =
Driver.Commands.get_output_format options ~ext:"_api_web.ml" output

2
compiler/plugins/explain.ml
View File

@ -1036,7 +1036,7 @@ let expr_to_dot_label0 :
let open Op in
let str =
match o with
| Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dur_dur | Eq_dat_dat | Eq
| Eq_boo_boo | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dur_dur | Eq_dat_dat | Eq
->
"="
| Minus_int | Minus_rat | Minus_mon | Minus_dur | Minus -> "-"

2
compiler/plugins/json_schema.ml
View File

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

2
compiler/plugins/python.ml
View File

@ -27,7 +27,7 @@ let run includes output optimize check_invariants closure_conversion options =
let prg, type_ordering =
Driver.Passes.scalc options ~includes ~optimize ~check_invariants
~closure_conversion ~keep_special_ops:false ~dead_value_assignment:true
~no_struct_literals:false ~monomorphize_types:false
~no_struct_literals:false ~monomorphize_types:false ~expand_ops:false
in
let output_file, with_output = get_output_format options ~ext:".py" output in

11
compiler/scalc/to_c.ml
View File

@ -621,7 +621,7 @@ let rec format_statement
@,@[<hov 2>catala_error(catala_assertion_failed,@ %a);@]\
@;<1 -2>}@]" (format_expression ctx)
e1
format_var (Pos.Map.find (Mark.get s) ctx.lifted_pos)
format_var (Pos.Map.find (Mark.get e1) ctx.lifted_pos)
| _ -> .
(* | SSpecialOp (OHandleDefaultOpt { exceptions; just; cons; return_typ }) ->
* let e_name =
@ -712,6 +712,15 @@ and format_block (ctx : ctx) (fmt : Format.formatter) (b : block) : unit =
| _ -> pmap)
b Pos.Map.empty
in
let new_pos =
List.fold_left
(fun pmap -> function
| SAssert _, pos ->
let v = VarName.fresh ("pos", pos) in
Pos.Map.add pos v pmap
| _ -> pmap)
new_pos b
in
let new_pos =
Pos.Map.merge (fun _ v1 v2 -> match v1 with None -> v2 | _ -> None)
ctx.lifted_pos new_pos

1
compiler/scalc/to_python.ml
View File

@ -71,6 +71,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
Format.pp_print_string fmt "/"
| And -> Format.pp_print_string fmt "and"
| Or -> Format.pp_print_string fmt "or"
| Eq -> Format.pp_print_string fmt "=="
| Xor -> Format.pp_print_string fmt "!="
| Lt_int_int | Lt_rat_rat | Lt_mon_mon | Lt_dat_dat | Lt_dur_dur ->
Format.pp_print_string fmt "<"

17
compiler/shared_ast/definitions.ml
View File

@ -301,6 +301,7 @@ module Op = struct
| Or : < monomorphic ; .. > t
| Xor : < monomorphic ; .. > t
(* * polymorphic *)
| Eq : < polymorphic ; .. > t
| Map : < polymorphic ; .. > t
| Map2 : < polymorphic ; .. > t
| Concat : < polymorphic ; .. > t
@ -330,13 +331,6 @@ module Op = struct
| Div_mon_rat : < resolved ; .. > t
| Div_mon_mon : < resolved ; .. > t
| Div_dur_dur : < resolved ; .. > t
| Eq : < overloaded ; .. > t
| Eq_boo_boo : < resolved ; .. > t
| Eq_int_int : < resolved ; .. > t
| Eq_rat_rat : < resolved ; .. > t
| Eq_mon_mon : < resolved ; .. > t
| Eq_dat_dat : < resolved ; .. > t
| Eq_dur_dur : < resolved ; .. > t
| Lt : < overloaded ; .. > t
| Lt_int_int : < resolved ; .. > t
| Lt_rat_rat : < resolved ; .. > t
@ -361,6 +355,15 @@ module Op = struct
| Gte_mon_mon : < resolved ; .. > t
| Gte_dat_dat : < resolved ; .. > t
| Gte_dur_dur : < resolved ; .. > t
(* Todo: Eq is not an overload at the moment, but it should be one. The
trick is that it needs generation of specific code for arrays, every
struct and enum: operators [Eq_structs of StructName.t], etc. *)
| Eq_boo_boo : < resolved ; .. > t
| Eq_int_int : < resolved ; .. > t
| Eq_rat_rat : < resolved ; .. > t
| Eq_mon_mon : < resolved ; .. > t
| Eq_dur_dur : < resolved ; .. > t
| Eq_dat_dat : < resolved ; .. > t
(* ternary *)
(* * polymorphic *)
| Reduce : < polymorphic ; .. > t

8
compiler/shared_ast/interpreter.ml
View File

@ -165,7 +165,7 @@ let handle_eq pos evaluate_operator m lang e1 e2 =
| _, _ -> false (* comparing anything else return false *)
(* Call-by-value: the arguments are expected to be already evaluated here *)
let evaluate_operator
let rec evaluate_operator
evaluate_expr
((op, opos) : < overloaded : no ; .. > operator Mark.pos)
m
@ -227,6 +227,8 @@ let evaluate_operator
effectively no-ops. *)
Mark.remove e'
| (ToClosureEnv | FromClosureEnv), _ -> err ()
| Eq, [(e1, _); (e2, _)] ->
ELit (LBool (handle_eq opos (evaluate_operator evaluate_expr) m lang e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
@ -303,7 +305,7 @@ let evaluate_operator
];
})))
init es)
| (Length | Log _ | Map | Map2 | Concat | Filter | Fold | Reduce), _ ->
| (Length | Log _ | Eq | Map | Map2 | Concat | Filter | Fold | Reduce), _ ->
err ()
| Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b))
| GetDay, [(ELit (LDate d), _)] -> ELit (LInt (o_getDay d))
@ -855,7 +857,7 @@ and partially_evaluate_expr_for_assertion_failure_message :
args = [e1; e2];
tys;
op =
( ( And | Or | Xor | Lt_int_int | Lt_rat_rat | Lt_mon_mon
( ( And | Or | Xor | Eq | Lt_int_int | Lt_rat_rat | Lt_mon_mon
| Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon
| Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon
| Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon

14
compiler/shared_ast/operator.ml
View File

@ -343,11 +343,11 @@ let kind_dispatch :
| And | Or | Xor ),
_ ) as op ->
monomorphic op
| ( ( Log _ | Length | Map | Map2 | Concat | Filter | Reduce | Fold
| ( ( Log _ | Length | Eq | Map | Map2 | Concat | Filter | Reduce | Fold
| HandleExceptions | FromClosureEnv | ToClosureEnv ),
_ ) as op ->
polymorphic op
| ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Eq | Lt | Lte | Gt
| ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt
| Gte ),
_ ) as op ->
overloaded op
@ -377,7 +377,7 @@ type 'a no_overloads =
let translate (t : 'a no_overloads t Mark.pos) : 'b no_overloads t Mark.pos =
match t with
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor | HandleExceptions | Log _ | Length | Map | Map2
| And | Or | Xor | HandleExceptions | Log _ | Length | Eq | Map | Map2
| Concat | Filter | Reduce | Fold | Minus_int | Minus_rat | Minus_mon
| Minus_dur | ToRat_int | ToRat_mon | ToMoney_rat | Round_rat | Round_mon
| Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur
@ -517,12 +517,6 @@ let resolve_overload_aux (op : overloaded t) (operands : typ_lit list) :
| Div, [TMoney; TMoney] -> Div_mon_mon, `Straight
| Div, [TMoney; TRat] -> Div_mon_rat, `Straight
| Div, [TDuration; TDuration] -> Div_dur_dur, `Straight
| Eq, [TBool; TBool] -> Eq_boo_boo, `Straight
| Eq, [TInt; TInt] -> Eq_int_int, `Straight
| Eq, [TRat; TRat] -> Eq_rat_rat, `Straight
| Eq, [TMoney; TMoney] -> Eq_mon_mon, `Straight
| Eq, [TDuration; TDuration] -> Eq_dur_dur, `Straight
| Eq, [TDate; TDate] -> Eq_dat_dat, `Straight
| Lt, [TInt; TInt] -> Lt_int_int, `Straight
| Lt, [TRat; TRat] -> Lt_rat_rat, `Straight
| Lt, [TMoney; TMoney] -> Lt_mon_mon, `Straight
@ -543,7 +537,7 @@ let resolve_overload_aux (op : overloaded t) (operands : typ_lit list) :
| Gte, [TMoney; TMoney] -> Gte_mon_mon, `Straight
| Gte, [TDuration; TDuration] -> Gte_dur_dur, `Straight
| Gte, [TDate; TDate] -> Gte_dat_dat, `Straight
| ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Eq | Lt | Lte | Gt
| ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt
| Gte ),
_ ) ->
raise Not_found

2
compiler/shared_ast/typing.ml
View File

@ -304,6 +304,7 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
let ty =
match Mark.remove op with
| Fold -> [[any2; any] @-> any2; any2; array any] @-> any2
| Eq -> [any; any] @-> bt
| Map -> [[any] @-> any2; array any] @-> array any2
| Map2 -> [[any; any2] @-> any3; array any; array any2] @-> array any3
| Filter -> [[any] @-> bt; array any] @-> array any
@ -337,6 +338,7 @@ let polymorphic_op_return_type
in
match Mark.remove op, targs with
| (Fold | Reduce), [_; tau; _] -> tau
| Eq, _ -> uf (TLit TBool)
| Map, [tf; _] -> uf (TArray (return_type tf 1))
| Map2, [tf; _; _] -> uf (TArray (return_type tf 2))
| (Filter | Concat), [_; tau] -> tau

19
compiler/verification/z3backend.real.ml
View File

@ -508,6 +508,22 @@ let rec translate_op :
be directly translated as >= in the Z3 encoding using the number of
days *)
ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2
| Eq, [(EAppOp { op = GetYear, _; args = [e1]; _ }, _); (ELit (LInt n), _)] ->
let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in
let min_date =
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int (date_of_year n))
in
let max_date =
Arithmetic.Integer.mk_numeral_i ctx.ctx_z3
(date_to_int (date_of_year (n + 1)))
in
( ctx,
Boolean.mk_and ctx.ctx_z3
[
Arithmetic.mk_ge ctx.ctx_z3 e1 min_date;
Arithmetic.mk_lt ctx.ctx_z3 e1 max_date;
] )
| And, _ -> app Boolean.mk_and
| Or, _ -> app Boolean.mk_or
| Xor, _ -> app2 Boolean.mk_xor
@ -530,8 +546,7 @@ let rec translate_op :
app2 Arithmetic.mk_gt
| (Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dat_dat | Gte_dur_dur), _ ->
app2 Arithmetic.mk_ge
| (Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat | Eq_dur_dur), _ ->
failwith "[Z3 encoding] not handling Eq"
| Eq, _ -> app2 Boolean.mk_eq
| Map, _ ->
failwith "[Z3 encoding] application of binary operator Map not supported"
| Concat, _ ->

4
runtimes/c/runtime.c
View File

@ -51,7 +51,9 @@ void catala_error(catala_error_code code,
/* --- Memory allocations --- */
#define BLOCKSIZE 4096
#define BLOCKSIZE 32 /* TODO:
For stressing the allocator for testing purposes only,
should be reverted to something like 4096 or 16384 */
struct catala_heap
{