Compiler: simplify EDefault term at construction

This allows to match on their structure further on.
This commit is contained in:
Louis Gesbert 2022-05-25 14:47:23 +02:00
parent 2d41f53300
commit cd70e16ea3
8 changed files with 54 additions and 53 deletions

View File

@ -129,8 +129,8 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
| EDefault (excepts, just, cons) ->
Bindlib.box_apply3
(fun new_excepts new_just new_cons ->
( Scopelang.Ast.EDefault (new_excepts, new_just, new_cons),
Pos.get_position e ))
Scopelang.Ast.make_default ~pos:(Pos.get_position e) new_excepts
new_just new_cons)
(Bindlib.box_list (List.map (translate_expr ctx) excepts))
(translate_expr ctx just) (translate_expr ctx cons)
| EIfThenElse (e1, e2, e3) ->
@ -181,7 +181,7 @@ let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) :
let base_case_as_rule_list =
List.map
(fun r -> Ast.RuleMap.find r def)
(List.of_seq (Ast.RuleSet.to_seq base_cases))
(Ast.RuleSet.elements base_cases)
in
match exceptions with
| [] -> Leaf base_case_as_rule_list
@ -261,21 +261,17 @@ let rec rule_tree_to_expr
let default_containing_base_cases =
Bindlib.box_apply2
(fun base_just_list base_cons_list ->
( Scopelang.Ast.EDefault
( List.map2
(fun base_just base_cons ->
( Scopelang.Ast.EDefault
( [],
(* 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
Dcalc.Ast.PosRecordIfTrueBool [],
base_cons ),
Pos.get_position base_just ))
base_just_list base_cons_list,
(Scopelang.Ast.ELit (Dcalc.Ast.LBool false), def_pos),
(Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, def_pos) ),
def_pos ))
Scopelang.Ast.make_default
(List.map2
(fun base_just base_cons ->
Scopelang.Ast.make_default ~pos:def_pos []
(* 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 Dcalc.Ast.PosRecordIfTrueBool [])
base_cons)
base_just_list base_cons_list)
(Scopelang.Ast.ELit (Dcalc.Ast.LBool false), def_pos)
(Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, def_pos))
(Bindlib.box_list (translate_and_unbox_list base_just_list))
(Bindlib.box_list (translate_and_unbox_list base_cons_list))
in
@ -288,11 +284,9 @@ let rec rule_tree_to_expr
let default =
Bindlib.box_apply2
(fun exceptions default_containing_base_cases ->
( Scopelang.Ast.EDefault
( exceptions,
(Scopelang.Ast.ELit (Dcalc.Ast.LBool true), def_pos),
default_containing_base_cases ),
def_pos ))
Scopelang.Ast.make_default exceptions
(Scopelang.Ast.ELit (Dcalc.Ast.LBool true), def_pos)
default_containing_base_cases)
exceptions default_containing_base_cases
in
match is_func, (List.hd base_rules).Ast.rule_parameter with

View File

@ -328,4 +328,19 @@ let make_let_in
(Pos.get_position (Bindlib.unbox e2)))
(Bindlib.box_list [e1])
let make_default ?(pos = Pos.no_pos) exceptions just cons =
let rec bool_value = function
| ELit (Dcalc.Ast.LBool b), _ -> Some b
| EApp ((EOp (Unop (Log _)), _), [e]), _ -> bool_value e
| _ -> None
in
match exceptions, bool_value just, cons with
| [], Some true, cons -> cons
| exceptions, Some true, (EDefault ([], just, cons), pos) ->
EDefault (exceptions, just, cons), pos
| [except], Some false, _ -> except
| exceptions, _, cons ->
let pos = if pos <> Pos.no_pos then pos else Pos.get_position just in
EDefault (exceptions, just, cons), pos
module VarMap = Map.Make (Var)

View File

@ -169,3 +169,13 @@ val make_let_in :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box
val make_default :
?pos:Pos.t ->
expr Pos.marked list ->
expr Pos.marked ->
expr Pos.marked ->
expr Pos.marked
(** [make_default ?pos exceptions just cons] builds the equivalent to an
[EDefault] term, while avoiding redundant nested constructions. The position
is extracted from [just] by default. *)

View File

