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/tools/dune_rule_gen/ (Beweissystem des Inria Version 9.1.0^©) Datei vom 15.8.2025 mit Größe 1 kB

Quelle path.ml Sprache: SML

(************************************************************************)
(* This file is licensed under The MIT License                          *)
(* See LICENSE for more information                                     *)
(************************************************************************)

(* We distinguish Path arguments as to adjust for subdirs in Coq
   theory evaluation *)

type t = Rel of string | Abs of string

let to_string = function Rel p -> p | Abs p -> p

(* paths which begin with a dune variable are considered absolute
   (eg %{project_root}/bla) *)
let is_relative path =
  not (CString.is_prefix "%{" path) && Filename.is_relative path

let make path = if is_relative path then Rel path else Abs path

let map ~f = function Rel p -> Rel (f p) | Abs p -> Abs (f p)

let fold ~f = function Rel p -> f p | Abs p -> f p

let relative dir path = map dir ~f:(fun dir -> Filename.concat dir path)

let gen_sub n = String.concat Filename.dir_sep @@ List.init n (fun _ -> "..")

let adjust ~lvl = function
  | Rel path -> Rel (Filename.concat (gen_sub lvl) path)
  | Abs path -> Abs path

let compare p1 p2 = match p1, p2 with
  | Rel p1, Rel p2 -> String.compare p1 p2
  | Abs p1, Abs p2 -> String.compare p1 p2
  | Rel _, Abs _ -> -1
  | Abs _, Rel _ -> 1

let pp fmt = function
  | Rel p -> Format.fprintf fmt "%s" p
  | Abs p -> Format.fprintf fmt "%s" p

let basename = fold ~f:Filename.basename

let add_extension ~ext = map ~f:(fun p -> p ^ ext)

let replace_ext ~ext = map ~f:(fun p -> Filename.remove_extension p ^ ext)

(* Coqdep strips files with dirname "." of the basename, so we need
   to fixup that until we can fix coqdep... [fixing coqdep breaks dune] *)
let coqdep_fixup_dir = function
  | Abs file -> Abs file
  | Rel file ->
    match Filename.dirname file with
    | "." -> Rel (Filename.basename file)
    | _ -> Rel file

quality94%

¤ Dauer der Verarbeitung: 0.16 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.