jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Added split operator

Browse source
This commit is contained in:
Cédric Pasteur 2011-04-29 13:58:31 +02:00
parent 9686e2db01
commit 2b2cba8e2d
17 changed files with 88 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
compiler/heptagon/analysis/causality.ml
View file

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

4
compiler/heptagon/analysis/initialization.ml
View file

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

14
compiler/heptagon/analysis/linear_typing.ml
View file

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

30
compiler/heptagon/analysis/typing.ml
View file

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

5
compiler/heptagon/hept_mapfold.ml
View file

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

3
compiler/heptagon/hept_printer.ml
View file

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

9
compiler/heptagon/hept_utils.ml
View file

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

1
compiler/heptagon/heptagon.ml
View file

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

1
compiler/heptagon/parsing/hept_lexer.mll
View file

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

4
compiler/heptagon/parsing/hept_parser.mly
View file

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

1
compiler/heptagon/parsing/hept_parsetree.ml
View file

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

4
compiler/heptagon/parsing/hept_parsetree_mapfold.ml
View file

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

5
compiler/heptagon/parsing/hept_scoping.ml
View file

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

14
compiler/heptagon/transformations/normalize.ml
View file

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

2
compiler/main/hept2mls.ml
View file

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

1
compiler/main/mls2obc.ml
View file

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

2
compiler/minils/analysis/interference.ml
View file

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