Added alias for types (aka typedef)

For instance:
type metres = int
type metres = MyLib.longueur
type matrice = metres^10^100

Code generation in C (with typedef) included. The 
code uses the aliases for traceability.

compiler/global/modules.ml

@@ -172,3 +172,15 @@ let currentname longname =
     | Modname{ qual = q; id = id} ->
         if current.name = q then Name(id) else longname
 
+exception Undefined_type of longname
+(** @return the unaliased version of a type. *)
+let rec unalias_type = function
+  | Tid ty_name ->
+      (try
+        let { qualid = q; info = ty_desc } = find_type ty_name in
+          match ty_desc with
+            | Talias ty -> unalias_type ty
+            | _ -> Tid (Modname q)
+      with Not_found -> raise (Undefined_type ty_name))
+  | Tarray (ty, n) -> Tarray(unalias_type ty, n)
+  | Tprod ty_list -> Tprod (List.map unalias_type ty_list)

compiler/global/signature.ml

@@ -37,7 +37,11 @@ type node =
 type field = { f_name : name; f_type : ty }
 type structure = field list
 
-type type_def = | Tabstract | Tenum of name list | Tstruct of structure
+type type_def =
+  | Tabstract
+  | Talias of ty
+  | Tenum of name list
+  | Tstruct of structure
 
 type const_def = { c_name : name; c_type : ty; c_value : static_exp }
 

compiler/heptagon/analysis/typing.ml

@@ -213,6 +213,10 @@ let array_size ty =
     | Tarray (_, e) -> e
     | _ -> error (Esubscripted_value_not_an_array ty)
 
+let unalias_type ty =
+  try unalias_type ty
+  with Undefined_type ln -> error (Eundefined (fullname ln))
+
 let rec unify t1 t2 =
   match t1, t2 with
     | b1, b2 when b1 = b2 -> ()
@@ -228,7 +232,9 @@ let rec unify t1 t2 =
     | _ -> raise Unify
 
 let unify t1 t2 =
-  try unify t1 t2 with Unify -> error (Etype_clash(t1, t2))
+  let ut1 = unalias_type t1 in
+  let ut2 = unalias_type t2 in
+  try unify ut1 ut2 with Unify -> error (Etype_clash(t1, t2))
 
 let kind f ty_desc =
   let ty_of_arg v = v.a_type in
@@ -429,7 +435,7 @@ let rec check_type const_env = function
   | Tarray(ty, e) ->
       let typed_e = expect_static_exp const_env (Tid Initial.pint) e in
         Tarray(check_type const_env ty, typed_e)
-  | Tid(ty_name) ->
+  | Tid ty_name ->
       (try Tid(Modname((find_type ty_name).qualid))
        with Not_found -> error (Eundefined(fullname ty_name)))
   | Tprod l ->
@@ -1075,6 +1081,7 @@ let deftype { t_name = n; t_desc = tdesc; t_loc = loc } =
   try
     match tdesc with
       | Type_abs -> add_type n Tabstract
+      | Type_alias ln -> add_type n (Talias ln)
       | Type_enum(tag_name_list) ->
           add_type n (Tenum tag_name_list);
           List.iter (fun tag -> add_constr tag (Tid (longname n))) tag_name_list

compiler/heptagon/hept_printer.ml

@@ -263,6 +263,8 @@ and print_block ff { b_local = v_list; b_equs = eqs; b_defnames = defnames } =
 let print_type_def ff { t_name = name; t_desc = tdesc } =
   match tdesc with
     | Type_abs -> fprintf ff "@[type %s@\n@]" name
+    | Type_alias ty ->
+        fprintf ff  "@[type %s@ = %a\n@]" name  print_type ty
     | Type_enum(tag_name_list) ->
         fprintf ff "@[type %s = " name;
         print_list_r print_name "" "| " "" ff tag_name_list;

compiler/heptagon/heptagon.ml

@@ -98,7 +98,11 @@ and last = Var | Last of static_exp option
 
 type type_dec = { t_name : name; t_desc : type_dec_desc; t_loc : location }
 
