Project

General

Profile

« Previous | Next » 

Revision 40f8d0f9

Added by Pierre-Loïc Garoche over 9 years ago

Second (almost) working version

View differences:

src/horn_backend.ml
4 4 
open Machine_code
5 5 

  		




  6
  6
  
    

  		




  7
  
  
    
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id


  		




  
  7
  
    
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id


  		




  8
  8
  
    
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id


  		




  9
  9
  
    

  		




  10
  10
  
    
let pp_type fmt t =


  		




  ......




  21
  21
  
    
    


  		




  22
  22
  
    

  		




  23
  23
  
    
let pp_decl_var fmt id = 


  		




  24
  
  
    
  Format.fprintf fmt "(declare_var %s %a)"


  		




  
  24
  
    
  Format.fprintf fmt "(declare-var %s %a)"


  		




  25
  25
  
    
    id.var_id


  		




  26
  26
  
    
    pp_type id.var_type


  		




  27
  27
  
    

  		




  ......




  186
  186
  
    
     (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs 


  		




  187
  187
  
    
    )


  		




  188
  188
  
    

  		




  189
  
  
    
let pp_machine_reset (m: machine_t) self fmt inst =


  		




  
  189
  
    
let pp_machine_init (m: machine_t) self fmt inst =


  		




  190
  190
  
    
  let (node, static) = List.assoc inst m.minstances in


  		




  191
  191
  
    
  fprintf fmt "(%a %a%t%s->%s)"


  		




  192
  
  
    
    pp_machine_reset_name (node_name node)


  		




  
  192
  
    
    pp_machine_init_name (node_name node)


  		




  193
  193
  
    
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static


  		




  194
  194
  
    
    (Utils.pp_final_char_if_non_empty " " static)


  		




  195
  195
  
    
    self inst


  		




  ......




  206
  206
  
    
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =


  		




  207
  207
  
    
  match instr with 


  		




  208
  208
  
    
  | MReset i ->


  		




  209
  
  
    
    pp_machine_reset m self fmt i


  		




  
  209
  
    
    pp_machine_init m self fmt i


  		




  210
  210
  
    
  | MLocalAssign (i,v) ->


  		




  211
  211
  
    
    pp_assign


  		




  212
  212
  
    
      m self (pp_horn_var m) fmt


  		




  ......




  249
  249
  
    
   Format.pp_print_newline fmt ();


  		




  250
  250
  
    
   (* Declaring predicate *)


  		




  251
  251
  
    
   Format.fprintf fmt "(declare-rel %a (%a))@."


  		




  252
  
  
    
     pp_machine_reset_name m.mname.node_id


  		




  
  252
  
    
     pp_machine_init_name m.mname.node_id


  		




  253
  253
  
    
     (Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m));


  		




  254
  254
  
    
   


  		




  255
  255
  
    
   Format.fprintf fmt "(declare-rel %a (%a))@."


  		












Also available in:  Unified diff