Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Roqc/vernac/ (Beweissystem des Inria Version 9.1.0^©) Datei vom 15.8.2025 mit Größe 10 kB

Quelle vernacControl.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type 'e profile_state_gen = {
  events : 'e;
  sums : NewProfile.sums;
  counters : NewProfile.Counters.t;
}

type profile_state = NewProfile.MiniJson.t list list profile_state_gen

let empty_profstate = {
  events = [];
  sums = NewProfile.empty_sums;
  counters = NewProfile.Counters.zero;
}

(** Partially interpreted control flags.

    [ControlTime {duration}] means "Time" where the
    partial interpretation has already take [duration].

    In [ControlRedirect], [truncate] tells whether we should truncate
    the file before printing (ie [false] if not the first phase).
    Alternatively we could do [ControlRedirect of out_channel],
    but that risks leaking open channels.

    [ControlFail {st}] means "Fail" where the partial interpretation
    did not fail and produced state [st].

    [ControlSucceed {st}] means "Succeed" where the partial
    interpretation succeeded and produced state [st].
*)
type 'state control_entry =
  | ControlTime of { duration: System.duration }
  | ControlInstructions of { instructions: System.instruction_count }
  | ControlProfile of { to_file : string option; profstate : profile_state }
  | ControlRedirect of { fname : string; truncate : bool}
  | ControlTimeout of { remaining : float }
  | ControlFail of { st : 'state }
  | ControlSucceed of { st : 'state }

type 'state control_entries = 'state control_entry list

let check_timeout_f n =
  if n <= 0. then CErrors.user_err Pp.(str "Timeout must be > 0.")

let with_measure measure add fmt flag init f =
  let result = measure f () in
  let result = match result with
    | Ok (v,d) -> Ok (v, add init d)
    | Error (e,d) -> Error (e, add init d)
  in
  begin match result with
  | Ok (v,result) -> Some (flag result, v)
  | Error (e,_) ->
    Feedback.msg_notice @@ fmt result;
    Exninfo.iraise e
  end

let measure_profile f () =
  let start_cnt = NewProfile.Counters.get() in
  let events, sums, v = NewProfile.with_profiling (fun () ->
      try Ok (f ())
      with e -> Error (Exninfo.capture e))
  in
  let counters = NewProfile.Counters.(get() - start_cnt) in
  let prof = { events=events; sums; counters } in
  match v with
  | Ok v -> Ok (v,prof)
  | Error e -> Error (e, prof)

let add_profile a b = {
  events = if CList.is_empty b.events then a.events else b.events :: a.events;
  sums = NewProfile.sums_union a.sums b.sums;
  counters = NewProfile.Counters.(a.counters + b.counters);
}

let fmt_profiling counters (sums:NewProfile.sums) =
  let open Pp in
  let sums = CString.Map.bindings sums in
  let sums = List.sort (fun (_,(t1,_)) (_,(t2,_)) -> Float.compare t2 t1) sums in
  let longest = List.fold_left (fun longest (name,_) -> max longest (String.length name)) 0 sums in
  let pr_one (name,(time,cnt)) =
    hov 1
      (str name ++ str ":" ++ brk (1 + longest - String.length name, 0) ++
       str (Format.asprintf "%a" NewProfile.pptime time) ++
       pr_comma () ++ int cnt ++ str " calls")
  in
  v 0 (
  NewProfile.Counters.print counters ++ spc() ++ spc() ++
  prlist_with_sep spc pr_one sums)

(* Output comma and newline separated events given as a list of nonempty lists.
   The last event is not followed by a comma. *)
let rec output_events fmt = function
  | [] -> ()
  | [[last]] -> Format.fprintf fmt "%a\n" NewProfile.MiniJson.pr last
  | [] :: rest -> assert false
  | (current :: next) :: rest ->
    Format.fprintf fmt "%a,\n" NewProfile.MiniJson.pr current;
    match next with
    | [] -> output_events fmt rest
    | _::_ -> output_events fmt (next :: rest)

let fmt_profile to_file v =
  let {events;sums;counters} = match v with
    | Ok (_,x) -> x
    | Error (_,x) -> x
  in
  to_file |> Option.iter (fun to_file ->
      let to_file = System.get_output_path (to_file ^ ".json") in
      let f = open_out to_file in
      let fmt = Format.formatter_of_out_channel f in
      NewProfile.format_header fmt;
      output_events fmt events;
      NewProfile.format_footer fmt;
      close_out f
    );
  fmt_profiling counters sums

let with_timeout ~timeout:n f =
  check_timeout_f n;
  let start = Unix.gettimeofday () in
  begin match Control.timeout n f () with
  | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
  | Some v ->
    let stop = Unix.gettimeofday () in
    let remaining = n -. (stop -. start) in
    if remaining <= 0. then Exninfo.iraise (Exninfo.capture CErrors.Timeout)
    else Some (ControlTimeout { remaining }, v)
  end

let real_error_loc ~cmdloc ~eloc =
  if Loc.finer eloc cmdloc then eloc
  else cmdloc

(* Restoring the state is the caller's responsibility *)
let with_fail f : (Loc.t option * Pp.t, 'a) result =
  try
    let x = f () in
    Error x
  with
  (* Fail Timeout is a common pattern so we need to support it. *)
  | e ->
    (* The error has to be printed in the failing state *)
    let _, info as exn = Exninfo.capture e in
    if CErrors.is_anomaly e && e != CErrors.Timeout then Exninfo.iraise exn;
    Ok (Loc.get_loc info, CErrors.iprint exn)

type ('st0,'st) with_local_state = { with_local_state : 'a. 'st0 -> (unit -> 'a) -> 'st * 'a }

let trivial_state = { with_local_state = fun () f -> (), f () }

let with_fail ~loc ~with_local_state st0 f =
  let transient_st, res = with_local_state.with_local_state st0 (fun () -> with_fail f) in
  match res with
  | Error v ->
    Some (ControlFail { st = transient_st }, v)
  | Ok (eloc, msg) ->
    let loc = if !Flags.test_mode then real_error_loc ~cmdloc:loc ~eloc else None in
    if not !Flags.quiet || !Flags.test_mode
    then Feedback.msg_notice ?loc Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg);
    None

let with_succeed ~with_local_state st0 f =
  let transient_st, v = with_local_state.with_local_state st0 f in
  Some (ControlSucceed { st = transient_st }, v)

let under_one_control ~loc ~with_local_state control f =
  match control with
  | ControlTime { duration } ->
    with_measure System.measure_duration System.duration_add System.fmt_transaction_result
      (fun duration -> ControlTime {duration})
      duration
      f
  | ControlInstructions {instructions} ->
    with_measure System.count_instructions System.instruction_count_add System.fmt_instructions_result
      (fun instructions -> ControlInstructions {instructions})
      instructions
      f
  | ControlProfile {to_file; profstate} ->
    with_measure measure_profile add_profile (fun v -> fmt_profile to_file v)
      (fun profstate -> ControlProfile {to_file; profstate})
      profstate
      f
  | ControlRedirect { fname; truncate } ->
    let v = Topfmt.with_output_to_file ~truncate fname f () in
    Some (ControlRedirect {fname; truncate=false}, v)
  | ControlTimeout {remaining} -> with_timeout ~timeout:remaining f
  | ControlFail {st} -> with_fail ~loc ~with_local_state st f
  | ControlSucceed {st} -> with_succeed ~with_local_state st f

let rec under_control ~loc ~with_local_state controls ~noop f =
  match controls with
  | [] -> [], f ()
  | control :: rest ->
    let f () = under_control ~loc ~with_local_state rest ~noop f in
    match under_one_control ~loc ~with_local_state control f with
    | Some (control, (rest,v)) -> control :: rest, v
    | None -> [], noop

let ignore_state = { with_local_state = fun _ f -> (), f () }

let rec after_last_phase ~loc = function
  | [] -> false
  | control :: rest ->
    (* don't match on [control] before processing [rest]: correctly handle eg [Fail Fail]. *)
    let rest () = after_last_phase ~loc rest in
    match under_one_control ~loc ~with_local_state:ignore_state control rest with
    | None -> true
    | Some (control,noop) ->
      match control with
      | ControlTime {duration} ->
        Feedback.msg_notice @@ System.fmt_transaction_result (Ok ((),duration));
        noop
      | ControlInstructions {instructions} ->
        Feedback.msg_notice @@ System.fmt_instructions_result (Ok ((),instructions));
        noop
      | ControlProfile {to_file; profstate} ->
        Feedback.msg_notice @@ fmt_profile to_file (Ok ((),profstate));
        noop
      | ControlRedirect _ -> noop
      | ControlTimeout _ -> noop
      | ControlFail _ -> CErrors.user_err Pp.(str "The command has not failed!")
      | ControlSucceed _ -> true

(** A global default timeout, controlled by option "Set Default Timeout n".
    Use "Unset Default Timeout" to deactivate it. *)

let default_timeout = ref None

let check_timeout n =
  if n <= 0 then CErrors.user_err Pp.(str "Timeout must be > 0.")

let () = let open Goptions in
  declare_int_option
    { optstage = Summary.Stage.Synterp;
      optdepr  = None;
      optkey   = ["Default";"Timeout"];
      optread  = (fun () -> !default_timeout);
      optwrite = (fun n -> Option.iter check_timeout n; default_timeout := n) }

let has_timeout ctrl = ctrl |> List.exists (function
    | Vernacexpr.ControlTimeout _ -> true
    | _ -> false)

let add_default_timeout control =
  match !default_timeout with
  | None -> control
  | Some n ->
    if has_timeout control then control
    else Vernacexpr.ControlTimeout n :: control

let from_syntax_one : Vernacexpr.control_flag -> unit control_entry = function
  | ControlTime -> ControlTime { duration = System.empty_duration }
  | ControlInstructions -> ControlInstructions { instructions = Ok 0L }
  | ControlProfile to_file -> ControlProfile {to_file; profstate = empty_profstate}
  | ControlRedirect s -> ControlRedirect { fname = s; truncate = true }
  | ControlTimeout timeout ->
    (* don't check_timeout here as the error won't be caught by surrounding Fail *)
    ControlTimeout { remaining = float_of_int timeout }
  | ControlFail -> ControlFail { st = () }
  | ControlSucceed -> ControlSucceed { st = () }

let from_syntax control = List.map from_syntax_one (add_default_timeout control)

quality98%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.