Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_export.ml @ d75eb6f1

History | View | Annotate | Download (3.66 KB)

1
(* Multiple export channels for switched systems:
2
- lustre
3
- matlab
4
- text
5
 *)
6
open Lustre_types
7
open Machine_code_types
8

    
9
let verbose = false
10
            
11
let to_lustre m sw_init sw_step init_out update_out =
12
  let orig_nd = m.mname in
13
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
14
  let vl = (* memories *)
15
    match sw_init with
16
    | [] -> assert false
17
    | (gl, up)::_ -> List.map (fun (v,_) -> v) up
18
  in
19
(*  let add_pre sw =
20
    List.map (fun (gl, up) ->
21
        List.map (fun (g,b) ->
22
            if not b then
23
              assert false (* should be guaranted by constrauction *)
24
            else
25
              add_pre_expr vl g) gl,
26
        List.map (fun (v,e) -> add_pre_expr vl e) up
27
      ) sw
28
  in
29
 *)
30
  
31
  let rec process_sw f_e sw =
32
    let process_branch g_opt up =
33
      let el = List.map (fun (v,e) -> f_e e) up in
34
      let loc = (List.hd el).expr_loc in
35
      let new_e = Corelang.mkexpr loc (Expr_tuple el) in
36
      match g_opt with
37
        None -> None, new_e, loc
38
      | Some g ->
39
         let g = f_e g in
40
         let ee = Corelang.mkeexpr loc g in
41
         let new_e = if verbose then
42
           {new_e with
43
             expr_annot =
44
               Some ({annots = [["seal";"guards"],ee];
45
                      annot_loc = loc})} else new_e 
46
         in
47
         Some g, new_e, loc
48
    in
49
    match sw with
50
    | [] -> assert false
51
    | [g_opt,up] -> ((* last case, no need to guard it *)
52
      let _, up_e, _ = process_branch g_opt up in
53
      up_e
54
    )
55
    | (g_opt,up)::tl ->
56
       let g_opt, up_e, loc = process_branch g_opt up in
57
       match g_opt with
58
       | None -> assert false (* How could this happen anyway ? *)
59
       | Some g ->
60
          let tl_e = process_sw f_e tl in
61
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
62
  in
63
    
64
  let e_init = process_sw (fun x -> x) sw_init in
65
  let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in
66
  let e_init_out = process_sw (fun x -> x) init_out in
67
  let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in
68
  let loc = Location.dummy_loc in 
69
  { copy_nd with
70
    node_id = copy_nd.node_id ^ "_seal";
71
    node_locals = m.mmemory;
72
    node_stmts = [Eq
73
                    { eq_loc = loc;
74
                      eq_lhs = vl; 
75
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step))
76
                    };
77
                 Eq
78
                    { eq_loc = loc;
79
                      eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
80
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
81
                    };
82
                 ]
83
(*
84
                   il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes
85

    
86

    
87
                                                                                                                                                                                        ecrire une expression
88

    
89
                                                                                                                                                                                        (mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2)
90

    
91
                                                                                                                                                                                                                                                                                         Il faut aussi calculer la fonction de sortie
92

    
93
  out1,out2 = if garde1 then e1,e2 else if garde2 ....
94
   *)    
95
  }