crash parsing raft spec. Proposed fix to ivy_logic_utils.py() in ivy_logic_utils.py

[glycerine]

Trying to run ivy_check on this Raft spec by James Wilcox https://github.com/glycerine/ivy-jea/blob/master/jea/raft.ivy resulted in the following crash:

(venv) jaten@Js-MacBook-Pro ~/pyivy/ivy/jea (darwin) $ ivy_check raft.ivy
Traceback (most recent call last):
  File "/Users/jaten/pyivy/venv/bin/ivy_check", line 33, in <module>
    sys.exit(load_entry_point('ms-ivy==1.8.25', 'console_scripts', 'ivy_check')())
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_check.py", line 907, in main
    check_module()
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_check.py", line 876, in check_module
    check_isolate()
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_check.py", line 453, in check_isolate
    ifc.check_fragment()
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_fragment.py", line 584, in check_fragment
    assumes,asserts,macros = get_assumes_and_asserts(preconds_only)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_fragment.py", line 517, in get_assumes_and_asserts
    triple = action.update(im.module,[])
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 219, in update
    return self.hide_formals(bind_olds_action(self.int_update(domain,in_scope)))
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 1066, in int_update
    update = self.args[-1].int_update(domain,pvars)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 784, in int_update
    thing = op.int_update(domain,pvars);
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 1066, in int_update
    update = self.args[-1].int_update(domain,pvars)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 784, in int_update
    thing = op.int_update(domain,pvars);
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 1066, in int_update
    update = self.args[-1].int_update(domain,pvars)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 784, in int_update
    thing = op.int_update(domain,pvars);
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 1066, in int_update
    update = self.args[-1].int_update(domain,pvars)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 784, in int_update
    thing = op.int_update(domain,pvars);
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 1207, in int_update
    v = self.apply_actuals(domain,pvars,v)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_actions.py", line 1228, in apply_actuals
    v = substitute_constants_ast(v,subst)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_ast.py", line 31, in clone
    res = type(self)(*args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_ast.py", line 31, in clone
    res = type(self)(*args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_ast.py", line 31, in clone
    res = type(self)(*args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_ast.py", line 647, in clone
    res = AST.clone(self,args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_ast.py", line 31, in clone
    res = type(self)(*args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in <genexpr>
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
  File "/Users/jaten/pyivy/venv/lib/python3.10/site-packages/ivy/ivy_logic_utils.py", line 180, in substitute_constants_ast
    return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)
AttributeError: 'NoneType' object has no attribute 'clone'
$

I propose this as a fix, in ivy/ivy_logic_utils.py, circa line 177, to handle the None case gracefully and idempotently.

@kenmcmil and friends: I would appreciate a review of this fix, to have some confidence that I have not messed up something else by making this change.

def substitute_constants_ast(ast,subs):
    """
    Substitute terms for *constants*. Here, subs is
    a dict from string names of constants to terms.
    """
    # jea comment: None gets here b/c lots of LabeledFormula are actually unlabelled.
    if ast is None:  # jea added
        return None  # jea added
    if is_constant(ast):
        return subs.get(ast.rep,ast)
    else:
        return ast.clone(substitute_constants_ast(x,subs) for x in ast.args)

With this fix, the same raft.ivy spec does now check and return OK. (Using my fork -- https://github.com/glycerine/ivy-jea -- with several other fixes applied, as noted in other issues.)