elaboration of expressions (formulas or terms)

[arademaker]

We need much more than just type the variables. For instance

Starting with

(=>
  (and
    (maxValue ?R ?ARG ?N)
    (?R @ARGS)
    (equal ?VAL (ListOrderFn (ListFn @ARGS) ?ARG)))
  (greaterThan ?N ?VAL))

the transformation is

(=>
  (and
    (maxValue ?R:Relation ?ARG:Entity ?N:Number)
    (?R @ARGS)
    (equal ?VAL:Number (ListOrderFn (ListFn @ARGS):[Entity] ?ARG:Number):Number))
  (greaterThan ?N:Number ?VAL:Number):bool)

...
(=>
  (and
    (maxValue ?R:Relation ?ARG:Entity ?N:Number)
    (subclass @ARGS)
    (equal ?VAL:Number (ListOrderFn (ListFn @ARGS):[Entity] ?ARG:Number):Number))
  (greaterThan ?N:Number ?VAL:Number):bool)
...
(=>
  (and
    (maxValue ?R:Relation ?ARG:Entity ?N:Number)
    (subclass ?ARG1:SetOrClass ?ARG2:SetOrClass)
    (equal ?VAL:Number (ListOrderFn (ListFn ARG1:SetOrClass ARG2:SetOrClass):[SetOrClass] ?ARG:Number):SetOrClass))
  (greaterThan ?N:Number ?VAL:Number):bool)
  ===> crash number is not SetOrClass
...

We need an elaborator similar to https://arxiv.org/abs/1505.04324