diff --git a/compiler/dcalc/ast.ml b/compiler/dcalc/ast.ml index 197fd431..3f2161b2 100644 --- a/compiler/dcalc/ast.ml +++ b/compiler/dcalc/ast.ml @@ -181,6 +181,14 @@ let make_let_in (x : Var.t) (tau : typ Pos.marked) (e1 : expr Pos.marked Bindlib (e2 : expr Pos.marked Bindlib.box) (pos : Pos.t) : expr Pos.marked Bindlib.box = make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos +let empty_thunked_term : expr Pos.marked = + let silent = Var.make ("_", Pos.no_pos) in + Bindlib.unbox + (make_abs + (Array.of_list [ silent ]) + (Bindlib.box (ELit LEmptyError, Pos.no_pos)) + Pos.no_pos [ (TLit TUnit, Pos.no_pos) ] Pos.no_pos) + let build_whole_scope_expr (ctx : decl_ctx) (body : scope_body) (pos_scope : Pos.t) = let body_expr = List.fold_right diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index faae0419..0cbdf867 100644 --- a/compiler/dcalc/ast.mli +++ b/compiler/dcalc/ast.mli @@ -206,6 +206,8 @@ val make_let_in : Pos.t -> expr Pos.marked Bindlib.box +val empty_thunked_term : expr Pos.marked + (** {1 AST manipulation helpers}*) val build_whole_scope_expr : decl_ctx -> scope_body -> Pos.t -> expr Pos.marked Bindlib.box diff --git a/compiler/dcalc/interpreter.ml b/compiler/dcalc/interpreter.ml index 4376c7c2..a3e2068b 100644 --- a/compiler/dcalc/interpreter.ml +++ b/compiler/dcalc/interpreter.ml @@ -22,16 +22,6 @@ module A = Ast let is_empty_error (e : A.expr Pos.marked) : bool = match Pos.unmark e with ELit LEmptyError -> true | _ -> false -let empty_thunked_term : Ast.expr Pos.marked = - let silent = Ast.Var.make ("_", Pos.no_pos) in - Bindlib.unbox - (Ast.make_abs - (Array.of_list [ silent ]) - (Bindlib.box (Ast.ELit Ast.LEmptyError, Pos.no_pos)) - Pos.no_pos - [ (Ast.TLit Ast.TUnit, Pos.no_pos) ] - Pos.no_pos) - let log_indent = ref 0 (** {1 Evaluation} *) @@ -439,7 +429,7 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) : (Uid.MarkedString.info * Ast.expr Pos.marked) list = match Pos.unmark (evaluate_expr ctx e) with | Ast.EAbs (_, [ (Ast.TTuple (taus, Some s_in), _) ]) -> ( - let application_term = List.map (fun _ -> empty_thunked_term) taus in + let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in let to_interpret = (Ast.EApp (e, [ (Ast.ETuple (application_term, Some s_in), Pos.no_pos) ]), Pos.no_pos) in diff --git a/compiler/dcalc/interpreter.mli b/compiler/dcalc/interpreter.mli index 3fc799e5..5434d548 100644 --- a/compiler/dcalc/interpreter.mli +++ b/compiler/dcalc/interpreter.mli @@ -16,8 +16,6 @@ open Utils -val empty_thunked_term : Ast.expr Pos.marked - val interpret_program : Ast.decl_ctx -> Ast.expr Pos.marked -> (Uid.MarkedString.info * Ast.expr Pos.marked) list (** Interpret a program. This function expects an expression typed as a function whose argument are diff --git a/compiler/dcalc/print.ml b/compiler/dcalc/print.ml index 18185eeb..b3fe690f 100644 --- a/compiler/dcalc/print.ml +++ b/compiler/dcalc/print.ml @@ -79,8 +79,8 @@ let rec format_typ (ctx : Ast.decl_ctx) (fmt : Format.formatter) (typ : typ Pos. (fun fmt t -> Format.fprintf fmt "%a" format_typ t)) ts | TTuple (args, Some s) -> - Format.fprintf fmt "%a [%a]" Ast.StructName.format_t s - (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ") format_typ) + Format.fprintf fmt "%a {%a}" Ast.StructName.format_t s + (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ;@ ") format_typ) args | TEnum (_, e) -> Format.fprintf fmt "%a" Ast.EnumName.format_t e | TArrow (t1, t2) -> diff --git a/compiler/desugared/ast.ml b/compiler/desugared/ast.ml index 863f632d..1442af75 100644 --- a/compiler/desugared/ast.ml +++ b/compiler/desugared/ast.ml @@ -118,6 +118,7 @@ type scope_def = { scope_def_rules : rule RuleMap.t; scope_def_typ : Scopelang.Ast.typ Pos.marked; scope_def_is_condition : bool; + scope_def_visibility : Scopelang.Ast.visibility; scope_def_label_groups : RuleSet.t LabelMap.t; } diff --git a/compiler/desugared/ast.mli b/compiler/desugared/ast.mli index 8e54da47..5ccdf2d4 100644 --- a/compiler/desugared/ast.mli +++ b/compiler/desugared/ast.mli @@ -79,6 +79,7 @@ type scope_def = { scope_def_rules : rule RuleMap.t; scope_def_typ : Scopelang.Ast.typ Pos.marked; scope_def_is_condition : bool; + scope_def_visibility : Scopelang.Ast.visibility; scope_def_label_groups : RuleSet.t LabelMap.t; } diff --git a/compiler/desugared/desugared_to_scope.ml b/compiler/desugared/desugared_to_scope.ml index 1438d85b..7c49b61c 100644 --- a/compiler/desugared/desugared_to_scope.ml +++ b/compiler/desugared/desugared_to_scope.ml @@ -124,13 +124,15 @@ let rec rule_tree_to_expr ~(toplevel : bool) (def_pos : Pos.t) (** Translates a definition inside a scope, the resulting expression should be an {!constructor: Dcalc.Ast.EDefault} *) let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) - (typ : Scopelang.Ast.typ Pos.marked) (is_cond : bool) : Scopelang.Ast.expr Pos.marked = + (typ : Scopelang.Ast.typ Pos.marked) ~(is_cond : bool) ~(is_subscope_var : bool) : + Scopelang.Ast.expr Pos.marked = (* Here, we have to transform this list of rules into a default tree. *) - let is_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.rule_parameter in - let all_rules_func = Ast.RuleMap.for_all is_func def in - let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_func n r)) def in - let is_def_func : Scopelang.Ast.typ Pos.marked option = - if all_rules_func && Ast.RuleMap.cardinal def > 0 then + let is_def_func = match Pos.unmark typ with Scopelang.Ast.TArrow (_, _) -> true | _ -> false in + let is_rule_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.rule_parameter in + let all_rules_func = Ast.RuleMap.for_all is_rule_func def in + let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_rule_func n r)) def in + let is_def_func_param_typ : Scopelang.Ast.typ Pos.marked option = + if is_def_func && all_rules_func then match Pos.unmark typ with | Scopelang.Ast.TArrow (t_param, _) -> Some t_param | _ -> @@ -139,7 +141,7 @@ let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) "The definitions of %a are function but its type, %a, is not a function type" Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ) (Pos.get_position typ) - else if all_rules_not_func then None + else if (not is_def_func) && all_rules_not_func then None else Errors.raise_multispanned_error "some definitions of the same variable are functions while others aren't" @@ -147,26 +149,43 @@ let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) (fun (_, r) -> ( Some "This definition is a function:", Pos.get_position (Bindlib.unbox r.Ast.rule_cons) )) - (Ast.RuleMap.bindings (Ast.RuleMap.filter is_func def)) + (Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def)) @ List.map (fun (_, r) -> ( Some "This definition is not a function:", Pos.get_position (Bindlib.unbox r.Ast.rule_cons) )) - (Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_func n r)) def))) + (Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def))) in let top_list = def_map_to_tree def_info def in let top_value = - (if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func + (if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func_param_typ in - Bindlib.unbox - (rule_tree_to_expr ~toplevel:true - (Ast.ScopeDef.get_position def_info) - (Option.map (fun _ -> Scopelang.Ast.Var.make ("param", Pos.no_pos)) is_def_func) - (match top_list with - | [] -> - (* In this case, there are no rules to define the expression *) - Leaf [ top_value ] - | _ -> Node (top_list, [ top_value ]))) + if + Ast.RuleMap.cardinal def = 0 && is_def_func && is_subscope_var + (* Here we have a special case for the empty definitions. Indeed, we could use the code for the + regular case below that would create a convoluted default always returning empty error, and + this would be correct. But it gets more complicated with functions. Indeed, if we create an + empty definition for a subscope argument whose type is a function, we get something like [fun + () -> (fun real_param -> < ... >)] that is passed as an argument to the subscope. The + sub-scope de-thunks but the de-thunking does not return empty error, signalling there is not + reentrant variable, because functions are values! So the subscope does not see that there is + not reentrant variable and does not pick its internal definition instead. See + [test/test_scope/subscope_function_arg_not_defined.catala_en] for a test case exercising that + subtlety. + + To avoid this complication we special case here and put an empty error whether the type of + the subscope argument is a function or not. *) + then (ELit LEmptyError, Pos.no_pos) + else + Bindlib.unbox + (rule_tree_to_expr ~toplevel:true + (Ast.ScopeDef.get_position def_info) + (Option.map (fun _ -> Scopelang.Ast.Var.make ("param", Pos.no_pos)) is_def_func_param_typ) + (match top_list with + | [] -> + (* In this case, there are no rules to define the expression *) + Leaf [ top_value ] + | _ -> Node (top_list, [ top_value ]))) (** Translates a scope *) let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl = @@ -183,7 +202,10 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl = let var_def = scope_def.scope_def_rules in let var_typ = scope_def.scope_def_typ in let is_cond = scope_def.scope_def_is_condition in - let expr_def = translate_def (Ast.ScopeDef.Var var) var_def var_typ is_cond in + let expr_def = + translate_def (Ast.ScopeDef.Var var) var_def var_typ ~is_cond + ~is_subscope_var:false + in [ Scopelang.Ast.Definition ( ( Scopelang.Ast.ScopeVar @@ -207,7 +229,9 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl = match def_key with | Ast.ScopeDef.Var _ -> assert false (* should not happen *) | Ast.ScopeDef.SubScopeVar (_, sub_scope_var) -> - let expr_def = translate_def def_key def def_typ is_cond in + let expr_def = + translate_def def_key def def_typ ~is_cond ~is_subscope_var:true + in let subscop_real_name = Scopelang.Ast.SubScopeMap.find sub_scope_index scope.scope_sub_scopes in diff --git a/compiler/scopelang/ast.ml b/compiler/scopelang/ast.ml index e936d44c..cee7619f 100644 --- a/compiler/scopelang/ast.ml +++ b/compiler/scopelang/ast.ml @@ -123,6 +123,8 @@ type rule = | Assertion of expr Pos.marked | Call of ScopeName.t * SubScopeName.t +type visibility = { visibility_output : bool; visibility_input : bool } + type scope_decl = { scope_decl_name : ScopeName.t; scope_sig : typ Pos.marked ScopeVarMap.t; diff --git a/compiler/scopelang/ast.mli b/compiler/scopelang/ast.mli index ebd8a17d..5bb5b532 100644 --- a/compiler/scopelang/ast.mli +++ b/compiler/scopelang/ast.mli @@ -89,6 +89,11 @@ type rule = | Assertion of expr Pos.marked | Call of ScopeName.t * SubScopeName.t +type visibility = { + visibility_output : bool; (** True if present in the scope's output *) + visibility_input : bool; (** True if present in the scope's input (reentrant) *) +} + type scope_decl = { scope_decl_name : ScopeName.t; scope_sig : typ Pos.marked ScopeVarMap.t; diff --git a/compiler/scopelang/scope_to_dcalc.ml b/compiler/scopelang/scope_to_dcalc.ml index f8acbc32..8e7240e0 100644 --- a/compiler/scopelang/scope_to_dcalc.ml +++ b/compiler/scopelang/scope_to_dcalc.ml @@ -378,7 +378,10 @@ let translate_rule (ctx : ctx) (rule : Ast.rule) List.map (fun (subvar, _) -> if subscope_var_not_yet_defined subvar then - Bindlib.box Dcalc.Interpreter.empty_thunked_term + (* This is a redundant check. Normally, all subscope varaibles should have been + defined (even an empty definition, if they're not defined by any rule in the source + code) by the translation from desugared to the scope language. *) + Bindlib.box Dcalc.Ast.empty_thunked_term else let a_var, _ = Ast.ScopeVarMap.find subvar subscope_vars_defined in Dcalc.Ast.make_var (a_var, pos_call)) diff --git a/compiler/surface/desugaring.ml b/compiler/surface/desugaring.ml index a423006c..f3fe19db 100644 --- a/compiler/surface/desugaring.ml +++ b/compiler/surface/desugaring.ml @@ -927,17 +927,7 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option) (Some (Pos.same_pos_as param_var param), ctxt) in let scope_updated = - let scope_def = - { - Desugared.Ast.scope_def_rules = - (match Desugared.Ast.ScopeDefMap.find_opt def_key scope.scope_defs with - | Some def -> def.scope_def_rules - | None -> Desugared.Ast.RuleMap.empty); - scope_def_typ = Name_resolution.get_def_typ ctxt def_key; - scope_def_is_condition = Name_resolution.is_def_cond ctxt def_key; - scope_def_label_groups = Name_resolution.label_groups ctxt scope_uid def_key; - } - in + let scope_def = Desugared.Ast.ScopeDefMap.find def_key scope.scope_defs in let rule_name = def.definition_id in let parent_rules = match def.Ast.definition_exception_to with @@ -945,7 +935,7 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option) | UnlabeledException -> ( match scope_def_ctxt.default_exception_rulename with (* This should have been caught previously by check_unlabeled_exception *) - | None | Some (Name_resolution.Ambiguous _) -> assert false + | None | Some (Name_resolution.Ambiguous _) -> assert false (* should not happen *) | Some (Name_resolution.Unique (name, pos)) -> (Desugared.Ast.RuleSet.singleton name, pos) ) | ExceptionToLabel label -> ( @@ -1099,18 +1089,57 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) : Desu s_context.Name_resolution.var_idmap Scopelang.Ast.ScopeVarSet.empty; Desugared.Ast.scope_sub_scopes = s_context.Name_resolution.sub_scopes; Desugared.Ast.scope_defs = - Desugared.Ast.IdentMap.fold - (fun _ v acc -> - let x, y = Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs in - Desugared.Ast.ScopeDefMap.add (Desugared.Ast.ScopeDef.Var v) - { - Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty; - Desugared.Ast.scope_def_typ = x; - Desugared.Ast.scope_def_label_groups = Desugared.Ast.LabelMap.empty; - Desugared.Ast.scope_def_is_condition = y; - } - acc) - s_context.Name_resolution.var_idmap Desugared.Ast.ScopeDefMap.empty; + (* Initializing the definitions of all scopes and subscope vars, with no rules yet + inside *) + (let scope_vars_defs = + Desugared.Ast.IdentMap.fold + (fun _ v acc -> + let x, y = Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs in + let def_key = Desugared.Ast.ScopeDef.Var v in + Desugared.Ast.ScopeDefMap.add def_key + { + Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty; + Desugared.Ast.scope_def_typ = x; + Desugared.Ast.scope_def_label_groups = + Name_resolution.label_groups ctxt s_uid def_key; + Desugared.Ast.scope_def_is_condition = y; + Desugared.Ast.scope_def_visibility = + { + Scopelang.Ast.visibility_input = true; + Scopelang.Ast.visibility_output = true; + }; + } + acc) + s_context.Name_resolution.var_idmap Desugared.Ast.ScopeDefMap.empty + in + let scope_and_subscope_vars_defs = + Scopelang.Ast.SubScopeMap.fold + (fun subscope_name subscope_uid acc -> + Desugared.Ast.IdentMap.fold + (fun _ v acc -> + let x, y = + Scopelang.Ast.ScopeVarMap.find v ctxt.Name_resolution.var_typs + in + let def_key = Desugared.Ast.ScopeDef.SubScopeVar (subscope_name, v) in + Desugared.Ast.ScopeDefMap.add def_key + { + Desugared.Ast.scope_def_rules = Desugared.Ast.RuleMap.empty; + Desugared.Ast.scope_def_typ = x; + Desugared.Ast.scope_def_label_groups = + Name_resolution.label_groups ctxt subscope_uid def_key; + Desugared.Ast.scope_def_is_condition = y; + Desugared.Ast.scope_def_visibility = + { + Scopelang.Ast.visibility_input = true; + Scopelang.Ast.visibility_output = true; + }; + } + acc) + (Scopelang.Ast.ScopeMap.find subscope_uid ctxt.Name_resolution.scopes) + .Name_resolution.var_idmap acc) + s_context.sub_scopes scope_vars_defs + in + scope_and_subscope_vars_defs); Desugared.Ast.scope_assertions = []; Desugared.Ast.scope_meta_assertions = []; Desugared.Ast.scope_uid = s_uid; diff --git a/compiler/surface/name_resolution.ml b/compiler/surface/name_resolution.ml index 162893d5..8a52279e 100644 --- a/compiler/surface/name_resolution.ml +++ b/compiler/surface/name_resolution.ml @@ -143,9 +143,11 @@ let is_def_cond (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : bool = let label_groups (ctxt : context) (s_uid : Scopelang.Ast.ScopeName.t) (def : Desugared.Ast.ScopeDef.t) : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t = - (Desugared.Ast.ScopeDefMap.find def - (Scopelang.Ast.ScopeMap.find s_uid ctxt.scopes).scope_defs_contexts) - .label_groups + try + (Desugared.Ast.ScopeDefMap.find def + (Scopelang.Ast.ScopeMap.find s_uid ctxt.scopes).scope_defs_contexts) + .label_groups + with Not_found -> Desugared.Ast.LabelMap.empty (** {1 Declarations pass} *) diff --git a/tests/test_bool/good/output/test_bool.catala_en.Dcalc b/tests/test_bool/good/output/test_bool.catala_en.Dcalc index 6174f9e6..1837a25b 100644 --- a/tests/test_bool/good/output/test_bool.catala_en.Dcalc +++ b/tests/test_bool/good/output/test_bool.catala_en.Dcalc @@ -1,8 +1,8 @@ let TestBool_6 : - TestBool_in [unit → bool | unit → integer] → TestBool_out [bool | - integer] = - λ (TestBool_in_7: TestBool_in [unit → bool | unit → integer]) → + TestBool_in {unit → bool ; unit → integer} → TestBool_out {bool ; + integer} = + λ (TestBool_in_7: TestBool_in {unit → bool ; unit → integer}) → let foo_8 : unit → bool = TestBool_in_7."foo_in" in let bar_9 : unit → integer = TestBool_in_7."bar_in" diff --git a/tests/test_proof/bad/output/prolala_motivating_example.catala_en.Proof b/tests/test_proof/bad/output/prolala_motivating_example.catala_en.Proof index 2f49fc62..d671227f 100644 --- a/tests/test_proof/bad/output/prolala_motivating_example.catala_en.Proof +++ b/tests/test_proof/bad/output/prolala_motivating_example.catala_en.Proof @@ -10,6 +10,8 @@ The solver generated the following counterexample to explain the faulty behavior [RESULT] [Amount.amount] No two exceptions to ever overlap for this variable [RESULT] [Amount.correct_amount] This variable never returns an empty error [RESULT] [Amount.correct_amount] No two exceptions to ever overlap for this variable +[RESULT] [Amount.eligibility.is_eligible_correct] No two exceptions to ever overlap for this variable +[RESULT] [Amount.eligibility.is_eligible] No two exceptions to ever overlap for this variable [RESULT] [Amount.eligibility.is_professor] No two exceptions to ever overlap for this variable [RESULT] [Amount.eligibility.is_student] No two exceptions to ever overlap for this variable [RESULT] [Amount.number_of_advisors] This variable never returns an empty error diff --git a/tests/test_scope/good/output/subscope_function_arg_not_defined.catala_en.Caller.Interpret b/tests/test_scope/good/output/subscope_function_arg_not_defined.catala_en.Caller.Interpret new file mode 100644 index 00000000..3460fe38 --- /dev/null +++ b/tests/test_scope/good/output/subscope_function_arg_not_defined.catala_en.Caller.Interpret @@ -0,0 +1,2 @@ +[RESULT] Computation successful! Results: +[RESULT] y = 1 diff --git a/tests/test_scope/good/subscope_function_arg_not_defined.catala_en b/tests/test_scope/good/subscope_function_arg_not_defined.catala_en new file mode 100644 index 00000000..41e49985 --- /dev/null +++ b/tests/test_scope/good/subscope_function_arg_not_defined.catala_en @@ -0,0 +1,18 @@ +## Article + +```catala +declaration scope Callee: + context input content integer depends on boolean + context output content integer + +declaration scope Caller: + context sub scope Callee + context y content integer + +scope Callee: + definition input of b equals if b then 0 else 1 + definition output equals input of true + 1 + +scope Caller: + definition y equals sub.output +``` \ No newline at end of file