Revision ae08b9fc
Added by Pierre-Loïc Garoche about 5 years ago
| src/corelang.ml | ||
|---|---|---|
| 1408 | 1408 |
| _ -> assert false (* no array, array access, power or merge/when yet *) |
| 1409 | 1409 |
in |
| 1410 | 1410 |
mkexpr e.expr_loc desc |
| 1411 |
|
|
| 1411 |
|
|
| 1412 |
|
|
| 1413 |
|
|
| 1414 |
let mk_eq l e1 e2 = |
|
| 1415 |
mkpredef_call l "=" [e1; e2] |
|
| 1416 |
|
|
| 1412 | 1417 |
(* Local Variables: *) |
| 1413 | 1418 |
(* compile-command:"make -C .." *) |
| 1414 | 1419 |
(* End: *) |
| src/corelang.mli | ||
|---|---|---|
| 200 | 200 |
val push_negations: ?neg:bool -> expr -> expr |
| 201 | 201 |
|
| 202 | 202 |
val add_pre_expr: ident list -> expr -> expr |
| 203 |
(* Local Variables: *) |
|
| 203 |
|
|
| 204 |
val mk_eq: Location.t -> expr -> expr -> expr |
|
| 205 |
(* Local Variables: *) |
|
| 204 | 206 |
(* compile-command:"make -C .." *) |
| 205 | 207 |
(* End: *) |
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 549 | 549 |
) ([], true) gel2 |
| 550 | 550 |
in |
| 551 | 551 |
not all_invalid, l |
| 552 |
|
|
| 553 |
(* Rewrite the expression expr, replacing any occurence of a variable |
|
| 552 |
|
|
| 553 |
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as |
|
| 554 |
[gl1, e1=id; gl2, e2=id; ...] *) |
|
| 555 |
let mk_ge_eq_id ge id = |
|
| 556 |
List.map |
|
| 557 |
(fun (gl, g_e) -> |
|
| 558 |
gl, |
|
| 559 |
if id = "true" then |
|
| 560 |
g_e |
|
| 561 |
else |
|
| 562 |
match g_e with |
|
| 563 |
| Expr g_e -> |
|
| 564 |
if id = "false" then |
|
| 565 |
Expr (Corelang.push_negations ~neg:true g_e) |
|
| 566 |
else |
|
| 567 |
let loc = g_e.expr_loc in |
|
| 568 |
Expr(Corelang.mk_eq loc |
|
| 569 |
g_e |
|
| 570 |
(Corelang.expr_of_ident id loc)) |
|
| 571 |
| _ -> assert false |
|
| 572 |
) ge |
|
| 573 |
|
|
| 574 |
(* Rewrite the expression expr, replacing any occurence of a variable |
|
| 554 | 575 |
by its definition. |
| 555 |
*) |
|
| 576 |
*)
|
|
| 556 | 577 |
let rec rewrite defs expr : elem_guarded_expr list = |
| 557 | 578 |
let rewrite = rewrite defs in |
| 558 | 579 |
let res = |
| ... | ... | |
| 578 | 599 |
let ok_else, g_else = concatenate_ge g false e2 in |
| 579 | 600 |
(if ok_then then g_then else [])@ |
| 580 | 601 |
(if ok_else then g_else else []) |
| 581 |
| Expr_merge (g, branches) -> |
|
| 582 |
assert false (* TODO: deal with merges *) |
|
| 583 |
|
|
| 584 |
| Expr_when (e, _, _) -> rewrite e |
|
| 602 |
| Expr_merge (g_id, branches) -> |
|
| 603 |
if Hashtbl.mem defs g_id then |
|
| 604 |
let g = Hashtbl.find defs g_id in |
|
| 605 |
(* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *) |
|
| 606 |
List.fold_left (fun accu (id, e) -> |
|
| 607 |
let g = mk_ge_eq_id g id in |
|
| 608 |
let e = rewrite e in |
|
| 609 |
let ok, g_eq_id = concatenate_ge g true e in |
|
| 610 |
if ok then g_eq_id@accu else accu |
|
| 611 |
) [] branches |
|
| 612 |
else |
|
| 613 |
assert false (* g should be defined already *) |
|
| 614 |
| Expr_when (e, id, l) -> |
|
| 615 |
let e = rewrite e in |
|
| 616 |
let id_def = Hashtbl.find defs id in |
|
| 617 |
let clock = mk_ge_eq_id id_def l in |
|
| 618 |
let ok, new_ge = concatenate_ge clock true e in |
|
| 619 |
if ok then new_ge else [] |
|
| 585 | 620 |
| Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *) |
| 586 | 621 |
| Expr_tuple el -> |
| 587 | 622 |
(* Each expr is associated to its flatten guarded expr list *) |
| ... | ... | |
| 628 | 663 |
* pp_guard_expr) res; *) |
| 629 | 664 |
res |
| 630 | 665 |
and add_def defs vid expr = |
| 666 |
(* Format.eprintf "Add_def: %s = %a@." |
|
| 667 |
* vid |
|
| 668 |
* Printers.pp_expr expr; *) |
|
| 631 | 669 |
let vid_defs = rewrite defs expr in |
| 670 |
(* Format.eprintf "-> @[<v 0>%a@]@." |
|
| 671 |
* (Utils.fprintf_list ~sep:"@ " |
|
| 672 |
* (pp_guard_expr pp_elem)) vid_defs; *) |
|
| 632 | 673 |
(* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@." |
| 633 | 674 |
* vid |
| 634 | 675 |
* Printers.pp_expr expr |
| ... | ... | |
| 740 | 781 |
((expr * bool) list * (ident * expr) list ) list = |
| 741 | 782 |
if !seal_debug then |
| 742 | 783 |
report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@." |
| 743 |
(Utils.fprintf_list ~sep:",@ " |
|
| 744 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
|
| 745 |
id |
|
| 746 |
(pp_mdefs pp_elem) gel)) |
|
| 747 |
mem_defs); |
|
| 784 |
pp_all_defs |
|
| 785 |
mem_defs); |
|
| 748 | 786 |
(* if all mem_defs have empty guards, we are done, return prefix, |
| 749 | 787 |
mem_defs expr. |
| 750 | 788 |
|
| ... | ... | |
| 755 | 793 |
if List.for_all (fun (m,mdefs) -> |
| 756 | 794 |
(* All defs are unguarded *) |
| 757 | 795 |
match mdefs with |
| 758 |
| [[], _] -> true |
|
| 796 |
| [[], _] -> true (* Regular unguarded expression *) |
|
| 797 |
| [] -> true (* A unbalanced definition of the memory. Here |
|
| 798 |
we have m_{k+1} -> m_k *)
|
|
| 759 | 799 |
| _ -> false |
| 760 | 800 |
) mem_defs |
| 761 | 801 |
then |
| ... | ... | |
| 769 | 809 |
| _ -> assert false (* No IsInit expression *) |
| 770 | 810 |
in |
| 771 | 811 |
m,e |
| 812 |
| [] -> m, Corelang.expr_of_ident m Location.dummy_loc |
|
| 772 | 813 |
| _ -> assert false |
| 773 | 814 |
) mem_defs] |
| 774 | 815 |
else |
| 775 | 816 |
(* Picking a guard *) |
| 776 | 817 |
let elem_opt : expr option = pick_guard mem_defs in |
| 777 | 818 |
match elem_opt with |
| 778 |
None -> assert false (* Otherwise the first case should have matched *) |
|
| 819 |
None -> ( |
|
| 820 |
Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs; |
|
| 821 |
assert false (* Otherwise the first case should have matched *) |
|
| 822 |
) |
|
| 779 | 823 |
| Some elem -> ( |
| 780 | 824 |
report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem); |
| 781 | 825 |
let pos, neg = |
| src/tools/seal/seal_utils.ml | ||
|---|---|---|
| 63 | 63 |
| Some gl -> |
| 64 | 64 |
Format.fprintf fmt "[@[%a@]] -> (%a)@ " |
| 65 | 65 |
Printers.pp_expr gl pp_up up) sw |
| 66 |
|
|
| 66 |
let pp_all_defs = |
|
| 67 |
(Utils.fprintf_list ~sep:",@ " |
|
| 68 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
|
| 69 |
id |
|
| 70 |
(pp_mdefs pp_elem) gel)) |
|
| 67 | 71 |
module UpMap = |
| 68 |
struct |
|
| 69 |
include Map.Make ( |
|
| 70 |
struct |
|
| 71 |
type t = (ident * expr) list |
|
| 72 |
let compare l1 l2 = |
|
| 73 |
let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in |
|
| 74 |
compare (proj l1) (proj l2) |
|
| 75 |
end) |
|
| 76 |
let pp = pp_up |
|
| 77 |
end |
|
| 72 |
struct
|
|
| 73 |
include Map.Make (
|
|
| 74 |
struct
|
|
| 75 |
type t = (ident * expr) list
|
|
| 76 |
let compare l1 l2 =
|
|
| 77 |
let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
|
|
| 78 |
compare (proj l1) (proj l2)
|
|
| 79 |
end)
|
|
| 80 |
let pp = pp_up
|
|
| 81 |
end
|
|
| 78 | 82 |
|
| 79 | 83 |
module Guards = struct |
| 80 | 84 |
include Set.Make ( |
| ... | ... | |
| 88 | 92 |
let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s) |
| 89 | 93 |
end |
| 90 | 94 |
|
| 91 |
|
|
| 92 |
|
|
| 95 |
|
|
| src/tools/zustre/zustre_common.ml | ||
|---|---|---|
| 54 | 54 |
|
| 55 | 55 |
let get_const_sort = Hashtbl.find const_sorts |
| 56 | 56 |
let get_sort_elems = Hashtbl.find sort_elems |
| 57 |
let get_tag_sort = Hashtbl.find const_tags
|
|
| 57 |
let get_tag_sort id = try Hashtbl.find const_tags id with _ -> Format.eprintf "Unable to find sort for tag=%s@." id; assert false
|
|
| 58 | 58 |
|
| 59 | 59 |
|
| 60 | 60 |
|
| src/types.ml | ||
|---|---|---|
| 168 | 168 |
fprintf fmt "_%s" (name_of_type ty.tid) |
| 169 | 169 |
| Tbasic t -> pp_basic fmt t |
| 170 | 170 |
| Tclock t -> |
| 171 |
fprintf fmt "%a clock" print_ty t
|
|
| 171 |
fprintf fmt "%a%s" print_ty t (if !Options.kind2_print then "" else " clock")
|
|
| 172 | 172 |
| Tstatic (d, t) -> |
| 173 | 173 |
fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t |
| 174 | 174 |
| Tconst t -> |
| ... | ... | |
| 204 | 204 |
end |
| 205 | 205 |
| Tbasic t -> BasicT.pp fmt t |
| 206 | 206 |
| Tclock t -> |
| 207 |
fprintf fmt "%a clock" print_node_ty t
|
|
| 207 |
fprintf fmt "%a%s" print_node_ty t (if !Options.kind2_print then "" else " clock")
|
|
| 208 | 208 |
| Tstatic (_, t) -> |
| 209 | 209 |
fprintf fmt "%a" print_node_ty t |
| 210 | 210 |
| Tconst t -> |
Also available in: Unified diff
[seal] delt with Merge and when
[printer] more kind2 syntax