Ada: skeletons for Ada compiler

src/_tags.in

@@ -7,6 +7,7 @@ true: bin_annot, color(always)
 "checks": include
 "parsers": include
 "backends": include
+"backends/Ada": include
 "backends/C": include
 "backends/Horn": include
 "backends/EMF": include

src/backends/Ada/.merlin

+REC
\ No newline at end of file

src/backends/Ada/ada_backend.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
+(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
+(*                                                                  *)
+(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
+(*  under the terms of the GNU Lesser General Public License        *)
+(*  version 2.1.                                                    *)
+(*                                                                  *)
+(********************************************************************)
+
+open Format
+
+let translate_to_ada basename prog machines dependencies =
+  let module Ads = Ada_backend_ads.Main in
+  let module Adb = Ada_backend_adb.Main in
+  let module Wrapper = Ada_backend_wrapper.Main in
+  print_endline "Ada code generated!"
+
+(* Local Variables: *)
+(* compile-command:"make -C ../../.." *)
+(* End: *)

src/backends/Ada/ada_backend_adb.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
+(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
+(*                                                                  *)
+(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
+(*  under the terms of the GNU Lesser General Public License        *)
+(*  version 2.1.                                                    *)
+(*                                                                  *)
+(********************************************************************)
+
+module Main =
+struct
+end

src/backends/Ada/ada_backend_ads.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
+(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
+(*                                                                  *)
+(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
+(*  under the terms of the GNU Lesser General Public License        *)
+(*  version 2.1.                                                    *)
+(*                                                                  *)
+(********************************************************************)
+
+module Main =
+struct
+end

src/backends/Ada/ada_backend_wrapper.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
+(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
+(*                                                                  *)
+(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
+(*  under the terms of the GNU Lesser General Public License        *)
+(*  version 2.1.                                                    *)
+(*                                                                  *)
+(********************************************************************)
+
+module Main =
+struct
+end

src/compiler_stages.ml

@@ -9,7 +9,7 @@ let dynamic_checks () =
   match !Options.output, !Options.spec with
   | "C", "C" -> true
   | _ -> false
-     
+
 
 (* check whether a source file has a compiled header, if not, generate the
    compiled header *)
@@ -68,7 +68,7 @@ let stage1 prog dirname basename =
   let orig, prog =
     if !Options.global_inline && !Options.main_node <> "" then
       (if !Options.witnesses then prog else []),
-      Inliner.global_inline basename prog 
+      Inliner.global_inline basename prog
     else (* if !Option.has_local_inline *)
       [],
       Inliner.local_inline prog (* type_env clock_env *)
@@ -88,7 +88,7 @@ let stage1 prog dirname basename =
 
   (* Registering and checking machine types *)
   if Machine_types.is_active then Machine_types.load prog;
-  
+
 
   (* Generating a .lusi header file only *)
   if !Options.lusi then
@@ -96,12 +96,12 @@ let stage1 prog dirname basename =
        exported as a lusi *)
     raise (StopPhase1 prog);
 
-  (* Optimization of prog: 
-     - Unfold consts 
+  (* Optimization of prog:
+     - Unfold consts
      - eliminate trivial expressions
   *)
   (*
-    let prog = 
+    let prog =
     if !Options.const_unfold || !Options.optimization >= 5 then
     begin
     Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
@@ -139,7 +139,7 @@ let stage1 prog dirname basename =
   Clock_calculus.uneval_prog_generics prog;
 
 
-(* Disabling witness option. Could but reactivated later 
+(* Disabling witness option. Could but reactivated later
   if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
     begin
       let orig = Corelang.copy_prog orig in
@@ -154,7 +154,7 @@ let stage1 prog dirname basename =
 	!Options.main_node
 	orig prog type_env clock_env
     end;
-*)  
+*)
 
   (* Computes and stores generic calls for each node,
      only useful for ANSI C90 compliant generic node compilation *)
@@ -201,19 +201,19 @@ let stage1 prog dirname basename =
       Access.check_prog prog;
     end;
 
-  
+
   let prog = SortProg.sort_nodes_locals prog in
-  
+
   prog, dependencies
 
 
     (* from source to machine code, with optimization *)
-let stage2 prog =    
+let stage2 prog =
   (* Computation of node equation scheduling. It also breaks dependency cycles
      and warns about unused input or memory variables *)
   Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
   let prog, node_schs =
-    try 
+    try
       Scheduling.schedule_prog prog
     with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
 				 systemtic way in AlgebraicLoop module *)
@@ -226,7 +226,7 @@ let stage2 prog =
   Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
   Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
 
-  (* TODO Salsa optimize prog: 
+  (* TODO Salsa optimize prog:
      - emits warning for programs with pre inside expressions
      - make sure each node arguments and memory is bounded by a local annotation
      - introduce fresh local variables for each real pure subexpression
@@ -238,14 +238,14 @@ let stage2 prog =
   Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
 
   (* Optimize machine code *)
-  Optimize_machine.optimize prog node_schs machine_code   
+  Optimize_machine.optimize prog node_schs machine_code
 
 
 (* printing code *)
 let stage3 prog machine_code dependencies basename =
   let basename    =  Filename.basename basename in
   match !Options.output with
-    "C" -> 
+    "C" ->
       begin
 	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
 	C_backend.translate_to_c
@@ -262,6 +262,12 @@ let stage3 prog machine_code dependencies basename =
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
        Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
      end
+  | "Ada" ->
+    begin
+      Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@,");
+      Ada_backend.translate_to_ada
+	basename prog machine_code dependencies
+    end
   | "horn" ->
      begin
        let destname = !Options.dest_dir ^ "/" ^ basename in

src/options_management.ml

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 open Options
-  
+
 let print_version () =
   Format.printf "Lustrec compiler, version %s (%s)@." version codename;
   Format.printf "Standard lib: %s@." Version.include_path;
@@ -21,13 +21,13 @@ let add_include_dir dir =
   let removed_slash_suffix =
     let len = String.length dir in
     if dir.[len-1] = '/' then
-      String.sub dir 0 (len - 1) 
+      String.sub dir 0 (len - 1)
     else
       dir
   in
   include_dirs := removed_slash_suffix :: !include_dirs
 
-    
+
 (** Solving the path of required library:
     If local: look in the folders described in !Options.include_dirs
     If non local: look first as a local, then in Version.include_path:
@@ -41,7 +41,7 @@ let search_lib_path (local, full_file_name) =
     List.fold_right (fun dir res ->
       match res with Some _ -> res
       | None ->
-	 let path_to_lib = dir ^ "/" ^ full_file_name in 
+	 let path_to_lib = dir ^ "/" ^ full_file_name in
 	 if Sys.file_exists path_to_lib then
 	   Some dir
 	 else
@@ -57,11 +57,11 @@ let search_lib_path (local, full_file_name) =
 (* Search for path of core libs (without lusic: arrow and io_frontend *)
 let core_dependency lib_name =
   search_lib_path (false, lib_name ^ ".h")
-    
+
 let name_dependency (local, dep) =
   let dir = search_lib_path (false, dep ^ ".lusic") in
   dir ^ "/" ^ dep
-  
+
 let set_mpfr prec =
   if prec > 0 then (
     mpfr := true;
@@ -79,7 +79,7 @@ let set_real_type s =
       real_type := "mpfr";
     )
   | _ -> real_type := s
-     
+
 let set_backend s =
   output := s;
   Backends.setup ()
@@ -90,15 +90,15 @@ let common_options =
     "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
     "-print-types", Arg.Set print_types, "prints node types";
     "-print-clocks", Arg.Set print_clocks, "prints node clocks";
-    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; 
-    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>"; 
+    "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
+    "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops  <default: 15>";
     "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
     "-version", Arg.Unit print_version, " displays the version";
   ]
 
 let lustrec_options =
   common_options @
-    [ 
+    [
       "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
       "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
       "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
@@ -108,6 +108,7 @@ let lustrec_options =
       "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
       "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
       (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
+      "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
       "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
       "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
       "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
@@ -119,7 +120,7 @@ let lustrec_options =
       "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
       "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
       "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
-      
+
       "-c++" , Arg.Set        cpp      , "c++ backend";
       "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
       "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
@@ -140,7 +141,7 @@ let lustret_options =
 let plugin_opt (name, activate, options) =
   ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
     (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
- 
+
 
 let get_witness_dir filename =
   (* Make sure the directory exists *)