import json
import os
import time
import re

def save_error_log(
  theorem, 
  error_log,
  save_dir='',
  file_format = 'log'
  ):
  theorem_name = theorem
  time_postfix = int(time.time())
  save_path = os.path.join(save_dir,f"{theorem_name}_{time_postfix}.{file_format}")
  assert file_format == 'json'

  assert isinstance(error_log,dict)
  if 'parse_itactic failed' not in error_log['Error']:
    json.dump(error_log,open(save_path,'w'))
  

def save_informal_log(informal_sample, theorem_name, save_dir='db/informal_db'):
  # theorem_name = error_sample.split()[1]
  time_postfix = int(time.time())
  save_path = os.path.join(save_dir,f"{theorem_name}_{time_postfix}.log")
  with open(save_path,'w') as fout:
    fout.write(informal_sample+'\n')


def save_pseudo_log(pseudo_code, theorem_name, save_dir="db/pseudo_db"):
  time_postfix = int(time.time())
  save_path = os.path.join(save_dir,f"{theorem_name}_{time_postfix}.log")
  with open(save_path,'w') as fout:
    fout.write(pseudo_code+'\n')