-
Notifications
You must be signed in to change notification settings - Fork 217
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added example for fixpointed to-directory-tree command
- Loading branch information
Showing
1 changed file
with
119 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,119 @@ | ||
-- This is an example on how to build a directory tree using the so-called | ||
-- fixpointed method. See the documenatation of the `Dhall.DirectoryTree` module | ||
-- for further information on it. | ||
|
||
-- First, define some types recognized by the `dhall to-directory-tree` command. | ||
|
||
-- A user, either identified by its numeric user id or its name. | ||
let User = < UserId : Natural | UserName : Text > | ||
|
||
-- Similarly, a group. | ||
let Group = < GroupId : Natural | GroupName : Text > | ||
|
||
-- The following two type aliases are a well-typed represenation of the bitmask | ||
-- for permissions used by the DAC access control found on Unix systems. See for | ||
-- example the chmod(5) manual entry. | ||
|
||
-- How much access we do grant... | ||
let Access = | ||
{ execute : Optional Bool, read : Optional Bool, write : Optional Bool } | ||
|
||
-- ... for whom. | ||
let Mode = | ||
{ user : Optional Access | ||
, group : Optional Access | ||
, other : Optional Access | ||
} | ||
|
||
-- A generic file system entry. It consists of a name, an abstract content and | ||
-- some metadata which might be set (Some) or not (None). | ||
let Entry = | ||
\(content : Type) -> | ||
{ name : Text | ||
, content : content | ||
, user : Optional User | ||
, group : Optional Group | ||
, mode : Optional Mode | ||
} | ||
|
||
-- This is the main program constructing our directory tree. It is a fixpoint | ||
-- definition similar to how we deal with recursive types in arbitrary Dhall | ||
-- programs but specialised to our use case. The first argument is the type of a | ||
-- directory tree and the second one is a record where each field is a | ||
-- constructor for a specific filesystem entry. | ||
in \(tree : Type) -> | ||
\ ( make | ||
: { directory : Entry (List tree) -> tree, file : Entry Text -> tree } | ||
) -> | ||
|
||
-- Before we define the actual directory tree we define some Dhall schemas | ||
-- and shortcuts for convenience. | ||
|
||
-- A schema suitable for a directory... | ||
let Directory = | ||
{ Type = | ||
{ name : Text | ||
, content : List tree | ||
, user : Optional User | ||
, group : Optional Group | ||
, mode : Optional Mode | ||
} | ||
, default = | ||
{ content = [] : List tree | ||
, user = None User | ||
, group = None Group | ||
, mode = None Mode | ||
} | ||
} | ||
|
||
-- ... and one for a file. | ||
let File = | ||
{ Type = | ||
{ name : Text | ||
, content : Text | ||
, user : Optional User | ||
, group : Optional Group | ||
, mode : Optional Mode | ||
} | ||
, default = | ||
{ content = "" | ||
, user = None User | ||
, group = None Group | ||
, mode = None Mode | ||
} | ||
} | ||
|
||
-- Give someone full access to an filesystem entry. | ||
let full_access | ||
: Access | ||
= { execute = Some True, read = Some True, write = Some True } | ||
|
||
-- Give someone no access at all to an filesystem entry. | ||
let no_access | ||
: Access | ||
= { execute = Some False, read = Some False, write = Some False } | ||
|
||
-- These permissions | ||
-- * grant full access to the user. | ||
-- * retain the permissions of the primary group of the user. | ||
-- * deny access to everyone else. | ||
let semi_private | ||
: Mode | ||
= { user = Some full_access, group = None Access, other = Some no_access } | ||
|
||
-- Now let's start with the directory tree ... | ||
in [ -- Some file with a gentle greeting. No metadata is set explicitly. | ||
make.file File::{ name = "some file", content = "Hello world!" } | ||
-- A directory with some metadata set explicitely. | ||
, make.directory | ||
Directory::{ | ||
, name = "my private directory" | ||
-- How owns the new directory: just_me | ||
, user = Some (User.UserName "just_me") | ||
-- We stick with the user's default group here. | ||
, group = None Group | ||
, mode = Some semi_private | ||
, content = [] : List tree | ||
} | ||
] | ||
: List tree |