Commit 21390374 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.13 Fri, 12 Dec 2003 14:21:26 +0100 by jahier

Parent-Version:      1.12
Version-Log:

aesthetic changes in mli files so that
the automatically generated doc looks ok.

Project-Description: Lurette
parent c3ab83b6
This diff is collapsed.
...@@ -5,13 +5,13 @@ ...@@ -5,13 +5,13 @@
# Where to find libs # Where to find libs
INCDIRS = $(HOME)/$(HOST_TYPE)/lib # INCDIRS = $(HOME)/$(HOST_TYPE)/lib
LIBDIRS = $(HOME)/$(HOST_TYPE)/lib # LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
# INCDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib \ INCDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib \
# $(SCADE_INSTALL_DIR)/SimulinkGateway/include \ $(SCADE_INSTALL_DIR)/SimulinkGateway/include \
# $(SCADE_INSTALL_DIR)/include $(SCADE_INSTALL_DIR)/include
# LIBDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib LIBDIRS = $(HOME)/$(HOST_TYPE)/lib $(SCADE_INSTALL_DIR)/lib
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
......
* faire un passage pour verifier que je ne cree pas de hash tbl que
n'utilise plus apres, auquel cas
-> soit je nettoie
-> soit j'utilise des map.
* essayer les versions precedentes de scade sous sparcs avec les programmes
de HS
*********** BUGS *********** BUGS
......
...@@ -57,7 +57,7 @@ ...@@ -57,7 +57,7 @@
\newenvironment{ocamldocdescription} \newenvironment{ocamldocdescription}
{ %\color{green3} { %\color{green3}
\list{}{\rightmargin0pt \topsep0pt}\raggedright\item\relax} \list{}{\rightmargin0pt \topsep0pt}\item\relax}
{\endlist\medskip} {\endlist\medskip}
\newenvironment{ocamldoccomment} \newenvironment{ocamldoccomment}
......
...@@ -51,7 +51,7 @@ all: opt cp ...@@ -51,7 +51,7 @@ all: opt cp
cp: cp:
ifeq ($(HOST_TYPE),cygwin) ifeq ($(HOST_TYPE),cygwin)
cp xlurette_exe.exe $(BIN_INSTALL_DIR) cp xlurette_exe.exe /cygdrive/u/cygwin/bin
else else
cp xlurette_exe $(BIN_INSTALL_DIR) cp xlurette_exe $(BIN_INSTALL_DIR)
endif endif
......
...@@ -1025,7 +1025,9 @@ class customized_callbacks = object(self) ...@@ -1025,7 +1025,9 @@ class customized_callbacks = object(self)
self#read_rif_files () self#read_rif_files ()
method on_env_name_entry_changed () =
self#read_env_files ()
method save_parameters () = method save_parameters () =
let msg = "Saving current parameters in .lurette_rc \n" let msg = "Saving current parameters in .lurette_rc \n"
and cmds = self#get_all_cmds () and cmds = self#get_all_cmds ()
......
;; -*- Prcs -*- ;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3) (Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette") (Project-Description "Lurette")
(Project-Version lurette 1 12) (Project-Version lurette 1 13)
(Parent-Version lurette 1 11) (Parent-Version lurette 1 12)
(Version-Log " (Version-Log "
Various fixes in the C scade parsing. aesthetic changes in mli files so that
the automatically generated doc looks ok.
") ")
(New-Version-Log "" (New-Version-Log ""
) )
(Checkin-Time "Tue, 09 Dec 2003 15:44:28 +0100") (Checkin-Time "Fri, 12 Dec 2003 14:21:26 +0100")
(Checkin-Login jahier) (Checkin-Login jahier)
(Populate-Ignore ()) (Populate-Ignore ())
(Project-Keywords) (Project-Keywords)
...@@ -27,8 +28,8 @@ Various fixes in the C scade parsing. ...@@ -27,8 +28,8 @@ Various fixes in the C scade parsing.
(source/command_line_luc_exe.mli (lurette/b/34_command_li 1.14 644)) (source/command_line_luc_exe.mli (lurette/b/34_command_li 1.14 644))
;; Sources files for lurette only ;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.14 644)) (source/lurette.mli (lurette/11_lurette.ml 1.15 644))
(source/lurette.ml (lurette/12_lurette.ml 1.80 644)) (source/lurette.ml (lurette/12_lurette.ml 1.81 644))
(source/command_line.ml (lurette/b/20_command_li 1.17 644)) (source/command_line.ml (lurette/b/20_command_li 1.17 644))
(source/command_line.mli (lurette/b/21_command_li 1.14 644)) (source/command_line.mli (lurette/b/21_command_li 1.14 644))
...@@ -37,30 +38,30 @@ Various fixes in the C scade parsing. ...@@ -37,30 +38,30 @@ Various fixes in the C scade parsing.
(source/graph.mli (lurette/13_graph.mli 1.12 644)) (source/graph.mli (lurette/13_graph.mli 1.12 644))
(source/graph.ml (lurette/14_graph.ml 1.10 644)) (source/graph.ml (lurette/14_graph.ml 1.10 644))
(source/lucky.mli (lurette/15_env.mli 1.22 644)) (source/lucky.mli (lurette/15_env.mli 1.23 644))
(source/lucky.ml (lurette/16_env.ml 1.36 644)) (source/lucky.ml (lurette/16_env.ml 1.37 644))
(source/util.ml (lurette/35_util.ml 1.60 644)) (source/util.ml (lurette/35_util.ml 1.60 644))
(source/formula_to_bdd.ml (lurette/g/34_formula_to 1.4 644)) (source/formula_to_bdd.ml (lurette/g/34_formula_to 1.4 644))
(source/formula_to_bdd.mli (lurette/g/35_formula_to 1.5 644)) (source/formula_to_bdd.mli (lurette/g/35_formula_to 1.6 644))
(source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.5 644)) (source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.5 644))
(source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.5 644)) (source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.5 644))
(source/bddd.ml (lurette/g/36_bddd.ml 1.7 644)) (source/bddd.ml (lurette/g/36_bddd.ml 1.7 644))
(source/bddd.mli (lurette/g/37_bddd.mli 1.7 644)) (source/bddd.mli (lurette/g/37_bddd.mli 1.8 644))
(source/solver.mli (lurette/38_solver.mli 1.21 644)) (source/solver.mli (lurette/38_solver.mli 1.22 644))
(source/solver.ml (lurette/39_solver.ml 1.59 644)) (source/solver.ml (lurette/39_solver.ml 1.60 644))
(source/polyhedron.ml (lurette/d/25_polyhedron 1.12 644)) (source/polyhedron.ml (lurette/d/25_polyhedron 1.13 644))
(source/polyhedron.mli (lurette/d/26_polyhedron 1.6 644)) (source/polyhedron.mli (lurette/d/26_polyhedron 1.7 644))
(source/store.mli (lurette/b/26_rnumsolver 1.23 644)) (source/store.mli (lurette/b/26_rnumsolver 1.24 644))
(source/store.ml (lurette/b/27_rnumsolver 1.32 644)) (source/store.ml (lurette/b/27_rnumsolver 1.33 644))
(source/parse_luc.mli (lurette/40_parse_env. 1.18 644)) (source/parse_luc.mli (lurette/40_parse_env. 1.19 644))
(source/parse_luc.ml (lurette/41_parse_env. 1.50 644)) (source/parse_luc.ml (lurette/41_parse_env. 1.51 644))
(source/show_env.mli (lurette/42_show_env.m 1.11 644)) (source/show_env.mli (lurette/42_show_env.m 1.11 644))
(source/show_env.ml (lurette/43_show_env.m 1.20 644)) (source/show_env.ml (lurette/43_show_env.m 1.20 644))
...@@ -68,11 +69,11 @@ Various fixes in the C scade parsing. ...@@ -68,11 +69,11 @@ Various fixes in the C scade parsing.
(source/print.mli (lurette/46_print.mli 1.14 644)) (source/print.mli (lurette/46_print.mli 1.14 644))
(source/print.ml (lurette/47_print.ml 1.25 644)) (source/print.ml (lurette/47_print.ml 1.25 644))
(source/env_state.mli (lurette/50_env_state. 1.37 644)) (source/env_state.mli (lurette/50_env_state. 1.38 644))
(source/env_state.ml (lurette/51_env_state. 1.52 644)) (source/env_state.ml (lurette/51_env_state. 1.52 644))
(source/run_aut.mli (lurette/b/46_automata.m 1.8 644)) (source/run_aut.mli (lurette/b/46_automata.m 1.9 644))
(source/run_aut.ml (lurette/b/47_automata.m 1.18 644)) (source/run_aut.ml (lurette/b/47_automata.m 1.19 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.10 644)) (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.10 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.23 644)) (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.23 644))
...@@ -104,8 +105,8 @@ Various fixes in the C scade parsing. ...@@ -104,8 +105,8 @@ Various fixes in the C scade parsing.
(source/ne.ml (lurette/c/21_ne.ml 1.11 644)) (source/ne.ml (lurette/c/21_ne.ml 1.11 644))
(source/ne.mli (lurette/c/22_ne.mli 1.9 644)) (source/ne.mli (lurette/c/22_ne.mli 1.9 644))
(source/value.ml (lurette/c/23_value.ml 1.6 644)) (source/value.ml (lurette/c/23_value.ml 1.7 644))
(source/value.mli (lurette/c/24_value.mli 1.5 644)) (source/value.mli (lurette/c/24_value.mli 1.6 644))
(source/prevar.ml (lurette/d/18_prevar.ml 1.4 644)) (source/prevar.ml (lurette/d/18_prevar.ml 1.4 644))
(source/prevar.mli (lurette/d/19_prevar.mli 1.5 644)) (source/prevar.mli (lurette/d/19_prevar.mli 1.5 644))
...@@ -142,10 +143,10 @@ Various fixes in the C scade parsing. ...@@ -142,10 +143,10 @@ Various fixes in the C scade parsing.
(share/pixmaps/button-close.xpm (lurette/f/24_button-clo 1.1 644)) (share/pixmaps/button-close.xpm (lurette/f/24_button-clo 1.1 644))
(share/config.guess (lurette/f/25_config.gue 1.1 755)) (share/config.guess (lurette/f/25_config.gue 1.1 755))
(share/configure.in (lurette/d/11_configure. 1.14 644)) (share/configure.in (lurette/d/11_configure. 1.14 644))
(Makefile.common.source (lurette/e/33_Makefile.c 1.8 644)) (Makefile.common.source (lurette/e/33_Makefile.c 1.9 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.51 644)) (OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
(share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.28 644)) (share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.28 644))
(user-rules (lurette/c/14_myrules 1.49 644)) (user-rules (lurette/c/14_myrules 1.50 644))
(share/Makefile.test.in (lurette/c/25_user-rules 1.10 644)) (share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
(Makefile (lurette/d/13_Makefile 1.4 644)) (Makefile (lurette/d/13_Makefile 1.4 644))
...@@ -162,7 +163,7 @@ Various fixes in the C scade parsing. ...@@ -162,7 +163,7 @@ Various fixes in the C scade parsing.
(doc/archi.fig (lurette/20_archi.fig 1.1 644)) (doc/archi.fig (lurette/20_archi.fig 1.1 644))
(doc/synthese (lurette/b/2_synthese 1.1 644)) (doc/synthese (lurette/b/2_synthese 1.1 644))
(doc/automata_format (lurette/b/3_automata_f 1.1 644)) (doc/automata_format (lurette/b/3_automata_f 1.1 644))
(doc/ocamldoc.sty (lurette/b/12_ocamldoc.s 1.2 644)) (doc/ocamldoc.sty (lurette/b/12_ocamldoc.s 1.3 644))
(doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644)) (doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644))
;; Misc ;; Misc
...@@ -170,19 +171,19 @@ Various fixes in the C scade parsing. ...@@ -170,19 +171,19 @@ Various fixes in the C scade parsing.
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644)) (ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(INSTALL (lurette/f/26_INSTALL 1.2 744)) (INSTALL (lurette/f/26_INSTALL 1.2 744))
(TAGS (lurette/21_TAGS 1.6 644)) (TAGS (lurette/21_TAGS 1.6 644))
(TODO (lurette/d/22_TODO 1.31 644)) (TODO (lurette/d/22_TODO 1.32 644))
(share/lucky_init.csh.in (lurette/e/23_lucky_init 1.8 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.11 644)) (share/lucky_init.sh.in (lurette/e/24_lucky_init 1.11 644))
(share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744)) (share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744))
(share/plot (lurette/e/35_plot 1.6 744)) (share/plot (lurette/e/35_plot 1.6 744))
(test/time-ossau.exp (lurette/b/48_time.exp 1.54 644)) (test/time-ossau.exp (lurette/b/48_time.exp 1.55 644))
(test/time-ossau.res (lurette/b/49_time.res 1.58 644)) (test/time-ossau.res (lurette/b/49_time.res 1.58 644))
(test/time-ecrins.res (lurette/d/20_time-ecrin 1.34 644)) (test/time-ecrins.res (lurette/d/20_time-ecrin 1.35 644))
(test/time-ecrins.exp (lurette/d/21_time-ecrin 1.33 644)) (test/time-ecrins.exp (lurette/d/21_time-ecrin 1.34 644))
(test/time-moucherotte.exp (lurette/e/37_time-mouch 1.12 644)) (test/time-moucherotte.exp (lurette/e/37_time-mouch 1.13 644))
(test/time-moucherotte.res (lurette/e/38_time-mouch 1.13 644)) (test/time-moucherotte.res (lurette/e/38_time-mouch 1.14 644))
;; Various files used for testing purposes ;; Various files used for testing purposes
(test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644)) (test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644))
...@@ -281,10 +282,10 @@ Various fixes in the C scade parsing. ...@@ -281,10 +282,10 @@ Various fixes in the C scade parsing.
(test/Makefile (lurette/c/0_Makefile 1.14 644)) (test/Makefile (lurette/c/0_Makefile 1.14 644))
;; xlurette ;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.30 644)) (ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.31 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.25 644)) (ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.25 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.23 644)) (ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.23 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.18 644)) (ihm/xlurette/makefile (lurette/c/16_makefile 1.19 644))
;; cudaux ;; cudaux
...@@ -438,48 +439,48 @@ Various fixes in the C scade parsing. ...@@ -438,48 +439,48 @@ Various fixes in the C scade parsing.
;; Files added by populate at Fri, 17 Oct 2003 12:22:17 +0200, ;; Files added by populate at Fri, 17 Oct 2003 12:22:17 +0200,
;; to version 1.7(w), by jahier: ;; to version 1.7(w), by jahier:
(source/poly_draw.ml (lurette/g/43_polyDraw.m 1.2 644)) (source/poly_draw.ml (lurette/g/43_polyDraw.m 1.3 644))
;; Files added by populate at Fri, 17 Oct 2003 12:22:20 +0200, ;; Files added by populate at Fri, 17 Oct 2003 12:22:20 +0200,
;; to version 1.7(w), by jahier: ;; to version 1.7(w), by jahier:
(source/poly_draw.mli (lurette/g/44_polyDraw.m 1.2 644)) (source/poly_draw.mli (lurette/g/44_polyDraw.m 1.3 644))
;; Files added by populate at Thu, 13 Nov 2003 16:59:39 +0100, ;; Files added by populate at Thu, 13 Nov 2003 16:59:39 +0100,
;; to version 1.8(w), by jahier: ;; to version 1.8(w), by jahier:
(source/lustreExp.ml (lurette/g/45_lustreExp. 1.1 644)) (source/lustreExp.ml (lurette/g/45_lustreExp. 1.2 644))
;; Files added by populate at Thu, 13 Nov 2003 16:59:41 +0100, ;; Files added by populate at Thu, 13 Nov 2003 16:59:41 +0100,
;; to version 1.8(w), by jahier: ;; to version 1.8(w), by jahier:
(source/lustreExp.mli (lurette/g/46_lustreExp. 1.1 644)) (source/lustreExp.mli (lurette/g/46_lustreExp. 1.2 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:47 +0100, ;; Files added by populate at Fri, 14 Nov 2003 14:32:47 +0100,
;; to version 1.8(w), by jahier: ;; to version 1.8(w), by jahier:
(source/exp.ml (lurette/g/47_exp.ml 1.1 644)) (source/exp.ml (lurette/g/47_exp.ml 1.2 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:49 +0100, ;; Files added by populate at Fri, 14 Nov 2003 14:32:49 +0100,
;; to version 1.8(w), by jahier: ;; to version 1.8(w), by jahier:
(source/exp.mli (lurette/g/48_exp.mli 1.1 644)) (source/exp.mli (lurette/g/48_exp.mli 1.2 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:53 +0100, ;; Files added by populate at Fri, 14 Nov 2003 14:32:53 +0100,
;; to version 1.8(w), by jahier: ;; to version 1.8(w), by jahier:
(source/var.ml (lurette/g/49_var.ml 1.2 644)) (source/var.ml (lurette/g/49_var.ml 1.3 644))
;; Files added by populate at Fri, 14 Nov 2003 14:32:55 +0100, ;; Files added by populate at Fri, 14 Nov 2003 14:32:55 +0100,
;; to version 1.8(w), by jahier: ;; to version 1.8(w), by jahier:
(source/var.mli (lurette/g/50_var.mli 1.2 644)) (source/var.mli (lurette/g/50_var.mli 1.3 644))
;; Files added by populate at Wed, 26 Nov 2003 08:47:27 +0100, ;; Files added by populate at Wed, 26 Nov 2003 08:47:27 +0100,
;; to version 1.10(w), by jahier: ;; to version 1.10(w), by jahier:
(source/thickness.ml (lurette/g/51_thickness. 1.1 644)) (source/thickness.ml (lurette/g/51_thickness. 1.2 644))
) )
(Merge-Parents) (Merge-Parents)
(New-Merge-Parents) (New-Merge-Parents)
...@@ -10,21 +10,25 @@ ...@@ -10,21 +10,25 @@
(** Bdd Drawer. *) (** Bdd Drawer. *)
(** Machinery to perform a draw in a bdd (hence the third d ...) *) (** Machinery to perform a draw in a bdd. *)
type sol_nb = float
val draw_in_bdd : Var.env_in -> Env_state.t -> Exp.var list -> Bdd.t -> val draw_in_bdd : Var.env_in -> Env_state.t -> Exp.var list -> Bdd.t ->
Bdd.t -> Var.subst list * Store.t' * Store.p Bdd.t -> Var.subst list * Store.t' * Store.p
(** [draw_in_bdd inputs state vars bdd comb] returns a draw of the (** [draw_in_bdd inputs state vars bdd comb] returns a draw of the
Boolean variables as well as a range based and a polyhedron based Boolean variables as well as a range based and a polyhedron based
representation of numeric constraints. representation of numeric constraints (cf the [Store] module).
*) *)
type sol_nb = float
(** We use floats to count solution numbers because it can be very
big. Moreover, for big numbers, we do not really care the extra
precision an abitrary-long-integer data-type would offer. *)
val sol_number : Bdd.t -> sol_nb * sol_nb val sol_number : Bdd.t -> sol_nb * sol_nb
(** Returns the solution number in the then and else branches of the bdd *) (** [sol_number bdd] returns the solution number in the then and else
branches of [bdd]. *)
(**/**) (**/**)
......
(*----------------------------------------------------------------------- (*-----------------------------------------------------------------------
** Copyright (C) - Verimag. ** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General ** This file may only be copied under the terms of the GNU Library General
** Public License ** Public License
**----------------------------------------------------------------------- **-----------------------------------------------------------------------
...@@ -8,12 +8,12 @@ ...@@ -8,12 +8,12 @@
** Author: jahier@imag.fr ** Author: jahier@imag.fr
*) *)
(** Defines the environment state data type. (** The environment state.
Such state contains two parts : Such a state is a structure that contains two parts :
- a static part, that is set after the lucky files parsing, - a static part ([static_state_fields]), which is set after the lucky files
and which never changes after parsing, and which never changes after
- a dynamic part, which changes after each step. - a dynamic part ([dynamic_state_fields]), which changes after each step.
*) *)
...@@ -26,9 +26,9 @@ type node_info = { ...@@ -26,9 +26,9 @@ type node_info = {
source : source_info source : source_info
} }
(** (** There are some redundancies, but it is on purpose: the goal is to
There are some redundancies, but it is on purpose. The goal is to pre-compute here and once for anything what will be needed at
precompute here and once for all what will be needed at runtime. runtime.
*) *)
type static_state_fields = { type static_state_fields = {
bool_vars_to_gen : Exp.var list list ; bool_vars_to_gen : Exp.var list list ;
...@@ -55,10 +55,11 @@ type t = { ...@@ -55,10 +55,11 @@ type t = {
val read_env_state : Parse_luc.automata list -> t val read_env_state : Parse_luc.automata list -> t
(** Build the initial state from the list of parsed automata *) (** Builds the initial state from the list of parsed automata *)
(**/**) (**/**)
val is_node_transient : Parse_luc.node -> t -> bool val is_node_transient : Parse_luc.node -> t -> bool
......
(*----------------------------------------------------------------------- (*-----------------------------------------------------------------------
** Copyright (C) 2001 - 2003 - Verimag. ** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General ** This file may only be copied under the terms of the GNU Library General
** Public License ** Public License
**----------------------------------------------------------------------- **-----------------------------------------------------------------------
...@@ -64,7 +64,6 @@ and ...@@ -64,7 +64,6 @@ and
type vut = (Var.name * (Var.user_type * var list))
(****************************************************************************) (****************************************************************************)
......
(*----------------------------------------------------------------------- (*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag. ** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General ** This file may only be copied under the terms of the GNU Library General
** Public License ** Public License
**----------------------------------------------------------------------- **-----------------------------------------------------------------------
...@@ -8,11 +8,7 @@ ...@@ -8,11 +8,7 @@
** Author: jahier@imag.fr ** Author: jahier@imag.fr
*) *)
(** Defines the formula data type that labels lucky automata. *) (** Lucky Boolean and numeric expressions. *)
(* open Constraint *)
(****************************************************************************)
type t = type t =
...@@ -21,28 +17,6 @@ type t = ...@@ -21,28 +17,6 @@ type t =
| Liste of simple list | Liste of simple list
(** struct and arrays are flattened in such a list *) (** struct and arrays are flattened in such a list *)
and simple =
Fo of formula
| Nu of num
and num =
| Sum of num * num
| Diff of num * num
| Prod of num * num
| Quot of num * num
| Mod of num * num (** modulo *)
| Div of num * num (** euclidian division *)
| Uminus of num
| Inf_int
| Ival of int
| Fval of float
| Ivar of var
| Fvar of var
| Ite of formula * num * num
and formula = and formula =
| And of formula * formula | And of formula * formula
| Or of formula * formula | Or of formula * formula
...@@ -61,21 +35,43 @@ and formula = ...@@ -61,21 +35,43 @@ and formula =
| SupEq of num * num (* >= *) | SupEq of num * num (* >= *)
| Inf of num * num (* < *) | Inf of num * num (* < *)
| InfEq of num * num (* <= *) | InfEq of num * num (* <= *)
and and
(** cf the [Var] module. *)
var = t Var.t var = t Var.t
and num =
| Sum of num * num
| Diff of num * num
| Prod of num * num
| Quot of num * num
| Mod of num * num (* modulo *)
| Div of num * num (* euclidian division *)
| Uminus of num
| Inf_int
| Ival of int
| Fval of float
| Ivar of var
| Fvar of var
type vut = (Var.name * (Var.user_type * var list)) | Ite of formula * num * num
(** if the var name is a struct, this field ougth to contain
the corresponding list of leaves variables *)
(****************************************************************************) and simple =
Fo of formula
| Nu of num
(**/**)
val support : formula -> Var.name list val support : formula -> Var.name list
(** [support f] returns the support of f, if it is a cube made of boolean var *) (** [support f] returns the support of f, if it is a cube made of Boolean var *)
val num_is_an_int : num -> bool
(** [num_to_var_value e] translate the expression [e] into a value (** [num_to_var_value e] translate the expression [e] into a value
if possible, fails otherwise *) if possible, fails otherwise *)
...@@ -90,9 +86,6 @@ val formula_to_var_value : formula -> Value.t ...@@ -90,9 +86,6 @@ val formula_to_var_value : formula -> Value.t
(** fails if the result is a list *) (** fails if the result is a list *)
val to_simple : t -> simple val to_simple : t -> simple
val num_is_an_int : num -> bool
(**/**)
(****************************************************************************) (****************************************************************************)
(** Pretty prints formula and expressions. *) (** Pretty prints formula and expressions. *)
......
...@@ -8,21 +8,21 @@ ...@@ -8,21 +8,21 @@
** Main author: jahier@imag.fr ** Main author: jahier@imag.fr
*)