From 2fc04353932debe0579a1f8ebfa63544c5238f43 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Tue, 22 Nov 2011 11:39:25 +0100 Subject: [PATCH] Added simple printf Typing and clocking done --- compiler/global/initial.ml | 3 ++ compiler/heptagon/analysis/typing.ml | 26 ++++++++++++- compiler/heptagon/parsing/hept_lexer.mll | 8 ++++ compiler/heptagon/parsing/hept_parser.mly | 4 ++ compiler/heptagon/parsing/hept_parsetree.ml | 1 + .../parsing/hept_parsetree_mapfold.ml | 2 +- compiler/heptagon/parsing/hept_scoping.ml | 3 +- compiler/minils/analysis/clocking.ml | 5 +++ compiler/utilities/global/printf_parser.ml | 21 ++++++++++ lib/iostream.epi | 39 ++----------------- test/good/format.ept | 11 ++++++ 11 files changed, 85 insertions(+), 38 deletions(-) create mode 100644 compiler/utilities/global/printf_parser.ml create mode 100644 test/good/format.ept diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml index 501b65b..eec8547 100644 --- a/compiler/global/initial.ml +++ b/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 = diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 2fb362f..8afbe94 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/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) -> diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index de00206..0a87c5f 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/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(); diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 1d9ab96..f30106e 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -17,6 +17,7 @@ open Hept_parsetree %token INT %token FLOAT %token BOOL +%token STRING %token 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 PREFIX %token INFIX0 %token 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 } ; %% diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index dd82838..fd4d0f8 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/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 diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index a06d7cd..d2b7044 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/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 diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 8de8815..e898a6a 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/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 diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 238f009..c82367d 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/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 diff --git a/compiler/utilities/global/printf_parser.ml b/compiler/utilities/global/printf_parser.ml new file mode 100644 index 0000000..5c83151 --- /dev/null +++ b/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 -> [] diff --git a/lib/iostream.epi b/lib/iostream.epi index 8216bf7..3452876 100644 --- a/lib/iostream.epi +++ b/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 () diff --git a/test/good/format.ept b/test/good/format.ept new file mode 100644 index 0000000..c41e6f8 --- /dev/null +++ b/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 \ No newline at end of file