Project

General

Profile

Revision 7c95dcab

View differences:

TODO.org
29 29
** clock calculus
30 30
*** extension from named clocks to valued clocks ?
31 31
*** static inputs should be polymorphic, as global constants are: done
32

  
33
* Horn backend
34
** enum types for automaton
35
   - issues with MBranches and clocks
36
     - control-on-clock generates a "if cond then expr else nothing
37
     - it has to be expressed in a functional way to enable its expression as
38
       horn
39

  
src/backends/Horn/horn_backend.ml
22 22
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
23 23
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
24 24

  
25
let pp_type fmt t =
25
let rec pp_type fmt t =
26 26
  match (Types.repr t).Types.tdesc with
27
  | Types.Tbool           -> Format.fprintf fmt "Bool"
28
  | Types.Tint            -> Format.fprintf fmt "Int"
29
  | Types.Treal           -> Format.fprintf fmt "Real"
30
  | Types.Tclock _
27
  | Types.Tbool           -> fprintf fmt "Bool"
28
  | Types.Tint            -> fprintf fmt "Int"
29
  | Types.Treal           -> fprintf fmt "Real"
30
  | Types.Tconst ty       -> pp_print_string fmt ty
31
  | Types.Tclock t        -> pp_type fmt t
31 32
  | Types.Tarray _
32 33
  | Types.Tstatic _
33
  | Types.Tconst _
34 34
  | Types.Tarrow _
35 35
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36 36
    Types.print_ty t; assert false
......
231 231
    (Utils.pp_final_char_if_non_empty " " static)
232 232
    self inst
233 233

  
234
(* TODO *)
235
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
234

  
235
let rec pp_bool_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
236 236
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
237 237
    (pp_horn_val self (pp_horn_var m)) c
238 238
    (Utils.pp_newline_if_non_empty tl)
239 239
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
240 240
    (Utils.pp_newline_if_non_empty el)
241 241
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
242

  
242
(* and pp_enum_conditional machines ?(init=false)  (m: machine_t) self fmt g hl = *)
243
(* (\* TODO: check that the enum has all its constructor defined: Xavier how have you handled that, could we have partial definition? *\) *)
244
(*   match hl with *)
245
(*   | [] -> assert false *)
246
(*   | [el] -> Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self) fmt el *)
247
(*   | hd::tl -> *)
248
(*   fprintf fmt "@[<v 2>if (= %a %a) {%t%a@]@,@[<v 2>} else {@.(%a)xxxx@]@,}" *)
249
(*     (pp_horn_val self (pp_horn_var m)) c *)
250
(*     TODOg *)
251
(*     (Utils.pp_newline_if_non_empty tl) *)
252
(*     (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) hd *)
253
(*     pp_print_newline fmt; *)
254
    
255
    
256
(* fprintf fmt  *)
243 257
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
244 258
  match instr with
245 259
  | MReset i ->
......
256 270
    assert false (* This should not happen anymore *)
257 271
  | MStep (il, i, vl) ->
258 272
    pp_instance_call machines ~init:init m self fmt i vl il
259
  | MBranch (g,hl) ->
260
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
261
    then (* boolean case, needs special treatment in C because truth value is not unique *)
262
      (* may disappear if we optimize code by replacing last branch test with default *)
263
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
264
      let el = try List.assoc tag_false hl with Not_found -> [] in
265
      pp_conditional machines ~init:init m self fmt g tl el
266
    else assert false (* enum type case *)
273
  | MBranch (g,hl) -> (* should not be produced *)
274
    assert false
275

  
276
    (* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
277
    (* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
278
    (*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
279
    (*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
280
    (*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
281
    (*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
282
    (* else (\* enum type case *\) *)
283

  
284
    (*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
267 285

  
268 286

  
269 287
(**************************************************************)
......
520 538
      get_cex machines fmt node machine)
521 539
end
522 540

  
541
let print_type_definitions fmt =
542
  let cpt_type = ref 0 in
543
  Hashtbl.iter (fun typ decl ->
544
		match typ with
545
		| Tydec_const var ->
546
		   (match decl.top_decl_desc with
547
		    | TypeDef tdef -> (
548
		      match tdef.tydef_desc with
549
		      | Tydec_enum tl ->
550
			incr cpt_type;
551
			fprintf fmt "(declare-datatypes () ((%s %a));@.@."
552
			  var
553
			  (Utils.fprintf_list ~sep:" " pp_print_string) tl
554
		      | _ -> assert false
555
		    )
556
		    | _ -> assert false
557
		   )
558
		| _        -> ()) type_table
559

  
523 560

  
524 561
let translate fmt basename prog machines =
562
  (* We print typedef *)
563
  print_type_definitions fmt;
564

  
525 565
  List.iter (print_machine machines fmt) (List.rev machines);
526 566
  main_print machines fmt
527 567

  
src/machine_code.ml
292 292
  | "C" -> specialize_to_c expr
293 293
  | _   -> expr
294 294

  
295
let rec merge_to_ite g hl =
296
  let loc = Location.dummy_loc in
297
  let mkcst x = mkexpr loc (Expr_const (Const_tag x)) in
298
  let g_expr = mkcst g in
299
  match hl with
300
  | [] -> assert false
301
  | [_, e] -> e
302
  | (l_c,l_e)::tl -> 
303
    let cond_expr = 
304
      mkpredef_call loc "=" [g_expr; mkcst l_c]
305
    in
306
    mkexpr loc (Expr_ite (cond_expr, l_e, merge_to_ite g tl))
307
      
295 308
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
296 309
  let expr = specialize_op expr in
297 310
 match expr.expr_desc with
......
305 318
 | Expr_fby _
306 319
 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
307 320
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
308
 | Expr_merge   (x, _)              -> raise NormalizationError
321
 | Expr_merge   (g, hl)              -> (
322
   (* Special treatment for functional backends. Is transformed into Ite *)
323
   match !Options.output with
324
   | "horn" -> translate_expr node  args (merge_to_ite g hl)
325
   | ("C" | "java")          -> raise NormalizationError (* should have been replaced by MBranch *)
326
   | _ ->
327
     (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
328

  
329
 )
330
  
309 331
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
310 332
   let nd = node_from_name id in
311 333
   Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
......
397 419
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
398 420
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
399 421
      backends. *)
400
  | [x], Expr_ite   (c, t, e)
422
  | [x], Expr_ite   _
423
  (* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *)
424
  | [x], Expr_merge _ 
401 425
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
426

  
427
      (* Remark for Ocaml: the when is shared among the two patterns *)
402 428
      ->
403 429
    let var_x = get_node_var x node in
404 430
    (m,
......
409 435
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
410 436
    )
411 437

  
438
 
412 439
  | [x], _                                       -> (
413 440
    let var_x = get_node_var x node in
414 441
    (m, si, j, d,

Also available in: Unified diff