Typed defaults: small simplification and fixes

This commit is contained in:
Louis Gesbert 2023-11-10 18:14:48 +01:00
parent 3a149bc86e
commit cc4e5339dd
7 changed files with 17 additions and 29 deletions

View File

@ -910,8 +910,6 @@ let translate_rule
scope_let_pos;
scope_let_typ;
scope_let_expr =
(* To ensure that we throw an error if the value is not
defined, we add an check "ErrorOnEmpty" here. *)
Mark.add
(Expr.map_ty (fun _ -> scope_let_typ) (Mark.get e))
(EAssert new_e);

View File

@ -174,10 +174,7 @@ let empty_rule
(parameters : (Uid.MarkedString.info * typ) list Mark.pos option) : rule =
{
rule_just = Expr.box (ELit (LBool false), Untyped { pos });
rule_cons =
Expr.eerroronempty
(Expr.box (EEmptyError, Untyped { pos }))
(Untyped { pos });
rule_cons = Expr.box (EEmptyError, Untyped { pos });
rule_parameter =
Option.map
(Mark.map (List.map (fun (lbl, typ) -> Mark.map Var.make lbl, typ)))

View File

@ -421,15 +421,22 @@ let rec rule_tree_to_expr
let default_containing_base_cases =
Expr.edefault
~excepts:
(List.map2
(fun base_just base_cons ->
Expr.make_default []
(* Here we insert the logging command that records when a
decision is taken for the value of a variable. *)
(tag_with_log_entry base_just PosRecordIfTrueBool [])
base_cons)
(List.fold_right2
(fun base_just base_cons acc ->
match Expr.unbox base_just with
| ELit (LBool false), _ -> acc
| _ ->
Expr.edefault
~excepts:[]
(* Here we insert the logging command that records when a
decision is taken for the value of a variable. *)
~just:(tag_with_log_entry base_just PosRecordIfTrueBool [])
~cons:(Expr.epuredefault base_cons emark)
emark
:: acc)
(translate_and_unbox_list base_just_list)
(translate_and_unbox_list base_cons_list))
(translate_and_unbox_list base_cons_list)
[])
~just:(Expr.elit (LBool false) emark)
~cons:(Expr.eemptyerror emark) emark
in

View File

@ -978,10 +978,6 @@ let make_puredefault e =
in
epuredefault e mark
let make_default excepts just cons =
let cons = make_puredefault cons in
edefault ~excepts ~just ~cons (Mark.get cons)
let make_tuple el m0 =
match el with
| [] -> etuple [] (with_ty m0 (TTuple [], mark_pos m0))

View File

@ -350,15 +350,6 @@ val make_multiple_let_in :
Pos.t ->
('a any, 'm) boxed_gexpr
val make_default :
('a, 'm) boxed_gexpr list ->
('a, 'm) boxed_gexpr ->
('a, 'm) boxed_gexpr ->
(* 'm mark -> *)
((< polymorphic : yes ; defaultTerms : yes ; .. > as 'a), 'm) boxed_gexpr
(** The [cons] argument is implicitely made into a [EPureDefault] by this
function *)
val make_tuple :
('a any, 'm) boxed_gexpr list -> 'm mark -> ('a, 'm) boxed_gexpr
(** Builds a tuple; the mark argument is only used as witness and for position

View File

@ -293,7 +293,6 @@ let polymorphic_op_type (op : Operator.polymorphic A.operator Mark.pos) :
let it = lazy (UnionFind.make (TLit TInt, pos)) in
let cet = lazy (UnionFind.make (TClosureEnv, pos)) in
let array a = lazy (UnionFind.make (TArray (Lazy.force a), pos)) in
(* let option a = lazy (UnionFind.make (TOption (Lazy.force a), pos)) in *)
let default a = lazy (UnionFind.make (TDefault (Lazy.force a), pos)) in
let ( @-> ) x y =
lazy (UnionFind.make (TArrow (List.map Lazy.force x, Lazy.force y), pos))

View File

@ -20,7 +20,7 @@ $ catala Interpret -s A
└─ Article
[ERROR]
This variable evaluated to an empty term (no rule that defined it applied in this situation):
error_empty ⟨ ⟨false ⊢ ⟨error_empty ∅⟩⟩ | false ⊢ ∅
error_empty ⟨false ⊢ ∅⟩
┌─⯈ tests/test_default/bad/empty.catala_en:6.10-6.11:
└─┐