Project

General

Profile

« Previous | Next » 

Revision c76f1d66

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

Working on bugs

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@149 041b043f-8d7c-46b2-b46e-ef0dd855326e

View differences:

src/horn_backend.ml
28 28 
let pp_var fmt id = Format.pp_print_string fmt id.var_id
29 29 

  		




  30
  30
  
    

  		




  
  31
  
    
let prefix prefix x = if prefix = "" then x else prefix ^ "." ^ x 


  		




  
  32
  
    
let rename_machine p = rename (fun n -> prefix p n)


  		




  
  33
  
    
let rename_machine_list p = List.map (rename_machine p)


  		




  
  34
  
    
    


  		




  31
  35
  
    
let rename f = (fun v -> {v with var_id = f v.var_id } )


  		




  32
  
  
    
let rename_current prefix =  rename (fun n -> prefix ^ "." ^ n ^ "_c")


  		




  33
  
  
    
let rename_current_list prefix = List.map (rename_current prefix)


  		




  34
  
  
    
let rename_next prefix = rename (fun n -> prefix ^ "." ^ n ^ "_x")


  		




  35
  
  
    
let rename_next_list prefix = List.map (rename_next prefix)


  		




  36
  
  
    
let rename_machine prefix = rename (fun n -> prefix ^ "." ^ n)


  		




  37
  
  
    
let rename_machine_list prefix = List.map (rename_machine prefix)


  		




  
  36
  
    
let rename_current =  rename (fun n -> n ^ "_c")


  		




  
  37
  
    
let rename_current_list = List.map rename_current


  		




  
  38
  
    
let rename_next = rename (fun n -> n ^ "_x")


  		




  
  39
  
    
let rename_next_list = List.map rename_next


  		




  
  40
  
    

  		




  38
  41
  
    

  		




  39
  42
  
    
let get_machine machines node_name = 


  		




  40
  43
  
    
  List.find (fun m  -> m.mname.node_id = node_name) machines 


  		




  41
  44
  
    

  		




  42
  
  
    
let full_memory_vars machines prefix machine =


  		




  43
  
  
    
  let rec aux prefix m =


  		




  44
  
  
    
    let pref x = if prefix = "" then x else prefix ^ "." ^ x in 


  		




  45
  
  
    
    (rename_machine_list (pref m.mname.node_id) m.mmemory) @


  		




  
  45
  
    
let full_memory_vars machines machine =


  		




  
  46
  
    
  let rec aux fst prefix_s m =


  		




  
  47
  
    
    (rename_machine_list (if fst then prefix else prefix ^ "." ^ m.mname.node_id) m.mmemory) @


  		




  46
  48
  
    
      List.fold_left (fun accu (id, (n, _)) -> 


  		




  47
  49
  
    
	let name = node_name n in 


  		




  48
  50
  
    
	if name = "_arrow" then accu else


  		




  49
  51
  
    
	  let machine_n = get_machine machines name in


  		




  50
  
  
    
	( aux (pref id) machine_n ) @ accu


  		




  
  52
  
    
	( aux false (prefix_s ^ "." ^ id) machine_n ) @ accu


  		




  51
  53
  
    
      ) [] (m.minstances) 


  		




  52
  54
  
    
  in


  		




  53
  
  
    
  aux prefix machine


  		




  
  55
  
    
  aux true machine.mname.node_id machine


  		




  54
  56
  
    

  		




  55
  57
  
    
let machine_vars machines m = 


  		




  56
  58
  
    
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@


  		




  57
  59
  
    
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@


  		




  58
  
  
    
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 


  		




  59
  
  
    
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 


  		




  
  60
  
    
    (rename_current_list (full_memory_vars machines m)) @ 


  		




  
  61
  
    
    (rename_next_list (full_memory_vars machines m)) 


  		




  60
  62
  
    

  		




  61
  63
  
    
let step_vars machines m = 


  		




  62
  64
  
    
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@


  		




  63
  65
  
    
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@


  		




  64
  
  
    
    (rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @ 


  		




  65
  
  
    
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 


  		




  
  66
  
    
    (rename_current_list (full_memory_vars machines m)) @ 


  		




  
  67
  
    
    (rename_next_list (full_memory_vars machines m)) 


  		




  66
  68
  
    

  		




  67
  69
  
    
let init_vars machines m = 


  		




  68
  70
  
    
    (rename_machine_list m.mname.node_id m.mstep.step_inputs)@


  		




  69
  71
  
    
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)@


  		




  70
  
  
    
    (rename_next_list m.mname.node_id (full_memory_vars machines "" m)) 


  		




  71
  
  
    

  		




  
  72
  
    
    (rename_next_list (full_memory_vars machines m)) 


  		




  72
  73
  
    
  


  		




  73
  74
  
    
(********************************************************************************************)


  		




  74
  75
  
    
(*                    Instruction Printing functions                                        *)


  		




  ......




  110
  111
  
    
      if Types.is_array_type v.var_type


  		




  111
  112
  
    
      then assert false 


  		




  112
  113
  
    
      else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)


  		




  113
  
  
    
    | Fun (n, vl)   -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl


  		




  
  114
  
    
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl


  		




  114
  115
  
    

  		




  115
  116
  
    
(* Prints a [value] indexed by the suffix list [loop_vars] *)


  		




  116
  117
  
    
let rec pp_value_suffix self pp_value fmt value =


  		












Also available in:  Unified diff