Project

General

Profile

Revision e8f55c25

View differences:

src/backends/Ada/ada_backend_common.ml
124 124
**)
125 125
let default_ada_cst cst_typ = match cst_typ with
126 126
  | Types.Basic.Tint  -> Const_int 0
127
  | Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
127
  | Types.Basic.Treal -> Const_real Real.zero
128 128
  | Types.Basic.Tbool -> Const_tag tag_false
129 129
  | _ -> assert false
130 130

  
......
200 200
let pp_ada_const fmt c =
201 201
  match c with
202 202
  | Const_int i                     -> pp_print_int fmt i
203
  | Const_real (c, e, s)            ->
204
      fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
203
  | Const_real r                    -> Real.pp_ada fmt r
205 204
  | Const_tag t                     -> pp_ada_tag fmt t
206 205
  | Const_string _ | Const_modeid _ ->
207 206
    (Format.eprintf
src/backends/C/c_backend_common.ml
226 226
let rec pp_c_const fmt c =
227 227
  match c with
228 228
    | Const_int i     -> pp_print_int fmt i
229
    | Const_real (c,e,s)-> pp_print_string fmt s (* Format.fprintf fmt "%ie%i" c e*)
229
    | Const_real r -> Real.pp fmt r
230 230
    (* | Const_float r   -> pp_print_float fmt r *)
231 231
    | Const_tag t     -> pp_c_tag fmt t
232 232
    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
src/backends/C/c_backend_src.ml
130 130
let rec pp_c_const_suffix var_type fmt c =
131 131
  match c with
132 132
    | Const_int i          -> pp_print_int fmt i
133
    | Const_real (_, _, s) -> pp_print_string fmt s
133
    | Const_real r         -> Real.pp fmt r
134 134
    | Const_tag t          -> pp_c_tag fmt t
135 135
    | Const_array ca       -> let var_type = Types.array_element_type var_type in
136 136
                              fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
src/backends/Horn/horn_backend_printers.ml
42 42
let rec pp_horn_const fmt c =
43 43
  match c with
44 44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real (_,_,s)   -> pp_print_string fmt s
45
    | Const_real r   -> Real.pp fmt r
46 46
    | Const_tag t    -> pp_horn_tag fmt t
47 47
    | _              -> assert false
48 48

  
src/corelang.ml
404 404
  | _                                  -> false
405 405
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
406 406

  
407
let tag_true = "true"
408
let tag_false = "false"
409 407
let tag_default = "default"
410 408

  
411 409
let const_is_bool c =
......
579 577
let sort_handlers hl =
580 578
 List.sort (fun (t, _) (t', _) -> compare t t') hl
581 579

  
582
let num_10 = Num.num_of_int 10
583

  
584
let cst_real_to_num n i =
585
  Num.(n // (num_10 **/ (num_of_int i)))
586

  
580
  
587 581
let rec is_eq_const c1 c2 =
588 582
  match c1, c2 with
589
  | Const_real (n1, i1, _), Const_real (n2, i2, _)
590
    -> let n1 = cst_real_to_num n1 i1 in
591
       let n2 = cst_real_to_num n2 i2 in
592
	    Num.eq_num n1 n2
583
  | Const_real r1, Const_real r2
584
    -> Real.eq r1 r1 
593 585
  | Const_struct lcl1, Const_struct lcl2
594 586
    -> List.length lcl1 = List.length lcl2
595 587
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
......
1414 1406
        
1415 1407
let mk_eq l e1 e2 =
1416 1408
  mkpredef_call l "=" [e1; e2]
1417
      
1409

  
1410

  
1411
let rec partial_eval e =
1412
  let pa = partial_eval in
1413
  let edesc =
1414
    match e.expr_desc with
1415
    | Expr_const _ -> e.expr_desc 
1416
    | Expr_ident id -> e.expr_desc
1417
    | Expr_ite (g,t,e) -> (
1418
       let g, t, e = pa g, pa t, pa e in
1419
       match g.expr_desc with
1420
       | Expr_const (Const_tag tag) when (tag = tag_true) -> t.expr_desc
1421
       | Expr_const (Const_tag tag) when (tag = tag_false) -> e.expr_desc
1422
       | _ -> Expr_ite (g, t, e)
1423
    )
1424
    | Expr_tuple t ->
1425
       Expr_tuple (List.map pa t)
1426
    | Expr_arrow (e1, e2) ->
1427
       Expr_arrow (pa e1, pa e2) 
1428
    | Expr_fby (e1, e2) ->
1429
       Expr_fby (pa e1, pa e2)
1430
    | Expr_pre e ->
1431
       Expr_pre (pa e)
1432
    | Expr_appl (op, args, opt) ->
1433
       let args = pa args in
1434
       if Basic_library.is_expr_internal_fun e then
1435
         Basic_library.partial_eval op args opt
1436
       else
1437
         Expr_appl (op, pa e, opt)
1438
    | Expr_array el ->
1439
       Expr_array (List.map pa el)
1440
    | Expr_access (e, d) ->
1441
       Expr_access (pa e, d)
1442
    | Expr_power (e, d) ->
1443
       Expr_power (pa e, d)
1444
    | Expr_when (e, id, l) ->
1445
       Expr_when (pa e, id, l)
1446
    | Expr_merge (id, gl) -> 
1447
       Expr_merge(id, List.map (fun (l, e) -> l, pa e) gl)
1448
  in
1449
  { e with expr_desc = edesc }
1450

  
1418 1451
    (* Local Variables: *)
1419 1452
    (* compile-command:"make -C .." *)
1420 1453
    (* End: *)
src/corelang.mli
70 70
val get_repr_type: type_dec_desc -> type_dec_desc
71 71
val is_user_type: type_dec_desc -> bool
72 72
val coretype_equal: type_dec_desc -> type_dec_desc -> bool
73
val tag_true: label
74
val tag_false: label
75 73
val tag_default: label
76 74
val tag_table: (label, top_decl) Hashtbl.t
77 75
val field_table: (label, top_decl) Hashtbl.t
......
190 188

  
191 189
val find_eq: ident list -> eq list -> eq * eq list
192 190

  
193
(* Extract a num to describe a real constant *)
194
val cst_real_to_num: Num.num -> int -> Num.num
195

  
196 191
val get_expr_calls: top_decl list -> expr -> Utils.ISet.t
197 192

  
198 193
val eq_has_arrows: eq -> bool
......
202 197
val add_pre_expr: ident list -> expr -> expr
203 198

  
204 199
val mk_eq: Location.t -> expr -> expr -> expr 
205
(* Local Variables: *)
200

  
201
(* Simple transformations: eg computation over constants *)
202
val partial_eval: expr -> expr
203

  
204
  (* Local Variables: *)
206 205
(* compile-command:"make -C .." *)
207 206
(* End: *)
src/lustre_types.ml
48 48

  
49 49
type constant =
50 50
  | Const_int of int
51
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
51
  | Const_real of Real.t
52 52
  | Const_array of constant list
53 53
  | Const_tag of label
54 54
  | Const_string of string (* used only for annotations *)
......
254 254
  | LocalContract of contract_desc
255 255
  | TopContract of top_decl list
256 256

  
257
let tag_true = "true"
258
let tag_false = "false"
257 259

  
258 260

  
259 261
(* Local Variables: *)
src/machine_code.ml
465 465
  in
466 466
  machines
467 467

  
468

  
469
(* Local Variables: *)
470
(* compile-command:"make -C .." *)
471
(* End: *)
468
    (* Local Variables: *)
469
    (* compile-command:"make -C .." *)
470
    (* End: *)
src/machine_code_common.ml
299 299
let rec value_of_dimension m dim =
300 300
  match dim.Dimension.dim_desc with
301 301
  | Dimension.Dbool b         ->
302
     mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool
302
     mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool
303 303
  | Dimension.Dint i          ->
304 304
     mk_val (Cst (Const_int i)) Type_predef.type_int
305 305
  | Dimension.Dident v        -> value_of_ident dim.Dimension.dim_loc m v
......
315 315

  
316 316
let rec dimension_of_value value =
317 317
  match value.value_desc with
318
  | Cst (Const_tag t) when t = Corelang.tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
319
  | Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
318
  | Cst (Const_tag t) when t = tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
319
  | Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
320 320
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i
321 321
  | Var v                                         -> Dimension.mkdim_ident Location.dummy_loc v.var_id
322 322
  | Fun (f, args)                                 -> Dimension.mkdim_appl  Location.dummy_loc f (List.map dimension_of_value args)
src/main_lustre_compiler.ml
80 80

  
81 81
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
82 82

  
83
  let machine_code = 
84
    Compiler_stages.stage2 prog 
83
  let prog, machine_code = 
84
    Compiler_stages.stage2 params prog 
85 85
  in
86 86

  
87 87
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ " Machine_code_common.pp_machines machine_code);
src/main_lustre_testgen.ml
76 76
    Options.output := "emf";
77 77
    let params = Backends.get_normalization_params () in
78 78
    let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
79
    let machine_code = Compiler_stages.stage2 prog_mcdc in
79
    let prog_mcdc, machine_code = Compiler_stages.stage2 params prog_mcdc in
80 80
    let source_emf = source_file ^ ".emf" in 
81 81
    let source_out = open_out source_emf in
82 82
    let fmt = formatter_of_out_channel source_out in
src/main_lustre_verifier.ml
56 56
  let module Verifier = (val verifier : VerifierType.S) in
57 57

  
58 58
  decr Options.verbose_level;
59
  let params = Verifier.get_normalization_params () in
59 60
  (* Normalizing it *)
60 61
  let prog, dependencies = 
61 62
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
62 63
    try
63 64
      incr Options.verbose_level;
64
      let params = Verifier.get_normalization_params () in
65 65
      decr Options.verbose_level;
66 66
      Compiler_stages.stage1 params prog dirname basename extension
67 67
    with Compiler_stages.StopPhase1 prog -> (
......
73 73

  
74 74
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
75 75

  
76
  let machine_code = 
77
    Compiler_stages.stage2 prog 
76
  let prog, machine_code = 
77
    Compiler_stages.stage2 params prog 
78 78
  in
79 79

  
80 80
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
src/mutation.ml
188 188
    let eshift = 10. ** (float_of_int shift) in
189 189
    let i = Random.int (1 + bound * (int_of_float eshift)) in
190 190
    let f = float_of_int i /. eshift in
191
    (Num.num_of_int i, shift, string_of_float f)
191
    Real.create (string_of_int i) shift (string_of_float f)
192 192
  else 
193 193
    r
194 194

  
......
224 224
let rdm_mutate_const_value c =
225 225
  match c with
226 226
  | Const_int i -> Const_int (rdm_mutate_int i)
227
  | Const_real (n, i, s) -> let (n', i', s') = rdm_mutate_real (n, i, s) in Const_real (n', i', s')
227
  | Const_real r -> Const_real (rdm_mutate_real r)
228 228
  | Const_array _
229 229
  | Const_string _
230 230
  | Const_modeid _
src/parsers/lexerLustreSpec.mll
90 90
  | blank +
91 91
      {token lexbuf}
92 92
  | (('-'? ['0'-'9'] ['0'-'9']* as l) '.' (['0'-'9']* as r)) as s
93
      {REAL (Num.num_of_string (l^r), String.length r, s)}
93
      {REAL (Real.create (l^r) (String.length r) s)}
94 94
  | (('-'? ['0'-'9']+ as l)  '.' (['0'-'9']+ as r) ('E'|'e') (('+'|'-') ['0'-'9'] ['0'-'9']* as exp)) as s
95
      {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp, s)}
95
      {REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)}
96 96
  | '-'? ['0'-'9']+ 
97 97
      {INT (int_of_string (Lexing.lexeme lexbuf)) }
98 98
 (* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s
src/parsers/lexer_lustre.mll
119 119
| blank +
120 120
    {token lexbuf}
121 121
| ((['0'-'9']+ as l)  '.' (['0'-'9']* as r) ('E'|'e') (('+'|'-')? ['0'-'9']+ as exp)) as s
122
    {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp , s)}
122
    {REAL (Real.create (l^r) (String.length r + -1 * int_of_string exp) s)}
123 123
| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s
124
    {REAL (Num.num_of_string (l^r), String.length r, s)}
124
    {REAL (Real.create (l^r) (String.length r) s)}
125 125
| ['0'-'9']+ 
126 126
    {INT (int_of_string (Lexing.lexeme lexbuf)) }
127 127
| "tel." {TEL}
src/parsers/parser_lustre.mly
54 54
%}
55 55

  
56 56
%token <int> INT
57
%token <Num.num * int * string> REAL
57
%token <Real.t> REAL
58 58

  
59 59
%token <string> STRING
60 60
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
......
470 470
expr:
471 471
/* constants */
472 472
  INT {mkexpr (Expr_const (Const_int $1))}
473
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
473
| REAL {mkexpr (Expr_const (Const_real $1))}
474 474
| STRING {mkexpr (Expr_const (Const_string $1))}
475 475
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} 
476 476
    