-and type_dec_desc = Type_abs | Type_enum of name list | Type_struct of structure
+and type_dec_desc =
+  | Type_abs
+  | Type_alias of ty
+  | Type_enum of name list
+  | Type_struct of structure
 
 type contract = {
   c_assume : exp;

compiler/heptagon/parsing/hept_parser.mly

@@ -121,6 +121,8 @@ type_decs:
 type_dec:
   | TYPE IDENT
       { mk_type_dec $2 Type_abs (Loc($startpos,$endpos)) }
+  | TYPE IDENT EQUAL ty_ident
+      { mk_type_dec $2 (Type_alias $4) (Loc($startpos,$endpos)) }
   | TYPE IDENT EQUAL enum_ty_desc
       { mk_type_dec $2 (Type_enum ($4)) (Loc($startpos,$endpos)) }
   | TYPE IDENT EQUAL struct_ty_desc
@@ -248,8 +250,8 @@ ident_list:
 ;
 
 ty_ident:
-  | IDENT
-      { Tid(Name($1)) }
+  | longname
+      { Tid $1 }
   | ty_ident POWER simple_exp
       { Tarray ($1, $3) }
 ;

compiler/heptagon/parsing/hept_parsetree.ml

@@ -110,6 +110,7 @@ type type_dec =
 
 and type_desc =
   | Type_abs
+  | Type_alias of ty
   | Type_enum of name list
   | Type_struct of (name * ty) list
 

compiler/heptagon/parsing/hept_scoping.ml

@@ -300,6 +300,7 @@ let translate_node const_env env node =
 let translate_typedec const_env ty =
   let onetype = function
     | Type_abs -> Heptagon.Type_abs
+    | Type_alias ty -> Heptagon.Type_alias (translate_type const_env ty)
     | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list)
     | Type_struct(field_ty_list) ->
         let translate_field_type (f,ty) =

compiler/main/hept2mls.ml

@@ -388,6 +388,7 @@ let typedec
     {Heptagon.t_name = n; Heptagon.t_desc = tdesc; Heptagon.t_loc = loc} =
   let onetype = function
     | Heptagon.Type_abs -> Type_abs
+    | Heptagon.Type_alias ln -> Type_alias ln
     | Heptagon.Type_enum tag_list -> Type_enum tag_list
     | Heptagon.Type_struct field_ty_list ->
         Type_struct field_ty_list

compiler/main/mls2obc.ml

@@ -473,6 +473,7 @@ let translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc;
   let tdesc =
     match tdesc with
       | Minils.Type_abs -> Type_abs
+      | Minils.Type_alias ln -> Type_alias ln
       | Minils.Type_enum tag_name_list -> Type_enum tag_name_list
       | Minils.Type_struct field_ty_list ->
           Type_struct field_ty_list

compiler/minils/minils.ml

