Improve unlabeled exceptions: Default definitions and unlabeled exceptions in the same scope can now be defined in different code blocks

This commit is contained in:
Aymeric Fromherz 2021-01-21 23:47:48 -05:00
parent 492683a000
commit 216bd87991
5 changed files with 220 additions and 185 deletions

View File

@ -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 *)

View File

@ -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 =

View File

@ -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

View File

@ -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

View File

@ -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