Added simple printf

Typing and clocking done

compiler/global/initial.ml

@@ -26,6 +26,9 @@ let tfloat = Types.Tid pfloat
 let pstring = { qual = Pervasives; name = "string" }
 let tstring = Types.Tid pstring
 
+let pfile = { qual = Module "Iostream"; name = "file" }
+let tfile = Types.Tid pfile
+
 let mk_pervasives s = { qual = Pervasives; name = s }
 
 let mk_static_int_op op args =

compiler/heptagon/analysis/typing.ml

@@ -57,6 +57,7 @@ type error =
   | Esplit_enum of ty
   | Esplit_tuple of ty
   | Eenable_memalloc
+  | Eformat_string_not_constant
 
 exception Unify
 exception TypingError of error
@@ -200,6 +201,10 @@ let message loc kind =
         "%aThis function was compiled with linear types. \
                Enable linear typing to call it.@."
           print_location loc
+    | Eformat_string_not_constant ->
+      eprintf
+        "%aA static format string was expected@."
+          print_location loc
   end;
   raise Errors.Error
 
@@ -548,7 +553,6 @@ and expect_static_exp cenv exp_ty se =
       _ -> message se.se_loc (Etype_clash(ty, exp_ty))
 
 
-
 (** @return the type of the field with name [f] in the list
     [fields]. [t1] is the corresponding record type and [loc] is
     the location, both used for error reporting. *)
@@ -729,6 +733,19 @@ and typing_app cenv h app e_list =
         let typed_e2 = expect cenv h t1 e2 in
         Tid Initial.pbool, app, [typed_e1; typed_e2]
 
+    | Efun { qual = Module "Iostream"; name = "printf" } ->
+        let e1, format_args = assert_1min e_list in
+        let typed_e1 = expect cenv h Initial.tstring e1 in
+        let typed_format_args = typing_format_args cenv h typed_e1 format_args in
+        Tprod [], app, typed_e1::typed_format_args
+
+    | Efun { qual = Module "Iostream"; name = "fprintf" } ->
+        let e1, e2, format_args = assert_2min e_list in
+        let typed_e1 = expect cenv h Initial.tfile e1 in
+        let typed_e2 = expect cenv h Initial.tstring e2 in
+        let typed_format_args = typing_format_args cenv h typed_e1 format_args in
+        Tprod [], app, typed_e1::typed_e2::typed_format_args
+
     | (Efun f | Enode f) ->
         let ty_desc = find_value f in
         let op, expected_ty_list, result_ty_list = kind f ty_desc in
@@ -968,6 +985,13 @@ and typing_node_params cenv params_sig params =
   List.map2 (fun p_sig p -> expect_static_exp cenv
                p_sig.p_type p) params_sig params
 
+and typing_format_args cenv h e args =
+  let s = match e.e_desc with
+    | Econst { se_desc = Sstring s } -> s
+    | _ -> raise (TypingError Eformat_string_not_constant)
+  in
+  let expected_ty_list = Printf_parser.extract_formatters s in
+  typing_args cenv h expected_ty_list args
 
 let rec typing_pat h acc = function
   | Evarpat(x) ->

compiler/heptagon/parsing/hept_lexer.mll

@@ -160,6 +160,7 @@ rule token = parse
   | ".."            {DOUBLE_DOT}
   | "<<"            {DOUBLE_LESS}
   | ">>"            {DOUBLE_GREATER}