@ -6,13 +6,10 @@ let TestBool_13 :
let foo_15 : unit → bool = TestBool_in_14."foo_in" in
let bar_16 : unit → integer = TestBool_in_14."bar_in" in
let bar_17 : integer = error_empty
⟨bar_16 () | true ⊢
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
⟨bar_16 () | true ⊢ ⟨1 | false ⊢ ∅ ⟩⟩ in
let foo_18 : bool = error_empty
⟨foo_15 () | true ⊢
⟨⟨true ⊢ ⟨⟨bar_17 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
⟨true ⊢ ⟨⟨bar_17 >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
⟨⟨bar_17 < 0 ⊢ false⟩, ⟨bar_17 >= 0 ⊢ true⟩ | false ⊢
∅ ⟩⟩ in
TestBool_out {"foo_out"= foo_18; "bar_out"= bar_17} in
TestBool_13

View File

@ -1,8 +1,4 @@
let scope TestBool (foo: bool|context|output) (bar: integer|context|output) =
let bar : integer = reentrant or by default
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩;
let bar : integer = reentrant or by default ⟨1 | false ⊢ ∅ ⟩;
let foo : bool = reentrant or by default
⟨⟨true ⊢ ⟨⟨bar < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩,
⟨true ⊢ ⟨⟨bar >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩
⟨⟨bar < 0 ⊢ false⟩, ⟨bar >= 0 ⊢ true⟩ | false ⊢ ∅ ⟩

View File

@ -5,19 +5,11 @@ let A =
let d_33 : integer = A_in_31."d_in" in
let e_34 : unit → integer = A_in_31."e_in" in
let f_35 : unit → integer = A_in_31."f_in" in
let a_36 : integer = error_empty
⟨⟨true ⊢ ⟨⟨true ⊢ 0⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
let b_37 : integer = error_empty
⟨⟨true ⊢ ⟨⟨true ⊢ a_36 + 1⟩ | false ⊢ ∅ ⟩⟩ | true
⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
let a_36 : integer = error_empty ⟨0 | false ⊢ ∅ ⟩ in
let b_37 : integer = error_empty ⟨a_36 + 1 | false ⊢ ∅ ⟩ in
let e_38 : integer = error_empty
⟨e_34 () | true ⊢
⟨⟨true ⊢
⟨⟨true ⊢ b_37 + c_32 + d_33 + 1⟩ | false ⊢ ∅ ⟩⟩
| true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
⟨e_34 () | true ⊢ ⟨b_37 + c_32 + d_33 + 1 | false ⊢ ∅ ⟩⟩
in
let f_39 : integer = error_empty
⟨f_35 () | true ⊢
⟨⟨true ⊢ ⟨⟨true ⊢ e_38 + 1⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩⟩ in
⟨f_35 () | true ⊢ ⟨e_38 + 1 | false ⊢ ∅ ⟩⟩ in
A_out {"b_out"= b_37; "d_out"= d_33; "f_out"= f_39}

View File

@ -1,7 +1,6 @@
let B =
λ (B_in_31: B_in{}) →
let a.x_32 : bool = error_empty
⟨true ⊢ ⟨⟨true ⊢ false⟩ | false ⊢ ∅ ⟩⟩ in
let a.x_32 : bool = error_empty false in
let result_33 : A_out{"y_out": integer} = A_24 (A_in {"x_in"= a.x_32}) in
let a.y_34 : integer = result_33."y_out" in
let __35 : unit = assert (error_empty a.y_34 = 1) in

View File

@ -1,9 +1,7 @@
let B =
λ (B_in_40: B_in{}) →
let a.a_41 : unit → integer = λ (__42: unit) → ∅ in
let a.b_43 : integer = error_empty
⟨⟨true ⊢ ⟨⟨true ⊢ 2⟩ | false ⊢ ∅ ⟩⟩ | true ⊢
⟨⟨false ⊢ ∅ ⟩ | false ⊢ ∅ ⟩⟩ in
let a.b_43 : integer = error_empty ⟨2 | false ⊢ ∅ ⟩ in
let result_44 : A_out{"c_out": integer} =
A_32 (A_in {"a_in"= a.a_41; "b_in"= a.b_43}) in
let a.c_45 : integer = result_44."c_out" in