File tree Expand file tree Collapse file tree 1 file changed +16
-4
lines changed Expand file tree Collapse file tree 1 file changed +16
-4
lines changed Original file line number Diff line number Diff line change @@ -580,15 +580,27 @@ defns reduce_exp :: '' ::=
580
580
581
581
582
582
delta |- e1 ~> e1'
583
- ------------------------------------------------------------------ :: ite_step
584
- delta |- if e1 then e2 else e3 ~> if e1' then e2 else e3
583
+ ------------------------------------------------------------------ :: ite_step_cond
584
+ delta |- if e1 then v2 else v3 ~> if e1' then v2 else v3
585
+
586
+ delta |- e2 ~> e2'
587
+ ------------------------------------------------------------------ :: ite_step_then
588
+ delta |- if e1 then e2 else v3 ~> if e1 then e2' else v3
589
+
590
+ delta |- e3 ~> e3'
591
+ ------------------------------------------------------------------ :: ite_step_else
592
+ delta |- if e1 then e2 else e3 ~> if e1 then e2 else e3'
585
593
586
594
----------------------------------------------- :: ite_true
587
- delta |- if true then e2 else e3 ~> e2
595
+ delta |- if true then v2 else v3 ~> v2
588
596
589
597
590
598
------------------------------------------------ :: ite_false
591
- delta |- if false then e2 else e3 ~> e3
599
+ delta |- if false then v2 else v3 ~> v3
600
+
601
+ type(v2) = t'
602
+ ------------------------------------------------------------------ :: ite_unk
603
+ delta |- if unknown[str]:t then v2 else v3 ~> unknown[str]:t'
592
604
593
605
delta |- e2 ~> e2'
594
606
------------------------------------------ :: bop_rhs
You can’t perform that action at this time.
0 commit comments