From 6332ac7a109abafeff5bbaa94a8beeb85033cf65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Wed, 27 Apr 2011 11:45:57 +0200 Subject: [PATCH] Added init construct It is part of a pattern, eg: (init<> x, y, init<>) = f() --- compiler/global/linearity.ml | 5 ++++ compiler/heptagon/analysis/linear_typing.ml | 28 +++++++++++++++++-- compiler/heptagon/hept_printer.ml | 19 +++++++++---- compiler/heptagon/hept_utils.ml | 1 + compiler/heptagon/heptagon.ml | 1 + compiler/heptagon/parsing/hept_lexer.mll | 1 + compiler/heptagon/parsing/hept_parser.mly | 24 ++++++++-------- compiler/heptagon/parsing/hept_parsetree.ml | 2 +- .../parsing/hept_parsetree_mapfold.ml | 4 +-- compiler/heptagon/parsing/hept_scoping.ml | 4 ++- 10 files changed, 67 insertions(+), 22 deletions(-) diff --git a/compiler/global/linearity.ml b/compiler/global/linearity.ml index 2f9b4a5..a4616ca 100644 --- a/compiler/global/linearity.ml +++ b/compiler/global/linearity.ml @@ -4,6 +4,11 @@ open Misc type linearity_var = name +type init = + | Lno_init + | Linit_var of linearity_var + | Linit_tuple of init list + type linearity = | Ltop | Lat of linearity_var diff --git a/compiler/heptagon/analysis/linear_typing.ml b/compiler/heptagon/analysis/linear_typing.ml index 00ed4e5..6020d78 100644 --- a/compiler/heptagon/analysis/linear_typing.ml +++ b/compiler/heptagon/analysis/linear_typing.ml @@ -17,6 +17,7 @@ type error = | Ewrong_linearity_for_iterator | Eoutput_linearity_not_declared of linearity_var | Emapi_bad_args of linearity + | Ewrong_init of linearity_var * linearity exception TypingError of error @@ -65,6 +66,13 @@ let message loc kind = variable as the last argument (found: %a).@." print_location loc print_linearity lin + | Ewrong_init (r, lin) -> + Format.eprintf + "%aThe variable defined by init<<%s>> should correspond \ + to the given location (found: %a).@." + print_location loc + r + print_linearity lin end; raise Errors.Error @@ -227,6 +235,21 @@ let subst_from_lin (s,m) expect_lin lin = let rec not_linear_for_exp e = lin_skeleton Ltop e.e_ty +let check_init loc init lin = + let check_one init lin = match init with + | Lno_init -> lin + | Linit_var r -> + (match lin with + | Lat r1 when r = r1 -> Ltop + | Lvar r1 when r = r1 -> Ltop + | _ -> message loc (Ewrong_init (r, lin))) + | Linit_tuple _ -> assert false + in + match init, lin with + | Linit_tuple il, Ltuple ll -> + Ltuple (List.map2 check_one il ll) + | _, _ -> check_one init lin + (** [unify_collect collect_list lin_list coll_exp] returns a list of linearities to use when a choice is possible (eg for a map). It collects the possible values for all args and then tries to map them to the expected values. @@ -375,8 +398,8 @@ let rec typing_exp env e = safe_expect env (not_linear_for_exp e1) e1; safe_expect env (not_linear_for_exp e1) e2; not_linear_for_exp e1 - | Eapp ({ a_op = Efield _ }, _, _) -> Ltop - | Eapp ({ a_op = Earray _ }, _, _) -> Ltop + | Eapp ({ a_op = Efield }, _, _) -> Ltop + | Eapp ({ a_op = Earray }, _, _) -> Ltop | Estruct _ -> Ltop | Emerge _ | Ewhen _ | Eapp _ | Eiterator _ -> assert false in @@ -646,6 +669,7 @@ and typing_eq env eq = ignore (typing_block env b) | Eeq(pat, e) -> let lin_pat = typing_pat env pat in + let lin_pat = check_init eq.eq_loc eq.eq_inits lin_pat in safe_expect env lin_pat e | Eblock b -> ignore (typing_block env b) diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index ef155af..f94ef02 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -33,10 +33,19 @@ let iterator_to_string i = let print_iterator ff it = fprintf ff "%s" (iterator_to_string it) -let rec print_pat ff = function - | Evarpat n -> print_ident ff n - | Etuplepat pat_list -> - fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list +let print_init ff = function + | Lno_init -> () + | Linit_var r -> fprintf ff "init<<%s>> " r + | _ -> () + +let rec print_pat_init ff (pat, inits) = match pat, inits with + | Evarpat n, i -> fprintf ff "%a%a" print_init i print_ident n + | Etuplepat pl, Linit_tuple il -> + fprintf ff "@[<2>(%a)@]" (print_list_r print_pat_init """,""") (List.combine pl il) + | Etuplepat pl, Lno_init -> + let l = List.map (fun p -> p, Lno_init) pl in + fprintf ff "@[<2>(%a)@]" (print_list_r print_pat_init """,""") l + | _, _ -> assert false let rec print_vd ff { v_ident = n; v_type = ty; v_linearity = lin; v_last = last } = fprintf ff "%a%a : %a%a%a" @@ -189,7 +198,7 @@ and print_app ff (app, args) = let rec print_eq ff eq = match eq.eq_desc with | Eeq(p, e) -> - fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e + fprintf ff "@[<2>%a =@ %a@]" print_pat_init (p, eq.eq_inits) print_exp e | Eautomaton(state_handler_list) -> fprintf ff "@[@[automaton @ %a@]@,end@]" print_state_handler_list state_handler_list diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml index 8953540..562ae66 100644 --- a/compiler/heptagon/hept_utils.ml +++ b/compiler/heptagon/hept_utils.ml @@ -36,6 +36,7 @@ let mk_equation ?(loc=no_location) desc = let _, s = Stateful.eqdesc Stateful.funs false desc in { eq_desc = desc; eq_stateful = s; + eq_inits = Lno_init; eq_loc = loc; } let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty = diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 6e720db..1de6193 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -81,6 +81,7 @@ and pat = type eq = { eq_desc : eqdesc; eq_stateful : bool; + eq_inits : init; eq_loc : location; } and eqdesc = diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index b1eb154..2e6fad4 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -61,6 +61,7 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "foldi", FOLDI; "mapfold", MAPFOLD; "at", AT; + "init", INIT; "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 9d2e2aa..b7aadf3 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 +%token AT INIT %token PREFIX %token INFIX0 %token INFIX1 @@ -99,6 +99,10 @@ slist(S, x) : delim_slist(S, L, R, x) : | {[]} | L l=slist(S, x) R {l} +/* Separated list with delimiter, even for empty list*/ +adelim_slist(S, L, R, x) : + | L R {[]} + | L l=slist(S, x) R {l} /*Separated Nonempty list */ snlist(S, x) : | x=x {[x]} @@ -268,7 +272,7 @@ ident_list: located_ty_ident: | ty_ident { $1, Ltop } - | ty_ident AT ident + | ty_ident AT IDENT { $1, Lat $3 } ; @@ -303,7 +307,7 @@ sblock(S) : equ: | eq=_equ { mk_equation eq (Loc($startpos,$endpos)) } _equ: - | pat EQUAL exp { Eeq($1, $3) } + | pat=pat EQUAL e=exp { Eeq(fst pat, snd pat, e) } | AUTOMATON automaton_handlers END { Eautomaton(List.rev $2) } | SWITCH exp opt_bar switch_handlers END @@ -389,14 +393,12 @@ present_handlers: ; pat: - | IDENT {Evarpat $1} - | LPAREN ids RPAREN {Etuplepat $2} -; - -ids: - | {[]} - | pat COMMA pat {[$1; $3]} - | pat COMMA ids {$1 :: $3} + | id=IDENT { Evarpat id, Lno_init } + | INIT DOUBLE_LESS r=IDENT DOUBLE_GREATER id=IDENT { Evarpat id, Linit_var r } + | pat_init_list=adelim_slist(COMMA, LPAREN, RPAREN, pat) + { let pat_list, init_list = List.split pat_init_list in + Etuplepat pat_list, Linit_tuple init_list + } ; nonmtexps: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index a80fad2..aa63c42 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -112,7 +112,7 @@ and eqdesc = | Epresent of present_handler list * block | Ereset of block * exp | Eblock of block - | Eeq of pat * exp + | Eeq of pat * Linearity.init * exp and block = { b_local : var_dec list; diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 29e6824..ca942ad 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -167,10 +167,10 @@ and eqdesc funs acc eqd = match eqd with | Eblock b -> let b, acc = block_it funs acc b in Eblock b, acc - | Eeq (p, e) -> + | Eeq (p, inits, e) -> let p, acc = pat_it funs acc p in let e, acc = exp_it funs acc e in - Eeq (p, e), acc + Eeq (p, inits, e), acc and block_it funs acc b = funs.block funs acc b diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index ea4ea69..2c7cc58 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -311,8 +311,10 @@ and translate_pat loc env = function | Etuplepat l -> Heptagon.Etuplepat (List.map (translate_pat loc env) l) let rec translate_eq env eq = + let init = match eq.eq_desc with | Eeq(_, init, _) -> init | _ -> Linearity.Lno_init in { Heptagon.eq_desc = translate_eq_desc eq.eq_loc env eq.eq_desc ; Heptagon.eq_stateful = false; + Heptagon.eq_inits = init; Heptagon.eq_loc = eq.eq_loc; } and translate_eq_desc loc env = function @@ -321,7 +323,7 @@ and translate_eq_desc loc env = function (translate_switch_handler loc env) switch_handlers in Heptagon.Eswitch (translate_exp env e, sh) - | Eeq(p, e) -> + | Eeq(p, _, e) -> Heptagon.Eeq (translate_pat loc env p, translate_exp env e) | Epresent (present_handlers, b) -> Heptagon.Epresent