Method inferRelTypesFromClause

analysis/infercontext.go:292–387

inferRelTypesFromClause infers possible relation types for the head predicate of a single clause.

()

// inferRelTypesFromClause infers possible relation types for the head predicate of a single clause.
func (ic *inferContext) inferRelTypesFromClause() (ast.BaseTerm, error) {
	clause := ic.clause

	usedVars := VarList{}
	state := &inferState{0, usedVars, []ast.BaseTerm{}}

	if ic.decl != nil && len(ic.modes) == 1 {
		for i, m := range ic.modes[0] {
			v, ok := clause.Head.Args[i].(ast.Variable)
			if !ok {
				continue
			}
			if m == ast.ArgModeInput {
				// Treat as bound variable.
				state.usedVars = state.usedVars.Extend([]ast.Variable{v})
				types := []ast.BaseTerm{}
				if len(ic.decl.Bounds) > 0 {
					for _, b := range ic.decl.Bounds {
						tpe := b.Bounds[i]
						types = append(types, tpe)
					}
				} else {
					types = append(types, ast.AnyBound)
				}
				if len(types) == 1 {
					state.varTpe = append(state.varTpe, types[0])
				} else {
					state.varTpe = append(state.varTpe, symbols.NewUnionType(types...))
				}
			}
		}
	}
	levels := make([][]*inferState, len(clause.Premises)+1)
	levels[0] = []*inferState{state}
	for i := range clause.Premises {
		for _, state := range levels[i] {
			nextStates, err := ic.inferRelTypesFromPremise(clause.Premises, state)
			if err != nil {
				continue
			}
			levels[i+1] = append(levels[i+1], nextStates...)
		}
		if len(levels[i+1]) == 0 {
			return nil, fmt.Errorf("type mismatch: cannot find assignment that works for premise %v", clause.Premises[i])
		}
	}

	// Constrain variables used in HeadTime to be of type Time.
	if clause.HeadTime != nil {
		var nextStates []*inferState
		var lastErr error
		for _, s := range levels[len(clause.Premises)] {
			valid := true
			if clause.HeadTime.Start.Type == ast.VariableBound {
				if err := s.addOrRefine(clause.HeadTime.Start.Variable, ast.TimeBound); err != nil {
					valid = false
					lastErr = err
				}