Replace HandleDefault* internal operators by HandleExceptions

HandleExceptions only takes an array of exceptions, and returns Some if only one
of them is Some, None if they are all None, or raises a conflict error
otherwise.

The compilation of default terms then wraps this in a match (for the result of
HandleExceptions), and an if-then-else (for the justification-consequence in the
None case).

This avoids the complexity of having to handle thunked functions as arguments.
This commit is contained in:
Louis Gesbert 2024-06-24 16:48:56 +02:00
parent b005652a85
commit 293bcd3817
17 changed files with 195 additions and 213 deletions

View File

@ -257,7 +257,7 @@ let rec transform_closures_expr :
free_vars, build_closure ctx (Var.Map.bindings free_vars) body vars tys m free_vars, build_closure ctx (Var.Map.bindings free_vars) body vars tys m
| EAppOp | EAppOp
{ {
op = ((HandleDefaultOpt | Fold | Map | Map2 | Filter | Reduce), _) as op; op = ((HandleExceptions | Fold | Map | Map2 | Filter | Reduce), _) as op;
tys; tys;
args; args;
} -> } ->
@ -534,12 +534,7 @@ let rec hoist_closures_expr :
in in
( collected_closures, ( collected_closures,
Expr.eapp ~f:(Expr.eabs new_binder tys e1_pos) ~args:new_args ~tys m ) Expr.eapp ~f:(Expr.eabs new_binder tys e1_pos) ~args:new_args ~tys m )
| EAppOp | EAppOp { op = ((Fold | Map | Filter | Reduce), _) as op; tys; args } ->
{
op = ((HandleDefaultOpt | Fold | Map | Filter | Reduce), _) as op;
tys;
args;
} ->
(* Special case for some operators: its arguments closures thunks because if (* Special case for some operators: its arguments closures thunks because if
you want to extract it as a function you need these closures to preserve you want to extract it as a function you need these closures to preserve
evaluation order, but backends that don't support closures will simply evaluation order, but backends that don't support closures will simply

View File

@ -60,26 +60,43 @@ let rec translate_default
(* Since the program is well typed, all exceptions have as type [option 't] *) (* Since the program is well typed, all exceptions have as type [option 't] *)
let pos = Expr.mark_pos mark_default in let pos = Expr.mark_pos mark_default in
let exceptions = List.map translate_expr exceptions in let exceptions = List.map translate_expr exceptions in
let exceptions_and_cons_ty = Expr.maybe_ty mark_default in let ty_option = Expr.maybe_ty mark_default in
Expr.eappop let ty_array = TArray ty_option, pos in
~op:(Op.HandleDefaultOpt, Expr.pos cons) let ty_alpha =
~tys: match ty_option with
[ | TOption ty, _ -> ty
TArray exceptions_and_cons_ty, pos; | (TAny, _) as ty -> ty
TArrow ([TLit TUnit, pos], (TLit TBool, pos)), pos; | _ -> assert false
TArrow ([TLit TUnit, pos], exceptions_and_cons_ty), pos; in
] let mark_alpha = Expr.with_ty mark_default ty_alpha in
~args: Expr.ematch ~name:Expr.option_enum
[ ~e:
Expr.earray exceptions (Expr.eappop
(Expr.map_ty (fun ty -> TArray ty, pos) mark_default); ~op:(Op.HandleExceptions, Expr.pos cons)
(* In call-by-value programming languages, as lcalc, arguments are ~tys:[ty_array]
evalulated before calling the function. Since we don't want to ~args:[Expr.earray exceptions (Expr.with_ty mark_default ty_array)]
execute the justification and conclusion while before checking every mark_default)
exceptions, we need to thunk them. *) ~cases:
Expr.thunk_term (translate_expr just); (EnumConstructor.Map.of_list
Expr.thunk_term (translate_expr cons); [
] (* Some x -> Some x *)
( Expr.some_constr,
let x = Var.make "x" in
Expr.make_abs [| x |]
(Expr.einj ~name:Expr.option_enum ~cons:Expr.some_constr
~e:(Expr.evar x mark_alpha) mark_default)
[ty_alpha] pos );
(* None -> if just then cons else None *)
( Expr.none_constr,
Expr.thunk_term
(Expr.eifthenelse (translate_expr just) (translate_expr cons)
(Expr.einj
~e:
(Expr.elit LUnit
(Expr.with_ty mark_default (TLit TUnit, pos)))
~cons:Expr.none_constr ~name:Expr.option_enum mark_default)
mark_default) );
])
mark_default mark_default
and translate_expr (e : 'm D.expr) : 'm A.expr boxed = and translate_expr (e : 'm D.expr) : 'm A.expr boxed =

View File

@ -409,21 +409,21 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
format_with_parens arg1 format_with_parens arg1
| EAppOp { op = Log _, _; args = [arg1]; _ } -> | EAppOp { op = Log _, _; args = [arg1]; _ } ->
Format.fprintf fmt "%a" format_with_parens arg1 Format.fprintf fmt "%a" format_with_parens arg1
| EAppOp (* | EAppOp
{ * {
op = (HandleDefaultOpt as op), _; * op = (HandleDefaultOpt as op), _;
args = (EArray excs, _) :: _ as args; * args = (EArray excs, _) :: _ as args;
_; * _;
} -> * } ->
let pos = List.map Expr.pos excs in * let pos = List.map Expr.pos excs in
Format.fprintf fmt "@[<hov 2>%s@ [|%a|]@ %a@]" * Format.fprintf fmt "@[<hov 2>%s@ [|%a|]@ %a@]"
(Print.operator_to_string op) * (Print.operator_to_string op)
(Format.pp_print_list * (Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ") * ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
format_pos) * format_pos)
pos * pos
(Format.pp_print_list ~pp_sep:Format.pp_print_space format_with_parens) * (Format.pp_print_list ~pp_sep:Format.pp_print_space format_with_parens)
args * args *)
| EApp { f; args; _ } -> | EApp { f; args; _ } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_with_parens f Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_with_parens f
(Format.pp_print_list (Format.pp_print_list
@ -443,6 +443,12 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
Format.fprintf ppf "%a@ " format_pos pos Format.fprintf ppf "%a@ " format_pos pos
| Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_rat | Div_dur_dur -> | Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_rat | Div_dur_dur ->
Format.fprintf ppf "%a@ " format_pos (Expr.pos (List.nth args 1)) Format.fprintf ppf "%a@ " format_pos (Expr.pos (List.nth args 1))
| HandleExceptions ->
Format.fprintf ppf "[|@[<hov>%a@]|]@ "
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
format_pos)
(List.map Expr.pos args)
| _ -> ()) | _ -> ())
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")

View File

@ -1085,7 +1085,7 @@ let expr_to_dot_label0 :
| Reduce -> xlang () ~en:"reduce" ~fr:"réunion" | Reduce -> xlang () ~en:"reduce" ~fr:"réunion"
| Filter -> xlang () ~en:"filter" ~fr:"filtre" | Filter -> xlang () ~en:"filter" ~fr:"filtre"
| Fold -> xlang () ~en:"fold" ~fr:"pliage" | Fold -> xlang () ~en:"fold" ~fr:"pliage"
| HandleDefaultOpt -> "" | HandleExceptions -> ""
| ToClosureEnv -> "" | ToClosureEnv -> ""
| FromClosureEnv -> "" | FromClosureEnv -> ""
in in

View File

@ -34,8 +34,7 @@ module VarName =
() ()
let dead_value = VarName.fresh ("dead_value", Pos.no_pos) let dead_value = VarName.fresh ("dead_value", Pos.no_pos)
let handle_default = FuncName.fresh ("handle_default", Pos.no_pos) let handle_exceptions = FuncName.fresh ("handle_exceptions", Pos.no_pos)
let handle_default_opt = FuncName.fresh ("handle_default_opt", Pos.no_pos)
type operator = Shared_ast.lcalc Shared_ast.operator type operator = Shared_ast.lcalc Shared_ast.operator

View File

@ -138,15 +138,15 @@ and translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : RevBlock.t * A.expr =
| ETupleAccess { e = e1; index; _ } -> | ETupleAccess { e = e1; index; _ } ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1 = translate_expr ctxt e1 in
e1_stmts, (A.ETupleAccess { e1 = new_e1; index }, Expr.pos expr) e1_stmts, (A.ETupleAccess { e1 = new_e1; index }, Expr.pos expr)
| EAppOp (* | EAppOp
{ * {
op = Op.HandleDefaultOpt, _; * op = Op.HandleDefaultOpt, _;
args = [_exceptions; _just; _cons]; * args = [_exceptions; _just; _cons];
tys = _; * tys = _;
} * }
when ctxt.config.keep_special_ops -> * when ctxt.config.keep_special_ops ->
(* This should be translated as a statement *) * (\* This should be translated as a statement *\)
raise (NotAnExpr { needs_a_local_decl = true }) * raise (NotAnExpr { needs_a_local_decl = true }) *)
| EAppOp { op; args; tys = _ } -> | EAppOp { op; args; tys = _ } ->
let args_stmts, new_args = translate_expr_list ctxt args in let args_stmts, new_args = translate_expr_list ctxt args in
(* FIXME: what happens if [arg] is not a tuple but reduces to one ? *) (* FIXME: what happens if [arg] is not a tuple but reduces to one ? *)
@ -274,60 +274,60 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
~tail:[A.SAssert (Mark.remove new_e), Expr.pos block_expr] ~tail:[A.SAssert (Mark.remove new_e), Expr.pos block_expr]
e_stmts e_stmts
| EFatalError err -> [SFatalError err, Expr.pos block_expr] | EFatalError err -> [SFatalError err, Expr.pos block_expr]
| EAppOp (* | EAppOp
{ op = Op.HandleDefaultOpt, _; tys = _; args = [exceptions; just; cons] } * { op = Op.HandleDefaultOpt, _; tys = _; args = [exceptions; just; cons] }
when ctxt.config.keep_special_ops -> * when ctxt.config.keep_special_ops ->
let exceptions = * let exceptions =
match Mark.remove exceptions with * match Mark.remove exceptions with
| EStruct { fields; _ } -> ( * | EStruct { fields; _ } -> (
let _, exceptions = * let _, exceptions =
List.find * List.find
(fun (field, _) -> * (fun (field, _) ->
String.equal (Mark.remove (StructField.get_info field)) "content") * String.equal (Mark.remove (StructField.get_info field)) "content")
(StructField.Map.bindings fields) * (StructField.Map.bindings fields)
in * in
match Mark.remove exceptions with * match Mark.remove exceptions with
| EArray exceptions -> exceptions * | EArray exceptions -> exceptions
| _ -> failwith "should not happen") * | _ -> failwith "should not happen")
| _ -> failwith "should not happen" * | _ -> failwith "should not happen"
in * in
let just = unthunk just in * let just = unthunk just in
let cons = unthunk cons in * let cons = unthunk cons in
let exceptions_stmts, new_exceptions = * let exceptions_stmts, new_exceptions =
translate_expr_list ctxt exceptions * translate_expr_list ctxt exceptions
in * in
let just_stmts, new_just = translate_expr ctxt just in * let just_stmts, new_just = translate_expr ctxt just in
let cons_stmts, new_cons = translate_expr ctxt cons in * let cons_stmts, new_cons = translate_expr ctxt cons in
RevBlock.rebuild exceptions_stmts * RevBlock.rebuild exceptions_stmts
~tail: * ~tail:
(RevBlock.rebuild just_stmts * (RevBlock.rebuild just_stmts
~tail: * ~tail:
[ * [
( A.SSpecialOp * ( A.SSpecialOp
(OHandleDefaultOpt * (OHandleDefaultOpt
{ * {
exceptions = new_exceptions; * exceptions = new_exceptions;
just = new_just; * just = new_just;
cons = * cons =
RevBlock.rebuild cons_stmts * RevBlock.rebuild cons_stmts
~tail: * ~tail:
[ * [
( (match ctxt.inside_definition_of with * ( (match ctxt.inside_definition_of with
| None -> A.SReturn (Mark.remove new_cons) * | None -> A.SReturn (Mark.remove new_cons)
| Some x -> * | Some x ->
A.SLocalDef * A.SLocalDef
{ * {
name = Mark.copy new_cons x; * name = Mark.copy new_cons x;
expr = new_cons; * expr = new_cons;
typ = * typ =
Expr.maybe_ty (Mark.get block_expr); * Expr.maybe_ty (Mark.get block_expr);
}), * }),
Expr.pos block_expr ); * Expr.pos block_expr );
]; * ];
return_typ = Expr.maybe_ty (Mark.get block_expr); * return_typ = Expr.maybe_ty (Mark.get block_expr);
}), * }),
Expr.pos block_expr ); * Expr.pos block_expr );
]) * ]) *)
| EApp { f = EAbs { binder; tys }, binder_mark; args; _ } -> | EApp { f = EAbs { binder; tys }, binder_mark; args; _ } ->
(* This defines multiple local variables at the time *) (* This defines multiple local variables at the time *)
let binder_pos = Expr.mark_pos binder_mark in let binder_pos = Expr.mark_pos binder_mark in

View File

@ -313,7 +313,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
| Reduce -> Format.pp_print_string fmt "catala_list_reduce" | Reduce -> Format.pp_print_string fmt "catala_list_reduce"
| Filter -> Format.pp_print_string fmt "catala_list_filter" | Filter -> Format.pp_print_string fmt "catala_list_filter"
| Fold -> Format.pp_print_string fmt "catala_list_fold_left" | Fold -> Format.pp_print_string fmt "catala_list_fold_left"
| HandleDefaultOpt | FromClosureEnv | ToClosureEnv | Map2 -> | HandleExceptions | FromClosureEnv | ToClosureEnv | Map2 ->
failwith "unimplemented" failwith "unimplemented"
let _format_string_list (fmt : Format.formatter) (uids : string list) : unit = let _format_string_list (fmt : Format.formatter) (uids : string list) : unit =
@ -367,8 +367,8 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1 Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp { op; args = [arg1] } -> | EAppOp { op; args = [arg1] } ->
Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1 Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1
| EAppOp { op = HandleDefaultOpt, _; args = _ } -> (* | EAppOp { op = HandleDefaultOpt, _; args = _ } ->
failwith "should not happen because of keep_special_ops" * failwith "should not happen because of keep_special_ops" *)
| EApp { f; args } -> | EApp { f; args } ->
Format.fprintf fmt "%a(@[<hov 0>%a)@]" (format_expression ctx) f Format.fprintf fmt "%a(@[<hov 0>%a)@]" (format_expression ctx) f
(Format.pp_print_list (Format.pp_print_list

View File

@ -88,7 +88,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
| Reduce -> Format.pp_print_string fmt "list_reduce" | Reduce -> Format.pp_print_string fmt "list_reduce"
| Filter -> Format.pp_print_string fmt "list_filter" | Filter -> Format.pp_print_string fmt "list_filter"
| Fold -> Format.pp_print_string fmt "list_fold_left" | Fold -> Format.pp_print_string fmt "list_fold_left"
| HandleDefaultOpt -> Format.pp_print_string fmt "handle_default_opt" | HandleExceptions -> Format.pp_print_string fmt "handle_exceptions"
| FromClosureEnv | ToClosureEnv -> failwith "unimplemented" | FromClosureEnv | ToClosureEnv -> failwith "unimplemented"
let format_uid_list (fmt : Format.formatter) (uids : Uid.MarkedString.info list) let format_uid_list (fmt : Format.formatter) (uids : Uid.MarkedString.info list)
@ -348,27 +348,25 @@ let rec format_expression ctx (fmt : Format.formatter) (e : expr) : unit =
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1 Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp { op; args = [arg1] } -> | EAppOp { op; args = [arg1] } ->
Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1 Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1
| EAppOp { op = (HandleDefaultOpt, _) as op; args } -> (* | EAppOp { op = ((HandleDefaultOpt), _) as op; args } ->
let pos = Mark.get e in * let pos = Mark.get e in
Format.fprintf fmt * Format.fprintf fmt
"%a(@[<hov 0>SourcePosition(filename=\"%s\",@ start_line=%d,@ \ * "%a(@[<hov 0>SourcePosition(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]" * start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]"
format_op op (Pos.get_file pos) (Pos.get_start_line pos) * format_op op (Pos.get_file pos) (Pos.get_start_line pos)
(Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos) * (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
format_string_list (Pos.get_law_info pos) * format_string_list (Pos.get_law_info pos)
* (Format.pp_print_list
* ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
* (format_expression ctx))
* args *)
| EApp { f = EFunc x, _; args = [(EArray el, _)] as args }
when Ast.FuncName.compare x Ast.handle_exceptions = 0 ->
Format.fprintf fmt "%a([%a], %a)@]" format_func_name x
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") ~pp_sep:(fun ppf () -> Format.fprintf ppf ",@ ")
(format_expression ctx)) format_position)
args (List.map Mark.get el)
| EApp { f = EFunc x, pos; args }
when Ast.FuncName.compare x Ast.handle_default = 0
|| Ast.FuncName.compare x Ast.handle_default_opt = 0 ->
Format.fprintf fmt
"%a(@[<hov 0>SourcePosition(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]"
format_func_name x (Pos.get_file pos) (Pos.get_start_line pos)
(Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos)
format_string_list (Pos.get_law_info pos)
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx)) (format_expression ctx))

View File

@ -103,7 +103,7 @@ let format_op (fmt : Format.formatter) (op : operator Mark.pos) : unit =
| Reduce -> Format.pp_print_string fmt "catala_list_reduce" | Reduce -> Format.pp_print_string fmt "catala_list_reduce"
| Filter -> Format.pp_print_string fmt "catala_list_filter" | Filter -> Format.pp_print_string fmt "catala_list_filter"
| Fold -> Format.pp_print_string fmt "catala_list_fold_left" | Fold -> Format.pp_print_string fmt "catala_list_fold_left"
| HandleDefaultOpt | FromClosureEnv | ToClosureEnv -> failwith "unimplemented" | HandleExceptions | FromClosureEnv | ToClosureEnv -> failwith "unimplemented"
let format_string_list (fmt : Format.formatter) (uids : string list) : unit = let format_string_list (fmt : Format.formatter) (uids : string list) : unit =
let sanitize_quotes = Re.compile (Re.char '"') in let sanitize_quotes = Re.compile (Re.char '"') in
@ -320,7 +320,7 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1 Format.fprintf fmt "%a %a" format_op op (format_expression ctx) arg1
| EAppOp { op; args = [arg1] } -> | EAppOp { op; args = [arg1] } ->
Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1 Format.fprintf fmt "%a(%a)" format_op op (format_expression ctx) arg1
| EAppOp { op = HandleDefaultOpt, _; _ } -> | EAppOp { op = HandleExceptions, _; _ } ->
Message.error ~internal:true Message.error ~internal:true
"R compilation does not currently support the avoiding of exceptions" "R compilation does not currently support the avoiding of exceptions"
(* TODO: port the following to avoid-exceptions (* TODO: port the following to avoid-exceptions
@ -337,8 +337,7 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
* (format_expression ctx)) * (format_expression ctx))
* args *) * args *)
| EApp { f = EFunc x, pos; args } | EApp { f = EFunc x, pos; args }
when Ast.FuncName.compare x Ast.handle_default = 0 when Ast.FuncName.compare x Ast.handle_exceptions = 0 ->
|| Ast.FuncName.compare x Ast.handle_default_opt = 0 ->
Format.fprintf fmt Format.fprintf fmt
"%a(@[<hov 0>catala_position(filename=\"%s\",@ start_line=%d,@ \ "%a(@[<hov 0>catala_position(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]" start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]"

View File

@ -372,7 +372,7 @@ module Op = struct
(* * polymorphic *) (* * polymorphic *)
| Reduce : < polymorphic ; .. > t | Reduce : < polymorphic ; .. > t
| Fold : < polymorphic ; .. > t | Fold : < polymorphic ; .. > t
| HandleDefaultOpt : < polymorphic ; .. > t | HandleExceptions : < polymorphic ; .. > t
end end
type 'a operator = 'a Op.t type 'a operator = 'a Op.t

View File

@ -422,7 +422,7 @@ let rec evaluate_operator
ELit (LBool (o_eq_dat_dat x y)) ELit (LBool (o_eq_dat_dat x y))
| Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] -> | Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (o_eq_dur_dur (rpos ()) x y)) ELit (LBool (o_eq_dur_dur (rpos ()) x y))
| HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> ( | HandleExceptions, [(EArray exps, _)] -> (
let valid_exceptions = let valid_exceptions =
ListLabels.filter exps ~f:(function ListLabels.filter exps ~f:(function
| EInj { name; cons; _ }, _ when EnumName.equal name Expr.option_enum -> | EInj { name; cons; _ }, _ when EnumName.equal name Expr.option_enum ->
@ -430,28 +430,9 @@ let rec evaluate_operator
| _ -> err ()) | _ -> err ())
in in
match valid_exceptions with match valid_exceptions with
| [] -> ( | [] ->
let e = evaluate_expr (Expr.unthunk_term_nobox justification) in EInj
match Mark.remove e with { name = Expr.option_enum; cons = Expr.none_constr; e = ELit LUnit, m }
| ELit (LBool true) ->
Mark.remove (evaluate_expr (Expr.unthunk_term_nobox conclusion))
| ELit (LBool false) ->
EInj
{
name = Expr.option_enum;
cons = Expr.none_constr;
e = Mark.copy justification (ELit LUnit);
}
| EInj { name; cons; e }
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.none_constr ->
EInj
{
name = Expr.option_enum;
cons = Expr.none_constr;
e = Mark.copy e (ELit LUnit);
}
| _ -> err ())
| [((EInj { cons; name; _ } as e), _)] | [((EInj { cons; name; _ } as e), _)]
when EnumName.equal name Expr.option_enum when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr -> && EnumConstructor.equal cons Expr.some_constr ->
@ -472,7 +453,7 @@ let rec evaluate_operator
| Lte_mon_mon | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_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 | Gt_mon_mon | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat
| Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat | Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleDefaultOpt ), | Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleExceptions ),
_ ) -> _ ) ->
err () err ()

