Introducing a hack to normalize comparison of tuples in Heptagon.

This commit is contained in:
Nicolas Berthier 2014-12-15 15:42:37 +01:00
parent 045e624f94
commit c86d7af0b1
3 changed files with 16 additions and 3 deletions

View file

@ -207,8 +207,8 @@ and typing_app h base pat op e_list = match op with
| None -> build_env a_l v_l env
| Some n -> build_env a_l v_l ((n,v)::env))
| _ ->
Printf.printf "Fun/node : %s\n" (Names.fullname f);
Misc.internal_error "Clocking, non matching signature"
Misc.internal_error ("Clocking, non matching signature in call of "^
Names.fullname f);
in
let env_pat = build_env node.node_outputs pat_id_list [] in
let env_args = build_env node.node_inputs e_list [] in

View file

@ -175,6 +175,18 @@ let rec translate kind context e =
merge context e n tag_e_list
| Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) ->
ifthenelse context e e1 e2 e3
(* XXX Huge hack to avoid comparing tuples... (temporary, until this is
fixed where it should be) *)
| Eapp({ a_op = (Efun ({ Names.qual = Names.Pervasives; Names.name = "=" }) as op)},
[x;y], reset) when is_list x ->
let x = e_to_e_list x and y = e_to_e_list y in
let xy = List.fold_left2 (fun acc x y ->
let cmp = mk_exp (mk_op_app op [x; y] ~reset) Initial.tbool ~linearity:Ltop in
mk_exp (mk_op_app (Efun Initial.pand) [acc; cmp] ~reset) Initial.tbool ~linearity:Ltop)
dtrue
x y
in
translate kind context xy
| Eapp(app, e_list, r) ->
let context, e_list = translate_list ExtValue context e_list in
context, { e with e_desc = Eapp(app, flatten_e_list e_list, r) }

View file

@ -137,7 +137,8 @@ let typing_app h base pat op w_list = match op with
| a::a_l, v::v_l -> (match a.a_name with
| None -> build_env a_l v_l env
| Some n -> build_env a_l v_l ((n,v)::env))
| _ -> Misc.internal_error "Clocking, non matching signature"
| _ -> Misc.internal_error ("Clocking, non matching signature in call of " ^
Names.fullname f)
in
let env_pat = build_env node.node_outputs pat_id_list [] in
let env_args = build_env node.node_inputs w_list [] in