Commit fa741106 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.24 Thu, 11 Mar 2004 15:19:19 +0100 by jahier

Parent-Version:      1.23
Version-Log:

source/lustreExp.ml:
   use a map indexed by the var name instead of a list of
   variables as the search in such a list is done very often
   during the type checking.

Project-Description: Lurette
parent 18e59b0d
......@@ -8,7 +8,7 @@
(source/constraint.mli 1702 1078751438 c/18_constraint 1.9)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(mlcuddidl/Changes 129 1071844798 d/10_Changes 1.2)
(TODO 4560 1078751438 d/22_TODO 1.40)
(TODO 4716 1079014759 d/22_TODO 1.41)
(share/gen_fake_lutin.sh.in 115 1063786164 g/30_gen_fake_l 1.1)
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(source/fair_bddd.ml 20312 1078751438 g/38_fair_bddd. 1.7)
......@@ -21,7 +21,7 @@
(test/cygwin-scade/lib_pilot.vsw 435 1055926783 f/46_lib_pilot. 1.1)
(mlcuddidl/idd.idl 10595 1034006019 d/1_idd.idl 1.1)
(share/pixmaps/open.xpm 782 1055926783 f/17_open.xpm 1.1)
(source/parse_luc.mli 2810 1078751438 40_parse_env. 1.22)
(source/parse_luc.mli 2807 1079014759 40_parse_env. 1.23)
(polka/C/internal.c 883 1071844798 e/8_internal.c 1.2)
(source/solver.ml 7618 1078751438 39_solver.ml 1.61)
(test/tram/passager.luc 268 1073401581 h/5_passager.l 1.1)
......@@ -52,7 +52,7 @@
(README 3111 1078749975 10_README 1.13)
(source/gen_stubs_scade.ml 9609 1078751438 f/5_gen_stubs_ 1.4)
(test/test9.rif.exp 2407 1078749975 g/17_test9.rif. 1.5)
(source/exp.ml 5891 1078751438 g/47_exp.ml 1.7)
(source/exp.ml 7130 1079014759 g/47_exp.ml 1.8)
(cuddaux/cuddauxMisc.c 13842 1034006019 c/27_cuddauxMis 1.1)
(source/polyhedron.ml 13885 1078751438 d/25_polyhedron 1.18)
(source/Makefile.gen_fake_lucky 699 1076684617 g/9_Makefile.g 1.4)
......@@ -76,7 +76,7 @@
(mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1)
(source/draw.ml 2898 1078751438 f/2_draw.ml 1.4)
(source/prevar.ml 3068 1078751438 d/18_prevar.ml 1.6)
(source/var.mli 3328 1078751438 g/50_var.mli 1.8)
(source/var.mli 3353 1079014759 g/50_var.mli 1.9)
(mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1)
(test/cygwin-scade/C_SQRT.saofd 214 1055926783 g/1_C_SQRT.sao 1.1)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
......@@ -110,7 +110,7 @@
(polka/C/Makefile 7704 1071844798 e/15_Makefile 1.2)
(source/Makefile.gen_fake_lutin 612 1076684617 d/17_Makefile.g 1.5)
(Makefile.common.source 455 1076684617 e/33_Makefile.c 1.11)
(test/test11.rif.exp 4071 1076684617 h/9_test11.rif 1.3)
(test/test11.rif.exp 4071 1079014759 h/9_test11.rif 1.4)
(test/tram/porte.luc 507 1073401581 h/3_porte.luc 1.1)
(test/giro/giro.luc 2755 1033738731 c/6_giro.ima 1.4)
(source/control.ml 4549 1078751438 c/4_control.ml 1.6)
......@@ -118,7 +118,7 @@
(test/cygwin-scade/Pilot.vsw 431 1055926783 f/39_Pilot.vsw 1.1)
(share/pixmaps/open_plus.xpm 787 1055926783 f/16_open_plus. 1.1)
(share/xlurettetop.bat.in 613 1063786164 g/19_xluretteto 1.1)
(source/env_state.ml 16108 1078751438 51_env_state. 1.57)
(source/env_state.ml 16139 1079014759 51_env_state. 1.58)
(test/test8.rif.exp 344 1078749975 g/18_test8.rif. 1.5)
(polka/caml/matrix.idl 6467 1076684617 d/34_matrix.idl 1.4)
(source/fair_bddd.mli 2478 1078751438 g/39_fair_bddd. 1.6)
......@@ -127,7 +127,7 @@
(share/pixmaps/clean-up.xpm 1565 1055926783 f/22_clean-up.x 1.1)
(source/Makefile.lurettetop 546 1076684617 d/14_Makefile.l 1.6)
(test/cygwin-scade/Control.saofd 6690 1055926783 g/3_Control.sa 1.1)
(source/exp.mli 2190 1078751438 g/48_exp.mli 1.4)
(source/exp.mli 3085 1079014759 g/48_exp.mli 1.5)
(test/cygwin-scade/telemetry_validation.saofd 4738 1055926783 f/34_telemetry_ 1.1)
(test/test12.rif.exp 2682 1076684617 h/10_test12.rif 1.3)
(share/lurettetop_sh.in 781 1063786164 g/24_lurettetop 1.1)
......@@ -150,7 +150,7 @@
(mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(source/sim2chro.mli 1532 1078751438 b/23_sim2chro.m 1.12)
(share/lucky_init.csh.in 150 1063786164 e/23_lucky_init 1.8)
(source/lustreExp.ml 21955 1078751438 g/45_lustreExp. 1.6)
(source/lustreExp.ml 25579 1079014759 g/45_lustreExp. 1.7)
(source/gen_fake_lucky.ml 3968 1078751438 g/8_gen_fake_l 1.7)
(polka/C/vector.h 2367 1071844798 d/47_vector.h 1.2)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
......@@ -162,7 +162,7 @@
(share/pixmaps/save.xpm 867 1055926783 f/12_save.xpm 1.1)
(source/solver.mli 1790 1078751438 38_solver.mli 1.24)
(test/passerelle.luc 963 1063786164 b/17_passerelle 1.12)
(source/store.ml 35888 1078751438 b/27_rnumsolver 1.39)
(source/store.ml 36282 1079014759 b/27_rnumsolver 1.40)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(test/sparc-scade/exo1.vsp 2123 1074519403 e/49_exo1.vsp 1.2)
(polka/C/satmat.h 1254 1047029868 d/48_satmat.h 1.1)
......@@ -175,10 +175,10 @@
(mlcuddidl/session.ml 603 1034006019 c/37_session.ml 1.1)
(demo-xlurette/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(share/Makefile.lurette.in 4289 1078749975 b/38_Makefile.l 1.32)
(source/lucky.ml 8866 1078751438 16_env.ml 1.42)
(source/lucky.ml 8867 1079014759 16_env.ml 1.43)
(source/graph.mli 2357 1078751438 13_graph.mli 1.14)
(source/store.mli 3812 1078751438 b/26_rnumsolver 1.26)
(test/time-ossau.res 9445 1078749975 b/49_time.res 1.62)
(test/time-ossau.res 9445 1079014759 b/49_time.res 1.63)
(test/sparc-scade/libmath.saofdm 1378 1055487917 e/45_libmath.sa 1.1)
(Makefile 68 1051024737 d/13_Makefile 1.4)
(share/Makefile.test.in 3891 1073401581 c/25_user-rules 1.12)
......@@ -210,12 +210,12 @@
(source/lexeme.mli 382 1078751438 h/21_lexeme.mli 1.1)
(test/tram/tramway.luc 1015 1073401581 h/2_tramway.lu 1.1)
(source/constraint.ml 3154 1078751438 c/19_constraint 1.11)
(test/structured_type.luc 2308 1076684617 g/32_structured 1.2)
(source/formula_to_bdd.ml 17596 1078751438 g/34_formula_to 1.7)
(test/structured_type.luc 2351 1079014759 g/32_structured 1.3)
(source/formula_to_bdd.ml 17677 1079014759 g/34_formula_to 1.8)
(test/cygwin-scade/counter.saofd 587 1055926783 g/2_counter.sa 1.1)
(test/test7.rif.exp 394 1078749975 g/12_test7.rif. 1.6)
(test/poly-int/poly.lus 72 1073401581 h/7_poly.lus 1.1)
(source/bddd.ml 18278 1076684617 g/36_bddd.ml 1.8)
(source/bddd.ml 18371 1079014759 g/36_bddd.ml 1.9)
(ihm/xlurette/xlurette_glade_interface.ml 81681 1078749975 c/15_xlurette_g 1.26)
(INSTALL 101 1056616700 f/26_INSTALL 1.2)
(test/cygwin-scade/MyConsts.saofd 153 1055926783 f/44_MyConsts.s 1.1)
......@@ -237,12 +237,12 @@
(mlcuddidl/rdd.idl 14806 1034006019 c/42_rdd.idl 1.1)
(test/cygwin-scade/det_mvt_mode_env.luc 283 1063029729 f/31_det_mvt_mo 1.2)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/lustreExp.mli 1948 1078751438 g/46_lustreExp. 1.5)
(source/parse_luc.ml 38390 1078751438 41_parse_env. 1.56)
(source/lustreExp.mli 2022 1079014759 g/46_lustreExp. 1.6)
(source/parse_luc.ml 40563 1079014759 41_parse_env. 1.57)
(OcamlMakefile 21318 1078749975 17_OcamlMakef 1.52)
(polka/caml/polka.ml 5602 1071844798 d/39_polka.ml 1.2)
(source/lurette.mli 752 1078751438 11_lurette.ml 1.17)
(test/time-rey.res 9441 1078749975 h/14_time-rey.r 1.2)
(test/time-rey.res 9441 1079014759 h/14_time-rey.r 1.3)
(share/pixmaps/halt.xpm 511 1055926783 f/18_halt.xpm 1.1)
(share/xlurette_sh.in 779 1063786164 g/20_xlurette_s 1.1)
(polka/C/matrix.c 26957 1071844798 e/7_matrix.c 1.2)
......@@ -292,7 +292,7 @@
(source/lurette_exe.c 220 1050421093 e/27_lurette_ex 1.2)
(share/pixmaps/close.xpm 803 1055926783 f/21_close.xpm 1.1)
(test/time-CHAILLOL.res 8235 1063029729 g/11_time-CHAIL 1.1)
(test/time-ecrins.res 9443 1078749975 d/20_time-ecrin 1.43)
(test/time-ecrins.res 7430 1079014759 d/20_time-ecrin 1.44)
(source/value.mli 1180 1078751438 c/24_value.mli 1.8)
(polka/Makefile.config 1803 1071844798 e/20_Makefile.c 1.6)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
......@@ -322,9 +322,9 @@
(share/set_env_var.in 1071 1078749975 g/23_set_env_va 1.3)
(source/formula_to_bdd.mli 1266 1078751438 g/35_formula_to 1.7)
(polka/Makefile 1646 1076684617 e/21_Makefile 1.2)
(test/dynamic_weight.luc 731 1078749975 g/14_dynamic_we 1.3)
(test/dynamic_weight.luc 705 1079014759 g/14_dynamic_we 1.4)
(test/poly-int/poly.luc 337 1073401581 h/8_poly.luc 1.1)
(source/var.ml 4972 1078751438 g/49_var.ml 1.8)
(source/var.ml 5278 1079014759 g/49_var.ml 1.9)
(test/porte.luc 1014 1063786164 b/16_porte.env 1.12)
(source/gen_stubs_common.mli 1511 1078751438 e/40_gen_stubs_ 1.3)
(test/cygwin-scade/scade.rif.exp 1380 1063029729 g/7_scade.rif. 1.2)
......
sed 's/[ ^t]*$//' file
* Faire un passge sur tous les List.find et tous les List.assoc
pour voir s'ils sont potentiellement appliquées avec des grosses listes.
*********** BUGS
* pb avec les tildes dans les formules !!!
* Bug dans le repertoire HS si dans Makefile.lurette on
positionne CFLAGS à -Oi pour i >= 1. Le bug ne se produit
que sur les machines linux possedant gcc 3.
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 1 23)
(Parent-Version lurette 1 22)
(Project-Version lurette 1 24)
(Parent-Version lurette 1 23)
(Version-Log "
source/*.ml*:
perform a sed 's/[ ]*$//' on all files to remove
trailing space.
source/lustreExp.ml:
use a map indexed by the var name instead of a list of
variables as the search in such a list is done very often
during the type checking.
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 08 Mar 2004 14:10:38 +0100")
(Checkin-Time "Thu, 11 Mar 2004 15:19:19 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -41,16 +42,16 @@ source/*.ml*:
(source/graph.ml (lurette/14_graph.ml 1.12 644))
(source/lucky.mli (lurette/15_env.mli 1.25 644))
(source/lucky.ml (lurette/16_env.ml 1.42 644))
(source/lucky.ml (lurette/16_env.ml 1.43 644))
(source/util.ml (lurette/35_util.ml 1.66 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.7 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.8 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.7 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.7 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.6 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.8 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.9 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.10 644))
(source/solver.mli (lurette/38_solver.mli 1.24 644))
......@@ -60,10 +61,10 @@ source/*.ml*:
(source/polyhedron.mli (lurette/d/26_polyhedron 1.10 644))
(source/store.mli (lurette/b/26_rnumsolver 1.26 644))
(source/store.ml (lurette/b/27_rnumsolver 1.39 644))
(source/store.ml (lurette/b/27_rnumsolver 1.40 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.22 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.56 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.23 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.57 644))
(source/show_env.mli (lurette/42_show_env.m 1.12 644))
(source/show_env.ml (lurette/43_show_env.m 1.21 644))
......@@ -72,7 +73,7 @@ source/*.ml*:
(source/print.ml (lurette/47_print.ml 1.27 644))
(source/env_state.mli (lurette/50_env_state. 1.40 644))
(source/env_state.ml (lurette/51_env_state. 1.57 644))
(source/env_state.ml (lurette/51_env_state. 1.58 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.12 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.25 644))
......@@ -172,7 +173,7 @@ source/*.ml*:
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.2 744))
(TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.40 644))
(TODO (lurette/d/22_TODO 1.41 644))
(share/lucky_init.csh.in (lurette/e/23_lucky_init 1.8 644))
(share/lucky_init.sh.in (lurette/e/24_lucky_init 1.12 644))
......@@ -180,10 +181,10 @@ source/*.ml*:
(share/plot (lurette/e/35_plot 1.9 744))
(test/time-rey.exp (lurette/h/13_time-rey.e 1.3 644))
(test/time-rey.res (lurette/h/14_time-rey.r 1.2 644))
(test/time-rey.res (lurette/h/14_time-rey.r 1.3 644))
(test/time-ossau.exp (lurette/b/48_time.exp 1.59 644))
(test/time-ossau.res (lurette/b/49_time.res 1.62 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.43 644))
(test/time-ossau.res (lurette/b/49_time.res 1.63 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.44 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.43 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.20 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.20 644))
......@@ -276,7 +277,7 @@ source/*.ml*:
(test/test7.rif.exp (lurette/g/12_test7.rif. 1.6 644))
(test/infinite_weight.luc (lurette/g/13_infinite_w 1.2 644))
(test/dynamic_weight.luc (lurette/g/14_dynamic_we 1.3 644))
(test/dynamic_weight.luc (lurette/g/14_dynamic_we 1.4 644))
(test/window.luc (lurette/g/15_window.luc 1.1 644))
(test/test10.rif.exp (lurette/g/16_test10.rif 1.5 644))
(test/test9.rif.exp (lurette/g/17_test9.rif. 1.5 644))
......@@ -416,7 +417,7 @@ source/*.ml*:
;; Files added by populate at Wed, 17 Sep 2003 09:47:12 +0200,
;; to version 1.1(w), by jahier:
(test/structured_type.luc (lurette/g/32_structured 1.2 644))
(test/structured_type.luc (lurette/g/32_structured 1.3 644))
;; Files added by populate at Wed, 17 Sep 2003 09:49:00 +0200,
;; to version 1.1(w), by jahier:
......@@ -448,32 +449,32 @@ source/*.ml*:
;; Files added by populate at Thu, 13 Nov 2003 16:59:39 +0100,
;; to version 1.8(w), by jahier:
(source/lustreExp.ml (lurette/g/45_lustreExp. 1.6 644))
(source/lustreExp.ml (lurette/g/45_lustreExp. 1.7 644))
;; Files added by populate at Thu, 13 Nov 2003 16:59:41 +0100,
;; to version 1.8(w), by jahier:
(source/lustreExp.mli (lurette/g/46_lustreExp. 1.5 644))
(source/lustreExp.mli (lurette/g/46_lustreExp. 1.6 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:47 +0100,
;; to version 1.8(w), by jahier:
(source/exp.ml (lurette/g/47_exp.ml 1.7 644))
(source/exp.ml (lurette/g/47_exp.ml 1.8 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:49 +0100,
;; to version 1.8(w), by jahier:
(source/exp.mli (lurette/g/48_exp.mli 1.4 644))
(source/exp.mli (lurette/g/48_exp.mli 1.5 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:53 +0100,
;; to version 1.8(w), by jahier:
(source/var.ml (lurette/g/49_var.ml 1.8 644))
(source/var.ml (lurette/g/49_var.ml 1.9 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:55 +0100,
;; to version 1.8(w), by jahier:
(source/var.mli (lurette/g/50_var.mli 1.8 644))
(source/var.mli (lurette/g/50_var.mli 1.9 644))
;; Files added by populate at Wed, 26 Nov 2003 08:47:27 +0100,
;; to version 1.10(w), by jahier:
......@@ -500,7 +501,7 @@ source/*.ml*:
;; Files added by populate at Tue, 06 Jan 2004 15:35:22 +0100,
;; to version 1.15(w), by jahier:
(test/test11.rif.exp (lurette/h/9_test11.rif 1.3 644))
(test/test11.rif.exp (lurette/h/9_test11.rif 1.4 644))
;; Files added by populate at Tue, 06 Jan 2004 15:35:25 +0100,
;; to version 1.15(w), by jahier:
......
......@@ -254,8 +254,9 @@ let (toss_up_one_var_index: Var.env_in -> Env_state.t -> var_idx ->
match cstr with
Bv(v) -> (
match (Var.default v) with
Some (Formu f) ->
| Some (Formu f) ->
let bdd = Formula_to_bdd.f input state f in
(* print_string ("\n give a default to " ^ (Var.name v) ^ "\n"); flush stdout; *)
if Bdd.is_false bdd then Some((Var.name v), B false)
else if Bdd.is_true bdd then Some((Var.name v), B true)
else
......@@ -274,8 +275,8 @@ let (toss_up_one_var_index: Var.env_in -> Env_state.t -> var_idx ->
| _ -> None
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.t -> Var.subst list * Store.t -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p) =
let rec (draw_in_bdd_rec: Var.env_in -> Env_state.t -> Var.subst list * Store.t
-> Bdd.t -> Bdd.t -> Var.subst list * Store.t' * Store.p) =
fun input state (sl, store) bdd comb ->
(** Returns [sl] appended to a draw of all the boolean variables
bigger than the topvar of [bdd] according to the ordering
......
......@@ -23,13 +23,13 @@ type node_info = {
}
type static_state_fields = {
bool_vars_to_gen : Exp.var list list ;
num_vars_to_gen : Exp.var list list ;
bool_vars_to_gen : Exp.var list list;
num_vars_to_gen : Exp.var list list;
in_vars : Exp.var list;
out_vars : Exp.var list;
loc_vars : Exp.var list;
memories_names : string list ;
output_var_names : Var.name list list ;
output_var_names : Var.name list list;
node : (node, node_info) Hashtbl.t;
graph : (node, arc_info) Graph.t
}
......@@ -72,7 +72,10 @@ let (merge_var : Exp.var list -> Exp.var list -> Exp.var list) =
- ditto for default and init
*)
fun vl1 vl2 ->
(* let _ = print_string ("merge_var " ^ (string_of_int (List.length vl1)) ^ " " ^(string_of_int (List.length vl2)) ^ "\n") ; flush stdout in *)
(* let _ = print_string ("merge_var " ^
(string_of_int (List.length vl1)) ^ " "
^(string_of_int (List.length vl2)) ^ "\n") ;
flush stdout in *)
let add_var vl1 var2 =
(* add [var2] into the list [vl1]. If one of the variables of
vl1 have the same name as var2, then merge the 2 as follows:
......@@ -244,7 +247,9 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
and current_nodes0 = state.d.current_nodes
in
let ovnl_current = List.map (Var.name) (fst list_out) in
(* let ovnl_current = List.map (Var.name) (fst list_out) in *)
let ovnl_current = StringMap.fold (fun vn var acc -> vn::acc) (fst list_out) [] in
(* nb: we only sort the list of list of autamata
according to outputs, as locals are supposed to be all different.
*)
......@@ -256,33 +261,39 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
In other words, we build the partition of independant automata
here step by step (on the fly).
*)
let ovnll = list_insert n (Util.merge) (Util.rm_dup ovnl_current) ovnll0 in
let ovnll = list_insert n (Util.merge) ovnl_current ovnll0 in
let (bvl_current0, nvl_current0) =
let (bvl_current, nvl_current) =
(* split the Boolean and the numeric vars *)
List.partition
(fun var -> Var.typ var = Type.BoolT)
(rev_append (fst list_out) (fst list_loc))
in
let (bvl_current1, nvl_current1) =
(*
Aliases should not really be generated: they are inlined
when the other variables have been computed.
*)
(List.filter (fun var -> Var.alias var = None) bvl_current0),
(List.filter (fun var -> Var.alias var = None) nvl_current0)
let split_bool_and_num var_tbl =
(StringMap.fold
(fun _vn var (bl, nl) ->
if
Var.alias var <> None
then
(*
Aliases are not really to be generated: they are
simply inlined once the other variables have been
computed.
*)
(bl, nl)
else if
Var.typ var = Type.BoolT
then
(var::bl, nl)
else
(bl, var::nl)
)
var_tbl
([], [])
)
in
let (bvl_out, nvl_out) = split_bool_and_num (fst list_out)
and (bvl_loc, nvl_loc) = split_bool_and_num (fst list_loc)
in
(rev_append bvl_out bvl_loc), (rev_append nvl_out nvl_loc)
in
(* in order to remove mutiple occurence of the same variable
in an automaton.
XXX Should i abort instead ??? I should, definitely
*)
(* let bvl_current = (merge_var [] bvl_current1) *)
(* and nvl_current = (merge_var [] nvl_current1) in *)
let bvl_current = (bvl_current1)
and nvl_current = (nvl_current1) in
let bvll = list_insert n merge_var bvl_current bvll0 in
let nvll = list_insert n merge_var nvl_current nvll0 in
......@@ -383,13 +394,15 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
)
in
let string_map_to_list map_tbl =
StringMap.fold (fun vn var acc -> var::acc) map_tbl []
in
let ssf = {
bool_vars_to_gen = bvll;
num_vars_to_gen = nvll;
in_vars = merge_var state.s.in_vars (fst list_in);
out_vars = merge_var state.s.out_vars (fst list_out);
loc_vars = rev_append state.s.loc_vars (fst list_loc);
in_vars = merge_var state.s.in_vars (string_map_to_list (fst list_in));
out_vars = merge_var state.s.out_vars (string_map_to_list (fst list_out));
loc_vars = rev_append state.s.loc_vars (string_map_to_list (fst list_loc));
memories_names = mnl;
output_var_names = ovnll;
node = node_tbl;
......@@ -401,9 +414,6 @@ let (read_env_state_one_automaton : t -> Parse_luc.automata -> t) =
input = [];
verbose = state.d.verbose
}
in
let all_vars_current =
rev_append (fst list_in) (rev_append (fst list_out) (fst list_loc))
in
{ s = ssf ; d = dsf }
......
......@@ -16,7 +16,7 @@ open Value
type t =
Formu of formula
| Numer of num
| Liste of simple list
| Liste of simple_tbl
(** struct and arrays are flattened in such a list *)
and simple =
......@@ -60,13 +60,69 @@ and formula =
| InfEq of num * num (* <= *)
and
var = t Var.t
and simple_tbl
= simple Util.StringMap.t
type var_tbl = var Util.StringMap.t
let (add_value : string -> simple -> simple_tbl -> simple_tbl) =
fun str exp tbl ->
Util.StringMap.add str exp tbl
let (add_var : string -> var -> var_tbl -> var_tbl) =
fun str var tbl ->
Util.StringMap.add str var tbl
let (empty_var_tbl : var Util.StringMap.t) =
Util.StringMap.empty
let (empty_simple_tbl : simple Util.StringMap.t) =
Util.StringMap.empty
let (remove_prefix : string -> string -> string) =
fun prefix vn0 ->
let l = String.length prefix in
let l2 = String.length vn0 in
assert (String.sub vn0 0 l = prefix);
String.sub vn0 l (l2-l)
let _ = assert (
(remove_prefix "s" "s.field1[1]" = ".field1[1]"))
let _ = assert (
(remove_prefix "s.field1" "s.field1[1]" = "[1]"))
let _ = assert (
(remove_prefix "s" "s[23].field[1]" = "[23].field[1]"))
let (remove_var_name : string -> string) =
fun vn0 ->
try
let index =
Str.search_forward (Str.regexp "\\.\\|\\[") vn0 0
in
String.sub vn0 index ((String.length vn0) - index)
with _ -> vn0
let _ = assert (
(remove_var_name "s.field[1]" = ".field[1]"))
let _ = assert (
(remove_var_name "s[23].field[1]" = "[23].field[1]"))
(****************************************************************************)
......@@ -185,6 +241,8 @@ let (to_simple : t -> simple) =
| Liste _ -> assert false
open Util
(* exported *)
let (to_string : t -> string) =
fun e ->
......@@ -192,10 +250,10 @@ let (to_string : t -> string) =
Formu f -> formula_to_string f
| Numer e -> num_to_string e
| Liste l ->
(List.fold_left
(fun acc e -> acc ^ " " ^ simple_to_string e)
""
(StringMap.fold
(fun _ e acc -> acc ^ " " ^ simple_to_string e)
l
""
)
let var_to_string var =
......
......@@ -10,11 +10,10 @@
(** Lucky Boolean and numeric expressions. *)
type t =
Formu of formula
| Numer of num
| Liste of simple list
| Liste of simple_tbl
(** struct and arrays are flattened in such a list *)
and formula =
......@@ -62,9 +61,33 @@ and simple =
Fo of formula
| Nu of num
and simple_tbl
= simple Util.StringMap.t
(* This table, used to represent the flatten list of atomic values
of a structured type expression. It is indexed b the string
that would be used to access the corresponding element.
For exemple, a variable of type {f1:int^3 ; f2:bool} will represented
by a map indexed by the strings ".f1[0]", ".f1[1]", ".f1[2]", and ".f2".
*)
(* Table of vars indexed by name *)
type var_tbl = var Util.StringMap.t
val add_value : string -> simple -> simple_tbl -> simple_tbl
val add_var : string -> var -> var_tbl -> var_tbl
val empty_var_tbl : var Util.StringMap.t
val empty_simple_tbl : simple Util.StringMap.t
(** remove from a string everything that is before the
first "." or the first "[". This is useful to go to
var_tbl indexes (which depends on the var name) to
simple_tbl indexes (which depend only on the type).
*)
val remove_prefix : string -> string -> string
(**/**)
......@@ -98,3 +121,5 @@ val num_to_string : num -> string
val to_string : t -> string
val print_var : var -> unit
val remove_var_name : string -> string
......@@ -58,7 +58,10 @@ let rec (lookup: Var.env_in -> Env_state.t -> Exp.var -> Value.t option) =
| Some (Numer (Fvar vf)) -> lookup input state vf
| Some (Formu True) -> Some (B true)
| Some (Formu False) -> Some (B false)
| Some (Liste [Nu (Ival i)]) -> Some (N (I i))
| Some (Liste _) ->
assert false (* XXX not sure ...*)
(* | Some (Liste [Nu (Ival i)]) -> *)
(* Some (N (I i)) *)
| Some _ ->
(* Structured expression ougth to have been
......
......@@ -295,7 +295,7 @@ let (env_step : step_mode -> env_in -> Env_state.t -> Env_state.t * solution) =
in
let new_state = { d = new_state_dyn ; s = state.s } in
some_al := None;
(* Clean-up cached info that depend on pre or inputs *)
(* Clean-up cached info that depends on pre or inputs *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
......
This diff is collapsed.
......@@ -50,14 +50,18 @@ type t =
| Le_struct_access of Lexeme.t * t * t
(** Output of the lustre expression parser *)
type vut = (Var.name * (Type.structured * Exp.var list))
(* type vut = (Type.structured * Exp.var_tbl) Util.StringMap.t *)
type vut = (Var.name * (Type.structured * Exp.var_tbl))
(** If the var name is a struct, this field ougth to contain
the corresponding list of leaves variables *)
the corresponding list of leaves atomic variables *)
type typedef = (string * Type.t)
val do_type : string -> Exp.var list -> vut list -> typedef list -> t ->
val do_type : string -> Exp.var_tbl -> vut list -> typedef list -> t ->
Exp.t * Type.t
(** Type lustre expression *)
......
This diff is collapsed.
......@@ -107,9 +107,9 @@ type lucky_arc = Arc of node * arc_info * node
type automata = {