Project

General

Profile

Revision 03c767b1 src/tools/seal/seal_export.ml

View differences:

src/tools/seal/seal_export.ml
5 5
 *)
6 6
open Lustre_types
7 7
open Machine_code_types
8
open Seal_utils
8 9

  
9 10
let verbose = true
10
            
11
let sw_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 process_sw vars f_e sw =
32
    let process_branch g_opt up =
33
      let el = List.map (fun (v,e) -> v, f_e e) up in
34
      (* Sorting list of elements, according to vars, safety check to
11

  
12
let process_sw vars f_e sw =
13
  let process_branch g_opt up =
14
    let el = List.map (fun (v,e) -> v, f_e e) up in
15
    (* Sorting list of elements, according to vars, safety check to
35 16
         ensure that no variable is forgotten. *)
36
      let el, forgotten = List.fold_right (fun v (res, remaining) ->
37
                   let vid = v.var_id in
38
                   if List.mem_assoc vid remaining then
39
                     ((List.assoc vid remaining)::res),
40
                     (List.remove_assoc vid remaining)
41
                   else
42
                     assert false (* Missing variable v in list *)
43
                            ) vars ([], el)
44
      in
45
      assert (forgotten = []);
46
      let loc = (List.hd el).expr_loc in
47
      let new_e = Corelang.mkexpr loc (Expr_tuple el) in
48
      match g_opt with
49
        None -> None, new_e, loc
50
      | Some g ->
51
         let g = f_e g in
52
         let ee = Corelang.mkeexpr loc g in
53
         let new_e = if verbose then
54
           {new_e with
55
             expr_annot =
56
               Some ({annots = [["seal";"guards"],ee];
57
                      annot_loc = loc})} else new_e 
58
         in
59
         Some g, new_e, loc
17
    let el, forgotten = List.fold_right (fun v (res, remaining) ->
18
                            let vid = v.var_id in
19
                            if List.mem_assoc vid remaining then
20
                              ((List.assoc vid remaining)::res),
21
                              (List.remove_assoc vid remaining)
22
                            else (
23
                              Format.eprintf
24
                                "Looking for variable %s in remaining expressions: [%a]@."
25
                                vid
26
                                (Utils.fprintf_list ~sep:";@ "
27
                                   (fun fmt (id,e) ->
28
                                     Format.fprintf fmt
29
                                       "(%s -> %a)"
30
                                       id
31
                                       Printers.pp_expr e))
32
                                remaining;
33
                              assert false (* Missing variable v in list *)
34
                            )
35
                          ) vars ([], el)
60 36
    in
61
    let rec process_sw f_e sw = 
62
      match sw with
37
    assert (forgotten = []);
38
    let loc = (List.hd el).expr_loc in
39
    let new_e = Corelang.mkexpr loc (Expr_tuple el) in
40
    match g_opt with
41
      None -> None, new_e, loc
42
    | Some g ->
43
       let g = f_e g in
44
       let ee = Corelang.mkeexpr loc g in
45
       let new_e = if verbose then
46
                     {new_e with
47
                       expr_annot =
48
                         Some ({annots = [["seal";"guards"],ee];
49
                                annot_loc = loc})} else new_e 
50
       in
51
       Some g, new_e, loc
52
  in
53
  let rec process_sw f_e sw = 
54
    match sw with
63 55
    | [] -> assert false
64 56
    | [g_opt,up] -> ((* last case, no need to guard it *)
65 57
      let _, up_e, _ = process_branch g_opt up in
......
68 60
    | (g_opt,up)::tl ->
69 61
       let g_opt, up_e, loc = process_branch g_opt up in
70 62
       match g_opt with
71
       | None -> assert false (* How could this happen anyway ? *)
63
       | None -> (
64
         Format.eprintf "SEAL issue: process_sw with %a"
65
           pp_sys sw
66
       ;
67
         assert false (* How could this happen anyway ? *)
68
       )
72 69
       | Some g ->
73 70
          let tl_e = process_sw f_e tl in
74 71
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
75
    in
76
    process_sw f_e sw
77 72
  in
73
  process_sw f_e sw
74

  
78 75
    
76
let sw_to_lustre m sw_init sw_step init_out update_out =
77
  let orig_nd = m.mname in
78
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
79
  let vl = (* memories *)
80
    match sw_init with
81
    | [] -> assert false
82
    | (gl, up)::_ -> List.map (fun (v,_) -> v) up
83
  in    
79 84
  let e_init = process_sw m.mmemory (fun x -> x) sw_init in
80 85
  let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in
81 86
  let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
......
96 101
                      eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out))
97 102
                    };
98 103
                 ];
99
    (*node_spec = Some (Contract contract);*)
100
                 
101
(*
102
                   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
103

  
104

  
105
                                                                                                                                                                                        ecrire une expression
106

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

  
109
                                                                                                                                                                                                                                                                                         Il faut aussi calculer la fonction de sortie
110

  
111
  out1,out2 = if garde1 then e1,e2 else if garde2 ....
112
   *)    
113 104
    }
114 105
  in
115 106
  new_nd, orig_nd

Also available in: Unified diff