Project

General

Profile

« Previous | Next » 

Revision f2c916b4

Added by Guillaume DAVY over 4 years ago

Ada: Correct some errors on the type checking due to polymorphic type.

View differences:

src/backends/Ada/ada_backend_ads.ml
31 31 
  let search_instr instruction =
32 32 
    match instruction.instr_desc with
33 33 
      | MStep (il, i, vl) when String.equal i ident -> [
34 
        (List.map (function x-> x.var_type) il,
35 
           List.map (function x-> x.value_type) vl)]
34 
        (List.map (function x-> x.value_type) vl,
35 
            List.map (function x-> x.var_type) il)]
36 36 
      | MBranch (_, l) -> List.flatten
37 37 
          (List.map (function x, y -> find_submachine_step_call ident y) l)
38 38 
      | _ -> []
......
44 44 
   @param t2 an other type
45 45 
   @param return true if the two types are Tbasic or Tunivar and equal
46 46 
**)
47 
let check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
47 
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
48 48 
  match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
49 49 
    | Types.Tbasic x, Types.Tbasic y -> x = y
50 50 
    | Types.Tunivar,  Types.Tunivar  -> t1.tid = t2.tid
51 
    | _ -> assert false (* TODO *)
51 
    | Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
52 
    | _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
53 
    | Types.Tstatic (_, t), _ -> check_type_equal t t2
54 
    | _, Types.Tstatic (_, t) -> check_type_equal t1 t
55 
    | _ -> eprintf "ERROR: %a | %a" pp_type t1 pp_type t2; assert false (* TODO *)
52 56 

  		




  53
  57
  
    
(** Extend a substitution to unify the two given types. Only the


  		




  54
  58
  
    
  first type can be polymorphic.


  		




  ......




  107
  111
  
    
   @return the correspondance between polymorphic type id and their instantiation


  		




  108
  112
  
    
**)


  		




  109
  113
  
    
let get_substitution machine ident submachine =


  		




  
  114
  
    
  eprintf "%s %s %s@." machine.mname.node_id ident submachine.mname.node_id;


  		




  110
  115
  
    
  (* extract the calls to submachines from the machine *)


  		




  111
  116
  
    
  let calls = find_submachine_step_call ident machine.mstep.step_instrs in


  		




  112
  117
  
    
  (* extract the first call  *)


  		




  ......




  126
  131
  
    
      and the call *)


  		




  127
  132
  
    
  assert (List.length machine_types = List.length call_types);


  		




  128
  133
  
    
  (* Unify the two lists of types *)


  		




  129
  
  
    
  let substituion = List.fold_left unification [] (List.combine machine_types call_types) in


  		




  
  134
  
    
  let substitution = List.fold_left unification [] (List.combine machine_types call_types) in


  		




  130
  135
  
    
  (* Assume that our substitution match all the possible


  		




  131
  136
  
    
       polymorphic type of the node *)


  		




  132
  137
  
    
  let polymorphic_types = find_all_polymorphic_type submachine in


  		




  133
  
  
    
  assert (List.length polymorphic_types = List.length substituion);


  		




  134
  
  
    
  assert (List.for_all (function x->List.mem_assoc x substituion) polymorphic_types);


  		




  135
  
  
    
  substituion


  		




  
  138
  
    
  assert (List.length polymorphic_types = List.length substitution);


  		




  
  139
  
    
  assert (List.for_all (function x->List.mem_assoc x substitution) polymorphic_types);


  		




  
  140
  
    
  substitution


  		




  136
  141
  
    

  		




  137
  142
  
    
(** Print the declaration of a state element of a subinstance of a machine.


  		




  138
  143
  
    
   @param machine the machine


  		












Also available in:  Unified diff