[ast2C] constants, simple assignations, variables (+ one fix about pre storage)

src/ast_to_c.ml

@@ -3,44 +3,45 @@ open Intermediate_ast
 open Intermediate_utils
 open Cprint
 open Utils
+open Ctranslation
 
 
 
-(** [ast_to_cast] translates a [t_nodelist] into a [i_nodelist] *)
+(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *)
-let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist =
+let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist =
   let c = ref 1 in
-  let ast_to_cast_varlist vl = snd vl in
+  let ast_to_intermediate_ast_varlist vl = snd vl in
-  let rec ast_to_cast_expr hloc = function
+  let rec ast_to_intermediate_ast_expr hloc = function
     | EVar   (_, v) ->
         begin
         match Hashtbl.find_opt hloc (v, false) with
-        | None -> IVar (CVInput (name_of_var v))
+        | None -> IEVar (CVInput (name_of_var v))
-        | Some (s, i) -> IVar (CVStored (s, i))
+        | Some (s, i) -> IEVar (CVStored (s, i))
         end
-    | EMonOp (_, op, e) -> IMonOp (op, ast_to_cast_expr hloc e)
+    | EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e)
     | EBinOp (_, op, e, e') ->
-       IBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e')
+       IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
     | ETriOp (_, op, e, e', e'') ->
-        ITriOp
+        IETriOp
-          (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e', ast_to_cast_expr hloc e'')
+          (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e', ast_to_intermediate_ast_expr hloc e'')
     | EComp  (_, op, e, e') ->
-        IComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e')
+        IEComp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
     | EWhen  (_, e, e') ->
-        IWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e')
+        IEWhen (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
     | EReset  (_, e, e') ->
-        IReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e')
+        IEReset (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
-    | EConst (_, c) -> IConst c
+    | EConst (_, c) -> IEConst c
-    | ETuple (_, l) -> ITuple (List.map (ast_to_cast_expr hloc) l)
+    | ETuple (_, l) -> IETuple (List.map (ast_to_intermediate_ast_expr hloc) l)
     | EApp   (_, n, e) ->
       begin
-        let e = ast_to_cast_expr hloc e in
+        let e = ast_to_intermediate_ast_expr hloc e in
-        let res = IApp (!c, n, e) in
+        let res = IEApp (!c, n, e) in
         let () = incr c in
         res
       end
   in
-  let ast_to_cast_eq hloc (patt, expr) : i_equation =
+  let ast_to_intermediate_ast_eq hloc (patt, expr) : i_equation =
-    (ast_to_cast_varlist patt, ast_to_cast_expr hloc expr) in
+    (ast_to_intermediate_ast_varlist patt, ast_to_intermediate_ast_expr hloc expr) in
   List.map
     begin
     fun node ->
@@ -48,10 +49,10 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist =
       let hloc = (Hashtbl.find h node.n_name).nt_map in
       {
         in_name = node.n_name;
-        in_inputs = ast_to_cast_varlist node.n_inputs;
+        in_inputs = ast_to_intermediate_ast_varlist node.n_inputs;
-        in_outputs = ast_to_cast_varlist node.n_outputs;
+        in_outputs = ast_to_intermediate_ast_varlist node.n_outputs;
-        in_local_vars = ast_to_cast_varlist node.n_local_vars;
+        in_local_vars = ast_to_intermediate_ast_varlist node.n_local_vars;
-        in_equations = List.map (ast_to_cast_eq hloc) node.n_equations;
+        in_equations = List.map (ast_to_intermediate_ast_eq hloc) node.n_equations;
       }
     end
     nodes
@@ -71,8 +72,11 @@ let make_state_types nodes: node_states =
     let vars =
       List.filter (fun v -> type_var v = [ty])
         (snd (varlist_concat node.n_outputs node.n_local_vars)) in
+    let all_vars =
+      List.filter (fun v -> type_var v = [ty])
+        (snd (varlist_concat (varlist_concat node.n_inputs node.n_outputs) node.n_local_vars)) in
     let pre_vars =
-      List.filter (fun v -> List.mem v pv) vars in
+      List.filter (fun v -> List.mem v pv) all_vars in
     let nb = (List.length vars) + (List.length pre_vars) in
     let tyh = Hashtbl.create nb in
     let i =
@@ -205,10 +209,16 @@ let cp_prevars fmt (node, h) =
         "\n\t/* Remember the values used in the [pre] construct */\n";
       List.iter
         (fun v -> (** Note that «dst_array = src_array» should hold. *)
-          let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in
+          match Hashtbl.find_opt node_st.nt_map (v, false) with
+          | Some (src_array, src_idx) ->
             let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
             Format.fprintf fmt "\t%s[%d] = %s[%d];\n"
-            dst_array dst_idx src_array src_idx)
+              dst_array dst_idx src_array src_idx
+          | None -> 
+            let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
+            Format.fprintf fmt "\t%s[%d] = %s;\n"
+              dst_array dst_idx (Utils.name_of_var v)
+          )
         l
 
 
@@ -241,20 +251,13 @@ let cp_init_aux_nodes fmt (node, h) =
 
 
 
-(** The following function prints one equation of the program into a set of
-  * instruction ending in assignments. *)
-let cp_equation fmt (eq, hloc) =
-  Format.fprintf fmt "\t\t/* TODO! */\n"
-
-
-
 (** [cp_equations] prints the node equations. *)
 let rec cp_equations fmt (eqs, hloc) =
   match eqs with
   | [] -> ()
   | eq :: eqs ->
     Format.fprintf fmt "%a%a"
-      cp_equation (eq, hloc)
+      cp_expression (equation_to_expression (hloc.nt_map, eq), hloc)
       cp_equations (eqs, hloc)
 
 (** [cp_node] prints a single node *)
@@ -276,10 +279,40 @@ let rec cp_nodes fmt (nodes, h) =
 
 
 
+let dump_var_locations (st: node_states) =
+  Hashtbl.iter
+    (fun n st ->
+      Format.printf "\n\n\tNODE: %s\n" n;
+    Hashtbl.iter
+    (fun ((v: t_var), (ispre: bool)) ((arr: string), (idx: int)) ->
+      match v, ispre with
+      | IVar s, true -> Format.printf "PRE Variable (int) %s stored as %s[%d]\n"
+                          s arr idx
+      | BVar s, true -> Format.printf "PRE Variable (bool) %s stored as %s[%d]\n"
+                          s arr idx
+      | RVar s, true -> Format.printf "PRE Variable (real) %s stored as %s[%d]\n"
+                          s arr idx
+      | IVar s, false -> Format.printf "Variable (int) %s stored as %s[%d]\n"
+                          s arr idx
+      | BVar s, false -> Format.printf "Variable (bool) %s stored as %s[%d]\n"
+                          s arr idx
+      | RVar s, false -> Format.printf "Variable (real) %s stored as %s[%d]\n"
+                          s arr idx)
+    st.nt_map)
+    st;
+    Format.printf "\n\n"
+
+
+
 (** main function that prints a C-code from a term of type [t_nodelist]. *)
-let ast_to_c prog =
+let ast_to_c (debug: bool) prog =
   let prog_st_types = make_state_types prog in
-  let prog: i_nodelist = ast_to_cast prog prog_st_types in
+  let () =
+    if debug
+      then dump_var_locations prog_st_types
+      else ()
+    in
+  let prog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
   Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a"
     cp_includes (Config.c_includes)
     cp_state_types prog_st_types

src/cast.ml

@@ -0,0 +1,26 @@
+open Intermediate_ast
+open Ast
+
+(** This file contains a small subset of the syntax of C required for the
+  * translation. *)
+
+(** A [c_block] represents a block in C. *)
+type c_block = c_expression list
+
+(** A [c_expresion] represents a C expression, which can need sequences and
+  * function calls. *)
+and c_expression =
+  | CAssign of c_var * c_value
+  | CSeq of c_expression * c_expression
+  | CIf of c_value * c_block * c_block
+  | CApplication of c_var list * c_expression
+
+(** A value here is anything that can be inlined into a single C expression
+  * containing no function call, condition, ... *)
+and c_value =
+  | CVariable of c_var
+  | CMonOp of monop * c_value
+  | CBinOp of binop * c_value * c_value
+  | CComp of compop * c_value * c_value
+  | CConst of const
+

src/cprint.ml

@@ -1,6 +1,7 @@
 open Intermediate_utils
 open Intermediate_ast
 open Ast
+open Cast
 
 (** This file contains extrimely simple functions printing C code. *)
 
@@ -76,3 +77,37 @@ let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) =
         cp_prototype (node, h)
         cp_prototypes (nodes, h)
 
+
+
+let cp_value fmt value =
+  match value with
+  | CVariable (CVInput s) -> Format.fprintf fmt "%s" s
+  | CVariable (CVStored (arr, idx)) ->
+      Format.fprintf fmt "%s[%d]" arr idx
+  | CConst (CInt i) -> Format.fprintf fmt "%d" i
+  | CConst (CBool true) -> Format.fprintf fmt "true"
+  | CConst (CBool false) -> Format.fprintf fmt "false"
+  | CConst (CReal r) -> Format.fprintf fmt "%f" r
+  (**| CMonOp of monop * c_value
+  | CBinOp of binop * c_value * c_value
+  | CComp of compop * c_value * c_value*)
+  | _ -> failwith "[cprint.ml] TODO!"
+
+
+
+
+(** The following function prints one transformed equation of the program into a
+  * set of instruction ending in assignments. *)
+let cp_expression fmt (expr, hloc) =
+  let prefix = "\t" in
+  match expr with
+  | CAssign (CVStored (arr, idx), value) ->
+    begin
+      Format.fprintf fmt "%s%s[%d] = %a;\n"
+        prefix arr idx cp_value value
+    end
+  | CAssign (CVInput _, _) -> failwith "should not happend."
+  (*| CSeq of c_expression * c_expression
+  | CIf of c_value * c_block * c_block
+  | CApplication of c_var list * c_expression*)
+  | _ -> failwith "[cprint.ml] TODO!"

src/ctranslation.ml

@@ -0,0 +1,40 @@
+open Ast
+open Intermediate_ast
+open Cast
+
+let iexpression_to_cvalue e = ()
+
+let equation_to_expression (hloc, ((vl, expr): i_equation)) : c_expression =
+  let fetch_unique_var () =
+    match vl with
+    | [v] ->
+      begin
+        match Hashtbl.find_opt hloc (v, false) with
+        | None -> CVInput (Utils.name_of_var v)
+        | Some (arr, idx) -> CVStored (arr, idx)
+      end
+    | _ -> failwith "[ctranslation.ml] This should not happened."
+  in
+  match expr with
+  | IEVar   vsrc ->
+      CAssign (fetch_unique_var (), CVariable vsrc)
+  | IEMonOp (MOp_pre, IEVar v) ->
+      CAssign (fetch_unique_var (), CVariable v)
+  | IEConst c ->
+      CAssign (fetch_unique_var (), CConst c)
+  (*| IEMonOp (op, e) ->
+      CMonOp (op, iexpression_to_cvalue e)
+  | IEBinOp (op, e, e') ->
+      CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')
+  | IEComp  (op, e, e') ->
+      CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')
+  | IEConst c -> CConst c
+  TODO!
+  | IETriOp of triop * i_expression * i_expression * i_expression
+  | IEWhen  of i_expression * i_expression
+  | IEReset of i_expression * i_expression
+  | IETuple of (i_expression list)
+      (** [CApp] below represents the n-th call to an aux node *)
+  | IEApp   of int * t_node * i_expression*)
+  | _ -> failwith "[ctranslation.ml] TODO!"
+

src/intermediate_ast.ml

@@ -45,17 +45,17 @@ type c_var =
   | CVInput of ident
 
 type i_expression =
-  | IVar   of c_var
+  | IEVar   of c_var
-  | IMonOp of monop * i_expression
+  | IEMonOp of monop * i_expression
-  | IBinOp of binop * i_expression * i_expression
+  | IEBinOp of binop * i_expression * i_expression
-  | ITriOp of triop * i_expression * i_expression * i_expression
+  | IETriOp of triop * i_expression * i_expression * i_expression
-  | IComp  of compop * i_expression * i_expression
+  | IEComp  of compop * i_expression * i_expression
-  | IWhen  of i_expression * i_expression
+  | IEWhen  of i_expression * i_expression
-  | IReset of i_expression * i_expression
+  | IEReset of i_expression * i_expression
-  | IConst of const
+  | IEConst of const
-  | ITuple of (i_expression list)
+  | IETuple of (i_expression list)
       (** [CApp] below represents the n-th call to an aux node *)
-  | IApp   of int * t_node * i_expression
+  | IEApp   of int * t_node * i_expression
 
 and i_varlist = t_var list
 

src/intermediate_utils.ml

@@ -2,15 +2,15 @@ open Intermediate_ast
 
 let rec find_app_opt eqs i =
   let rec find_app_expr_opt i = function
-    | IVar _ | IConst _ -> None
+    | IEVar _ | IEConst _ -> None
-    | IMonOp (_, e) -> find_app_expr_opt i e
+    | IEMonOp (_, e) -> find_app_expr_opt i e
-    | IReset (e, e') | IWhen (e, e') | IComp (_, e, e') | IBinOp (_, e, e') ->
+    | IEReset (e, e') | IEWhen (e, e') | IEComp (_, e, e') | IEBinOp (_, e, e') ->
         begin
         match find_app_expr_opt i e with
         | None -> find_app_expr_opt i e'
         | Some n -> Some n
         end
-    | ITriOp (_, e, e', e'') ->
+    | IETriOp (_, e, e', e'') ->
         begin
         match find_app_expr_opt i e with
         | None ->
@@ -21,15 +21,15 @@ let rec find_app_opt eqs i =
           end
         | Some n -> Some n
         end
-    | ITuple l ->
+    | IETuple l ->
         List.fold_left
           (fun acc e ->
             match acc, find_app_expr_opt i e with
             | Some n, _ -> Some n
             | None, v -> v)
           None l
-        (** [IApp] below represents the n-th call to an aux node *)
+        (** [IEApp] below represents the n-th call to an aux node *)
-    | IApp (j, n, e) ->
+    | IEApp (j, n, e) ->
         if i = j
           then Some n
           else find_app_expr_opt i e

src/main.ml

@@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f =
 
 let _ =
   (** Usage and argument parsing. *)
-  let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"; "clock_unification"] in
+  let default_passes = [] in
   let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
   let usage_msg =
     "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
@@ -127,6 +127,6 @@ let _ =
     else (
       if !nopopt
         then (fun _ -> ())
-        else Ast_to_c.ast_to_c)
+        else Ast_to_c.ast_to_c !debug)
   end