First attempt at adding conditionals as expressions.
Warning: The simplifier is not done yet.
This commit is contained in:
parent
62e6b1d469
commit
704c744ace
@ -339,6 +339,16 @@ and record_patch = {
|
|||||||
record_inj : record_expr
|
record_inj : record_expr
|
||||||
}
|
}
|
||||||
|
|
||||||
|
and cond_expr = {
|
||||||
|
kwd_if : kwd_if;
|
||||||
|
test : expr;
|
||||||
|
kwd_then : kwd_then;
|
||||||
|
ifso : expr;
|
||||||
|
terminator : semi option;
|
||||||
|
kwd_else : kwd_else;
|
||||||
|
ifnot : expr
|
||||||
|
}
|
||||||
|
|
||||||
and conditional = {
|
and conditional = {
|
||||||
kwd_if : kwd_if;
|
kwd_if : kwd_if;
|
||||||
test : expr;
|
test : expr;
|
||||||
@ -438,7 +448,8 @@ and collection =
|
|||||||
(* Expressions *)
|
(* Expressions *)
|
||||||
|
|
||||||
and expr =
|
and expr =
|
||||||
| ECase of expr case reg
|
ECase of expr case reg
|
||||||
|
| ECond of cond_expr reg
|
||||||
| EAnnot of annot_expr reg
|
| EAnnot of annot_expr reg
|
||||||
| ELogic of logic_expr
|
| ELogic of logic_expr
|
||||||
| EArith of arith_expr
|
| EArith of arith_expr
|
||||||
@ -629,6 +640,7 @@ let rec expr_to_region = function
|
|||||||
| EBytes {region; _}
|
| EBytes {region; _}
|
||||||
| EUnit region
|
| EUnit region
|
||||||
| ECase {region;_}
|
| ECase {region;_}
|
||||||
|
| ECond {region; _}
|
||||||
| EPar {region; _} -> region
|
| EPar {region; _} -> region
|
||||||
|
|
||||||
and tuple_expr_to_region {region; _} = region
|
and tuple_expr_to_region {region; _} = region
|
||||||
|
@ -330,6 +330,16 @@ and record_patch = {
|
|||||||
record_inj : field_assign reg injection reg
|
record_inj : field_assign reg injection reg
|
||||||
}
|
}
|
||||||
|
|
||||||
|
and cond_expr = {
|
||||||
|
kwd_if : kwd_if;
|
||||||
|
test : expr;
|
||||||
|
kwd_then : kwd_then;
|
||||||
|
ifso : expr;
|
||||||
|
terminator : semi option;
|
||||||
|
kwd_else : kwd_else;
|
||||||
|
ifnot : expr
|
||||||
|
}
|
||||||
|
|
||||||
and conditional = {
|
and conditional = {
|
||||||
kwd_if : kwd_if;
|
kwd_if : kwd_if;
|
||||||
test : expr;
|
test : expr;
|
||||||
@ -430,6 +440,7 @@ and collection =
|
|||||||
|
|
||||||
and expr =
|
and expr =
|
||||||
ECase of expr case reg
|
ECase of expr case reg
|
||||||
|
| ECond of cond_expr reg
|
||||||
| EAnnot of annot_expr reg
|
| EAnnot of annot_expr reg
|
||||||
| ELogic of logic_expr
|
| ELogic of logic_expr
|
||||||
| EArith of arith_expr
|
| EArith of arith_expr
|
||||||
|
@ -497,7 +497,7 @@ proc_call:
|
|||||||
conditional:
|
conditional:
|
||||||
If expr Then if_clause option(SEMI) Else if_clause {
|
If expr Then if_clause option(SEMI) Else if_clause {
|
||||||
let region = cover $1 (if_clause_to_region $7) in
|
let region = cover $1 (if_clause_to_region $7) in
|
||||||
let value = {
|
let value : conditional = {
|
||||||
kwd_if = $1;
|
kwd_if = $1;
|
||||||
test = $2;
|
test = $2;
|
||||||
kwd_then = $3;
|
kwd_then = $3;
|
||||||
@ -640,14 +640,28 @@ interactive_expr:
|
|||||||
|
|
||||||
expr:
|
expr:
|
||||||
case(expr) { ECase ($1 expr_to_region) }
|
case(expr) { ECase ($1 expr_to_region) }
|
||||||
|
| cond_expr { $1 }
|
||||||
| disj_expr { $1 }
|
| disj_expr { $1 }
|
||||||
|
|
||||||
|
cond_expr:
|
||||||
|
If expr Then expr option(SEMI) Else expr {
|
||||||
|
let region = cover $1 (expr_to_region $7) in
|
||||||
|
let value : cond_expr = {
|
||||||
|
kwd_if = $1;
|
||||||
|
test = $2;
|
||||||
|
kwd_then = $3;
|
||||||
|
ifso = $4;
|
||||||
|
terminator = $5;
|
||||||
|
kwd_else = $6;
|
||||||
|
ifnot = $7}
|
||||||
|
in ECond {region; value} }
|
||||||
|
|
||||||
disj_expr:
|
disj_expr:
|
||||||
disj_expr Or conj_expr {
|
disj_expr Or conj_expr {
|
||||||
let start = expr_to_region $1
|
let start = expr_to_region $1
|
||||||
and stop = expr_to_region $3 in
|
and stop = expr_to_region $3 in
|
||||||
let region = cover start stop
|
let region = cover start stop
|
||||||
and value = {arg1 = $1; op = $2; arg2 = $3} in
|
and value = {arg1=$1; op=$2; arg2=$3} in
|
||||||
ELogic (BoolExpr (Or {region; value}))
|
ELogic (BoolExpr (Or {region; value}))
|
||||||
}
|
}
|
||||||
| conj_expr { $1 }
|
| conj_expr { $1 }
|
||||||
@ -657,7 +671,7 @@ conj_expr:
|
|||||||
let start = expr_to_region $1
|
let start = expr_to_region $1
|
||||||
and stop = expr_to_region $3 in
|
and stop = expr_to_region $3 in
|
||||||
let region = cover start stop
|
let region = cover start stop
|
||||||
and value = {arg1 = $1; op = $2; arg2 = $3}
|
and value = {arg1=$1; op=$2; arg2=$3}
|
||||||
in ELogic (BoolExpr (And {region; value}))
|
in ELogic (BoolExpr (And {region; value}))
|
||||||
}
|
}
|
||||||
| set_membership { $1 }
|
| set_membership { $1 }
|
||||||
|
@ -256,16 +256,23 @@ and print_instruction buffer = function
|
|||||||
| MapRemove {value; _} -> print_map_remove buffer value
|
| MapRemove {value; _} -> print_map_remove buffer value
|
||||||
| SetRemove {value; _} -> print_set_remove buffer value
|
| SetRemove {value; _} -> print_set_remove buffer value
|
||||||
|
|
||||||
and print_conditional buffer node =
|
and print_cond_expr buffer (node: cond_expr) =
|
||||||
let {kwd_if; test; kwd_then; ifso; terminator;
|
print_token buffer node.kwd_if "if";
|
||||||
kwd_else; ifnot} = node in
|
print_expr buffer node.test;
|
||||||
print_token buffer kwd_if "if";
|
print_token buffer node.kwd_then "then";
|
||||||
print_expr buffer test;
|
print_expr buffer node.ifso;
|
||||||
print_token buffer kwd_then "then";
|
print_terminator buffer node.terminator;
|
||||||
print_if_clause buffer ifso;
|
print_token buffer node.kwd_else "else";
|
||||||
print_terminator buffer terminator;
|
print_expr buffer node.ifnot
|
||||||
print_token buffer kwd_else "else";
|
|
||||||
print_if_clause buffer ifnot
|
and print_conditional buffer (node: conditional) =
|
||||||
|
print_token buffer node.kwd_if "if";
|
||||||
|
print_expr buffer node.test;
|
||||||
|
print_token buffer node.kwd_then "then";
|
||||||
|
print_if_clause buffer node.ifso;
|
||||||
|
print_terminator buffer node.terminator;
|
||||||
|
print_token buffer node.kwd_else "else";
|
||||||
|
print_if_clause buffer node.ifnot
|
||||||
|
|
||||||
and print_if_clause buffer = function
|
and print_if_clause buffer = function
|
||||||
ClauseInstr instr -> print_instruction buffer instr
|
ClauseInstr instr -> print_instruction buffer instr
|
||||||
@ -374,6 +381,7 @@ and print_bind_to buffer = function
|
|||||||
|
|
||||||
and print_expr buffer = function
|
and print_expr buffer = function
|
||||||
ECase {value;_} -> print_case_expr buffer value
|
ECase {value;_} -> print_case_expr buffer value
|
||||||
|
| ECond {value;_} -> print_cond_expr buffer value
|
||||||
| EAnnot {value;_} -> print_annot_expr buffer value
|
| EAnnot {value;_} -> print_annot_expr buffer value
|
||||||
| ELogic e -> print_logic_expr buffer e
|
| ELogic e -> print_logic_expr buffer e
|
||||||
| EArith e -> print_arith_expr buffer e
|
| EArith e -> print_arith_expr buffer e
|
||||||
@ -919,7 +927,22 @@ and pp_instruction buffer ~pad:(_,pc as pad) = function
|
|||||||
pp_node buffer ~pad "SetRemove";
|
pp_node buffer ~pad "SetRemove";
|
||||||
pp_set_remove buffer ~pad value
|
pp_set_remove buffer ~pad value
|
||||||
|
|
||||||
and pp_conditional buffer ~pad:(_,pc) cond =
|
and pp_cond_expr buffer ~pad:(_,pc) (cond: cond_expr) =
|
||||||
|
let () =
|
||||||
|
let _, pc as pad = mk_pad 3 0 pc in
|
||||||
|
pp_node buffer ~pad "<condition>";
|
||||||
|
pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.test in
|
||||||
|
let () =
|
||||||
|
let _, pc as pad = mk_pad 3 1 pc in
|
||||||
|
pp_node buffer ~pad "<true>";
|
||||||
|
pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.ifso in
|
||||||
|
let () =
|
||||||
|
let _, pc as pad = mk_pad 3 2 pc in
|
||||||
|
pp_node buffer ~pad "<false>";
|
||||||
|
pp_expr buffer ~pad:(mk_pad 1 0 pc) cond.ifnot
|
||||||
|
in ()
|
||||||
|
|
||||||
|
and pp_conditional buffer ~pad:(_,pc) (cond: conditional) =
|
||||||
let () =
|
let () =
|
||||||
let _, pc as pad = mk_pad 3 0 pc in
|
let _, pc as pad = mk_pad 3 0 pc in
|
||||||
pp_node buffer ~pad "<condition>";
|
pp_node buffer ~pad "<condition>";
|
||||||
@ -1254,6 +1277,9 @@ and pp_expr buffer ~pad:(_,pc as pad) = function
|
|||||||
ECase {value; _} ->
|
ECase {value; _} ->
|
||||||
pp_node buffer ~pad "ECase";
|
pp_node buffer ~pad "ECase";
|
||||||
pp_case pp_expr buffer ~pad value
|
pp_case pp_expr buffer ~pad value
|
||||||
|
| ECond {value; _} ->
|
||||||
|
pp_node buffer ~pad "ECond";
|
||||||
|
pp_cond_expr buffer ~pad value
|
||||||
| EAnnot {value; _} ->
|
| EAnnot {value; _} ->
|
||||||
pp_node buffer ~pad "EAnnot";
|
pp_node buffer ~pad "EAnnot";
|
||||||
pp_annotated buffer ~pad value
|
pp_annotated buffer ~pad value
|
||||||
|
@ -379,6 +379,28 @@ let rec simpl_expression (t:Raw.expr) : expr result =
|
|||||||
| ELogic l -> simpl_logic_expression l
|
| ELogic l -> simpl_logic_expression l
|
||||||
| EList l -> simpl_list_expression l
|
| EList l -> simpl_list_expression l
|
||||||
| ESet s -> simpl_set_expression s
|
| ESet s -> simpl_set_expression s
|
||||||
|
| ECond _ -> ( failwith "TODO"
|
||||||
|
(*
|
||||||
|
let (c , loc) = r_split c in
|
||||||
|
let%bind expr = simpl_expression c.test in
|
||||||
|
|
||||||
|
let%bind match_true = simpl_expression c.ifso in
|
||||||
|
let%bind match_false = simpl_expression c.ifnot in
|
||||||
|
|
||||||
|
let%bind match_true = match_true None in
|
||||||
|
let%bind match_false = match_false None in
|
||||||
|
return @@ e_matching expr ~loc (Match_bool {match_true; match_false})
|
||||||
|
*)
|
||||||
|
|
||||||
|
(*
|
||||||
|
let%bind lst =
|
||||||
|
bind_list @@
|
||||||
|
[ok (Raw.PTrue Region.ghost, simpl_expression c.ifso);
|
||||||
|
ok (Raw.PFalse Region.ghost, simpl_expression c.ifnot)] in
|
||||||
|
let%bind cases = simpl_cases lst in
|
||||||
|
return @@ e_matching ~loc e cases
|
||||||
|
*)
|
||||||
|
)
|
||||||
| ECase c -> (
|
| ECase c -> (
|
||||||
let (c , loc) = r_split c in
|
let (c , loc) = r_split c in
|
||||||
let%bind e = simpl_expression c.expr in
|
let%bind e = simpl_expression c.expr in
|
||||||
|
Loading…
Reference in New Issue
Block a user