From 2b2cba8e2d567322b586768d88896345c82620ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 29 Apr 2011 13:58:31 +0200 Subject: [PATCH] Added split operator --- compiler/heptagon/analysis/causality.ml | 4 +++ compiler/heptagon/analysis/initialization.ml | 4 ++- compiler/heptagon/analysis/linear_typing.ml | 14 +++++---- compiler/heptagon/analysis/typing.ml | 30 +++++++++++++++++++ compiler/heptagon/hept_mapfold.ml | 5 +++- compiler/heptagon/hept_printer.ml | 3 ++ compiler/heptagon/hept_utils.ml | 9 +++--- compiler/heptagon/heptagon.ml | 1 + compiler/heptagon/parsing/hept_lexer.mll | 1 + compiler/heptagon/parsing/hept_parser.mly | 4 ++- compiler/heptagon/parsing/hept_parsetree.ml | 1 + .../parsing/hept_parsetree_mapfold.ml | 4 +++ compiler/heptagon/parsing/hept_scoping.ml | 5 +++- .../heptagon/transformations/normalize.ml | 14 +++++++++ compiler/main/hept2mls.ml | 2 +- compiler/main/mls2obc.ml | 1 - compiler/minils/analysis/interference.ml | 2 +- 17 files changed, 88 insertions(+), 16 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index fa94912..ba17ffd 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -121,6 +121,10 @@ let rec typing e = let t = read x in let tl = List.map (fun (_,e) -> typing e) c_e_list in cseq t (candlist tl) + | Esplit(c, e) -> + let t = typing c in + let te = typing e in + cseq t te (** Typing an application *) diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index cc23707..cd0aaa4 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -260,7 +260,9 @@ let rec typing h e = (fun acc (_, e) -> imax acc (itype (typing h e))) izero c_e_list in let i = imax (IEnv.find_var x h) i in skeleton i e.e_ty - + | Esplit (c, e2) -> + let i = imax (itype (typing h c)) (itype (typing h e2)) in + skeleton i e.e_ty (** Typing an application *) and apply h app e_list = diff --git a/compiler/heptagon/analysis/linear_typing.ml b/compiler/heptagon/analysis/linear_typing.ml index 9f269eb..9269c56 100644 --- a/compiler/heptagon/analysis/linear_typing.ml +++ b/compiler/heptagon/analysis/linear_typing.ml @@ -401,7 +401,7 @@ let rec typing_exp env e = | Eapp ({ a_op = Efield }, _, _) -> Ltop | Eapp ({ a_op = Earray }, _, _) -> Ltop | Estruct _ -> Ltop - | Emerge _ | Ewhen _ | Eapp _ | Eiterator _ -> assert false + | Emerge _ | Ewhen _ | Esplit _ | Eapp _ | Eiterator _ -> assert false in e.e_linearity <- l; l @@ -701,15 +701,19 @@ and expect env lin e = check_linearity_exp env e lin; unify_lin lin actual_lin - | Emerge (c, c_e_list) -> - safe_expect env Ltop c; + | Emerge (_, c_e_list) -> List.iter (fun (_, e) -> safe_expect env lin e) c_e_list; lin - | Ewhen (e, _, x) -> - safe_expect env Ltop x; + | Ewhen (e, _, _) -> expect env lin e + | Esplit (c, e) -> + safe_expect env Ltop c; + let l = linearity_list_of_linearity lin in + safe_expect env (List.hd l) e; + lin + | Eapp ({ a_op = Etuple }, e_list, _) -> let lin_list = linearity_list_of_linearity lin in (try diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 9e7eb08..b297568 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -52,6 +52,8 @@ type error = | Emerge_missing_constrs of QualSet.t | Emerge_uniq of qualname | Emerge_mix of qualname + | Esplit_enum of ty + | Esplit_tuple of ty exception Unify exception TypingError of error @@ -168,6 +170,18 @@ let message loc kind = as the last argument (found: %a).@." print_location loc print_type ty + | Esplit_enum ty -> + eprintf + "%aThe first argument of split has to be an \ + enumerated type (found: %a).@." + print_location loc + print_type ty + | Esplit_tuple ty -> + eprintf + "%aThe second argument of spit cannot \ + be a tuple (found: %a).@." + print_location loc + print_type ty end; raise Errors.Error @@ -595,6 +609,22 @@ let rec typing const_env h e = List.map (fun (c, e) -> (c, expect const_env h t e)) c_e_list in Emerge (x, (c1,typed_e1)::typed_c_e_list), t | Emerge (_, []) -> assert false + + | Esplit(c, e2) -> + let typed_c, ty_c = typing const_env h c in + let typed_e2, ty = typing const_env h e2 in + let n = + match ty_c with + | Tid tc -> + (match find_type tc with | Tenum cl-> List.length cl | _ -> -1) + | _ -> -1 in + if n < 0 then + message e.e_loc (Esplit_enum ty_c); + (*the type of e should not be a tuple *) + (match ty with + | Tprod _ -> message e.e_loc (Esplit_tuple ty) + | _ -> ()); + Esplit(typed_c, typed_e2), Tprod (repeat_list ty n) in { e with e_desc = typed_desc; e_ty = ty; }, ty with diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index 3b27e08..c3ca34b 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -125,7 +125,10 @@ and edesc funs acc ed = match ed with (c,e), acc in let c_e_list, acc = mapfold aux acc c_e_list in Emerge (n, c_e_list), acc - + | Esplit (e1, e2) -> + let e1, acc = exp_it funs acc e1 in + let e2, acc = exp_it funs acc e2 in + Esplit(e1, e2), acc and app_it funs acc a = funs.app funs acc a diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index f94ef02..3117cb7 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -132,6 +132,9 @@ and print_exp_desc ff = function | Emerge (x, tag_e_list) -> fprintf ff "@[<2>merge %a@ %a@]" print_ident x print_tag_e_list tag_e_list + | Esplit (x, e1) -> + fprintf ff "@[<2>split %a@ %a@]" + print_exp x print_exp e1 and print_handler ff c = fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml index 562ae66..90380a9 100644 --- a/compiler/heptagon/hept_utils.ml +++ b/compiler/heptagon/hept_utils.ml @@ -14,13 +14,14 @@ open Idents open Static open Signature open Types +open Linearity open Clocks open Initial open Heptagon (* Helper functions to create AST. *) -let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = - { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; +let mk_exp desc ?(linearity = Ltop) ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = + { e_desc = desc; e_ty = ty; e_linearity = linearity; e_ct_annot = ct_annot; e_base_ck = Cbase; e_loc = loc; } let mk_app ?(params=[]) ?(unsafe=false) op = @@ -39,8 +40,8 @@ let mk_equation ?(loc=no_location) desc = eq_inits = Lno_init; eq_loc = loc; } -let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty = - { v_ident = name; v_type = ty; v_clock = clock; +let mk_var_dec ?(last = Var) ?(linearity = Ltop) ?(clock = fresh_clock()) name ty = + { v_ident = name; v_type = ty; v_linearity = linearity; v_clock = clock; v_last = last; v_loc = no_location } let mk_block ?(stateful = true) ?(defnames = Env.empty) ?(locals = []) eqs = diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 1de6193..56ddfc4 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -47,6 +47,7 @@ and desc = (** exp when Constructor(ident) *) | Emerge of var_ident * (constructor_name * exp) list (** merge ident (Constructor -> exp)+ *) + | Esplit of exp * exp | Eapp of app * exp list * exp option | Eiterator of iterator_type * app * static_exp * exp list * exp list * exp option diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 2e6fad4..9bfd0a3 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -62,6 +62,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "mapfold", MAPFOLD; "at", AT; "init", INIT; + "split", SPLIT; "quo", INFIX3("quo"); "mod", INFIX3("mod"); "land", INFIX3("land"); diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index b7aadf3..f86c698 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -48,7 +48,7 @@ open Hept_parsetree %token AROBASE %token DOUBLE_LESS DOUBLE_GREATER %token MAP MAPI FOLD FOLDI MAPFOLD -%token AT INIT +%token AT INIT SPLIT %token PREFIX %token INFIX0 %token INFIX1 @@ -442,6 +442,8 @@ _exp: /* node call*/ | n=qualname p=call_params LPAREN args=exps RPAREN { Eapp(mk_app (Enode n) p , args) } + | SPLIT n=exp e=exp + { Esplit(n, 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 aa63c42..1f04bd3 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -77,6 +77,7 @@ and edesc = | Eiterator of iterator_type * app * exp * exp list * exp list | Ewhen of exp * constructor_name * var_name | Emerge of var_name * (constructor_name * exp) list + | Esplit of exp * exp and app = { a_op: op; a_params: exp list; } diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index ca942ad..1b30c2d 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -111,6 +111,10 @@ and edesc funs acc ed = match ed with | Ewhen (e, c, x) -> let e, acc = exp_it funs acc e in Ewhen (e, c, x), acc + | Esplit (e1, e2) -> + let e1, acc = exp_it funs acc e1 in + let e2, acc = exp_it funs acc e2 in + Esplit(e1, e2), acc | Eapp (app, args) -> let app, acc = app_it funs acc app in let args, acc = mapfold (exp_it funs) acc args in diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 2c7cc58..3adf2bc 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -286,7 +286,10 @@ and translate_desc loc env = function (c, e) in List.map fun_c_e c_e_list in Heptagon.Emerge (x, c_e_list) - + | Esplit (x, e1) -> + let x = translate_exp env x in + let e1 = translate_exp env e1 in + Heptagon.Esplit(x, e1) and translate_op = function | Eequal -> Heptagon.Eequal diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 27608c5..dbb4282 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -149,6 +149,20 @@ let rec translate kind context e = let context, e_list = translate_list ExtValue context e_list in context, { e with e_desc = Eiterator(it, app, n, flatten_e_list pe_list, flatten_e_list e_list, reset) } + | Esplit (x, e1) -> + let context, e1 = translate ExtValue context e1 in + let context, x = translate ExtValue context x in + let id = match x.e_desc with Evar x -> x | _ -> assert false in + let mk_when c = mk_exp ~linearity:e1.e_linearity (Ewhen (e1, c, id)) e1.e_ty in + (match x.e_ty with + | Tid t -> + (match Modules.find_type t with + | Signature.Tenum cl -> + let el = List.map mk_when cl in + context, { e with e_desc = Eapp(mk_app Etuple, el, None) } + | _ -> Misc.internal_error "normalize split" 0) + | _ -> Misc.internal_error "normalize split" 0) + | Elast _ | Efby _ -> Error.message e.e_loc Error.Eunsupported_language_construct in add context kind e' diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 359905b..1e5c379 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -141,7 +141,7 @@ let translate List.map translate_extvalue pe_list, List.map translate_extvalue e_list, translate_reset reset)) - | Heptagon.Efby _ + | Heptagon.Efby _ | Heptagon.Esplit _ | Heptagon.Elast _ -> Error.message loc Error.Eunsupported_language_construct | Heptagon.Emerge (x, c_e_list) -> diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index c76dec9..2856dff 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -92,7 +92,6 @@ let rec bound_check_expr idx_list bounds = [mk_exp_int (Econst (mk_static_int 0)); idx])) in mk_exp_bool (Eop (op_from_string "&", [e1;e2])) in - Format.printf "%d == %d@." (List.length idx_list) (List.length bounds); match (idx_list, bounds) with | [idx], n::_ -> mk_comp idx n | (idx :: idx_list, n :: bounds) -> diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml index 56b1640..f6dfaca 100644 --- a/compiler/minils/analysis/interference.ml +++ b/compiler/minils/analysis/interference.ml @@ -9,7 +9,7 @@ open Containers open Printf let print_interference_graphs = false -let verbose_mode = true +let verbose_mode = false let print_debug0 s = if verbose_mode then Format.printf s