/ - Diff - LustreC

     backends/C/C_backend_makefile
     backends/C/C_backend_spec
     backends/C/C_backend_src
     backends/Horn/Horn_backend_common
     backends/Horn/Horn_backend_printers
     backends/Horn/Horn_backend_collecting_sem
     backends/Horn/Horn_backend
     plugins/scopes/Scopes
     Basic_library

       | Cst c         -> pp_c_const fmt c
       | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
       | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
       | Power (v, n)  -> assert false
       | Power (v, n)  -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
       | LocalVar v    -> pp_var fmt v
       | StateVar v    ->
         (* array memory vars are represented by an indirection to a local var with the right type,

       fprintf fmt "@.";
       (* Main binary *)
       fprintf fmt "%s_%s:@." basename nodename;
       fprintf fmt "%s_%s: %s.c %s_main.c@." basename nodename basename basename;
       fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s.c@." basename;
       fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s_main.c@." basename;
       fprintf_dependencies fmt dependencies;

     and pp_machine_instr dependencies (m: machine_t) self fmt instr =
       match instr with
       | MNoReset _ -> ()
       | MReset i ->
         pp_machine_reset m self fmt i
       | MLocalAssign (i,v) ->
-...
     	(pp_c_val self (pp_c_var_read m)) g
     	(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
       | MComment s  ->
           fprintf fmt "//%s@ " s
           fprintf fmt "/*%s*/@ " s
     and pp_machine_branch dependencies m self fmt (t, h) =

     let rec pp_horn_const fmt c =
       match c with
         | Const_int i    -> pp_print_int fmt i
         | Const_real (_,_s)   -> pp_print_string fmt s
         | Const_real (_,_,s)   -> pp_print_string fmt s
         | Const_tag t    -> pp_horn_tag fmt t
         | _              -> assert false
-...
        but an offset suffix may be added for array variables
     *)
     let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
       match v with
       match v.value_desc with
         | Cst c         -> pp_horn_const fmt c
         | Array _
         | Access _ -> assert false (* no arrays *)
-...
     (* Prints a [value] indexed by the suffix list [loop_vars] *)
     let rec pp_value_suffix self pp_value fmt value =
      match value with
      match value.value_desc with
      | Fun (n, vl)  ->
        Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
      |  _            ->
-...
        - [value]: assigned value
        - [pp_var]: printer for variables
     *)
     let pp_assign m pp_var fmt var_type var_name value =
     let pp_assign m pp_var fmt var_name value =
       let self = m.mname.node_id in
       fprintf fmt "(= %a %a)"
         (pp_horn_val ~is_lhs:true self pp_var) var_name
-...
           | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
     	fprintf fmt "@[<v 5>(and ";
     	fprintf fmt "(= %a (ite %a %a %a))"
     	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
     	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
     	  (pp_horn_var m) mem_m
     	  (pp_horn_val self (pp_horn_var m)) i1
     	  (pp_horn_val self (pp_horn_var m)) i2
-...
     	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
     	  (Utils.pp_final_char_if_non_empty "@ " inputs)
     	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
     	  (List.map (fun v -> LocalVar v) outputs)
     	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
     	  (Utils.pp_final_char_if_non_empty "@ " outputs)
     	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
