CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-09 22:16:10 +03:00
Code Issues Projects Releases Wiki Activity

Flipped defaults to an exception-based structured

Browse Source
This commit is contained in:
Denis Merigoux 2020-12-18 15:59:15 +01:00
parent 81c464ea7e
commit ea1611cd41
15 changed files with 139 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/catala/catala_surface/desugaring.ml
View File

@ -364,7 +364,7 @@ let process_default (ctxt : Name_resolution.context) (scope : Scopelang.Ast.Scop
(def_key : Desugared.Ast.ScopeDef.t Pos.marked)
(param_uid : Scopelang.Ast.Var.t Pos.marked option)
(precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
(parent_rule : Desugared.Ast.RuleName.t option) (just : Ast.expression Pos.marked option)
(exception_to_rule : Desugared.Ast.RuleName.t option) (just : Ast.expression Pos.marked option)
(cons : Ast.expression Pos.marked) : Desugared.Ast.rule =
let just = match just with Some just -> Some (translate_expr scope ctxt just) | None -> None in
let just = merge_conditions precond just (Pos.get_position def_key) in
@ -385,7 +385,7 @@ let process_default (ctxt : Name_resolution.context) (scope : Scopelang.Ast.Scop
"this definition has a parameter but its type is not a function"
(Pos.get_position (Bindlib.unbox cons))
| _ -> None);
parent_rule;
exception_to_rule;
}
(** Wrapper around {!val: process_default} that performs some name disambiguation *)

2
src/catala/default_calculus/ast.ml
View File

@ -89,7 +89,7 @@ type expr =
| EApp of expr Pos.marked * expr Pos.marked list
| EAssert of expr Pos.marked
| EOp of operator
| EDefault of expr Pos.marked * expr Pos.marked * expr Pos.marked list
| EDefault of expr Pos.marked list * expr Pos.marked * expr Pos.marked
| EIfThenElse of expr Pos.marked * expr Pos.marked * expr Pos.marked
(** {1 Variable helpers} *)

59
src/catala/default_calculus/interpreter.ml
View File

@ -248,44 +248,31 @@ let rec evaluate_expr (e : A.expr Pos.marked) : A.expr Pos.marked =
"Expected a term having a sum type as an argument to a match (should not happend if \
the term was well-typed"
(Pos.get_position e1) )
| EDefault (just, cons, subs) -> (
let just = evaluate_expr just in
match Pos.unmark just with
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| ELit (LBool true) -> (
match evaluate_expr cons with
| ELit LEmptyError, pos ->
evaluate_expr
(Pos.same_pos_as
(Ast.EDefault ((ELit (LBool false), pos), (Ast.ELit LEmptyError, pos), subs))
e)
| e' -> e' )
| ELit (LBool false) -> (
let subs_orig = subs in
let subs = List.map evaluate_expr subs in
let empty_count = List.length (List.filter is_empty_error subs) in
match List.length subs - empty_count with
| 0 -> Pos.same_pos_as (A.ELit LEmptyError) e
| 1 -> List.find (fun sub -> not (is_empty_error sub)) subs
| EDefault (exceptions, just, cons) -> (
let exceptions_orig = exceptions in
let exceptions = List.map evaluate_expr exceptions in
let empty_count = List.length (List.filter is_empty_error exceptions) in
match List.length exceptions - empty_count with
| 0 -> (
let just = evaluate_expr just in
match Pos.unmark just with
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| ELit (LBool true) -> evaluate_expr cons
| ELit (LBool false) -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_multispanned_error
"There is a conflict between multiple rules for assigning the same variable."
( ( if Pos.get_position e = Pos.no_pos then []
else
[
( Some "This rule is not triggered, so we consider rules of lower priority:",
Pos.get_position e );
] )
@ List.map
(fun (_, sub) -> (Some "This justification is true:", Pos.get_position sub))
(List.filter
(fun (sub, _) -> not (is_empty_error sub))
(List.map2 (fun x y -> (x, y)) subs subs_orig)) ) )
Errors.raise_spanned_error
"Default justification has not been reduced to a boolean at evaluation (should not \
happen if the term was well-typed"
(Pos.get_position e) )
| 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions
| _ ->
Errors.raise_spanned_error
"Default justification has not been reduced to a boolean at evaluation (should not \
happen if the term was well-typed"
(Pos.get_position e) )
Errors.raise_multispanned_error
"There is a conflict between multiple exceptions for assigning the same variable."
(List.map
(fun (_, except) -> (Some "This justification is true:", Pos.get_position except))
(List.filter
(fun (sub, _) -> not (is_empty_error sub))
(List.map2 (fun x y -> (x, y)) exceptions exceptions_orig))) )
| EIfThenElse (cond, et, ef) -> (
match Pos.unmark (evaluate_expr cond) with
| ELit (LBool true) -> evaluate_expr et

8
src/catala/default_calculus/print.ml
View File

@ -202,11 +202,11 @@ let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
e1 format_expr e2 format_expr e3
| EOp (Binop op) -> Format.fprintf fmt "%a" format_binop (op, Pos.no_pos)
| EOp (Unop op) -> Format.fprintf fmt "%a" format_unop (op, Pos.no_pos)
| EDefault (just, cons, subs) ->
if List.length subs = 0 then
| EDefault (exceptions, just, cons) ->
if List.length exceptions = 0 then
Format.fprintf fmt "@[⟨%a ⊢ %a⟩@]" format_expr just format_expr cons
else
Format.fprintf fmt "@[<hov 2>⟨%a ⊢ %a |@ %a⟩@]" format_expr just format_expr cons
Format.fprintf fmt "@[<hov 2>⟨%a@ |@ %a ⊢ %a ⟩@]"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr)
subs
exceptions format_expr just format_expr cons
| EAssert e' -> Format.fprintf fmt "@[<hov 2>assert@ (%a)@]" format_expr e'

