Package imandra
Expand source code
#!/usr/bin/python3
from . import ipl
from .auth import Auth
from . import instance
from . import rule_synth
from . import cfb
from . import core
from .session import HttpInstanceSession
def main():
import sys
import argparse
parser = argparse.ArgumentParser(prog="imandra", description="Imandra CLI")
parser.set_defaults(run=lambda args: parser.print_help())
subparsers = parser.add_subparsers()
auth = Auth()
parser_auth = subparsers.add_parser('auth')
parser_auth.set_defaults(run=lambda args: parser_auth.print_help())
parser_auth_subparsers = parser_auth.add_subparsers()
def login(args):
auth.login()
print("Logged in")
parser_login = parser_auth_subparsers.add_parser('login')
parser_login.set_defaults(run=login)
def logout(args):
auth.logout()
print("Logged out")
parser_logout = parser_auth_subparsers.add_parser('logout')
parser_logout.set_defaults(run=logout)
parser_export = parser_auth_subparsers.add_parser('export')
parser_export.set_defaults(run=lambda args: auth.export())
parser_import = parser_auth_subparsers.add_parser('import')
parser_import.set_defaults(run=lambda args: auth.import_())
parser_ipl = subparsers.add_parser('ipl')
parser_ipl.set_defaults(run=lambda args: parser_ipl.print_help())
parser_ipl_subparsers = parser_ipl.add_subparsers()
def ipl_decompose(args):
if args.file is not None and args.parent_job_id is not None:
print("error: --file and --parent-job-id are mutually exclusive operations. "
"You must pick one or the other")
sys.exit(1)
if args.file is None and args.parent_job_id is None:
print ('error: --file must be provided')
else:
ipl.decompose(auth, args.file, args.testgen_lang, args.organization,
args.callback, args.doc_gen, args.parent_job_id)
parser_ipl_decompose = parser_ipl_subparsers.add_parser('decompose')
parser_ipl_decompose.add_argument('--file')
parser_ipl_decompose.add_argument('--callback')
parser_ipl_decompose.add_argument('--testgen-lang', help=argparse.SUPPRESS)
parser_ipl_decompose.add_argument('--organization')
parser_ipl_decompose.add_argument('--doc-gen', choices=['true','false'], default='true')
parser_ipl_decompose.add_argument('--parent-job-id',
help=("The id of a previously completed job. Instead of running a "
"full decomposition, re-run just the script generation phase of "
"this parent-job. When using this option all other options will be "
"ignore and the original values from the parent-job will be used."))
parser_ipl_decompose.set_defaults(run=ipl_decompose)
def ipl_simulator(args):
if args.file is None:
print ('error: --file must be provided')
else:
ipl.simulator(auth, args.file)
parser_ipl_simulator = parser_ipl_subparsers.add_parser('simulator')
parser_ipl_simulator.add_argument('--file')
parser_ipl_simulator.set_defaults(run=ipl_simulator)
def ipl_status(args):
if args.uuid is None:
print ('error: --uuid must be provided')
else:
ipl.status(auth, args.uuid)
parser_ipl_status = parser_ipl_subparsers.add_parser('status')
parser_ipl_status.add_argument('--uuid')
parser_ipl_status.set_defaults(run=ipl_status)
def ipl_data(args):
if args.uuid is None:
print ('error: --uuid must be provided')
else:
ipl.data(auth, args.uuid)
parser_ipl_decompose = parser_ipl_subparsers.add_parser('data')
parser_ipl_decompose.add_argument('--uuid')
parser_ipl_decompose.set_defaults(run=ipl_data)
parser_ipl_jobs = parser_ipl_subparsers.add_parser('list-jobs')
parser_ipl_jobs.set_defaults(run=lambda args: ipl.list_jobs(auth))
def ipl_cancel(args):
if args.uuid is None:
print ('error: --uuid must be provided')
else:
ipl.cancel(auth, args.uuid)
parser_ipl_cancel = parser_ipl_subparsers.add_parser('cancel')
parser_ipl_cancel.add_argument('--uuid')
parser_ipl_cancel.set_defaults(run=ipl_cancel)
parser_core = subparsers.add_parser('core')
parser_core.set_defaults(run=lambda args: parser_core.print_help())
parser_core_subparsers = parser_core.add_subparsers()
parser_instances = parser_core_subparsers.add_parser('instances')
parser_instances.set_defaults(run=lambda args: parser_instances.print_help())
parser_instances_subparsers = parser_instances.add_subparsers()
parser_instances_list = parser_instances_subparsers.add_parser('list')
parser_instances_list.set_defaults(run=lambda args: instance.list(auth))
def create_instance(args):
if args.instance_type is None:
print ('error: --instance-type must be provided')
else:
instance.create(auth, args.version, args.instance_type)
parser_instances_create = parser_instances_subparsers.add_parser('create')
parser_instances_create.add_argument('--instance-type')
parser_instances_create.add_argument('--version')
parser_instances_create.set_defaults(run=create_instance)
def kill_instance(args):
if args.id is None:
print ('error: --id must be provided')
else:
instance.delete(auth, args.id)
parser_instances_kill = parser_instances_subparsers.add_parser('kill')
parser_instances_kill.add_argument('--id')
parser_instances_kill.set_defaults(run=kill_instance)
def rule_synth(args):
if args.file is None:
print ('error: --file must be provided')
else:
rule_synth.synth(auth, args.file)
parser_rule_synth = subparsers.add_parser('rule-synth')
parser_rule_synth.set_defaults(run=lambda args: parser_rule_synth.print_help())
parser_rule_synth_subparsers = parser_rule_synth.add_subparsers()
parser_synth = parser_rule_synth_subparsers.add_parser('synth')
parser_synth.add_argument('--file')
parser_synth.set_defaults(run=rule_synth)
def cfb_analyze(args):
if args.job is None:
print ('error: --job must be provided')
else:
if args.path is None:
print ('error: --path must be provided')
else:
cfb.analyze(auth, args.job, args.path)
parser_cfb = subparsers.add_parser('cfb')
parser_cfb.set_defaults(run=lambda args: parser_cfb.print_help())
parser_cfb_subparsers = parser_cfb.add_subparsers()
parser_cfb_analyze = parser_cfb_subparsers.add_parser('analyze')
parser_cfb_analyze.add_argument('--job')
parser_cfb_analyze.add_argument('--path')
parser_cfb_analyze.set_defaults(run=cfb_analyze)
def repl(args):
core.run_repl(auth, args.args)
parser_repl = parser_core_subparsers.add_parser('repl')
parser_repl.add_argument('args', nargs=argparse.REMAINDER)
parser_repl.set_defaults(run=repl)
def install_imandra_core(args):
core.install(auth)
parser_install = parser_core_subparsers.add_parser('install')
parser_install.set_defaults(run=install_imandra_core)
if len(sys.argv) > 2 and sys.argv[1] == 'core' and sys.argv[2] == 'repl':
# Run this directly so we can pass --help directly to the repl command to see its own help text
core.run_repl(auth, sys.argv[3:])
else:
args = parser.parse_args()
args.run(args)
def session():
return HttpInstanceSession()
Sub-modules
imandra.auth
imandra.cfb
imandra.core
imandra.instance
imandra.ipl
imandra.rule_synth
Functions
def main()
-
Expand source code
def main(): import sys import argparse parser = argparse.ArgumentParser(prog="imandra", description="Imandra CLI") parser.set_defaults(run=lambda args: parser.print_help()) subparsers = parser.add_subparsers() auth = Auth() parser_auth = subparsers.add_parser('auth') parser_auth.set_defaults(run=lambda args: parser_auth.print_help()) parser_auth_subparsers = parser_auth.add_subparsers() def login(args): auth.login() print("Logged in") parser_login = parser_auth_subparsers.add_parser('login') parser_login.set_defaults(run=login) def logout(args): auth.logout() print("Logged out") parser_logout = parser_auth_subparsers.add_parser('logout') parser_logout.set_defaults(run=logout) parser_export = parser_auth_subparsers.add_parser('export') parser_export.set_defaults(run=lambda args: auth.export()) parser_import = parser_auth_subparsers.add_parser('import') parser_import.set_defaults(run=lambda args: auth.import_()) parser_ipl = subparsers.add_parser('ipl') parser_ipl.set_defaults(run=lambda args: parser_ipl.print_help()) parser_ipl_subparsers = parser_ipl.add_subparsers() def ipl_decompose(args): if args.file is not None and args.parent_job_id is not None: print("error: --file and --parent-job-id are mutually exclusive operations. " "You must pick one or the other") sys.exit(1) if args.file is None and args.parent_job_id is None: print ('error: --file must be provided') else: ipl.decompose(auth, args.file, args.testgen_lang, args.organization, args.callback, args.doc_gen, args.parent_job_id) parser_ipl_decompose = parser_ipl_subparsers.add_parser('decompose') parser_ipl_decompose.add_argument('--file') parser_ipl_decompose.add_argument('--callback') parser_ipl_decompose.add_argument('--testgen-lang', help=argparse.SUPPRESS) parser_ipl_decompose.add_argument('--organization') parser_ipl_decompose.add_argument('--doc-gen', choices=['true','false'], default='true') parser_ipl_decompose.add_argument('--parent-job-id', help=("The id of a previously completed job. Instead of running a " "full decomposition, re-run just the script generation phase of " "this parent-job. When using this option all other options will be " "ignore and the original values from the parent-job will be used.")) parser_ipl_decompose.set_defaults(run=ipl_decompose) def ipl_simulator(args): if args.file is None: print ('error: --file must be provided') else: ipl.simulator(auth, args.file) parser_ipl_simulator = parser_ipl_subparsers.add_parser('simulator') parser_ipl_simulator.add_argument('--file') parser_ipl_simulator.set_defaults(run=ipl_simulator) def ipl_status(args): if args.uuid is None: print ('error: --uuid must be provided') else: ipl.status(auth, args.uuid) parser_ipl_status = parser_ipl_subparsers.add_parser('status') parser_ipl_status.add_argument('--uuid') parser_ipl_status.set_defaults(run=ipl_status) def ipl_data(args): if args.uuid is None: print ('error: --uuid must be provided') else: ipl.data(auth, args.uuid) parser_ipl_decompose = parser_ipl_subparsers.add_parser('data') parser_ipl_decompose.add_argument('--uuid') parser_ipl_decompose.set_defaults(run=ipl_data) parser_ipl_jobs = parser_ipl_subparsers.add_parser('list-jobs') parser_ipl_jobs.set_defaults(run=lambda args: ipl.list_jobs(auth)) def ipl_cancel(args): if args.uuid is None: print ('error: --uuid must be provided') else: ipl.cancel(auth, args.uuid) parser_ipl_cancel = parser_ipl_subparsers.add_parser('cancel') parser_ipl_cancel.add_argument('--uuid') parser_ipl_cancel.set_defaults(run=ipl_cancel) parser_core = subparsers.add_parser('core') parser_core.set_defaults(run=lambda args: parser_core.print_help()) parser_core_subparsers = parser_core.add_subparsers() parser_instances = parser_core_subparsers.add_parser('instances') parser_instances.set_defaults(run=lambda args: parser_instances.print_help()) parser_instances_subparsers = parser_instances.add_subparsers() parser_instances_list = parser_instances_subparsers.add_parser('list') parser_instances_list.set_defaults(run=lambda args: instance.list(auth)) def create_instance(args): if args.instance_type is None: print ('error: --instance-type must be provided') else: instance.create(auth, args.version, args.instance_type) parser_instances_create = parser_instances_subparsers.add_parser('create') parser_instances_create.add_argument('--instance-type') parser_instances_create.add_argument('--version') parser_instances_create.set_defaults(run=create_instance) def kill_instance(args): if args.id is None: print ('error: --id must be provided') else: instance.delete(auth, args.id) parser_instances_kill = parser_instances_subparsers.add_parser('kill') parser_instances_kill.add_argument('--id') parser_instances_kill.set_defaults(run=kill_instance) def rule_synth(args): if args.file is None: print ('error: --file must be provided') else: rule_synth.synth(auth, args.file) parser_rule_synth = subparsers.add_parser('rule-synth') parser_rule_synth.set_defaults(run=lambda args: parser_rule_synth.print_help()) parser_rule_synth_subparsers = parser_rule_synth.add_subparsers() parser_synth = parser_rule_synth_subparsers.add_parser('synth') parser_synth.add_argument('--file') parser_synth.set_defaults(run=rule_synth) def cfb_analyze(args): if args.job is None: print ('error: --job must be provided') else: if args.path is None: print ('error: --path must be provided') else: cfb.analyze(auth, args.job, args.path) parser_cfb = subparsers.add_parser('cfb') parser_cfb.set_defaults(run=lambda args: parser_cfb.print_help()) parser_cfb_subparsers = parser_cfb.add_subparsers() parser_cfb_analyze = parser_cfb_subparsers.add_parser('analyze') parser_cfb_analyze.add_argument('--job') parser_cfb_analyze.add_argument('--path') parser_cfb_analyze.set_defaults(run=cfb_analyze) def repl(args): core.run_repl(auth, args.args) parser_repl = parser_core_subparsers.add_parser('repl') parser_repl.add_argument('args', nargs=argparse.REMAINDER) parser_repl.set_defaults(run=repl) def install_imandra_core(args): core.install(auth) parser_install = parser_core_subparsers.add_parser('install') parser_install.set_defaults(run=install_imandra_core) if len(sys.argv) > 2 and sys.argv[1] == 'core' and sys.argv[2] == 'repl': # Run this directly so we can pass --help directly to the repl command to see its own help text core.run_repl(auth, sys.argv[3:]) else: args = parser.parse_args() args.run(args)
def session()
-
Expand source code
def session(): return HttpInstanceSession()