Translate assertions.

src/compiledData.ml

-(** Time-stamp: <modified the 14/03/2008 (at 10:59) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:21) by Erwan Jahier> *)
 
 (** 
 
@@ -312,7 +312,7 @@ and node_def_eff =
   | BodyEff of node_body_eff
 
 and node_body_eff = {
-  asserts_eff : (val_eff srcflagged) list;
+  asserts_eff : (val_exp_eff srcflagged) list;
   eqs_eff     : (eq_info_eff srcflagged) list;
 }
 

src/evalEq.ml

-(** Time-stamp: <modified the 14/03/2008 (at 09:45) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:17) by Erwan Jahier> *)
 
 open Lxm
 open SyntaxTreeCore
@@ -158,6 +158,13 @@ and (translate_slice_info  : id_solver -> slice_info -> int -> Lxm.t ->
     EvalConst.eval_array_slice id_solver si size lxm
 
 
+(**********************************************************************************)
+let (translate_assertions : CompiledData.id_solver -> 
+      SyntaxTreeCore.val_exp  Lxm.srcflagged -> 
+      CompiledData.val_exp_eff  Lxm.srcflagged) =
+  fun id_solver vef -> 
+    Lxm.flagit (translate_val_exp id_solver vef.it) vef.src
+
 (**********************************************************************************)
 
 let (type_check: eq_info_eff srcflagged -> unit) =

src/evalEq.mli

-(** Time-stamp: <modified the 12/03/2008 (at 14:14) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:17) by Erwan Jahier> *)
 
 
 
 val f : CompiledData.id_solver -> SyntaxTreeCore.eq_info Lxm.srcflagged -> 
   CompiledData.eq_info_eff Lxm.srcflagged
+
+val translate_assertions : CompiledData.id_solver -> 
+  SyntaxTreeCore.val_exp  Lxm.srcflagged -> CompiledData.val_exp_eff  Lxm.srcflagged

src/lazyCompiler.ml

-(** Time-stamp: <modified the 14/03/2008 (at 13:28) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/03/2008 (at 15:16) by Erwan Jahier> *)
 
 
 open Lxm
@@ -602,7 +602,8 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
 			    filled
 			 *)
 		 BodyEff {
-		   asserts_eff = []; (* XXX finish me! *)
+		   asserts_eff = 
+		     List.map (EvalEq.translate_assertions node_id_solver) nb.asserts;
 		   eqs_eff = List.map (EvalEq.f node_id_solver) nb.eqs; 
 		 }
 	      )

src/test/should_work/call/call06.lus

@@ -3,5 +3,6 @@ extern function bip(x,y : bool) returns (z,t : bool);
 
 node call06(x,y : bool) returns (z,t : bool);
 let
-	(z,t) = bip(x,y);
+  assert (x=>z);
+  (z,t) = bip(x,y);
 tel