+  | "..."           {THREE_DOTS}
   | (['A'-'Z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id)
       {Constructor id}
   | (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id)
@@ -177,6 +178,13 @@ rule token = parse
       { INT (int_of_string(Lexing.lexeme lexbuf)) }
   | ['0'-'9']+ ('.' ['0'-'9']+)? (['e' 'E'] ['+' '-']? ['0'-'9']+)?
       { FLOAT (float_of_string(Lexing.lexeme lexbuf)) }
+  | "\""
+      { reset_string_buffer();
+        (*let string_start = lexbuf.lex_curr_p in
+        string_start_loc := Location.curr lexbuf;*)
+        string lexbuf;
+        (*lexbuf.lex_start_p <- string_start; *)
+        STRING (get_stored_string()) }
   | "(*@ " (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id)
       {
   reset_string_buffer();

compiler/heptagon/parsing/hept_parser.mly

@@ -17,6 +17,7 @@ open Hept_parsetree
 %token <int> INT
 %token <float> FLOAT
 %token <bool> BOOL
+%token <string> STRING
 %token <string * string> PRAGMA
 %token TYPE FUN NODE RETURNS VAR VAL OPEN END CONST UNSAFE
 %token FBY PRE SWITCH EVERY
@@ -50,6 +51,7 @@ open Hept_parsetree
 %token DOUBLE_LESS DOUBLE_GREATER
 %token MAP MAPI FOLD FOLDI MAPFOLD
 %token AT INIT SPLIT REINIT
+%token THREE_DOTS
 %token <string> PREFIX
 %token <string> INFIX0
 %token <string> INFIX1
@@ -607,6 +609,7 @@ _const:
   | INT                { Sint $1 }
   | FLOAT              { Sfloat $1 }
   | BOOL               { Sbool $1 }
+  | STRING             { Sstring $1 }
   | constructor        { Sconstructor $1 }
   | q=qualified(ident) { Svar q }
 ;
@@ -688,6 +691,7 @@ nonmt_params_signature:
 param_signature:
   | IDENT COLON located_ty_ident ck=ck_annot { mk_arg (Some $1) $3 ck }
   | located_ty_ident ck=ck_annot { mk_arg None $1 ck }
+  | THREE_DOTS ck=ck_annot { mk_arg None (Tinvalid, Linearity.Ltop) ck }
 ;
 
 %%

compiler/heptagon/parsing/hept_parsetree.ml

@@ -60,6 +60,7 @@ type ty =
   | Tprod of ty list
   | Tid of qualname
   | Tarray of ty * exp
+  | Tinvalid
 
 and ck =
   | Cbase

compiler/heptagon/parsing/hept_parsetree_mapfold.ml

@@ -264,7 +264,7 @@ and node_dec funs acc nd =
 
 and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t
 and ty funs acc t = match t with
-  | Tid _ -> t, acc
+  | Tid _ | Tinvalid -> t, acc
   | Tprod t_l -> let t_l, acc = mapfold (ty_it funs) acc t_l in Tprod t_l, acc
   | Tarray (t, e) ->
       let t, acc = ty_it funs acc t in

compiler/heptagon/parsing/hept_scoping.ml

@@ -203,7 +203,7 @@ let translate_iterator_type = function
 let rec translate_static_exp se =
   try
     let se_d = translate_static_exp_desc se.se_loc se.se_desc in
-    Types.mk_static_exp Tinvalid ~loc:se.se_loc se_d
+    Types.mk_static_exp Types.Tinvalid ~loc:se.se_loc se_d
   with
     | ScopingError err -> message se.se_loc err
 
@@ -239,6 +239,7 @@ let rec translate_type loc ty =
       | Tarray (ty, e) ->
           let ty = translate_type loc ty in
           Types.Tarray (ty, expect_static_exp e)
+      | Tinvalid -> Types.Tinvalid
     )
   with
     | ScopingError err -> message loc err

compiler/minils/analysis/clocking.ml

@@ -19,6 +19,7 @@
 
 open Misc
 open Idents
+open Names
 open Minils
 open Global_printer
 open Mls_printer
@@ -98,6 +99,10 @@ let typing_app h base pat op w_list = match op with
   | Eselect_slice | Econcat | Earray | Efield_update | Eifthenelse ->
       List.iter (expect_extvalue h base) w_list;
       Ck base
+  | Efun { qual = Module "Iostream"; name = "printf" }
+  | Efun { qual = Module "Iostream"; name = "fprintf" } ->
+    List.iter (expect_extvalue h base) w_list;
+    Cprod []
   | ( Efun f | Enode f) ->
       let node = Modules.find_value f in
       let pat_id_list = Mls_utils.ident_list_of_pat pat in

compiler/utilities/global/printf_parser.ml

@@ -0,0 +1,21 @@
+open Types
+
+exception Bad_format
+
+let tail s start =
+  String.sub s start (String.length s - start)
+
+(** Return a list of expected types from a format string *)
+let rec extract_formatters s =
+  try
+    let i = String.index s '%' in
+    let ty = match s.[i+1] with
+      | 'b' -> Initial.tbool
+      | 'd' -> Initial.tint
+      | 'f' -> Initial.tfloat
+      | _ -> raise Bad_format
+    in
+    ty::(extract_formatters (tail s (i+1)))
+  with
+    | Invalid_argument _ -> raise Bad_format (* String.get failed*)
+    | Not_found -> []

lib/iostream.epi

@@ -1,44 +1,13 @@
 (* The printing module *)
 
-(*
 type file
 
+(*
 const file stdout
 const file stdin
 const file stderr
+*)
 
 (* Basic Printing *)
-
-unsafe val fun open(name :string) returns (file)
-unsafe val fun flush(file) returns ()
-unsafe val fun print_int(file,int) returns ()
-unsafe val fun print_float(file,float) returns ()
-unsafe val fun print_string(file,string) returns ()
-unsafe val fun print_bool(file, bool) returns ()
-unsafe val fun print_nl(file) returns ()
-*)
-unsafe val fun out_flush() returns ()
-unsafe val fun out_int(int) returns ()
-unsafe val fun out_float(float) returns ()
-unsafe val fun out_string(string) returns ()
-unsafe val fun out_bool( bool) returns ()
-unsafe val fun out_nl() returns ()
-
-unsafe val fun err_flush() returns ()
-unsafe val fun err_int(int) returns ()
-unsafe val fun err_float(float) returns ()
-unsafe val fun err_string(string) returns ()
-unsafe val fun err_bool( bool) returns ()
-unsafe val fun err_nl() returns ()
- 
-(* Basic Parsing *)
-(*
-val fun read_int(file) returns (int)
-val fun read_float(file) returns (float)
-val fun read_string(file) returns (string)
-val fun read_bool(file) returns (bool)
-*)
-unsafe val fun in_int() returns (int)
-unsafe val fun in_float() returns (float)
-unsafe val fun in_string() returns (string)
-unsafe val fun in_bool() returns (bool)
+unsafe val fun printf(string;...) returns ()
+unsafe val fun fprintf(file;string;...) returns ()

test/good/format.ept

@@ -0,0 +1,11 @@
+open Iostream
+
+unsafe fun f(a:int) returns (o:int)
+var x:int;
+let
+  x = a + 2;
+  () = printf("Int is %d@.", x);
+  () = printf("Bool is %b@.", x = 0);
+  () = printf("Test");
+  o = x - 1;
+tel