diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index 4eb9825..ba7b00d 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -528,6 +528,10 @@ let gen_ctrlf_calls ~requal_types gd node_name equs = contract. *) let translate_node ~requal_types typdefs = function | ({ n_contract = None } as node) -> node, None + | ({ n_name; n_params } as node) when n_params <> [] -> + warn "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \ + contract@ into@ Controllable-Nbac!" (Names.fullname n_name); + node, None | ({ n_name; n_input; n_output; n_local; n_equs; n_contract = Some contr } as node) -> diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 41ca676..12d1e82 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -522,12 +522,17 @@ let translate_node let program p = let acc_proc, acc_p_desc = List.fold_left - (fun (acc_proc,acc_p_desc) p_desc -> - match p_desc with - | Minils.Pnode(node) -> - let (node,proc) = translate_node node in - (proc::acc_proc),((Minils.Pnode(node))::acc_p_desc) - | p -> (acc_proc,p::acc_p_desc)) + (fun (acc_proc,acc_p_desc) -> function + | Minils.Pnode(node) as p when node.Minils.n_contract = None -> + (acc_proc,p::acc_p_desc) + | Minils.Pnode(node) as p when node.Minils.n_params <> [] -> + warn "Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \ + contract@ into@ Z/3Z!" (Names.fullname node.Minils.n_name); + (acc_proc,p::acc_p_desc) + | Minils.Pnode(node) -> + let (node,proc) = translate_node node in + (proc::acc_proc),((Minils.Pnode(node))::acc_p_desc) + | p -> (acc_proc,p::acc_p_desc)) ([],[]) p.Minils.p_desc in let procs = List.rev acc_proc in