......
606 606

  
607 607
signed_const:
608 608
  INT {Const_int $1}
609
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
609
| REAL {Const_real $1}
610 610
/* | FLOAT {Const_float $1} */
611 611
| tag_ident {Const_tag $1}
612 612
| MINUS INT {Const_int (-1 * $2)}
613
| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
613
| MINUS REAL {Const_real (Real.uminus $2)}
614 614
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
615 615
| LCUR signed_const_struct RCUR { Const_struct $2 }
616 616
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
src/plugins/salsa/machine_salsa_opt.ml
778 778
      match value.LT.eexpr_qfexpr.LT.expr_desc with 
779 779
      | LT.Expr_tuple [minv; maxv] -> (
780 780
	let get_cst e = match e.LT.expr_desc with 
781
	  | LT.Expr_const (LT.Const_real (c,e,s)) -> 
782
	    (* calculer la valeur c * 10^e *) 
783
	    Num.div_num c (Num.power_num (Num.num_of_int 10) (Num.num_of_int e))
781
	  | LT.Expr_const (LT.Const_real r) -> 
782
	     (* calculer la valeur c * 10^e *)
783
             Real.to_num r 
784 784
	  | _ -> 
785 785
	    Format.eprintf 
786 786
	      "Invalid salsa range: %a. It should be a pair of constant floats and %a is not a float.@." 
src/plugins/salsa/salsaDatatypes.ml
113 113
*)
114 114
  let inject cst = match cst with  