8
src/catala/default_calculus/typing.ml
View File

@ -241,10 +241,10 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m
typecheck_expr_top_down env e1 t_app;
t_ret
| EOp op -> op_type (Pos.same_pos_as op e)
| EDefault (just, cons, subs) ->
| EDefault (excepts, just, cons) ->
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as (TLit TBool) just));
let tcons = typecheck_expr_bottom_up env cons in
List.iter (fun sub -> typecheck_expr_top_down env sub tcons) subs;
List.iter (fun except -> typecheck_expr_top_down env except tcons) excepts;
tcons
| EIfThenElse (cond, et, ef) ->
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as (TLit TBool) cond));
@ -372,10 +372,10 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
| EOp op ->
let op_typ = op_type (Pos.same_pos_as op e) in
unify op_typ tau
| EDefault (just, cons, subs) ->
| EDefault (excepts, just, cons) ->
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as (TLit TBool) just));
typecheck_expr_top_down env cons tau;
List.iter (fun sub -> typecheck_expr_top_down env sub tau) subs
List.iter (fun except -> typecheck_expr_top_down env except tau) excepts
| EIfThenElse (cond, et, ef) ->
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as (TLit TBool) cond));
typecheck_expr_top_down env et tau;

11
src/catala/desugared/ast.ml
View File

