Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / linearize.ml @ 15003796

History | View | Annotate | Download (4.32 KB)

1
open LustreSpec
2

    
3
let check_input nd value =
4
      Format.eprintf "lin check input@.";
5
  if not (value.eexpr_quantifiers = []) then (
6
    Log.report ~level:1 
7
      (fun fmt -> Format.fprintf fmt "Invalid linearization command for node %s. No quantifiers allowed!@." nd.node_id );
8
    false
9
 
10
  ) else 
11
    let value_type = 
12
      match (Types.repr value.eexpr_type).Types.tdesc with
13
      | Types.Ttuple tl -> Types.Ttuple (List.map Types.dynamic_type tl)
14
      | t -> t
15
    in 
16
    let vardecl_types = Types.Ttuple(List.map (fun v -> Types.repr v.var_type) nd.node_inputs) in
17
    if not (value_type = vardecl_types) then (
18
    Log.report ~level:1 
19
      (fun fmt -> Format.fprintf fmt "Invalid linearization command for node %s: expecting type %a, got type %a@." nd.node_id
20
	Types.print_ty (Types.new_ty vardecl_types)
21
	Types.print_ty (Types.repr value.eexpr_type)
22
 );
23
    false
24
  )
25
  else 
26
    true
27
  
28
(* Eliminate variables. It will change the order of the statements. Do not touch automaton *)
29

    
30
  
31
let rec elim_vars vars stmts =
32
  Format.eprintf "lin elim var@.";
33
  
34
  (* Removing memories (lhs = Pre _ or Fby _) *)
35
  let memory_vars, non_memory_vars = List.partition (fun vid -> 
36
    let v_def = List.find (fun stm -> match stm with Eq e -> e.eq_lhs = [vid] | _ -> false) stmts in
37
    match v_def with
38
      Eq eq -> (match eq.eq_rhs.expr_desc with 
39
      Expr_pre _ | Expr_fby _ -> true
40
    | _ -> false
41
      )
42
    | _ -> false
43
  ) vars 
44
  in
45
  
46
  (* we partition this level stmts. Local Automata are left untouched and
47
     are addressed separately *)
48
  let local_defs, mem_defs, aut_defs = List.fold_left 
49
    (fun (ll,el,al) def -> (
50
      match def with
51
      | Aut a -> (ll, el, a::al) (* we do not handle automaton now. Will be down later *)
52
      | Eq eq -> (
53
	match eq.eq_lhs with 
54
	| [v] -> if List.mem v non_memory_vars then
55
	    eq::ll, el, al
56
	  else
57
	    ll, eq::el, al
58
	| _ -> raise (Failure "elim eq failed, unnormalized equation"))
59
     )) ([], [], []) stmts
60
  in
61
      Format.eprintf "lin local ok@.";
62
    let mem_defs' = 
63
      (* let local_defs, _ = (\* local defs have to be normalized to avoid loops (fixpoints) in unrolling *\) *)
64
      (* 	List.fold_left (fun (accu, vl) def ->  *)
65
      (* 	  (\* we clean def wrt accu *\) *)
66
      (* 	  Format.eprintf "lin cleaning local %a@." Printers.pp_node_eq def; *)
67
      (* 	  let def_e = Corelang.substitute_expr vl accu def.eq_rhs in *)
68
      (* 	  Format.eprintf "lin obtaining %a@." Printers.pp_expr def_e; *)
69
      (* 	  {def with eq_rhs = def_e}::accu, def.eq_lhs @ vl *)
70
      (* 	  ) ([],[]) local_defs *)
71
      (* in *)
72
      List.map (fun e -> 
73
	Format.eprintf "lin cleaning %a@." Printers.pp_expr e.eq_rhs; 
74
	let res = {e with eq_rhs = Corelang.substitute_expr ~open_pre:true non_memory_vars local_defs e.eq_rhs } in
75
	Format.eprintf "lin cleaned %a@." Printers.pp_expr res.eq_rhs; 
76
	Eq res
77
      ) mem_defs in
78
      Format.eprintf "lin main def ok@.";
79
    let aut_defs' = List.map (fun a -> Aut {a with aut_handlers = List.map elim_handler a.aut_handlers}) aut_defs in   
80
    Format.eprintf "lin aut def ok@.";
81
    mem_defs'@aut_defs', memory_vars
82

    
83
and elim_handler h = 
84
  Format.eprintf "lin elim handler@.";
85
  let stmts, mem_vid = elim_vars (List.map (fun v -> v.var_id) h.hand_locals) h.hand_stmts in
86
  { h with
87
    hand_locals = (List.filter (fun v -> List.mem v.var_id mem_vid) h.hand_locals); 
88
    hand_stmts = stmts }
89

    
90

    
91
    
92
  
93

    
94
(* This function returns a modified node. 
95
   TODO make sure there is no function call in the node (or nothing with a lhs of length > 1 
96
 *)
97
    let node nd value = 
98
      (* We check that value is a tuple compatible with the input arguments of the node *)
99
      Format.eprintf "lin node@.";
100
      if not (check_input nd value) then
101
	nd (* not applicable *)
102
      else (
103
	Log.report ~level:1 
104
	  (fun fmt -> Format.fprintf fmt "Linearizing node %s around point %a@." 
105
	    nd.node_id 
106
	    Printers.pp_eexpr value
107
	  );
108
	(* Node is simplified. No more local non memory variables *)
109
	let unrolled_stmts, mem_vid = 
110
	  elim_vars (List.map (fun v -> v.var_id) nd.node_locals) nd.node_stmts 
111
	in
112
	(* Each expression is expressed as (expr -> Pre expr) ie. normalized wrt pre *)
113
	let stmts = unrolled_stmts in
114
	{ nd with
115
	  node_locals = (List.filter (fun v -> List.mem v.var_id mem_vid) nd.node_locals); 
116
	  node_stmts = stmts
117
	}
118
      )
119

    
120
(* Local Variables: *)
121
(* compile-command:"make -C .." *)
122
(* End: *)
123