Merge pull request #1111 from daniel-larraz/opaque-transparent

Add modifiers to control the opacity of a node/function

src/ivcMcs.ml

@@ -225,7 +225,7 @@ let rand_node name ts =
   |> List.map2 (fun t out -> dpos,HString.mk_hstring out,t,A.ClockTrue) ts
   in
   A.NodeDecl (dspan,
-    (name, true, [], [dpos,HString.mk_hstring "id",A.Int dpos,A.ClockTrue, false],
+    (name, true, Opaque, [], [dpos,HString.mk_hstring "id",A.Int dpos,A.ClockTrue, false],
     outs, [], [], None)
   )
 
@@ -413,7 +413,7 @@ let minimize_contract_node_eq ue lst cne =
   | A.AssumptionVars _ -> [cne]
 
 let minimize_node_decl ue loc_core
-  ((id, extern, tparams, inputs, outputs, locals, items, spec) as ndecl) =
+  ((id, extern, opac, tparams, inputs, outputs, locals, items, spec) as ndecl) =
 
   let id' = HString.string_of_hstring id in
   let id_typ_map = build_id_typ_map inputs outputs locals in
@@ -428,7 +428,7 @@ let minimize_node_decl ue loc_core
     end
     in
     let locals = List.map (minimize_node_local_decl ue lst) locals in
-    (id, extern, tparams, inputs, outputs, locals, items, spec)
+    (id, extern, opac, tparams, inputs, outputs, locals, items, spec)
   in
 
   let scope = (Scope.mk_scope [id']) in
@@ -471,7 +471,7 @@ let minimize_decl ue loc_core = function
   | decl -> decl 
 
 let fill_input_types_hashtbl ast =
-  let aux_node_decl (id, _, _, inputs, _, _, _, _) =
+  let aux_node_decl (id, _, _, _, inputs, _, _, _, _) =
     let typ_of_input (_,_,t,_,_) = t in
     Hashtbl.replace nodes_input_types id (List.map typ_of_input inputs) ;
   in

src/lustre/contractsToProps.ml

@@ -188,7 +188,7 @@ let rec fmt_declarations fmt = function
       " pp_print_position spos
       |> failwith
 
-    | Ast.NodeDecl (_, (wan, _, two,tri,far,fiv,six,contract)) -> (
+    | Ast.NodeDecl (_, (wan, _, _, two,tri,far,fiv,six,contract)) -> (
       let contract_info = match contract with
         | None -> ([],[],[],[])
         | Some (_, c) -> collect_contracts ([],[],[],[]) c

src/lustre/lspInfo.ml

@@ -73,7 +73,7 @@ let lsp_const_decl_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } =
         elnum ecnum
 
 let lsp_node_json ppf { Ast.start_pos = spos; Ast.end_pos = epos }
-    (id, imported, _, _, _, _, _, contract) = 
+    (id, imported, _, _, _, _, _, _, contract) =
   let file, slnum, scnum = Lib.file_row_col_of_pos spos in
   let _, elnum, ecnum = Lib.file_row_col_of_pos epos in
   match contract with 
@@ -113,7 +113,7 @@ let lsp_node_json ppf { Ast.start_pos = spos; Ast.end_pos = epos }
     elnum ecnum
 
 let lsp_function_json ppf { Ast.start_pos = spos; Ast.end_pos = epos }
-    (id, imported, _, _, _, _, _, _) =
+    (id, imported, _, _, _, _, _, _, _) =
   let file, slnum, scnum = Lib.file_row_col_of_pos spos in
   let _, elnum, ecnum = Lib.file_row_col_of_pos epos in
   Format.fprintf ppf

src/lustre/lustreAbstractInterpretation.ml

@@ -234,7 +234,7 @@ and interpret_contract_node ty_ctx (id, ps, ins, outs, contract) =
   let ty_ctx = TC.add_io_node_ctx ty_ctx id ps ins outs in
   interpret_contract id empty_context ty_ctx contract
 
-and interpret_node ty_ctx gids (id, _, ps, ins, outs, locals, items, contract) =
+and interpret_node ty_ctx gids (id, _, _, ps, ins, outs, locals, items, contract) =
   (* Setup the typing context *)
   let ty_ctx = TC.add_io_node_ctx ty_ctx id ps ins outs in
   let ctx = IMap.empty in

src/lustre/lustreArrayDependencies.ml

@@ -268,7 +268,7 @@ let rec check_inductive_array_dependencies ctx ns = function
   | [] -> Ok ()
 
 and check_node_decl ctx ns decl =
-  let (id, _, params, inputs, outputs, locals, items, _) = decl in
+  let (id, _, _, params, inputs, outputs, locals, items, _) = decl in
   (* Setup the typing context *)
   let ctx = Chk.add_full_node_ctx ctx id params inputs outputs locals in
   let* (graph, pos_map, count, idx_len) = process_items ctx ns items in

src/lustre/lustreAst.ml

@@ -274,13 +274,18 @@ type contract_node_equation =
 (* A contract is some ghost consts / var, and assumes guarantees and modes. *)
 type contract = position * (contract_node_equation list)
 
+type opacity =
+  | Default
+  | Opaque
+  | Transparent
 
 (* A node or function declaration
 
 Boolean flag indicates whether node / function is extern. *)
 type node_decl =
   ident
   * bool
+  * opacity
   * ident list
   * const_clocked_typed_decl list
   * clocked_typed_decl list
@@ -1146,17 +1151,22 @@ let pp_print_contract_node_decl ppf (n,p,i,o,(_,e))
 
 
 let pp_print_node_or_fun_decl is_fun ppf (
-  _, (n, ext, p, i, o, l, e, r)
+  _, (n, ext, opac, p, i, o, l, e, r)
 ) =
     if e = [] then
       Format.fprintf ppf
-        "@[<hv>@[<hv 2>%s%s %a%t@ \
+        "@[<hv>@[<hv 2>%s%s%s %a%t@ \
         @[<hv 1>(%a)@]@;<1 -2>\
         returns@ @[<hv 1>(%a)@];@]@.\
         %a@?\
         %a@?@]@?"
         (if is_fun then "function" else "node")
         (if ext then " imported" else "")
+        (match opac with
+         | Default -> ""
+         | Opaque -> "opaque "
+         | Transparent -> "transparent "
+        )
         pp_print_ident n 
         (function ppf -> pp_print_node_param_list ppf p)
         (pp_print_list pp_print_const_clocked_typed_ident ";@ ") i

src/lustre/lustreAst.mli

@@ -285,10 +285,16 @@ type contract = position * (contract_node_equation list)
   (*   contract_mode list * contract_call list *)
   (* ) list *)
 
+type opacity =
+  | Default
+  | Opaque
+  | Transparent
+
 (** Declaration of a node or function as a tuple of
 
     - its identifier,
     - a flag, true if the node / function is extern
+    - its opacity
     - its type parameters,
     - the list of its inputs,
     - the list of its outputs,
@@ -298,6 +304,7 @@ type contract = position * (contract_node_equation list)
 type node_decl =
   ident
   * bool
+  * opacity
   * ident list
   * const_clocked_typed_decl list
   * clocked_typed_decl list

src/lustre/lustreAstDependencies.ml

@@ -521,7 +521,7 @@ and extract_node_calls: LA.node_item list -> (LA.ident * Lib.position) list
 = fun l -> List.fold_left (fun acc i -> extract_node_calls_item i @ acc) [] l
 
 let mk_graph_node_decl: Lib.position -> LA.node_decl -> dependency_analysis_data
-  = fun pos (i, _, _, ips, ops, locals, nitems, contract_opt) ->    
+  = fun pos (i, _, _, _, ips, ops, locals, nitems, contract_opt) ->
   let cg = connect_g_pos
              (match contract_opt with
               | None -> empty_dependency_analysis_data
@@ -580,8 +580,8 @@ let rec  mk_decl_map: LA.declaration option IMap.t -> LA.t -> ((LA.declaration o
     let* m' = check_and_add m pos const_prefix i (Some cnstd)  in
     mk_decl_map m' decls 
 
-  | (LA.NodeDecl (span, (i, _, _, _, _, _, _, _)) as ndecl) :: decls
-  | (LA.FuncDecl (span, (i, _, _, _, _, _, _, _)) as ndecl) :: decls ->
+  | (LA.NodeDecl (span, (i, _, _, _, _, _, _, _, _)) as ndecl) :: decls
+  | (LA.FuncDecl (span, (i, _, _, _, _, _, _, _, _)) as ndecl) :: decls ->
     let {LA.start_pos = pos} = span in
     let* m' = check_and_add m pos node_prefix i (Some ndecl) in
     mk_decl_map m' decls
@@ -1152,7 +1152,7 @@ let summarize_ip_vars: LA.ident list -> SI.t -> int list = fun ips critial_ips -
 (** Helper function to generate a node summary *)
 
 let mk_node_summary: bool -> node_summary -> LA.node_decl -> node_summary
-    = fun connect_imported s (i, imported, _, ips, ops, _, items, _) ->
+    = fun connect_imported s (i, imported, _, _, ips, ops, _, items, _) ->
   if not imported
   then 
     let op_vars = List.map (fun o -> LH.extract_op_ty o |> fst) ops in
@@ -1345,7 +1345,7 @@ let check_no_input_output_local_duplicate ips ops locals =
 let check_node_equations: dependency_analysis_data
                           -> LA.node_decl
                           -> (LA.node_decl, [> error]) result
-  = fun ad ((i, imported, params, ips, ops, locals, items, contract_opt) as ndecl)->
+  = fun ad ((i, imported, opac, params, ips, ops, locals, items, contract_opt) as ndecl)->
   (if not imported then
     let* _ = check_no_input_output_local_duplicate ips ops locals in
     analyze_circ_node_equations ad.nsummary2 items >> 
@@ -1357,7 +1357,7 @@ let check_node_equations: dependency_analysis_data
       let* (_, _, _, _, c') = sort_and_check_contract_eqns ad
         (HString.concat (HString.mk_hstring "inline$") [contract_prefix;i], params, ips, ops, c)
       in
-      R.ok (i, imported, params, ips, ops, locals, items, Some c')
+      R.ok (i, imported, opac, params, ips, ops, locals, items, Some c')
 (** Check if node equations do not have circularity and also, if the node has a contract
     sort the contract equations. *)
 

src/lustre/lustreAstHelpers.ml

@@ -1226,7 +1226,7 @@ let get_last_node_name: declaration list -> ident option
   let rec get_first_node_name: declaration list -> ident option =
     function
     | [] -> None
-    | NodeDecl (_, (n, _, _, _, _, _, _, _)) :: _ -> Some n
+    | NodeDecl (_, (n, _, _, _, _, _, _, _, _)) :: _ -> Some n
     | _ :: rest -> get_first_node_name rest
   in get_first_node_name (List.rev ds)   
 
@@ -1238,7 +1238,7 @@ let rec remove_node_in_declarations:
   fun n pres ->
   function
   | [] -> None
-  | (NodeDecl (_, (n', _, _, _, _, _, _, _)) as mn) :: rest ->
+  | (NodeDecl (_, (n', _, _, _, _, _, _, _, _)) as mn) :: rest ->
      if HString.compare n' n = 0
      then Some (mn, pres @ rest)
      else remove_node_in_declarations n (pres @ [mn]) rest 

src/lustre/lustreAstInlineConstants.ml

@@ -515,7 +515,7 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati
     let e' = simplify_expr ctx e in
     let ctx' = TC.add_ty (TC.add_const ctx i e' ty' Global) i ty' in
     (ctx', ConstDecl (span, TypedConst (pos', i, e', ty')))
-  | (LA.NodeDecl (span, (i, imported, params, ips, ops, ldecls, items, contract))) ->
+  | (LA.NodeDecl (span, (i, imported, opac, params, ips, ops, ldecls, items, contract))) ->
     let ips' = inline_constants_of_const_clocked_type_decl ctx ips in
     let ops' = inline_constants_of_clocked_type_decl ctx ops in
     let contract' = match contract with
@@ -524,8 +524,8 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati
     in
     let ctx', ldecls' = inline_constants_of_node_locals ctx ldecls in
     let items' = inline_constants_of_node_items ctx' items in
-     ctx, (LA.NodeDecl (span, (i, imported, params, ips', ops', ldecls', items', contract')))
-  | (LA.FuncDecl (span, (i, imported, params, ips, ops, ldecls, items, contract))) ->
+     ctx, (LA.NodeDecl (span, (i, imported, opac, params, ips', ops', ldecls', items', contract')))
+  | (LA.FuncDecl (span, (i, imported, opac, params, ips, ops, ldecls, items, contract))) ->
     let ips' = inline_constants_of_const_clocked_type_decl ctx ips in
     let ops' = inline_constants_of_clocked_type_decl ctx ops in
     let contract' = match contract with
@@ -534,7 +534,7 @@ let substitute: TC.tc_context -> LA.declaration -> (TC.tc_context * LA.declarati
     in
     let ctx', ldecls' = inline_constants_of_node_locals ctx ldecls in
     let items' = inline_constants_of_node_items ctx' items in
-     ctx, (LA.FuncDecl (span, (i, imported, params, ips', ops', ldecls', items', contract')))
+     ctx, (LA.FuncDecl (span, (i, imported, opac, params, ips', ops', ldecls', items', contract')))
   | (LA.ContractNodeDecl (span, (i, params, ips, ops, (p, contract)))) ->
      ctx, (LA.ContractNodeDecl (span, (i, params, ips, ops, (p, inline_constants_of_contract ctx contract))))
   | e -> (ctx, e)

src/lustre/lustreAstNormalizer.ml

@@ -296,10 +296,10 @@ let pp_print_generated_identifiers ppf gids =
 
 let compute_node_input_constant_mask decls =
   let over_decl map = function
-  | A.NodeDecl (_, (id, _, _, inputs, _, _, _, _)) ->
+  | A.NodeDecl (_, (id, _, _, _, inputs, _, _, _, _)) ->
     let is_consts = List.map (fun (_, _, _, _, c) -> c) inputs in
     StringMap.add id is_consts map
-  | FuncDecl (_, (id, _, _, inputs, _, _, _, _)) ->
+  | FuncDecl (_, (id, _, _, _, inputs, _, _, _, _)) ->
     let is_consts = List.map (fun (_, _, _, _, c) -> c) inputs in
     StringMap.add id is_consts map
   | _ -> map
@@ -1134,7 +1134,7 @@ and normalize_ghost_declaration info node_id map = function
     FreeConst (pos, id, ty), map, warnings
 
 and normalize_node info map
-    (node_id, is_extern, params, inputs, outputs, locals, items, contract) =
+    (node_id, is_extern, opac, params, inputs, outputs, locals, items, contract) =
   (* Setup the typing context *)
   let ctx = Chk.add_io_node_ctx info.context node_id params inputs outputs in
   let ctx = Ctx.add_ty ctx ctr_id (A.Int dpos) in
@@ -1250,7 +1250,7 @@ and normalize_node info map
                              gids4; gids5; gids7; gids6_8; gids9; gids10] in
   let old_gids, warnings6 = normalize_gid_equations info map node_id in
   let map = StringMap.add node_id (union old_gids new_gids) map in
-  (node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts),
+  (node_id, is_extern, opac, params, inputs, outputs, locals, List.flatten nitems, ncontracts),
   map, 
   List.flatten warnings1 @ List.flatten warnings2 @ List.flatten warnings3 @ warnings4 @ warnings5 @ warnings6
 

src/lustre/lustreDeclarations.ml

@@ -2105,7 +2105,7 @@ and declaration_to_context ctx = function
 
 (* Function declaration without parameters *)
 | A.FuncDecl (
-  {A.start_pos = pos}, (i, ext, [], inputs, outputs, locals, items, contracts)
+  {A.start_pos = pos}, (i, ext, _, [], inputs, outputs, locals, items, contracts)
 ) -> (
 
   (* Identifier of AST identifier *)
@@ -2185,7 +2185,7 @@ and declaration_to_context ctx = function
 
 (* Node declaration without parameters *)
 | A.NodeDecl (
-  {A.start_pos = pos}, (i, ext, [], inputs, outputs, locals, items, contracts)
+  {A.start_pos = pos}, (i, ext, _, [], inputs, outputs, locals, items, contracts)
 ) -> (
 
   (* Identifier of AST identifier *)

src/lustre/lustreDependencies.ml

@@ -125,9 +125,9 @@ let info_of_decl = function
 | A.ConstDecl ({A.start_pos=pos}, A.TypedConst(_, ident, _, _)) ->
   pos, ident |> HString.string_of_hstring |> I.mk_string_ident, Const
 
-| A.NodeDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _)) ->
+| A.NodeDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _, _)) ->
   pos, ident |> HString.string_of_hstring |> I.mk_string_ident, NodeOrFun
-| A.FuncDecl ({A.start_pos=pos}, (ident, _, _, _, _, _, _, _)) ->
+| A.FuncDecl ({A.start_pos=pos}, (ident, _,  _, _, _, _, _, _, _)) ->
   pos, ident |> HString.string_of_hstring |> I.mk_string_ident, NodeOrFun
 
 | A.ContractNodeDecl ({A.start_pos=pos}, (ident, _, _, _, _)) ->
@@ -146,8 +146,8 @@ let insert_decl decl (f_type, f_ident) decls =
   let has_ident = match f_type with
     | NodeOrFun -> (
       function
-      | A.NodeDecl (_, (i, _, _, _, _, _, _, _)) -> i = ident
-      | A.FuncDecl (_, (i, _, _, _, _, _, _, _)) -> i = ident
+      | A.NodeDecl (_, (i, _, _, _, _, _, _, _, _)) -> i = ident
+      | A.FuncDecl (_, (i, _, _, _, _, _, _, _, _)) -> i = ident
       | _ -> false
     )
     | Type -> (

src/lustre/lustreDesugarAnyOps.ml

@@ -97,11 +97,11 @@ fun ctx node_name fun_ids expr ->
     let generated_node = 
       if has_pre_arrow_or_node_call then
         A.NodeDecl (span, 
-        (name, true, ty_params, inputs, 
+        (name, true, A.Opaque, ty_params, inputs,
         [pos, id, ty, A.ClockTrue], [], [], Some (pos, contract))) 
       else 
         A.FuncDecl (span, 
-        (name, true, ty_params, inputs, 
+        (name, true, A.Opaque, ty_params, inputs,
         [pos, id, ty, A.ClockTrue], [], [], Some (pos, contract)))  
     in
     A.Call(pos, ty_vars, name, inputs_call), [generated_node]
@@ -263,24 +263,24 @@ fun ctx node_name fun_ids ni ->
 let desugar_any_ops: Ctx.tc_context -> A.declaration list -> A.declaration list = 
 fun ctx decls -> 
   let fun_ids = List.filter_map 
-    (fun decl -> match decl with | A.FuncDecl (_, (id, _, _, _, _, _, _, _)) -> Some id | _ -> None) 
+    (fun decl -> match decl with | A.FuncDecl (_, (id, _, _, _, _, _, _, _, _)) -> Some id | _ -> None)
     decls 
   in
   let decls =
   List.fold_left (fun decls decl ->
     match decl with
-    | A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract)) -> 
+    | A.NodeDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract)) ->
       let ctx = Chk.add_full_node_ctx ctx id params inputs outputs locals in
       let items, gen_nodes = List.map (desugar_node_item ctx id fun_ids) items |> List.split in 
       let contract, gen_nodes2 = desugar_contract ctx id fun_ids contract in
       let gen_nodes = List.flatten gen_nodes in
-      decls @ gen_nodes @ gen_nodes2 @ [A.NodeDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))]
-    | A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract)) -> 
+      decls @ gen_nodes @ gen_nodes2 @ [A.NodeDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract))]
+    | A.FuncDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract)) ->
       let ctx = Chk.add_full_node_ctx ctx id params inputs outputs locals in
       let items, gen_nodes = List.map (desugar_node_item ctx id fun_ids) items |> List.split in 
       let contract, gen_nodes2 = desugar_contract ctx id fun_ids contract in
       let gen_nodes = List.flatten gen_nodes in
-      decls @ gen_nodes @ gen_nodes2 @ [A.FuncDecl (span, (id, ext, params, inputs, outputs, locals, items, contract))]
+      decls @ gen_nodes @ gen_nodes2 @ [A.FuncDecl (span, (id, ext, opac, params, inputs, outputs, locals, items, contract))]
     | A.ContractNodeDecl (span, (id, params, inputs, outputs, contract)) ->
       let ctx = Chk.add_io_node_ctx ctx id params inputs outputs in
       let contract, gen_nodes = desugar_contract ctx id fun_ids (Some contract) in

src/lustre/lustreDesugarFrameBlocks.ml

@@ -339,15 +339,15 @@ let desugar_node_item node_id ni = match ni with
 let desugar_frame_blocks sorted_node_contract_decls = 
   HString.HStringHashtbl.clear pos_list_map ;
   let desugar_node_decl decl = (match decl with
-    | A.NodeDecl (s, ((node_id, b, nps, cctds, ctds, nlds, nis2, co))) -> 
+    | A.NodeDecl (s, ((node_id, b, o, nps, cctds, ctds, nlds, nis2, co))) ->
       let* res = R.seq (List.map (desugar_node_item node_id) nis2) in
       let decls, nis, warnings = split3 res in
       let warnings = List.flatten warnings in 
-      R.ok (A.NodeDecl (s, (node_id, b, nps, cctds, ctds, 
+      R.ok (A.NodeDecl (s, (node_id, b, o, nps, cctds, ctds,
                        (List.flatten decls) @ nlds, List.flatten nis, co)), warnings) 
 
     (* Make sure there are no frame blocks in functions *)
-    | A.FuncDecl (_, ((_, _, _, _, _, _, nis, _))) -> (
+    | A.FuncDecl (_, ((_, _, _, _, _, _, _, nis, _))) -> (
       let contains_frame_block = List.find_opt (fun ni -> match ni with | A.FrameBlock _ -> true | _ -> false) nis in
       match contains_frame_block with
         | Some (FrameBlock (pos, _, _, _) as fb) -> mk_error pos (MisplacedFrameBlockError fb)