inferRelTypesFromPremise is called for index \in 0..len(premises). It maps one state of inference to its (possibly empty) list of successors.
(premises []ast.Term, state *inferState)
| 111 | // inferRelTypesFromPremise is called for index \in 0..len(premises). It |
| 112 | // maps one state of inference to its (possibly empty) list of successors. |
| 113 | func (ic *inferContext) inferRelTypesFromPremise(premises []ast.Term, state *inferState) ([]*inferState, error) { |
| 114 | bc := ic.bc |
| 115 | var nextStates []*inferState |
| 116 | |
| 117 | // TODO: this should be piped through in inferState. |
| 118 | typeCtx := map[ast.Variable]ast.BaseTerm{} |
| 119 | |
| 120 | premise := premises[state.index] |
| 121 | switch t := premise.(type) { |
| 122 | case ast.Atom: |
| 123 | atom := t |
| 124 | var ( |
| 125 | alternatives []ast.BaseTerm |
| 126 | err error |
| 127 | ) |
| 128 | if atom.Predicate == symbols.MatchField { |
| 129 | // The first argument *must* be bound, therefore we *must* have a type for it, |
| 130 | // it must be a record type the selected field. |
| 131 | |
| 132 | scrutinee, ok := atom.Args[0].(ast.Variable) |
| 133 | if !ok { |
| 134 | return nil, fmt.Errorf(":match_field must be applied to a variable") |
| 135 | } |
| 136 | i := state.usedVars.Find(scrutinee) |
| 137 | if i == -1 { |
| 138 | // This cannot happen. |
| 139 | return nil, fmt.Errorf(":match_field must be applied to a bound variable") |
| 140 | } |
| 141 | scrutineeType := state.varTpe[i] |
| 142 | if scrutineeType == ast.AnyBound { // Give up. |
| 143 | alternatives = []ast.BaseTerm{symbols.BuiltinRelations[symbols.MatchField]} |
| 144 | } else { |
| 145 | |
| 146 | name, ok := atom.Args[1].(ast.Constant) |
| 147 | if !ok || name.Type != ast.NameType { |
| 148 | // This cannot happen. |
| 149 | return nil, fmt.Errorf(":match_field field selector must be a constant") |
| 150 | } |
| 151 | projected, err := symbols.StructTypeField(scrutineeType, name) |
| 152 | if err != nil { |
| 153 | return nil, fmt.Errorf(":match_field struct type %v does not have field %v", scrutineeType, name) |
| 154 | } |
| 155 | |
| 156 | alternatives = []ast.BaseTerm{symbols.NewRelType(scrutineeType, ast.NameBound, projected)} |
| 157 | } |
| 158 | |
| 159 | } else if declared, ok := bc.relTypeMap[atom.Predicate]; ok { |
| 160 | alternatives, _, err = bc.feasibleAlternatives(atom.Predicate, declared, atom.Args, state.asMap(), typeCtx) |
| 161 | } else { |
| 162 | alternatives, err = bc.getOrInferRelTypes(atom.Predicate, atom.Args, state.asMap(), typeCtx) |
| 163 | } |
| 164 | |
| 165 | if err != nil { |
| 166 | return nil, fmt.Errorf("type mismatch %v : %v ", premise, err) |
| 167 | } |
| 168 | for _, alternative := range alternatives { |
| 169 | relTypeArgs, err := symbols.RelTypeArgs(alternative) |
| 170 | if err != nil { |
no test coverage detected