RectifyAtom ensures all arguments of an atom are variables. It returns a tuple (rectified atom, extra terms, fresh variables, defined variables). An atom p(t_1, ..., t_n) is rectified if each t_i is a variable and all are distinct. We go a bit further and also ensure that t_i are distinct from a s
(atom ast.Atom, usedVars VarList)
| 14 | // this stronger sense, than extra terms and fresh variables will be empty and boundVars |
| 15 | // contains atom arguments in left-to-right order. |
| 16 | func RectifyAtom(atom ast.Atom, usedVars VarList) (ast.Atom, []ast.Term, []ast.Variable, []ast.Variable) { |
| 17 | used := usedVars.AsMap() |
| 18 | pred := atom.Predicate |
| 19 | newArgs := make([]ast.BaseTerm, pred.Arity) |
| 20 | |
| 21 | var freshVars, boundVars []ast.Variable |
| 22 | var fml []ast.Term |
| 23 | makeFresh := func(i int, arg ast.BaseTerm) { |
| 24 | fresh := ast.FreshVariable(used) |
| 25 | freshVars = append(freshVars, fresh) |
| 26 | newArgs[i] = fresh |
| 27 | fml = append(fml, ast.Eq{fresh, arg}) |
| 28 | } |
| 29 | for i, arg := range atom.Args { |
| 30 | switch a := arg.(type) { |
| 31 | case ast.ApplyFn: |
| 32 | makeFresh(i, arg) |
| 33 | |
| 34 | case ast.Constant: |
| 35 | makeFresh(i, arg) |
| 36 | |
| 37 | case ast.Variable: |
| 38 | if a.Symbol == "_" { |
| 39 | newArgs[i] = a |
| 40 | continue |
| 41 | } |
| 42 | if _, ok := used[a]; ok { |
| 43 | makeFresh(i, arg) |
| 44 | continue |
| 45 | } |
| 46 | used[a] = true |
| 47 | newArgs[i] = a |
| 48 | boundVars = append(boundVars, a) |
| 49 | } |
| 50 | } |
| 51 | return ast.Atom{pred, newArgs}, fml, freshVars, boundVars |
| 52 | } |