let modes_of sys = (* Retrieving top modes. *) let top = modes_of_sys sys in (* Retrieving subsystems' modes. *) (* let subs = Sys.get_subsystems sys |> List.fold_left (fun subs subsys -> match modes_of_sys subsys with | None, [] -> subs (* No contract, ignoring. We might want to go down the hierarchy in this case. *) | global, modes -> (* Subsystem has contracts, instantiating. *) (* Builds the list of instantiated modes for each call to [subsys] in [sys]. Accum is an option of a list the length of which is the number of calls to [subsys] in [sys]. *) let rec instantiate_modes accum = function | (name,term) :: tail -> let instantiated = Sys.instantiate_terms_for_sys subsys [term] sys |> List.map (function (* Building a list so that everything works fine if [accum = None]. *) | [term] -> [ name, term ] | _ -> failwith "unreachable 2" ) in instantiate_modes ( Some ( match accum with | None -> instantiated | Some modes -> (* Doing a [map2] so that instantiations match. *) modes |> List.map2 (fun l l' -> l @ l') instantiated ) ) tail | [] -> ( match accum with | Some res -> res | None -> [] ) in let instantiated_modes = instantiate_modes None modes in ( subsys, match global, instantiated_modes with (* No global, adding node to each instantiation. *) | None, _ -> instantiated_modes |> List.map (fun ms -> None, ms) (* Global mode, instantiating. *) | Some (name, term), [] -> Sys.instantiate_terms_for_sys subsys [term] sys |> List.map (function | [ term ] -> Some (name, term), [] | _ -> failwith "unreachable 3" ) | Some (name, term), _ -> Sys.instantiate_terms_for_sys subsys [term] sys (* [map2] with instantiated modes. *) |> List.map2 (fun modes -> function | [ term ] -> Some (name, term), modes | _ -> failwith "unreachable 4" ) instantiated_modes ) :: subs ) [] in *) top, []