Make Efield an op (as in Minils)
The fact that this commit mostly removes code proves that this was a good choice.
This commit is contained in:
parent
62e216314d
commit
46a09cf369
|
@ -105,7 +105,6 @@ let rec typing e =
|
||||||
let t2 = pre (typing e2) in
|
let t2 = pre (typing e2) in
|
||||||
candlist [t1; t2]
|
candlist [t1; t2]
|
||||||
| Eapp({ a_op = op }, e_list, _) -> apply op e_list
|
| Eapp({ a_op = op }, e_list, _) -> apply op e_list
|
||||||
| Efield(e1, _) -> typing e1
|
|
||||||
| Estruct(l) ->
|
| Estruct(l) ->
|
||||||
let l = List.map (fun (_, e) -> typing e) l in
|
let l = List.map (fun (_, e) -> typing e) l in
|
||||||
candlist l
|
candlist l
|
||||||
|
@ -119,6 +118,7 @@ and apply op e_list =
|
||||||
let t1 = typing e1 in
|
let t1 = typing e1 in
|
||||||
let t2 = typing e2 in
|
let t2 = typing e2 in
|
||||||
candlist [t1; t2]
|
candlist [t1; t2]
|
||||||
|
| Efield, [e1] -> typing e1
|
||||||
| Eifthenelse, [e1; e2; e3] ->
|
| Eifthenelse, [e1; e2; e3] ->
|
||||||
let t1 = typing e1 in
|
let t1 = typing e1 in
|
||||||
let i2 = typing e2 in
|
let i2 = typing e2 in
|
||||||
|
|
|
@ -207,9 +207,6 @@ let rec typing h e =
|
||||||
| Eapp({ a_op = op }, e_list, _) ->
|
| Eapp({ a_op = op }, e_list, _) ->
|
||||||
let i = apply h op e_list in
|
let i = apply h op e_list in
|
||||||
skeleton i e.e_ty
|
skeleton i e.e_ty
|
||||||
| Efield(e1, _) ->
|
|
||||||
let i = itype (typing h e1) in
|
|
||||||
skeleton i e.e_ty
|
|
||||||
| Estruct(l) ->
|
| Estruct(l) ->
|
||||||
let i =
|
let i =
|
||||||
List.fold_left
|
List.fold_left
|
||||||
|
@ -226,6 +223,8 @@ and apply h op e_list =
|
||||||
let ty1 = typing h e1 in
|
let ty1 = typing h e1 in
|
||||||
let _ = typing h e2 in
|
let _ = typing h e2 in
|
||||||
itype ty1
|
itype ty1
|
||||||
|
| Efield, [e1] ->
|
||||||
|
itype (typing h e1)
|
||||||
| Earray, e_list ->
|
| Earray, e_list ->
|
||||||
List.fold_left
|
List.fold_left
|
||||||
(fun acc e -> max acc (itype (typing h e))) izero e_list
|
(fun acc e -> max acc (itype (typing h e))) izero e_list
|
||||||
|
|
|
@ -240,7 +240,6 @@ let rec is_statefull_exp e =
|
||||||
| Eiterator(_, { a_op = Enode _ }, _, _, _) -> true
|
| Eiterator(_, { a_op = Enode _ }, _, _, _) -> true
|
||||||
| Eiterator(_, _, _, e_list, _) ->
|
| Eiterator(_, _, _, e_list, _) ->
|
||||||
List.exists is_statefull_exp e_list
|
List.exists is_statefull_exp e_list
|
||||||
| Efield(e, _) -> is_statefull_exp e
|
|
||||||
|
|
||||||
let rec is_statefull_eq_desc = function
|
let rec is_statefull_eq_desc = function
|
||||||
| Eautomaton(handlers) ->
|
| Eautomaton(handlers) ->
|
||||||
|
@ -580,12 +579,6 @@ let rec typing statefull const_env h e =
|
||||||
typing_app statefull const_env h op e_list in
|
typing_app statefull const_env h op e_list in
|
||||||
Eapp(op, typed_e_list, r), ty
|
Eapp(op, typed_e_list, r), ty
|
||||||
|
|
||||||
| Efield(e, f) ->
|
|
||||||
let typed_e, t1 = typing statefull const_env h e in
|
|
||||||
let q, fields = struct_info e.e_loc t1 in
|
|
||||||
let t2 = field_type const_env f fields t1 e.e_loc in
|
|
||||||
Efield(typed_e, Modname { qual = q.qual; id = shortname f }), t2
|
|
||||||
|
|
||||||
| Estruct(l) ->
|
| Estruct(l) ->
|
||||||
(* find the record type using the first field *)
|
(* find the record type using the first field *)
|
||||||
let q, fields =
|
let q, fields =
|
||||||
|
@ -708,6 +701,18 @@ and typing_app statefull const_env h op e_list =
|
||||||
(Sint (List.length e_list + 1)) in
|
(Sint (List.length e_list + 1)) in
|
||||||
Tarray(t1, n), op, typed_exp::typed_e_list
|
Tarray(t1, n), op, typed_exp::typed_e_list
|
||||||
|
|
||||||
|
| { a_op = Efield; a_params = [f] }, [e] ->
|
||||||
|
let fn =
|
||||||
|
(match f.se_desc with
|
||||||
|
| Sconstructor fn -> fn
|
||||||
|
| _ -> assert false) in
|
||||||
|
let typed_e, t1 = typing statefull const_env h e in
|
||||||
|
let q, fields = struct_info e.e_loc t1 in
|
||||||
|
let t2 = field_type const_env fn fields t1 e.e_loc in
|
||||||
|
let fn = Modname { qual = q.qual; id = shortname fn } in
|
||||||
|
let f = { f with se_desc = Sconstructor fn } in
|
||||||
|
t2, { op with a_params = [f] }, [typed_e]
|
||||||
|
|
||||||
| { a_op = Efield_update; a_params = [f] }, [e1; e2] ->
|
| { a_op = Efield_update; a_params = [f] }, [e1; e2] ->
|
||||||
let typed_e1, t1 = typing statefull const_env h e1 in
|
let typed_e1, t1 = typing statefull const_env h e1 in
|
||||||
let q, fields = struct_info e1.e_loc t1 in
|
let q, fields = struct_info e1.e_loc t1 in
|
||||||
|
|
|
@ -108,9 +108,6 @@ and edesc funs acc ed = match ed with
|
||||||
let e1, acc = exp_it funs acc e1 in
|
let e1, acc = exp_it funs acc e1 in
|
||||||
let e2, acc = exp_it funs acc e2 in
|
let e2, acc = exp_it funs acc e2 in
|
||||||
Efby (e1,e2), acc
|
Efby (e1,e2), acc
|
||||||
| Efield (e, n) ->
|
|
||||||
let e, acc = exp_it funs acc e in
|
|
||||||
Efield(e, n), acc
|
|
||||||
| Estruct n_e_list ->
|
| Estruct n_e_list ->
|
||||||
let aux acc (n,e) =
|
let aux acc (n,e) =
|
||||||
let e, acc = exp_it funs acc e in
|
let e, acc = exp_it funs acc e in
|
||||||
|
|
|
@ -64,9 +64,6 @@ and print_exp ff e =
|
||||||
| None -> ()
|
| None -> ()
|
||||||
| Some r -> fprintf ff " every %a" print_exp r
|
| Some r -> fprintf ff " every %a" print_exp r
|
||||||
)
|
)
|
||||||
| Efield(e, field) ->
|
|
||||||
print_exp ff e; fprintf ff ".";
|
|
||||||
print_longname ff field
|
|
||||||
| Estruct(f_e_list) ->
|
| Estruct(f_e_list) ->
|
||||||
print_list_r
|
print_list_r
|
||||||
(fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
|
(fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
|
||||||
|
@ -116,6 +113,9 @@ and print_op ff op params e_list =
|
||||||
print_longname ff f;
|
print_longname ff f;
|
||||||
print_call_params ff params;
|
print_call_params ff params;
|
||||||
print_exps ff e_list
|
print_exps ff e_list
|
||||||
|
| Efield, [field], [e] ->
|
||||||
|
print_exp ff e; fprintf ff ".";
|
||||||
|
print_static_exp ff field
|
||||||
| Efield_update, [se], [e1;e2] ->
|
| Efield_update, [se], [e1;e2] ->
|
||||||
fprintf ff "(@[";
|
fprintf ff "(@[";
|
||||||
print_exp ff e1;
|
print_exp ff e1;
|
||||||
|
|
|
@ -30,7 +30,6 @@ and desc =
|
||||||
| Elast of var_ident
|
| Elast of var_ident
|
||||||
| Epre of static_exp option * exp
|
| Epre of static_exp option * exp
|
||||||
| Efby of exp * exp
|
| Efby of exp * exp
|
||||||
| Efield of exp * field_name
|
|
||||||
| Estruct of (field_name * exp) list
|
| Estruct of (field_name * exp) list
|
||||||
| Eapp of app * exp list * exp option
|
| Eapp of app * exp list * exp option
|
||||||
| Eiterator of iterator_type * app * static_exp * exp list * exp option
|
| Eiterator of iterator_type * app * static_exp * exp list * exp option
|
||||||
|
@ -43,6 +42,7 @@ and op =
|
||||||
| Enode of fun_name
|
| Enode of fun_name
|
||||||
| Eifthenelse
|
| Eifthenelse
|
||||||
| Earrow
|
| Earrow
|
||||||
|
| Efield
|
||||||
| Efield_update (* field name args would be [record ; value] *)
|
| Efield_update (* field name args would be [record ; value] *)
|
||||||
| Earray
|
| Earray
|
||||||
| Earray_fill
|
| Earray_fill
|
||||||
|
|
|
@ -446,8 +446,6 @@ exp:
|
||||||
{ mk_exp (mk_call Earrow [$1; $3]) }
|
{ mk_exp (mk_call Earrow [$1; $3]) }
|
||||||
| LAST IDENT
|
| LAST IDENT
|
||||||
{ mk_exp (Elast $2) }
|
{ mk_exp (Elast $2) }
|
||||||
| simple_exp DOT longname
|
|
||||||
{ mk_exp (Efield ($1, $3)) }
|
|
||||||
/*Array operations*/
|
/*Array operations*/
|
||||||
| exp POWER simple_exp
|
| exp POWER simple_exp
|
||||||
{ mk_exp (mk_call ~params:[$3] Earray_fill [$1]) }
|
{ mk_exp (mk_call ~params:[$3] Earray_fill [$1]) }
|
||||||
|
@ -468,9 +466,11 @@ exp:
|
||||||
RPAREN DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN
|
RPAREN DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN
|
||||||
{ mk_exp (mk_iterator_call $1 $3 $5 $9 $12) }
|
{ mk_exp (mk_iterator_call $1 $3 $5 $9 $12) }
|
||||||
/*Records operators */
|
/*Records operators */
|
||||||
| LBRACE e=simple_exp WITH DOT ln=longname EQUAL nv=exp RBRACE
|
| simple_exp DOT longname
|
||||||
{ let fn = mk_exp (Econst (mk_static_exp (Sconstructor ln))) in
|
{ mk_exp (mk_call ~params:[mk_constructor_exp $3] Efield [$1]) }
|
||||||
mk_exp (mk_call ~params:[fn] Efield_update [e; nv]) }
|
| LBRACE simple_exp WITH DOT longname EQUAL exp RBRACE
|
||||||
|
{ mk_exp (mk_call ~params:[mk_constructor_exp $5]
|
||||||
|
Efield_update [$2; $7]) }
|
||||||
;
|
;
|
||||||
|
|
||||||
call_params:
|
call_params:
|
||||||
|
|
|
@ -33,7 +33,6 @@ and desc =
|
||||||
| Elast of name
|
| Elast of name
|
||||||
| Epre of exp option * exp
|
| Epre of exp option * exp
|
||||||
| Efby of exp * exp
|
| Efby of exp * exp
|
||||||
| Efield of exp * longname
|
|
||||||
| Estruct of (longname * exp) list
|
| Estruct of (longname * exp) list
|
||||||
| Eapp of app * exp list
|
| Eapp of app * exp list
|
||||||
| Eiterator of iterator_type * app * exp * exp list
|
| Eiterator of iterator_type * app * exp * exp list
|
||||||
|
@ -46,6 +45,7 @@ and op =
|
||||||
| Efun of longname
|
| Efun of longname
|
||||||
| Eifthenelse
|
| Eifthenelse
|
||||||
| Earrow
|
| Earrow
|
||||||
|
| Efield
|
||||||
| Efield_update (* field name args would be [record ; value] *)
|
| Efield_update (* field name args would be [record ; value] *)
|
||||||
| Earray
|
| Earray
|
||||||
| Earray_fill
|
| Earray_fill
|
||||||
|
@ -183,6 +183,9 @@ let mk_op_call ?(params=[]) s exps =
|
||||||
let mk_iterator_call it ln params n exps =
|
let mk_iterator_call it ln params n exps =
|
||||||
Eiterator (it, mk_app (Enode ln) params, n, exps)
|
Eiterator (it, mk_app (Enode ln) params, n, exps)
|
||||||
|
|
||||||
|
let mk_constructor_exp f =
|
||||||
|
mk_exp (Econst (mk_static_exp (Sconstructor f)))
|
||||||
|
|
||||||
let mk_type_dec name desc =
|
let mk_type_dec name desc =
|
||||||
{ t_name = name; t_desc = desc; t_loc = Location.current_loc () }
|
{ t_name = name; t_desc = desc; t_loc = Location.current_loc () }
|
||||||
|
|
||||||
|
|
|
@ -169,7 +169,6 @@ and translate_desc loc const_env env = function
|
||||||
translate_exp const_env env e)
|
translate_exp const_env env e)
|
||||||
| Efby (e1, e2) -> Heptagon.Efby (translate_exp const_env env e1,
|
| Efby (e1, e2) -> Heptagon.Efby (translate_exp const_env env e1,
|
||||||
translate_exp const_env env e2)
|
translate_exp const_env env e2)
|
||||||
| Efield (e, field) -> Heptagon.Efield (translate_exp const_env env e, field)
|
|
||||||
| Estruct f_e_list ->
|
| Estruct f_e_list ->
|
||||||
let f_e_list =
|
let f_e_list =
|
||||||
List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in
|
List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in
|
||||||
|
@ -190,6 +189,7 @@ and translate_desc loc const_env env = function
|
||||||
and translate_op = function
|
and translate_op = function
|
||||||
| Earrow -> Heptagon.Earrow
|
| Earrow -> Heptagon.Earrow
|
||||||
| Eifthenelse -> Heptagon.Eifthenelse
|
| Eifthenelse -> Heptagon.Eifthenelse
|
||||||
|
| Efield -> Heptagon.Efield
|
||||||
| Efield_update -> Heptagon.Efield_update
|
| Efield_update -> Heptagon.Efield_update
|
||||||
| Etuple -> Heptagon.Etuple
|
| Etuple -> Heptagon.Etuple
|
||||||
| Earray -> Heptagon.Earray
|
| Earray -> Heptagon.Earray
|
||||||
|
|
|
@ -90,10 +90,6 @@ and translate v acc_eq_list e =
|
||||||
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
|
let v, acc_eq_list, e_list = translate_list v acc_eq_list e_list in
|
||||||
v, acc_eq_list,
|
v, acc_eq_list,
|
||||||
{ e with e_desc = Eiterator(it, op, n, e_list, r) }
|
{ e with e_desc = Eiterator(it, op, n, e_list, r) }
|
||||||
| Efield(e', field) ->
|
|
||||||
let v, acc_eq_list, e' = translate v acc_eq_list e' in
|
|
||||||
v,acc_eq_list,
|
|
||||||
{ e with e_desc = Efield(e', field) }
|
|
||||||
| Estruct(e_f_list) ->
|
| Estruct(e_f_list) ->
|
||||||
let v,acc_eq_list,e_f_list =
|
let v,acc_eq_list,e_f_list =
|
||||||
List.fold_left
|
List.fold_left
|
||||||
|
|
|
@ -60,8 +60,6 @@ and translate env e =
|
||||||
{ e with e_desc = Efby(translate env e1, translate env e2) }
|
{ e with e_desc = Efby(translate env e1, translate env e2) }
|
||||||
| Eapp(op, e_list, r) ->
|
| Eapp(op, e_list, r) ->
|
||||||
{ e with e_desc = Eapp(op, List.map (translate env) e_list, r) }
|
{ e with e_desc = Eapp(op, List.map (translate env) e_list, r) }
|
||||||
| Efield(e', field) ->
|
|
||||||
{ e with e_desc = Efield(translate env e', field) }
|
|
||||||
| Estruct(e_f_list) ->
|
| Estruct(e_f_list) ->
|
||||||
{ e with e_desc =
|
{ e with e_desc =
|
||||||
Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) }
|
Estruct(List.map (fun (f, e) -> (f, translate env e)) e_f_list) }
|
||||||
|
|
|
@ -248,8 +248,6 @@ and translate res e =
|
||||||
|
|
||||||
| Eapp(op, e_list, _) ->
|
| Eapp(op, e_list, _) ->
|
||||||
{ e with e_desc = Eapp(op, List.map (translate res) e_list, None) }
|
{ e with e_desc = Eapp(op, List.map (translate res) e_list, None) }
|
||||||
| Efield(e', field) ->
|
|
||||||
{ e with e_desc = Efield(translate res e', field) }
|
|
||||||
| Estruct(e_f_list) ->
|
| Estruct(e_f_list) ->
|
||||||
{ e with e_desc =
|
{ e with e_desc =
|
||||||
Estruct(List.map (fun (f, e) -> (f, translate res e)) e_f_list) }
|
Estruct(List.map (fun (f, e) -> (f, translate res e)) e_f_list) }
|
||||||
|
|
|
@ -196,6 +196,7 @@ let rec translate_op env = function
|
||||||
| Heptagon.Eifthenelse -> Eifthenelse
|
| Heptagon.Eifthenelse -> Eifthenelse
|
||||||
| Heptagon.Efun f -> Efun f
|
| Heptagon.Efun f -> Efun f
|
||||||
| Heptagon.Enode f -> Enode f
|
| Heptagon.Enode f -> Enode f
|
||||||
|
| Heptagon.Efield -> Efield
|
||||||
| Heptagon.Efield_update -> Efield_update
|
| Heptagon.Efield_update -> Efield_update
|
||||||
| Heptagon.Earray_fill -> Earray_fill
|
| Heptagon.Earray_fill -> Earray_fill
|
||||||
| Heptagon.Eselect -> Eselect
|
| Heptagon.Eselect -> Eselect
|
||||||
|
@ -226,8 +227,6 @@ let rec translate env
|
||||||
mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, translate env e))
|
mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, translate env e))
|
||||||
| Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
|
| Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
|
||||||
mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, translate env e))
|
mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, translate env e))
|
||||||
| Heptagon.Efield(e, field) ->
|
|
||||||
assert false (**TODO *)
|
|
||||||
| Heptagon.Estruct f_e_list ->
|
| Heptagon.Estruct f_e_list ->
|
||||||
let f_e_list = List.map
|
let f_e_list = List.map
|
||||||
(fun (f, e) -> (f, translate env e)) f_e_list in
|
(fun (f, e) -> (f, translate env e)) f_e_list in
|
||||||
|
|
Loading…
Reference in a new issue