From 87226f67894aefde5899fb6d80debc4bfb256aed Mon Sep 17 00:00:00 2001 From: Pascal Raymond <Pascal.Raymond@imag.fr> Date: Fri, 6 Jul 2012 18:50:25 +0200 Subject: [PATCH] =?UTF-8?q?un=20peu=20avanc=C3=83=C2=A9=20dans=20LicPrg=20?= =?UTF-8?q?...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Makefile | 1 + src/compile.ml | 3 ++- src/eff.ml | 2 +- src/ident.mli | 2 +- src/lazyCompiler.ml | 23 +++++++++++++------- src/licPrg.ml | 51 +++++++++++++++++++++++++++++++++++++++++++++ src/licPrg.mli | 12 +++++++++++ 7 files changed, 83 insertions(+), 11 deletions(-) create mode 100644 src/licPrg.mli diff --git a/Makefile b/Makefile index 7ab097d5..9e429209 100644 --- a/Makefile +++ b/Makefile @@ -64,6 +64,7 @@ SOURCES = \ $(OBJDIR)/name.ml \ $(OBJDIR)/polymorphism.ml \ $(OBJDIR)/licDump.ml \ + $(OBJDIR)/licPrg.mli \ $(OBJDIR)/licPrg.ml \ $(OBJDIR)/unifyType.mli \ $(OBJDIR)/unifyType.ml \ diff --git a/src/compile.ml b/src/compile.ml index 10364727..0044a5f0 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -38,4 +38,5 @@ let (doit : SyntaxTree.pack_or_model list -> Ident.idref option -> unit) = LazyCompiler.compile_all lzcomp else LazyCompiler.compile_node lzcomp main_node - in () + in + LicPrg.to_file !Global.oc zelic diff --git a/src/eff.ml b/src/eff.ml index f52d4e2b..0e9cabdd 100644 --- a/src/eff.ml +++ b/src/eff.ml @@ -302,7 +302,7 @@ and node_exp = { def_eff : node_def; has_mem_eff : bool; is_safe_eff : bool; - is_polym_eff : bool + is_polym_eff : bool } and node_def = diff --git a/src/ident.mli b/src/ident.mli index 1f818366..5bf0b34c 100644 --- a/src/ident.mli +++ b/src/ident.mli @@ -3,7 +3,7 @@ type t = string type long = t * t -type pack_name +type pack_name = t val to_string : t -> string val of_string : string -> t diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index 439af9ad..27575f9e 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1360,20 +1360,27 @@ let compile_all_nodes pack_name this id ni_f = (**** to_lic : translate the (finalized) internal structure into a proper LicPrg, for forthcoming manip and other prg 2 prg transformations + N.B. items belonging to the "Lustre" virtual pack are not + taken into account *) -let unflag (xflg: 'a Eff.check_flag) : 'a = - match xflg with - | Checked x -> x - | _ -> assert false - let to_lic (this:t) : LicPrg.t = (* normally, only checked and correct programs are lic'ified *) let unflag = function Checked x -> x | _ -> assert false in + let add_item add_x k v prg = + match Ident.pack_of_long k with + | "Lustre" -> prg + | _ -> add_x k (unflag v) prg + in + let add_node k v prg = + match Ident.pack_of_long (fst k) with + | "Lustre" -> prg + | _ -> LicPrg.add_node k (unflag v) prg + in let res = LicPrg.empty in - let res = Hashtbl.fold (fun k vflg prg -> LicPrg.add_type k (unflag vflg) prg) this.types res in - let res = Hashtbl.fold (fun k vflg prg -> LicPrg.add_const k (unflag vflg) prg) this.consts res in - let res = Hashtbl.fold (fun k vflg prg -> LicPrg.add_node k (unflag vflg) prg) this.nodes res in + let res = Hashtbl.fold (add_item LicPrg.add_type) this.types res in + let res = Hashtbl.fold (add_item LicPrg.add_const) this.consts res in + let res = Hashtbl.fold add_node this.nodes res in res (**** Entry points of the module : diff --git a/src/licPrg.ml b/src/licPrg.ml index 64faca01..485ca027 100644 --- a/src/licPrg.ml +++ b/src/licPrg.ml @@ -61,6 +61,57 @@ let add_const (k:Eff.item_key) (v:Eff.const) (prg:t) : t = { prg with consts = ItemKeyMap.add k v prg.consts } let add_node (k:Eff.node_key) (v:Eff.node_exp) (prg:t) : t = +Verbose.printf ~level:3 "## LicPrg.add_node %s\n" (LicDump.string_of_node_key_rec k); { prg with nodes = NodeKeyMap.add k v prg.nodes } +let dump_entete oc = + let time = Unix.localtime (Unix.time ()) in + let sys_call, _ = Array.fold_left + (fun (acc,i) x -> + if 70 < i + (String.length x) then + acc ^ "\n--\t\t" ^ x, String.length ("\n--\t\t" ^ x) + else + acc ^ " " ^ x , (i+1+(String.length x)) + ) + ("",0) + Sys.argv + and + date = Printf.sprintf "%d/%02d/%02d" + (1900+time.Unix.tm_year) + (time.Unix.tm_mon+1) + (time.Unix.tm_mday) + and + time_str = Printf.sprintf "%02d:%02d:%02d" + (time.Unix.tm_hour) + (time.Unix.tm_min) + (time.Unix.tm_sec) + (* and user = Unix.getlogin () *) + and hostname = Unix.gethostname () + in + (* Printf.fprintf oc "-- lus2lic version %s\n" Version.str; *) + (* Printf.fprintf oc "-- cmd: %s\n" sys_call; *) + (* Printf.fprintf oc "-- host: %s date: %s time: %s\n" hostname date time_str *) + Printf.fprintf oc "-- This file was generated by lus2lic version %s.\n" Version.str; + Printf.fprintf oc "-- %s\n" sys_call; + Printf.fprintf oc "-- on %s the %s at %s\n" hostname date time_str + +let to_file (oc: out_channel) (this:t) = + dump_entete oc; + (* On imprime dans l'ordre du iter, donc pas terrible ??? + *) + ItemKeyMap.iter + (fun tn te -> output_string !Global.oc (LicDump.type_decl tn te)) this.types; + ItemKeyMap.iter + (fun cn ce -> output_string !Global.oc (LicDump.const_decl cn ce)) this.consts; + + (* Pour les noeuds, pas sur que ça marche tant qu'on n'a + pas séparés les transformations source_to_source du LazyCompiler : + en cas d'expansion, il y avait cette remarque : + nb: we print res_struct, but do not return it from + node_check, because the structure and array expansion + modify (instanciate) the node profiles. *) + + NodeKeyMap.iter + (fun _ nexp -> output_string !Global.oc (LicDump.node_of_node_exp_eff nexp)) this.nodes + diff --git a/src/licPrg.mli b/src/licPrg.mli new file mode 100644 index 00000000..d600d081 --- /dev/null +++ b/src/licPrg.mli @@ -0,0 +1,12 @@ + +type t + +val empty : t + +val add_type : Eff.item_key -> Eff.type_ -> t -> t +val add_const : Eff.item_key -> Eff.const -> t -> t +val add_node : Eff.node_key -> Eff.node_exp -> t -> t + + +val to_file : out_channel -> t -> unit + -- GitLab