-...
           inputs
           (Utils.pp_final_char_if_non_empty "@ " inputs)
           (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
           (List.map (fun v -> LocalVar v) outputs)
           (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
+      )
-...
       | MLocalAssign (i,v) ->
         pp_assign
           m (pp_horn_var m) fmt
           i.var_type (LocalVar i) v;
           (mk_val (LocalVar i) i.var_type) v;
         reset_instances
       | MStateAssign (i,v) ->
         pp_assign
           m (pp_horn_var m) fmt
           i.var_type (StateVar i) v;
           (mk_val (StateVar i) i.var_type) v;
         reset_instances
       | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
       | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
         assert false (* This should not happen anymore *)
       | MStep (il, i, vl) ->
         (* if reset instance, just print the call over mem_m , otherwise declare mem_m =

       | Ctuple ckl ->
           List.exists (occurs cvar) ckl
       | Con (ck',_,_) -> occurs cvar ck'
       | Pck_up (ck',_) -> occurs cvar ck'
       | Pck_down (ck',_) -> occurs cvar ck'
       | Pck_phase (ck',_) -> occurs cvar ck'
       | Cvar _ -> ck=cvar
       | Cunivar _ | Pck_const (_,_) -> false
       | Cvar  -> ck=cvar
       | Cunivar   -> false
       | Clink ck' -> occurs cvar ck'
       | Ccarrying (_,ck') -> occurs cvar ck'
-...
         | Ctuple clist ->
             List.iter generalize clist
         | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
         | Cvar cset ->
         | Cvar ->
             if ck.cscoped then
               raise (Scope_clock ck);
             ck.cdesc <- Cunivar cset
         | Pck_up (ck',_) -> generalize ck'
         | Pck_down (ck',_) -> generalize ck'
         | Pck_phase (ck',_) -> generalize ck'
         | Pck_const (_,_) | Cunivar _ -> ()
             ck.cdesc <- Cunivar
         | Cunivar -> ()
         | Clink ck' ->
             generalize ck'
         | Ccarrying (cr,ck') ->
-...
       | Con (ck',c,l) ->
           let c' = instantiate_carrier c inst_cr_vars in
           {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
       | Cvar _ | Pck_const (_,_) -> ck
       | Pck_up (ck',k) ->
           {ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
       | Pck_down (ck',k) ->
           {ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
       | Pck_phase (ck',q) ->
           {ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)}
       | Cvar  -> ck
       | Clink ck' ->
           {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
       | Ccarrying (cr,ck') ->
           let cr' = instantiate_carrier cr inst_cr_vars in
             {ck with cdesc =
              Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
       | Cunivar cset ->
       | Cunivar ->
           try
             List.assoc ck.cid !inst_ck_vars
           with Not_found ->
             let var = new_ck (Cvar cset) true in
             let var = new_ck Cvar true in
     	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
     	var
     (** [subsume pck1 cset1] subsumes clock [pck1] by clock subset
         [cset1]. The clock constraint is actually recursively transfered to
         the clock variable appearing in [pck1] *)
     let subsume pck1 cset1 =
       let rec aux pck cset =
         match cset with
         | CSet_all ->
             ()
         | CSet_pck (k,(a,b)) ->
             match pck.cdesc with
             | Cvar cset' ->
                 pck.cdesc <- Cvar (intersect cset' cset)
             | Pck_up (pck',k') ->
                 let rat = if a=0 then (0,1) else (a,b*k') in
                 aux pck' (CSet_pck ((k*k'),rat))
             | Pck_down (pck',k') ->
                 let k''=k/(gcd k k') in
                 aux pck' (CSet_pck (k'',(a*k',b)))
             | Pck_phase (pck',(a',b')) ->
                 let (a'',b'')= max_rat (sum_rat (a,b) (-a',b')) (0,1) in
                 aux pck' (CSet_pck (k, (a'',b'')))
             | Pck_const (n,(a',b')) ->
                 if n mod k <> 0 || (max_rat (a,b) (a',b')) <> (a',b') then
                   raise (Subsume (pck1, cset1))
             | Clink pck' ->
                 aux pck' cset
             | Cunivar _ -> ()
             | Ccarrying (_,ck') ->
                 aux ck' cset
             | _ -> raise (Subsume (pck1, cset1))
       in
       aux pck1 cset1
     let rec update_scope_carrier scoped cr =
       if (not scoped) then
-...
           | Ctuple clist ->
               List.iter (update_scope scoped) clist
           | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
           | Cvar cset ->
               ck.cdesc <- Cvar cset
           | Pck_up (ck',_) -> update_scope scoped ck'
           | Pck_down (ck',_) -> update_scope scoped ck'
           | Pck_phase (ck',_) -> update_scope scoped ck'
           | Pck_const (_,_) | Cunivar _ -> ()
           | Cvar | Cunivar -> ()
           | Clink ck' ->
               update_scope scoped ck'
           | Ccarrying (cr,ck') ->
               update_scope_carrier scoped cr; update_scope scoped ck'
         end
     (* Unifies two static pclocks. *)
     let unify_static_pck ck1 ck2 =
       if (period ck1 <> period ck2) || (phase ck1 <> phase ck2) then
         raise (Unify (ck1,ck2))
     (* Unifies two clock carriers *)
     let unify_carrier cr1 cr2 =
-...
       with
       | Unify (ck1',ck2') ->
         raise (Error (loc, Clock_clash (ck1',ck2')))
       | Subsume (ck,cset) ->
         raise (Error (loc, Clock_set_mismatch (ck,cset)))
       | Mismatch (cr1,cr2) ->
         raise (Error (loc, Carrier_mismatch (cr1,cr2)))
-...
       if ck1==ck2 then
         ()
       else
         let left_const = is_concrete_pck ck1 in
         let right_const = is_concrete_pck ck2 in
         if left_const && right_const then
           unify_static_pck ck1 ck2
         else
           match ck1.cdesc,ck2.cdesc with
           | Cvar cset1,Cvar cset2->
               if ck1.cid < ck2.cid then
                 begin
                   ck2.cdesc <- Clink (simplify ck1);
                   update_scope ck2.cscoped ck1;
                   subsume ck1 cset2
                 end
               else
                 begin
                   ck1.cdesc <- Clink (simplify ck2);
                   update_scope ck1.cscoped ck2;
                   subsume ck2 cset1
                 end
           | Cvar cset, Pck_up (_,_) | Cvar cset, Pck_down (_,_)
           | Cvar cset, Pck_phase (_,_) | Cvar cset, Pck_const (_,_) ->
               if (occurs ck1 ck2) then
                 begin
                   if (simplify ck2 = ck1) then
                     ck2.cdesc <- Clink (simplify ck1)
                   else
                     raise (Unify (ck1,ck2));
                   end
               else
                 begin
                   ck1.cdesc <- Clink (simplify ck2);
                   subsume ck2 cset
                 end
           | Pck_up (_,_), Cvar cset | Pck_down (_,_), Cvar cset
           | Pck_phase (_,_), Cvar cset | Pck_const (_,_), Cvar cset ->
                 if (occurs ck2 ck1) then
                   begin
                     if ((simplify ck1) = ck2) then
                       ck1.cdesc <- Clink (simplify ck2)
                     else
                       raise (Unify (ck1,ck2));
                   end
                 else
                   begin
                     ck2.cdesc <- Clink (simplify ck1);
                     subsume ck1 cset
                   end
           | (Cvar cset,_) when (not (occurs ck1 ck2)) ->
               subsume ck2 cset;
               update_scope ck1.cscoped ck2;
               ck1.cdesc <- Clink (simplify ck2)
           | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
               subsume ck1 cset;
               update_scope ck2.cscoped ck1;
               ck2.cdesc <- Clink (simplify ck1)
           | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
               unify_carrier cr1 cr2;
               unify ck1' ck2'
           | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
               raise (Unify (ck1,ck2))
           | Carrow (c1,c2), Carrow (c1',c2') ->
               unify c1 c1'; unify c2 c2'
           | Ctuple ckl1, Ctuple ckl2 ->
               if (List.length ckl1) <> (List.length ckl2) then
                 raise (Unify (ck1,ck2));
               List.iter2 unify ckl1 ckl2
           | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
               unify_carrier c1 c2;
               unify ck' ck''
           | Pck_const (i,r), Pck_const (i',r') ->
               if i<>i' || r <> r' then
                 raise (Unify (ck1,ck2))
           | (_, Pck_up (pck2',k)) when (not right_const) ->
               let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in
               unify ck1' pck2'
           | (_,Pck_down (pck2',k)) when (not right_const) ->
               subsume ck1 (CSet_pck (k,(0,1)));
               let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in
               unify ck1' pck2'
           | (_,Pck_phase (pck2',(a,b))) when (not right_const) ->
               subsume ck1 (CSet_pck (b,(a,b)));
               let ck1' = simplify (new_ck (Pck_phase (ck1,(-a,b))) true) in
               unify ck1' pck2'
           | Pck_up (pck1',k),_ ->
               let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in
               unify pck1' ck2'
           | Pck_down (pck1',k),_ ->
               subsume ck2 (CSet_pck (k,(0,1)));
               let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in
               unify pck1' ck2'
           | Pck_phase (pck1',(a,b)),_ ->
               subsume ck2 (CSet_pck (b,(a,b)));
               let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in
               unify pck1' ck2'
           | Cunivar _, _ | _, Cunivar _ -> ()
           | _,_ -> raise (Unify (ck1,ck2))
         match ck1.cdesc,ck2.cdesc with
         | Cvar, Cvar ->
           if ck1.cid < ck2.cid then
             begin
               ck2.cdesc <- Clink (simplify ck1);
               update_scope ck2.cscoped ck1
             end
           else
             begin
               ck1.cdesc <- Clink (simplify ck2);
               update_scope ck1.cscoped ck2
             end
         | (Cvar, _) when (not (occurs ck1 ck2)) ->
           update_scope ck1.cscoped ck2;
           ck1.cdesc <- Clink (simplify ck2)
         | (_, Cvar) when (not (occurs ck2 ck1)) ->
           update_scope ck2.cscoped ck1;
           ck2.cdesc <- Clink (simplify ck1)
         | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
           unify_carrier cr1 cr2;
           unify ck1' ck2'
         | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
           raise (Unify (ck1,ck2))
         | Carrow (c1,c2), Carrow (c1',c2') ->
           unify c1 c1'; unify c2 c2'
         | Ctuple ckl1, Ctuple ckl2 ->
           if (List.length ckl1) <> (List.length ckl2) then
             raise (Unify (ck1,ck2));
           List.iter2 unify ckl1 ckl2
         | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
           unify_carrier c1 c2;
           unify ck' ck''
         | Cunivar, _ | _, Cunivar -> ()
         | _,_ -> raise (Unify (ck1,ck2))
     (** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
         (ck1,ck2)] if the clocks are not semi-unifiable.*)
-...
         ()
       else
           match ck1.cdesc,ck2.cdesc with
           | Cvar cset1,Cvar cset2->
           | Cvar, Cvar ->
               if ck1.cid < ck2.cid then
                 begin
                   ck2.cdesc <- Clink (simplify ck1);
-...
                   ck1.cdesc <- Clink (simplify ck2);
                   update_scope ck1.cscoped ck2
                 end
           | (Cvar cset,_) -> raise (Unify (ck1,ck2))
           | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
           | (Cvar, _) -> raise (Unify (ck1,ck2))
           | (_, Cvar) when (not (occurs ck2 ck1)) ->
               update_scope ck2.cscoped ck1;
               ck2.cdesc <- Clink (simplify ck1)
           | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
-...
           | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
               semi_unify_carrier c1 c2;
               semi_unify ck' ck''
           | Cunivar _, _ | _, Cunivar _ -> ()
           | Cunivar, _ | _, Cunivar -> ()
           | _,_ -> raise (Unify (ck1,ck2))
     (* Returns the value corresponding to a pclock (integer) factor
-...
       with
       | Unify (ck1',ck2') ->
         raise (Error (loc, Clock_clash (ck1',ck2')))
       | Subsume (ck,cset) ->
         raise (Error (loc, Clock_set_mismatch (ck,cset)))
       | Mismatch (cr1,cr2) ->
         raise (Error (loc, Carrier_mismatch (cr1,cr2)))
-...
       with
       | Unify (ck1',ck2') ->
         raise (Error (loc, Clock_clash (ck1',ck2')))
       | Subsume (ck,cset) ->
         raise (Error (loc, Clock_set_mismatch (ck,cset)))
       | Mismatch (cr1,cr2) ->
         raise (Error (loc, Carrier_mismatch (cr1,cr2)))
-...
       with
       | Unify (ck1',ck2') ->
         raise (Error (loc, Clock_clash (ck1',ck2')))
       | Subsume (ck,cset) ->
         raise (Error (loc, Clock_set_mismatch (ck,cset)))
       | Mismatch (cr1,cr2) ->
         raise (Error (loc, Carrier_mismatch (cr1,cr2)))
-...
       let rec aux ck =
         match (repr ck).cdesc with
         | Con _
         | Cvar _ ->
         | Cvar ->
             begin
               match !ck_var with
               | None ->
-...
       let ck_var = ref ref_ck_opt in
       let rec aux ck =
         match (repr ck).cdesc with
         | Cvar _ ->
         | Cvar ->
             begin
               match !ck_var with
               | None ->
-...
     let clock_coreclock env cck id loc scoped =
       match cck.ck_dec_desc with
       | Ckdec_any -> new_var scoped
       | Ckdec_pclock (n,(a,b)) ->
           let ck = new_ck (Pck_const (n,(a,b))) scoped in
           if n mod b <> 0 then raise (Error (loc,Invalid_const ck));
           ck
       | Ckdec_bool cl ->
           let temp_env = Env.add_value env id (new_var true) in
           (* We just want the id to be present in the environment *)
-...
         | Carrow (ck1,ck2) -> aux ck1; aux ck2
         | Ctuple cl -> List.iter aux cl
         | Con (ck',_,_) -> aux ck'
         | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) ->
             raise (Error (loc, (Invalid_imported_clock ck_node)))
         | Pck_const (n,p) ->
             begin
               match !pck with
               | None -> pck := Some (n,p)
               | Some (n',p') ->
                   if (n,p) <> (n',p') then
                     raise (Error (loc, (Invalid_imported_clock ck_node)))
             end
         | Clink ck' -> aux ck'
         | Ccarrying (_,ck') -> aux ck'
         | Cvar _ | Cunivar _ ->
         | Cvar | Cunivar  ->
             match !pck with
             | None -> ()
             | Some (_,_) ->

     open Utils
     open Format
     (* Clock type sets, for subtyping. *)
     type clock_set =
         CSet_all
       | CSet_pck of int*rat
     (* (\* Clock type sets, for subtyping. *\) *)
     (* type clock_set = *)
     (*     CSet_all *)
     (*   | CSet_pck of int*rat *)
     (* Clock carriers basically correspond to the "c" in "x when c" *)
     type carrier_desc =
-...
       | Carrow of clock_expr * clock_expr
       | Ctuple of clock_expr list
       | Con of clock_expr * carrier_expr * ident
       | Pck_up of clock_expr * int
       | Pck_down of clock_expr * int
       | Pck_phase of clock_expr * rat
       | Pck_const of int * rat
       | Cvar of clock_set (* Monomorphic clock variable *)
       | Cunivar of clock_set (* Polymorphic clock variable *)
       (* | Pck_up of clock_expr * int *)
       (* | Pck_down of clock_expr * int *)
       (* | Pck_phase of clock_expr * rat *)
       (* | Pck_const of int * rat *)
       | Cvar (* of clock_set *) (* Monomorphic clock variable *)
       | Cunivar (* of clock_set *) (* Polymorphic clock variable *)
       | Clink of clock_expr (* During unification, make links instead of substitutions *)
       | Ccarrying of carrier_expr * clock_expr
     type error =
       | Clock_clash of clock_expr * clock_expr
       | Not_pck
       | Clock_set_mismatch of clock_expr * clock_set
       (* | Not_pck *)
       (* | Clock_set_mismatch of clock_expr * clock_set *)
       | Cannot_be_polymorphic of clock_expr
       | Invalid_imported_clock of clock_expr
       | Invalid_const of clock_expr
-...
       | Clock_extrusion of clock_expr * clock_expr
     exception Unify of clock_expr * clock_expr
     exception Subsume of clock_expr * clock_set
     exception Mismatch of carrier_expr * carrier_expr
     exception Scope_carrier of carrier_expr
     exception Scope_clock of clock_expr
     exception Error of Location.t * error
     let print_ckset fmt s =
       match s with
       | CSet_all -> ()
       | CSet_pck (k,q) ->
           let (a,b) = simplify_rat q in
           if k = 1 && a = 0 then
             fprintf fmt "<:P"
           else
             fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
     let rec print_carrier fmt cr =
      (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
       match cr.carrier_desc with
-...
           (fprintf_list ~sep:" * " print_ck_long) cklist
       | Con (ck,c,l) ->
         fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
       | Pck_up (ck,k) ->
         fprintf fmt "%a*^%i" print_ck_long ck k
       | Pck_down (ck,k) ->
         fprintf fmt "%a/^%i" print_ck_long ck k
       | Pck_phase (ck,q) ->
         fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
       | Pck_const (n,p) ->
         fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
       | Cvar cset ->
         fprintf fmt "'_%i%a" ck.cid print_ckset cset
       | Cunivar cset ->
         fprintf fmt "'%i%a" ck.cid print_ckset cset
       | Cvar -> fprintf fmt "'_%i" ck.cid
       | Cunivar -> fprintf fmt "'%i" ck.cid
       | Clink ck' ->
         fprintf fmt "link %a" print_ck_long ck'
       | Ccarrying (cr,ck') ->
-...
     let new_ck desc scoped =
       incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
     let new_var scoped =
       new_ck (Cvar CSet_all) scoped
     let new_var scoped = new_ck Cvar scoped
     let new_univar () =
       new_ck (Cunivar CSet_all) false
     let new_univar () = new_ck Cunivar false
     let new_carrier_id = ref (-1)
-...
     (* Removes all links in a clock. Only used for clocks
        simplification though. *)
     let rec deep_repr ck =
     let rec simplify ck =
       match ck.cdesc with
       | Carrow (ck1,ck2) ->
           new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
           new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
       | Ctuple cl ->
           new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
           new_ck (Ctuple (List.map simplify cl)) ck.cscoped
       | Con (ck', c, l) ->
           new_ck (Con (deep_repr ck', c, l)) ck.cscoped
       | Pck_up (ck',k) ->
           new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
       | Pck_down (ck',k) ->
           new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
       | Pck_phase (ck',q) ->
           new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
       | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
       | Clink ck' -> deep_repr ck'
       | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
           new_ck (Con (simplify ck', c, l)) ck.cscoped
       | Cvar | Cunivar -> ck
       | Clink ck' -> simplify ck'
       | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
     (** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
         (ensured by language syntax) *)
-...
     let clock_of_impnode_clock ck =
       let ck = repr ck in
       match ck.cdesc with
       | Carrow _ | Clink _ | Cvar _ | Cunivar _ ->
       | Carrow _ | Clink _ | Cvar | Cunivar ->
           failwith "internal error clock_of_impnode_clock"
       | Ctuple cklist -> List.hd cklist
       | Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_)
       | Pck_const (_,_) | Ccarrying (_,_) -> ck
     (** [intersect set1 set2] returns the intersection of clock subsets
         [set1] and [set2]. *)
     let intersect set1 set2 =
       match set1,set2 with
       | CSet_all,_ -> set2
       | _,CSet_all -> set1
       | CSet_pck (k,q), CSet_pck (k',q') ->
           let k'',q'' = lcm k k',max_rat q q' in
           CSet_pck (k'',q'')
     (** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is
         due to clock variables) *)
     let rec can_be_pck ck =
       match (repr ck).cdesc with
       | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_)
       | Cvar _ | Cunivar _ ->
           true
       | Ccarrying (_,ck') -> can_be_pck ck
       | _ -> false
     (** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck
         transformations applied to a pck constant) *)
     let rec is_concrete_pck ck =
       match ck.cdesc with
       | Carrow (_,_) | Ctuple _ | Con (_,_,_)
       | Cvar _ | Cunivar _ -> false
       | Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck'
       | Pck_phase (ck',_) -> is_concrete_pck ck'
       | Pck_const (_,_) -> true
       | Clink ck' -> is_concrete_pck ck'
       | Ccarrying (_,ck') -> false
       | Con (_,_,_)
       | Ccarrying (_,_) -> ck
     (** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
     let rec is_polymorphic ck =
       match ck.cdesc with
       | Cvar _ | Pck_const (_,_) -> false
       | Cvar -> false
       | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
       | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
       | Con (ck',_,_) -> is_polymorphic ck'
       | Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck'
       | Pck_phase (ck',_) -> is_polymorphic ck'
       | Cunivar _ -> true
       | Cunivar  -> true
       | Clink ck' -> is_polymorphic ck'
       | Ccarrying (_,ck') -> is_polymorphic ck'
-...
     let rec constrained_vars_of_clock ck =
       let rec aux vars ck =
         match ck.cdesc with
         | Pck_const (_,_) ->
             vars
         | Cvar cset ->
             begin
               match cset with
               | CSet_all -> vars
               | _ ->
                   list_union [ck] vars
             end
         | Cvar -> vars
         | Carrow (ck1,ck2) ->
             let l = aux vars ck1 in
             aux l ck2
-...
               (fun acc ck' -> aux acc ck')
               vars ckl
         | Con (ck',_,_) -> aux vars ck'
         | Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck'
         | Pck_phase (ck',_) -> aux vars ck'
         | Cunivar cset ->
             begin
               match cset with
               | CSet_all -> vars
               | _ -> list_union [ck] vars
             end
         | Cunivar -> vars
         | Clink ck' -> aux vars ck'
         | Ccarrying (_,ck') -> aux vars ck'
       in
       aux [] ck
     (** [period ck] returns the period of [ck]. Expects a constant pclock
         expression belonging to the correct clock set. *)
     let rec period ck =
       let rec aux ck =
         match ck.cdesc with
         | Carrow (_,_) | Ctuple _ | Con (_,_,_)
         | Cvar _ | Cunivar _ ->
             failwith "internal error: can only compute period of const pck"
         | Pck_up (ck',k) ->
             (aux ck')/.(float_of_int k)
         | Pck_down (ck',k) ->
             (float_of_int k)*.(aux ck')
         | Pck_phase (ck',_) ->
             aux ck'
         | Pck_const (n,_) ->
             float_of_int n
         | Clink ck' -> aux ck'
         | Ccarrying (_,ck') -> aux ck'
       in
       int_of_float (aux ck)
     (** [phase ck] returns the phase of [ck]. It is not expressed as a
         fraction of the period, but instead as an amount of time. Expects a
         constant expression belonging to the correct P_k *)
     let phase ck =
       let rec aux ck =
       match ck.cdesc with
       | Carrow (_,_) | Ctuple _ | Con (_,_,_)
       | Cvar _ | Cunivar _ ->
           failwith "internal error: can only compute phase of const pck"
       | Pck_up (ck',_) ->
           aux ck'
       | Pck_down (ck',k) ->
           aux ck'
       | Pck_phase (ck',(a,b)) ->
           let n = period ck' in
           let (a',b') = aux ck' in
           sum_rat (a',b') (n*a,b)
       | Pck_const (n,(a,b)) ->
           (n*a,b)
       | Clink ck' -> aux ck'
       | Ccarrying (_,ck') -> aux ck'
       in
       let (a,b) = aux ck in
       simplify_rat (a,b)
     let eq_carrier cr1 cr2 =
       match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
      | Carry_const id1, Carry_const id2 -> id1 = id2
-...
       match ck.cdesc with
       | Ctuple (ck'::_)
       | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
       | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
       | Cvar | Cunivar -> ck
       | Carrow _ | Ctuple _ -> failwith "Internal error root"
     (* Returns the branch of clock [ck] in its clock tree *)
-...
     let disjoint ck1 ck2 =
       eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
     (** [normalize pck] returns the normal form of clock [pck]. *)
     let normalize pck =
       let changed = ref true in
       let rec aux pck =
         match pck.cdesc with
         | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
             changed:=true;
             new_ck (Pck_up (aux pck',k*k')) pck.cscoped
         | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
             changed:=true;
             new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
         | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
             changed:=true;
             new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
         | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
             changed:=true;
             new_ck (Pck_down (aux pck',k*k')) pck.cscoped
         | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
             changed:=true;
             new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
         | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
             changed:=true;
             let (a'',b'') = sum_rat (a,b) (a',b') in
             new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
         | Pck_up (pck',k') ->
             new_ck (Pck_up (aux pck',k')) pck.cscoped
         | Pck_down (pck',k') ->
             new_ck (Pck_down (aux pck',k')) pck.cscoped
         | Pck_phase (pck',k') ->
             new_ck (Pck_phase (aux pck',k')) pck.cscoped
         | Ccarrying (cr,ck') ->
             new_ck (Ccarrying (cr, aux ck')) pck.cscoped
         | _ -> pck
       in
       let nf=ref pck in
       while !changed do
         changed:=false;
         nf:=aux !nf
       done;
       !nf
     (** [canonize pck] reduces transformations of [pck] and removes
         identity transformations. Expects a normalized periodic clock ! *)
     let canonize pck =
       let rec remove_id_trans pck =
         match pck.cdesc with
         | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
             remove_id_trans pck'
         | _ -> pck
       in
       let pck =
         match pck.cdesc with
         | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
             let gcd = gcd k k' in
             new_ck (Pck_phase
                       (new_ck (Pck_down
                                  (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
                          pck.cscoped,k''))
               pck.cscoped
         | Pck_down ({cdesc=Pck_up (v,k)},k') ->
             let gcd = gcd k k' in
             new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
         | _ -> pck
       in
       remove_id_trans pck
     (** [simplify pck] applies pclocks simplifications to [pck] *)
     let simplify pck =
       if (is_concrete_pck pck) then
         let n = period pck in
         let (a,b) = phase pck in
         let phase' = simplify_rat (a,b*n) in
         new_ck (Pck_const (n,phase')) pck.cscoped
       else
         let pck' = deep_repr pck in
         let nf_pck = normalize pck' in
         canonize nf_pck
     let print_cvar fmt cvar =
       match cvar.cdesc with
       | Cvar cset ->
       | Cvar ->
      (*
           if cvar.cscoped
           then
     	fprintf fmt "[_%s%a]"
     	fprintf fmt "[_%s]"
     	  (name_of_type cvar.cid)
     	  print_ckset cset
           else
      *)
     	fprintf fmt "_%s%a"
     	fprintf fmt "_%s"
     	  (name_of_type cvar.cid)
     	  print_ckset cset
       | Cunivar cset ->
       | Cunivar ->
      (*
           if cvar.cscoped
           then
     	fprintf fmt "['%s%a]"
     	fprintf fmt "['%s]"
     	  (name_of_type cvar.cid)
     	  print_ckset cset
           else
      *)
     	fprintf fmt "'%s%a"
     	fprintf fmt "'%s"
     	  (name_of_type cvar.cid)
     	  print_ckset cset
       | _ -> failwith "Internal error print_cvar"
     (* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
        complexity. *)
     let print_ck fmt ck =
       let rec aux fmt ck =
         let ck = simplify ck in
         match ck.cdesc with
         | Carrow (ck1,ck2) ->
           fprintf fmt "%a -> %a" aux ck1 aux ck2
-...
     	(fprintf_list ~sep:" * " aux) cklist
         | Con (ck,c,l) ->
           fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
         | Pck_up (ck,k) ->
           fprintf fmt "%a*.%i" aux ck k
         | Pck_down (ck,k) ->
           fprintf fmt "%a/.%i" aux ck k
         | Pck_phase (ck,q) ->
           fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
         | Pck_const (n,p) ->
           fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
         | Cvar cset ->
         | Cvar ->
     (*
           if ck.cscoped
           then
-...
           else
     *)
     	fprintf fmt "_%s" (name_of_type ck.cid)
         | Cunivar cset ->
         | Cunivar ->
     (*
           if ck.cscoped
           then
-...
     (* prints only the Con components of a clock, useful for printing nodes *)
     let rec print_ck_suffix fmt ck =
       let ck = simplify ck in
       match ck.cdesc with
       | Carrow _
       | Ctuple _
       | Cvar _
       | Cunivar _   -> ()
       | Cvar
       | Cunivar    -> ()
       | Con (ck,c,l) ->
         fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
       | Clink ck' ->
         print_ck_suffix fmt ck'
       | Ccarrying (cr,ck') ->
         fprintf fmt "%a" print_ck_suffix ck'
       | _ -> assert false
     let pp_error fmt = function
       | Clock_clash (ck1,ck2) ->
-...
           fprintf fmt "Expected clock %a, got clock %a@."
           print_ck ck1
           print_ck ck2
       | Not_pck ->
         fprintf fmt "The clock of this expression must be periodic@."
       | Carrier_mismatch (cr1, cr2) ->
          fprintf fmt "Name clash. Expected clock %a, got clock %a@."
            print_carrier cr1
            print_carrier cr2
       | Clock_set_mismatch (ck,cset) ->
           reset_names ();
         fprintf fmt "Clock %a is not included in clock set %a@."
           print_ck ck
           print_ckset cset
       | Cannot_be_polymorphic ck ->
           reset_names ();
         fprintf fmt "The main node cannot have a polymorphic clock: %a@."
-...
           print_ck ck
     let const_of_carrier cr =
      match (carrier_repr cr).carrier_desc with
      | Carry_const id -> id
      | Carry_name
      | Carry_var
      | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
       match (carrier_repr cr).carrier_desc with
       | Carry_const id -> id
       | Carry_name
       | Carry_var
       | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
     let uneval const cr =
       (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)

         eq_lhs = List.map rename eq.eq_lhs;
         eq_rhs = rename_expr rename eq.eq_rhs
+      }
     let rec add_expr_reset_cond cond expr =
       let aux = add_expr_reset_cond cond in
       let new_desc =
         match expr.expr_desc with
         | Expr_const _
         | Expr_ident _ -> expr.expr_desc
         | Expr_tuple el -> Expr_tuple (List.map aux el)
         | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e)
         | Expr_arrow (e1, e2) ->
           (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
           let e1 = aux e1 and e2 = aux e2 in
           (* inlining is performed before typing. we can leave the fields free *)
           let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
           Expr_arrow (e1, new_e2)
         | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *)
         | Expr_array el -> Expr_array (List.map aux el)
         | Expr_access (e, dim) -> Expr_access (aux e, dim)
         | Expr_power (e, dim) -> Expr_power (aux e, dim)
         | Expr_pre e -> Expr_pre (aux e)
         | Expr_when (e, id, l) -> Expr_when (aux e, id, l)
         | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases)
         | Expr_appl (id, args, reset_opt) ->
           (* we "add" cond to the reset field. *)
           let new_reset = match reset_opt with
     	  None -> cond
     	| Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond']
           in
           Expr_appl (id, args, Some new_reset)
       in
       { expr with expr_desc = new_desc }
     let add_eq_reset_cond cond eq =
       { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs }
     (*
     let get_static_inputs input_arg_list =
      List.fold_right (fun (vdecl, arg) res ->
-...
        else res)
        input_arg_list []
     *)
     (*
         expr, locals', eqs = inline_call id args' reset locals node nodes
-...
     the resulting expression is tuple_of_renamed_outputs
     TODO: convert the specification/annotation/assert and inject them
     DONE: annotations
     TODO: deal with reset
     *)
     let inline_call node orig_expr args reset locals caller =
       let loc = orig_expr.expr_loc in
       let uid = orig_expr.expr_tag in
     (** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
         locals, eqs, asserts)
     *)
     let inline_call node loc uid args reset locals caller =
       let rename v =
         if v = tag_true || v = tag_false || not (is_node_var node v) then v else
           Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
-...
     	 v.var_dec_const,
     	 Utils.option_map (rename_expr rename) v.var_dec_value) in
         begin
     (*
           (try
     	 Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
     	 Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
            with Not_found -> ());
           (try
     Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
            with Not_found -> ());
     (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
     *)
           (*
     	(try
     	Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
     	Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
     	with Not_found -> ());
     	(try
     	Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
     	with Not_found -> ());
           (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
           *)
           vdecl
         end
         (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
       (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
       in
       let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
       let outputs' = List.map rename_var node.node_outputs in
       let locals' =
           (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
         (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
         @ (List.map rename_var node.node_locals)
     in
       in
       (* checking we are at the appropriate (early) step: node_checks and
          node_gencalls should be empty (not yet assigned) *)
       assert (node.node_checks = []);
       assert (node.node_gencalls = []);
       (* Bug included: todo deal with reset *)
       assert (reset = None);
       let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
       (* Expressing reset locally in equations *)
       let eqs_r' =
         match reset with
           None -> eqs'
         | Some cond -> List.map (add_eq_reset_cond cond) eqs'
       in
       let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs',
                                     expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
       let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
       in
       let asserts' = (* We rename variables in assert expressions *)
-...
     	{a with assert_expr =
     	    let expr = a.assert_expr in
     	    rename_expr rename expr
           })
     	})
           node.node_asserts
       in
       let annots' =
-...
       in
       expr,
       inputs'@outputs'@locals'@locals,
       assign_inputs::eqs',
       assign_inputs::eqs_r',
       asserts',
       annots'
-...
           let called = node_of_top called in
           let called' = inline_node called nodes in
           let expr, locals', eqs'', asserts'', annots'' =
     	inline_call called' expr args' reset locals' node in
     	inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
           expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
         else
           (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)

     and clock_dec_desc =
       | Ckdec_any
       | Ckdec_bool of (ident * ident) list
       | Ckdec_pclock of int * rat
     type constant =
       | Const_int of int
-...
       | MLocalAssign of var_decl * value_t
       | MStateAssign of var_decl * value_t
       | MReset of ident
       | MNoReset of ident
       | MStep of var_decl list * ident * value_t list
       | MBranch of value_t * (label * instr_t list) list
       | MComment of string

         | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
         | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
         | MReset i           -> Format.fprintf fmt "reset %s" i
         | MNoReset i         -> Format.fprintf fmt "noreset %s" i
         | MStep (il, i, vl)  ->
           Format.fprintf fmt "%a = %s (%a)"
     	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
-...
         var_dec_const = false;
         var_dec_value = None;
         var_type =  typ;
         var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
         var_clock = Clocks.new_ck Clocks.Cvar true;
         var_loc = Location.dummy_loc
+      }
-...
         | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
           let nd = node_from_name id in
           Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
         | Expr_ite (g,t,e) -> (
         (*| Expr_ite (g,t,e) -> (
           (* special treatment depending on the active backend. For horn backend, ite
     	 are preserved in expression. While they are removed for C or Java
     	 backends. *)
-...
     	Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
           | "C" | "java" | _ ->
     	(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
+        )
         )*)
         | _                   -> raise NormalizationError
       in
       mk_val value_desc expr.expr_type
-...
     let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
       match expr.expr_desc with
       | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
     			    conditional g [translate_act node args (y, t)]
     			    conditional g
                                   [translate_act node args (y, t)]
                                   [translate_act node args (y, e)]
       | Expr_merge (x, hl)   -> MBranch (translate_ident node args x, List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
       | Expr_merge (x, hl)   -> MBranch (translate_ident node args x,
                                          List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
       | _                    -> MLocalAssign (y, translate_expr node args expr)
     let reset_instance node args i r c =
       match r with
       | None        -> []
       | Some r      -> let g = translate_guard node args r in
                        [control_on_clock node args c (conditional g [MReset i] [])]
                        [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
     let translate_eq node ((m, si, j, d, s) as args) eq =
       (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
-...
           then []
           else reset_instance node args o r call_ck) @
            (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
     (*
        (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
           are preserved. While they are replaced as if g then x = t else x = e in  C or Java
           backends. *)
-...
     	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
+        )
     *)
       | [x], _                                       -> (
         let var_x = get_node_var x node in
         (m, si, j, d,
-...
     	(* special treatment depending on the active backend. For horn backend,
     	   common branches are not merged while they are in C or Java
     	   backends. *)
     	match !Options.output with
     	(*match !Options.output with
     	| "horn" -> s
     	| "C" | "java" | _ -> join_guards_list s
     	| "C" | "java" | _ ->*) join_guards_list s
           );
           step_asserts =
     	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in

       end
     let functional_backend () =
       match !Options.output with
       | "horn" | "lustre" | "acsl" -> true
       | _ -> false
     (* From prog to prog *)
     let stage1 prog dirname basename =
       (* Removing automata *)
-...
       (* Typing *)
       let computed_types_env = type_decls type_env prog in
       (* Clock calculus *)
       let computed_clocks_env = clock_decls clock_env prog in
-...
       in
       *)
       (* Delay calculus *)
       (*
       (* TO BE DONE LATER (Xavier)
         if(!Options.delay_calculus)
         then
         begin
-...
           end
         else
           begin
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
     	prog
           end in
       Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-...
       (* Checking array accesses *)
       if !Options.check then
         begin
           Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
           Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
           Access.check_prog prog;
         end;
-...
       let machine_code =
         if !Options.optimization >= 4 && !Options.output <> "horn" then
           begin
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: common sub-expression elimination@,");
     	Optimize_machine.machines_cse machine_code
           end
         else
-...
       let machine_code, removed_table =
         if !Options.optimization >= 2 && !Options.output <> "horn" then
           begin
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@ ");
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
     	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
           end
         else
-...
       let machine_code =
         if !Options.optimization >= 3 && !Options.output <> "horn" then
           begin
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
     	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
     	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
     	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
-...
         if !Options.salsa_enabled then
           begin
     	check_main ();
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
     	(* Selecting float constants for Salsa *)
     	let constEnv = List.fold_left (
     	  fun accu c_topdecl ->
-...
     	let source_out = open_out source_file in
     	let fmt = formatter_of_out_channel source_out in
     	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
             Horn_backend.translate fmt basename prog machine_code;
             Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
     	(* Tracability file if option is activated *)
     	if !Options.traces then (
     	let traces_file = destname ^ ".traces" in (* Could be changed *)
     	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
     	let traces_out = open_out traces_file in
     	let fmt = formatter_of_out_channel traces_out in
             Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
     	Horn_backend.traces_file fmt basename prog machine_code;
     	Horn_backend_traces.traces_file fmt basename prog machine_code;
+    	)
           end
         | "lustre" ->

     	  annots = List.map (fun v ->
     	    let eq =
     	      try
     		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs)
     	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
     		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs)
     	      with Not_found ->
+    		(
     		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id;
     		  assert false
+    		)
     	    in
     	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
     	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
     	    (["traceability"], pair)

       | MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)
       | MStateAssign (i,v) -> MStateAssign (i, e_expr v)
       | MReset i           -> instr
       | MNoReset i         -> instr
       | MStep (il, i, vl)  -> MStep(il, i, List.map e_expr vl)
       | MBranch (g,hl)     ->
         MBranch
-...
       | Cst _ | StateVar _ -> expr
     let eliminate_dim elim dim =
       Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
       Dimension.expr_replace_expr
         (fun v -> try
     		dimension_of_value (IMap.find v elim)
           with Not_found -> mkdim_ident dim.dim_loc v)
         dim
     let unfold_expr_offset m offset expr =
       List.fold_left
-...
       | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr)
       | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr)
       | MReset id              -> instr
       | MNoReset id            -> instr
       | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs)
       | MBranch (cond, brl)
         -> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)

       | Undefined_token tok   -> fprintf fmt "undefined token '%s'" tok
       | Unfinished_string        -> fprintf fmt "unfinished string"
       | Unfinished_comment  -> fprintf fmt "unfinished comment"
       | Syntax_error               -> fprintf fmt "syntax error"
       | Syntax_error               -> fprintf fmt ""
       | Unfinished_annot        -> fprintf fmt "unfinished annotation"
       | Unfinished_node_spec -> fprintf fmt "unfinished node specification"
       | Annot_error s              -> fprintf fmt "impossible to parse the following annotation:@.%s@.@?" s

     ident_list:
       vdecl_ident {[$1]}
     | ident_list COMMA vdecl_ident {$3::$1}
     | vdecl_ident COMMA ident_list {$1::$3}
     SCOL_opt:
         SCOL {} | {}

        in environment [env] *)
     let type_coreclock env ck id loc =
       match ck.ck_dec_desc with
       | Ckdec_any | Ckdec_pclock (_,_) -> ()
       | Ckdec_any -> ()
       | Ckdec_bool cl ->
           let dummy_id_expr = expr_of_ident id loc in
           let when_expr =

Project

General

Profile

CristalCaveGem » LustreC

Revision 45f0f48d

Added by Xavier Thirioux almost 6 years ago