Commit 09a83a18 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add the lutin source (from Pascal Raymond).

parent b92a4b5f
-include ../Makefile.version
-include ./Makefile.version
# to run after a checkout in a fresh WS, or a change in the ocaml version
......@@ -31,18 +31,15 @@ test:
cia: test cia_notest
cia_notest:
git commit -a -F log
git commit -a -F log && rm source/version.ml
amend:
git commit -a -F log --amend
git commit -a -F log --amend && rm source/version.ml
ci: test
git commit -F log
git commit -F log && rm source/version.ml
lci:
prcs checkin -r unstable lurette.prj
make gen_version
ldiff:
pdiff -r unstable
......
open MainArg
open Printf
open Expand
open AutoExplore
(** Impression des expressions algbriques *)
let print_algexp
(os : Pervasives.out_channel)
(e : CoAlgExp.t) =
(
(* normalement, la syntaxe Lustre doit passer ??? *)
CoAlgExp.lus_dumpf os e
)
(** utilitaires *)
let print_header
(mnode: string)
(os : Pervasives.out_channel)
(auto : AutoExplore.t) =
(
fprintf os
"-- generated by lutin2 %s.%s\n" LutVersion.number LutVersion.release;
fprintf os
"-- file: %s node: %s\n"
(if (MainArg.infile() = "") then "stdin" else (MainArg.infile()))
(mnode );
(*
fprintf os "\nlibraries {\n";
fprintf os " liblutin = \"liblutin\";\n";
fprintf os "}\n";
fprintf os "\nfunctions {\n";
fprintf os " average_goon : int * int * int -> int : liblutin;\n";
fprintf os " average_stop : int * int * int -> int : liblutin;\n";
fprintf os " interval_goon : int * int * int -> int : liblutin;\n";
fprintf os " interval_stop : int * int * int -> int : liblutin;\n";
fprintf os "}\n";
*)
)
let make
(mnode : string)
(auto : AutoExplore.t)
(os : Pervasives.out_channel) =
(
(* le source au cas ou ... *)
let source_code = AutoExplore.source auto in
(*************** EN-TTE ************************************)
print_header mnode os auto;
(***********************************************************)
(*************** FONCTIONS EXTERNES ************************)
(***********************************************************)
let etab2prof s xi acc = (
(s, xi.xi_prof)::acc
) in
let xlist = Hashtbl.fold etab2prof
(Expand.extern_tab source_code) [] in
if (xlist = []) then ()
else (
fprintf os "\nfunctions {\n";
let pxd (s, p) = (
fprintf os " %s : %s;\n" s (CkTypeEff.prof_to_string p)
) in
List.iter pxd xlist;
fprintf os "}\n";
);
(***********************************************************)
(*************** VARIABLES *********************************)
(***********************************************************)
(* pour les dumps des vars support *)
(* Hashtbl.iter (print_support Local) (Expand.support_tab source_code); *)
let print_support nme = (
let info = Hashtbl.find (Expand.support_tab source_code) nme in
fprintf os " %s : %s"
(CoIdent.to_string nme)
(CkTypeEff.to_string info.si_type);
(* init ? *)
let _ = match info.si_init with
| None -> ()
| Some e -> (
fprintf os " ~init (";
CoAlgExp.lus_dumpf os e ;
fprintf os ")"
) in
(* default ? *)
let _ = match info.si_default with
| None -> ()
| Some e -> (
fprintf os " ~default (";
CoAlgExp.lus_dumpf os e ;
fprintf os ")"
) in
fprintf os ";\n"
) in
(* pour les dumps de la liste d'alias *)
let print_alias nme = (
let info = Hashtbl.find
(Expand.alias_tab source_code) nme in
fprintf os " %s : %s"
(CoIdent.to_string nme)
(CkTypeEff.to_string info.ai_type);
fprintf os " ~alias " ;
print_algexp os info.ai_def_exp;
fprintf os ";\n"
) in
let print_counter (nme: CoIdent.t) = (
fprintf os " %s : %s"
(CoIdent.to_string nme)
(CkTypeEff.to_string CkTypeEff.integer);
fprintf os " ~init 0 ";
fprintf os " ~default (";
let precpt = CoAlgExp.of_pre nme CkTypeEff.integer in
CoAlgExp.lus_dumpf os precpt;
fprintf os ");\n"
) in
(* ENTRES *)
fprintf os "inputs {\n" ;
(* Hashtbl.iter (print_support Input) (Expand.support_tab source_code); *)
List.iter print_support (Expand.input_list source_code);
fprintf os "}\n";
(* SORTIES *)
fprintf os "outputs {\n" ;
(* Hashtbl.iter (print_support Output) (Expand.support_tab source_code); *)
List.iter print_support (Expand.output_list source_code);
fprintf os "}\n";
(* les LOCALES lucky regroupent : *)
fprintf os "locals {\n" ;
(* - les variables support "Local" (de source_code) *)
(* Hashtbl.iter (print_support Local) (Expand.support_tab source_code); *)
List.iter print_support (Expand.local_list source_code);
(* - les alias (de source_code) *)
List.iter print_alias (Expand.alias_list source_code);
(* - les compteurs de boucles (de auto) *)
List.iter print_counter (AutoExplore.counters auto);
fprintf os "}\n";
(***********************************************************)
(*************** ETATS *************************************)
(***********************************************************)
let print_state (nme: string) (info: AutoExplore.state_info) = (
match info with
AutoExplore.SS_transient -> (
fprintf os " %s : transient;\n" nme
) |
AutoExplore.SS_final _ -> (
fprintf os " %s : final;\n" nme
) |
AutoExplore.SS_stable tracexp -> (
fprintf os " %s : stable;\n" nme
)
) in
fprintf os "nodes {\n" ;
Hashtbl.iter print_state (AutoExplore.states auto) ;
fprintf os "}\n" ;
fprintf os "start_node { %s }\n" (AutoExplore.init_state auto) ;
(***********************************************************)
(*************** TRANSITIONS *******************************)
(***********************************************************)
(* on fabrique le "and" et on omprime ... *)
let print_and_form flist = (
let rec makeand = ( function
[f] -> f
| f::fl -> CoAlgExp.of_and f (makeand fl)
| _ -> assert false
) in
print_algexp os (makeand flist)
) in
let print_trans t = (
fprintf os " %s -> %s" t.src t.dest;
let _ = match t.wgt with
None -> ()
| Some w -> (
fprintf os "\n ~weight ";
match w with
| AutoExplore.W_huge -> fprintf os "infinity"
| AutoExplore.W_exp e -> print_algexp os e ;
) in
let _ = match t.form with
[] -> ()
| flist -> (
fprintf os "\n ~cond ";
print_and_form flist
) in
fprintf os ";\n"
) in
fprintf os "transitions {\n" ;
List.iter print_trans (AutoExplore.transitions auto);
fprintf os "}\n" ;
)
(** COMPILATION/GENERATION D'AUTOMATE :
------------------------------------------------------------
Traduction de la structure AutoGen.t en lucky.
----------------------------------------------------------*)
val make : string -> AutoExplore.t -> Pervasives.out_channel -> unit
This diff is collapsed.
(** COMPILATION/GENERATION D'AUTOMATE : interface
------------------------------------------------------------
La génération d'automate intervient après l'expansion, qui
a produit les infos suivantes :
_support_tab : (CoIdent.t, support_info) Hashtbl.t
_alias_tab : (CoIdent.t, alias_info) Hashtbl.t
_trace_tab : (CoIdent.t, trace_info) Hashtbl.t
_main_trace : CoIdent.t
Les exceptions ont été expansées en place, par des identificateurs
uniques dans le expressions associées. Il n'y a donc pas de table
pour elles.
----------------------------------------------------------*)
(** le type du résultat *)
type weightexp =
| W_huge
| W_exp of CoAlgExp.t
(* obsolete
val algexp_of_weight: weightexp -> CoAlgExp.t
*)
(* gtree -> forme externe des transitions adaptée
à la génération de lurette *)
type gtree = string * gtree_node
and gtree_node =
| GT_leaf of (CoAlgExp.t list * string)
| GT_choice of (weightexp option * gtree) list
| GT_stop of string
(* trans -> forme externe des transitions
(liste de trans) adaptée à la génération de lucky *)
type trans = {
src: string;
wgt: weightexp option;
form: CoAlgExp.t list;
dest: string;
}
(** N.b. le CoTraceExp.t est l'expression lutin
EXPANSEE correspondant à l'état, c'est pas forcement tres
lisible => juste pour le debug ... *)
type state_info =
SS_stable of CoTraceExp.t
| SS_transient
| SS_final of string
(*
type t = {
(* le source expansé *)
source_code : Expand.t;
nb_stables : int;
nb_transients : int;
init_state : string;
final_state : string;
loop_counters : CoIdent.t list;
states : (string, state_info) Hashtbl.t ;
transitions : trans list;
}
*)
(* Abstrait ! *)
type t
val source : t -> Expand.t
val counters : t -> CoIdent.t list
val init_state : t -> string
val transitions : t -> trans list
(* Explore le sous-graphe du state *)
val state2gtree : t -> string -> gtree
val state2trans : t -> string -> trans list
(* Construit TOUT l'automate *)
val make : Expand.t -> t
val get_state_def : t -> string -> CoTraceExp.t
val get_state_info : t -> string -> state_info
(* Table des états connus *)
val states : t -> (string, state_info) Hashtbl.t
val dump : t -> unit
(*----------------------------------------------------------
TYPE/BINDING CHECK
------------------------------------------------------------
Table de symboles pour le check
---------------------------------------------------------------
C'est la structure qui permet :
- de réaliser le type/binding check (cf. CheckType)
- de conserver, après ce check, les infos calculées/inférées
Toute référence à un identificateur est identifiée
de manière UNIQUE par son ident (string + lexeme).
Au cours du check, on utilise TROIS tables :
- une table "dynamique" de scoping "string -> ident_info"
qui permet de résoudre les référence sous "scope"
- une table GLOBALE de binding "ident -> ident_info"
remplie au fur et à mesure que les références sont résolue
- une table de typage des "val_exp -> CkTypeEff.t"
n.b. les val_exp SONT identifiées de manière unique
par leur lexeme
-------------------------------------------------------------*)
open Hashtbl
open Lexeme
open Verbose
open Errors
open Format
open Syntaxe
(* sous-modules *)
open CkTypeEff
open CkIdentInfo
(*-------------------------------------------*)
(* CREATION DE L'ENVIRONNEMENT *)
(*-------------------------------------------*)
(* Il contient :
- une association (fluctuante au cours
du check) ident -> info
- une association globale entre les
val_exp et leur CkTypeEff.t
N.B. pour eviter tout problème de collision,
on passe via le lexeme (par définition unique)
asocié à la val_exp
*)
type t = {
ce_scope : (string, CkIdentInfo.t) Hashtbl.t ;
ce_binding : (Syntaxe.ident, CkIdentInfo.t) Hashtbl.t;
ce_typing : (Lexeme.t, CkTypeEff.t) Hashtbl.t
}
(* création *)
let create : unit -> t = (
fun () -> {
ce_scope = Hashtbl.create 200;
ce_binding = Hashtbl.create 200;
ce_typing = Hashtbl.create 200;
}
)
(*********************************************)
(* INTEROGATION DU TYPING *)
(*********************************************)
(*
Ne doit être utilisé QU'APRES le type/binding check !
Toute erreur est forcément un BUG !
*)
let get_exp_type (env : t) (e : Syntaxe.val_exp)
(* -> CkTypeEff.t *)
= (
try (
Hashtbl.find env.ce_typing e.src
) with Not_found -> (
raise (Internal_error
("CheckEnv.get_exp_type", "untyped exp"))
)
)
(*********************************************
AJOUT DU TYPING
Dans certains cas, une expression peut etre
partagee : cas typique de la valeur d'init
distribuee sur plusieurs vars !
*********************************************)
let set_exp_type (env : t) (ve: Syntaxe.val_exp) (tf: CkTypeEff.t) = (
(* assert (not (Hashtbl.mem env.ce_typing ve.src)); *)
try (
let t1 = Hashtbl.find env.ce_typing ve.src in
if (t1 <> tf) then (
let msg = Printf.sprintf "can't assign type '%s' to exp '%s', already typed with '%s'"
(CkTypeEff.to_string tf)
(Errors.lexeme_details ve.src)
(CkTypeEff.to_string t1)
in
Errors.print_internal_error "CheckEnv.set_exp_type" msg;
exit 1
)
) with Not_found ->
Hashtbl.add env.ce_typing ve.src tf
)
(*********************************************)
(* INTEROGATION DU BINDING *)
(*********************************************)
(*
Ne doit être utilisé QU'APRES le type/binding check !
Toute erreur est forcément un BUG !
*)
let get_binding (env : t) (id : Syntaxe.ident)
(* -> CkIdentInfo.t *)
= (
try (
Hashtbl.find env.ce_binding id
) with Not_found -> (
raise (Internal_error
("CheckEnv.get_binding",
"unbounded ident "^(Lexeme.to_string id.src)
))
)
)
(*********************************************)
(* MODIFICATION DU SCOPE *)
(*********************************************)
(*
Toutes modif DOIT passer par la fonction suivante
qui gère les problèmes de collision : si l'ident
est déjà "bindé" :
- erreur si hideable = false
- rien (ou warning ?) si hideable
*)
let put_in_scope (env: t) (id : Syntaxe.ident) (ii : CkIdentInfo.t) = (
( try (
let ifo = Hashtbl.find env.ce_scope id.it in
if (CkIdentInfo.is_hideable ifo) then (
Hashtbl.add env.ce_scope id.it ii ;
) else (
raise (Compile_error (id.src,
"declaration conflicts with a global one"
))
)
) with Not_found -> (
Hashtbl.add env.ce_scope id.it ii
));
(*
let bdgs = Hashtbl.find_all env.ce_scope id.it in
let pii ii = (printf " %s\n" (CkIdentInfo.to_string ii)) in
printf "CURRENT SCOPE: %s = \n" id.it ;
List.iter pii bdgs
*)
)
(*
clé pour la modif du scope : juste la liste des idents
*)
type scope_key = string list
let restore (env : t) (k : scope_key) = (
let rm_scope s = (
Hashtbl.remove env.ce_scope s
) in
List.iter rm_scope k
)
(*---------------------------------------------------
Ajout d'une cste abstraite dans le scope
=> global on n'a pas le droit de la redefinir
=> local on a le droit de la redefinir
---------------------------------------------------*)
let add_global_cst
(env: t)
(id: Syntaxe.ident)
(te: CkTypeEff.t) =
(
let ii = CkIdentInfo.of_global_cst id te in
put_in_scope env id ii;
[id.it]
)
let add_local_cst
(env: t)
(id: Syntaxe.ident)
(te: CkTypeEff.t) =
(
(* printf "add_local_cst: src=%s\n" (Lexeme.to_string id.src); *)
let ii = CkIdentInfo.of_local_cst id te in
put_in_scope env id ii;
(* printf "add_local_cst: def=%s\n" (CkIdentInfo.to_string ii); *)
[id.it]
)
(*---------------------------------------------------
Ajout de paramètres formels dans le scope
---------------------------------------------------*)
type typed_ids = (Syntaxe.ident * Syntaxe.type_exp) list
type eff_typed_ids = (Syntaxe.ident * CkTypeEff.t) list
let add_formal_params (env : t) (params : typed_ids option) = (
match params with
None -> []
| Some palist -> (
let k = ref [] in
let treat_param = function (i,t) -> (
let s = i.it in
let te = CkTypeEff.of_texp t in
let ii = CkIdentInfo.of_param i te in
(* ICI => warning shadow au cas ou ? *)
put_in_scope env i ii;
k := s::!k
) in
List.iter treat_param palist;
(* retourne la clé (liste des entrées) *)
!k
)
)
(*---------------------------------------------------
Ajout de variables support dans le scope
ELLES SONT IMPLICITEMENT MISES EN REF
Le type checking est déjà fait -> t est un CkTypeEff.t
---------------------------------------------------*)
let add_support_vars (env : t) (valist : eff_typed_ids) = (
let k = ref [] in
let treat_param = function (i,t) -> (
let s = i.it in
let te = CkTypeEff.ref_of t in
let ii = CkIdentInfo.of_support i te in
(* ICI => warning shadow au cas ou ? *)
put_in_scope env i ii;
k := s::!k
) in
List.iter treat_param valist;
(* retourne la clé (liste des entrées) *)
!k
)
let add_support_profile
(env : t)
(ins : eff_typed_ids)
(outs : eff_typed_ids) =
(
let ki = add_support_vars env ins in
let ko = add_support_vars env outs in
ki@ko
)
(*---------------------------------------------------
Ajout d'une macro dans le scope.
N.B. on distingue les macros avec
liste de param éventuellement vide
et les alias qui n'ont pas du tout
d'entrées (impornat pour l'expansion)
---------------------------------------------------*)
let add_let
(env: t)
(li : Syntaxe.let_info)
(tres : CkTypeEff.t)
(id : Syntaxe.ident) = (*unit*)
(
(* inutile ? let def = li.lti_def in *)
let ii = match li.lti_inputs with
None -> CkIdentInfo.of_alias id tres li
| Some inlist -> (
(* le profil ... *)
let teff_of_param = ( function
(_, te) -> CkTypeEff.of_texp te
) in
let tinlist = List.map teff_of_param inlist in
let prof = CkTypeEff.get_prof tinlist tres in
CkIdentInfo.of_macro id prof li
) in