Cleaning Makefiles (OcamlRM is now part of rdbg-plugin !)

Makefile.common.source

@@ -196,7 +196,7 @@ ifeq ($(HOSTTYPE),win32)
 
 else
 # LINUX quoi ...
-  
+
   OCAML_PATH=/usr/local/soft/ocaml/3.10.0/bin/
   OCAML_PATH=
 
@@ -379,13 +379,6 @@ LUTIN_SOURCES = \
 	$(OBJDIR)/lutExe.mli \
 	$(OBJDIR)/lutExe.ml 
 
-EVENT= \
-	$(OBJDIR)/failure.ml \
-	$(OBJDIR)/failure.mli \
-	$(OBJDIR)/data.ml \
-	$(OBJDIR)/data.mli \
-	$(OBJDIR)/expr.ml \
-	$(OBJDIR)/event.ml
 
 
 LUTIN_FILES = \

examples/lutin/crazy-rabbit/Makefile

 export OCAMLOPT=ocamlopt
 LTOP=../../../bin/lurettetop$(EXE)
-LIB=../../../lib  -I +rdbg-plugin
+LIB=../../../lib  -I +rdbg-plugin 
 
 MAIN=rabbit
 
@@ -14,7 +14,7 @@ $(EXPDIR):
 
 
 %.cmxs: %.ml
-	 ocamlopt -shared -o $*.cmxs  -I $(LIB) graphics.cmxa ocamlRM.cmx  $*.ml 
+	 ocamlopt -shared -o $*.cmxs  -I $(LIB) graphics.cmxa  $*.ml 
 
 
 clean:

source/Lurettetop/Makefile.comon

@@ -145,8 +145,6 @@ LTOP_SOURCES = \
 	$(OBJDIR)/lus2licRun.ml \
 	$(OBJDIR)/lutinRun.mli  \
 	$(OBJDIR)/lutinRun.ml  \
-	$(OBJDIR)/ocamlRM.mli  \
-	$(OBJDIR)/ocamlRM.ml  \
 	$(OBJDIR)/ocamlRun.mli  \
 	$(OBJDIR)/ocamlRun.ml  \
 	$(OBJDIR)/lustreRun.mli  \

source/Lurettetop/exprUtil.mli

@@ -9,8 +9,12 @@
    expression representing the list of monomes that makes its true *)
 
 (* [get_info bdd bdd1 (bdd2,e2)] tries to explain as concisely as
-   possible why bdd is false
+   possible why bdd is not satisfiable
 
-   hyp: bdd=bdd1^bdd2=false ; bdd2=to_bdd(e2).
+   hyp: 
+   - bbd1 has sol
+   - bbd2 has sol
+   - bdd=bdd1^bdd2 has no sol 
+   - bdd2=to_bdd(e2).
 *)
 val get_info : Bdd.t -> Bdd.t ->  (Expr.t * Bdd.t) -> Failure.info

source/Makefile

@@ -650,10 +650,11 @@ ifeq ($(HOSTTYPE),cygwin)
   LUCKY_DEF=lucky.def
 endif
 
-compile_all: gen_version $(OBJDIR) lucky   show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2luciole luc4c liblucky_nc.a libluc4c_nc.a draw-all   $(LUCKY_DEF) lutin check-rif  ltop  lut4ocaml-clean lut4ocaml-all ldbg 
+old: lucky luc2luciole luc4c  liblucky_nc.a  libluc4c_nc.a
 
-rest:   stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2luciole luc4c liblucky_nc.a libluc4c_nc.a draw-all   $(LUCKY_DEF) lutin check-rif  ltop  lut4ocaml-clean lut4ocaml ldbg 
+compile_all: gen_version $(OBJDIR)  gnuplot-rif gnuplot-socket call-via-socket  draw-all   $(LUCKY_DEF) lutin check-rif  ltop  lut4ocaml-clean lut4ocaml-all ldbg 
 
+rest:  ltop  lut4ocaml-clean lut4ocaml-all ldbg 
 allnc:  clean lucky ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc  luc2luciole luc4c libluc4c_nc.a draw-all lut4ocaml-all check-rif  
 
 static: lucky_static ltop_static show_static stubs_static  gen_luc_static
@@ -700,8 +701,6 @@ cp: create_dirs lut4ocaml-cp  draw-cp
 	cp $(OBJDIR)/check-rif$(EXE) $(BIN_INSTALL_DIR) ; \
 	cp $(OBJDIR)/luc2luciole$(EXE) $(BIN_INSTALL_DIR) ; \
 	cp $(OBJDIR)/lurettetop_exe$(EXE) $(BIN_INSTALL_DIR) ; \
-	cp $(OBJDIR)/ocamlRM.o  $(LIB_INSTALL_DIR)   ;\
-	cp $(OBJDIR)/ocamlRM.cm*  $(LIB_INSTALL_DIR)   ;\
 	cp Lurettetop/ldbg.mli  $(LIB_INSTALL_DIR)   ;\
 	cp Lurettetop/ldbg_utils.mli  $(LIB_INSTALL_DIR)   ;\
 	cp Lurettetop/ldbg_utils.ml  $(LIB_INSTALL_DIR)   ;\
