mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Cleaned code for generating exception graph, now correct and fully general
Missing some encoding optimizations
This commit is contained in:
parent
85cb2d5c8d
commit
3895743f20
@ -270,12 +270,20 @@ end
|
||||
|
||||
type vars = expr Bindlib.mvar
|
||||
|
||||
type exception_situation =
|
||||
| BaseCase
|
||||
| ExceptionToLabel of LabelName.t Marked.pos
|
||||
| ExceptionToRule of RuleName.t Marked.pos
|
||||
|
||||
type label_situation = ExplicitlyLabeled of LabelName.t Marked.pos | Unlabeled
|
||||
|
||||
type rule = {
|
||||
rule_id : RuleName.t;
|
||||
rule_just : expr Marked.pos Bindlib.box;
|
||||
rule_cons : expr Marked.pos Bindlib.box;
|
||||
rule_parameter : (Var.t * Scopelang.Ast.typ Marked.pos) option;
|
||||
rule_exception_to_rules : RuleSet.t Marked.pos;
|
||||
rule_exception : exception_situation;
|
||||
rule_label : label_situation;
|
||||
}
|
||||
|
||||
module Rule = struct
|
||||
@ -323,8 +331,9 @@ let empty_rule
|
||||
(match have_parameter with
|
||||
| Some typ -> Some (Var.make "dummy", typ)
|
||||
| None -> None);
|
||||
rule_exception_to_rules = RuleSet.empty, pos;
|
||||
rule_exception = BaseCase;
|
||||
rule_id = RuleName.fresh ("empty", pos);
|
||||
rule_label = Unlabeled;
|
||||
}
|
||||
|
||||
let always_false_rule
|
||||
@ -337,8 +346,9 @@ let always_false_rule
|
||||
(match have_parameter with
|
||||
| Some typ -> Some (Var.make "dummy", typ)
|
||||
| None -> None);
|
||||
rule_exception_to_rules = RuleSet.empty, pos;
|
||||
rule_exception = BaseCase;
|
||||
rule_id = RuleName.fresh ("always_false", pos);
|
||||
rule_label = Unlabeled;
|
||||
}
|
||||
|
||||
type assertion = expr Marked.pos Bindlib.box
|
||||
@ -354,7 +364,6 @@ type scope_def = {
|
||||
scope_def_typ : Scopelang.Ast.typ Marked.pos;
|
||||
scope_def_is_condition : bool;
|
||||
scope_def_io : Scopelang.Ast.io;
|
||||
scope_def_label_groups : RuleSet.t LabelMap.t;
|
||||
}
|
||||
|
||||
type var_or_states = WholeVar | States of StateName.t list
|
||||
|
@ -126,12 +126,20 @@ val make_let_in :
|
||||
|
||||
(** {2 Rules and scopes}*)
|
||||
|
||||
type exception_situation =
|
||||
| BaseCase
|
||||
| ExceptionToLabel of LabelName.t Marked.pos
|
||||
| ExceptionToRule of RuleName.t Marked.pos
|
||||
|
||||
type label_situation = ExplicitlyLabeled of LabelName.t Marked.pos | Unlabeled
|
||||
|
||||
type rule = {
|
||||
rule_id : RuleName.t;
|
||||
rule_just : expr Marked.pos Bindlib.box;
|
||||
rule_cons : expr Marked.pos Bindlib.box;
|
||||
rule_parameter : (Var.t * Scopelang.Ast.typ Marked.pos) option;
|
||||
rule_exception_to_rules : RuleSet.t Marked.pos;
|
||||
rule_exception : exception_situation;
|
||||
rule_label : label_situation;
|
||||
}
|
||||
|
||||
module Rule : Set.OrderedType with type t = rule
|
||||
@ -152,7 +160,6 @@ type scope_def = {
|
||||
scope_def_typ : Scopelang.Ast.typ Marked.pos;
|
||||
scope_def_is_condition : bool;
|
||||
scope_def_io : Scopelang.Ast.io;
|
||||
scope_def_label_groups : RuleSet.t LabelMap.t;
|
||||
}
|
||||
|
||||
type var_or_states = WholeVar | States of StateName.t list
|
||||
|
@ -240,8 +240,17 @@ module ExceptionVertex = struct
|
||||
let equal x y = compare x y = 0
|
||||
end
|
||||
|
||||
module EdgeExceptions = struct
|
||||
type t = Pos.t list
|
||||
|
||||
let compare = compare
|
||||
let default = [Pos.no_pos]
|
||||
end
|
||||
|
||||
module ExceptionsDependencies =
|
||||
Graph.Persistent.Digraph.ConcreteBidirectionalLabeled (ExceptionVertex) (Edge)
|
||||
Graph.Persistent.Digraph.ConcreteBidirectionalLabeled
|
||||
(ExceptionVertex)
|
||||
(EdgeExceptions)
|
||||
(** Module of the graph, provided by OCamlGraph. [x -> y] if [y] is an exception
|
||||
to [x] *)
|
||||
|
||||
@ -250,102 +259,190 @@ module ExceptionsSCC = Graph.Components.Make (ExceptionsDependencies)
|
||||
|
||||
(** {2 Graph computations} *)
|
||||
|
||||
type exception_edge = {
|
||||
label_from : Ast.LabelName.t;
|
||||
label_to : Ast.LabelName.t;
|
||||
edge_positions : Pos.t list;
|
||||
}
|
||||
|
||||
let build_exceptions_graph
|
||||
(def : Ast.rule Ast.RuleMap.t)
|
||||
(def_info : Ast.ScopeDef.t) : ExceptionsDependencies.t =
|
||||
(* First we partition the definitions into groups bearing the same label. *)
|
||||
let rule_sets : Ast.RuleSet.t Ast.LabelMap.t =
|
||||
(* First we partition the definitions into groups bearing the same label. To
|
||||
handle the rules that were not labeled by the user, we create implicit
|
||||
labels. *)
|
||||
|
||||
(* All the rules of the form [definition x ...] are base case with no explicit
|
||||
label, so they should share this implicit label. *)
|
||||
let base_case_implicit_label =
|
||||
Ast.LabelName.fresh ("base_case", Pos.no_pos)
|
||||
in
|
||||
(* When declaring [exception definition x ...], it means there is a unique
|
||||
rule [R] to which this can be an exception to. So we give a unique label to
|
||||
all the rules that are implicitly exceptions to rule [R]. *)
|
||||
let exception_to_rule_implicit_labels : Ast.LabelName.t Ast.RuleMap.t =
|
||||
Ast.RuleMap.fold
|
||||
(fun rule_name _rule rule_sets -> assert false)
|
||||
(fun _ rule_from exception_to_rule_implicit_labels ->
|
||||
match rule_from.Ast.rule_exception with
|
||||
| Ast.ExceptionToRule (rule_to, _) -> (
|
||||
match
|
||||
Ast.RuleMap.find_opt rule_to exception_to_rule_implicit_labels
|
||||
with
|
||||
| Some _ ->
|
||||
(* we already created the label *) exception_to_rule_implicit_labels
|
||||
| None ->
|
||||
Ast.RuleMap.add rule_to
|
||||
(Ast.LabelName.fresh
|
||||
( "exception_to_"
|
||||
^ Marked.unmark (Ast.RuleName.get_info rule_to),
|
||||
Pos.no_pos ))
|
||||
exception_to_rule_implicit_labels)
|
||||
| _ -> exception_to_rule_implicit_labels)
|
||||
def Ast.RuleMap.empty
|
||||
in
|
||||
(* When declaring [exception foo_l definition x ...], the rule is exception to
|
||||
all the rules sharing label [foo_l]. So we give a unique label to all the
|
||||
rules that are implicitly exceptions to rule [foo_l]. *)
|
||||
let exception_to_label_implicit_labels : Ast.LabelName.t Ast.LabelMap.t =
|
||||
Ast.RuleMap.fold
|
||||
(fun _ rule_from
|
||||
(exception_to_label_implicit_labels : Ast.LabelName.t Ast.LabelMap.t) ->
|
||||
match rule_from.Ast.rule_exception with
|
||||
| Ast.ExceptionToLabel (label_to, _) -> (
|
||||
match
|
||||
Ast.LabelMap.find_opt label_to exception_to_label_implicit_labels
|
||||
with
|
||||
| Some _ ->
|
||||
(* we already created the label *)
|
||||
exception_to_label_implicit_labels
|
||||
| None ->
|
||||
Ast.LabelMap.add label_to
|
||||
(Ast.LabelName.fresh
|
||||
( "exception_to_"
|
||||
^ Marked.unmark (Ast.LabelName.get_info label_to),
|
||||
Pos.no_pos ))
|
||||
exception_to_label_implicit_labels)
|
||||
| _ -> exception_to_label_implicit_labels)
|
||||
def Ast.LabelMap.empty
|
||||
in
|
||||
|
||||
(* first we collect all the rule sets referred by exceptions *)
|
||||
let all_rule_sets_pointed_to_by_exceptions : Ast.RuleSet.t list =
|
||||
(* Now we have all the labels necessary to partition our rules into sets, each
|
||||
one corresponding to a label relating to the structure of the exception
|
||||
DAG. *)
|
||||
let label_to_rule_sets =
|
||||
Ast.RuleMap.fold
|
||||
(fun _rule_name rule acc ->
|
||||
if Ast.RuleSet.is_empty (Marked.unmark rule.Ast.rule_exception_to_rules)
|
||||
then acc
|
||||
else Marked.unmark rule.Ast.rule_exception_to_rules :: acc)
|
||||
(fun rule_name rule rule_sets ->
|
||||
let label_of_rule =
|
||||
match rule.Ast.rule_label with
|
||||
| Ast.ExplicitlyLabeled (l, _) -> l
|
||||
| Ast.Unlabeled -> (
|
||||
match rule.Ast.rule_exception with
|
||||
| BaseCase -> base_case_implicit_label
|
||||
| ExceptionToRule (r, _) ->
|
||||
Ast.RuleMap.find r exception_to_rule_implicit_labels
|
||||
| ExceptionToLabel (l', _) ->
|
||||
Ast.LabelMap.find l' exception_to_label_implicit_labels)
|
||||
in
|
||||
Ast.LabelMap.update label_of_rule
|
||||
(fun rule_set ->
|
||||
match rule_set with
|
||||
| None -> Some (Ast.RuleSet.singleton rule_name)
|
||||
| Some rule_set -> Some (Ast.RuleSet.add rule_name rule_set))
|
||||
rule_sets)
|
||||
def Ast.LabelMap.empty
|
||||
in
|
||||
let find_label_of_rule (r : Ast.RuleName.t) : Ast.LabelName.t =
|
||||
fst
|
||||
(Ast.LabelMap.choose
|
||||
(Ast.LabelMap.filter
|
||||
(fun _ rule_set -> Ast.RuleSet.mem r rule_set)
|
||||
label_to_rule_sets))
|
||||
in
|
||||
(* Next, we collect the exception edges between those groups of rules referred
|
||||
by their labels. This is also at this step that we check consistency of the
|
||||
edges as they are declared at each rule but should be the same for all the
|
||||
rules of the same group. *)
|
||||
let exception_edges : exception_edge list =
|
||||
Ast.RuleMap.fold
|
||||
(fun rule_name rule exception_edges ->
|
||||
let label_from = find_label_of_rule rule_name in
|
||||
let label_to_and_pos =
|
||||
match rule.Ast.rule_exception with
|
||||
| Ast.BaseCase -> None
|
||||
| Ast.ExceptionToRule (r', pos) -> Some (find_label_of_rule r', pos)
|
||||
| Ast.ExceptionToLabel (l', pos) -> Some (l', pos)
|
||||
in
|
||||
match label_to_and_pos with
|
||||
| None -> exception_edges
|
||||
| Some (label_to, edge_pos) -> (
|
||||
let other_edges_originating_from_same_label =
|
||||
List.filter
|
||||
(fun edge -> Ast.LabelName.compare edge.label_from label_from = 0)
|
||||
exception_edges
|
||||
in
|
||||
(* We check the consistency*)
|
||||
if Ast.LabelName.compare label_from label_to = 0 then
|
||||
Errors.raise_spanned_error edge_pos
|
||||
"Cannot define rule as an exception to itself";
|
||||
List.iter
|
||||
(fun edge ->
|
||||
if Ast.LabelName.compare edge.label_to label_to <> 0 then
|
||||
Errors.raise_multispanned_error
|
||||
(( Some
|
||||
"This declaration contradicts another exception \
|
||||
declarations:",
|
||||
edge_pos )
|
||||
:: List.map
|
||||
(fun pos ->
|
||||
Some "Here is another exception declaration:", pos)
|
||||
edge.edge_positions)
|
||||
"The declaration of exceptions are inconsistent for variable \
|
||||
%a."
|
||||
Ast.ScopeDef.format_t def_info)
|
||||
other_edges_originating_from_same_label;
|
||||
(* Now we add the edge to the list*)
|
||||
let existing_edge =
|
||||
List.find_opt
|
||||
(fun edge ->
|
||||
Ast.LabelName.compare edge.label_from label_from = 0
|
||||
&& Ast.LabelName.compare edge.label_to label_to = 0)
|
||||
exception_edges
|
||||
in
|
||||
match existing_edge with
|
||||
| None ->
|
||||
{ label_from; label_to; edge_positions = [edge_pos] }
|
||||
:: exception_edges
|
||||
| Some existing_edge ->
|
||||
{
|
||||
label_from;
|
||||
label_to;
|
||||
edge_positions = edge_pos :: existing_edge.edge_positions;
|
||||
}
|
||||
:: List.filter (fun edge -> edge <> existing_edge) exception_edges))
|
||||
def []
|
||||
in
|
||||
(* we make sure these sets are either disjoint or equal ; should be a
|
||||
syntactic invariant since you currently can't assign two labels to a single
|
||||
rule but an extra check is valuable since this is a required invariant for
|
||||
the graph to be sound *)
|
||||
List.iter
|
||||
(fun rule_set1 ->
|
||||
List.iter
|
||||
(fun rule_set2 ->
|
||||
if Ast.RuleSet.equal rule_set1 rule_set2 then ()
|
||||
else if Ast.RuleSet.disjoint rule_set1 rule_set2 then ()
|
||||
else
|
||||
let spans =
|
||||
List.of_seq
|
||||
(Seq.map
|
||||
(fun rule ->
|
||||
( Some "Rule or definition from the first group:",
|
||||
Marked.get_mark (Ast.RuleName.get_info rule) ))
|
||||
(Ast.RuleSet.to_seq rule_set1))
|
||||
@ List.of_seq
|
||||
(Seq.map
|
||||
(fun rule ->
|
||||
( Some "Rule or definition from the second group:",
|
||||
Marked.get_mark (Ast.RuleName.get_info rule) ))
|
||||
(Ast.RuleSet.to_seq rule_set2))
|
||||
in
|
||||
Errors.raise_multispanned_error spans
|
||||
"Definitions or rules grouped by different labels overlap, \
|
||||
whereas these groups shoule be disjoint")
|
||||
all_rule_sets_pointed_to_by_exceptions)
|
||||
all_rule_sets_pointed_to_by_exceptions;
|
||||
(* Then we add the exception graph vertices by taking all those sets of rules
|
||||
pointed to by exceptions, and adding the remaining rules not pointed as
|
||||
separate singleton set vertices *)
|
||||
(* We've got the vertices and the edges, let's build the graph! *)
|
||||
let g =
|
||||
List.fold_left
|
||||
(fun g rule_set -> ExceptionsDependencies.add_vertex g rule_set)
|
||||
ExceptionsDependencies.empty all_rule_sets_pointed_to_by_exceptions
|
||||
in
|
||||
let g =
|
||||
Ast.RuleMap.fold
|
||||
(fun (rule_name : Ast.RuleName.t) _ g ->
|
||||
if
|
||||
List.exists
|
||||
(fun rule_set_pointed_to_by_exceptions ->
|
||||
Ast.RuleSet.mem rule_name rule_set_pointed_to_by_exceptions)
|
||||
all_rule_sets_pointed_to_by_exceptions
|
||||
then g
|
||||
else
|
||||
ExceptionsDependencies.add_vertex g (Ast.RuleSet.singleton rule_name))
|
||||
def g
|
||||
Ast.LabelMap.fold
|
||||
(fun _label rule_set g -> ExceptionsDependencies.add_vertex g rule_set)
|
||||
label_to_rule_sets ExceptionsDependencies.empty
|
||||
in
|
||||
(* then we add the edges *)
|
||||
let g =
|
||||
Ast.RuleMap.fold
|
||||
(fun rule_name rule g ->
|
||||
(* Right now, exceptions can only consist of one rule, we may want to
|
||||
relax that constraint later in the development of Catala. *)
|
||||
let exception_to_ruleset, pos = rule.Ast.rule_exception_to_rules in
|
||||
if Ast.RuleSet.is_empty exception_to_ruleset then g
|
||||
(* we don't add an edge*)
|
||||
else if ExceptionsDependencies.mem_vertex g exception_to_ruleset then
|
||||
if exception_to_ruleset = Ast.RuleSet.singleton rule_name then
|
||||
Errors.raise_spanned_error pos
|
||||
"Cannot define rule as an exception to itself"
|
||||
else
|
||||
let edge =
|
||||
ExceptionsDependencies.E.create
|
||||
(Ast.RuleSet.singleton rule_name)
|
||||
pos exception_to_ruleset
|
||||
in
|
||||
ExceptionsDependencies.add_edge_e g edge
|
||||
else
|
||||
Errors.raise_spanned_error pos
|
||||
"This rule has been declared as an exception to an incorrect \
|
||||
label: this label is not attached to a definition of \"%a\""
|
||||
Ast.ScopeDef.format_t def_info)
|
||||
def g
|
||||
List.fold_left
|
||||
(fun g edge ->
|
||||
let rule_group_from =
|
||||
Ast.LabelMap.find edge.label_from label_to_rule_sets
|
||||
in
|
||||
let rule_group_to =
|
||||
Ast.LabelMap.find edge.label_to label_to_rule_sets
|
||||
in
|
||||
let edge =
|
||||
ExceptionsDependencies.E.create rule_group_from edge.edge_positions
|
||||
rule_group_to
|
||||
in
|
||||
ExceptionsDependencies.add_edge_e g edge)
|
||||
g exception_edges
|
||||
in
|
||||
g
|
||||
|
||||
@ -377,7 +474,7 @@ let check_for_exception_cycle (g : ExceptionsDependencies.t) : unit =
|
||||
( Some
|
||||
("Used here in the definition of another cyclic exception \
|
||||
for defining \"" ^ var_str ^ "\":"),
|
||||
edge_pos );
|
||||
List.hd edge_pos );
|
||||
])
|
||||
scc)
|
||||
in
|
||||
|
@ -68,8 +68,10 @@ val build_scope_dependencies : Ast.scope -> ScopeDependencies.t
|
||||
|
||||
(** {1 Exceptions dependency graph} *)
|
||||
|
||||
module EdgeExceptions : Graph.Sig.ORDERED_TYPE_DFT with type t = Pos.t list
|
||||
|
||||
module ExceptionsDependencies :
|
||||
Graph.Sig.P with type V.t = Ast.RuleSet.t and type E.label = Edge.t
|
||||
Graph.Sig.P with type V.t = Ast.RuleSet.t and type E.label = EdgeExceptions.t
|
||||
|
||||
val build_exceptions_graph :
|
||||
Ast.rule Ast.RuleMap.t -> Ast.ScopeDef.t -> ExceptionsDependencies.t
|
||||
|
@ -151,8 +151,8 @@ type rule_tree =
|
||||
| Leaf of Ast.rule list
|
||||
(** Rules defining a base case piecewise. List is non-empty. *)
|
||||
| Node of rule_tree list * Ast.rule list
|
||||
(** A list of exceptions to a non-empty list of rules defining a base case
|
||||
piecewise. *)
|
||||
(** [Node (exceptions, base_case)] is a list of exceptions to a non-empty
|
||||
list of rules defining a base case piecewise. *)
|
||||
|
||||
(** Transforms a flat list of rules into a tree, taking into account the
|
||||
priorities declared between rules *)
|
||||
@ -160,17 +160,6 @@ let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) :
|
||||
rule_tree list =
|
||||
let exc_graph = Dependency.build_exceptions_graph def def_info in
|
||||
Dependency.check_for_exception_cycle exc_graph;
|
||||
Dependency.ExceptionsDependencies.iter_vertex
|
||||
(fun rule_group ->
|
||||
Cli.debug_format "Rule group: [%a]"
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt " ; ")
|
||||
(fun fmt rule ->
|
||||
Format.fprintf fmt "%d"
|
||||
(Pos.get_start_line
|
||||
(Pos.get_position (Ast.RuleName.get_info rule)))))
|
||||
(Ast.RuleSet.elements rule_group))
|
||||
exc_graph;
|
||||
(* we start by the base cases: they are the vertices which have no
|
||||
successors *)
|
||||
let base_cases =
|
||||
@ -181,7 +170,6 @@ let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) :
|
||||
else base_cases)
|
||||
exc_graph []
|
||||
in
|
||||
|
||||
let rec build_tree (base_cases : Ast.RuleSet.t) : rule_tree =
|
||||
let exceptions =
|
||||
Dependency.ExceptionsDependencies.pred exc_graph base_cases
|
||||
@ -260,7 +248,7 @@ let rec rule_tree_to_expr
|
||||
Scopelang.Ast.expr Marked.pos Bindlib.box list =
|
||||
List.map
|
||||
(fun e ->
|
||||
(* There are two levels of boxing here, the outermost is introduced by
|
||||
(* There are two levels of boxing her e, the outermost is introduced by
|
||||
the [translate_expr] function for which all of the bindings should
|
||||
have been closed by now, so we can safely unbox. *)
|
||||
Bindlib.unbox (Bindlib.box_apply (translate_expr ctx) e))
|
||||
|
@ -1053,7 +1053,8 @@ let process_default
|
||||
(rule_id : Desugared.Ast.RuleName.t)
|
||||
(param_uid : Desugared.Ast.Var.t Marked.pos option)
|
||||
(precond : Desugared.Ast.expr Marked.pos Bindlib.box option)
|
||||
(exception_to_rules : Desugared.Ast.RuleSet.t Marked.pos)
|
||||
(exception_situation : Desugared.Ast.exception_situation)
|
||||
(label_situation : Desugared.Ast.label_situation)
|
||||
(just : Ast.expression Marked.pos option)
|
||||
(cons : Ast.expression Marked.pos) : Desugared.Ast.rule =
|
||||
let just =
|
||||
@ -1082,8 +1083,9 @@ let process_default
|
||||
(Marked.get_mark (Bindlib.unbox cons))
|
||||
"This definition has a parameter but its type is not a function"
|
||||
| _ -> None);
|
||||
rule_exception_to_rules = exception_to_rules;
|
||||
rule_exception = exception_situation;
|
||||
rule_id;
|
||||
rule_label = label_situation;
|
||||
}
|
||||
|
||||
(** Wrapper around {!val: process_default} that performs some name
|
||||
@ -1120,30 +1122,37 @@ let process_def
|
||||
let scope_updated =
|
||||
let scope_def = Desugared.Ast.ScopeDefMap.find def_key scope.scope_defs in
|
||||
let rule_name = def.definition_id in
|
||||
let parent_rules =
|
||||
let label_situation =
|
||||
match def.definition_label with
|
||||
| Some (label_str, label_pos) ->
|
||||
Desugared.Ast.ExplicitlyLabeled
|
||||
( Desugared.Ast.IdentMap.find label_str scope_def_ctxt.label_idmap,
|
||||
label_pos )
|
||||
| None -> Desugared.Ast.Unlabeled
|
||||
in
|
||||
let exception_situation =
|
||||
match def.Ast.definition_exception_to with
|
||||
| NotAnException ->
|
||||
Desugared.Ast.RuleSet.empty, Marked.get_mark def.Ast.definition_name
|
||||
| NotAnException -> Desugared.Ast.BaseCase
|
||||
| UnlabeledException -> (
|
||||
match scope_def_ctxt.default_exception_rulename with
|
||||
(* This should have been caught previously by
|
||||
check_unlabeled_exception *)
|
||||
| None | Some (Name_resolution.Ambiguous _) ->
|
||||
(* This should have been caught previously by
|
||||
check_unlabeled_exception *)
|
||||
assert false (* should not happen *)
|
||||
| Some (Name_resolution.Unique (name, pos)) ->
|
||||
Desugared.Ast.RuleSet.singleton name, pos)
|
||||
| ExceptionToLabel label -> (
|
||||
Desugared.Ast.ExceptionToRule (name, pos))
|
||||
| ExceptionToLabel label_str -> (
|
||||
try
|
||||
let label_id =
|
||||
Desugared.Ast.IdentMap.find (Marked.unmark label)
|
||||
Desugared.Ast.IdentMap.find (Marked.unmark label_str)
|
||||
scope_def_ctxt.label_idmap
|
||||
in
|
||||
( Desugared.Ast.LabelMap.find label_id scope_def.scope_def_label_groups,
|
||||
Marked.get_mark def.Ast.definition_name )
|
||||
Desugared.Ast.ExceptionToLabel (label_id, Marked.get_mark label_str)
|
||||
with Not_found ->
|
||||
Errors.raise_spanned_error (Marked.get_mark label)
|
||||
Errors.raise_spanned_error
|
||||
(Marked.get_mark label_str)
|
||||
"Unknown label for the scope variable %a: \"%s\""
|
||||
Desugared.Ast.ScopeDef.format_t def_key (Marked.unmark label))
|
||||
Desugared.Ast.ScopeDef.format_t def_key (Marked.unmark label_str))
|
||||
in
|
||||
let scope_def =
|
||||
{
|
||||
@ -1152,8 +1161,8 @@ let process_def
|
||||
Desugared.Ast.RuleMap.add rule_name
|
||||
(process_default new_ctxt scope_uid
|
||||
(def_key, Marked.get_mark def.definition_name)
|
||||
rule_name param_uid precond parent_rules def.definition_condition
|
||||
def.definition_expr)
|
||||
rule_name param_uid precond exception_situation label_situation
|
||||
def.definition_condition def.definition_expr)
|
||||
scope_def.scope_def_rules;
|
||||
}
|
||||
in
|
||||
@ -1368,8 +1377,6 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
|
||||
Desugared.Ast.scope_def_rules =
|
||||
Desugared.Ast.RuleMap.empty;
|
||||
Desugared.Ast.scope_def_typ = v_sig.var_sig_typ;
|
||||
Desugared.Ast.scope_def_label_groups =
|
||||
Name_resolution.label_groups ctxt s_uid def_key;
|
||||
Desugared.Ast.scope_def_is_condition =
|
||||
v_sig.var_sig_is_condition;
|
||||
Desugared.Ast.scope_def_io =
|
||||
@ -1389,9 +1396,6 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
|
||||
Desugared.Ast.RuleMap.empty;
|
||||
Desugared.Ast.scope_def_typ =
|
||||
v_sig.var_sig_typ;
|
||||
Desugared.Ast.scope_def_label_groups =
|
||||
Name_resolution.label_groups ctxt s_uid
|
||||
def_key;
|
||||
Desugared.Ast.scope_def_is_condition =
|
||||
v_sig.var_sig_is_condition;
|
||||
Desugared.Ast.scope_def_io =
|
||||
@ -1447,9 +1451,6 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
|
||||
Desugared.Ast.scope_def_rules =
|
||||
Desugared.Ast.RuleMap.empty;
|
||||
Desugared.Ast.scope_def_typ = v_sig.var_sig_typ;
|
||||
Desugared.Ast.scope_def_label_groups =
|
||||
Name_resolution.label_groups ctxt subscope_uid
|
||||
def_key;
|
||||
Desugared.Ast.scope_def_is_condition =
|
||||
v_sig.var_sig_is_condition;
|
||||
Desugared.Ast.scope_def_io =
|
||||
|
@ -32,7 +32,6 @@ type unique_rulename =
|
||||
type scope_def_context = {
|
||||
default_exception_rulename : unique_rulename option;
|
||||
label_idmap : Desugared.Ast.LabelName.t Desugared.Ast.IdentMap.t;
|
||||
label_groups : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t;
|
||||
}
|
||||
|
||||
type scope_context = {
|
||||
@ -180,17 +179,6 @@ let is_def_cond (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : bool =
|
||||
| Desugared.Ast.ScopeDef.Var (x, _) ->
|
||||
is_var_cond ctxt x
|
||||
|
||||
let label_groups
|
||||
(ctxt : context)
|
||||
(s_uid : Scopelang.Ast.ScopeName.t)
|
||||
(def : Desugared.Ast.ScopeDef.t) :
|
||||
Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t =
|
||||
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} *)
|
||||
|
||||
(** Process a subscope declaration *)
|
||||
@ -659,7 +647,6 @@ let process_definition
|
||||
definition for this definition key *)
|
||||
default_exception_rulename = None;
|
||||
label_idmap = Desugared.Ast.IdentMap.empty;
|
||||
label_groups = Desugared.Ast.LabelMap.empty;
|
||||
}
|
||||
~some:(fun x -> x)
|
||||
def_key_ctx
|
||||
@ -679,27 +666,7 @@ let process_definition
|
||||
Some (Desugared.Ast.LabelName.fresh label))
|
||||
def_key_ctx.label_idmap
|
||||
in
|
||||
let label_id =
|
||||
Desugared.Ast.IdentMap.find (Marked.unmark label)
|
||||
new_label_idmap
|
||||
in
|
||||
{
|
||||
def_key_ctx with
|
||||
label_idmap = new_label_idmap;
|
||||
label_groups =
|
||||
Desugared.Ast.LabelMap.update label_id
|
||||
(fun group ->
|
||||
match group with
|
||||
| None ->
|
||||
Some
|
||||
(Desugared.Ast.RuleSet.singleton
|
||||
d.definition_id)
|
||||
| Some existing_group ->
|
||||
Some
|
||||
(Desugared.Ast.RuleSet.add d.definition_id
|
||||
existing_group))
|
||||
def_key_ctx.label_groups;
|
||||
}
|
||||
{ def_key_ctx with label_idmap = new_label_idmap }
|
||||
in
|
||||
(* And second, we update the map of default rulenames for
|
||||
unlabeled exceptions *)
|
||||
|
@ -32,7 +32,6 @@ type unique_rulename =
|
||||
type scope_def_context = {
|
||||
default_exception_rulename : unique_rulename option;
|
||||
label_idmap : Desugared.Ast.LabelName.t Desugared.Ast.IdentMap.t;
|
||||
label_groups : Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t;
|
||||
}
|
||||
|
||||
type scope_context = {
|
||||
@ -136,13 +135,6 @@ val get_def_typ : context -> Desugared.Ast.ScopeDef.t -> typ Marked.pos
|
||||
(** Retrieves the type of a scope definition from the context *)
|
||||
|
||||
val is_def_cond : context -> Desugared.Ast.ScopeDef.t -> bool
|
||||
|
||||
val label_groups :
|
||||
context ->
|
||||
Scopelang.Ast.ScopeName.t ->
|
||||
Desugared.Ast.ScopeDef.t ->
|
||||
Desugared.Ast.RuleSet.t Desugared.Ast.LabelMap.t
|
||||
|
||||
val is_type_cond : Ast.typ Marked.pos -> bool
|
||||
|
||||
val add_def_local_var : context -> ident -> context * Desugared.Ast.Var.t
|
||||
|
@ -1,15 +1,15 @@
|
||||
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_default/bad/conflict.catala_en
|
||||
|
|
||||
9 | definition x under condition true consequence equals 0
|
||||
| ^
|
||||
+ Article
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_default/bad/conflict.catala_en
|
||||
|
|
||||
8 | definition x under condition true consequence equals 1
|
||||
| ^
|
||||
+ Article
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_default/bad/conflict.catala_en
|
||||
|
|
||||
9 | definition x under condition true consequence equals 0
|
||||
| ^
|
||||
+ Article
|
||||
|
@ -14,8 +14,8 @@ Cyclic exception for definition of variable "x", declared here:
|
||||
Used here in the definition of another cyclic exception for defining "x":
|
||||
--> tests/test_exception/bad/exceptions_cycle.catala_en
|
||||
|
|
||||
18 | definition x equals 2
|
||||
| ^
|
||||
17 | exception exception_x
|
||||
| ^^^^^^^^^^^
|
||||
+ Test
|
||||
|
||||
Cyclic exception for definition of variable "x", declared here:
|
||||
@ -32,8 +32,8 @@ Cyclic exception for definition of variable "x", declared here:
|
||||
Used here in the definition of another cyclic exception for defining "x":
|
||||
--> tests/test_exception/bad/exceptions_cycle.catala_en
|
||||
|
|
||||
14 | definition x equals 1
|
||||
| ^
|
||||
13 | exception base_x
|
||||
| ^^^^^^
|
||||
+ Test
|
||||
|
||||
Cyclic exception for definition of variable "x", declared here:
|
||||
@ -48,8 +48,8 @@ Cyclic exception for definition of variable "x", declared here:
|
||||
+
|
||||
|
||||
Used here in the definition of another cyclic exception for defining "x":
|
||||
--> tests/test_exception/bad/exceptions_cycle.catala_en
|
||||
|
|
||||
10 | definition x equals 0
|
||||
| ^
|
||||
+ Test
|
||||
--> tests/test_exception/bad/exceptions_cycle.catala_en
|
||||
|
|
||||
9 | exception exception_exception_x
|
||||
| ^^^^^^^^^^^^^^^^^^^^^
|
||||
+ Test
|
||||
|
@ -1,7 +1,7 @@
|
||||
[ERROR] Cannot define rule as an exception to itself
|
||||
|
||||
--> tests/test_exception/bad/self_exception.catala_en
|
||||
|
|
||||
10 | definition y equals 0
|
||||
| ^
|
||||
+ Test
|
||||
--> tests/test_exception/bad/self_exception.catala_en
|
||||
|
|
||||
9 | exception base_y
|
||||
| ^^^^^^
|
||||
+ Test
|
||||
|
@ -1,15 +1,15 @@
|
||||
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_exception/bad/two_exceptions.catala_en
|
||||
|
|
||||
15 | definition x equals 2
|
||||
| ^
|
||||
+ Test
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_exception/bad/two_exceptions.catala_en
|
||||
|
|
||||
12 | definition x equals 1
|
||||
| ^
|
||||
+ Test
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_exception/bad/two_exceptions.catala_en
|
||||
|
|
||||
15 | definition x equals 2
|
||||
| ^
|
||||
+ Test
|
||||
|
@ -1,6 +1,8 @@
|
||||
let scope Foo (y: integer|input) (x: integer|internal|output) =
|
||||
let x : integer =
|
||||
⟨⟨⟨y = 5 ⊢ 5⟩, ⟨y = 4 ⊢ 4⟩ | true ⊢
|
||||
⟨⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | true ⊢
|
||||
⟨⟨y = 0 ⊢ 0⟩, ⟨y = 1 ⊢ 1⟩ | false ⊢ ∅ ⟩⟩⟩
|
||||
| false ⊢ ∅ ⟩
|
||||
⟨⟨⟨⟨⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ ∅ ⟩ |
|
||||
true ⊢
|
||||
⟨⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ ∅ ⟩⟩ |
|
||||
true ⊢
|
||||
⟨⟨y = 0 ⊢ 0⟩, ⟨y = 1 ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ |
|
||||
false ⊢ ∅ ⟩
|
||||
|
@ -1,15 +1,15 @@
|
||||
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_func/bad/bad_func.catala_en
|
||||
|
|
||||
15 | definition f of x under condition not b consequence equals x * x
|
||||
| ^^^^^
|
||||
+ Article
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_func/bad/bad_func.catala_en
|
||||
|
|
||||
14 | definition f of x under condition (x >= x) consequence equals x + x
|
||||
| ^^^^^
|
||||
+ Article
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_func/bad/bad_func.catala_en
|
||||
|
|
||||
15 | definition f of x under condition not b consequence equals x * x
|
||||
| ^^^^^
|
||||
+ Article
|
||||
|
@ -1,15 +1,15 @@
|
||||
[ERROR] There is a conflict between multiple valid consequences for assigning the same variable.
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_scope/bad/scope.catala_en
|
||||
|
|
||||
14 | definition b under condition not c consequence equals 0
|
||||
| ^
|
||||
+ Article
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_scope/bad/scope.catala_en
|
||||
|
|
||||
13 | definition b under condition not c consequence equals 1337
|
||||
| ^^^^
|
||||
+ Article
|
||||
|
||||
This consequence has a valid justification:
|
||||
--> tests/test_scope/bad/scope.catala_en
|
||||
|
|
||||
14 | definition b under condition not c consequence equals 0
|
||||
| ^
|
||||
+ Article
|
||||
|
Loading…
Reference in New Issue
Block a user