poi 0.25.0

A pragmatic point-free theorem prover assistant
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
104
105
106
107
108
109
110
111
112
113
114
115
116

use crate::*;

pub fn transpose(a: &Vec<Expr>) -> Result<Expr, Error> {
    let mut res = vec![];
    let cols = if let Some(a) = a.get(0) {
        if let List(a) = a {
            a.len()
        } else {
            return Err(Error::InvalidComputation);
        }
    } else {
        return Err(Error::InvalidComputation);
    };
    if a.len() != cols {
        return Err(Error::InvalidComputation);
    }
    for i in 0..a.len() {
        let mut row = vec![];
        for j in 0..cols {
            if let Some(List(a)) = a.get(j) {
                if let Some(el) = a.get(i) {
                    row.push(el.clone());
                } else {
                    return Err(Error::InvalidComputation);
                }
            } else {
                return Err(Error::InvalidComputation);
            }
        }
        res.push(List(row));
    }
    Ok(List(res))
}

pub fn is_square_mat(a: &Vec<Expr>) -> Result<Expr, Error> {
    let n = a.len();
    let mut sq = true;
    for i in 0..n {
        if let List(b) = &a[i] {
            if b.len() != n {
                sq = false;
                break;
            }
        } else {
            sq = false;
            break;
        }
    }
    Ok(Ret(Bool(sq)))
}

pub fn dim(a: &Vec<Expr>) -> Result<Expr, Error> {
    let n = a.len();
    let mut m: Option<usize> = None;
    for i in 0..n {
        if let List(b) = &a[i] {
            if let Some(m) = m {
                if b.len() != m {
                    return Err(Error::InvalidComputation);
                }
            } else {
                m = Some(b.len());
            }
        } else {
            return Err(Error::InvalidComputation);
        }
    }
    if let Some(m) = m {
        Ok(List(vec![(n as f64).into(), (m as f64).into()]))
    } else {
        return Err(Error::InvalidComputation);
    }
}

pub fn col(a: f64, b: &Vec<Expr>) -> Result<Expr, Error> {
    let mut res = vec![];
    for bi in b {
        if let List(bi) = bi {
            if let Some(bi) = bi.get(a as usize) {
                res.push(bi.clone());
            } else {
                return Err(Error::InvalidComputation);
            }
        } else {
            return Err(Error::InvalidComputation);
        }
    }
    Ok(List(res))
}

pub fn mul_mat(a: &Vec<Expr>, b: &Vec<Expr>) -> Result<Expr, Error> {
    let mut res = vec![];
    let cols = if let Some(b) = b.get(0) {
        if let List(b) = b {
            b.len()
        } else {
            return Err(Error::InvalidComputation);
        }
    } else {
        return Err(Error::InvalidComputation);
    };
    for i in 0..a.len() {
        let mut row = vec![];
        for j in 0..cols {
            if let Some(a) = a.get(i) {
                row.push(app(Sum,
                    app2(Mul, a.clone(), col(j as f64, b)?)
                ));
            } else {
                return Err(Error::InvalidComputation);
            }
        }
        res.push(List(row));
    }
    Ok(List(res))
}