@@ -711,8 +710,6 @@ cp: create_dirs lut4ocaml-cp  draw-cp
 	cp $(OBJDIR)/lexeme.cmo  $(LIB_INSTALL_DIR)   ;\
 	cp $(OBJDIR)/ldbg.cmi  $(LIB_INSTALL_DIR)   ;\
 	cp $(OBJDIR)/ldbg.cmo  $(LIB_INSTALL_DIR)   ;\
-	cp $(OBJDIR)/ocamlRM.mli  $(LIB_INSTALL_DIR)   ;\
-	cp $(OBJDIR)/ocamlRM.ml  $(LIB_INSTALL_DIR)   ;\
 	cp $(OBJDIR)/value.cmi  $(LIB_INSTALL_DIR)   ;\
 	cp $(OBJDIR)/var.cmi  $(LIB_INSTALL_DIR)   ;\
 	cp $(OBJDIR)/libluc*.a  $(LIB_INSTALL_DIR)   ;\

source/common/ocamlRM.ml

-
-
-type t = {
-  inputs : (string, (string * string) list) Hashtbl.t;
-  outputs : (string, (string * string) list) Hashtbl.t;
-  mems : (string, (Data.subst list * Data.subst list))  Hashtbl.t;
-  kill : (string, (string -> unit))  Hashtbl.t;
-  step : (string,  (Data.subst list -> Data.subst list)) Hashtbl.t;
-}
-
-let it = {
-  inputs = Hashtbl.create 1;
-  outputs  = Hashtbl.create 1;
-  mems  = Hashtbl.create 1;
-  kill  = Hashtbl.create 1;
-  step  = Hashtbl.create 1;
-} 
-
-
-let (add_inputs : string ->  (string * string) list -> unit) =
-  fun cmxs l -> 
-    Hashtbl.add it.inputs cmxs l
-
-let (get_inputs : string ->  (string * string) list) =
-  fun cmxs -> 
-    try Hashtbl.find it.inputs cmxs
-    with Not_found ->
-      Printf.eprintf  "Cannot find input decls in  %s\n" cmxs;
-      exit 2
-        
-let (add_outputs : string ->  (string * string) list -> unit) =
-  fun cmxs l -> 
-    Hashtbl.add it.outputs cmxs l
-
-let (get_outputs : string ->  (string * string) list) =
-  fun cmxs -> 
-    try Hashtbl.find it.outputs cmxs
-    with Not_found ->  
-      Printf.eprintf "Cannot find output decls in  %s\n" cmxs;
-      exit 2
-
-let (add_kill : string -> (string -> unit) -> unit) =
-  fun cmxs l -> 
-    Hashtbl.add it.kill cmxs l
-
-let (get_kill : string -> (string -> unit)) =
-  fun cmxs -> 
-    try Hashtbl.find it.kill cmxs
-    with Not_found ->  
-      Printf.eprintf "Cannot find the kill function in %s\n"  cmxs;
-      exit 2
-
-let (add_step : string ->  (Data.subst list -> Data.subst list) -> unit) =
-  fun cmxs l -> 
-    Hashtbl.add it.step cmxs l
-        
-let (get_step : string ->  (Data.subst list -> Data.subst list)) =
-  fun cmxs -> 
-    try Hashtbl.find it.step cmxs
-    with Not_found ->  
-      Printf.eprintf "Cannot find step function in %s\n" cmxs;
-      exit 2
-
-let (add_mems : string -> Data.subst list -> Data.subst list -> unit) =
-  fun cmxs i o -> 
-    Hashtbl.add it.mems cmxs (i,o)
-
-let (get_mems : string -> Data.subst list * Data.subst list) =
-  fun cmxs -> 
-    try Hashtbl.find it.mems cmxs
-    with Not_found ->
-      Printf.eprintf  "Cannot find mem decls in  %s\n" cmxs;
-      exit 2
-

source/common/ocamlRM.mli

-
-
-(** In order to generate a xxx.cmxs loadable for lurette, one need 
-    to define a .ml program that registry various info using the
-    functions below. e.g.,
-
-let _ = 
-  OcamlRM.add_inputs  "xxx.cmxs" inputs;
-  OcamlRM.add_outputs "xxx.cmxs" outputs;
-  OcamlRM.add_kill "xxx.cmxs" kill;
-  OcamlRM.add_step "xxx.cmxs" step;
-  OcamlRM.add_mems "xxx.cmxs" mems_i mems_o
-;;
- 
-*)
-val add_inputs : string ->  (string * string) list -> unit
-val add_outputs : string ->  (string * string) list -> unit
-val add_kill : string -> (string -> unit) -> unit
-val add_step : string ->  (Data.subst list -> Data.subst list) -> unit
-val add_mems : string -> Data.subst list -> Data.subst list -> unit
-
-
-val get_inputs : string ->  (string * string) list
-val get_outputs : string ->  (string * string) list
-val get_kill : string -> (string -> unit)
-val get_step : string ->  (Data.subst list -> Data.subst list)
-val get_mems : string -> Data.subst list * Data.subst list

source/misc/Makefile.check_rif

@@ -30,8 +30,6 @@ SOURCES_OCAML = \
           $(OBJDIR)/coverage.ml \
           $(OBJDIR)/luciole.mli \
           $(OBJDIR)/luciole.ml \
-	  $(OBJDIR)/ocamlRM.mli  \
-	  $(OBJDIR)/ocamlRM.ml  \
           $(OBJDIR)/lustreRun.mli \
           $(OBJDIR)/lustreRun.ml \
           $(OBJDIR)/checkRif.ml