115 115
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
116
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
116
    | LT.Const_real r -> (* TODO: this is incorrect. We should rather
117 117
				  compute the error associated to the float *)
118 118
       (* let f = float_of_string s in *)
119
       let n = Corelang.cst_real_to_num c e in
119
       let n = Real.to_num r in
120 120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
121 121
       
122 122
       (* let r = Salsa.Prelude.r_of_f_aux r in *)
src/scheduling.ml
260 260
  	(Utils.fprintf_list ~sep:" ; " pp_eq_schedule) sch);
261 261
  let split_eqs = Splitting.tuple_split_eq_list eqs in
262 262
  (* Flatten schedule *)
263
  let sch = List.fold_right (fun vl res -> (List.map (fun v -> [v]) vl)@res) sch [] in
263
   let sch = List.fold_right (fun vl res -> (List.map (fun v -> [v]) vl)@res) sch [] in 
264 264
  let eqs_rev, remainder =
265 265
    List.fold_left
266 266
      (fun (accu, node_eqs_remainder) vl ->
src/types.ml
169 169
  | Tbasic t -> pp_basic fmt t
170 170
  | Tclock t ->
171 171
    fprintf fmt "%a%s" print_ty t (if !Options.kind2_print then "" else " clock")
172
  | Tstatic (d, t) ->
173
    fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t
172
  | Tstatic (d, t) -> print_ty fmt t
173
                        (* fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t *)
174 174
  | Tconst t ->
175 175
    fprintf fmt "%s" t
176 176
  | Tarrow (ty1,ty2) ->
src/typing.ml
259 259
	       else (fun c -> None) in
260 260
	     begin
261 261
	       unif t1' t2';
262
	       Dimension.eval Basic_library.eval_env eval_const e1;
263
	       Dimension.eval Basic_library.eval_env eval_const e2;
262
	       Dimension.eval Basic_library.eval_dim_env eval_const e1;
263
	       Dimension.eval Basic_library.eval_dim_env eval_const e2;
264 264
	       Dimension.unify ~semi:semi e1 e2;
265 265
	     end
266 266
          (* Special cases for machine_types. Rules to unify static types infered
......
359 359
	     then dimension_of_expr arg
360 360
	     else Dimension.mkdim_var () in
361 361
           let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
362
           Dimension.eval Basic_library.eval_env eval_const d;
362
           Dimension.eval Basic_library.eval_dim_env eval_const d;
363 363
           let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
364 364
           (match (* Types. *)get_static_value targ with
365 365
            | None    -> ()
......
477 477
        | Expr_power (e1, d) ->
478 478
           let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
479 479
           type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
480
           Dimension.eval Basic_library.eval_env eval_const d;
480
           Dimension.eval Basic_library.eval_dim_env eval_const d;
481 481
           let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
482 482
           let ty = (* Type_predef. *)type_array d ty_elt in
483 483
           expr.expr_type <- Expr_type_hub.export ty;
......
637 637
      let type_dim d =
638 638
        begin
639 639
          type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
640
          Dimension.eval Basic_library.eval_env eval_const d;
640
          Dimension.eval Basic_library.eval_dim_env eval_const d;
641 641
        end in
642 642
      let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
643 643

  

Also available in: Unified diff