View File

@ -108,7 +108,7 @@ let name : type a. a t -> string = function
| Eq_dur_dur -> "o_eq_dur_dur" | Eq_dur_dur -> "o_eq_dur_dur"
| Eq_dat_dat -> "o_eq_dat_dat" | Eq_dat_dat -> "o_eq_dat_dat"
| Fold -> "o_fold" | Fold -> "o_fold"
| HandleDefaultOpt -> "o_handledefaultopt" | HandleExceptions -> "handle_exceptions"
| ToClosureEnv -> "o_toclosureenv" | ToClosureEnv -> "o_toclosureenv"
| FromClosureEnv -> "o_fromclosureenv" | FromClosureEnv -> "o_fromclosureenv"
@ -231,7 +231,7 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
| Eq_dat_dat, Eq_dat_dat | Eq_dat_dat, Eq_dat_dat
| Eq_dur_dur, Eq_dur_dur | Eq_dur_dur, Eq_dur_dur
| Fold, Fold | Fold, Fold
| HandleDefaultOpt, HandleDefaultOpt | HandleExceptions, HandleExceptions
| FromClosureEnv, FromClosureEnv | ToClosureEnv, ToClosureEnv -> 0 | FromClosureEnv, FromClosureEnv | ToClosureEnv, ToClosureEnv -> 0
| Not, _ -> -1 | _, Not -> 1 | Not, _ -> -1 | _, Not -> 1
| Length, _ -> -1 | _, Length -> 1 | Length, _ -> -1 | _, Length -> 1
@ -316,7 +316,7 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
| Eq_mon_mon, _ -> -1 | _, Eq_mon_mon -> 1 | Eq_mon_mon, _ -> -1 | _, Eq_mon_mon -> 1
| Eq_dat_dat, _ -> -1 | _, Eq_dat_dat -> 1 | Eq_dat_dat, _ -> -1 | _, Eq_dat_dat -> 1
| Eq_dur_dur, _ -> -1 | _, Eq_dur_dur -> 1 | Eq_dur_dur, _ -> -1 | _, Eq_dur_dur -> 1
| HandleDefaultOpt, _ -> -1 | _, HandleDefaultOpt -> 1 | HandleExceptions, _ -> -1 | _, HandleExceptions -> 1
| FromClosureEnv, _ -> -1 | _, FromClosureEnv -> 1 | FromClosureEnv, _ -> -1 | _, FromClosureEnv -> 1
| ToClosureEnv, _ -> -1 | _, ToClosureEnv -> 1 | ToClosureEnv, _ -> -1 | _, ToClosureEnv -> 1
| Fold, _ | _, Fold -> . | Fold, _ | _, Fold -> .
@ -341,7 +341,7 @@ let kind_dispatch :
_ ) as op -> _ ) as op ->
monomorphic op monomorphic op
| ( ( Log _ | Length | Eq | Map | Map2 | Concat | Filter | Reduce | Fold | ( ( Log _ | Length | Eq | Map | Map2 | Concat | Filter | Reduce | Fold
| HandleDefaultOpt | FromClosureEnv | ToClosureEnv ), | HandleExceptions | FromClosureEnv | ToClosureEnv ),
_ ) as op -> _ ) as op ->
polymorphic op polymorphic op
| ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt | ( ( Minus | ToRat | ToMoney | Round | Add | Sub | Mult | Div | Lt | Lte | Gt
@ -374,7 +374,7 @@ type 'a no_overloads =
let translate (t : 'a no_overloads t Mark.pos) : 'b no_overloads t Mark.pos = let translate (t : 'a no_overloads t Mark.pos) : 'b no_overloads t Mark.pos =
match t with match t with
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor | HandleDefaultOpt | Log _ | Length | Eq | Map | Map2 | And | Or | Xor | HandleExceptions | Log _ | Length | Eq | Map | Map2
| Concat | Filter | Reduce | Fold | Minus_int | Minus_rat | Minus_mon | Concat | Filter | Reduce | Fold | Minus_int | Minus_rat | Minus_mon
| Minus_dur | ToRat_int | ToRat_mon | ToMoney_rat | Round_rat | Round_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 | Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur

View File

@ -280,7 +280,7 @@ let operator_to_string : type a. a Op.t -> string =
| Eq_dur_dur -> "=^" | Eq_dur_dur -> "=^"
| Eq_dat_dat -> "=@" | Eq_dat_dat -> "=@"
| Fold -> "fold" | Fold -> "fold"
| HandleDefaultOpt -> "handle_default_opt" | HandleExceptions -> "handle_exceptions"
| ToClosureEnv -> "to_closure_env" | ToClosureEnv -> "to_closure_env"
| FromClosureEnv -> "from_closure_env" | FromClosureEnv -> "from_closure_env"
@ -324,7 +324,7 @@ let operator_to_shorter_string : type a. a Op.t -> string =
| Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dur_dur | Gte_dat_dat | Gte -> | Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dur_dur | Gte_dat_dat | Gte ->
">=" ">="
| Fold -> "fold" | Fold -> "fold"
| HandleDefaultOpt -> "handle_default_opt" | HandleExceptions -> "handle_exceptions"
| ToClosureEnv -> "to_closure_env" | ToClosureEnv -> "to_closure_env"
| FromClosureEnv -> "from_closure_env" | FromClosureEnv -> "from_closure_env"
@ -400,7 +400,7 @@ module Precedence = struct
| Div | Div_int_int | Div_rat_rat | Div_mon_rat | Div_mon_mon | Div | Div_int_int | Div_rat_rat | Div_mon_rat | Div_mon_mon
| Div_dur_dur -> | Div_dur_dur ->
Op Div Op Div
| HandleDefaultOpt | Map | Map2 | Concat | Filter | Reduce | Fold | HandleExceptions | Map | Map2 | Concat | Filter | Reduce | Fold
| ToClosureEnv | FromClosureEnv -> | ToClosureEnv | FromClosureEnv ->
App) App)
| EApp _ -> App | EApp _ -> App
@ -865,13 +865,12 @@ let enum
fmt fmt
(pp_name : Format.formatter -> unit) (pp_name : Format.formatter -> unit)
(c : typ EnumConstructor.Map.t) = (c : typ EnumConstructor.Map.t) =
Format.fprintf fmt "@[<h 0>%a %t %a@ %a@]" keyword "type" pp_name punctuation Format.fprintf fmt "@[<h 0>%a %t %a@ %a@]@," keyword "type" pp_name
"=" punctuation "="
(EnumConstructor.Map.format_bindings (EnumConstructor.Map.format_bindings ~pp_sep:Format.pp_print_space
~pp_sep:(fun _ _ -> ())
(fun fmt pp_n ty -> (fun fmt pp_n ty ->
Format.fprintf fmt "@[<hov2> %a %t %a %a@]@," punctuation "|" pp_n Format.fprintf fmt "@[<hov2>%a %t %a %a@]" punctuation "|" pp_n keyword
keyword "of" "of"
(if debug then typ_debug else typ decl_ctx) (if debug then typ_debug else typ decl_ctx)
ty)) ty))
c c

View File

@ -294,7 +294,6 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
let any2 = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in let any2 = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in
let any3 = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in let any3 = lazy (UnionFind.make (TAny (Any.fresh ()), pos)) in
let bt = lazy (UnionFind.make (TLit TBool, pos)) in let bt = lazy (UnionFind.make (TLit TBool, pos)) in
let ut = lazy (UnionFind.make (TLit TUnit, pos)) in
let it = lazy (UnionFind.make (TLit TInt, pos)) in let it = lazy (UnionFind.make (TLit TInt, pos)) in
let cet = lazy (UnionFind.make (TClosureEnv, pos)) in let cet = lazy (UnionFind.make (TClosureEnv, pos)) in
let array a = lazy (UnionFind.make (TArray (Lazy.force a), pos)) in let array a = lazy (UnionFind.make (TArray (Lazy.force a), pos)) in
@ -314,8 +313,7 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
| Log (PosRecordIfTrueBool, _) -> [bt] @-> bt | Log (PosRecordIfTrueBool, _) -> [bt] @-> bt
| Log _ -> [any] @-> any | Log _ -> [any] @-> any
| Length -> [array any] @-> it | Length -> [array any] @-> it
| HandleDefaultOpt -> | HandleExceptions -> [array (option any)] @-> option any
[array (option any); [ut] @-> bt; [ut] @-> option any] @-> option any
| ToClosureEnv -> [any] @-> cet | ToClosureEnv -> [any] @-> cet
| FromClosureEnv -> [cet] @-> any | FromClosureEnv -> [cet] @-> any
in in
@ -347,7 +345,10 @@ let polymorphic_op_return_type
| Log (PosRecordIfTrueBool, _), _ -> uf (TLit TBool) | Log (PosRecordIfTrueBool, _), _ -> uf (TLit TBool)
| Log _, [tau] -> tau | Log _, [tau] -> tau
| Length, _ -> uf (TLit TInt) | Length, _ -> uf (TLit TInt)
| HandleDefaultOpt, [_; _; tf] -> return_type tf 1 | HandleExceptions, [tau] ->
let t_inner = any () in
unify ctx e tau (uf (TArray t_inner));
t_inner
| ToClosureEnv, _ -> uf TClosureEnv | ToClosureEnv, _ -> uf TClosureEnv
| FromClosureEnv, _ -> any () | FromClosureEnv, _ -> any ()
| _ -> Message.error ~pos "Mismatched operator arguments" | _ -> Message.error ~pos "Mismatched operator arguments"

View File

@ -716,11 +716,9 @@ module EventParser = struct
ctx.events ctx.events
end end
let handle_default_opt let handle_exceptions
(pos : source_position array) (pos : source_position array)
(exceptions : 'a Eoption.t array) (exceptions : 'a Eoption.t array) : 'a Eoption.t =
(just : unit -> bool)
(cons : unit -> 'a Eoption.t) : 'a Eoption.t =
let len = Array.length exceptions in let len = Array.length exceptions in
let rec filt_except i = let rec filt_except i =
if i < len then if i < len then
@ -730,7 +728,7 @@ let handle_default_opt
else [] else []
in in
match filt_except 0 with match filt_except 0 with
| [] -> if just () then cons () else Eoption.ENone () | [] -> Eoption.ENone ()
| [(res, _)] -> res | [(res, _)] -> res
| res -> error Conflict (List.map (fun (_, i) -> pos.(i)) res) | res -> error Conflict (List.map (fun (_, i) -> pos.(i)) res)

View File

@ -335,12 +335,8 @@ val duration_to_string : duration -> string
(**{1 Defaults} *) (**{1 Defaults} *)
val handle_default_opt : val handle_exceptions :
source_position array -> source_position array -> 'a Eoption.t array -> 'a Eoption.t
'a Eoption.t array ->
(unit -> bool) ->
(unit -> 'a Eoption.t) ->
'a Eoption.t
(** @raise Error Conflict *) (** @raise Error Conflict *)
(**{1 Operators} *) (**{1 Operators} *)

View File

@ -383,9 +383,9 @@ class NoValue(CatalaError):
source_position) source_position)
class Conflict(CatalaError): class Conflict(CatalaError):
def __init__(self, source_position: SourcePosition) -> None: def __init__(self, pos1: SourcePosition, pos2: SourcePosition) -> None:
super().__init__("two or more concurring valid computations", super().__init__("two or more concurring valid computations:\nAt {}".format(pos2),
source_position) pos1)
class DivisionByZero(CatalaError): class DivisionByZero(CatalaError):
def __init__(self, source_position: SourcePosition) -> None: def __init__(self, source_position: SourcePosition) -> None:
@ -606,28 +606,21 @@ def list_length(l: List[Alpha]) -> Integer:
# ======== # ========
def handle_default_opt( def handle_exceptions(
pos: SourcePosition, pos: List[SourcePosition],
exceptions: List[Optional[Any]], exceptions: List[Optional[Alpha]])
just: Callable[[Unit], bool], -> Optional[Alpha]:
cons: Callable[[Unit], Optional[Alpha]]
) -> Optional[Alpha]:
acc: Optional[Alpha] = None acc: Optional[Alpha] = None
for exception in exceptions: acc_pos: Optional[pos] = None
if acc is None: for exception, pos in zip(exceptions, pos):
acc = exception if exception is None:
elif not (acc is None) and exception is None:
pass # acc stays the same pass # acc stays the same
elif not (acc is None) and not (exception is None): elif acc is None:
raise Conflict(pos) acc = exception
if acc is None: acc_pos = pos
b = just(Unit()) else
if b: raise Conflict(acc_pos,pos)
return cons(Unit()) return acc
else:
return None
else:
return acc
def no_input() -> Callable[[Unit], Alpha]: def no_input() -> Callable[[Unit], Alpha]: