async constants.

compiler/global/global_compare.ml

@@ -83,7 +83,10 @@ let rec static_exp_compare se1 se2 =
       | Sfield _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _) -> -1
       | Sfield _, _ -> 1
 
-      | Stuple _, (Srecord _ | Sop _ | Sarray _ | Sarray_power _) -> 1
+      | Sasync _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ | Sfield _) -> -1
+      | Sasync _, _ -> 1
+
+      | Stuple _, (Srecord _ | Sop _ | Sarray _ | Sarray_power _ ) -> 1
       | Stuple _, _ -> -1
 
       | Sarray_power _, (Srecord _ | Sop _ | Sarray _) -> -1

compiler/global/global_mapfold.ml

@@ -49,6 +49,9 @@ and static_exp_desc funs acc sd = match sd with
         (f, se), acc in
       let f_se_l, acc = mapfold aux acc f_se_l in
       Srecord f_se_l, acc
+  | Sasync se ->
+      let se, acc = static_exp_it funs acc se in
+      Sasync se, acc
 
 
 and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t

compiler/global/global_printer.ml

@@ -62,6 +62,7 @@ let rec print_static_exp ff se = match se.se_desc with
   | Srecord f_se_list ->
       print_record (print_couple print_qualname
                       print_static_exp """ = """) ff f_se_list
+  | Sasync se -> fprintf ff "@[<2>async %a@]" print_static_exp se
 
 and print_static_exp_tuple ff l =
   fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l

compiler/global/modules.ml

@@ -165,7 +165,7 @@ let add_const f v =
 let replace_value f v =
   g_env.values <- QualEnv.add f v g_env.values
 
-(** { 3 Find functions look in the global environnement, nothing more } *)
+(** { 3 Find functions look in the global environement, nothing more } *)
 
 let find_value x = QualEnv.find x g_env.values
 let find_type x = QualEnv.find x g_env.types

compiler/global/static.ml

@@ -74,6 +74,8 @@ let eval_core eval apply_op env se = match se.se_desc with
   | Srecord f_se_list ->
       { se with se_desc = Srecord
           (List.map (fun (f,se) -> f, eval env se) f_se_list) }
+  | Sasync se' ->
+      { se with se_desc = Sasync (eval env se') }
 
 (** [simplify env e] returns e simplified with the
     variables values taken from [env] or from the global env with [find_const].

compiler/global/types.ml

@@ -27,6 +27,7 @@ and static_exp_desc =
   | Sarray of static_exp list (** [ e1, e2, e3 ] *)
   | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *)
   | Sop of fun_name * static_exp list (** defined ops for now in pervasives *)
+  | Sasync of static_exp
 
 and ty =
   | Tprod of ty list (** Product type used for tuples *)

compiler/heptagon/analysis/typing.ml

@@ -449,6 +449,9 @@ and typing_static_exp const_env se =
             List.map (typing_static_field const_env fields
                         (Tid q)) f_se_list in
           Srecord f_se_list, Tid q
+     | Sasync se ->
+          let typed_se, ty = typing_static_exp const_env se in
+          Sasync typed_se, Tasync ((),ty)
   in
    { se with se_ty = ty; se_desc = desc }, ty
 

compiler/heptagon/parsing/hept_parser.mly

@@ -427,6 +427,7 @@ simple_exp:
 _simple_exp:
   | IDENT                            { Evar $1 }
   | const                            { Econst $1 }
+  | ASYNC c=const                    { Econst (mk_static_exp (Sasync c) (Loc($startpos,$endpos))) }
   | LBRACE field_exp_list RBRACE     { Estruct $2 }
   | LBRACKET array_exp_list RBRACKET { mk_call Earray $2 }
   | LPAREN tuple_exp RPAREN          { mk_call Etuple $2 }
@@ -555,14 +556,14 @@ qualname:
 ;
 
 
-const: c=_const { mk_static_exp c (Loc($startpos,$endpos)) }
+const:
+  | c=_const { mk_static_exp c (Loc($startpos,$endpos)) }
 _const:
-  | INT         { Sint $1 }
-  | FLOAT       { Sfloat $1 }
-  | BOOL        { Sbool $1 }
-  | constructor { Sconstructor $1 }
-  | q=qualified (ident)
-      { Svar q }
+  | INT                { Sint $1 }
+  | FLOAT              { Sfloat $1 }
+  | BOOL               { Sbool $1 }
+  | constructor        { Sconstructor $1 }
+  | q=qualified(ident) { Svar q }
 ;
 
 tuple_exp:

compiler/heptagon/parsing/hept_parsetree.ml

@@ -49,6 +49,7 @@ and static_exp_desc =
   | Sarray of static_exp list (** [ e1, e2, e3 ] *)
   | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *)
   | Sop of fun_name * static_exp list (** defined ops for now in pervasives *)
+  | Sasync of static_exp
 
 type iterator_type =
   | Imap

compiler/heptagon/parsing/hept_parsetree_mapfold.ml

@@ -104,6 +104,9 @@ and static_exp_desc funs acc sd = match sd with
         (f, se), acc in
       let f_se_l, acc = mapfold aux acc f_se_l in
       Srecord f_se_l, acc
+  | Sasync se ->
+      let se, acc = static_exp_it funs acc se in
+      Sasync se, acc
 
 
 and exp_it funs acc e = funs.exp funs acc e

compiler/heptagon/parsing/hept_scoping.ml

@@ -201,6 +201,7 @@ and translate_static_exp_desc ed =
         let qualf (f, se) = (qualify_field f, t se) in
         Types.Srecord (List.map qualf se_f_list)
     | Sop (fn, se_list) -> Types.Sop (qualify_value fn, List.map t se_list)
+    | Sasync se -> Types.Sasync (t se)
 
 let expect_static_exp e = match e.e_desc with
   | Econst se -> translate_static_exp se

compiler/minils/main/mls2seq.ml

@@ -18,6 +18,7 @@ open Misc
     with or without static parameters *)
 type target =
   | Obc of (Obc.program -> unit)
+  | Obc_scalar of (Obc.program -> unit)
   | Obc_no_params of (Obc.program -> unit)
   | Minils of (Minils.program -> unit)
   | Minils_no_params of (Minils.program -> unit)
@@ -39,7 +40,7 @@ let write_obc_file p =
     comment "Generation of Obc code"
 
 let targets = [ (*"c", Obc_no_params Cmain.program;*)
-                "java", Obc Java_main.program;
+                "java", Obc_scalar Java_main.program;
                 "obc", Obc write_obc_file;
                 "obc_np", Obc_no_params write_obc_file;
                 "epo", Minils write_object_file ]
@@ -65,10 +66,17 @@ let generate_target p s =
         let p_list = Callgraph.program p in
         let o_list = List.map Mls2obc.program p_list in
         print_unfolded p_list;
-        comment "Translation to Obc";
+        comment "Obc Callgraph";
         if !verbose then
           List.iter (Obc_printer.print stdout) o_list;
         List.iter convert_fun o_list
+    | Obc_scalar convert_fun ->
+        let o = Mls2obc.program p in
+        comment "Obc Scalarize";
+        let o_s = Scalarize.program o in
+        convert_fun o;
+        if !verbose then Obc_printer.print stdout o_s
+
 
 (** Translation into dataflow and sequential languages, defaults to obc. *)
 let program p =

compiler/minils/transformations/tomato.ml

@@ -67,6 +67,10 @@ module PatEnv =
 
     type penv_t = (int * exp * ident list) P.t
 
+
+    (* An environment used for automata minimization: holds both a pattern environment mapping patterns to equivalence
+       classes, and a [(pat * int list) Env.t] that maps variable [x] to a [(pat, pth)] tuple where [pat] is the pattern
+       holding [x] at path [pth] *)
     type t = penv_t * (pat * int list) Env.t
 
     let empty = (P.empty, Env.empty)

compiler/obc/_tags

@@ -1 +1 @@
-<c> or <java>:include
+<transformations> or <c> or <java>:include

compiler/obc/java/java.ml

@@ -111,8 +111,8 @@ let default_value ty = match ty with
   | Tarray _ -> Enew_array (ty,[])
 
 
-let java_pervasives = Names.modul_of_string "jeptagon.Pervasives"
-let java_pervasives_class = Names.qualname_of_string "jeptagon.Pervasives"
+let java_pervasive_class c = Names.qualname_of_string ("jeptagon.Pervasives."^c)
+let the_java_pervasives = Names.qualname_of_string "jeptagon.Pervasives"
 
 let java_callable = Names.qualname_of_string "java.util.concurrent.Callable"
 

compiler/obc/java/obc2java.ml

@@ -15,6 +15,9 @@
        Obc.Oobj and Oarray are simply Pvar and Parray_elem
        Obc.Types_alias are dereferenced since no simple type alias is possible in Java *)
 
+(** Requires scalar Obc : [p = e] when [e] is an array is understand as a copy of the reference,
+  not a copy of the array. *)
+
 open Format
 open Misc
 open Names
@@ -97,6 +100,9 @@ let rec static_exp param_env se = match se.Types.se_desc with
   | Types.Sarray se_l -> Enew_array (ty param_env se.Types.se_ty, List.map (static_exp param_env) se_l)
   | Types.Srecord _ -> eprintf "ojSrecord@."; assert false; (* TODO java *)
   | Types.Sop (f, se_l) -> Efun (qualname_to_class_name f, List.map (static_exp param_env) se_l)
+  | Types.Sasync se ->
+      let t_c = Tgeneric (java_pervasive_class "StaticFuture", [boxed_ty param_env se.Types.se_ty]) in
+      Enew (t_c, [static_exp param_env se])
 
 and boxed_ty param_env t = match t with
   | Types.Tprod ty_l -> tuple_ty param_env ty_l
@@ -110,7 +116,7 @@ and boxed_ty param_env t = match t with
 
 and tuple_ty param_env ty_l =
   let ln = ty_l |> List.length |> Pervasives.string_of_int in
-  Tgeneric ({ qual = java_pervasives; name = "Tuple"^ln }, List.map (boxed_ty param_env) ty_l)
+  Tgeneric (java_pervasive_class ("Tuple"^ln), List.map (boxed_ty param_env) ty_l)
 
 and ty param_env t :Java.ty = match t with
   | Types.Tprod ty_l -> tuple_ty param_env ty_l
