From 216bd87991f0fdf2a13d3372fc447614033e1c9a Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 21 Jan 2021 23:47:48 -0500 Subject: [PATCH] Improve unlabeled exceptions: Default definitions and unlabeled exceptions in the same scope can now be defined in different code blocks --- src/catala/catala_surface/desugaring.ml | 173 +++++---------- src/catala/catala_surface/name_resolution.ml | 204 +++++++++++++----- ...ambiguous_unlabeled_exception.catala.A.out | 10 +- .../missing_unlabeled_definition.catala.A.out | 8 +- .../one_ambiguous_exception.catala.A.out | 10 +- 5 files changed, 220 insertions(+), 185 deletions(-) diff --git a/src/catala/catala_surface/desugaring.ml b/src/catala/catala_surface/desugaring.ml index a2eaf0ca..d2c7c9bb 100644 --- a/src/catala/catala_surface/desugaring.ml +++ b/src/catala/catala_surface/desugaring.ml @@ -745,33 +745,15 @@ let process_default (ctxt : Name_resolution.context) (scope : Scopelang.Ast.Scop exception_to_rule; } -let get_def_key (def : Ast.definition) (scope_uid : Scopelang.Ast.ScopeName.t) - (ctxt : Name_resolution.context) : Desugared.Ast.ScopeDef.t = - let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in - match Pos.unmark def.definition_name with - | [ x ] -> - let x_uid = Name_resolution.get_var_uid scope_uid ctxt x in - Desugared.Ast.ScopeDef.Var x_uid - | [ y; x ] -> - let subscope_uid : Scopelang.Ast.SubScopeName.t = - Name_resolution.get_subscope_uid scope_uid ctxt y - in - let subscope_real_uid : Scopelang.Ast.ScopeName.t = - Scopelang.Ast.SubScopeMap.find subscope_uid scope_ctxt.sub_scopes - in - let x_uid = Name_resolution.get_var_uid subscope_real_uid ctxt x in - Desugared.Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid) - | _ -> - Errors.raise_spanned_error "Structs are not handled yet" - (Pos.get_position def.definition_expr) - (** Wrapper around {!val: process_default} that performs some name disambiguation *) let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option) (scope_uid : Scopelang.Ast.ScopeName.t) (ctxt : Name_resolution.context) (prgm : Desugared.Ast.program) (def : Ast.definition) : Desugared.Ast.program = let scope : Desugared.Ast.scope = Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes in let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in - let def_key = get_def_key def scope_uid ctxt in + let def_key = Name_resolution.get_def_key + (Pos.unmark def.definition_name) scope_uid ctxt (Pos.get_position def.definition_expr) + in (* We add to the name resolution context the name of the parameter variable *) let param_uid, new_ctxt = match def.definition_parameter with @@ -815,21 +797,19 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option) if is_exception def then rule_name else match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with - | None -> rule_name - | Some x -> x + | None | Some Name_resolution.Ambiguous -> rule_name + | Some (Name_resolution.Unique x) -> x in let parent_rule = match def.Ast.definition_exception_to with | NotAnException -> None | UnlabeledException -> Some - ( try - Pos.same_pos_as - (Desugared.Ast.ScopeDefMap.find def_key scope_ctxt.default_rulemap) - def.Ast.definition_name - with Not_found -> - Errors.raise_spanned_error "No definition associated to this exception" - (Pos.get_position def.Ast.definition_name) ) + ( match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with + (* This should have been caught previously by check_unlabeled_exception *) + | None | Some Name_resolution.Ambiguous -> assert false + | Some (Name_resolution.Unique name) -> Pos.same_pos_as name def.Ast.definition_name + ) | ExceptionToLabel label -> Some ( try @@ -918,82 +898,50 @@ let process_scope_use_item (precond : Ast.expression Pos.marked option) (** {1 Translating top-level items} *) -(* Collects the scope definition in the set if it is an unlabeled exception *) -let gather_unnamed_exceptions (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resolution.context) - (defset : Desugared.Ast.ScopeDefSet.t) (item : Ast.scope_use_item Pos.marked) : - Desugared.Ast.ScopeDefSet.t = +(* If this is an unlabeled exception, ensures that it has a unique default definition *) +let check_unlabeled_exception (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resolution.context) + (item : Ast.scope_use_item Pos.marked) : unit = + let scope_ctxt = Scopelang.Ast.ScopeMap.find scope ctxt.scopes in match Pos.unmark item with | Ast.Rule rule -> ( - match rule.Ast.rule_exception_to with - | UnlabeledException -> - let def = rule_to_def rule in - let scope_def = get_def_key def scope ctxt in - Desugared.Ast.ScopeDefSet.add scope_def defset - | _ -> defset ) + match rule.rule_exception_to with + | Ast.NotAnException | Ast.ExceptionToLabel _ -> () + (* If this is an unlabeled exception, we check that it has a unique default definition *) + | Ast.UnlabeledException -> + let def_key = Name_resolution.get_def_key + (Pos.unmark rule.rule_name) scope ctxt (Pos.get_position rule.rule_consequence) + in + match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with + | None -> + Errors.raise_spanned_error + "This exception does not have a corresponding definition" + (Pos.get_position item) + | Some Ambiguous -> + Errors.raise_spanned_error + "This exception can refer to several definitions. Try using labels to disambiguate" + (Pos.get_position item) + | Some (Unique _) -> () + ) | Ast.Definition def -> ( - match def.Ast.definition_exception_to with - | UnlabeledException -> - let scope_def = get_def_key def scope ctxt in - Desugared.Ast.ScopeDefSet.add scope_def defset - | _ -> defset ) - | _ -> defset - -let generate_default_rulenames (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resolution.context) - (defset : Desugared.Ast.ScopeDefSet.t) - (rulemap : Desugared.Ast.RuleName.t Desugared.Ast.ScopeDefMap.t) - (item : Ast.scope_use_item Pos.marked) : Desugared.Ast.RuleName.t Desugared.Ast.ScopeDefMap.t = - let is_exception (def : Ast.definition) = - match def.Ast.definition_exception_to with NotAnException -> false | _ -> true - in - match Pos.unmark item with - | Ast.Rule rule -> - let def = rule_to_def rule in - let scope_def = get_def_key def scope ctxt in - if Desugared.Ast.ScopeDefSet.mem scope_def defset && not (is_exception def) then - (* This is a non-exception definition corresponding to an unnamed exception *) - match def.Ast.definition_label with - | Some label -> - Errors.raise_spanned_error - "This definition has a label, but an unlabeled exception refers to it" - (Pos.get_position label) - | None -> ( - match Desugared.Ast.ScopeDefMap.find_opt scope_def rulemap with - | Some _ -> - (* There is already a default definition for this, we raise an error *) - Errors.raise_spanned_error - "An unlabeled exception refers to several definitions, including this one. \ - Disambiguate by using labels." - (Pos.get_position def.Ast.definition_name) - | None -> - let fresh_name = - Desugared.Ast.RuleName.fresh (Pos.same_pos_as "dummy" def.Ast.definition_name) - in - Desugared.Ast.ScopeDefMap.add scope_def fresh_name rulemap ) - else rulemap - | Ast.Definition def -> - let scope_def = get_def_key def scope ctxt in - if Desugared.Ast.ScopeDefSet.mem scope_def defset && not (is_exception def) then - (* This is a non-exception definition corresponding to an unnamed exception *) - match def.Ast.definition_label with - | Some label -> - Errors.raise_spanned_error - "This definition has a label, but an unlabeled exception refers to it" - (Pos.get_position label) - | None -> ( - match Desugared.Ast.ScopeDefMap.find_opt scope_def rulemap with - | Some _ -> - (* There is already a default definition for this, we raise an error *) - Errors.raise_spanned_error - "An unlabeled exception refers to several definitions, including this one. \ - Disambiguate by using labels." - (Pos.get_position def.Ast.definition_name) - | None -> - let fresh_name = - Desugared.Ast.RuleName.fresh (Pos.same_pos_as "dummy" def.Ast.definition_name) - in - Desugared.Ast.ScopeDefMap.add scope_def fresh_name rulemap ) - else rulemap - | _ -> rulemap + match def.definition_exception_to with + | Ast.NotAnException | Ast.ExceptionToLabel _ -> () + (* If this is an unlabeled exception, we check that it has a unique default definition *) + | Ast.UnlabeledException -> + let def_key = Name_resolution.get_def_key + (Pos.unmark def.definition_name) scope ctxt (Pos.get_position def.definition_expr) + in + match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with + | None -> + Errors.raise_spanned_error + "This exception does not have a corresponding definition" + (Pos.get_position item) + | Some Ambiguous -> + Errors.raise_spanned_error + "This exception can refer to several definitions. Try using labels to disambiguate" + (Pos.get_position item) + | Some (Unique _) -> () + ) + | _ -> () (** Translates a surface scope use, which is a bunch of definitions *) let process_scope_use (ctxt : Name_resolution.context) (prgm : Desugared.Ast.program) @@ -1008,24 +956,7 @@ let process_scope_use (ctxt : Name_resolution.context) (prgm : Desugared.Ast.pro (* should not happen *) in let precond = use.scope_use_condition in - let defset = - List.fold_left - (gather_unnamed_exceptions scope_uid ctxt) - Desugared.Ast.ScopeDefSet.empty use.scope_use_items - in - let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in - let new_scope_ctxt = - { - scope_ctxt with - default_rulemap = - List.fold_left - (generate_default_rulenames scope_uid ctxt defset) - scope_ctxt.default_rulemap use.scope_use_items; - } - in - let ctxt = - { ctxt with scopes = Scopelang.Ast.ScopeMap.add scope_uid new_scope_ctxt ctxt.scopes } - in + List.iter (check_unlabeled_exception scope_uid ctxt) use.scope_use_items; List.fold_left (process_scope_use_item precond scope_uid ctxt) prgm use.scope_use_items (** Main function of this module *) diff --git a/src/catala/catala_surface/name_resolution.ml b/src/catala/catala_surface/name_resolution.ml index 14889dcc..33cdde2b 100644 --- a/src/catala/catala_surface/name_resolution.ml +++ b/src/catala/catala_surface/name_resolution.ml @@ -23,10 +23,14 @@ type ident = string type typ = Scopelang.Ast.typ +type unique_rulename = + | Ambiguous + | Unique of Desugared.Ast.RuleName.t + type scope_context = { var_idmap : Scopelang.Ast.ScopeVar.t Desugared.Ast.IdentMap.t; (** Scope variables *) label_idmap : Desugared.Ast.RuleName.t Desugared.Ast.IdentMap.t; - default_rulemap : Desugared.Ast.RuleName.t Desugared.Ast.ScopeDefMap.t; + default_rulemap : unique_rulename Desugared.Ast.ScopeDefMap.t; (** What is the default rule to refer to for unnamed exceptions, if any *) sub_scopes_idmap : Scopelang.Ast.SubScopeName.t Desugared.Ast.IdentMap.t; (** Sub-scopes variables *) @@ -421,67 +425,151 @@ let process_program_item (ctxt : context) (item : Ast.program_item) (** {1 Scope uses pass} *) -let process_rule (ctxt : context) (s_name : Scopelang.Ast.ScopeName.t) (r : Ast.rule) : context = - match r.Ast.rule_label with - | None -> ctxt - | Some label -> - let rule_name = - Desugared.Ast.RuleName.fresh - ( match r.rule_label with - | None -> - Pos.map_under_mark - (fun qident -> String.concat "." (List.map (fun i -> Pos.unmark i) qident)) - r.rule_name - | Some label -> label ) +let get_def_key (name : Ast.qident) (scope_uid : Scopelang.Ast.ScopeName.t) + (ctxt : context) (default_pos : Pos.t) : Desugared.Ast.ScopeDef.t = + let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in + match name with + | [ x ] -> + let x_uid = get_var_uid scope_uid ctxt x in + Desugared.Ast.ScopeDef.Var x_uid + | [ y; x ] -> + let subscope_uid : Scopelang.Ast.SubScopeName.t = + get_subscope_uid scope_uid ctxt y in - { - ctxt with - scopes = - Scopelang.Ast.ScopeMap.update s_name - (fun s_ctxt -> - match s_ctxt with - | None -> assert false (* should not happen *) - | Some s_ctxt -> - Some - { - s_ctxt with - label_idmap = - Desugared.Ast.IdentMap.add (Pos.unmark label) rule_name s_ctxt.label_idmap; - }) - ctxt.scopes; - } + let subscope_real_uid : Scopelang.Ast.ScopeName.t = + Scopelang.Ast.SubScopeMap.find subscope_uid scope_ctxt.sub_scopes + in + let x_uid = get_var_uid subscope_real_uid ctxt x in + Desugared.Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid) + | _ -> + Errors.raise_spanned_error "Structs are not handled yet" + default_pos + + + +let process_rule (ctxt : context) (s_name : Scopelang.Ast.ScopeName.t) (r : Ast.rule) : context = + (* Process the label map first *) + let ctxt = + match r.Ast.rule_label with + | None -> ctxt + | Some label -> + let rule_name = + Desugared.Ast.RuleName.fresh + ( match r.rule_label with + | None -> + Pos.map_under_mark + (fun qident -> String.concat "." (List.map (fun i -> Pos.unmark i) qident)) + r.rule_name + | Some label -> label ) + in + { + ctxt with + scopes = + Scopelang.Ast.ScopeMap.update s_name + (fun s_ctxt -> + match s_ctxt with + | None -> assert false (* should not happen *) + | Some s_ctxt -> + Some + { + s_ctxt with + label_idmap = + Desugared.Ast.IdentMap.add (Pos.unmark label) rule_name s_ctxt.label_idmap; + }) + ctxt.scopes; + } + in + (* And update the map of default rulenames for unlabeled exceptions *) + match r.Ast.rule_exception_to with + (* If this definition is an exception, it cannot be a default definition *) + | UnlabeledException | ExceptionToLabel _ -> ctxt + (* If it is not an exception, we need to distinguish between several cases *) + | NotAnException -> + let def_key = get_def_key + (Pos.unmark r.rule_name) s_name ctxt (Pos.get_position r.rule_consequence) + in + let scope_ctxt = Scopelang.Ast.ScopeMap.find s_name ctxt.scopes in + let rulemap = + match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with + (* There was already a default definition for this key. If we need it, it is ambiguous *) + | Some _ -> Desugared.Ast.ScopeDefMap.add def_key Ambiguous scope_ctxt.default_rulemap + (* No definition has been set yet for this key *) + | None -> + match r.Ast.rule_label with + (* This default definition has a label. This is not allowed for unlabeled exceptions *) + | Some _ -> Desugared.Ast.ScopeDefMap.add def_key Ambiguous scope_ctxt.default_rulemap + (* This is a possible default definition for this key. + We create and store a fresh rulename *) + | None -> Desugared.Ast.ScopeDefMap.add def_key + (Unique (Desugared.Ast.RuleName.fresh (Pos.same_pos_as "default" r.rule_name))) + scope_ctxt.default_rulemap + in + let new_scope_ctxt = { scope_ctxt with default_rulemap = rulemap } in + { ctxt with scopes = Scopelang.Ast.ScopeMap.add s_name new_scope_ctxt ctxt.scopes } + let process_definition (ctxt : context) (s_name : Scopelang.Ast.ScopeName.t) (d : Ast.definition) : context = - match d.Ast.definition_label with - | None -> ctxt - | Some label -> - let definition_name = - Desugared.Ast.RuleName.fresh - ( match d.definition_label with - | None -> - Pos.map_under_mark - (fun qident -> String.concat "." (List.map (fun i -> Pos.unmark i) qident)) - d.definition_name - | Some label -> label ) - in - { - ctxt with - scopes = - Scopelang.Ast.ScopeMap.update s_name - (fun s_ctxt -> - match s_ctxt with - | None -> assert false (* should not happen *) - | Some s_ctxt -> - Some - { - s_ctxt with - label_idmap = - Desugared.Ast.IdentMap.add (Pos.unmark label) definition_name - s_ctxt.label_idmap; - }) - ctxt.scopes; - } + (* Process the label map first *) + let ctxt = + match d.Ast.definition_label with + | None -> ctxt + | Some label -> + let definition_name = + Desugared.Ast.RuleName.fresh + ( match d.definition_label with + | None -> + Pos.map_under_mark + (fun qident -> String.concat "." (List.map (fun i -> Pos.unmark i) qident)) + d.definition_name + | Some label -> label ) + in + { + ctxt with + scopes = + Scopelang.Ast.ScopeMap.update s_name + (fun s_ctxt -> + match s_ctxt with + | None -> assert false (* should not happen *) + | Some s_ctxt -> + Some + { + s_ctxt with + label_idmap = + Desugared.Ast.IdentMap.add (Pos.unmark label) definition_name + s_ctxt.label_idmap; + }) + ctxt.scopes; + } + in + (* And update the map of default rulenames for unlabeled exceptions *) + match d.Ast.definition_exception_to with + (* If this definition is an exception, it cannot be a default definition *) + | UnlabeledException | ExceptionToLabel _ -> ctxt + (* If it is not an exception, we need to distinguish between several cases *) + | NotAnException -> + let def_key = get_def_key + (Pos.unmark d.definition_name) s_name ctxt (Pos.get_position d.definition_expr) + in + let scope_ctxt = Scopelang.Ast.ScopeMap.find s_name ctxt.scopes in + let rulemap = + match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with + (* There was already a default definition for this key. If we need it, it is ambiguous *) + | Some _ -> Desugared.Ast.ScopeDefMap.add def_key Ambiguous scope_ctxt.default_rulemap + (* No definition has been set yet for this key *) + | None -> + match d.Ast.definition_label with + (* This default definition has a label. This is not allowed for unlabeled exceptions *) + | Some _ -> Desugared.Ast.ScopeDefMap.add def_key Ambiguous scope_ctxt.default_rulemap + (* This is a possible default definition for this key. + We create and store a fresh rulename *) + | None -> Desugared.Ast.ScopeDefMap.add def_key + (Unique (Desugared.Ast.RuleName.fresh (Pos.same_pos_as "default" d.definition_name))) + scope_ctxt.default_rulemap + in + let new_scope_ctxt = { scope_ctxt with default_rulemap = rulemap } in + { ctxt with scopes = Scopelang.Ast.ScopeMap.add s_name new_scope_ctxt ctxt.scopes } + let process_scope_use_item (s_name : Scopelang.Ast.ScopeName.t) (ctxt : context) (sitem : Ast.scope_use_item Pos.marked) : context = diff --git a/tests/test_exception/ambiguous_unlabeled_exception.catala.A.out b/tests/test_exception/ambiguous_unlabeled_exception.catala.A.out index 468f7f46..71f3741d 100644 --- a/tests/test_exception/ambiguous_unlabeled_exception.catala.A.out +++ b/tests/test_exception/ambiguous_unlabeled_exception.catala.A.out @@ -1,7 +1,13 @@ -[ERROR] An unlabeled exception refers to several definitions, including this one. Disambiguate by using labels. +[ERROR] This exception can refer to several definitions. Try using labels to disambiguate [ERROR] [ERROR] --> test_exception/ambiguous_unlabeled_exception.catala [ERROR] | [ERROR] 10 | def x := 1 -[ERROR] | ^ +[ERROR] | +[ERROR] 11 | +[ERROR] | +[ERROR] 12 | exception +[ERROR] | ^^^^^^^^^^ +[ERROR] 13 | def x := 2 +[ERROR] | ^^^^^^^^^^^ [ERROR] + Test diff --git a/tests/test_exception/missing_unlabeled_definition.catala.A.out b/tests/test_exception/missing_unlabeled_definition.catala.A.out index 8162e4e2..16bccf23 100644 --- a/tests/test_exception/missing_unlabeled_definition.catala.A.out +++ b/tests/test_exception/missing_unlabeled_definition.catala.A.out @@ -1,7 +1,11 @@ -[ERROR] No definition associated to this exception +[ERROR] This exception does not have a corresponding definition [ERROR] [ERROR] --> test_exception/missing_unlabeled_definition.catala [ERROR] | +[ERROR] 7 | scope A: +[ERROR] | +[ERROR] 8 | exception +[ERROR] | ^^^^^^^^^^ [ERROR] 9 | def x := 1 -[ERROR] | ^ +[ERROR] | ^^^^^^^^^^^ [ERROR] + Test diff --git a/tests/test_exception/one_ambiguous_exception.catala.A.out b/tests/test_exception/one_ambiguous_exception.catala.A.out index 41474a45..b136d6dd 100644 --- a/tests/test_exception/one_ambiguous_exception.catala.A.out +++ b/tests/test_exception/one_ambiguous_exception.catala.A.out @@ -1,7 +1,13 @@ -[ERROR] An unlabeled exception refers to several definitions, including this one. Disambiguate by using labels. +[ERROR] This exception can refer to several definitions. Try using labels to disambiguate [ERROR] [ERROR] --> test_exception/one_ambiguous_exception.catala [ERROR] | [ERROR] 16 | def y := 4 -[ERROR] | ^ +[ERROR] | +[ERROR] 17 | +[ERROR] | +[ERROR] 18 | exception +[ERROR] | ^^^^^^^^^ +[ERROR] 19 | def y := 3 +[ERROR] | ^^^^^^^^^^^ [ERROR] + Test