tensorlogic-compiler 0.1.0

Compiler for transforming logic expressions into tensor computation graphs
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103

//! Differentiation arms for temporal, modal, and hybrid-logic operators.

use tensorlogic_ir::TLExpr;

use super::diff_core::diff_expr;
use super::helpers::zero;
use super::types::{DiffContext, DiffError};

/// Try to differentiate `expr` using temporal / modal / hybrid rules.
pub(super) fn try_diff_modal(
    expr: &TLExpr,
    ctx: &mut DiffContext<'_>,
) -> Option<Result<TLExpr, DiffError>> {
    match expr {
        TLExpr::Next(inner) => Some((|| {
            let di = diff_expr(inner, ctx)?;
            Ok(TLExpr::Next(Box::new(di)))
        })()),

        TLExpr::Eventually(inner) => Some((|| {
            let di = diff_expr(inner, ctx)?;
            Ok(TLExpr::Eventually(Box::new(di)))
        })()),

        TLExpr::Always(inner) => Some((|| {
            let di = diff_expr(inner, ctx)?;
            Ok(TLExpr::Always(Box::new(di)))
        })()),

        TLExpr::Box(inner) => Some((|| {
            let di = diff_expr(inner, ctx)?;
            Ok(TLExpr::Box(Box::new(di)))
        })()),

        TLExpr::Diamond(inner) => Some((|| {
            let di = diff_expr(inner, ctx)?;
            Ok(TLExpr::Diamond(Box::new(di)))
        })()),

        TLExpr::Until { before, after } => Some((|| {
            let db = diff_expr(before, ctx)?;
            let da = diff_expr(after, ctx)?;
            Ok(TLExpr::Until {
                before: Box::new(db),
                after: Box::new(da),
            })
        })()),

        TLExpr::Release { released, releaser } => Some((|| {
            let dr = diff_expr(released, ctx)?;
            let da = diff_expr(releaser, ctx)?;
            Ok(TLExpr::Release {
                released: Box::new(dr),
                releaser: Box::new(da),
            })
        })()),

        TLExpr::WeakUntil { before, after } => Some((|| {
            let db = diff_expr(before, ctx)?;
            let da = diff_expr(after, ctx)?;
            Ok(TLExpr::WeakUntil {
                before: Box::new(db),
                after: Box::new(da),
            })
        })()),

        TLExpr::StrongRelease { released, releaser } => Some((|| {
            let dr = diff_expr(released, ctx)?;
            let da = diff_expr(releaser, ctx)?;
            Ok(TLExpr::StrongRelease {
                released: Box::new(dr),
                releaser: Box::new(da),
            })
        })()),

        // Hybrid / modal
        TLExpr::Nominal { .. } => Some(Ok(zero())),

        TLExpr::At { nominal, formula } => Some((|| {
            let df = diff_expr(formula, ctx)?;
            Ok(TLExpr::At {
                nominal: nominal.clone(),
                formula: Box::new(df),
            })
        })()),

        TLExpr::Somewhere { formula } => Some((|| {
            let df = diff_expr(formula, ctx)?;
            Ok(TLExpr::Somewhere {
                formula: Box::new(df),
            })
        })()),

        TLExpr::Everywhere { formula } => Some((|| {
            let df = diff_expr(formula, ctx)?;
            Ok(TLExpr::Everywhere {
                formula: Box::new(df),
            })
        })()),

        _ => None,
    }
}