gdp_rs 0.1.1

A library for implementing Ghosts-of-departed-proofs pattern in rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

//! I define types for representing inference rules.
//!

use std::marker::PhantomData;

use crate::predicate::Predicate;

/// A trait for defining an inference rule.
pub trait InferenceRule {
    /// Type of source proposition's subject.
    type SourceSub;

    /// Type of source proposition's predicate.
    type SourcePredicate: Predicate<Self::SourceSub>;

    /// Type of target proposition's subject.
    type TargetSub;

    /// Type of target proposition's predicate.
    type TargetPredicate: Predicate<Self::TargetSub>;

    /// Type of subject transform.
    type SubjectTransform: Operation<Arg = Self::SourceSub, Result = Self::TargetSub>;
}

/// A trait for representing an operation over a subject.
/// It is analogous to `FnOnce<(Arg, )>`
pub trait Operation {
    /// Type of source proposition's subject.
    type Arg;

    /// Type of target proposition's subject.
    type Result;

    /// Call the operation.
    fn call(self, source_sub: Self::Arg) -> Self::Result;
}

/// A marker trait for marking an inference rule as authorized.
/// This can be used to limit who can authorize an inference, using rust's orphan rules.
pub trait AuthorizedInferenceRuleGhost<TPredicate: Predicate<TSub>, TSub> {}

/// A marker trait for marking a subject transform as predicate preserving transform.
pub trait PreservingTransformGhost<SPredicate: Predicate<Sub>, Sub> {}

/// A struct for representing identity transform.
#[derive(Debug)]
pub struct IdentityTransform<Sub> {
    _phantom: PhantomData<fn() -> Sub>,
}

impl<Sub> Default for IdentityTransform<Sub> {
    #[inline]
    fn default() -> Self {
        Self {
            _phantom: PhantomData,
        }
    }
}

impl<Sub> Operation for IdentityTransform<Sub> {
    type Arg = Sub;
    type Result = Sub;

    #[inline]
    fn call(self, source_sub: Self::Arg) -> Self::Result {
        source_sub
    }
}

impl<Sub, P: Predicate<Sub>> PreservingTransformGhost<P, Sub>
    for PhantomData<IdentityTransform<Sub>>
{
}