#!/usr/bin/env python3

import re
import sys

types = [
  "InstructionM64",
  "InstructionM",
  "InstructionI64",
  "InstructionI",
  "InstructionCSR",
  "InstructionA64",
  "InstructionA",
  "InstructionF64",
  "InstructionF",
]

def ends_with_colon_instruction(s):
    for tp in types:
        if s.endswith(":" + tp):
            return True
    return False

print(f"""(* File generated by {sys.argv[0]}, do not edit *)
Require Export riscv.Spec.Decode.
Require Export riscv.Utility.InstructionCoercions.
Require Export riscv.Utility.RegisterNameNotations.

Notation "'RISCV:' x y .. z" :=
  (@cons Instruction x (@cons Instruction y .. (@cons Instruction z nil) ..))
  (at level 10, format "'RISCV:' x y .. z '//'").
""")

with open('./src/riscv/Spec/Decode.v', 'r') as file:
    chunks = file.read().replace('\n', '').replace(' ', '').split('|')
    ctors = filter(ends_with_colon_instruction, chunks)
    for s in ctors:
        s = re.sub(":Instruction[^:]+$", "", s)
        parts = s.replace(')', '').split('(')
        iname = parts[0]
        argtuples = [part.split(':') for part in parts[1:]]
        if len(argtuples) == 0:
            print(f"""Notation "'{iname.lower()}'" := {iname} (at level 10, format "'//'     '{iname.lower()}'").""")
        else:
            argnames = [argname for [argname, argtype] in argtuples]
            print(f"""Notation "'{iname.lower()}' {' , '.join(argnames)}" := ({iname} {' '.join(argnames)})
  (at level 10, {', '.join([argname + (' custom register_name' if argtype == 'Register' else ' constr at level 35') for [argname, argtype] in argtuples])},
   format "'//'     '{iname.lower()}'{' ' * (7 - len(iname))}  {' ,  '.join(argnames)}").""")
