Path

Imports
open Array;
Table of Contents

Types

Path

(type)
type Path

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Path (opaque · mk*)

mk

Builds a Path from a non-empty string.
def mk (s : String | s ≠ "") : Path

Functions

pathlib

def pathlib : Unit

shutil

def shutil : Unit

mk

Builds a Path from a non-empty string.
def mk (s : String | s ≠ "") : Path

cwd

Returns the current working directory. Thunked so each call returns the cwd at call time (which can change after os.chdir).
def cwd (_ : Unit) : Path

home

Returns the current user's home directory.
def home (_ : Unit) : Path

toString

Renders a Path to its string form.
def toString (p : Path) : String

parent

The parent directory of p. The parent of a root path is itself.
def parent (p : Path) : Path

name

The final path component (e.g. the filename).
def name (p : Path) : String

stem

The filename without its suffix (e.g. "report" for "report.txt").
def stem (p : Path) : String

suffix

The file suffix including the leading dot (e.g. ".txt"), or "" if none.
def suffix (p : Path) : String

join

Appends a non-empty segment to p, producing a new Path.
def join (p : Path) (segment : String | segment ≠ "") : Path

withSuffix

Returns a copy of p with a different suffix. The new suffix must start with "." or be empty (to strip).
def withSuffix (p : Path) (newSuffix : String) : Path

absolute

Returns the absolute form of p, anchored at the current working dir.
def absolute (p : Path) : Path

resolve

Returns the canonical absolute path with symlinks resolved. Raises if the path does not exist on Python 3.6+ when strict=True; here we default to permissive (strict=False).
def resolve (p : Path) : Path

exists

True if p exists on the filesystem.
def exists (p : Path) : Bool

isFile

True if p exists and is a regular file.
def isFile (p : Path) : Bool

isDir

True if p exists and is a directory.
def isDir (p : Path) : Bool

isAbsolute

True if p is anchored at a root (has a drive or starts with "/").
def isAbsolute (p : Path) : Bool

isRelative

True if p is not absolute.
def isRelative (p : Path) : Bool

read

Reads a text file as a String. Raises if p is not a readable file.
def read (p : Path) : String

write

Writes content to p, overwriting any existing file.
def write (p : Path) (content : String) : Unit

appendTo

Appends content to p. Creates the file if it does not exist.
def appendTo (p : Path) (content : String) : Unit

mkdir

Creates the directory at p. Raises if p already exists or its parent is missing.
def mkdir (p : Path) : Unit

mkdirAll

Creates the directory at p along with any missing parents. Does not raise if p already exists. Equivalent to mkdir -p.
def mkdirAll (p : Path) : Unit

listDir

Lists immediate children of p as a list of names. Raises if p is not a directory.
def listDir (p : Path) : Array String

glob

Returns paths matching pattern relative to p (e.g. "*.py").
def glob (p : Path) (pattern : String | pattern ≠ "") : Array Path

remove

Deletes the file at p. Raises if p is a directory or does not exist.
def remove (p : Path) : Unit

removeDir

Deletes an empty directory at p. Raises if p is not empty.
def removeDir (p : Path) : Unit

removeAll

Recursively deletes a directory and its contents. Raises if p is not a directory.
def removeAll (p : Path) : Unit

rename

Renames or moves p to dst. Returns the new Path.
def rename (p : Path) (dst : Path) : Path

copy

Copies a file from src to dst, preserving metadata.
def copy (src : Path) (dst : Path) : Unit