Description of the blob_tree(tree) SETL procedure
This procedure blobs a tree down to MLSS (other versions will also be needed); top entry, whose only autonomous work is to clear auxiliary global counter and map.
Description of the blob_tree_in(node) and blob_tree_inr(node) SETL procedures
This routines call each other in mutual recursion, being the "outer" recursive workhorse and the "inner" recursive workhorse for blobbing, respectively.
Method: We descend the tree, checking the nodes. As soon as an "unmanageable" node is found, the remainder is blobbed to a string, which is given a generated
"blob_name", equal strings always being given identical blob_names. The blobbed parse tree is returned.
Range of applicability: The built-in unblobbed operations in this version are:
and, or, „imp, if, ==, =, :=, +, *, -, {-}, [-], incs, „incin, in, not, notin, /==, /=, „nincs, „nincin.
Simplifications:
The following special simplifications can be detected and made during the blobbing process.
Note that these need to be turned off during equality deduction, to ensure that equality detection
reflects the external form of formulae; but should be turned on during processing of
inference procedures for which this is not an issue.
- Is_map({[anything_1,anything_2]: ..}) --> true
- Is_svm({[x,anything]: x in s | P}) --> true
- {x: x in s} --> s
- {expn: iters | true} --> {expn: iters}
- {expn: iters | false} --> {}
- One_one({[anything,anything]: ...}) --> true
- One_one({[[anything_1,anything_2],[anything_2,anything_1]]: ...}) --> true
- {[x,e(x)]: x in s | P} @ {[y,ee(y)]: y in ss | PP} --> {[y,e(ee(y))]: y in ss | PP & ee(y) in s & P(ee(y))}
- Finite(#s) --> Finite(s)
- ##s --> #s
- {e_independent_of_x: x in s| P} --> if {x: x in s | P} = {} then {} else {e_independent_of_x} end if
***** Note: should also do if any iterator is null
- {e(x): iterator,...,x in 0,iterator,... | P} --> 0
- {e(x): x in {a} | P(x)} --> if P(a) then {e(a)} else 0 end if
- (FORALL iterator,...,x in 0,iterator,... | P) --> true
- (EXISTS iterator,...,x in 0,iterator,... | P) --> false
- arb({s}) --> s
- car([x,y]) --> x
- cdr([x,y]) --> y
- domain({[anything,anything']: iterator | P}) --> {anything: iterator (reduced_if_no_condition) | P}
- range({[anything,anything']: iterator | P}) --> {anything': iterator (reduced_if_no_condition) | P}
- #{[x,e(x)]: x in s} --> #s
- Ord(next(s)) --> Ord(s)