diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 61702f7..dd372a5 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -94,7 +94,8 @@ let rec skeleton ck = function Format.eprintf "Internal error, an exp with invalid type@."; assert false; | _ -> Cprod (List.map (skeleton ck) ty_list)) - | Tarray _ | Tid _ | Tunit -> Ck ck + | Tarray (t, _) | Tasync (_, t) -> skeleton ck t + | Tid _ | Tunit -> Ck ck (* TODO here it implicitely says that the base clock is Cbase and that all tuple is on Cbase *) diff --git a/compiler/global/global_compare.ml b/compiler/global/global_compare.ml index 00c75df..d216388 100644 --- a/compiler/global/global_compare.ml +++ b/compiler/global/global_compare.ml @@ -35,6 +35,9 @@ and link_compare li1 li2 = match li1, li2 with | Cindex _, _ -> 1 | Clink _, _ -> -1 + +let async_t_compare a1 a2 = Pervasives.compare a1 a2 + let rec static_exp_compare se1 se2 = let cr = type_compare se1.se_ty se2.se_ty in @@ -100,7 +103,20 @@ and type_compare ty1 ty2 = match ty1, ty2 with | Tarray (ty1, se1), Tarray (ty2, se2) -> let cr = type_compare ty1 ty2 in if cr <> 0 then cr else static_exp_compare se1 se2 - | (Tprod _ | Tid _), _ -> 1 - | (Tarray _), _ -> -1 + | Tasync (a1, t1), Tasync (a2, t2) -> + let cr = type_compare t1 t2 in + if cr <> 0 then cr else async_t_compare a1 a2 | Tunit, Tunit -> 0 + + | Tprod _, _ -> 1 + + | Tid _, Tprod _ -> -1 + | Tid _, _ -> 1 + + | Tarray _, (Tprod _ | Tid _) -> -1 + | Tarray _, _ -> 1 + + | Tasync _, Tunit -> 1 + | Tasync _, _ -> -1 + | Tunit, _ -> -1 diff --git a/compiler/global/global_mapfold.ml b/compiler/global/global_mapfold.ml index 1af3f94..c3e9cff 100644 --- a/compiler/global/global_mapfold.ml +++ b/compiler/global/global_mapfold.ml @@ -60,6 +60,7 @@ and ty funs acc t = match t with let se, acc = static_exp_it funs acc se in Tarray (t, se), acc | Tunit -> t, acc + | Tasync (a, t) -> let t, acc = ty_it funs acc t in Tasync (a, t), acc (* and ct_it funs acc c = try funs.ct funs acc c with Fallback -> ct funs acc t and ct funs acc c = match c with diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 814895c..118b800 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -13,6 +13,9 @@ let print_qualname ff qn = match qn with | { qual = m; name = n } when m = local_qualname -> print_name ff n | { qual = m; name = n } -> fprintf ff "%s.%a" m print_name n +let print_async ff async = match async with + | None -> () + | Some () -> fprintf ff "async " let rec print_static_exp ff se = match se.se_desc with | Sint i -> fprintf ff "%d" i @@ -49,6 +52,7 @@ and print_type ff = function | Tarray (ty, n) -> fprintf ff "@[%a^%a@]" print_type ty print_static_exp n | Tunit -> fprintf ff "()" + | Tasync (a, t) -> fprintf ff "%a%a" print_async (Some a) print_type t let print_field ff field = fprintf ff "@[%a: %a@]" print_qualname field.f_name print_type field.f_type diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index c132353..1b2b8aa 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -287,6 +287,7 @@ let rec unalias_type t = match t with | Tarray (ty, n) -> Tarray(unalias_type ty, n) | Tprod ty_list -> Tprod (List.map unalias_type ty_list) | Tunit -> Tunit + | Tasync (a, t) -> Tasync (a, unalias_type t) (** Return the current module as a [module_object] *) diff --git a/compiler/global/types.ml b/compiler/global/types.ml index c2832b0..dc5e453 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -11,6 +11,8 @@ open Names open Misc open Location +type async_t = unit + type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location } and static_exp_desc = @@ -30,6 +32,7 @@ and ty = | Tprod of ty list | Tid of type_name | Tarray of ty * static_exp + | Tasync of async_t * ty | Tunit let invalid_type = Tprod [] @@ -39,6 +42,10 @@ let prod = function | [ty] -> ty | ty_list -> Tprod ty_list +let asyncify async ty_list = match async with + | None -> ty_list + | Some a -> List.map (fun ty -> Tasync (a,ty)) ty_list + (** DO NOT use this after the typing, since it could give invalid_type *) let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc = diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 289b470..48799ee 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -150,6 +150,7 @@ and apply op e_list = let t1 = typing e1 in let t2 = ctuplelist (List.map typing e_list) in cseq t2 t1 + | Ebang -> let e = assert_1 e_list in typing e let rec typing_pat = function | Evarpat(x) -> cwrite(x) diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 9115bea..9edef47 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -51,8 +51,11 @@ type error = | Emerge_missing_constrs of QualSet.t | Emerge_uniq of qualname | Emerge_mix of qualname + | Epat_should_be_async of ty + | Eshould_be_async of ty exception Unify +exception Should_be_async of ty exception TypingError of error let error kind = raise (TypingError(kind)) @@ -161,6 +164,16 @@ let message loc kind = as the last but one argument (found: %a).@." print_location loc print_type ty + | Epat_should_be_async ty -> + eprintf "%aThis pattern is expected to be of async vars \ + but the type found is %a.@." + print_location loc + print_type ty + | Eshould_be_async ty -> + eprintf "%aThis expression is expected to be async \ + but the type found is %a.@." + print_location loc + print_type ty end; raise Errors.Error @@ -385,6 +398,7 @@ let rec check_type const_env = function | Tprod l -> Tprod (List.map (check_type const_env) l) | Tunit -> Tunit + | Tasync (a, t) -> Tasync (a, check_type const_env t) and typing_static_exp const_env se = try @@ -628,18 +642,15 @@ and typing_app const_env h app e_list = | (Efun f | Enode f) -> let ty_desc = find_value f in let op, expected_ty_list, result_ty_list = kind f ty_desc in - let node_params = - List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in + let node_params = List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in let m = build_subst node_params app.a_params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in - let typed_e_list = typing_args const_env h - expected_ty_list e_list in + let typed_e_list = typing_args const_env h expected_ty_list e_list in let result_ty_list = List.map (subst_type_vars m) result_ty_list in + let result_ty_list = asyncify app.a_async result_ty_list in (* Type static parameters and generate constraints *) - let typed_params = typing_node_params const_env - ty_desc.node_params app.a_params in - let size_constrs = - instanciate_constr m ty_desc.node_params_constraints in + let typed_params = typing_node_params const_env ty_desc.node_params app.a_params in + let size_constrs = instanciate_constr m ty_desc.node_params_constraints in List.iter add_size_constraint size_constrs; prod result_ty_list, { app with a_op = op; a_params = typed_params }, @@ -740,6 +751,13 @@ and typing_app const_env h app e_list = let n = mk_static_int_op (mk_pervasives "+") [array_size t1; array_size t2] in Tarray (element_type t1, n), app, [typed_e1; typed_e2] + | Ebang -> + let e = assert_1 e_list in + let typed_e, t = typing const_env h e in + (match t with + | Tasync (_, t) -> t, app, [typed_e] + | _ -> message e.e_loc (Eshould_be_async t)) + and typing_iterator const_env h it n args_ty_list result_ty_list e_list = match it with @@ -831,6 +849,7 @@ and typing_node_params const_env params_sig params = List.map2 (fun p_sig p -> expect_static_exp const_env p_sig.p_type p) params_sig params + let rec typing_pat h acc = function | Evarpat(x) -> let ty = typ_of_name h x in @@ -947,7 +966,7 @@ and typing_present_handlers const_env h acc def_names (typed_present_handlers, (add total (add partial acc))) -and typing_block const_env h +and typing_block const_env h (* TODO async deal with it ! *) ({ b_local = l; b_equs = eq_list; b_loc = loc } as b) = try let typed_l, (local_names, h0) = build const_env h l in diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 1af1988..f845937 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -128,54 +128,59 @@ and print_tag_e_list ff tag_e_list = and print_every ff reset = print_opt (fun ff id -> fprintf ff " every %a" print_exp id) ff reset -and print_app ff (app, args) = match app.a_op with - | Eequal -> - let e1, e2 = assert_2 args in - fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2 - | Etuple -> print_exp_tuple ff args - | Efun f | Enode f -> - fprintf ff "@[%a@,%a@,%a@]" - print_qualname f print_params app.a_params print_exp_tuple args - | Eifthenelse -> - let e1, e2, e3 = assert_3 args in - fprintf ff "@[if %a@ then %a@ else %a@]" - print_exp e1 print_exp e2 print_exp e3 - | Efield -> - let r = assert_1 args in - let f = assert_1 app.a_params in - fprintf ff "%a.%a" print_exp r print_static_exp f - | Efield_update -> - let r,e = assert_2 args in - let f = assert_1 app.a_params in - fprintf ff "@[<2>{%a with .%a =@ %a}@]" - print_exp r print_static_exp f print_exp e - | Earray -> fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") args - | Earray_fill -> - let e = assert_1 args in - let n = assert_1 app.a_params in - fprintf ff "%a^%a" print_exp e print_static_exp n - | Eselect -> - let e = assert_1 args in - fprintf ff "%a%a" print_exp e print_index app.a_params - | Eselect_slice -> - let e = assert_1 args in - let idx1, idx2 = assert_2 app.a_params in - fprintf ff "%a[%a..%a]" - print_exp e print_static_exp idx1 print_static_exp idx2 - | Eselect_dyn -> - let r, d, e = assert_2min args in - fprintf ff "%a%a default %a" - print_exp r print_dyn_index e print_exp d - | Eupdate -> - let e1, e2, idx = assert_2min args in - fprintf ff "@[<2>(%a with %a =@ %a)@]" - print_exp e1 print_dyn_index idx print_exp e2 - | Econcat -> - let e1, e2 = assert_2 args in - fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 - | Earrow -> - let e1, e2 = assert_2 args in - fprintf ff "@[<2>%a ->@ %a@]" print_exp e1 print_exp e2 +and print_app ff (app, args) = + print_async ff app.a_async; + match app.a_op with + | Eequal -> + let e1, e2 = assert_2 args in + fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2 + | Etuple -> print_exp_tuple ff args + | Efun f | Enode f -> + fprintf ff "@[%a@,%a@,%a@]" + print_qualname f print_params app.a_params print_exp_tuple args + | Eifthenelse -> + let e1, e2, e3 = assert_3 args in + fprintf ff "@[if %a@ then %a@ else %a@]" + print_exp e1 print_exp e2 print_exp e3 + | Efield -> + let r = assert_1 args in + let f = assert_1 app.a_params in + fprintf ff "%a.%a" print_exp r print_static_exp f + | Efield_update -> + let r,e = assert_2 args in + let f = assert_1 app.a_params in + fprintf ff "@[<2>{%a with .%a =@ %a}@]" + print_exp r print_static_exp f print_exp e + | Earray -> fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") args + | Earray_fill -> + let e = assert_1 args in + let n = assert_1 app.a_params in + fprintf ff "%a^%a" print_exp e print_static_exp n + | Eselect -> + let e = assert_1 args in + fprintf ff "%a%a" print_exp e print_index app.a_params + | Eselect_slice -> + let e = assert_1 args in + let idx1, idx2 = assert_2 app.a_params in + fprintf ff "%a[%a..%a]" + print_exp e print_static_exp idx1 print_static_exp idx2 + | Eselect_dyn -> + let r, d, e = assert_2min args in + fprintf ff "%a%a default %a" + print_exp r print_dyn_index e print_exp d + | Eupdate -> + let e1, e2, idx = assert_2min args in + fprintf ff "@[<2>(%a with %a =@ %a)@]" + print_exp e1 print_dyn_index idx print_exp e2 + | Econcat -> + let e1, e2 = assert_2 args in + fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 + | Earrow -> + let e1, e2 = assert_2 args in + fprintf ff "@[<2>%a ->@ %a@]" print_exp e1 print_exp e2 + | Ebang -> + let e = assert_1 args in + fprintf ff "!(%a)" print_exp e let rec print_eq ff eq = match eq.eq_desc with diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 8930d05..dec2663 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -49,6 +49,7 @@ and desc = and app = { a_op : op; a_params : static_exp list; + a_async : async_t option; a_unsafe : bool } and op = @@ -67,6 +68,7 @@ and op = | Eselect_slice | Eupdate | Econcat + | Ebang and pat = | Etuplepat of pat list @@ -75,7 +77,7 @@ and pat = type eq = { eq_desc : eqdesc; eq_statefull : bool; - eq_loc : location } + eq_loc : location; } and eqdesc = | Eautomaton of state_handler list @@ -90,7 +92,8 @@ and block = { b_equs : eq list; b_defnames : ty Env.t; b_statefull : bool; - b_loc : location } + b_loc : location; + b_async : async_t option; } and state_handler = { s_state : state_name; @@ -186,11 +189,11 @@ let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_base_ck = Cbase; e_loc = loc; } -let mk_op ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(unsafe=false) ?(async=None) op = + { a_op = op; a_params = params; a_async = async; a_unsafe = unsafe } let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = - Eapp(mk_op ~params:params ~unsafe:unsafe op, args, reset) + Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset) let mk_type_dec name desc = { t_name = name; t_desc = desc; t_loc = no_location; } @@ -202,9 +205,9 @@ let mk_var_dec ?(last = Var) ?(ck = fresh_clock()) name ty = { v_ident = name; v_type = ty; v_clock = ck; v_last = last; v_loc = no_location } -let mk_block ?(statefull = true) ?(defnames = Env.empty) ?(locals = []) eqs = +let mk_block ?(statefull = true) ?(defnames = Env.empty) ?(async = None) ?(locals = []) eqs = { b_local = locals; b_equs = eqs; b_defnames = defnames; - b_statefull = statefull; b_loc = no_location } + b_statefull = statefull; b_loc = no_location; b_async = async; } let dfalse = mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 9f035a9..18da7d3 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -14,6 +14,7 @@ let comment_depth = ref 0 let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);; List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ + "async", ASYNC; "node", NODE; "fun", FUN; "returns", RETURNS; @@ -145,6 +146,7 @@ rule token = parse | ".." {DOUBLE_DOT} | "<<" {DOUBLE_LESS} | ">>" {DOUBLE_GREATER} + | "!" {BANG} | (['A'-'Z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) {Constructor id} | (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index a849c22..3462aaa 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -47,6 +47,7 @@ open Hept_parsetree %token AROBASE %token DOUBLE_LESS DOUBLE_GREATER %token MAP FOLD FOLDI MAPFOLD +%token ASYNC BANG %token PREFIX %token INFIX0 %token INFIX1 @@ -77,6 +78,7 @@ open Hept_parsetree %left POWER %right PREFIX %left DOT +%left BANG %start program @@ -286,6 +288,8 @@ ty_ident: { Tid $1 } | ty_ident POWER simple_exp { Tarray ($1, $3) } + | ASYNC t=ty_ident + { Tasync ((), t) } ; equs: @@ -309,7 +313,8 @@ sblock(S) : | VAR l=loc_params S eq=equs { mk_block l eq (Loc($startpos,$endpos)) } | eq=equs { mk_block [] eq (Loc($startpos,$endpos)) } -equ: eq=_equ { mk_equation eq (Loc($startpos,$endpos)) } +equ: + | eq=_equ { mk_equation eq (Loc($startpos,$endpos)) } _equ: | pat EQUAL exp { Eeq($1, $3) } | AUTOMATON automaton_handlers END @@ -430,8 +435,6 @@ _simple_exp: Efield [$1] } ; -node_name: - | qualname call_params { mk_app (Enode $1) $2 } merge_handlers: | hs=nonempty_list(merge_handler) { hs } @@ -446,8 +449,13 @@ _exp: { Efby ($1, $3) } | PRE exp { Epre (None, $2) } - | node_name LPAREN exps RPAREN - { Eapp($1, $3) } + /* node call*/ + | n=qualname p=call_params LPAREN args=exps RPAREN + { Eapp(mk_app (Enode n) p , args) } + | ASYNC n=qualname p=call_params LPAREN args=exps RPAREN + { Eapp(mk_app (Enode n) ~async:(Some ()) p, args) } + | BANG e=exp + { mk_call Ebang [e] } | NOT exp { mk_op_call "not" [$2] } | exp INFIX4 exp diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 106a044..444d1d1 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -31,6 +31,8 @@ type field_name = qualname type constructor_name = qualname type constant_name = qualname +type async_t = unit + type static_exp = { se_desc: static_exp_desc; se_loc: location } and static_exp_desc = @@ -56,6 +58,7 @@ type ty = | Tprod of ty list | Tid of qualname | Tarray of ty * exp + | Tasync of async_t * ty and exp = { e_desc : edesc; @@ -74,7 +77,7 @@ and edesc = | Ewhen of exp * constructor_name * var_name | Emerge of var_name * (constructor_name * exp) list -and app = { a_op: op; a_params: exp list; } +and app = { a_op: op; a_params: exp list; a_async : async_t option } and op = | Eequal @@ -92,6 +95,7 @@ and op = | Eselect_slice | Eupdate | Econcat + | Ebang and pat = | Etuplepat of pat list @@ -112,7 +116,8 @@ and eqdesc = and block = { b_local : var_dec list; b_equs : eq list; - b_loc : location; } + b_loc : location; + b_async : async_t option; } and state_handler = { s_state : state_name; @@ -211,8 +216,8 @@ and interface_desc = let mk_exp desc ?(ct_annot = Clocks.invalid_clock) loc = { e_desc = desc; e_ct_annot = ct_annot; e_loc = loc } -let mk_app op params = - { a_op = op; a_params = params } +let mk_app op ?(async=None) params = + { a_op = op; a_params = params; a_async = async; } let mk_call ?(params=[]) op exps = Eapp (mk_app op params, exps) @@ -246,9 +251,9 @@ let mk_var_dec name ty last loc = { v_name = name; v_type = ty; v_last = last; v_loc = loc } -let mk_block locals eqs loc = +let mk_block locals ?(async=None) eqs loc = { b_local = locals; b_equs = eqs; - b_loc = loc } + b_loc = loc; b_async = async } let mk_const_dec id ty e loc = { c_name = id; c_type = ty; c_value = e; c_loc = loc } diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 912fefc..7a8c3d0 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -298,6 +298,7 @@ and ty funs acc t = match t with let t, acc = ty_it funs acc t in let e, acc = exp_it funs acc e in Tarray (t, e), acc + | Tasync (a, t) -> let t, acc = ty_it funs acc t in Tasync (a, t), acc and const_dec_it funs acc c = funs.const_dec funs acc c diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 9b52935..064d69a 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -214,7 +214,8 @@ let rec translate_type loc ty = | Tid ln -> Types.Tid (qualify_type ln) | Tarray (ty, e) -> let ty = translate_type loc ty in - Types.Tarray (ty, expect_static_exp e)) + Types.Tarray (ty, expect_static_exp e) + | Tasync (a, ty) -> Types.Tasync (a, translate_type loc ty)) with | ScopingError err -> message loc err @@ -242,16 +243,17 @@ and translate_desc loc env = function List.map (fun (f,e) -> qualify_field f, translate_exp env e) f_e_list in Heptagon.Estruct f_e_list - | Eapp ({ a_op = op; a_params = params }, e_list) -> + | Eapp ({ a_op = op; a_params = params; a_async = async }, e_list) -> let e_list = List.map (translate_exp env) e_list in let params = List.map (expect_static_exp) params in - let app = Heptagon.mk_op ~params:params (translate_op op) in + let app = Heptagon.mk_app ~params:params ~async:async (translate_op op) in Heptagon.Eapp (app, e_list, None) + | Eiterator (it, { a_op = op; a_params = params }, n, e_list) -> let e_list = List.map (translate_exp env) e_list in let n = expect_static_exp n in let params = List.map (expect_static_exp) params in - let app = Heptagon.mk_op ~params:params (translate_op op) in + let app = Heptagon.mk_app ~params:params (translate_op op) in Heptagon.Eiterator (translate_iterator_type it, app, n, e_list, None) | Ewhen (e, c, ce) -> @@ -269,6 +271,7 @@ and translate_desc loc env = function List.map fun_c_e c_e_list in Heptagon.Emerge (e, c_e_list) + and translate_op = function | Eequal -> Heptagon.Eequal | Earrow -> Heptagon.Earrow @@ -285,6 +288,7 @@ and translate_op = function | Eselect_dyn -> Heptagon.Eselect_dyn | Efun ln -> Heptagon.Efun (qualify_value ln) | Enode ln -> Heptagon.Enode (qualify_value ln) + | Ebang -> Heptagon.Ebang and translate_pat loc env = function | Evarpat x -> Heptagon.Evarpat (Rename.var loc env x) @@ -293,7 +297,7 @@ and translate_pat loc env = function let rec translate_eq env eq = { Heptagon.eq_desc = translate_eq_desc eq.eq_loc env eq.eq_desc ; Heptagon.eq_statefull = false; - Heptagon.eq_loc = eq.eq_loc } + Heptagon.eq_loc = eq.eq_loc; } and translate_eq_desc loc env = function | Eswitch(e, switch_handlers) -> @@ -323,7 +327,8 @@ and translate_block env b = Heptagon.b_equs = List.map (translate_eq env) b.b_equs; Heptagon.b_defnames = Env.empty; Heptagon.b_statefull = false; - Heptagon.b_loc = b.b_loc }, env + Heptagon.b_loc = b.b_loc; + Heptagon.b_async = b.b_async; }, env and translate_state_handler env sh = let b, env = translate_block env sh.s_block in diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index a2c36ac..0de28cb 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -209,11 +209,11 @@ let rec translate_op = function | Heptagon.Econcat -> Econcat | Heptagon.Earray -> Earray | Heptagon.Etuple -> Etuple - | Heptagon.Earrow -> - Error.message no_location Error.Eunsupported_language_construct + | Heptagon.Earrow -> Error.message no_location Error.Eunsupported_language_construct + | Heptagon.Ebang -> Ebang let translate_app app = - mk_app ~params:app.Heptagon.a_params + mk_app ~params:app.Heptagon.a_params ~async:app.Heptagon.a_async ~unsafe:app.Heptagon.a_unsafe (translate_op app.Heptagon.a_op) let rec translate env diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index c9bd4ae..b47870c 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -74,8 +74,7 @@ let rec translate map e = | Minils.Evar n -> Elhs (var_from_name map n) | Minils.Eapp ({ Minils.a_op = Minils.Eequal }, e_list, _) -> Eop (op_from_string "=", List.map (translate map ) e_list) - | Minils.Eapp ({ Minils.a_op = Minils.Efun n }, - e_list, _) when Mls_utils.is_op n -> + | Minils.Eapp ({ Minils.a_op = Minils.Efun n }, e_list, _) when Mls_utils.is_op n -> Eop (n, List.map (translate map ) e_list) | Minils.Ewhen (e, _, _) -> let e = translate map e in @@ -98,9 +97,18 @@ let rec translate map e = let e = translate map (assert_1 e_list) in let idx_list = List.map (fun idx -> mk_exp (Econst idx)) idx in Elhs (lhs_of_idx_list (lhs_of_exp e) idx_list) - | _ -> - Format.eprintf "%a@." Mls_printer.print_exp e; - assert false + (* Async operators *) + | Minils.Eapp ({Minils.a_op = Minils.Ebang }, e_list, _) -> + let e = translate map (assert_1 e_list) in + Ebang e + (* Already treated cases when translating the [eq] *) + | Minils.Eiterator _ | Minils.Emerge _ | Minils.Efby _ + | Minils.Eapp ({Minils.a_op=(Minils.Enode _|Minils.Efun _|Minils.Econcat|Minils.Eupdate|Minils.Eselect_dyn + |Minils.Eselect_slice|Minils.Earray_fill|Minils.Efield_update|Minils.Eifthenelse + |Minils.Etuple)}, _, _) -> + Format.eprintf "%aThis should not be treated as an exp in mls2obc : %a@." + Location.print_location e.Minils.e_loc Mls_printer.print_exp e; + assert false in mk_exp ~ty:e.Minils.e_ty desc @@ -347,12 +355,14 @@ and mk_node_call map call_context app loc name_list args = { o_name = obj_ref_name o; o_class = f; o_params = app.Minils.a_params; o_size = size_from_call_context call_context; o_loc = loc } in - let si = - (match app.Minils.a_op with - | Minils.Efun _ -> [] - | Minils.Enode _ -> [reinit o] - | _ -> assert false) in - [], si, [obj], [Acall (name_list, o, Mstep, args)] + let si = (match app.Minils.a_op with + | Minils.Efun _ -> [] + | Minils.Enode _ -> [reinit o] + | _ -> assert false) in + let s = (match app.Minils.a_async with + | None -> [Acall (name_list, o, Mstep, args)] + | Some a -> [Aasync_call (a, name_list, o, Mstep, args)]) in + [], si, [obj], s | _ -> assert false and translate_iterator map call_context it name_list app loc n x c_list = diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index b13cc27..06978f2 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -95,6 +95,9 @@ and typing_op op e_list h e ck = match op with let e1, e2 = assert_2 e_list in let ct = skeleton ck e.e_ty in (expect h (Ck ck) e1; expect h ct e2; ct) + | Ebang -> + let e = assert_1 e_list in + typing h e and expect h expected_ty e = let actual_ty = typing h e in diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 361cfe2..4ecebcc 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -61,7 +61,7 @@ and edesc = | Eiterator of iterator_type * app * static_exp * exp list * var_ident option (** map f <> (exp, exp...) reset ident *) -and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } +and app = { a_op: op; a_params: static_exp list; a_async : async_t option; a_unsafe: bool } (** Unsafe applications could have side effects and be delicate about optimizations, !be careful! *) @@ -80,6 +80,7 @@ and op = | Eselect_dyn (** arg1.[arg3...] default arg2 *) | Eupdate (** [ arg1 with arg3..arg_n = arg2 ] *) | Econcat (** arg1@@arg2 *) + | Ebang (** !arg1 *) type pat = @@ -165,8 +166,8 @@ let mk_type_dec type_desc name loc = let mk_const_dec id ty e loc = { c_name = id; c_type = ty; c_value = e; c_loc = loc } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } +let mk_app ?(params=[]) ?(async=None) ?(unsafe=false) op = + { a_op = op; a_params = params; a_async = async; a_unsafe = unsafe } (** The modname field has to be set when known, TODO LG : format_version *) let mk_program o n t c = diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index a4fe171..9c07fde 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -90,7 +90,7 @@ and app_compare app1 app2 = | (Eequal | Etuple | Efun _ | Enode _ | Eifthenelse | Efield | Efield_update), _ -> -1 | (Earray | Earray_fill | Eselect | Eselect_slice | Eselect_dyn | Eupdate - | Econcat), _ -> 1 in + | Econcat | Ebang), _ -> 1 in if cr <> 0 then cr else list_compare static_exp_compare app1.a_params app2.a_params diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 8bebfc0..0fb87f3 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -110,51 +110,56 @@ and print_exp_desc ff = function print_exp_tuple args print_every reset -and print_app ff (app, args) = match app.a_op with - | Eequal -> - let e1, e2 = assert_2 args in - fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2 - | Etuple -> print_exp_tuple ff args - | Efun f | Enode f -> - fprintf ff "@[%a@,%a@,%a@]" - print_qualname f print_params app.a_params print_exp_tuple args - | Eifthenelse -> - let e1, e2, e3 = assert_3 args in - fprintf ff "@[if %a@ then %a@ else %a@]" - print_exp e1 print_exp e2 print_exp e3 - | Efield -> - let r = assert_1 args in - let f = assert_1 app.a_params in - fprintf ff "%a.%a" print_exp r print_static_exp f - | Efield_update -> - let r,e = assert_2 args in - let f = assert_1 app.a_params in - fprintf ff "@[<2>{%a with .%a =@ %a}@]" - print_exp r print_static_exp f print_exp e - | Earray -> fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") args - | Earray_fill -> - let e = assert_1 args in - let n = assert_1 app.a_params in - fprintf ff "%a^%a" print_exp e print_static_exp n - | Eselect -> - let e = assert_1 args in - fprintf ff "%a%a" print_exp e print_index app.a_params - | Eselect_slice -> - let e = assert_1 args in - let idx1, idx2 = assert_2 app.a_params in - fprintf ff "%a[%a..%a]" - print_exp e print_static_exp idx1 print_static_exp idx2 - | Eselect_dyn -> - let r, d, e = assert_2min args in - fprintf ff "%a%a default %a" - print_exp r print_dyn_index e print_exp d - | Eupdate -> - let e1, e2, idx = assert_2min args in - fprintf ff "@[<2>(%a with %a =@ %a)@]" - print_exp e1 print_dyn_index idx print_exp e2 - | Econcat -> - let e1, e2 = assert_2 args in - fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 +and print_app ff (app, args) = + print_async ff app.a_async; + match app.a_op with + | Eequal -> + let e1, e2 = assert_2 args in + fprintf ff "@[<2>%a@ = %a@]" print_exp e1 print_exp e2 + | Etuple -> print_exp_tuple ff args + | Efun f | Enode f -> + fprintf ff "@[%a@,%a@,%a@]" + print_qualname f print_params app.a_params print_exp_tuple args + | Eifthenelse -> + let e1, e2, e3 = assert_3 args in + fprintf ff "@[if %a@ then %a@ else %a@]" + print_exp e1 print_exp e2 print_exp e3 + | Efield -> + let r = assert_1 args in + let f = assert_1 app.a_params in + fprintf ff "%a.%a" print_exp r print_static_exp f + | Efield_update -> + let r,e = assert_2 args in + let f = assert_1 app.a_params in + fprintf ff "@[<2>{%a with .%a =@ %a}@]" + print_exp r print_static_exp f print_exp e + | Earray -> fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") args + | Earray_fill -> + let e = assert_1 args in + let n = assert_1 app.a_params in + fprintf ff "%a^%a" print_exp e print_static_exp n + | Eselect -> + let e = assert_1 args in + fprintf ff "%a%a" print_exp e print_index app.a_params + | Eselect_slice -> + let e = assert_1 args in + let idx1, idx2 = assert_2 app.a_params in + fprintf ff "%a[%a..%a]" + print_exp e print_static_exp idx1 print_static_exp idx2 + | Eselect_dyn -> + let r, d, e = assert_2min args in + fprintf ff "%a%a default %a" + print_exp r print_dyn_index e print_exp d + | Eupdate -> + let e1, e2, idx = assert_2min args in + fprintf ff "@[<2>(%a with %a =@ %a)@]" + print_exp e1 print_dyn_index idx print_exp e2 + | Econcat -> + let e1, e2 = assert_2 args in + fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 + | Ebang -> + let e = assert_1 args in + fprintf ff "!(%a)" print_exp e and print_handler ff c = fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index a15d639..6fd38f4 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -274,6 +274,10 @@ and translate_app kind context op e_list = let context, e1 = translate VRef context e1 in let context, e2 = translate VRef context e2 in context, [e1; e2] + | Ebang -> + let e = assert_1 e_list in + let context, e = translate Exp context e in + context, [e] | Enode _ | Efun _ | Eifthenelse _ -> assert false (*already done in translate*) diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index dce1cfd..9352d46 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -398,7 +398,7 @@ let rec reconstruct input_type (env : PatEnv.t) = | Etuplepat pat_list, Tprod ty_list -> List.fold_right2 mk_var_decs pat_list ty_list var_list | Etuplepat [], Tunit -> var_list - | Etuplepat _, (Tarray _ | Tid _ | Tunit) -> assert false (* ill-typed *) in + | Etuplepat _, (Tarray _ | Tid _ | Tunit | Tasync _) -> assert false (* ill-typed *) in (* TODO async *) let add_to_lists pat (_, head, children) (eq_list, var_list) = (* Remember the encoding of resets given above. *) diff --git a/compiler/obc/c/cgen.ml b/compiler/obc/c/cgen.ml index 4f6728a..20ede8c 100644 --- a/compiler/obc/c/cgen.ml +++ b/compiler/obc/c/cgen.ml @@ -103,6 +103,7 @@ let rec ctype_of_otype oty = ctype_of_otype ty) | Tprod _ -> assert false | Tunit -> assert false + | Tasync _ -> assert false (* TODO async *) let cvarlist_of_ovarlist vl = let cvar_of_ovar vd = @@ -288,6 +289,8 @@ let rec cexpr_of_exp var_env exp = Cstructlit (ctyn, cexps) | Earray e_list -> Carraylit (cexprs_of_exps var_env e_list) + | Ebang _ -> + (* TODO async *) assert false and cexprs_of_exps var_env exps = List.map (cexpr_of_exp var_env) exps @@ -491,6 +494,8 @@ let rec cstm_of_act var_env obj_env act = [Csexpr (Cfun_call (classn ^ "_reset", elt ))] )] ) + | Aasync_call _ -> assert false (* TODO async *) + (** Special case for x = 0^n^n...*) | Aassgn (vn, { e_desc = Econst c }) -> let vn = clhs_of_lhs var_env vn in diff --git a/compiler/obc/c/cmain.ml b/compiler/obc/c/cmain.ml index d295da5..c5bf85e 100644 --- a/compiler/obc/c/cmain.ml +++ b/compiler/obc/c/cmain.ml @@ -85,14 +85,14 @@ let assert_node_res cd = (** [main_def_of_class_def cd] returns a [(var_list, rst_i, step_i)] where [var_list] (resp. [rst_i] and [step_i]) is a list of variables (resp. of statements) needed for a main() function calling [cd]. *) -(* TODO: refactor into something more readable. *) let main_def_of_class_def cd = let format_for_type ty = match ty with | Tarray _ | Tprod _ | Tunit -> assert false | Types.Tid id when id = Initial.pfloat -> "%f" | Types.Tid id when id = Initial.pint -> "%d" | Types.Tid id when id = Initial.pbool -> "%d" - | Tid _ -> "%s" in + | Tid _ -> "%s" + | Tasync _ -> assert false (* TODO async *) in (** Does reading type [ty] need a buffer? When it is the case, [need_buf_for_ty] also returns the type's name. *) @@ -101,7 +101,8 @@ let main_def_of_class_def cd = | Types.Tid id when id = Initial.pfloat -> None | Types.Tid id when id = Initial.pint -> None | Types.Tid id when id = Initial.pbool -> None - | Tid { name = n } -> Some n in + | Tid { name = n } -> Some n + | Tasync _ -> assert false (* TODO async *) in let cprint_string s = Csexpr (Cfun_call ("printf", [Cconst (Cstrlit s)])) in diff --git a/compiler/obc/obc.ml b/compiler/obc/obc.ml index 9dd83de..7b7107a 100644 --- a/compiler/obc/obc.ml +++ b/compiler/obc/obc.ml @@ -53,6 +53,7 @@ and exp_desc = | Eop of op_name * exp list | Estruct of type_name * (field_name * exp) list | Earray of exp list + | Ebang of exp type obj_ref = | Oobj of obj_name @@ -65,6 +66,7 @@ type method_name = type act = | Aassgn of pattern * exp | Acall of pattern list * obj_ref * method_name * exp list + | Aasync_call of async_t * pattern list * obj_ref * method_name * exp list | Acase of exp * (constructor_name * block) list | Afor of var_ident * static_exp * static_exp * block diff --git a/compiler/obc/obc_mapfold.ml b/compiler/obc/obc_mapfold.ml index 32cdde3..a0c8dd6 100644 --- a/compiler/obc/obc_mapfold.ml +++ b/compiler/obc/obc_mapfold.ml @@ -62,6 +62,9 @@ and edesc funs acc ed = match ed with | Earray args -> let args, acc = mapfold (exp_it funs) acc args in Earray args, acc + | Ebang e -> + let e, acc = exp_it funs acc e in + Ebang e, acc and lhs_it funs acc l = funs.lhs funs acc l @@ -97,6 +100,10 @@ and act funs acc a = match a with let lhs_list, acc = mapfold (lhs_it funs) acc lhs_list in let args, acc = mapfold (exp_it funs) acc args in Acall(lhs_list, obj, n, args), acc + | Aasync_call(a, lhs_list, obj, n, args) -> + let lhs_list, acc = mapfold (lhs_it funs) acc lhs_list in + let args, acc = mapfold (exp_it funs) acc args in + Aasync_call(a, lhs_list, obj, n, args), acc | Acase(x, c_b_list) -> let aux acc (c,b) = let b, acc = block_it funs acc b in diff --git a/compiler/obc/obc_printer.ml b/compiler/obc/obc_printer.ml index 8738572..4d7c8e5 100644 --- a/compiler/obc/obc_printer.ml +++ b/compiler/obc/obc_printer.ml @@ -51,6 +51,8 @@ and print_exp ff e = fprintf ff "@["; print_list_r print_exp "[" ";" "]" ff e_list; fprintf ff "@]" + | Ebang e -> + fprintf ff "!(%a)" print_exp e and print_op ff op e_list = match e_list with | [l; r] -> @@ -75,6 +77,7 @@ let print_method_name ff = function | Mstep -> fprintf ff "step" | Mreset -> fprintf ff "reset" + let rec print_act ff a = let print_lhs_tuple ff var_list = match var_list with | [] -> () @@ -98,6 +101,13 @@ let rec print_act ff a = print_obj_call o print_method_name meth print_exps es + | Aasync_call (a, var_list, o, meth, es) -> + fprintf ff "@[<2>%a%a%a.%a(%a)@]" + print_lhs_tuple var_list + print_async (Some a) + print_obj_call o + print_method_name meth + print_exps es and print_var_dec_list ff var_dec_list = match var_dec_list with | [] -> ()