@ -25,6 +25,8 @@ module RuleName : Uid.Id with type info = Uid.MarkedString.info = Uid.Make (Uid.
module RuleMap : Map.S with type key = RuleName.t = Map.Make (RuleName)
module RuleSet : Set.S with type elt = RuleName.t = Set.Make (RuleName)
(** Inside a scope, a definition can refer either to a scope def, or a subscope def *)
module ScopeDef = struct
type t =
@ -39,6 +41,11 @@ module ScopeDef = struct
Scopelang.Ast.ScopeVar.compare x y
| SubScopeVar (_, x), SubScopeVar (_, y) -> Scopelang.Ast.ScopeVar.compare x y
let get_position x =
match x with
| Var x -> Pos.get_position (Scopelang.Ast.ScopeVar.get_info x)
| SubScopeVar (x, _) -> Pos.get_position (Scopelang.Ast.SubScopeName.get_info x)
let format_t fmt x =
match x with
| Var v -> Scopelang.Ast.ScopeVar.format_t fmt v
@ -62,7 +69,7 @@ type rule = {
just : Scopelang.Ast.expr Pos.marked Bindlib.box;
cons : Scopelang.Ast.expr Pos.marked Bindlib.box;
parameter : (Scopelang.Ast.Var.t * Scopelang.Ast.typ Pos.marked) option;
parent_rule : RuleName.t option;
exception_to_rule : RuleName.t option;
}
let empty_rule (pos : Pos.t) (have_parameter : Scopelang.Ast.typ Pos.marked option) : rule =
@ -73,7 +80,7 @@ let empty_rule (pos : Pos.t) (have_parameter : Scopelang.Ast.typ Pos.marked opti
( match have_parameter with
| Some typ -> Some (Scopelang.Ast.Var.make ("dummy", pos), typ)
| None -> None );
parent_rule = None;
exception_to_rule = None;
}
type assertion = Scopelang.Ast.expr Pos.marked Bindlib.box

125
src/catala/desugared/desugared_to_scope.ml
View File

@ -20,47 +20,85 @@ module Cli = Utils.Cli
(** {1 Rule tree construction} *)
type rule_tree = Leaf of Ast.rule | Node of Ast.rule * rule_tree list
type rule_tree = Leaf of Ast.rule | Node of rule_tree list * Ast.rule
(** Transforms a flat list of rules into a tree, taking into account the priorities declared between
rules
{e Invariant:} only one rule does not have any parent rule
{e Invariant:} there are no exceptions cycles
{e Invariant:} there are no dandling pointer parents in the rules *)
let rec def_map_to_tree (def : Ast.rule Ast.RuleMap.t) : rule_tree =
(* first we look to the only rule that does not have any parent *)
let has_no_parent _ (r : Ast.rule) = Option.is_none r.Ast.parent_rule in
let no_parent = Ast.RuleMap.filter has_no_parent def in
let no_parent_name, no_parent =
if Ast.RuleMap.cardinal no_parent = 1 then Ast.RuleMap.choose no_parent else assert false
{e Invariant:} there are no dandling exception pointers in the rules *)
let rec def_map_to_tree (def_info : Ast.ScopeDef.t)
(is_def_func : Scopelang.Ast.typ Pos.marked option) (def : Ast.rule Ast.RuleMap.t) :
rule_tree list =
(* first we look to the rules that don't have any exceptions *)
let has_no_exception (r : Ast.RuleName.t) _ =
not
(Ast.RuleMap.exists
(fun _ r' -> match r'.Ast.exception_to_rule with Some r_ex -> r_ex = r | None -> false)
def)
in
let def = Ast.RuleMap.remove no_parent_name def in
(* we look for all the direct children of no_parent *)
let children, rest =
Ast.RuleMap.partition (fun _ r -> r.Ast.parent_rule = Some no_parent_name) def
let no_exceptions = Ast.RuleMap.filter has_no_exception def in
(* Then, for each top-level rule (that has no exceptions), we build a rule tree *)
(* Among the top-level rules are the base rules that are exceptions to nothing *)
let base_rules, rules_that_are_exceptions =
Ast.RuleMap.partition (fun _ r -> Option.is_none r.Ast.exception_to_rule) no_exceptions
in
if Ast.RuleMap.cardinal children = 0 then Leaf no_parent
(* it doesn't matter that [rest] contains more rules since each rule in [rest] is supposed to
have a parent rule containted in the original tree, so it will get treated at some point *)
else
let children_no_parent =
Ast.RuleMap.map (fun r -> { r with Ast.parent_rule = None }) children
in
let tree_children =
List.map
(fun (child_no_parent_name, child_no_parent) ->
def_map_to_tree (Ast.RuleMap.add child_no_parent_name child_no_parent rest))
(Ast.RuleMap.bindings children_no_parent)
in
Node (no_parent, tree_children)
let base_trees : rule_tree Ast.RuleMap.t =
Ast.RuleMap.map
(fun r ->
(* we look at the the eventual rule of which r is an exception *)
match r.Ast.exception_to_rule with None -> Leaf r | Some _ -> assert false
(* should not happen *))
base_rules
in
(* Now let's deal with the rules that are exceptions but have no exception. We have to bucket
these, each bucket containing all the rules that are exception to the same rule *)
let exception_targets =
Ast.RuleMap.fold
(fun _ r acc ->
match r.Ast.exception_to_rule with
| None -> assert false (* should not happen *)
| Some r' -> Ast.RuleMap.add r' () acc)
rules_that_are_exceptions Ast.RuleMap.empty
in
(* In each bucket corresponding to an exception target, we have all the rules that are exceptions
to the target *)
let exception_trees =
Ast.RuleMap.mapi
(fun r' _ ->
(* we recursively call the function of a def where we have removed exception edges: this is
why the function should terminate *)
let def_rec =
Ast.RuleMap.map
(fun r ->
{
r with
Ast.exception_to_rule =
( match r.Ast.exception_to_rule with
| None -> None
| Some r'' -> if r'' = r' then None else Some r'' );
})
def
in
let def_rec =
Ast.RuleMap.filter (fun r _ -> not (Ast.RuleMap.mem r exception_targets)) def_rec
in
let exceptions = def_map_to_tree def_info is_def_func def_rec in
Node (exceptions, Ast.RuleMap.find r' def))
exception_targets
in
List.map snd (Ast.RuleMap.bindings base_trees)
@ List.map snd (Ast.RuleMap.bindings exception_trees)
(** From the {!type: rule_tree}, builds an {!constructor: Dcalc.Ast.EDefault} expression in the
scope language. The [~toplevel] parameter is used to know when to place the toplevel binding in
the case of functions. *)
let rec rule_tree_to_expr ~(toplevel : bool) (is_func : Scopelang.Ast.Var.t option)
(tree : rule_tree) : Scopelang.Ast.expr Pos.marked Bindlib.box =
let rule, children = match tree with Leaf r -> (r, []) | Node (r, child) -> (r, child) in
let exceptions, rule =
match tree with Leaf r -> ([], r) | Node (exceptions, r) -> (exceptions, r)
in
(* because each rule has its own variable parameter and we want to convert the whole rule tree
into a function, we need to perform some alpha-renaming of all the expressions *)
let substitute_parameter (e : Scopelang.Ast.expr Pos.marked Bindlib.box) :
@ -77,12 +115,14 @@ let rec rule_tree_to_expr ~(toplevel : bool) (is_func : Scopelang.Ast.Var.t opti
in
let just = substitute_parameter rule.Ast.just in
let cons = substitute_parameter rule.Ast.cons in
let children = Bindlib.box_list (List.map (rule_tree_to_expr ~toplevel:false is_func) children) in
let exceptions =
Bindlib.box_list (List.map (rule_tree_to_expr ~toplevel:false is_func) exceptions)
in
let default =
Bindlib.box_apply3
(fun just cons children ->
(Scopelang.Ast.EDefault (just, cons, children), Pos.get_position just))
just cons children
(fun exceptions just cons ->
(Scopelang.Ast.EDefault (exceptions, just, cons), Pos.get_position just))
exceptions just cons
in
match (is_func, rule.parameter) with
| None, None -> default
@ -99,8 +139,6 @@ let rec rule_tree_to_expr ~(toplevel : bool) (is_func : Scopelang.Ast.Var.t opti
let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
(typ : Scopelang.Ast.typ Pos.marked) : Scopelang.Ast.expr Pos.marked =
(* Here, we have to transform this list of rules into a default tree. *)
(* Because we can have multiple rules at the top-level and our syntax does not allow that, we
insert a dummy rule at the top *)
let is_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.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
@ -128,22 +166,15 @@ let translate_def (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
Pos.get_position (Bindlib.unbox r.Ast.cons) ))
(Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_func n r)) def)) )
in
let dummy_rule = Ast.empty_rule Pos.no_pos is_def_func in
let dummy_rule_name = Ast.RuleName.fresh ("dummy", Pos.no_pos) in
let def =
Ast.RuleMap.add dummy_rule_name dummy_rule
(Ast.RuleMap.map
(fun r ->
match r.Ast.parent_rule with
| Some _ -> r
| None -> { r with parent_rule = Some dummy_rule_name })
def)
in
let def_tree = def_map_to_tree def in
let top_list = def_map_to_tree def_info is_def_func def in
Bindlib.unbox
(rule_tree_to_expr ~toplevel:true
(Option.map (fun _ -> Scopelang.Ast.Var.make ("ρ", Pos.no_pos)) is_def_func)
def_tree)
( match top_list with
| [] ->
(* In this case, there are no rules to define the expression *)
Leaf (Ast.empty_rule Pos.no_pos is_def_func)
| _ -> Node (top_list, Ast.empty_rule Pos.no_pos is_def_func) ))
(** Translates a scope *)
let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =

8
src/catala/scope_language/ast.ml
View File

@ -94,7 +94,7 @@ type expr =
| EAbs of Pos.t * (expr, expr Pos.marked) Bindlib.mbinder * typ Pos.marked list
| EApp of expr Pos.marked * expr Pos.marked list
| EOp of Dcalc.Ast.operator
| EDefault of expr Pos.marked * expr Pos.marked * expr Pos.marked list
| EDefault of expr Pos.marked list * expr Pos.marked * expr Pos.marked
| EIfThenElse of expr Pos.marked * expr Pos.marked * expr Pos.marked
let rec locations_used (e : expr Pos.marked) : LocationSet.t =
@ -121,11 +121,11 @@ let rec locations_used (e : expr Pos.marked) : LocationSet.t =
| EIfThenElse (e1, e2, e3) ->
LocationSet.union (locations_used e1)
(LocationSet.union (locations_used e2) (locations_used e3))
| EDefault (just, cons, subs) ->
| EDefault (excepts, just, cons) ->
List.fold_left
(fun acc sub -> LocationSet.union (locations_used sub) acc)
(fun acc except -> LocationSet.union (locations_used except) acc)
(LocationSet.union (locations_used just) (locations_used cons))
subs
excepts
type rule =
| Definition of location Pos.marked * typ Pos.marked * expr Pos.marked