@@ -34,6 +34,7 @@ type type_dec = {
 
 and tdesc =
   | Type_abs
+  | Type_alias of ty
   | Type_enum of name list
   | Type_struct of structure
 

compiler/minils/mls_printer.ml

@@ -169,6 +169,8 @@ let rec print_type_dec ff { t_name = name; t_desc = tdesc } =
     adding a heading space itself when needed and exporting a break*)
 and print_type_desc ff = function
   | Type_abs -> () (* that's the reason of the exception *)
+  | Type_alias ty ->
+      fprintf ff  " =@ %a" print_type ty
   | Type_enum tag_name_list ->
       fprintf ff " =@ %a" (print_list print_name """|""") tag_name_list
   | Type_struct f_ty_list ->

compiler/obc/c/c.ml

@@ -107,6 +107,8 @@ and cstm =
 (** C type declarations ; will {b always} correspond to a typedef in emitted
     source code. *)
 type cdecl =
+  (** C typedef declaration (alias, name)*)
+  | Cdecl_typedef of cty * string
     (** C enum declaration, with associated value tags. *)
   | Cdecl_enum of string * string list
     (** C structure declaration, with each field's name and type. *)
@@ -255,6 +257,9 @@ let pp_cdecl fmt cdecl = match cdecl with
   | Cdecl_enum (s, sl) ->
       fprintf fmt "@[<v>@[<v 2>typedef enum {@ %a@]@ } %a;@ @]@\n"
         (pp_list1 pp_string ",") sl  pp_string s
+  | Cdecl_typedef (cty, n) ->
+      fprintf fmt "@[<v>@[<v 2>typedef %a;@ @]@\n"
+        pp_vardecl (n, cty)
   | Cdecl_struct (s, fl) ->
       let pp_field fmt (s, cty) =
         fprintf fmt "@ %a;" pp_vardecl (s,cty) in

compiler/obc/c/c.mli

@@ -74,6 +74,8 @@ and cstm =
 (** C type declarations ; will {b always} correspond to a typedef in emitted
     source code. *)
 type cdecl =
+  (** C typedef declaration (type, alias)*)
+  | Cdecl_typedef of cty * string
   (** C enum declaration, with associated value tags. *)
   | Cdecl_enum of string * string list
   (** C structure declaration, with each field's name and type. *)

compiler/obc/c/cgen.ml

@@ -192,12 +192,25 @@ let rec assoc_type n var_env =
         else
           assoc_type n var_env
 
+(** @return the unaliased version of a type. *)
+let rec unalias_ctype = function
+  | Cty_id ty_name ->
+      (try
+        let { qualid = q; info = ty_desc } = find_type (longname ty_name) in
+          match ty_desc with
+            | Talias ty -> unalias_ctype (ctype_of_otype ty)
+            | _ -> Cty_id ty_name
+      with Not_found -> Cty_id ty_name)
+  | Cty_arr (n, cty) -> Cty_arr (n, unalias_ctype cty)
+  | Cty_ptr cty -> Cty_ptr (unalias_ctype cty)
+  | cty -> cty
+
 (** Returns the type associated with the lhs [lhs]
     in the environnement [var_env] (which is an association list
     mapping strings to cty).*)
 let rec assoc_type_lhs lhs var_env =
   match lhs with
-    | Cvar x -> assoc_type x var_env
+    | Cvar x -> unalias_ctype (assoc_type x var_env)
     | Carray (lhs, _) ->
         let ty = assoc_type_lhs lhs var_env in
         array_base_ctype ty [1]
@@ -545,8 +558,6 @@ let fun_def_of_step_fun name obj_env mem objs md =
   (** Its arguments, translating Obc types to C types and adding our internal
       memory structure. *)
   let args = step_fun_args name md in
-  (** Its normal local variables. *)
-  let local_vars = List.map cvar_of_vd md.m_body.b_locals in
 
   (** Out vars for function calls *)
   let out_vars =
@@ -557,7 +568,7 @@ let fun_def_of_step_fun name obj_env mem objs md =
 
   (** The body *)
   let mems = List.map cvar_of_vd (mem@md.m_outputs) in
-  let var_env = args @ mems @ local_vars @ out_vars in
+  let var_env = args @ mems @ out_vars in
   let body = cstm_of_act_list var_env obj_env md.m_body in
 
   (** Substitute the return value variables with the corresponding
@@ -653,6 +664,7 @@ let decls_of_type_decl otd =
   let name = otd.t_name in
   match otd.t_desc with
     | Type_abs -> [] (*assert false*)
+    | Type_alias ty -> [Cdecl_typedef (ctype_of_otype ty, name)]
     | Type_enum nl ->
         let name = !global_name ^ "_" ^ name in
         [Cdecl_enum (otd.t_name, nl);
@@ -672,6 +684,7 @@ let cdefs_and_cdecls_of_type_decl otd =
   let name = otd.t_name in
   match otd.t_desc with
     | Type_abs -> [], [] (*assert false*)
+    | Type_alias ty -> [], [Cdecl_typedef (ctype_of_otype ty, name)]
     | Type_enum nl ->
         let of_string_fun = Cfundef
           { f_name = name ^ "_of_string";

compiler/obc/obc.ml

@@ -27,6 +27,7 @@ type type_dec =
 
 and tdesc =
   | Type_abs
+  | Type_alias of ty
   | Type_enum of name list
   | Type_struct of structure
 

compiler/obc/obc_printer.ml

@@ -145,6 +145,8 @@ let print_def ff
 let print_type_def ff { t_name = name; t_desc = tdesc } =
   match tdesc with
     | Type_abs -> fprintf ff "@[type %s@\n@]" name
+    | Type_alias ty ->
+        fprintf ff  "@[type %s@ = %a\n@]" name  print_type ty
     | Type_enum(tag_name_list) ->
         fprintf ff "@[type %s = " name;
         print_list_r print_name "" "|" "" ff tag_name_list;