FormalSystemsMain.py

#!/usr/bin/python
# -*- coding: utf-8 -*-

import sys
import argparse

from formalsystems.formalsystems import FormalSystem, Theorem




def main():

    parser = argparse.ArgumentParser(description='Formal system processor.')

    parser.add_argument('yaml_file', 
                        metavar='file', 
                        type=str, 
                        help='path to YAML definition of the formal system')

    parser.add_argument('-d', '--derivation', 
                        dest='theorem', 
                        type=Theorem,
                        default=None,
                        help='print theorem derivation')

    parser.add_argument('-s', '--schema', 
                        action='store_true',
                        default=None,
                        help='iteration over axioms schema')

    parser.add_argument('-a', '--axiom', 
                        dest='axiom', 
                        type=Theorem,
                        default=None,
                        help='check axiom definition')

    parser.add_argument('-i', '--iteration', 
                        type=int,
                        default=10,
                        help='define max iteration (default 10)')

    parser.add_argument('-q', '--quiet', 
                        action='store_true',
                        help='quiet mode')

    args = parser.parse_args()
    #print args

    fs = FormalSystem()
    fs.read_formal_system(args.yaml_file)

    has_wildcards  = lambda schema: schema.wildcards
    has_multi_rule = lambda rule: len(rule.oldts) > 1

    infinite_axioms = any(map(has_wildcards,  fs.axioms))
    and_in_rule     = any(map(has_multi_rule, fs.rules))

    if args.schema is not None:
        print '> Generating axioms schema'

        for ax in fs.iterate_over_schema(max=args.iteration):
            print ax
        exit()

    if args.axiom is not None:
        fs.is_axiom(args.axiom, verbose=not(args.quiet))
        exit()


    if infinite_axioms:
        print '> Infinite number of axioms, using bucket algorithm'
    else:
        print '> Finite number of axioms, using step algorithm'

    if and_in_rule:
        print '> Rule with several parents, using recursivity'
    print

    # Main
    if args.theorem is None:

        if infinite_axioms:
            fs.apply_rules_bucket_till(fs.iterate_over_schema(), 
                                       min_len=None, # wont apply 
                                       max_turns=args.iteration, 
                                       full=and_in_rule,
                                       verbose=not(args.quiet))
        else:
            ths = fs.apply_rules_step(fs.iterate_over_schema(), 
                                      step=args.iteration,
                                      verbose=not(args.quiet))
    else:
        if infinite_axioms:
            fs.derivation_asc(fs.iterate_over_schema(), 
                              args.theorem, 
                              max_turns=args.iteration, 
                              full=and_in_rule,
                              verbose=not(args.quiet))
        else:
            fs.derivation_step(fs.iterate_over_schema(),
                               args.theorem, 
                               step=args.iteration,
                               verbose=not(args.quiet))


if __name__ == '__main__':
    main()