@@ -197,6 +203,9 @@ let rec act_list param_env act_l acts =
     | Obc.Afor (v, se, se', b) ->
         let afor = Afor (var_dec param_env v, static_exp param_env se, static_exp param_env se', block param_env b) in
         afor::acts
+    | Obc.Ablock b ->
+        let ablock = Ablock (block param_env b) in
+        ablock::acts
   in
   List.fold_right _act act_l acts
 
@@ -304,7 +313,7 @@ let create_async_classe async base_classe =
       let act_result =
         let exp_call =
           let args = var_inst::exps_step in
-          let executor = Eval (Pfield (Pclass java_pervasives_class, "executor_cached")) in
+          let executor = Eval (Pfield (Pclass the_java_pervasives, "executor_cached")) in
           Emethod_call (executor, "submit", [Enew (Tclass callable_classe_name, args)] )
         in Aassgn (Pthis id_result, exp_call)
       in

compiler/obc/obc.ml

@@ -8,6 +8,21 @@
 (**************************************************************************)
 (* Object code internal representation *)
 
+(** { 3 Semantics }
+  Any variable is a reference to a constant memory.
+    Thus [p = e] is not the change of the reference,
+    but a recursive copy of what is referenced (deep copy).
+    As an example, [x = 3] but also [x = \[3; 4; 5\]]
+    and [t1 = t2] with the content of the array [t2] copied into the array [t1].
+  Obc is also "SSA" in the sens that a variable is assigned a value only once per call of [step] etc.
+    Thus arguments are passed as constant references to a constant memory.
+
+  One exception to the SSA rule is through the [mutable] variables.
+    Theses variables can be assigned multiple times.
+    Thus a [mutable] argument is passed as a reference to a constant memory.
+*)
+
+
 open Misc
 open Names
 open Idents
@@ -69,6 +84,7 @@ type act =
   | Aasync_call of async_t * pattern list * obj_ref * method_name * exp list
   | Acase of exp * (constructor_name * block) list
   | Afor of var_dec * static_exp * static_exp * block
+  | Ablock of block
 
 and block =
     { b_locals : var_dec list;

compiler/obc/obc_mapfold.ml

@@ -115,6 +115,9 @@ and act funs acc a = match a with
       let idx2, acc = static_exp_it funs.global_funs acc idx2 in
       let b, acc = block_it funs acc b in
         Afor(x, idx1, idx2, b), acc
+  | Ablock b ->
+      let b, acc = block_it funs acc b in
+      Ablock b, acc
 
 and block_it funs acc b = funs.block funs acc b
 and block funs acc b =

compiler/obc/obc_printer.ml

@@ -108,6 +108,8 @@ let rec print_act ff a =
           print_obj_call o
           print_method_name meth
           print_exps es
+    | Ablock b ->
+        fprintf ff "do@\n  %a@\ndone" print_block b
 
 and print_var_dec_list ff var_dec_list = match var_dec_list with
   | [] -> ()

lib/java/jeptagon/Pervasives.java

@@ -1,17 +1,46 @@
 package jeptagon;
 
+import java.util.concurrent.Executors;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Future;
+import java.util.concurrent.TimeUnit;
+
 public class Pervasives {
 
-    public static final java.util.concurrent.ExecutorService executor_cached = java.util.concurrent.Executors.newCachedThreadPool();
+    public static final ExecutorService executor_cached = Executors.newCachedThreadPool();
 
+    public static class StaticFuture<V> implements Future<V> {
+    	V v;
+    	
+    	public StaticFuture(V v) { this.v = v;	}
+    	
+    	public boolean cancel(boolean mayInterruptIfRunning) { return false; }
+    	
+    	public boolean isCancelled() { return false; }
+    	
+    	public boolean isDone() { return true; }
+    	
+    	public V get() { return v; }
+    	
+    	public V get(long timeout, TimeUnit unit) { return v; }	
+    }
 	
-    public static class Tuple1 <T> {
+    public static class Tuple1<T> {
     	public final T c0;
     	public Tuple1(T v) {
     		c0 = v;
     	}
     }
     
+    public static class Tuple22 {
+    	public final Object c0;
+    	public final Object c1;
+    	public Tuple22(Object v0, Object v1) {
+    		c0 = v0;
+    		c1 = v1;
+    	}
+    }
+    
     public static class Tuple2 <T0,T1> {
     	public final T0 c0;
     	public final T1 c1;

test/async/lent.ept

@@ -0,0 +1,12 @@
+
+node g () returns (y : int)
+let
+  y = 3
+tel
+
+node f (x : int; c : bool) returns (z : int)
+let
+  z = merge c (true -> (0 fby (g(z when true(c))))) (false -> 0)
+tel
+
+

test/async/rapide_lent.ept

@@ -0,0 +1,24 @@
+
+
+node lent(coeff:int) returns (y:int)
+let
+  y = do_stuff(coeff);
+tel
+
+
+node rapide<<size:int>>() returns (z:int)
+var y,cpt : int; big_step : bool;
+let
+  big_step = cpt = 0;
+  cpt = size fby (if big_step then size else cpt - 1);
+  y = merge big_step
+        (true  -> 0 -> (pre (lent(size))))
+	(false -> 0 fby y when false(big_step));
+  z = do_stuff(1) - y;
+tel
+
+
+node main() returns(r: int)
+let
+  r = rapide<<1000>>();
+tel

test/async/rapide_lent_a.ept

@@ -0,0 +1,24 @@
+
+
+node lent(coeff:int) returns (y:int)
+let
+  y = do_stuff(coeff);
+tel
+
+
+node rapide<<size:int>>() returns (z:int)
+var y : int; cpt : int; big_step : bool;
+let
+  big_step = cpt = 0;
+  cpt = size fby (if big_step then size else cpt - 1);
+  y = merge big_step
+        (true  -> 0 -> !(pre (async lent(size))))
+	(false -> 0 fby y when false(big_step));
+  z = do_stuff(1) - y;
+tel
+
+
+node main() returns(r: int)
+let
+  r = rapide<<1000>>();
+tel

test/async/tt.ept

@@ -0,0 +1,12 @@
+node counter(res: bool; tick: bool) returns (o: int)
+let
+  o = if res then 0 else if tick then 1 -> pre o + 1 else 0 -> pre o;
+tel
+
+node counter2() returns (b: bool)
+var t : async int;
+let
+  t = async 0 fby async counter(false,true);
+  b = counter(false,true) -1 = !t;
+tel
+  

test/async/ttt.ept

@@ -0,0 +1,18 @@
+node counter(res: bool; tick: bool) returns (o: int)
+let
+  o = if res then 0 else if tick then 1 -> pre o + 1 else 0 -> pre o;
+tel
+
+node counter3() returns (t: async bool)
+var last async t: int; cpt: int;
+let
+  cpt = counter(false,true);
+  automaton
+    state I do
+      t = async counter(false,true)));
+      until true continue III
+    state III do
+      until cpt/3 = 0 continue I
+  end;
+  b = 0 fby cpt - 1 = 0 -> !t ;
+tel

tools/debugger_script

@@ -1,5 +1,3 @@
-load_printer "/sw/lib/ocaml/menhirLib/menhirLib.cmo"
-load_printer "/sw/lib/ocaml/str.cma"
 load_printer "_build/global/names.d.cmo"
 load_printer "_build/global/location.d.cmo"
 load_printer "_build/utilities/misc.d.cmo"