[ctrl-n] Suppression of type declarations in Heptagon controller

TODO : move type declarations in separated module.

compiler/main/ctrl2ept.ml

@@ -117,6 +117,24 @@ let parse_input ?filename (parse: ?filename:string -> _) =
 
 exception Error of string
 
+let suppress_typedecl ?mo prog =
+  let open Heptagon in
+  let p_desc =
+    List.fold_left
+      (fun acc d -> match d with
+		      Ptype _ -> acc
+		    | _ -> d::acc)
+      []
+      prog.p_desc in
+  let p_opened =
+    match mo with
+      None -> prog.p_opened
+    | Some m -> m :: prog.p_opened in
+  { prog with
+    p_opened;
+    p_desc = List.rev p_desc;
+  }
+
 let parse_n_gen_ept_node ?filename ?node_name ?node_sig ?typ_symbs () =
   let name, func = parse_input ?filename CtrlNbac.Parser.Unsafe.parse_func in
   let node_name = match node_name with Some n -> n
@@ -129,6 +147,7 @@ let handle_ctrlf ?filename mk_oc =
   let _, decls = parse_n_gen_ept_node ?filename () in
   let prog = CtrlNbacAsEpt.create_prog Names.LocalModule in    (* don't care? *)
   let prog = List.fold_right CtrlNbacAsEpt.add_to_prog decls prog in
+  let prog = suppress_typedecl prog in
   let oc, close = mk_oc.out_exec "ept" in
   Hept_printer.print oc prog;
   close ()
@@ -193,7 +212,9 @@ let handle_node arg =
   let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in
   let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
   let prog = try try_ctrls typ_symbs nn prog with
-    | Exit -> try_ctrlf typ_symbs nn prog in
+	     | Exit -> try_ctrlf typ_symbs nn prog in
+  (* Suppress type declarations in controller *)
+  let prog = suppress_typedecl ~mo prog in
   output_prog prog om
 
 (* -------------------------------------------------------------------------- *)

compiler/minils/ctrln/ctrlNbacGen.ml

@@ -611,7 +611,7 @@ let translate_node ~requal_types typdefs = function
     types of expressions to avoid some errors in code generation later on. *)
 let requal_declared_types prog =
 
-  let cmodul = controller_modul prog.p_modname in
+  let cmodul = types_modul prog.p_modname in
   let requal m = m = prog.p_modname in
 
   let requal_constr ({ qual; name } as cstr) =

compiler/obc/java/obc2java.ml

@@ -120,7 +120,10 @@ let translate_constructor_name_2 q q_ty =
   { qual = QualModule classe; name = String.uppercase q.name }
 
 let translate_constructor_name q =
-  match Modules.unalias_type (Types.Tid (Modules.find_constrs q)) with
+  Format.eprintf "lala %a@." Global_printer.print_qualname q;
+  let x = Modules.find_constrs q in
+  Format.eprintf "ok@.";
+  match Modules.unalias_type (Types.Tid x) with
     | Types.Tid q_ty when q_ty = Initial.pbool -> q |> shortname |> local_qn
     | Types.Tid q_ty -> translate_constructor_name_2 q q_ty
     | _ -> assert false

compiler/utilities/ctrln/ctrln_utils.ml

@@ -32,6 +32,8 @@ open Names
 
 let ctrlr_mod_suffix = "_controller"
 
+let types_mod_suffix = "_types"
+
 let dirname_for_modul modul =
   build_path (filename_of_name (modul_to_string modul) ^ "_ctrln")
 
@@ -50,6 +52,12 @@ let controller_modul = function
       QualModule { q with name = n ^ ctrlr_mod_suffix }
   | _ -> failwith "Unexpected module"
 
+let types_modul = function
+  | Module n -> Module (n ^ types_mod_suffix)
+  | QualModule ({ name = n } as q) ->
+      QualModule { q with name = n ^ types_mod_suffix }
+  | _ -> failwith "Unexpected module"
+
 let controller_node ?num { qual; name } = match num with
   | Some num -> { qual = controller_modul qual;
                  name = Printf.sprintf "%s_ctrlr%d" name num }