CheckFact verifies that a store containing this fact respects inclusion constraints. It also checks types, since after desugaring, the argument types may affect which of the inclusion constraint alternatives need to be checked.
(fact ast.Atom, store factstore.FactStore)
| 51 | // It also checks types, since after desugaring, the argument types may affect which of the |
| 52 | // inclusion constraint alternatives need to be checked. |
| 53 | func (i InclusionChecker) CheckFact(fact ast.Atom, store factstore.FactStore) error { |
| 54 | decl, ok := i.decls[fact.Predicate] |
| 55 | if !ok { |
| 56 | return fmt.Errorf("could not find declaration for %v", fact.Predicate) |
| 57 | } |
| 58 | subst, err := unionfind.UnifyTerms(fact.Args, decl.DeclaredAtom.Args) |
| 59 | if err != nil { |
| 60 | return fmt.Errorf("could not unify %v and %v: %w", fact, decl.DeclaredAtom, err) |
| 61 | } |
| 62 | |
| 63 | var reasons []string |
| 64 | // Try each disjunction and return when the first one succeeds. |
| 65 | // Otherwise, we collect the reason why it fails. |
| 66 | disjunctions: |
| 67 | for j, alternative := range decl.Constraints.Alternatives { |
| 68 | if err := i.typeChecker.CheckOneBoundDecl(fact, decl.Bounds[j]); err != nil { |
| 69 | reasons = append(reasons, fmt.Sprintf("%v does not match type bounds %v", fact, decl.Bounds[j])) |
| 70 | continue |
| 71 | } |
| 72 | |
| 73 | for _, c := range alternative { |
| 74 | want := c.ApplySubst(subst) |
| 75 | extraVars := make(map[ast.Variable]bool) |
| 76 | ast.AddVars(want, extraVars) |
| 77 | if len(extraVars) > 0 { |
| 78 | return fmt.Errorf("%v found extra variables %v", want, extraVars) |
| 79 | } |
| 80 | switch a := want.(type) { |
| 81 | case ast.Atom: |
| 82 | if !store.Contains(a) { |
| 83 | reasons = append(reasons, fmt.Sprintf("%v fails, store does not contain %v", alternative, want)) |
| 84 | continue disjunctions |
| 85 | } |
| 86 | case ast.NegAtom: |
| 87 | if store.Contains(a.Atom) { |
| 88 | reasons = append(reasons, fmt.Sprintf("%v fails, store contains %v but shouldn't", alternative, want)) |
| 89 | continue disjunctions |
| 90 | } |
| 91 | case ast.Eq: |
| 92 | if !a.Left.Equals(a.Right) { |
| 93 | reasons = append(reasons, fmt.Sprintf("%v fails, equality does not hold %v", alternative, want)) |
| 94 | continue disjunctions |
| 95 | } |
| 96 | case ast.Ineq: |
| 97 | if a.Left.Equals(a.Right) { |
| 98 | reasons = append(reasons, fmt.Sprintf("%v fails, equality %v holds but shouldn't", alternative, want)) |
| 99 | continue disjunctions |
| 100 | } |
| 101 | default: |
| 102 | return fmt.Errorf("unexpected inclusion constraint %v", want) |
| 103 | } |
| 104 | } |
| 105 | // All constraints from this disjunction element have worked out. |
| 106 | return nil |
| 107 | } |
| 108 | return fmt.Errorf("none of the inclusion constraints are satisfied. reasons: %s", strings.Join(reasons, ",")) |
| 109 | } |