From 670d8962dfd15e813b46afb2a40f36b2ceaae2ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Fri, 29 Apr 2011 15:12:24 +0200 Subject: [PATCH] add useful files --- .../analysis/{statefull.ml => stateful.ml} | 14 +-- compiler/heptagon/hept_utils.ml | 99 +++++++++++++++++++ compiler/heptagon/main/hept_compiler.ml | 2 +- 3 files changed, 102 insertions(+), 13 deletions(-) rename compiler/heptagon/analysis/{statefull.ml => stateful.ml} (93%) create mode 100644 compiler/heptagon/hept_utils.ml diff --git a/compiler/heptagon/analysis/statefull.ml b/compiler/heptagon/analysis/stateful.ml similarity index 93% rename from compiler/heptagon/analysis/statefull.ml rename to compiler/heptagon/analysis/stateful.ml index 98064d6..2daae49 100644 --- a/compiler/heptagon/analysis/statefull.ml +++ b/compiler/heptagon/analysis/stateful.ml @@ -21,8 +21,7 @@ type error = let message loc kind = begin match kind with | Eshould_be_a_node -> - Format.eprintf "%aThis node is stateful \ - but was declared stateless.@." + Format.eprintf "%aThis node is stateful but was declared stateless.@." print_location loc | Eexp_should_be_stateless -> Format.eprintf "%aThis expression should be stateless.@." @@ -30,16 +29,7 @@ let message loc kind = end; raise Errors.Error - -let stateful_mapfold f acc l = - let map_or (l,acc) e = - let e,acc' = f false e in - e::l, acc or acc' - in - let l,acc = List.fold_left map_or ([],acc) l in - List.rev l, acc - - +(* a last is stateful *) let last _ stateful l = match l with | Var -> l, stateful | Last _ -> l, true diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml new file mode 100644 index 0000000..8953540 --- /dev/null +++ b/compiler/heptagon/hept_utils.ml @@ -0,0 +1,99 @@ +(**************************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Author : Marc Pouzet *) +(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) +(* *) +(**************************************************************************) +(* the internal representation *) +open Location +open Misc +open Names +open Idents +open Static +open Signature +open Types +open Clocks +open Initial +open Heptagon + +(* Helper functions to create AST. *) +let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = + { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; + e_base_ck = Cbase; e_loc = loc; } + +let mk_app ?(params=[]) ?(unsafe=false) op = + { a_op = op; a_params = params; a_unsafe = unsafe } + +let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = + Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset) + +let mk_type_dec name desc = + { t_name = name; t_desc = desc; t_loc = no_location; } + +let mk_equation ?(loc=no_location) desc = + let _, s = Stateful.eqdesc Stateful.funs false desc in + { eq_desc = desc; + eq_stateful = s; + eq_loc = loc; } + +let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty = + { v_ident = name; v_type = ty; v_clock = clock; + v_last = last; v_loc = no_location } + +let mk_block ?(stateful = true) ?(defnames = Env.empty) ?(locals = []) eqs = + { b_local = locals; b_equs = eqs; b_defnames = defnames; + b_stateful = stateful; b_loc = no_location; } + +let dfalse = + mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) +let dtrue = + mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) + +let mk_ifthenelse e1 e2 e3 = + { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] } + +let mk_simple_equation pat e = + mk_equation (Eeq(pat, e)) + +let mk_switch_equation e l = + mk_equation (Eswitch (e, l)) + +let mk_signature name ins outs stateful params loc = + { sig_name = name; + sig_inputs = ins; + sig_stateful = stateful; + sig_outputs = outs; + sig_params = params; + sig_loc = loc } + +let mk_node + ?(input = []) ?(output = []) ?(contract = None) ?(local = []) + ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = []) + name block = + { n_name = name; + n_stateful = stateful; + n_input = input; + n_output = output; + n_contract = contract; + n_block = block; + n_loc = loc; + n_params = param; + n_params_constraints = constraints } + +(** @return the set of variables defined in [pat]. *) +let vars_pat pat = + let rec _vars_pat locals acc = function + | Evarpat x -> + if (IdentSet.mem x locals) or (IdentSet.mem x acc) + then acc + else IdentSet.add x acc + | Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list + in _vars_pat IdentSet.empty IdentSet.empty pat + +(** @return whether an object of name [n] belongs to + a list of [var_dec]. *) +let rec vd_mem n = function + | [] -> false + | vd::l -> vd.v_ident = n or (vd_mem n l) diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index f3a31cd..be145f9 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -16,7 +16,7 @@ let pp p = if !verbose then Hept_printer.print stdout p let compile_program p = (* Typing *) - let p = silent_pass "Statefullness check" true Statefull.program p in + let p = silent_pass "Statefulness check" true Stateful.program p in let p = pass "Typing" true Typing.program p pp in if !print_types then print_interface Format.std_formatter;