remake_packages.py

#!/usr/bin/env python
from __future__ import with_statement
import re, os
import io

PACKAGE_NAMES = [('../CurveParameters.v', [])]
CP_LIST = ['../CurveParametersPackage.v']
CP_BASE_LIST = ['../CurveParametersPackage.v', 'BasePackage.v']
CP_BASE_DEFAULTS_LIST = ['../CurveParametersPackage.v', 'BasePackage.v', 'DefaultsPackage.v']
CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST = ['../CurveParametersPackage.v', 'BasePackage.v', 'DefaultsPackage.v', 'FreezePackage.v', 'LadderstepPackage.v']
NORMAL_PACKAGE_NAMES = [('Base.v', (CP_LIST, None)),
                        ('Defaults.v', (CP_BASE_LIST, 'not_exists')),
                        ('../ReificationTypes.v', (CP_BASE_LIST, None)),
                        ('Freeze.v', (CP_BASE_LIST, ('freeze', 'not_exists'))),
                        ('Ladderstep.v', (CP_BASE_DEFAULTS_LIST, ('ladderstep', 'not_exists'))),
                        ('Karatsuba.v', (CP_BASE_DEFAULTS_LIST, 'goldilocks')),
                        ('Montgomery.v', (CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST, 'montgomery')),
                        ('../MontgomeryReificationTypes.v', (CP_BASE_LIST + ['MontgomeryPackage.v', '../ReificationTypesPackage.v'], 'montgomery'))]
ALL_FILE_NAMES = PACKAGE_NAMES + NORMAL_PACKAGE_NAMES # PACKAGE_CP_NAMES + WITH_CURVE_BASE_NAMES + ['../ReificationTypes.v']
CONFIGS = ('goldilocks', 'karatsuba', 'montgomery', 'freeze', 'ladderstep')

EXCLUDES = ('constr:((wt_divides_chain, wt_divides_chains))', )

contents = {}
lines = {}
fns = {}

PY_FILE_NAME = os.path.basename(__file__)

def init_contents(lines=lines, contents=contents):
    for fname, _ in ALL_FILE_NAMES:
        with open(fname, 'r') as f:
            contents[fname] = f.read()
    lines.update(dict((k, v.split('\n')) for k, v in contents.items()))

def strip_prefix(name, prefix='local_'):
    if name.startswith(prefix): return name[len(prefix):]
    return name

def init_fns(lines=lines, fns=fns):
    header = 'Ltac pose_'
    for fname, _ in ALL_FILE_NAMES:
        stripped_lines = [i.strip() for i in lines[fname]]
        fns[fname] = [(strip_prefix(name, 'local_'), args.strip(), name.startswith('local_'))
                      for line in stripped_lines
                      if line.startswith(header)
                      for name, args in re.findall('Ltac pose_([^ ]*' + ') ([A-Za-z0-9_\' ]*' + ')', line.strip())]

def get_file_root(folder=os.path.dirname(__file__), filename='Makefile'):
    dir_path = os.path.realpath(folder)
    while not os.path.isfile(os.path.join(dir_path, filename)) and dir_path != '/':
        dir_path = os.path.realpath(os.path.join(dir_path, '..'))
    if not os.path.isfile(os.path.join(dir_path, filename)):
        print('ERROR: Could not find Makefile in the root of %s' % folder)
        raise Exception
    return dir_path

def modname_of_file_name(fname):
    assert(fname[-2:] == '.v')
    return 'Crypto.' + os.path.normpath(os.path.relpath(os.path.realpath(fname), os.path.join(root, 'src'))).replace(os.sep, '.')[:-2]

def split_args(name, args_str, indent=''):
    args = [arg.strip() for arg in args_str.split(' ')]
    pass_args = [arg for arg in args if arg.startswith('P_')]
    extract_args = [arg for arg in args if arg not in pass_args and arg != name]
    if name not in args:
        print('Error: %s not in %s' % (name, repr(args)))
        assert(name in args)
    assert(len(pass_args) + len(extract_args) + 1 == len(args))
    pass_args_str = ' '.join(pass_args)
    if pass_args_str != '': pass_args_str += ' '
    extract_args_str = ''
    nl_indent = ('\n%(indent)s  ' % locals())
    if len(extract_args) > 0:
        extract_args_str = nl_indent + nl_indent.join('let %s := Tag.get pkg TAG.%s in' % (arg, arg) for arg in extract_args)
    return args, pass_args, extract_args, pass_args_str, extract_args_str

