700 lines
17 KiB
OCaml
700 lines
17 KiB
OCaml
(**************************************************************************)
|
|
(* *)
|
|
(* Lucid Synchrone *)
|
|
(* *)
|
|
(* Author : Marc Pouzet *)
|
|
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
|
(* *)
|
|
(**************************************************************************)
|
|
|
|
(* $Id: declarative_printer.ml,v 1.13 2007-01-11 07:35:53 pouzet Exp $ *)
|
|
|
|
open Misc
|
|
open Names
|
|
open Declarative
|
|
open Modules
|
|
open Format
|
|
|
|
(* generic printing of a list *)
|
|
let print_list print l =
|
|
let rec printrec l =
|
|
match l with
|
|
[] -> ()
|
|
| [x] ->
|
|
print x
|
|
| x::l ->
|
|
print x;
|
|
print_space ();
|
|
printrec l in
|
|
printrec l
|
|
|
|
(* local name *)
|
|
let print_name i =
|
|
print_string "/";print_int i
|
|
|
|
(* global names *)
|
|
let print_qualified_ident { qual = q; id = id } =
|
|
if (q = pervasives_module) or (q = compiled_module_name ())
|
|
or (q = "")
|
|
then print_string id
|
|
else
|
|
begin
|
|
print_string q;
|
|
print_string ".";
|
|
print_string id
|
|
end
|
|
|
|
(* print types *)
|
|
let rec print_type typ =
|
|
open_box 1;
|
|
begin match typ with
|
|
Darrow(is_node, typ1, typ2) ->
|
|
print_string "(";
|
|
if is_node then print_string "=>" else print_string "->";
|
|
print_space ();
|
|
print_list print_type [typ1;typ2];
|
|
print_string ")"
|
|
| Dproduct(ty_list) ->
|
|
print_string "(";
|
|
print_string "*";
|
|
print_space ();
|
|
print_list print_type ty_list;
|
|
print_string ")"
|
|
| Dconstr(qual_ident, ty_list) ->
|
|
if ty_list <> [] then print_string "(";
|
|
print_qualified_ident qual_ident;
|
|
if ty_list <> [] then
|
|
begin print_space ();
|
|
print_list print_type ty_list;
|
|
print_string ")"
|
|
end
|
|
| Dsignal(ty) -> print_type ty; print_space (); print_string "sig"
|
|
| Dtypvar(i) -> print_int i
|
|
| Dbase(b) -> print_base_type b
|
|
end;
|
|
close_box ()
|
|
|
|
and print_base_type b =
|
|
match b with
|
|
Dtyp_bool -> print_string "bool"
|
|
| Dtyp_int -> print_string "int"
|
|
| Dtyp_float -> print_string "float"
|
|
| Dtyp_unit -> print_string "unit"
|
|
| Dtyp_string -> print_string "string"
|
|
| Dtyp_char -> print_string "char"
|
|
|
|
let print_typs (Dtypforall(l, typ)) =
|
|
match l with
|
|
[] -> (* we do not print the quantifier when there is no type variable *)
|
|
print_type typ
|
|
| l ->
|
|
open_box 1;
|
|
print_string "(forall";
|
|
print_space ();
|
|
print_list print_name l;
|
|
print_space ();
|
|
print_type typ;
|
|
print_string ")";
|
|
close_box ()
|
|
|
|
(* print clocks *)
|
|
let rec print_clock clk =
|
|
match clk with
|
|
| Dfalse -> print_string "false"
|
|
| Dtrue -> print_string "true"
|
|
| Dclockvar(i) -> print_name i
|
|
| Don(b, clk, c) ->
|
|
print_string "(";
|
|
if b then print_string "on" else print_string "onot";
|
|
print_space ();
|
|
print_clock clk;
|
|
print_space ();
|
|
print_carrier c;
|
|
print_string ")"
|
|
and print_carrier c =
|
|
match c with
|
|
Dcfalse -> print_string "false"
|
|
| Dctrue -> print_string "true"
|
|
| Dcvar(i) -> print_name i
|
|
| Dcglobal(qual_ident, res, clk) ->
|
|
print_qualified_ident qual_ident;
|
|
print_string "(";
|
|
(match res with
|
|
None -> ()
|
|
| Some(n) -> print_space ();print_name n;print_space ());
|
|
print_clock clk;
|
|
print_string ")"
|
|
|
|
(* immediate values *)
|
|
let print_immediate i =
|
|
match i with
|
|
Dbool(b) -> print_string (if b then "true" else "false")
|
|
| Dint(i) -> print_int i
|
|
| Dfloat(f) -> print_float f
|
|
| Dchar(c) -> print_char c
|
|
| Dstring(s) -> print_string s
|
|
| Dvoid -> print_string "()"
|
|
|
|
(* print patterns *)
|
|
let atom_pat pat =
|
|
match pat with
|
|
Dconstantpat _ | Dvarpat _ | Dwildpat -> true
|
|
| _ -> false
|
|
|
|
let rec print_pat pat =
|
|
open_box 1;
|
|
if not (atom_pat pat) then print_string "(";
|
|
begin match pat with
|
|
Dwildpat -> print_string "_"
|
|
| Dconstantpat(i) -> print_immediate i
|
|
| Dvarpat(i) -> print_name i
|
|
| Dconstructpat(qual_ident, pat_list) ->
|
|
print_string "constr";
|
|
print_space ();
|
|
print_qualified_ident qual_ident;
|
|
if pat_list <> [] then print_space ();
|
|
print_list print_pat pat_list
|
|
| Dtuplepat(pat_list) ->
|
|
print_string ",";
|
|
print_space ();
|
|
print_list print_pat pat_list
|
|
| Drecordpat(l) ->
|
|
print_string "record";
|
|
print_list
|
|
(fun (qual_ident, pat) ->
|
|
open_box 1;
|
|
print_string "(";
|
|
print_qualified_ident qual_ident;
|
|
print_space ();
|
|
print_pat pat;
|
|
print_string ")";
|
|
close_box ()) l
|
|
| Dorpat(pat1, pat2) ->
|
|
print_string "orpat";
|
|
print_space ();
|
|
print_list print_pat [pat1;pat2]
|
|
| Daliaspat(pat, i) ->
|
|
print_string "as";
|
|
print_space ();
|
|
print_pat pat;
|
|
print_space ();
|
|
print_int i
|
|
end;
|
|
if not (atom_pat pat) then print_string ")";
|
|
close_box ()
|
|
|
|
(* print statepat *)
|
|
let print_statepat (s, l) =
|
|
match l with
|
|
[] -> print_string s
|
|
| l -> print_string "(";
|
|
print_string s;
|
|
print_space ();
|
|
print_list print_pat l;
|
|
print_string ")"
|
|
|
|
(* print expressions *)
|
|
let atom e =
|
|
match e.d_desc with
|
|
Dconstant _ -> true
|
|
| _ -> false
|
|
|
|
(* print variables *)
|
|
let print_var v =
|
|
match v with
|
|
Dlocal(n) ->
|
|
print_string "local";
|
|
print_space ();
|
|
print_name n
|
|
| Dglobal(qual_ident) ->
|
|
print_string "global";
|
|
print_space ();
|
|
print_qualified_ident qual_ident
|
|
|
|
let rec print e =
|
|
open_box 1;
|
|
if not (atom e) then print_string "(";
|
|
begin match e.d_desc with
|
|
Dconstant(i) -> print_immediate i
|
|
| Dvar(v, subst) ->
|
|
print_var v;
|
|
print_subst subst
|
|
| Dlast(i) ->
|
|
print_string "last";
|
|
print_space ();
|
|
print_name i
|
|
| Dpre(opt_default, e) ->
|
|
print_string "pre";
|
|
print_space ();
|
|
begin match opt_default with
|
|
None -> print e
|
|
| Some(default) ->
|
|
print default; print_space (); print e
|
|
end
|
|
| Dinit(ck, None) ->
|
|
print_string "init";
|
|
print_space ();
|
|
print_clock ck
|
|
| Dinit(ck, Some(n)) ->
|
|
print_string "init";
|
|
print_space ();
|
|
print_clock ck;
|
|
print_space ();
|
|
print_name n
|
|
| Difthenelse(e0,e1,e2) ->
|
|
print_string "if";
|
|
print_space ();
|
|
print e0;
|
|
print_space ();
|
|
print e1;
|
|
print_space ();
|
|
print e2
|
|
| Dtuple(l) ->
|
|
print_string ",";
|
|
print_space ();
|
|
print_list print l
|
|
| Dconstruct(qual_ident,l) ->
|
|
print_string "constr";
|
|
print_space ();
|
|
print_qualified_ident qual_ident;
|
|
if l <> [] then print_space ();
|
|
print_list print l
|
|
| Dprim(qual_ident, l) ->
|
|
print_string "(";
|
|
print_qualified_ident qual_ident;
|
|
print_space ();
|
|
print_list print l;
|
|
print_string ")"
|
|
| Drecord(l) ->
|
|
print_string "record";
|
|
print_space ();
|
|
print_list (fun (qual_ident, e) ->
|
|
open_box 1;
|
|
print_string "(";
|
|
print_qualified_ident qual_ident;
|
|
print_space ();
|
|
print e;
|
|
print_string ")";
|
|
close_box ()) l
|
|
| Drecord_access(e,qual_ident) ->
|
|
print_string "access";
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_qualified_ident qual_ident
|
|
| Dfun(is_state, params, args, block, e) ->
|
|
print_string ("fun" ^ (if is_state then "(s)" else "(c)"));
|
|
print_space ();
|
|
print_params params;
|
|
print_space ();
|
|
print_list print_pat args;
|
|
print_space ();
|
|
print_block block;
|
|
print_space ();
|
|
print_string "return ";
|
|
print e
|
|
| Dapply(is_state, f, e_list) ->
|
|
print_string ("apply" ^ (if is_state then "(s)" else "(c)"));
|
|
print_space ();
|
|
print f;
|
|
print_space ();
|
|
print_list print e_list
|
|
| Dlet(block, e) ->
|
|
print_string "let";
|
|
print_space ();
|
|
print_block block;
|
|
print_space ();
|
|
print e
|
|
| Deseq(e1, e2) ->
|
|
print_string "seq";
|
|
print_space ();
|
|
print e1;
|
|
print_space ();
|
|
print e2
|
|
| Dtest(e1) ->
|
|
print_string "test";
|
|
print_space ();
|
|
print e1
|
|
| Dwhen(e1) ->
|
|
print_string "when";
|
|
print_space ();
|
|
print e1
|
|
| Dclock(ck) ->
|
|
print_string "clock";
|
|
print_space ();
|
|
print_clock ck
|
|
end;
|
|
if not (atom e) then print_string ")";
|
|
close_box()
|
|
|
|
and print_block b =
|
|
(* print variable definitions *)
|
|
let print_env env =
|
|
open_box 1;
|
|
print_string "(env";
|
|
print_space ();
|
|
Hashtbl.iter (fun i ident -> print_ident ident;print_space ()) env;
|
|
print_string ")";
|
|
close_box () in
|
|
(* main function *)
|
|
open_box 1;
|
|
print_string "(";
|
|
(* environment *)
|
|
print_env b.b_env;
|
|
print_space ();
|
|
(* equations *)
|
|
print_equation b.b_equations;
|
|
print_space ();
|
|
(* write variables *)
|
|
print_string "(write";
|
|
print_space ();
|
|
print_list print_name b.b_write;
|
|
print_string ")";
|
|
print_string ")";
|
|
close_box ()
|
|
|
|
(* print ident declarations *)
|
|
(* e.g, "(kind x/412 (int) (cl) (write) (last) (signal) (= 412))" *)
|
|
and print_ident id =
|
|
let print_kind () =
|
|
match id.id_kind with
|
|
Kinit -> print_string "init"
|
|
| Kclock -> print_string "clock"
|
|
| Kmemo -> print_string "memo"
|
|
| Kstatic -> print_string "static"
|
|
| Klast -> print_string "last"
|
|
| Kreset -> print_string "reset"
|
|
| Kvalue -> print_string "value"
|
|
| Kinput -> print_string "input"
|
|
| Kshared -> print_string "shared" in
|
|
let print_name () =
|
|
begin match id.id_original with
|
|
None -> ()
|
|
| Some(s) -> print_string s
|
|
end;
|
|
print_name id.id_name in
|
|
let print_typs () =
|
|
print_string "(";
|
|
print_typs id.id_typ;
|
|
print_string ")" in
|
|
let print_write () =
|
|
if id.id_write then
|
|
begin print_space (); print_string "(write)" end in
|
|
let print_last () =
|
|
if id.id_last then
|
|
begin print_space (); print_string "(last)" end in
|
|
let print_signal () =
|
|
if id.id_signal then
|
|
begin print_space (); print_string "(signal)" end in
|
|
let print_expr () =
|
|
match id.id_value with
|
|
None -> ()
|
|
| Some(e) ->
|
|
print_space ();print_string "(= "; print e; print_string ")" in
|
|
(* main function *)
|
|
open_box 1;
|
|
print_string "(";
|
|
print_kind ();
|
|
print_space ();
|
|
print_name ();
|
|
print_space ();
|
|
print_typs ();
|
|
print_space ();
|
|
print_write ();
|
|
print_last ();
|
|
print_signal ();
|
|
print_expr ();
|
|
print_string ")";
|
|
close_box ()
|
|
|
|
(* prints a sequence of sets of parallel equations *)
|
|
and print_equation eq =
|
|
open_box 1;
|
|
print_string "(";
|
|
begin match eq with
|
|
Dequation(pat, e) ->
|
|
print_string "let";
|
|
print_space ();
|
|
print_pat pat;
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_clock e.d_guard
|
|
| Dlasteq(n, e) ->
|
|
print_string "last";
|
|
print_space ();
|
|
print_name n;
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_clock e.d_guard
|
|
| Demit(pat, e) ->
|
|
print_string "emit";
|
|
print_space ();
|
|
print_pat pat;
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_clock e.d_guard
|
|
| Dstatic(pat, e) ->
|
|
print_string "static";
|
|
print_space ();
|
|
print_pat pat;
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_clock e.d_guard
|
|
| Dnext(n, e) ->
|
|
print_string "next";
|
|
print_space ();
|
|
print_name n;
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_clock e.d_guard
|
|
| Dget(pat, v) ->
|
|
print_string "get";
|
|
print_space ();
|
|
print_pat pat;
|
|
print_space ();
|
|
print_var v
|
|
| Dwheneq(eq, clk) ->
|
|
print_string "when";
|
|
print_space ();
|
|
print_clock clk;
|
|
print_space ();
|
|
print_equation eq
|
|
| Dmerge(is_static, e, pat_block_list) ->
|
|
print_string "merge";
|
|
print_space ();
|
|
if is_static then print_string "static"
|
|
else print_clock e.d_guard;
|
|
print_space ();
|
|
print e;
|
|
print_space ();
|
|
print_list (fun (pat, block) ->
|
|
open_box 1;
|
|
print_string "(";
|
|
print_pat pat;
|
|
print_space ();
|
|
print_block block;
|
|
print_string ")";
|
|
close_box ()) pat_block_list
|
|
| Dpresent(ck, scondpat_block_list, block) ->
|
|
print_string "present";
|
|
print_space ();
|
|
print_clock ck;
|
|
print_space ();
|
|
print_list (fun (scondpat, block) ->
|
|
open_box 1;
|
|
print_string "(";
|
|
print_spat scondpat;
|
|
print_space ();
|
|
print_block block;
|
|
print_string ")";
|
|
close_box ()) scondpat_block_list;
|
|
print_space ();
|
|
print_block block
|
|
| Dreset(eq, e) ->
|
|
print_string "reset";
|
|
print_space ();
|
|
print_equation eq;
|
|
print_space ();
|
|
print e
|
|
| Dautomaton(ck, handlers) ->
|
|
print_string "automaton";
|
|
print_space ();
|
|
print_clock ck;
|
|
print_space ();
|
|
print_list print_handler handlers
|
|
| Dpar(eq_list) ->
|
|
print_string "par";
|
|
print_space ();
|
|
print_list print_equation eq_list
|
|
| Dseq(eq_list) ->
|
|
print_string "seq";
|
|
print_space ();
|
|
print_list print_equation eq_list
|
|
| Dblock(b) ->
|
|
print_string "block";
|
|
print_space ();
|
|
print_block b
|
|
end;
|
|
print_string ")";
|
|
close_box ()
|
|
|
|
(* print the handlers of an automaton *)
|
|
and print_handler (statepat, b_weak, b_strong, weak_escape, strong_escape) =
|
|
open_box 1;
|
|
print_string "(state";
|
|
print_space ();
|
|
print_statepat statepat;
|
|
print_space ();
|
|
print_block b_weak;
|
|
print_space ();
|
|
print_block b_strong;
|
|
print_space ();
|
|
print_string "(weak ";
|
|
print_escape weak_escape;
|
|
print_string ")";
|
|
print_space ();
|
|
print_string "(strong ";
|
|
print_escape weak_escape;
|
|
print_string ")";
|
|
print_string ")";
|
|
close_box ()
|
|
|
|
and print_escape escape_list =
|
|
print_list
|
|
(fun (spat, b, is_continue, state) ->
|
|
print_string "(";
|
|
if is_continue then print_string "continue " else print_string "then ";
|
|
print_spat spat;
|
|
print_space ();
|
|
print_block b;
|
|
print_space ();
|
|
print_state state;
|
|
print_string ")")
|
|
escape_list;
|
|
close_box ()
|
|
|
|
|
|
(* print type and clock instance *)
|
|
and print_subst { s_typ = st; s_clock = scl; s_carrier = sc } =
|
|
match st, scl, sc with
|
|
[],[],[] -> ()
|
|
| l1,l2,l3 ->
|
|
print_string "[";
|
|
print_list print_type l1;
|
|
print_string "]";
|
|
print_space ();
|
|
print_string "[";
|
|
print_list print_clock l2;
|
|
print_string "]";
|
|
print_space ();
|
|
print_string "[";
|
|
print_list print_carrier l3;
|
|
print_string "]";
|
|
|
|
and print_params { s_typ = pt; s_clock = pcl; s_carrier = pc } =
|
|
match pt, pcl, pc with
|
|
[],[],[] -> ()
|
|
| l1,l2,l3 ->
|
|
print_string "[";
|
|
print_list print_name l1;
|
|
print_string "]";
|
|
print_space ();
|
|
print_string "[";
|
|
print_list print_name l2;
|
|
print_string "]";
|
|
print_space ();
|
|
print_string "[";
|
|
print_list print_name l3;
|
|
print_string "]"
|
|
|
|
and print_state (s, l) =
|
|
match l with
|
|
[] -> print_string s
|
|
| l -> print_string "(";
|
|
print_string s;
|
|
print_space ();
|
|
print_list print l;
|
|
print_string ")"
|
|
|
|
and atom_spat spat =
|
|
match spat with
|
|
Dexppat _ | Dcondpat _ -> true
|
|
| _ -> false
|
|
|
|
and print_spat spat =
|
|
open_box 1;
|
|
if not (atom_spat spat) then print_string "(";
|
|
begin match spat with
|
|
Dandpat(spat1, spat2) ->
|
|
print_string "& ";
|
|
print_spat spat1;
|
|
print_space ();
|
|
print_spat spat2
|
|
| Dexppat(e) ->
|
|
print e
|
|
| Dcondpat(e, pat) ->
|
|
print_string "is ";
|
|
print e;
|
|
print_space ();
|
|
print_pat pat
|
|
end;
|
|
if not (atom_spat spat) then print_string ")";
|
|
close_box ()
|
|
|
|
(* the main entry for printing definitions *)
|
|
let print_definition (name, e) =
|
|
open_box 2;
|
|
print_string "(def ";
|
|
if is_an_infix_or_prefix_operator name
|
|
then begin print_string "( "; print_string name; print_string " )" end
|
|
else print_string name;
|
|
print_space ();
|
|
print e;
|
|
print_string ")";
|
|
print_newline ();
|
|
close_box ()
|
|
|
|
(* print types *)
|
|
let print_variant (qualid, { arg = typ_list; res = typ }) =
|
|
print_string "(";
|
|
print_qualified_ident qualid;
|
|
print_string "(";
|
|
print_list print_type typ_list;
|
|
print_string ")";
|
|
print_space ();
|
|
print_type typ;
|
|
print_string ")"
|
|
|
|
let print_record (qualid, is_mutable, { arg = typ1; res = typ2 }) =
|
|
print_string "(";
|
|
if is_mutable then print_string "true" else print_string "false";
|
|
print_space ();
|
|
print_qualified_ident qualid;
|
|
print_space ();
|
|
print_type typ1;
|
|
print_space ();
|
|
print_type typ2;
|
|
print_string ")"
|
|
|
|
let print_type_declaration s { d_type_desc = td; d_type_arity = arity } =
|
|
open_box 2;
|
|
print_string "(type[";
|
|
print_list print_name arity;
|
|
print_string "]";
|
|
print_space ();
|
|
print_string s;
|
|
print_space ();
|
|
begin match td with
|
|
Dabstract_type -> ()
|
|
| Dabbrev(ty) ->
|
|
print_type ty
|
|
| Dvariant_type variant_list ->
|
|
List.iter print_variant variant_list
|
|
| Drecord_type record_list ->
|
|
List.iter print_record record_list
|
|
end;
|
|
print_string ")";
|
|
print_newline ();
|
|
close_box ();;
|
|
|
|
(* the main functions *)
|
|
set_max_boxes max_int ;;
|
|
|
|
let output_equations oc eqs =
|
|
set_formatter_out_channel oc;
|
|
List.iter print_equation eqs
|
|
|
|
let output oc declarative_code =
|
|
set_formatter_out_channel oc;
|
|
(* print type declarations *)
|
|
Hashtbl.iter print_type_declaration declarative_code.d_types;
|
|
(* print value definitions *)
|
|
List.iter print_definition declarative_code.d_code;
|
|
print_flush ()
|
|
|