6.16.10.3. Code generator

    48: #line 63 "python_tangler.ipk"
    49: def tangle_precondition(indent, precondition):
    50:   return ' ' * indent + 'assert ' + precondition + '\n'
    51: 
    52: def tangle_postcondition(indent, postcondition):
    53:   return ' ' * indent + 'assert ' + postcondition + '\n'
    54: 
    55: def tangle_argument_check(indent, argument):
    56:   code = ''
    57:   if argument.protocol:
    58:     code = code + ' '* indent + 'assert has_protocol('+\
    59:       argument.name + ', '+ argument.protocol + ')\n'
    60:   return code
    61: 
    62: def tangle_argument_checks(indent, arguments):
    63:   code = ''
    64:   for argument in arguments:
    65:     code = code + tangle_argument_check(indent, argument)
    66:   return code
    67: 
    68: def tangle_argument(argument):
    69:   code = argument.name
    70:   if argument.default: code = code + '='+argument.default
    71:   return code
    72: 
    73: def tangle_arguments(indent, arguments):
    74:   code = ''
    75:   for argument in arguments[:-1]:
    76:     code = code + ' '*indent + tangle_argument(argument)
    77:     code = code + ',\n'
    78:   code = code + ' '*indent + tangle_argument(arguments[-1])
    79:   return code
    80: 
    81: def tangle_result(indent, results):
    82:   code = ''
    83:   for result in results:
    84:     if result.protocol:
    85:       code = code + ' '*indent + 'assert has_protocol(' +\
    86:         result.name+', '+ result.protocol+')\n'
    87:   code = code + ' '*indent + 'return '
    88:   for result in results[:-1]:
    89:     code = code + result.name + ', '
    90:   code = code + results[-1].name+'\n'
    91:   return code
    92: 
    93: def tangle_function(
    94:   sink,
    95:   source_file,
    96:   source_line,
    97:   indent,
    98:   name,
    99:   description=None,
   100:   arguments=None,
   101:   precondition=None,
   102:   result=None,
   103:   postcondition=None,
   104:   initial=None,
   105:   final=None,
   106:   body=None):
   107: 
   108:   # argument list
   109:   code = ' '* indent + 'def '+name
   110:   if arguments:
   111:     code = code + '(\n'
   112:     code = code + tangle_arguments(indent+2, arguments)
   113:     code = code + '):\n'
   114:   else: code = code + '():\n'
   115: 
   116:   # argument checks
   117:   if arguments:
   118:     code = code + ' ' * (indent + 2) + '#check arguments\n'
   119:     code = code + tangle_argument_checks(indent+2, arguments)
   120: 
   121:   # precondition
   122:   if precondition:
   123:     code = code + ' ' * (indent + 2) + '#precondition\n'
   124:     code = code + tangle_precondition(indent+2, precondition)
   125: 
   126:   # begin try/finally block
   127:   code = code + ' '* (indent+2) + 'try:\n'
   128: 
   129:   # initial
   130:   if initial:
   131:     code = code + ' ' * (indent + 4) + '#initially\n'
   132:     for line in initial:
   133:       code = code + ' ' * (indent+4) + line + '\n'
   134: 
   135:   # begin try/except block
   136:   code = code + ' '* (indent+4) + 'try:\n'
   137: 
   138:   # body
   139:   if body:
   140:     code = code + ' ' * (indent + 6) + '#body\n'
   141:     for line in body:
   142:       code = code + ' ' * (indent+6) + line + '\n'
   143: 
   144: 
   145:   # exception
   146:   code = code + ' ' * (indent + 4) + '#transmit user exceptions\n'
   147:   code = code + ' ' * (indent +4) + 'except: raise\n'
   148:   code = code + ' ' * (indent +4) + 'else:\n'
   149: 
   150: 
   151:   # postcondition
   152:   if postcondition:
   153:     code = code + ' ' * (indent + 6) + '#postcondition\n'
   154:     code = code + tangle_postcondition(indent + 6, postcondition)
   155: 
   156: 
   157:   # result
   158:   if result:
   159:     code = code + ' ' * (indent + 6) + '#return result\n'
   160:     code = code + tangle_result(indent + 6, result)
   161:   else: code = code + ' ' * (indent+6) + 'pass\n'
   162: 
   163:   # finally
   164:   code = code + ' ' * (indent + 2) + '#cleanup\n'
   165:   code = code + ' '* (indent+2) + 'finally:\n'
   166:   if final:
   167:     for line in final:
   168:       code = code + ' ' * (indent+4) + line + '\n'
   169:   else:
   170:     code = code + ' ' * (indent+4) + 'pass\n'
   171: 
   172:   for line in string.split(code,'\n')[:-1]:
   173:     sink.writeline(line)
   174:   return code
   175: