Added init construct

It is part of a pattern, eg:
  (init<<r>> x, y, init<<r2>>) = f()
This commit is contained in:
Cédric Pasteur 2011-04-27 11:45:57 +02:00
parent d5218ff91c
commit 6332ac7a10
10 changed files with 67 additions and 22 deletions

View file

@ -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

View file

@ -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)

View file

@ -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 "@[<v>@[<hv 2>automaton @ %a@]@,end@]"
print_state_handler_list state_handler_list

View file

@ -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 =

View file

@ -81,6 +81,7 @@ and pat =
type eq = {
eq_desc : eqdesc;
eq_stateful : bool;
eq_inits : init;
eq_loc : location; }
and eqdesc =

View file

@ -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");

View file

@ -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 <string> PREFIX
%token <string> INFIX0
%token <string> 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:

View file

@ -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;

View file

@ -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

View file

@ -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