8
src/catala/scope_language/print.ml
View File

@ -106,10 +106,10 @@ let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
e1 format_expr e2 format_expr e3
| EOp (Binop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_binop (op, Pos.no_pos)
| EOp (Unop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_unop (op, Pos.no_pos)
| EDefault (just, cons, subs) ->
if List.length subs = 0 then
| EDefault (excepts, just, cons) ->
if List.length excepts = 0 then
Format.fprintf fmt "@[⟨%a ⊢ %a⟩@]" format_expr just format_expr cons
else
Format.fprintf fmt "@[<hov 2>⟨%a ⊢ %a |@ %a⟩@]" format_expr just format_expr cons
Format.fprintf fmt "@[<hov 2>⟨%a@ |@ %a ⊢ %a⟩@]"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr)
subs
excepts format_expr just format_expr cons

8
src/catala/scope_language/scope_to_dcalc.ml
View File

@ -68,7 +68,7 @@ let merge_defaults (caller : Dcalc.Ast.expr Pos.marked Bindlib.box)
Bindlib.box_apply2
(fun caller callee ->
( Dcalc.Ast.EDefault
((Dcalc.Ast.ELit (Dcalc.Ast.LBool true), Pos.no_pos), caller, [ callee ]),
([ caller ], (Dcalc.Ast.ELit (Dcalc.Ast.LBool true), Pos.no_pos), callee),
Pos.no_pos ))
caller callee
in
@ -211,11 +211,11 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Po
Bindlib.box_apply
(fun b -> Dcalc.Ast.EAbs (pos_binder, b, List.map (translate_typ ctx) typ))
binder
| EDefault (just, cons, subs) ->
| EDefault (excepts, just, cons) ->
Bindlib.box_apply3
(fun j c s -> Dcalc.Ast.EDefault (j, c, s))
(fun e j c -> Dcalc.Ast.EDefault (e, j, c))
(Bindlib.box_list (List.map (translate_expr ctx) excepts))
(translate_expr ctx just) (translate_expr ctx cons)
(Bindlib.box_list (List.map (translate_expr ctx) subs))
| ELocation (ScopeVar a) ->
Bindlib.box_var (fst (Ast.ScopeVarMap.find (Pos.unmark a) ctx.scope_vars))
| ELocation (SubScopeVar (_, s, a)) -> (

2
tests/test_default/conflict.catala.A.out
View File

@ -1,4 +1,4 @@
[ERROR] There is a conflict between multiple rules for assigning the same variable.
[ERROR] There is a conflict between multiple exceptions for assigning the same variable.
[ERROR]
[ERROR] This justification is true:
[ERROR] --> test_default/conflict.catala

2
tests/test_func/func.catala.S.out
View File

@ -1,4 +1,4 @@
[ERROR] There is a conflict between multiple rules for assigning the same variable.
[ERROR] There is a conflict between multiple exceptions for assigning the same variable.
[ERROR]
[ERROR] This justification is true:
[ERROR] --> test_func/func.catala

4
tests/test_money/no_mingle.catala.A.out
View File

@ -18,7 +18,7 @@
[ERROR] 12 | def z := (x *$ y)
[ERROR] | ^^
[ERROR]
[ERROR] Type money → money coming from expression:
[ERROR] Type money → any type coming from expression:
[ERROR] --> test_money/no_mingle.catala
[ERROR] |
[ERROR] 12 | def z := (x *$ y)
@ -30,7 +30,7 @@
[ERROR] 12 | def z := (x *$ y)
[ERROR] | ^^
[ERROR]
[ERROR] Type money → money → money coming from expression:
[ERROR] Type money → money → any type coming from expression:
[ERROR] --> test_money/no_mingle.catala
[ERROR] |
[ERROR] 12 | def z := (x *$ y)

2
tests/test_scope/scope.catala.A.out
View File

@ -1,4 +1,4 @@
[ERROR] There is a conflict between multiple rules for assigning the same variable.
[ERROR] There is a conflict between multiple exceptions for assigning the same variable.
[ERROR]
[ERROR] This justification is true:
[ERROR] --> test_scope/scope.catala

2
tests/test_scope/sub_sub_scope.catala.B.out
View File

@ -1,4 +1,4 @@
[ERROR] There is a conflict between multiple rules for assigning the same variable.
[ERROR] There is a conflict between multiple exceptions for assigning the same variable.
[ERROR]
[ERROR] This justification is true:
[ERROR] --> test_scope/sub_sub_scope.catala