modus_lib/
wellformed.rs

1// Modus, a language for building container images
2// Copyright (C) 2022 University College London
3
4// This program is free software: you can redistribute it and/or modify
5// it under the terms of the GNU Affero General Public License as
6// published by the Free Software Foundation, either version 3 of the
7// License, or (at your option) any later version.
8
9// This program is distributed in the hope that it will be useful,
10// but WITHOUT ANY WARRANTY; without even the implied warranty of
11// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12// GNU Affero General Public License for more details.
13
14// You should have received a copy of the GNU Affero General Public License
15// along with this program.  If not, see <https://www.gnu.org/licenses/>.
16
17use std::collections::{HashMap, HashSet};
18
19use crate::logic::{Clause, IRTerm, Signature};
20
21/// infer image predicates, i.e. those that transitively depend on image/1
22/// check that image predicates depend on image/1 in each disjunct
23pub fn check_image_predicates(
24    clauses: &Vec<Clause<IRTerm>>,
25) -> Result<HashSet<Signature>, HashSet<Signature>> {
26    todo!()
27}
28
29fn combine_groundness(g1: &[bool], g2: &[bool]) -> Vec<bool> {
30    debug_assert_eq!(g1.len(), g2.len());
31
32    // NOTE: this'll never fail since the lengths match, i.e. we'll always
33    // be able to combine then. The extreme case is when we enforce that
34    // all arguments have to be ground.
35    let mut new_g = Vec::with_capacity(g1.len());
36    for (&allowed1, &allowed2) in g1.iter().zip(g2) {
37        // This argument is only allowed to be ungrounded if both are allowed
38        // to be ungrounded.
39        new_g.push(allowed1 && allowed2);
40    }
41    new_g
42}
43
44// infer grounded variables, check if grounded variables are grounded in each rule
45pub fn check_grounded_variables(
46    clauses: &[Clause<IRTerm>],
47) -> Result<HashMap<Signature, Vec<bool>>, HashSet<Signature>> {
48    let mut errors: HashSet<Signature> = HashSet::new();
49    let mut result: HashMap<Signature, Vec<bool>> = HashMap::new();
50
51    fn infer(c: &Clause<IRTerm>) -> Vec<bool> {
52        let body_vars = c
53            .body
54            .iter()
55            .map(|r| r.variables(true))
56            .reduce(|mut l, r| {
57                l.extend(r);
58                l
59            })
60            .unwrap_or_default();
61        c.head
62            .args
63            .iter()
64            .map(|t| match t {
65                IRTerm::Constant(_) => true,
66                IRTerm::Array(ts) => {
67                    // either the terms of this array are constant or contained in the body
68                    ts.iter()
69                        .all(|t| t.is_constant_or_compound_constant() || body_vars.contains(t))
70                        || body_vars.contains(t)
71                }
72                v => body_vars.contains(v),
73            })
74            .collect()
75    }
76
77    let signatures: HashSet<Signature> = clauses.iter().map(|c| c.head.signature()).collect();
78
79    for c in clauses {
80        let sig = c.head.signature();
81        let grounded = infer(c);
82
83        let new_groundness = if let Some(prev_groundness) = result.get(&sig) {
84            combine_groundness(&prev_groundness, &grounded)
85        } else {
86            grounded
87        };
88        result.insert(sig, new_groundness);
89    }
90
91    if errors.is_empty() {
92        Ok(result)
93    } else {
94        Err(errors)
95    }
96}
97
98#[cfg(test)]
99mod tests {
100    use super::*;
101    use crate::{logic::Predicate, modusfile};
102    #[test]
103    fn consistently_grounded() {
104        let clauses: Vec<Clause> = vec![
105            "a(X, Y) :- b(X), c(X, Z).".parse().unwrap(),
106            "a(X, Y) :- d(X).".parse().unwrap(),
107            "b(X) :- d(X).".parse().unwrap(),
108        ];
109        let result = check_grounded_variables(&clauses);
110        assert!(result.is_ok());
111        let a_sig = Signature(Predicate("a".into()), 2);
112        let a_grounded = result.unwrap().get(&a_sig).unwrap().clone();
113        assert!(a_grounded[0]);
114        assert!(!a_grounded[1]);
115    }
116
117    #[test]
118    fn correctly_combined_grounded() {
119        let clauses: Vec<Clause> = vec![
120            "a(X, Y) :- b(X), c(X, Z).".parse().unwrap(),
121            "a(X, Y) :- d(Y).".parse().unwrap(),
122        ];
123        let result = check_grounded_variables(&clauses);
124        assert!(result.is_ok());
125        let a_sig = Signature(Predicate("a".into()), 2);
126        let a_grounded = result.unwrap().get(&a_sig).unwrap().clone();
127        assert!(!a_grounded[0]);
128        assert!(!a_grounded[1]);
129    }
130
131    #[test]
132    fn groundness_after_translation() {
133        let modus_clause: modusfile::ModusClause = "foo(X) :- bar(X) ; baz.".parse().unwrap();
134        let clauses: Vec<Clause> = (&modus_clause).into();
135        let result = check_grounded_variables(&clauses);
136        assert!(result.is_ok());
137        let foo_sig = Signature(Predicate("foo".into()), 1);
138        let foo_grounded = result.unwrap().get(&foo_sig).unwrap().clone();
139        assert!(!foo_grounded[0]);
140    }
141}
modus_lib/wellformed.rs

modus_lib/
wellformed.rs
