get_theorem.py (1848B)
1 #!/usr/bin/python 2 3 import sys 4 5 readif = False 6 readif_and = False 7 readthen = False 8 readthen_and = False 9 10 ifs = [] 11 thens = [] 12 13 def myfmt(x, pol=1): 14 if x[1] == ("true" if pol==1 else "false"): 15 return x[0] 16 else: 17 assert(x[1] == "false" if pol==1 else "true") 18 return "-" + x[0] 19 20 def parse_one(l, pref=" "): 21 assert(l[0:len(pref)] == pref) 22 f = l[len(pref):].split(":") 23 p = f[0].strip() 24 pp = f[1].strip() 25 assert(p.startswith("P")) 26 assert(pp in ["true", "false"]) 27 return (p, pp) 28 29 for l in sys.stdin.readlines(): 30 assert(l[-1] == '\n') 31 l = l[:-1] 32 if l == "if:": 33 assert(not readif) 34 assert(not readthen) 35 readif = True 36 continue 37 if l == " and:" and readif: 38 assert(not readif_and) 39 readif_and = True 40 continue 41 if l == "then:": 42 readif = False 43 assert(not readthen) 44 assert(len(ifs) > 0) 45 readthen = True 46 continue 47 if l == " and:" and readthen: 48 assert(not readthen_and) 49 readthen_and = True 50 continue 51 if not readif and not readthen: 52 continue 53 if readif: 54 if not readif_and: 55 assert(len(ifs) == 0) 56 ifs.append(parse_one(l)) 57 readif = False 58 else: 59 if not l.startswith(" "): 60 readif = False 61 else: 62 ifs.append(parse_one(l, pref=" - ")) 63 if readthen: 64 if not readthen_and: 65 assert(len(thens) == 0) 66 thens.append(parse_one(l)) 67 readthen = False 68 else: 69 if not l.startswith(" "): 70 readthen = False 71 else: 72 thens.append(parse_one(l, pref=" - ")) 73 74 for t in thens: 75 print sys.argv[1], ' '.join([myfmt(x, pol=-1) for x in ifs]), myfmt(t) 76 77 78