Commit dc8f78dc authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.112 Thu, 31 Oct 2002 08:21:03 +0100 by jahier

Parent-Version:      0.111
Version-Log:

source/parse_poc.ml: (new file)
source/gen_stubs.ml:
   put everything that is related to poc parsing into
   parse_poc.ml.

source/gen_fake_lutin.ml: (new file)
source/parse_poc.ml: (new file)
source/Makefile.gen_fake_lutin: (new file)
   When no .lut is provided, we generate a fake one.

Project-Description: Lurette
parent a5e54d03
......@@ -22,12 +22,12 @@
(source/ne.ml 9140 1033723811 c/21_ne.ml 1.1)
(source/value.mli 1101 1033723811 c/24_value.mli 1.1)
(user-rules.skel 973 1034006019 c/25_user-rules 1.1)
(source/Makefile.gen_stubs 176 1034351455 b/42_Makefile.g 1.4)
(source/Makefile.gen_stubs 212 1036048863 b/42_Makefile.g 1.5)
(test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3)
(source/luc_exe.ml 12191 1034351455 b/32_ima_exe.ml 1.21)
(test/heater_float.rif.exp 1485 1034951022 b/30_heater_flo 1.11)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(ihm/xlurette/makefile 1517 1035531408 c/16_makefile 1.5)
(ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6)
(test/usager.luc 495 1032789516 b/14_usager.env 1.9)
(mlcuddidl/manager.ml 8017 1034006019 c/47_manager.ml 1.1)
(cuddaux/cuddauxInt.h 2058 1034006019 c/28_cuddauxInt 1.1)
......@@ -42,25 +42,26 @@
(mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1)
(test/Makefile 32 1035531408 c/0_Makefile 1.8)
(source/parse_env.ml 24584 1033723811 41_parse_env. 1.29)
(ihm/xlurette/xlurette_glade_main.ml 23237 1035885606 c/12_xlurette_g 1.13)
(ihm/xlurette/xlurette_glade_main.ml 23753 1036048863 c/12_xlurette_g 1.14)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(source/solver.ml 31802 1033732198 39_solver.ml 1.32)
(source/solver.ml 31941 1036048863 39_solver.ml 1.33)
(test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1)
(source/gen_fake_lutin.ml 3449 1036048863 d/16_gen_fake_l 1.1)
(source/lurette.ml 14202 1035898240 12_lurette.ml 1.59)
(source/Makefile 1114 1035531408 c/20_Makefile 1.7)
(source/util.ml 19170 1035898240 35_util.ml 1.33)
(source/Makefile 1285 1036048863 c/20_Makefile 1.8)
(source/util.ml 20341 1036048863 35_util.ml 1.34)
(mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1)
(test/time.res 6326 1035898240 b/49_time.res 1.19)
(test/time.res 6325 1036048863 b/49_time.res 1.20)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
(source/command_line_luc_exe.mli 1082 1034006019 b/34_command_li 1.5)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/Makefile.lucky 2003 1035531408 b/41_Makefile.i 1.8)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1)
(source/Makefile.lurette_lib 1741 1035531408 c/2_Makefile.l 1.8)
(source/parse_env.mli 1025 1033738731 40_parse_env. 1.10)
(source/gen_stubs.ml 33941 1035898240 24_generate_l 1.40)
(source/gen_stubs.ml 27065 1036048863 24_generate_l 1.41)
(OcamlMakefile 22626 1034951022 17_OcamlMakef 1.45)
(source/command_line.ml 4914 1035557853 b/20_command_li 1.10)
(mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1)
......@@ -70,26 +71,26 @@
(make_lurette 1306 1034006019 27_make_luret 1.17)
(source/control.ml 4416 1030975996 c/4_control.ml 1.3)
(ihm/xlurette/xlurette_glade_interface.ml 32774 1035885606 c/15_xlurette_g 1.8)
(source/lurettetop.ml 30041 1035898240 c/1_lurettetop 1.21)
(source/lurettetop.ml 30402 1036048863 c/1_lurettetop 1.22)
(mlcuddidl/README 1574 1034006019 d/8_README 1.1)
(source/Makefile.lurettetop 300 1035531408 d/14_Makefile.l 1.1)
(cuddaux/README 1427 1034006019 c/34_README 1.1)
(source/Makefile.lurettetop 300 1035531408 d/14_Makefile.l 1.1)
(source/ne.mli 2376 1033723811 c/22_ne.mli 1.1)
(README 2264 1034951022 10_README 1.4)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(source/env_state.ml 20707 1033125605 51_env_state. 1.29)
(source/env_state.ml 20705 1036048863 51_env_state. 1.30)
(mlcuddidl/manager_caml.c 39233 1034006019 c/45_manager_ca 1.1)
(mlcuddidl/mtbdd.mli 4395 1034006019 c/43_mtbdd.mli 1.1)
(source/env.mli 2027 1033738731 15_env.mli 1.16)
(mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1)
(Makefile.common.in 528 1034951022 d/12_Makefile.c 1.2)
(user-rules 14031 1035885606 c/14_myrules 1.16)
(user-rules 14209 1036048863 c/14_myrules 1.17)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/gne.mli 1552 1033397911 b/36_gne.mli 1.4)
(test/giro/giro.luc 2755 1033738731 c/6_giro.ima 1.4)
(source/show_env.mli 1091 1033738731 42_show_env.m 1.8)
(Makefile.lurette 546 1034951022 b/38_Makefile.l 1.14)
(Makefile.lurette 548 1036048863 b/38_Makefile.l 1.15)
(source/luc_exe.mli 447 1033738731 b/31_ima_exe.ml 1.2)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(mlcuddidl/bdd.idl 18233 1034006019 d/7_bdd.idl 1.1)
......@@ -119,10 +120,11 @@
(cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1)
(mlcuddidl/macros.m4 11290 1034006019 c/49_macros.m4 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(source/Makefile.gen_fake_lutin 248 1036048863 d/17_Makefile.g 1.1)
(mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/rnumsolver.ml 20636 1033732198 b/27_rnumsolver 1.13)
(source/rnumsolver.ml 20806 1036048863 b/27_rnumsolver 1.14)
(mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1)
(source/print.ml 5807 1033723811 47_print.ml 1.21)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
......@@ -130,13 +132,14 @@
(cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1)
(source/show_env.ml 3436 1034351455 43_show_env.m 1.14)
(mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1)
(source/parse_poc.ml 7093 1036048863 d/15_parse_poc. 1.1)
(cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1)
(source/rnumsolver.mli 2198 1033732198 b/26_rnumsolver 1.9)
(source/sim2chro.ml 2721 1033397911 b/24_sim2chro.m 1.14)
(source/command_line_luc_exe.ml 2786 1034006019 b/33_command_li 1.7)
(mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1)
(source/value.ml 2355 1033723811 c/23_value.ml 1.1)
(test/time.exp 6326 1035898240 b/48_time.exp 1.16)
(test/time.exp 6325 1036048863 b/48_time.exp 1.17)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1)
......
......@@ -24,5 +24,7 @@ SOURCES = $(SOURCES_C) $(SOURCES_OCAML)
RESULT = lurette
-include $(OCAMLMAKEFILE)
......@@ -15,7 +15,8 @@ xlurette: dummy
ocamlc -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlc -c -i -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlc -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlc $(THREAD) -I +lablgtk -o xlurette unix.cma lablgtk.cma gtkInit.cmo \
ocamlc $(THREAD) \
-I +lablgtk -I +str -o xlurette str.cma unix.cma lablgtk.cma gtkInit.cmo util.cmo \
xlurette_glade_callbacks.cmo xlurette_glade_interface.cmo xlurette_glade_main.cmo
xlurette.opt: dummy
......@@ -23,15 +24,15 @@ xlurette.opt: dummy
ocamlopt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt -c -pp "camlp4o" -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt -I +lablgtk -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx \
ocamlopt -I +lablgtk -I +str -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx util.cmx \
xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
xlurette.opt_opt: dummy
mlglade xlurette.glade
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_interface.ml
ocamlopt.opt -c -I +lablgtk -labels -c xlurette_glade_callbacks.ml
ocamlopt.opt -pp "camlp4o" -c -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -I +lablgtk -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx \
ocamlopt.opt -pp "camlp4o" -c -I +lablgtk $(THREAD) -c xlurette_glade_main.ml
ocamlopt.opt -I +lablgtk -I +str -labels -o xlurette unix.cmxa lablgtk.cmxa gtkInit.cmx util.cmx \
xlurette_glade_callbacks.cmx xlurette_glade_interface.cmx xlurette_glade_main.cmx
......
......@@ -39,6 +39,8 @@ class customized_callbacks = object(self)
inherit Xlurette_glade_callbacks.default_callbacks
method put str = self#top_xlurette#output_window#insert str
method read_pipe () =
let length = float_of_string self#top_xlurette#test_length#text in
let
......@@ -352,6 +354,22 @@ class customized_callbacks = object(self)
self#top_xlurette#oracle_node#set_text node
method run_lurette () =
if self#top_xlurette#env_name#text = ""
then
(
let str = self#top_xlurette#sut_name#text in
let base = Filename.basename str in
let node =
try Filename.chop_extension base
with _ -> base
in
self#put "Since no environment is provided, I generate a fake one named\n";
self#put (node ^ "_env.lut, that you can edit and modify.\n\n");
Util.gen_fake_lutin (node ^ ".h") ;
self#top_xlurette#env_name#set_text (node ^ "_env.lut")
);
let all_cmds = (self#get_all_cmds ()) ^ "run\n" in
if self#top_xlurette#radiobutton_step_yes#active
......@@ -476,8 +494,8 @@ class customized_callbacks = object(self)
match tok with parser
| [< 'Genlex.Ident "x" ; tail = parse_env >] -> (" x " ^ tail)
| [< 'Genlex.String str ; tail = parse_env >] ->
((remove_extension str) ^ ".luc " ^ tail)
| [< 'Genlex.Ident id ; tail = parse_env >] -> (id ^ ".luc " ^ tail)
( str ^ tail)
| [< 'Genlex.Ident id ; tail = parse_env >] -> (id ^ " " ^ tail)
| [< _ >] -> ""
)
with e ->
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 111)
(Parent-Version lurette 0 110)
(Project-Version lurette 0 112)
(Parent-Version lurette 0 111)
(Version-Log "
source/util.ml:
source/formula.ml:
source/lurette.ml:
Only print one counter example if the test failed.
source/lurettetop.ml:
source/parse_poc.ml: (new file)
source/gen_stubs.ml:
try to guess the node name in lurettetop rather than in gen_stubs
if not given.
put everything that is related to poc parsing into
parse_poc.ml.
source/gen_fake_lutin.ml: (new file)
source/parse_poc.ml: (new file)
source/Makefile.gen_fake_lutin: (new file)
When no .lut is provided, we generate a fake one.
")
(New-Version-Log ""
)
(Checkin-Time "Tue, 29 Oct 2002 14:30:40 +0100")
(Checkin-Time "Thu, 31 Oct 2002 08:21:03 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -51,13 +48,13 @@ source/gen_stubs.ml:
(source/env.mli (lurette/15_env.mli 1.16 644))
(source/env.ml (lurette/16_env.ml 1.29 644))
(source/util.ml (lurette/35_util.ml 1.33 444))
(source/util.ml (lurette/35_util.ml 1.34 444))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.32 644))
(source/solver.ml (lurette/39_solver.ml 1.33 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.9 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.13 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.14 644))
(source/parse_env.mli (lurette/40_parse_env. 1.10 644))
(source/parse_env.ml (lurette/41_parse_env. 1.29 644))
......@@ -75,7 +72,7 @@ source/gen_stubs.ml:
(source/eval.ml (lurette/49_eval.ml 1.13 644))
(source/env_state.mli (lurette/50_env_state. 1.24 644))
(source/env_state.ml (lurette/51_env_state. 1.29 644))
(source/env_state.ml (lurette/51_env_state. 1.30 644))
(source/automata.mli (lurette/b/46_automata.m 1.3 644))
(source/automata.ml (lurette/b/47_automata.m 1.5 644))
......@@ -86,8 +83,8 @@ source/gen_stubs.ml:
(source/gne.mli (lurette/b/36_gne.mli 1.4 644))
(source/gne.ml (lurette/b/37_gne.ml 1.4 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.21 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.40 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.22 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.41 644))
(source/control.mli (lurette/c/3_control.ml 1.2 644))
(source/control.ml (lurette/c/4_control.ml 1.3 644))
......@@ -101,6 +98,10 @@ source/gen_stubs.ml:
(source/value.ml (lurette/c/23_value.ml 1.1 644))
(source/value.mli (lurette/c/24_value.mli 1.1 644))
(source/parse_poc.ml (lurette/d/15_parse_poc. 1.1 644))
(source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.1 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.17 755))
......@@ -108,15 +109,18 @@ source/gen_stubs.ml:
(configure.in (lurette/d/11_configure. 1.1 644))
(Makefile.common.in (lurette/d/12_Makefile.c 1.2 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.45 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.14 644))
(user-rules (lurette/c/14_myrules 1.16 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.15 644))
(user-rules (lurette/c/14_myrules 1.17 644))
(user-rules.skel (lurette/c/25_user-rules 1.1 644))
(Makefile (lurette/d/13_Makefile 1.1 644))
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.1 644))
(source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.1 644))
(source/Makefile.show_luc (lurette/b/40_Makefile.s 1.7 644))
(source/Makefile.lucky (lurette/b/41_Makefile.i 1.8 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.4 644))
(source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644))
(source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.8 644))
(source/Makefile (lurette/c/20_Makefile 1.7 644))
(source/Makefile (lurette/c/20_Makefile 1.8 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -133,8 +137,8 @@ source/gen_stubs.ml:
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.16 644))
(test/time.res (lurette/b/49_time.res 1.19 644))
(test/time.exp (lurette/b/48_time.exp 1.17 644))
(test/time.res (lurette/b/49_time.res 1.20 644))
;; Various files used for testing purposes
(test/usager.luc (lurette/b/14_usager.env 1.9 644))
......@@ -172,10 +176,10 @@ source/gen_stubs.ml:
(test/Makefile (lurette/c/0_Makefile 1.8 644))
;; xlurette
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.13 644))
(ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.14 644))
(ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.9 644))
(ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.8 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.5 644))
(ihm/xlurette/makefile (lurette/c/16_makefile 1.6 644))
;; cudaux
......@@ -227,12 +231,6 @@ source/gen_stubs.ml:
;; Files added by populate at Thu, 24 Oct 2002 15:46:40 +0200,
;; to version 0.105(w), by jahier:
(Makefile (lurette/d/13_Makefile 1.1 644))
;; Files added by populate at Thu, 24 Oct 2002 15:50:53 +0200,
;; to version 0.105(w), by jahier:
(source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -12,6 +12,7 @@ lib_debug:
make -f Makefile.lurette_lib dc OCAMLFLAGS=""
lucky:
make -k -f Makefile.lucky OCAMLFLAGS="-noassert -unsafe"
lucky_debug:
......@@ -32,20 +33,25 @@ stubs:
make -k -f Makefile.gen_stubs OCAMLFLAGS="-noassert -unsafe"
gen_lut:
make -f Makefile.gen_fake_lutin OCAMLFLAGS="-noassert -unsafe"
all: lib lucky ltop show stubs
all: lib lucky ltop show stubs gen_lut
clean:
make -k clean -f Makefile.gen_stubs ; \
make -k clean -f Makefile.lucky ; \
make -k clean -f Makefile.lurettetop ; \
make -k clean -f Makefile.lurette_lib ; \
make -k clean -f Makefile.gen_fake_lutin ; \
make -k clean -f Makefile.show_luc
install: all
cp gen_stubs $(BIN_INSTALL_DIR) ; \
cp gen_fake_lutin $(BIN_INSTALL_DIR) ; \
cp lucky $(BIN_INSTALL_DIR) ; \
cp show_luc $(BIN_INSTALL_DIR) ; \
cp lurettetop $(BIN_INSTALL_DIR) ; \
......
#
-include ../Makefile.common
SOURCES = $(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/parse_poc.ml \
$(LURETTE_PATH)/source/gen_fake_lutin.ml
RESULT = gen_fake_lutin
LIBS = str unix
-include $(OCAMLMAKEFILE)
......@@ -3,7 +3,7 @@
-include ../Makefile.common
SOURCES = $(LURETTE_PATH)/source/util.ml $(LURETTE_PATH)/source/gen_stubs.ml
SOURCES = $(LURETTE_PATH)/source/util.ml $(LURETTE_PATH)/source/parse_poc.ml $(LURETTE_PATH)/source/gen_stubs.ml
RESULT = gen_stubs
LIBS = str unix
......
......@@ -82,7 +82,7 @@ type env_stateT = {
contained in its lhs (then) and rhs (else) branches. Note that
adding those two numbers only give a number of solution that is
relative to which bdd points to it. *)
mutable current_nodes : node list list;
(** List of the automata current nodes (there are as many nodes as
there are environment run in parallel). *)
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: gen_fake_lutin.ml
** Main author: jahier@imag.fr
*)
(** generate a fake lutin file from a C-poc one. *)
let usage = "gen_fake_lutin <POC C header file>
take a C header file and generates a lutin file containing
a fake lutin description of the environment of the header file.
"
open Parse_poc
type lutinT = Int | Bool | Real
let (c_type_to_lutin_type : string -> lutinT) =
fun ct ->
(** *)
match ct with
"byte" -> Int
| "short" -> Int
| "short int" -> Int
| "int" -> Int
| "long" -> Int
| "long int" -> Int
| "unsigned short" -> Int
| "unsigned short int" -> Int
| "unsigned int" -> Int
| "unsigned long" -> Int
| "unsigned long int" -> Int
| "float" -> Real
| "double" -> Real
| "long double" -> Real
| "bool" -> Bool
| "boolean" -> Bool
(* | "char" -> assert false *)
(* | "unsigned char" -> assert false *)
| str ->
print_string (str ^ ": Unsupported C type.\n");
flush stdout;
assert false
let (lutin_to_string : lutinT -> string) =
fun t ->
match t with
| Int -> "int"
| Real -> "real"
| Bool -> "bool"
let (generate_lutin: string -> vn_ct list -> vn_ct list -> unit) =
fun mod_name vi vo ->
let oc = open_out (mod_name ^ ".lut") in
let put s = output_string oc s in
let (_, vo_num) =
List.partition
(fun (_,ct) -> (c_type_to_lutin_type ct) = Bool)
vo
in
let string_of_var_list (vn, ct) =
("\t" ^ vn ^ " : " ^ (lutin_to_string (c_type_to_lutin_type ct)))
in
let put_fake_constraints (vn, ct) =
match (c_type_to_lutin_type ct) with
| Int ->
put "and (0 < "; put vn; put ") and ("; put vn ; put " < 5) \n\t\t"
| Real ->
put "and (0. < "; put vn; put ") and ("; put vn ; put " < 1.)\n\t\t"
| Bool -> assert false
in
put ("-- Automatically generated from " ^ mod_name
^ ".h by gen_fake_lutin.\n\n") ;
put "model "; put mod_name ; put " (\n";
put (String.concat ";\n" (List.map (string_of_var_list) vi));
put ")\n";
put "returns (\n";
put (String.concat ";\n" (List.map (string_of_var_list) vo));
put ")\n";
put "let\n";
put "\tfake_constraints = true \n\t";
List.iter (put_fake_constraints) vo_num ;
put ";\n";
put mod_name;
put " = {
loop fake_constraints pool
};\n\n";
put "tel\n";
close_out oc
let rec (main : unit -> unit) =
fun _ ->
let header_file = Sys.argv.(1) in
let _=
if
(((Filename.chop_extension header_file) ^ ".h") <> header_file)
then
(
print_string (header_file ^ " is not a C header file.\n");
print_string usage;
flush stdout;
exit 2
)
in
let (mod_name, vi0, vo0) = Parse_poc.get_vn_and_ct_list header_file in
let alias = replace_bool_representation (get_typedef_alias header_file) in
let vi = replace_ct_by_their_alias vi0 alias in
let vo = replace_ct_by_their_alias vo0 alias in
generate_lutin (mod_name ^ "_env") vo vi
;;
main ();;
......@@ -36,183 +36,8 @@ open Parse_poc
//OUT: <C type of the mth output var> <a C identifier for the mth output var>
*)
(****************************************************************************)
(****************************************************************************)
type file = string
type module_name = string
type var_name = string
type c_type = string
type ml_type = string
type fresh_var_name = string
type vn_ct = var_name * c_type
type vn_ct_mlt_fvn = var_name * c_type * ml_type * fresh_var_name
(****************************************************************************)
(****************************************************************************)
(* XXX Is it really a good idea to use regexp to parse those files ? *)
let reg_typedef = Str.regexp "^typedef"
let reg_blank = Str.regexp " "
let reg_semicol = Str.regexp ";"
type alias = c_type * c_type
(**
[get_typedef_alias file] reads [file] (a C header file) and search
for typedef C expressions and returns the list of (alias_type, C_type)
found in [file].
*)
let rec
(get_typedef_alias: file -> alias list) =
fun file ->
let str = Util.readfile file in
find_typedef_list str 0 []
and
(find_typedef_list: string -> int -> alias list -> alias list) =
fun str sptr list ->
try
let (alias, sptr1) = find_next_typedef str sptr in
find_typedef_list str sptr1 (alias::list)
with Not_found -> list
and
(find_next_typedef: string -> int -> ((string * string) * int)) =
fun str sptr ->
let sptr1 = Str.search_forward reg_typedef str sptr in
let sptr2 = Str.search_forward reg_blank str (sptr1+1) in
let sptr3 = Str.search_forward reg_blank str (sptr2+1) in
let sptr4 = Str.search_forward reg_semicol str (sptr3+1) in
let c_type = String.sub str (sptr2 + 1) (sptr3 - sptr2 - 1) in
let alias_type = String.sub str (sptr3 + 1) (sptr4 - sptr3 - 1) in
((alias_type, c_type), sptr4)
(* let () = assert(
(Util.list_are_equals
(get_typedef_alias "tram_simple.h")
(Util.sort_list_string_pair [("_float", "float"); ("_double", "double");
("_real", "double"); ("_string", "char*");
("_integer", "int"); ("_boolean", "int")] )))
*)
(****************************************************************************)
(****************************************************************************)
let reg_MOD = Str.regexp "^//MODULE:"
let reg_IN = Str.regexp "^//IN:"
let reg_OUT = Str.regexp "^//OUT:"
let reg_cr = Str.regexp "\n"
(**
Parses poc pragmas in a C header file and returns the module name, the
list of input vars, and the list of output vars name and type.
poc pragmas have the following shape:
//MODULE: <module name> n m
(* where [n] is the input var number, and [m] the output var one *)
//IN: <C type of the first input var> <a C identifier for the first input var>
...
//IN: <C type of the nth input var> <a C identifier for the nth input var>
//OUT: <C type of the first output var> <a C identifier for the first output var>
...
//OUT: <C type of the mth output var> <a C identifier for the mth output var>
*)
let rec (get_vn_and_ct_list: file -> module_name * vn_ct list * vn_ct list) =
fun file ->
let str = Util.readfile file in
let (mod_name, ni, no, str_ptr1) = find_module_name str in
let (vi, str_ptr2) = find_var_list reg_IN str str_ptr1 [] in
let (vo, _) = find_var_list reg_OUT str str_ptr2 [] in
if (List.length vi = ni && List.length vo = no) then
(mod_name, vi, vo)
else
failwith ("Inconsistent pragmas found in `" ^ file ^
"'. The number of variables is wrong: " ^
(string_of_int ni) ^ " and " ^ (string_of_int no) ^
" were declared whereas " ^ (string_of_int (List.length vi)) ^
" and " ^ (string_of_int (List.length vo)) ^ " were counted")