Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 27dc3869

History | View | Annotate | Download (19.4 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Utils
13
open LustreSpec
14
open Corelang
15
open Format
16

    
17
(** Normalisation iters through the AST of expressions and bind fresh definition
18
    when some criteria are met. This creation of fresh definition is performed by
19
    the function mk_expr_alias_opt when the alias argument is on.
20

    
21
    Initial expressions, ie expressions attached a variable in an equation
22
    definition are not aliased. This non-alias feature is propagated in the
23
    expression AST for array access and power construct, tuple, and some special
24
    cases of arrows.
25

    
26
    Two global variables may impact the normalization process:
27
    - unfold_arrow_active
28
    - force_alias_ite: when set, bind a fresh alias for then and else
29
      definitions.
30
*)
31

    
32
(* Two global variables *)
33
let unfold_arrow_active = ref true
34
let force_alias_ite = ref false
35

    
36
  
37
let expr_true loc ck =
38
{ expr_tag = Utils.new_tag ();
39
  expr_desc = Expr_const (Const_tag tag_true);
40
  expr_type = Type_predef.type_bool;
41
  expr_clock = ck;
42
  expr_delay = Delay.new_var ();
43
  expr_annot = None;
44
  expr_loc = loc }
45

    
46
let expr_false loc ck =
47
{ expr_tag = Utils.new_tag ();
48
  expr_desc = Expr_const (Const_tag tag_false);
49
  expr_type = Type_predef.type_bool;
50
  expr_clock = ck;
51
  expr_delay = Delay.new_var ();
52
  expr_annot = None;
53
  expr_loc = loc }
54

    
55
let expr_once loc ck =
56
 { expr_tag = Utils.new_tag ();
57
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
58
  expr_type = Type_predef.type_bool;
59
  expr_clock = ck;
60
  expr_delay = Delay.new_var ();
61
  expr_annot = None;
62
  expr_loc = loc }
63

    
64
let is_expr_once =
65
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
66
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
67

    
68
let unfold_arrow expr =
69
 match expr.expr_desc with
70
 | Expr_arrow (e1, e2) ->
71
    let loc = expr.expr_loc in
72
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
73
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
74
 | _                   -> assert false
75

    
76
let cpt_fresh = ref 0
77

    
78
(* Generate a new local [node] variable *)
79
let mk_fresh_var node loc ty ck =
80
  let vars = get_node_vars node in
81
  let rec aux () =
82
  incr cpt_fresh;
83
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
84
  if List.exists (fun v -> v.var_id = s) vars then aux () else
85
  {
86
    var_id = s;
87
    var_orig = false;
88
    var_dec_type = dummy_type_dec;
89
    var_dec_clock = dummy_clock_dec;
90
    var_dec_const = false;
91
    var_dec_value = None;
92
    var_type = ty;
93
    var_clock = ck;
94
    var_loc = loc
95
  }
96
  in aux ()
97

    
98
(* Get the equation in [defs] with [expr] as rhs, if any *)
99
let get_expr_alias defs expr =
100
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
101
 with
102
 | Not_found -> None
103
  
104
(* Replace [expr] with (tuple of) [locals] *)
105
let replace_expr locals expr =
106
 match locals with
107
 | []  -> assert false
108
 | [v] -> { expr with
109
   expr_tag = Utils.new_tag ();
110
   expr_desc = Expr_ident v.var_id }
111
 | _   -> { expr with
112
   expr_tag = Utils.new_tag ();
113
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
114

    
115
let unfold_offsets e offsets =
116
  let add_offset e d =
117
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
118
    let res = *)
119
    { e with
120
      expr_tag = Utils.new_tag ();
121
      expr_loc = d.Dimension.dim_loc;
122
      expr_type = Types.array_element_type e.expr_type;
123
      expr_desc = Expr_access (e, d) }
124
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
125
  in
126
 List.fold_left add_offset e offsets
127

    
128
(* Create an alias for [expr], if none exists yet *)
129
let mk_expr_alias node (defs, vars) expr =
130
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
131
  match get_expr_alias defs expr with
132
  | Some eq ->
133
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
134
    (defs, vars), replace_expr aliases expr
135
  | None    ->
136
    let new_aliases =
137
      List.map2
138
	(mk_fresh_var node expr.expr_loc)
139
	(Types.type_list_of_type expr.expr_type)
140
	(Clocks.clock_list_of_clock expr.expr_clock) in
141
    let new_def =
142
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
143
    in
144
    (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
145
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
146

    
147
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
148
   and [opt] is true *)
149
let mk_expr_alias_opt opt node (defs, vars) expr =
150
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
151
  match expr.expr_desc with
152
  | Expr_ident alias ->
153
    (defs, vars), expr
154
  | _                ->
155
    match get_expr_alias defs expr with
156
    | Some eq ->
157
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
158
      (defs, vars), replace_expr aliases expr
159
    | None    ->
160
      if opt
161
      then
162
	let new_aliases =
163
	  List.map2
164
	    (mk_fresh_var node expr.expr_loc)
165
	    (Types.type_list_of_type expr.expr_type)
166
	    (Clocks.clock_list_of_clock expr.expr_clock) in
167
	let new_def =
168
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
169
	in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
170
      else
171
	(defs, vars), expr
172

    
173
(* Create a (normalized) expression from [ref_e],
174
   replacing description with [norm_d],
175
   taking propagated [offsets] into account
176
   in order to change expression type *)
177
let mk_norm_expr offsets ref_e norm_d =
178
  (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
179
  let drop_array_type ty =
180
    Types.map_tuple_type Types.array_element_type ty in
181
  { ref_e with
182
    expr_desc = norm_d;
183
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
184
														
185
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
186
let rec normalize_list alias node offsets norm_element defvars elist =
187
  List.fold_right
188
    (fun t (defvars, qlist) ->
189
      let defvars, norm_t = norm_element alias node offsets defvars t in
190
      (defvars, norm_t :: qlist)
191
    ) elist (defvars, [])
192

    
193
let rec normalize_expr ?(alias=true) node offsets defvars expr =
194
  (*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
195
  match expr.expr_desc with
196
  | Expr_const _
197
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
198
  | Expr_array elist ->
199
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
200
    let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
201
    mk_expr_alias_opt alias node defvars norm_expr
202
  | Expr_power (e1, d) when offsets = [] ->
203
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
204
    let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
205
    mk_expr_alias_opt alias node defvars norm_expr
206
  | Expr_power (e1, d) ->
207
    normalize_expr ~alias:alias node (List.tl offsets) defvars e1
208
  | Expr_access (e1, d) ->
209
    normalize_expr ~alias:alias node (d::offsets) defvars e1
210
  | Expr_tuple elist ->
211
    let defvars, norm_elist =
212
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
213
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
214
  | Expr_appl (id, args, None)
215
      when Basic_library.is_homomorphic_fun id 
216
	&& Types.is_array_type expr.expr_type ->
217
    let defvars, norm_args =
218
      normalize_list
219
	alias
220
	node
221
	offsets
222
	(fun _ -> normalize_array_expr ~alias:true)
223
	defvars
224
	(expr_list_of_expr args)
225
    in
226
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
227
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
228
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
229
    defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
230
  | Expr_appl (id, args, r) ->
231
    let defvars, norm_args = normalize_expr node [] defvars args in
232
    let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
233
    if offsets <> []
234
    then
235
      let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
236
      normalize_expr ~alias:alias node offsets defvars norm_expr
237
    else
238
      mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr
239
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
240
    (* Here we differ from Colaco paper: arrows are pushed to the top *)
241
    normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
242
  | Expr_arrow (e1,e2) ->
243
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
244
    let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
245
    let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
246
    mk_expr_alias_opt alias node defvars norm_expr
247
  | Expr_pre e ->
248
    let defvars, norm_e = normalize_expr node offsets defvars e in
249
    let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
250
    mk_expr_alias_opt alias node defvars norm_expr
251
  | Expr_fby (e1, e2) ->
252
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
253
    let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
254
    let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
255
    mk_expr_alias_opt alias node defvars norm_expr
256
  | Expr_when (e, c, l) ->
257
    let defvars, norm_e = normalize_expr node offsets defvars e in
258
    defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
259
  | Expr_ite (c, t, e) ->
260
    let defvars, norm_c = normalize_guard node defvars c in
261
    let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
262
    let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
263
    let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
264
    mk_expr_alias_opt alias node defvars norm_expr
265
  | Expr_merge (c, hl) ->
266
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
267
    let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
268
    mk_expr_alias_opt alias node defvars norm_expr
269

    
270
(* Creates a conditional with a merge construct, which is more lazy *)
271
(*
272
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
273
 match expr.expr_desc with
274
 | Expr_ite (c, t, e) ->
275
   let defvars, norm_t = norm_expr (alias node offsets defvars t in
276
 | _ -> assert false
277
*)
278
and normalize_branches node offsets defvars hl =
279
 List.fold_right
280
   (fun (t, h) (defvars, norm_q) ->
281
     let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
282
     defvars, (t, norm_h) :: norm_q
283
   )
284
   hl (defvars, [])
285

    
286
and normalize_array_expr ?(alias=true) node offsets defvars expr =
287
  (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
288
  match expr.expr_desc with
289
  | Expr_power (e1, d) when offsets = [] ->
290
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
291
    defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
292
  | Expr_power (e1, d) ->
293
    normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
294
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
295
  | Expr_array elist when offsets = [] ->
296
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
297
    defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
298
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
299
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
300
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
301
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
302

    
303
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
304
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
305
  match expr.expr_desc with
306
  | Expr_access (e1, d) ->
307
    normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
308
  | Expr_ite (c, t, e) ->
309
    let defvars, norm_c = normalize_guard node defvars c in
310
    let defvars, norm_t = normalize_cond_expr node offsets defvars t in
311
    let defvars, norm_e = normalize_cond_expr node offsets defvars e in
312
    defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
313
  | Expr_merge (c, hl) ->
314
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
315
    defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
316
  | _ when !force_alias_ite ->
317
     (* Forcing alias creation for then/else expressions *)
318
     let defvars, norm_expr =
319
       normalize_expr ~alias:alias node offsets defvars expr
320
     in
321
     mk_expr_alias_opt true node defvars norm_expr
322
  | _ -> (* default case without the force_alias_ite option *)
323
     normalize_expr ~alias:alias node offsets defvars expr
324
     
325
and normalize_guard node defvars expr =
326
  let defvars, norm_expr = normalize_expr node [] defvars expr in
327
  mk_expr_alias_opt true node defvars norm_expr
328

    
329
(* outputs cannot be memories as well. If so, introduce new local variable.
330
*)
331
let decouple_outputs node defvars eq =
332
  let rec fold_lhs defvars lhs tys cks =
333
   match lhs, tys, cks with
334
   | [], [], []          -> defvars, []
335
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
336
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
337
			    then
338
			      let newvar = mk_fresh_var node eq.eq_loc t c in
339
			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
340
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
341
			    else
342
			      (defs_q, vars_q), v::lhs_q
343
   | _                   -> assert false in
344
  let defvars', lhs' =
345
    fold_lhs
346
      defvars
347
      eq.eq_lhs
348
      (Types.type_list_of_type eq.eq_rhs.expr_type)
349
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
350
  defvars', {eq with eq_lhs = lhs' }
351

    
352
let rec normalize_eq node defvars eq =
353
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
354
  match eq.eq_rhs.expr_desc with
355
  | Expr_pre _
356
  | Expr_fby _  ->
357
    let (defvars', eq') = decouple_outputs node defvars eq in
358
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
359
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
360
    (norm_eq::defs', vars')
361
  | Expr_array _ ->
362
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
363
    let norm_eq = { eq with eq_rhs = norm_rhs } in
364
    (norm_eq::defs', vars')
365
  | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
366
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
367
    let norm_eq = { eq with eq_rhs = norm_rhs } in
368
    (norm_eq::defs', vars')
369
  | Expr_appl _ ->
370
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
371
    let norm_eq = { eq with eq_rhs = norm_rhs } in
372
    (norm_eq::defs', vars')
373
  | _ ->
374
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
375
    let norm_eq = { eq with eq_rhs = norm_rhs } in
376
    norm_eq::defs', vars'
377

    
378
(** normalize_node node returns a normalized node,
379
    ie.
380
    - updated locals
381
    - new equations
382
    -
383
*)
384
let normalize_node node =
385
  cpt_fresh := 0;
386
  let inputs_outputs = node.node_inputs@node.node_outputs in
387
  let is_local v =
388
    List.for_all ((!=) v) inputs_outputs in
389
  let orig_vars = inputs_outputs@node.node_locals in
390
  let defs, vars =
391
    List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
392
  (* Normalize the asserts *)
393
  let vars, assert_defs, asserts =
394
    List.fold_left (
395
    fun (vars, def_accu, assert_accu) assert_ ->
396
      let assert_expr = assert_.assert_expr in
397
      let (defs, vars'), expr = 
398
	normalize_expr 
399
	  ~alias:true (* forcing introduction of new equations for fcn calls *) 
400
	  node 
401
	  [] (* empty offset for arrays *)
402
	  ([], vars) (* defvar only contains vars *)
403
	  assert_expr
404
      in
405
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
406
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
407
    ) (vars, [], []) node.node_asserts in
408
  let new_locals = List.filter is_local vars in
409
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
410

    
411
  let new_annots =
412
    if !Options.traces then
413
      begin
414
	(* Compute traceability info:
415
	   - gather newly bound variables
416
	   - compute the associated expression without aliases
417
	*)
418
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
419
	let norm_traceability = {
420
	  annots = List.map (fun v ->
421
	    let eq =
422
	      try
423
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
424
	      with Not_found -> 
425
		(
426
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
427
		  assert false
428
		) 
429
	    in
430
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
431
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
432
	    (["traceability"], pair)
433
	  ) diff_vars;
434
	  annot_loc = Location.dummy_loc
435
	}
436
	in
437
	norm_traceability::node.node_annot
438
      end
439
    else
440
      node.node_annot
441
  in
442

    
443
  let node =
444
  { node with
445
    node_locals = new_locals;
446
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
447
    node_asserts = asserts;
448
    node_annot = new_annots;
449
  }
450
  in ((*Printers.pp_node Format.err_formatter node;*)
451
    node
452
)
453

    
454

    
455
let normalize_decl decl =
456
  match decl.top_decl_desc with
457
  | Node nd ->
458
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
459
    Hashtbl.replace Corelang.node_table nd.node_id decl';
460
    decl'
461
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
462

    
463
let normalize_prog ?(backend="C") decls =
464
  let old_unfold_arrow_active = !unfold_arrow_active in
465
  let old_force_alias_ite = !force_alias_ite in
466
  
467
  (* Backend specific configurations for normalization *)
468
  let _ =
469
    match backend with
470
    | "lustre" ->
471
    (* Special treatment of arrows in lustre backend. We want to keep them *)
472
       unfold_arrow_active := false;
473
    | "emf" -> (* Forcing ite normalization *)
474
       force_alias_ite := true;
475
    | _ -> () (* No fancy options for other backends *)
476
  in
477

    
478
  (* Main algorithm: iterates over nodes *)
479
  let res = List.map normalize_decl decls in
480
  
481
  (* Restoring previous settings *)
482
  unfold_arrow_active := old_unfold_arrow_active;
483
  force_alias_ite := old_force_alias_ite;
484

    
485
  res
486
  
487
  (* Local Variables: *)
488
(* compile-command:"make -C .." *)
489
(* End: *)