def make_add_from_pose(name, args_str, indent='', only_if=None, local=False):
    args, pass_args, extract_args, pass_args_str, extract_args_str = split_args(name, args_str, indent=indent)
    ret = r'''%(indent)sLtac add_%(name)s pkg %(pass_args_str)s:=''' % locals()
    local_str = ('local_' if local else '')
    if_not_exists_str = ''
    body = r'''%(extract_args_str)s
%(indent)s  let %(name)s := fresh "%(name)s" in
%(indent)s  ''' % locals()
    body += r'''let %(name)s := pose_%(local_str)s%(name)s %(args_str)s in
%(indent)s  ''' % locals()
    if only_if == 'not_exists':
        assert(not local)
        body += 'constr:(%(name)s)' % locals()
        body = body.strip('\n ').replace('\n', '\n                 ')
        ret += r'''
%(indent)s  Tag.update_by_tac_if_not_exists
%(indent)s    pkg
%(indent)s    TAG.%(name)s
%(indent)s    ltac:(fun _ => %(body)s).''' % locals()
    else:
        if isinstance(only_if, tuple) and 'not_exists' in only_if:
            only_if = [i for i in only_if if i != 'not_exists']
            assert(len(only_if) == 1)
            only_if = only_if[0]
            body += 'constr:(%(name)s)' % locals()
            body = body.strip('\n ').replace('\n', '\n                   ')
            body = r'''Tag.update_by_tac_if_not_exists
%(indent)s      pkg
%(indent)s      TAG.%(name)s
%(indent)s      ltac:(fun _ => %(body)s).''' % locals()
        else:
            body += r'''Tag.%(local_str)supdate pkg TAG.%(name)s %(name)s''' % locals()
        if only_if is None:
            ret += body + '.\n'
        else:
            body = body.strip('\n .').replace('\n', '\n                 ')
            ret += r'''
%(indent)s  if_%(only_if)s
%(indent)s    pkg
%(indent)s    ltac:(fun _ => %(body)s)
%(indent)s    ltac:(fun _ => pkg)
%(indent)s    ().''' % locals()
    return ret

def make_add_all(fname, indent=''):
    modname, ext = os.path.splitext(os.path.basename(fname))
    all_items = [(name, split_args(name, args_str, indent=indent)) for name, args_str, local in fns[fname]]
    all_pass_args = []
    for name, (args, pass_args, extract_args, pass_args_str, extract_args_str) in all_items:
        for arg in pass_args:
            if arg not in all_pass_args: all_pass_args.append(arg)
    all_pass_args_str = ' '.join(all_pass_args)
    if all_pass_args_str != '': all_pass_args_str += ' '
    ret = r'''%(indent)sLtac add_%(modname)s_package pkg %(all_pass_args_str)s:=''' % locals()
    nl_indent = ('\n%(indent)s  ' % locals())
    ret += nl_indent + nl_indent.join('let pkg := add_%s pkg %sin' % (name, pass_args_str)
                                      for name, (args, pass_args, extract_args, pass_args_str, extract_args_str) in all_items)
    ret += nl_indent + 'Tag.strip_subst_local pkg.\n'
    return ret

def make_if(name, indent=''):
    ret = r'''%(indent)sLtac if_%(name)s pkg tac_true tac_false arg :=
%(indent)s  let %(name)s := Tag.get pkg TAG.%(name)s in
%(indent)s  let %(name)s := (eval vm_compute in (%(name)s : bool)) in
%(indent)s  lazymatch %(name)s with
%(indent)s  | true => tac_true arg
%(indent)s  | false => tac_false arg
%(indent)s  end.
''' % locals()
    return ret

def write_if_changed(fname, value):
    if os.path.isfile(fname):
        with open(fname, 'r') as f:
            old_value = f.read()
        if old_value == value: return
    value = unicode(value)
    print('Writing %s...' % fname)
    with io.open(fname, 'w', newline='\n') as f:
        f.write(value)

def do_replace(fname, headers, new_contents):
    lines = contents[fname].split('\n')
    ret = []
    for line in lines:
        if any(header in line for header in headers):
            ret.append(new_contents)
            break
        else:
            ret.append(line)
    ret = unicode('\n'.join(ret))
    write_if_changed(fname, ret)

def get_existing_tags(fname, deps):
    return set(name for dep in deps for name, args, local in fns[dep.replace('Package.v', '.v')])

def make_package(fname, deps, extra_modname_prefix='', extra_imports=None, prefix=None, add_package=True):
    py_file_name = PY_FILE_NAME
    existing_tags = get_existing_tags(fname, deps)
    full_mod = modname_of_file_name(fname)
    modname, ext = os.path.splitext(os.path.basename(fname))
    ret = (r'''(* This file is autogenerated from %(modname)s.v by %(py_file_name)s *)
''' % locals())
    if extra_imports is not None:
        ret += extra_imports
    ret += (r'''Require Export %(full_mod)s.
Require Import Crypto.Specific.Framework.Packages.
Require Import Crypto.Util.TagList.
''' % locals())
    if prefix is not None:
        ret += prefix
    new_names = [name for name, args, local in fns[fname] if name not in existing_tags and not local]
    if add_package: # and len(new_names) > 0:
        ret += (r'''

Module Make%(extra_modname_prefix)s%(modname)sPackage (PKG : PrePackage).
  Module Import Make%(extra_modname_prefix)s%(modname)sPackageInternal := MakePackageBase PKG.
''' % locals())
        for name in new_names:
            ret += ("\n  Ltac get_%s _ := get TAG.%s." % (name, name))
            ret += ("\n  Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (name, name))
        ret += ('\nEnd Make%(extra_modname_prefix)s%(modname)sPackage.\n' % locals())
    return ret

def make_tags(fname, deps):
    existing_tags = get_existing_tags(fname, deps)
    new_tags = [name for name, args, local in fns[fname] if name not in existing_tags]
    if len(new_tags) == 0: return ''
    names = ' | '.join(new_tags)
    return r'''Module TAG.
  Inductive tags := %s.
End TAG.
''' % names

def write_package(fname, pkg):
    pkg_name = fname[:-2] + 'Package.v'
    write_if_changed(pkg_name, pkg)

def update_CurveParameters(fname='../CurveParameters.v'):
    endline = contents[fname].strip().split('\n')[-1]
    assert(endline.startswith('End '))
    header = '(* Everything below this line autogenerated by %s *)' % PY_FILE_NAME
    assert(header in contents[fname])
    ret = '  %s' % header
    for name, args, local in fns[fname]:
        ret += '\n' + make_add_from_pose(name, args, indent='  ', local=local)
    ret += '\n' + make_add_all(fname, indent='  ')
    ret += endline + '\n'
    prefix = ''
    for name in CONFIGS:
        prefix += '\n' + make_if(name, indent='')
    pkg = make_package(fname, [], prefix=prefix)
    do_replace(fname, (header,), ret)
    write_package(fname, pkg)

def make_normal_package(fname, deps, only_if=None):
    prefix = ''
    extra_imports = ''
    for dep in deps:
        extra_imports += 'Require Import %s.\n' % modname_of_file_name(dep)
    prefix += '\n' + make_tags(fname, deps)
    for name, args, local in fns[fname]:
        prefix += '\n' + make_add_from_pose(name, args, indent='', only_if=only_if, local=local)
    prefix += '\n' + make_add_all(fname, indent='')
    return make_package(fname, deps, extra_imports=extra_imports, prefix=prefix)

def update_normal_package(fname, deps, only_if=None):
    pkg = make_normal_package(fname, deps, only_if=only_if)
    write_package(fname, pkg)

root = get_file_root()
init_contents()
init_fns()
update_CurveParameters()
for fname, (deps, only_if) in NORMAL_PACKAGE_NAMES:
    update_normal_package(fname, deps, only_if=only_if)